Add compare_exchange support for GenMC mode #4578
Conversation
rustbot
added
the
S-waiting-on-author
|
r? @RalfJung I have more tests that use |
src/concurrency/genmc/mod.rs
Outdated
| warnings_cache.warn_once_rmw_failure_ordering( | ||
| ecx, | ||
| success, | ||
| upgraded_success_ordering, | ||
| fail, | ||
| ); |
There was a problem hiding this comment.
Please have the logic that decides whether we will warn here, instead of splitting it across files.
I don't think you need an entire file for this, all you need is something like
type WarningCache = RwLock<FxHashSet<Span>>;
fn emit_warning(cache: &WarningCache, diagnostic: impl FnOnce() -> NonHaltingDiagnostic) { ... }|
|
||
| // Translated from GenMC's test `wrong/racy/MPU2+rels+rlx`. | ||
| // Test if Miri with GenMC can detect the data race on `X`. | ||
| // The data race only occurs if thread 1 finishes, then threads 3 and 4 run, then thread 1. |
There was a problem hiding this comment.
One of the 1 here should be a 2 I assume?
There was a problem hiding this comment.
Yes, one at the end.
tests/genmc/pass/litmus/casdep.rs
Outdated
There was a problem hiding this comment.
What is this test about? Please at least link to the corresponding GenMC test.
Same for ccr and cii.
Also, none of the actually concurrent tests are checking the values we are seeing, would one of them be suited for that?
There was a problem hiding this comment.
I'll add result printing to the MPU2_rels_acqf test.
| Y.store(1, Relaxed); | ||
| }); | ||
| spawn_pthread_closure(|| { | ||
| let expected = 2; |
There was a problem hiding this comment.
Please inline these trivial let-bindings that are only used once (in all tests).
There was a problem hiding this comment.
Ah these are some leftovers from C/C++, where the compare_exchange functions take a pointer/reference, so they can update the expected value ^^
|
@rustbot ready |
rustbot
added
S-waiting-on-review
|
That CI failure doesn't look like it is caused by my change? |
|
Yeah, the Ubuntu repos are having some sort of trouble. |
|
Please rebase, that should fix the CI. |
|
Oh and you can also squash the commits, this is ready otherwise. :) |
- Handling Compare-Exchange operations.
- Limitation: Compare-Exchange currently ignores possibility of spurious failures.
- Limitation: Compare-Exchange failure memory ordering is ignored.
- Upgrade compare-exchange success ordering to avoid reporting non-existent bugs.
- Add warnings for GenMC mode for unsupported features.
- Add a lot of tests, including translation of GenMC litmus tests and Loom tests.
- Cleanup
Patrick-6
force-pushed
the
miri-genmc-cas
branch
from
9fb7383 to
a00b17a
Compare
|
This PR was rebased onto a different master commit. Here's a range-diff highlighting what actually changed. Rebasing is a normal part of keeping PRs up to date, so no action is needed—this note is just to help reviewers. |
Followup to #4566 and #4506.
This PR adds support for using
compare_exchange{_weak}for GenMC mode, and adds code to emit warnings in cases where bugs may be missed. This includes the missing support for spurious failures for the weak variant, and missing modelling for the failure memory ordering leading to certain executions that cannot be explored.This PR also adds tests
compare_exchange.