Add minimal functionality for using GenMC mode #4506
Conversation
rustbot
added
the
S-waiting-on-author
- Add genmc-sys crate for building GenMC C++ code.
- Implemented program features:
- Handling of atomic loads, stores, allocations and deallocations.
- Implement consistent address allocations for globals
- Non-global addresses allocated by GenMC.
- Limitation: No address randomization.
- Limitation: No address reuse.
- Handling of non-atomic memory accesses.
- Limitation: need to split up NA reads and stores into max 8 byte chunks.
- Limitation: no mixed size access support.
- Limitation: Incomplete (unsound) handling of uninitialized memory.
- Implement Pointer conversions to and from GenMC
- Limitation: Aliasing model checking must be disabled.
- Handling of Read-Modify-Write, Compare-Exchange and Atomic Exchange operations.
- Limitation: Compare-Exchange currently ignores possibility of spurious failures.
- Limitation: Compare-Exchange failure memory ordering is ignored.
- Handling of thread creation and finishing.
- Added Miri to GenMC thread id mapping.
- Implement mutex lock, try_lock and unlock.
- Make use of annotations to reduce number of blocked executions for programs with mutexes.
- Add estimation mode for Miri-GenMC.
- Limitation: Printing currently handled on C++ side (Should be moved once VerificationResult is available to Rust code)
- Thread scheduling in Miri done through GenMC, add loop over eval_entry function.
- Rebase GenMC to use new scheduler.
- Added GenMC `__VERIFIER_assume` equivalent for Miri (`miri_genmc_verifier_assume`)
- Add warnings for GenMC mode for unsupported features.
- Add a lot of test, including translation of GenMC litmus tests.
- Only run tests if 'genmc' feature enabled.
- WIP: try implementing NonNullUniquePtr wrapper for CXX.
- WIP: work on mixed atomic/non-atomics.
- Partially working, some issues with globals
- FIX: Make naming consistent with GenMC for blocked execution
Squashed changes:
- Add git support to build, move C++ files into genmc-sys crate
- Implement building GenMC-Miri after GenMC codebase split.
- Cleanup genmc-sys build, remove walkdir dependency.
- Fix printing after LLVM IO removal.
- WIP: temporarily point GenMC repo to private branch.
- WIP: Work on building without LLVM dependency.
- Fix build for Ubuntu 22
- Disable stacked borrows for GenMC tests
- Get Miri-GenMC building again after rebasing onto GenMC release 0.12.0
- Translate some Loom tests for Miri-GenMC.
- Add error for using native-lib with GenMC mode.
- Remove on_stack_empty handling except for main thread.
- Rename 'stuck' to 'blocked' to be in line with GenMC terminology.
- Enable tests that were blocked on rust-lang #116707
- Remove redundant file in compilation step.
- Clean up InterpResult<'tcx, ()>
- Improve program exit handling, remove 'thread_stack_empty' hack, clean up terminator cache leftovers.
Patrick-6
force-pushed
the
miri-genmc-mvp
branch
from
7c34fc3 to
37e652f
Compare
Patrick-6
force-pushed
the
miri-genmc-mvp
branch
from
37e652f to
5104d08
Compare
|
I'll add some comments on the PR later in places that need discussion or that might need to change (since they are based on changes not yet merged into GenMC). There is also some C++ code that is currently in my fork of GenMC, but makes more sense to move to the Miri repo (e.g., error handling code). The Rust side should be ready for reviewing. r? @RalfJung |
| #[derive(Debug, Clone, Copy)] | ||
| struct GenmcScalar { | ||
| value: u64, | ||
| is_init: bool, | ||
| } |
There was a problem hiding this comment.
We have this type with the is_init flag since CXX doesn't support sending Option (or std::optional) across the language boundary. GenMC only supports up to 64 bit memory accesses, therefore the u64. Lastly, we don't support sending pointers to GenMC in this PR, so no field for provenance information (this also needs some design work on the GenMC side first).
src/concurrency/thread.rs
Outdated
| // FIXME(genmc): properly handle sleep in GenMC mode. | ||
| SchedulingAction::Sleep(duration) => { | ||
| this.machine.monotonic_clock.sleep(duration); | ||
| } |
There was a problem hiding this comment.
Probably not a problem for this PR, but we need to figure out how to handle sleep (just ignoring sleep might work).
Co-authored-by: Ralf Jung <[email protected]>
…checks, remove unused stderr file.
rustbot
added
S-waiting-on-review
|
@RalfJung what should I do about this warning, should I rebase & force push to remove the line in the message? Does it matter since we squash the commits in the end anyway? I thought I could mark the PR as not being a draft anymore, but maybe I should keep it as draft until we are ready to squash. |
|
Yeah, we'll squash this away.
Once you think it is in a state that it can land (except for squashing), you can remove the draft status. |
rustbot
added
S-waiting-on-author
| // This function is called to get the initial value of globals. | ||
| // Ideally, the function signature (on the GenMC side) would be changed to return an | ||
| // `std::optional<SVal>`, since the given `AAccess` may not point to a valid and initialized | ||
| // allocation. |
There was a problem hiding this comment.
As before, please add a sentence like "This dummy value can never be observed by the program because ...".
| * Automatically calls `inc_pos` and `dec_pos` where needed for the given thread. | ||
| */ | ||
| template <EventLabel::EventLabelKind k, typename... Ts> | ||
| auto handle_load_reset_if_none(ThreadId tid, Ts&&... params) -> HandleResult<SVal> { |
There was a problem hiding this comment.
This is only used once, is it really worth a function?
At the very least, please make it private to EventHandling.cpp; seems odd to have this in the "interface" file.
There was a problem hiding this comment.
It will be used 4 times in the final code, 3 times in EventHandling.cpp once in Mutex.cpp (for mutex interception code, not yet in this PR).
Also, it needs to be part of the class, since it accesses private member functions incPos, decPos and GenMCDriver::handleLoad.
There was a problem hiding this comment.
Argh, annoying C++ visibility rules...
I feel like I'll have a hard time finding anything in these C++ files, it's quite unclear what goes in which header vs which cpp file, and there's not the usual 1:1 relationship of headers and cpp files. But at this point it's not worth moving everything around, maybe I'll do that once we landed all your things.
This PR is the MVP for Miri-GenMC, which adds enough functionality to be able to check some simple programs.
A lot of functionality is missing and will be added in future PRs (e.g., atomic read-modify-write/compare_exchange/fences,
Mutexsupport, support for mixed atomic and non-atomic memory accesses to the same location, etc.)(The commit history shows some of the features that were removed for this PR.)
The current branch uses a fork of GenMC, since are some changes there that must be upstreamed there first. This PR should not be merged until this is finished.