Add more features for GenMC mode (RMW, fences, new printing options) #4566

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Merged

RalfJung merged 2 commits into rust-lang:master from Patrick-6:miri-genmc-rmw

Sep 8, 2025

Contributor

Patrick-6 commented Sep 4, 2025 •

edited

Loading

This PR is a followup to #4506

New features for GenMC mode include:

Support for read-modify-write operations (no compare-exchange yet).
Support for fences.
New option to print GenMC output message on errors.
New option to print GenMC execution graphs after every execution.
New option to set memory model to "Sequential Consistency" (SC).
~~Throw an error when attempting to use a futex, since they are unsupported.~~
Throw an error on acquire_clock and release_clock in GenMC mode.

There is also some cleanup for changes from the last PR, including the switch to std::process::abort in tests.

rustbot added the S-waiting-on-author label

Patrick-6 commented

View reviewed changes

genmc-sys/cpp/src/MiriInterface/EventHandling.cpp Outdated Show resolved Hide resolved

src/concurrency/genmc/helper.rs Outdated Show resolved Hide resolved

src/concurrency/genmc/mod.rs Show resolved Hide resolved

src/concurrency/genmc/mod.rs Outdated Show resolved Hide resolved

src/concurrency/genmc/mod.rs Outdated Show resolved Hide resolved

src/concurrency/genmc/mod.rs Outdated Show resolved Hide resolved

tests/genmc/fail/loom/buggy_inc.rs Show resolved Hide resolved

tests/genmc/pass/atomics/rmw_edge_cases.rs Outdated Show resolved Hide resolved

tests/utils/genmc.rs Outdated Show resolved Hide resolved

Contributor Author

Patrick-6 commented Sep 4, 2025

Next part of merging GenMC mode, but a bit less code this time ^^

rustbot assigned RalfJung

RalfJung reviewed

View reviewed changes

src/concurrency/genmc/mod.rs Outdated Show resolved Hide resolved

RalfJung reviewed

View reviewed changes

src/concurrency/genmc/mod.rs Outdated Show resolved Hide resolved

RalfJung reviewed

View reviewed changes

Member

RalfJung left a comment •

edited by rustbot

Loading

First round of feedback

View changes since this review

genmc-sys/cpp/src/MiriInterface/EventHandling.cpp Show resolved Hide resolved

genmc-sys/src/lib.rs Show resolved Hide resolved

genmc-sys/src/lib.rs Show resolved Hide resolved

src/concurrency/genmc/helper.rs Outdated Show resolved Hide resolved

src/concurrency/genmc/helper.rs Outdated Show resolved Hide resolved

genmc-sys/cpp/src/MiriInterface/EventHandling.cpp Show resolved Hide resolved

src/concurrency/genmc/run.rs Outdated Show resolved Hide resolved

src/concurrency/sync.rs Outdated Show resolved Hide resolved

tests/genmc/fail/loom/buggy_inc.rs Outdated Show resolved Hide resolved

tests/genmc/fail/loom/buggy_inc.rs Show resolved Hide resolved

RalfJung reviewed

View reviewed changes

Member

RalfJung left a comment •

edited by rustbot

Loading

And now I also went over the tests

View changes since this review

tests/utils/genmc.rs Outdated Show resolved Hide resolved

tests/utils/genmc.rs Outdated Show resolved Hide resolved

tests/genmc/pass/atomics/rmw_simple.rs Outdated Show resolved Hide resolved

tests/genmc/pass/atomics/rmw_simple.rs Outdated Show resolved Hide resolved

tests/genmc/pass/litmus/IRIWish.rs Show resolved Hide resolved

This comment has been minimized.

Sign in to view

RalfJung reviewed

View reviewed changes

genmc-sys/src/lib.rs Outdated Show resolved Hide resolved

RalfJung reviewed

View reviewed changes

src/concurrency/genmc/mod.rs Outdated Show resolved Hide resolved

RalfJung reviewed

View reviewed changes

genmc-sys/src/lib.rs Outdated Show resolved Hide resolved

RalfJung reviewed

View reviewed changes

genmc-sys/cpp/src/MiriInterface/EventHandling.cpp Show resolved Hide resolved

RalfJung reviewed

View reviewed changes

genmc-sys/src/lib.rs Show resolved Hide resolved

RalfJung reviewed

View reviewed changes

genmc-sys/src/lib.rs Outdated Show resolved Hide resolved

Patrick-6 force-pushed the miri-genmc-rmw branch from 8c8a1d6 to 425f2af Compare

September 5, 2025 15:08

RalfJung reviewed

View reviewed changes

genmc-sys/build.rs Outdated Show resolved Hide resolved

RalfJung reviewed

View reviewed changes

genmc-sys/src/lib.rs Show resolved Hide resolved

RalfJung reviewed

View reviewed changes

tests/genmc/pass/litmus/Z6_U.weak.stderr Outdated Show resolved Hide resolved

RalfJung reviewed

View reviewed changes

tests/genmc/pass/litmus/Z6_U.rs Outdated Show resolved Hide resolved

RalfJung reviewed

View reviewed changes

src/concurrency/genmc/config.rs Outdated Show resolved Hide resolved

Patrick-6 marked this pull request as ready for review

September 7, 2025 10:35

rustbot added S-waiting-on-review and removed S-waiting-on-author labels

RalfJung reviewed

View reviewed changes

src/concurrency/data_race.rs Outdated Show resolved Hide resolved

src/concurrency/data_race.rs Outdated Show resolved Hide resolved

src/concurrency/data_race.rs Outdated Show resolved Hide resolved

tests/genmc/pass/atomics/rmw_ops.rs Outdated Show resolved Hide resolved

Member

RalfJung commented Sep 7, 2025

LGTM, please squash. :)
@rustbot author

rustbot removed the S-waiting-on-review label

Collaborator

rustbot commented Sep 7, 2025

Reminder, once the PR becomes ready for a review, use @rustbot ready.

rustbot added the S-waiting-on-author label


          Implement more features for GenMC mode

aceac27

- Support for atomic fences.
- Support for atomic read-modify-write (RMW).
- Add tests using RMW and fences.
- Add options:
  - to disable weak memory effects in GenMC mode.
  - to print GenMC execution graphs.
  - to print GenMC output message.
- Fix GenMC full rebuild issue and run configure step when commit changes.
- Do cleanup.

Co-authored-by: Ralf Jung <[email protected]>

Patrick-6 force-pushed the miri-genmc-rmw branch from 44ce1ee to aceac27 Compare

September 7, 2025 21:55

Contributor Author

Patrick-6 commented Sep 7, 2025

rustbot added S-waiting-on-review and removed S-waiting-on-author labels


          print proper error when using unsupported synchronization primitive w…

63b4257

…ith GenMC

RalfJung enabled auto-merge

September 8, 2025 05:56

Member

RalfJung commented Sep 8, 2025

Thanks! I have added a patch for the release/acquire clock error messages.

RalfJung added this pull request to the merge queue

Merged via the queue into rust-lang:master with commit 0d56e22

15 checks passed

rustbot removed the S-waiting-on-review label

Patrick-6 mentioned this pull request

Add compare_exchange support for GenMC mode #4578

Merged

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet