Miri-GenMC API refactor by michaliskok · Pull Request #4959 · rust-lang/miri

michaliskok · 2026-04-13T20:45:15Z

Another follow up on #4949 making the following changes:

Replaces bool with per-operation status enums in CXX types
Renames *Ext factory namespaces to Make* and drops from_ prefix in CXX
Uses std::visit with overloaded{} for HandleResult dispatch in MiriGenmcShim
Adds GenmcHandleResult<T> to collapse 3-field status checks in Miri
Flattens genmc-sys/cpp/src/ folder
Renames MiriGenmcShim to MiriGenMCInterface

These map to the respective commits.

I'm not sure how this looks to you. I'm happy to split to smaller PRs or revise as you see fit.

Each result type in the Miri-GenMC interface previously used at least `invalid: bool` (other results used more bools, e.g., `MutexLockResult`) as ad-hoc discriminants alongside payload fields. This made valid field combinations implicit and documented only in comments. This commit replace these bools with typed status enums: - `OperationStatus { Invalid, Error, Ok }`: shared by `LoadResult`, `StoreResult`, `NonAtomicResult`, `ReadModifyWriteResult`. - `CasStatus { Invalid, Error, Failed, Succeeded }`: used only by CASes, which have two success modes. - `MutexLockStatus { Invalid, Error, Reset, Acquired, NotAcquired }`: used by mutex lock operations, which have three success modes. Non-atomic loads and stores now use a dedicated `NonAtomicResult` type instead of sharing `LoadResult`/`StoreResult`, as they have no payload on success. Atomic loads always produce a value when `Ok`, so a `NoValue` variant is no longer necessary. Callers in `mod.rs` and `shims.rs` are updated to exhaustive `match` blocks, which also makes the mutex-lock and unlock handlers no longer ignore `invalid=true`.

Until now, we were using `*Ext` names in the Miri-GenMC interface to create result types, such as `LoadResultExt::from_value()`, `StoreResultExt::ok(...)`, etc. These were unconventional: `Ext` suggests an "extension", while the `from_` prefix is redundant given the namespace name. This commit replaces `Ext` with `Make<T>::<variant>()`, which reads more like a constructor (e.g., `MakeLoadResult::value(v)`, `MakeStoreResult::ok(b)`, etc.). The function names are shortened accordingly (e.g., `from_value` -> `value`). `GenmcScalarExt` is kept as-is since it is not a factory.

Until now, the Miri-GenMC interface used ad-hoc get_if/holds_alternative chains to return results to Miri. This commit replaces this mechanism with std::visit, which provides compile-time exhaustiveness checking for all dispatch sites and makes each case explicit with a dedicated lambda. For two-call functions such as CASes and locks, the first call keeps the get_if chain to extract the intermediate SVal, while the final dispatch uses std::visit.

For operations that use OperationStatus (atomic/non-atomic loads and stores, RMW), callers previously had to match on result.status, then separately access the payload fields, plus carry a required wildcard arm because CXX enums are non-exhaustive. This commit adds GenmcHandleResult<T> { Invalid, Error(String), Ok(T) } to genmc-sys and into_genmc_result() conversion methods on {Load,Store,NonAtomic}Result. Each method bakes in payload extraction, so callers get a clean match with no wildcard arm and no manual .as_ref().unwrap() on the error string. CompareExchangeResult and MutexLockResult have their own status enums with multiple distinct success modes; their call sites remain unchanged.

No point in having `genmc-sys/cpp/src/MiriInterface` just for two files. This commit moves all cpp files under `genmc-sys/cpp/src/`.

"Shim" has a specific meaning in Miri: https://github.com/rust-lang/miri/tree/master/src/shims

RalfJung · 2026-04-13T20:51:29Z

Renames MiriGenmcShim to MiriGenMCInterface

The usual naming convention in Rust is CamelCase, including for acronyms, entirely disregarding the usual capitalization of the component words. That's why it's Arc, not ARC or ARc, and IoSliceMut, not IOSliceMut. So it should be MiriGenmcInterface.

RalfJung

Thanks! Some nice refactors. :)
@rustbot author

Comments for the commit messages:

This made valid field combinations implicit and documented only in
comments.

FWIW they are still only documented in comments, right?

Ext suggests an "extension"

Yeah, that's exactly what it is -- it's kind of like an extension trait in Rust.
But the new names are also fine 🤷 .

provides compile-time exhaustiveness checking

There seems to always be an UNREACHABLE fallback. So is this really compile-time exhaustiveness checking? Looks more like runtime exhaustiveness checking.

genmc/build,cpp: Flatten genmc-sys/cpp/src/ folder

This commit also seems to do some of the renaming of MiriGenmcShim already...

View changes since this review

RalfJung · 2026-04-14T06:03:17Z

genmc-sys/src/lib.rs

        blocked_execs: u64,
    }

+    #[derive(Debug, Clone, Copy)]


The usual style is to put attributes after the doc comment, so please move them down.

This applies consistently everywhere; I won't add comments for every instance of this.

RalfJung · 2026-04-14T06:03:54Z

genmc-sys/src/lib.rs


+    #[derive(Debug, Clone, Copy)]
+    /// Status tag shared by operations with a single success mode
+    /// (atomic loads/stores, non-atomic loads/stores, and FAIs.


Missing closing parenthesis before the ).

(And GH doesn't allow suggestions when one does per-commit review...)

RalfJung · 2026-04-14T06:05:01Z

genmc-sys/src/lib.rs

+    #[derive(Debug, Clone, Copy)]
+    /// Status tag shared by operations with a single success mode
+    /// (atomic loads/stores, non-atomic loads/stores, and FAIs.
+    /// For operations with multiple success modes, see [`CasStatus`] and [`MutexLockStatus`].


Hm, is that really worth a separate enum? Wouldn't it be more uniform to always use this enum and treat the success mode as "payload"?

RalfJung · 2026-04-14T06:06:01Z

genmc-sys/src/lib.rs

+
    #[must_use]
    #[derive(Debug)]
+    /// Result from an atomic load. When `status == Ok`, `read_value` is valid.


The 2nd sentence is redundant with the per-field comments.

RalfJung · 2026-04-14T06:06:41Z

genmc-sys/src/lib.rs

+    #[derive(Debug)]
+    /// Result from a non-atomic load or store. GenMC uses these only for data-race detection;
+    /// no value is communicated back to Miri. When `status == Ok` there is no payload.
+    struct NonAtomicResult {


Please don't put this in between LoadResult and StoreResult. Those two should be next to each other.

RalfJung · 2026-04-14T06:22:27Z

genmc-sys/src/lib.rs

+/// [`MutexLockResult`]) the status enums carry sufficient information and should be
+/// matched directly.
+#[must_use]
+pub enum GenmcHandleResult<T> {


"handle" sounds like a verb here. Maybe call this just GenmcResult?

RalfJung · 2026-04-14T06:22:40Z

genmc-sys/src/lib.rs

+/// The payload type `T` is operation-specific:
+/// - [`LoadResult`]:           `T = GenmcScalar`                      (the value read)
+/// - [`NonAtomicResult`]:      `T = ()`                               (no payload)
+/// - [`StoreResult`]:          `T = bool`                             (is the write co-max)
+/// - [`ReadModifyWriteResult`]:`T = (GenmcScalar, GenmcScalar, bool)` (old, new, is_co_max)


No need to give an exhaustive list.

RalfJung · 2026-04-14T06:24:23Z

genmc-sys/src/lib.rs

+}
+
+impl ReadModifyWriteResult {
+    pub fn into_genmc_result(self) -> GenmcHandleResult<(GenmcScalar, GenmcScalar, bool)> {


I'm not a fan of how this conversion into a tuple loses the field names that distinguish old and new value. So I don't think for RMWs this is a win in its current form.

RalfJung · 2026-04-14T06:26:39Z

src/concurrency/genmc/mod.rs

+            status => unreachable!("unexpected OperationStatus: {status:?}"),
        }
        // Miri will always write non-atomic stores to memory. Make sure GenMC agrees with that.
        assert!(store_result.is_coherence_order_maximal_write);


Doesn't this fail to compile now since that field does not exist on NonAtomicStore?

RalfJung · 2026-04-14T06:29:30Z

src/concurrency/genmc/mod.rs

 pub struct GenmcCtx {
    /// Handle to the GenMC model checker.
-    handle: RefCell<UniquePtr<MiriGenmcShim>>,
+    handle: RefCell<UniquePtr<MiriGenMCInterface>>,


Is handle truly the best name for this?
Would it make sense to just call this genmc?

rustbot · 2026-04-14T06:30:30Z

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

michaliskok added 3 commits April 13, 2026 22:28

rustbot added the S-waiting-on-author Status: Waiting for the PR author to address review comments label Apr 13, 2026

rustbot assigned RalfJung Apr 13, 2026

michaliskok marked this pull request as ready for review April 13, 2026 20:45

rustbot added S-waiting-on-review Status: Waiting for a review to complete and removed S-waiting-on-author Status: Waiting for the PR author to address review comments labels Apr 13, 2026

michaliskok added 3 commits April 13, 2026 22:46

genmc/build,cpp: Flatten genmc-sys/cpp/src/ folder

b4d11e3

No point in having `genmc-sys/cpp/src/MiriInterface` just for two files. This commit moves all cpp files under `genmc-sys/cpp/src/`.

genmc: Rename MiriGenmcShim to MiriGenMCInterface

5f76116

"Shim" has a specific meaning in Miri: https://github.com/rust-lang/miri/tree/master/src/shims

michaliskok force-pushed the genmc-miri-api-refactor branch from fd40ccd to 5f76116 Compare April 13, 2026 20:46

RalfJung reviewed Apr 14, 2026

View reviewed changes

rustbot added S-waiting-on-author Status: Waiting for the PR author to address review comments and removed S-waiting-on-review Status: Waiting for a review to complete labels Apr 14, 2026

Conversation

michaliskok commented Apr 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

RalfJung commented Apr 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

RalfJung left a comment • edited by rustbot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

rustbot commented Apr 14, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

michaliskok commented Apr 13, 2026 •

edited

Loading

RalfJung commented Apr 13, 2026 •

edited

Loading

RalfJung left a comment •

edited by rustbot

Loading