Add support for temporal mixing of atomic and non-atomic accesses in GenMC mode #4611
Conversation
|
Thank you for contributing to Miri! |
There was a problem hiding this comment.
Feels a bit arbitrary to use this random existing test to check the thread::spawn APIs. This is fully subsumed by tests/genmc/pass/thread/spawn_std_threads.rs, isn't it?
There was a problem hiding this comment.
Yeah we don't need it, I've removed the changes.
| // FIXME(genmc,HACK): remove this initializing write once Miri-GenMC supports mixed atomic-non-atomic accesses. | ||
| x.store(123, ORD); | ||
|
|
||
| // MAX, ADD |
There was a problem hiding this comment.
Looks like you removed a bit too much here, this comment should stay.
There was a problem hiding this comment.
arc isn't really a "primitive". It's just a library construct.
Maybe have a folder std to check various std things (main, thread::spawn, thread_local, Arc)? Those tests should all use normal Rust APIs then, no pthread APIs and no miri_start.
There was a problem hiding this comment.
Done. Are there any existing tests that should be in the genmc/pass/std/ directory, e.g., pass/thread/thread_locals.rs?
Also, my next PR will be std::sync::Mutex interception, should tests for that be in the pass/intercept or the pass/std directory?
There was a problem hiding this comment.
Are there any existing tests that should be in the genmc/pass/std/ directory, e.g., pass/thread/thread_locals.rs?
Yeah that one would make sense to move.
Also, my next PR will be std::sync::Mutex interception, should tests for that be in the pass/intercept or the pass/std directory?
Hm, no strong opinion. intercept is fine.
There was a problem hiding this comment.
As I said above:
Those tests should all use normal Rust APIs then, no pthread APIs and no miri_start.
|
@rustbot author |
rustbot
added
S-waiting-on-author
|
Reminder, once the PR becomes ready for a review, use |
|
This looks great, thanks! Please squash the commits using @rustbot author |
…n GenMC mode. Remove atomic initialization dummy writes from tests.
Patrick-6
force-pushed
the
miri-genmc-temporal-mixing
branch
from
28acc86 to
57a7380
Compare
|
@rustbot ready |
rustbot
added
S-waiting-on-review
This PR switches to using a new GenMC commit containing a temporary implementation of temporal mixing of atomics/non-atomics in GenMC. The API for this change should be identical to the one that will be in the official GenMC release once it is ready.
Which this PR, initializing writes are no longer required and were removed from all tests.
We can now also support using
fn main() {}andstd::sync::Arcin GenMC mode!