From c1be740564dd4a3aaafca93539ca428223226278 Mon Sep 17 00:00:00 2001
From: Patrick-6 <pamu99@gmx.ch>
Date: Mon, 14 Apr 2025 08:53:50 +0200
Subject: Implement basic support for running Miri with GenMC. - Implement
 memory allocation compatible with GenMC.   - Extract address generator struct
 from Miri's allocator. - Support thread creation and joining. - Support
 atomic load and store. - Support scheduling through GenMC. - Add tests for
 GenMC mode. - Add clang-format file for C++ code in Miri. - Update genmc-sys
 crate license to MIT/Apache to match GenMC dependency. - Add documentation
 for GenMC mode.

Note: this commit depends on changes to GenMC not yet upstreamed to its official repository.

Co-authored-by: Ralf Jung <post@ralfj.de>
---
 .../miri/genmc-sys/cpp/include/MiriInterface.hpp   | 274 +++++++++++++++++++++
 .../miri/genmc-sys/cpp/include/ResultHandling.hpp  |  21 ++
 2 files changed, 295 insertions(+)
 create mode 100644 src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp
 create mode 100644 src/tools/miri/genmc-sys/cpp/include/ResultHandling.hpp

(limited to 'src/tools/miri/genmc-sys/cpp/include')

diff --git a/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp b/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp
new file mode 100644
index 00000000000..4484f0b73ca
--- /dev/null
+++ b/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp
@@ -0,0 +1,274 @@
+#ifndef GENMC_MIRI_INTERFACE_HPP
+#define GENMC_MIRI_INTERFACE_HPP
+
+// CXX.rs generated headers:
+#include "rust/cxx.h"
+
+// GenMC generated headers:
+#include "config.h"
+
+// Miri `genmc-sys/src_cpp` headers:
+#include "ResultHandling.hpp"
+
+// GenMC headers:
+#include "ExecutionGraph/EventLabel.hpp"
+#include "Static/ModuleID.hpp"
+#include "Support/MemOrdering.hpp"
+#include "Support/RMWOps.hpp"
+#include "Verification/Config.hpp"
+#include "Verification/GenMCDriver.hpp"
+
+// C++ headers:
+#include <cstdint>
+#include <format>
+#include <iomanip>
+#include <memory>
+
+/**** Types available to both Rust and C++ ****/
+
+struct GenmcParams;
+enum class LogLevel : std::uint8_t;
+
+struct GenmcScalar;
+struct SchedulingResult;
+struct LoadResult;
+struct StoreResult;
+
+// GenMC uses `int` for its thread IDs.
+using ThreadId = int;
+
+/// Set the log level for GenMC.
+///
+/// # Safety
+///
+/// This function is not thread safe, since it writes to the global, mutable, non-atomic `logLevel`
+/// variable. Any GenMC function may read from `logLevel` unsynchronized.
+/// The safest way to use this function is to set the log level exactly once before first calling
+/// `create_handle`.
+/// Never calling this function is safe, GenMC will fall back to its default log level.
+/* unsafe */ void set_log_level_raw(LogLevel log_level);
+
+struct MiriGenmcShim : private GenMCDriver {
+
+  public:
+    MiriGenmcShim(std::shared_ptr<const Config> conf, Mode mode /* = VerificationMode{} */)
+        : GenMCDriver(std::move(conf), nullptr, mode) {}
+
+    /// Create a new `MiriGenmcShim`, which wraps a `GenMCDriver`.
+    ///
+    /// # Safety
+    ///
+    /// This function is marked as unsafe since the `logLevel` global variable is non-atomic.
+    /// This function should not be called in an unsynchronized way with `set_log_level_raw`,
+    /// since this function and any methods on the returned `MiriGenmcShim` may read the
+    /// `logLevel`, causing a data race. The safest way to use these functions is to call
+    /// `set_log_level_raw` once, and only then start creating handles. There should not be any
+    /// other (safe) way to create a `MiriGenmcShim`.
+    /* unsafe */ static auto create_handle(const GenmcParams& params)
+        -> std::unique_ptr<MiriGenmcShim>;
+
+    virtual ~MiriGenmcShim() {}
+
+    /**** Execution start/end handling ****/
+
+    // This function must be called at the start of any execution, before any events are
+    // reported to GenMC.
+    void handle_execution_start();
+    // This function must be called at the end of any execution, even if an error was found
+    // during the execution.
+    // Returns `null`, or a string containing an error message if an error occured.
+    std::unique_ptr<std::string> handle_execution_end();
+
+    /***** Functions for handling events encountered during program execution. *****/
+
+    /**** Memory access handling ****/
+
+    [[nodiscard]] LoadResult handle_load(
+        ThreadId thread_id,
+        uint64_t address,
+        uint64_t size,
+        MemOrdering ord,
+        GenmcScalar old_val
+    );
+    [[nodiscard]] StoreResult handle_store(
+        ThreadId thread_id,
+        uint64_t address,
+        uint64_t size,
+        GenmcScalar value,
+        GenmcScalar old_val,
+        MemOrdering ord
+    );
+
+    /**** Memory (de)allocation ****/
+    auto handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment) -> uint64_t;
+    void handle_free(ThreadId thread_id, uint64_t address);
+
+    /**** Thread management ****/
+    void handle_thread_create(ThreadId thread_id, ThreadId parent_id);
+    void handle_thread_join(ThreadId thread_id, ThreadId child_id);
+    void handle_thread_finish(ThreadId thread_id, uint64_t ret_val);
+    void handle_thread_kill(ThreadId thread_id);
+
+    /***** Exploration related functionality *****/
+
+    /** Ask the GenMC scheduler for a new thread to schedule and return whether the execution is
+     * finished, blocked, or can continue.
+     * Updates the next instruction kind for the given thread id. */
+    auto schedule_next(const int curr_thread_id, const ActionKind curr_thread_next_instr_kind)
+        -> SchedulingResult;
+
+    /**
+     * Check whether there are more executions to explore.
+     * If there are more executions, this method prepares for the next execution and returns
+     * `true`. Returns true if there are no more executions to explore. */
+    auto is_exploration_done() -> bool {
+        return GenMCDriver::done();
+    }
+
+    /**** Result querying functionality. ****/
+
+    // NOTE: We don't want to share the `VerificationResult` type with the Rust side, since it
+    // is very large, uses features that CXX.rs doesn't support and may change as GenMC changes.
+    // Instead, we only use the result on the C++ side, and only expose these getter function to
+    // the Rust side.
+
+    // Note that CXX.rs doesn't support returning a C++ string to Rust by value,
+    // it must be behind an indirection like a `unique_ptr` (tested with CXX 1.0.170).
+
+    /// Get the number of blocked executions encountered by GenMC (cast into a fixed with
+    /// integer)
+    auto get_blocked_execution_count() const -> uint64_t {
+        return static_cast<uint64_t>(getResult().exploredBlocked);
+    }
+
+    /// Get the number of executions explored by GenMC (cast into a fixed with integer)
+    auto get_explored_execution_count() const -> uint64_t {
+        return static_cast<uint64_t>(getResult().explored);
+    }
+
+    /// Get all messages that GenMC produced (errors, warnings), combined into one string.
+    auto get_result_message() const -> std::unique_ptr<std::string> {
+        return std::make_unique<std::string>(getResult().message);
+    }
+
+    /// If an error occurred, return a string describing the error, otherwise, return `nullptr`.
+    auto get_error_string() const -> std::unique_ptr<std::string> {
+        const auto& result = GenMCDriver::getResult();
+        if (result.status.has_value())
+            return format_error(result.status.value());
+        return nullptr;
+    }
+
+  private:
+    /** Increment the event index in the given thread by 1 and return the new event. */
+    [[nodiscard]] inline auto inc_pos(ThreadId tid) -> Event {
+        ERROR_ON(tid >= threads_action_.size(), "ThreadId out of bounds");
+        return ++threads_action_[tid].event;
+    }
+    /** Decrement the event index in the given thread by 1 and return the new event. */
+    inline auto dec_pos(ThreadId tid) -> Event {
+        ERROR_ON(tid >= threads_action_.size(), "ThreadId out of bounds");
+        return --threads_action_[tid].event;
+    }
+
+    /**
+     * Helper function for loads that need to reset the event counter when no value is returned.
+     * Same syntax as `GenMCDriver::handleLoad`, but this takes a thread id instead of an Event.
+     * 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> {
+        const auto pos = inc_pos(tid);
+        const auto ret = GenMCDriver::handleLoad<k>(pos, std::forward<Ts>(params)...);
+        // If we didn't get a value, we have to reset the index of the current thread.
+        if (!std::holds_alternative<SVal>(ret)) {
+            dec_pos(tid);
+        }
+        return ret;
+    }
+
+    /**
+     * GenMC uses the term `Action` to refer to a struct of:
+     * - `ActionKind`, storing whether the next instruction in a thread may be a load
+     * - `Event`, storing the most recent event index added for a thread
+     *
+     * Here we store the "action" for each thread. In particular we use this to assign event
+     * indices, since GenMC expects us to do that.
+     */
+    std::vector<Action> threads_action_;
+};
+
+/// Get the bit mask that GenMC expects for global memory allocations.
+/// FIXME(genmc): currently we use `get_global_alloc_static_mask()` to ensure the
+/// `SAddr::staticMask` constant is consistent between Miri and GenMC, but if
+/// https://github.com/dtolnay/cxx/issues/1051 is fixed we could share the constant
+///   directly.
+constexpr auto get_global_alloc_static_mask() -> uint64_t {
+    return SAddr::staticMask;
+}
+
+// CXX.rs generated headers:
+// NOTE: this must be included *after* `MiriGenmcShim` and all the other types we use are defined,
+// otherwise there will be compilation errors due to missing definitions.
+#include "genmc-sys/src/lib.rs.h"
+
+/**** Result handling ****/
+// NOTE: these must come after the cxx_bridge generated code, since that contains the actual
+// definitions of these types.
+
+namespace GenmcScalarExt {
+inline GenmcScalar uninit() {
+    return GenmcScalar {
+        /* value: */ 0,
+        /* is_init: */ false,
+    };
+}
+
+inline GenmcScalar from_sval(SVal sval) {
+    return GenmcScalar {
+        /* value: */ sval.get(),
+        /* is_init: */ true,
+    };
+}
+
+inline SVal to_sval(GenmcScalar scalar) {
+    ERROR_ON(!scalar.is_init, "Cannot convert an uninitialized `GenmcScalar` into an `SVal`\n");
+    return SVal(scalar.value);
+}
+} // namespace GenmcScalarExt
+
+namespace LoadResultExt {
+inline LoadResult no_value() {
+    return LoadResult {
+        /* error: */ std::unique_ptr<std::string>(nullptr),
+        /* has_value: */ false,
+        /* read_value: */ GenmcScalarExt::uninit(),
+    };
+}
+
+inline LoadResult from_value(SVal read_value) {
+    return LoadResult { /* error: */ std::unique_ptr<std::string>(nullptr),
+                        /* has_value: */ true,
+                        /* read_value: */ GenmcScalarExt::from_sval(read_value) };
+}
+
+inline LoadResult from_error(std::unique_ptr<std::string> error) {
+    return LoadResult { /* error: */ std::move(error),
+                        /* has_value: */ false,
+                        /* read_value: */ GenmcScalarExt::uninit() };
+}
+} // namespace LoadResultExt
+
+namespace StoreResultExt {
+inline StoreResult ok(bool is_coherence_order_maximal_write) {
+    return StoreResult { /* error: */ std::unique_ptr<std::string>(nullptr),
+                         is_coherence_order_maximal_write };
+}
+
+inline StoreResult from_error(std::unique_ptr<std::string> error) {
+    return StoreResult { /* error: */ std::move(error),
+                         /* is_coherence_order_maximal_write: */ false };
+}
+} // namespace StoreResultExt
+
+#endif /* GENMC_MIRI_INTERFACE_HPP */
diff --git a/src/tools/miri/genmc-sys/cpp/include/ResultHandling.hpp b/src/tools/miri/genmc-sys/cpp/include/ResultHandling.hpp
new file mode 100644
index 00000000000..189f32e6f51
--- /dev/null
+++ b/src/tools/miri/genmc-sys/cpp/include/ResultHandling.hpp
@@ -0,0 +1,21 @@
+#ifndef GENMC_RESULT_HANDLING_HPP
+#define GENMC_RESULT_HANDLING_HPP
+
+// CXX.rs generated headers:
+#include "rust/cxx.h"
+
+// GenMC headers:
+#include "Verification/VerificationError.hpp"
+
+#include <string>
+
+/** Information about an error, formatted as a string to avoid having to share an error enum and
+ * printing functionality with the Rust side. */
+static auto format_error(VerificationError err) -> std::unique_ptr<std::string> {
+    auto buf = std::string();
+    auto s = llvm::raw_string_ostream(buf);
+    s << err;
+    return std::make_unique<std::string>(s.str());
+}
+
+#endif /* GENMC_RESULT_HANDLING_HPP */
-- 
cgit 1.4.1-3-g733a5


From 61af5da8dfc9f5fd6e2d36f8316f7bf5884f5388 Mon Sep 17 00:00:00 2001
From: Patrick-6 <pamu99@gmx.ch>
Date: Fri, 14 Mar 2025 09:58:46 +0100
Subject: Implement more features for GenMC mode - 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 <post@ralfj.de>
---
 src/tools/miri/doc/genmc.md                        |   7 +-
 src/tools/miri/genmc-sys/build.rs                  |  37 ++--
 .../miri/genmc-sys/cpp/include/MiriInterface.hpp   |  29 ++++
 .../cpp/src/MiriInterface/EventHandling.cpp        |  66 +++++++
 .../miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp |  13 +-
 src/tools/miri/genmc-sys/src/lib.rs                |  77 ++++++++-
 src/tools/miri/src/bin/miri.rs                     |  23 +--
 src/tools/miri/src/concurrency/data_race.rs        |  12 +-
 src/tools/miri/src/concurrency/genmc/config.rs     |  60 ++++++-
 src/tools/miri/src/concurrency/genmc/dummy.rs      |   8 +-
 src/tools/miri/src/concurrency/genmc/helper.rs     |  54 +++++-
 src/tools/miri/src/concurrency/genmc/mod.rs        | 191 +++++++++++++--------
 src/tools/miri/src/concurrency/genmc/run.rs        |  13 +-
 src/tools/miri/tests/genmc/fail/loom/buggy_inc.rs  |  66 +++++++
 .../miri/tests/genmc/fail/loom/buggy_inc.stderr    |  13 ++
 .../genmc/fail/simple/2w2w_weak.relaxed4.stderr    |   8 +-
 .../genmc/fail/simple/2w2w_weak.release4.stderr    |   8 +-
 .../miri/tests/genmc/fail/simple/2w2w_weak.rs      |   7 +-
 .../genmc/fail/simple/2w2w_weak.sc3_rel1.stderr    |   8 +-
 src/tools/miri/tests/genmc/pass/atomics/rmw_ops.rs |  91 ++++++++++
 .../miri/tests/genmc/pass/atomics/rmw_ops.stderr   |   2 +
 .../miri/tests/genmc/pass/litmus/2w2w_2sc_scf.rs   |  33 ++++
 .../tests/genmc/pass/litmus/2w2w_2sc_scf.stderr    |   2 +
 .../miri/tests/genmc/pass/litmus/2w2w_4rel.rs      |   4 +
 .../tests/genmc/pass/litmus/2w2w_4rel.sc.stderr    |   2 +
 .../miri/tests/genmc/pass/litmus/2w2w_4rel.stderr  |   2 -
 .../tests/genmc/pass/litmus/2w2w_4rel.weak.stderr  |   2 +
 .../miri/tests/genmc/pass/litmus/IRIW-acq-sc.rs    |   2 +-
 src/tools/miri/tests/genmc/pass/litmus/IRIWish.rs  |  66 +++++++
 .../miri/tests/genmc/pass/litmus/IRIWish.stderr    |  30 ++++
 .../miri/tests/genmc/pass/litmus/LB_incMPs.rs      |  41 +++++
 .../miri/tests/genmc/pass/litmus/LB_incMPs.stderr  |   2 +
 .../miri/tests/genmc/pass/litmus/MPU_rels_acq.rs   |  42 +++++
 .../tests/genmc/pass/litmus/MPU_rels_acq.stderr    |   2 +
 .../miri/tests/genmc/pass/litmus/MP_incMPs.rs      |  36 ++++
 .../miri/tests/genmc/pass/litmus/MP_incMPs.stderr  |   2 +
 .../miri/tests/genmc/pass/litmus/MP_rels_acqf.rs   |  40 +++++
 .../tests/genmc/pass/litmus/MP_rels_acqf.stderr    |   2 +
 .../miri/tests/genmc/pass/litmus/SB_2sc_scf.rs     |  32 ++++
 .../miri/tests/genmc/pass/litmus/SB_2sc_scf.stderr |   2 +
 src/tools/miri/tests/genmc/pass/litmus/Z6_U.rs     |  65 +++++++
 .../miri/tests/genmc/pass/litmus/Z6_U.sc.stderr    |  20 +++
 .../miri/tests/genmc/pass/litmus/Z6_U.weak.stderr  |  24 +++
 src/tools/miri/tests/genmc/pass/litmus/Z6_acq.rs   |  38 ++++
 .../miri/tests/genmc/pass/litmus/Z6_acq.stderr     |   2 +
 src/tools/miri/tests/genmc/pass/litmus/atomicpo.rs |  32 ++++
 .../miri/tests/genmc/pass/litmus/atomicpo.stderr   |   2 +
 .../miri/tests/genmc/pass/litmus/cumul-release.rs  |  58 +++++++
 .../tests/genmc/pass/litmus/cumul-release.stderr   |   2 +
 .../miri/tests/genmc/pass/litmus/fr_w_w_w_reads.rs |   1 -
 src/tools/miri/tests/genmc/pass/litmus/inc2w.rs    |  45 +++++
 .../miri/tests/genmc/pass/litmus/inc2w.stderr      |   2 +
 .../tests/genmc/pass/litmus/inc_inc_RR_W_RR.rs     |  63 +++++++
 .../tests/genmc/pass/litmus/inc_inc_RR_W_RR.stderr |   2 +
 src/tools/miri/tests/genmc/pass/litmus/riwi.rs     |  31 ++++
 src/tools/miri/tests/genmc/pass/litmus/riwi.stderr |   2 +
 .../miri/tests/genmc/pass/litmus/viktor-relseq.rs  |  36 ++++
 .../tests/genmc/pass/litmus/viktor-relseq.stderr   |   2 +
 src/tools/miri/tests/utils/genmc.rs                |   7 +
 59 files changed, 1433 insertions(+), 138 deletions(-)
 create mode 100644 src/tools/miri/tests/genmc/fail/loom/buggy_inc.rs
 create mode 100644 src/tools/miri/tests/genmc/fail/loom/buggy_inc.stderr
 create mode 100644 src/tools/miri/tests/genmc/pass/atomics/rmw_ops.rs
 create mode 100644 src/tools/miri/tests/genmc/pass/atomics/rmw_ops.stderr
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/2w2w_2sc_scf.rs
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/2w2w_2sc_scf.stderr
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.sc.stderr
 delete mode 100644 src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.stderr
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.weak.stderr
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/IRIWish.rs
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/IRIWish.stderr
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/LB_incMPs.rs
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/LB_incMPs.stderr
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/MPU_rels_acq.rs
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/MPU_rels_acq.stderr
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/MP_incMPs.rs
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/MP_incMPs.stderr
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/MP_rels_acqf.rs
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/MP_rels_acqf.stderr
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/SB_2sc_scf.rs
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/SB_2sc_scf.stderr
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/Z6_U.rs
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/Z6_U.sc.stderr
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/Z6_U.weak.stderr
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/Z6_acq.rs
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/Z6_acq.stderr
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/atomicpo.rs
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/atomicpo.stderr
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/cumul-release.rs
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/cumul-release.stderr
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/inc2w.rs
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/inc2w.stderr
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/inc_inc_RR_W_RR.rs
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/inc_inc_RR_W_RR.stderr
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/riwi.rs
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/riwi.stderr
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.rs
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.stderr

(limited to 'src/tools/miri/genmc-sys/cpp/include')

diff --git a/src/tools/miri/doc/genmc.md b/src/tools/miri/doc/genmc.md
index fdbf2defe42..8af697be34a 100644
--- a/src/tools/miri/doc/genmc.md
+++ b/src/tools/miri/doc/genmc.md
@@ -24,6 +24,9 @@ Note that `cargo miri test` in GenMC mode is currently not supported.
 ### Supported Parameters
 
 - `-Zmiri-genmc`: Enable GenMC mode (not required if any other GenMC options are used).
+- `-Zmiri-genmc-print-exec-graphs={none,explored,blocked,all}`: Make GenMC print the execution graph of the program after every explored, every blocked, or after every execution (default: None).
+- `-Zmiri-genmc-print-exec-graphs`: Shorthand for suffix `=explored`.
+- `-Zmiri-genmc-print-genmc-output`: Print the output that GenMC provides. NOTE: this output is quite verbose and the events in the printed execution graph are hard to map back to the Rust code location they originate from.
 - `-Zmiri-genmc-log=LOG_LEVEL`: Change the log level for GenMC. Default: `warning`.
   - `quiet`:    Disable logging.
   - `error`:    Print errors.
@@ -34,7 +37,9 @@ Note that `cargo miri test` in GenMC mode is currently not supported.
     - `debug2`:   Print the execution graph after every memory access.
     - `debug3`:   Print reads-from values considered by GenMC.
 
-<!-- FIXME(genmc): explain options. -->
+#### Regular Miri parameters useful for GenMC mode
+
+- `-Zmiri-disable-weak-memory-emulation`: Disable any weak memory effects (effectively upgrading all atomic orderings in the program to `SeqCst`). This option may reduce the number of explored program executions, but any bugs related to weak memory effects will be missed. This option can help determine if an error is caused by weak memory effects (i.e., if it disappears with this option enabled).
 
 <!-- FIXME(genmc): explain Miri-GenMC specific functions. -->
 
diff --git a/src/tools/miri/genmc-sys/build.rs b/src/tools/miri/genmc-sys/build.rs
index 8eb818a6b26..8d437c20a09 100644
--- a/src/tools/miri/genmc-sys/build.rs
+++ b/src/tools/miri/genmc-sys/build.rs
@@ -30,13 +30,23 @@ mod downloading {
     /// The GenMC commit we depend on. It must be available on the specified GenMC repository.
     pub(crate) const GENMC_COMMIT: &str = "af9cc9ccd5d412b16defc35dbf36571c63a19c76";
 
-    pub(crate) fn download_genmc() -> PathBuf {
+    /// Ensure that a local GenMC repo is present and set to the correct commit.
+    /// Return the path of the GenMC repo and whether the checked out commit was changed.
+    pub(crate) fn download_genmc() -> (PathBuf, bool) {
         let Ok(genmc_download_path) = PathBuf::from_str(GENMC_DOWNLOAD_PATH);
         let commit_oid = Oid::from_str(GENMC_COMMIT).expect("Commit should be valid.");
 
         match Repository::open(&genmc_download_path) {
             Ok(repo) => {
                 assert_repo_unmodified(&repo);
+                if let Ok(head) = repo.head()
+                    && let Ok(head_commit) = head.peel_to_commit()
+                    && head_commit.id() == commit_oid
+                {
+                    // Fast path: The expected commit is already checked out.
+                    return (genmc_download_path, false);
+                }
+                // Check if the local repository already contains the commit we need, download it otherwise.
                 let commit = update_local_repo(&repo, commit_oid);
                 checkout_commit(&repo, &commit);
             }
@@ -51,7 +61,7 @@ mod downloading {
             }
         };
 
-        genmc_download_path
+        (genmc_download_path, true)
     }
 
     fn get_remote(repo: &Repository) -> Remote<'_> {
@@ -71,7 +81,8 @@ mod downloading {
 
         // Update remote URL.
         println!(
-            "cargo::warning=GenMC repository remote URL has changed from '{remote_url:?}' to '{GENMC_GITHUB_URL}'"
+            "cargo::warning=GenMC repository remote URL has changed from '{}' to '{GENMC_GITHUB_URL}'",
+            remote_url.unwrap_or_default()
         );
         repo.remote_set_url("origin", GENMC_GITHUB_URL)
             .expect("cannot rename url of remote 'origin'");
@@ -175,7 +186,7 @@ fn link_to_llvm(config_file: &Path) -> (String, String) {
 }
 
 /// Build the GenMC model checker library and the Rust-C++ interop library with cxx.rs
-fn compile_cpp_dependencies(genmc_path: &Path) {
+fn compile_cpp_dependencies(genmc_path: &Path, always_configure: bool) {
     // Give each step a separate build directory to prevent interference.
     let out_dir = PathBuf::from(std::env::var("OUT_DIR").as_deref().unwrap());
     let genmc_build_dir = out_dir.join("genmc");
@@ -184,15 +195,13 @@ fn compile_cpp_dependencies(genmc_path: &Path) {
     // Part 1:
     // Compile the GenMC library using cmake.
 
-    let cmakelists_path = genmc_path.join("CMakeLists.txt");
-
     // FIXME(genmc,cargo): Switch to using `CARGO_CFG_DEBUG_ASSERTIONS` once https://github.com/rust-lang/cargo/issues/15760 is completed.
     // Enable/disable additional debug checks, prints and options for GenMC, based on the Rust profile (debug/release)
     let enable_genmc_debug = matches!(std::env::var("PROFILE").as_deref().unwrap(), "debug");
 
-    let mut config = cmake::Config::new(cmakelists_path);
+    let mut config = cmake::Config::new(genmc_path);
     config
-        .always_configure(false) // We don't need to reconfigure on subsequent compilation runs.
+        .always_configure(always_configure) // We force running the configure step when the GenMC commit changed.
         .out_dir(genmc_build_dir)
         .profile(GENMC_CMAKE_PROFILE)
         .define("GENMC_DEBUG", if enable_genmc_debug { "ON" } else { "OFF" });
@@ -251,7 +260,8 @@ fn compile_cpp_dependencies(genmc_path: &Path) {
 
 fn main() {
     // Select which path to use for the GenMC repo:
-    let genmc_path = if let Some(genmc_src_path) = option_env!("GENMC_SRC_PATH") {
+    let (genmc_path, always_configure) = if let Some(genmc_src_path) = option_env!("GENMC_SRC_PATH")
+    {
         let genmc_src_path =
             PathBuf::from_str(&genmc_src_path).expect("GENMC_SRC_PATH should contain a valid path");
         assert!(
@@ -261,13 +271,18 @@ fn main() {
         );
         // Rebuild files in the given path change.
         println!("cargo::rerun-if-changed={}", genmc_src_path.display());
-        genmc_src_path
+        // We disable `always_configure` when working with a local repository,
+        // since it increases compile times when working on `genmc-sys`.
+        (genmc_src_path, false)
     } else {
+        // Download GenMC if required and ensure that the correct commit is checked out.
+        // If anything changed in the downloaded repository (e.g., the commit),
+        // we set `always_configure` to ensure there are no weird configs from previous builds.
         downloading::download_genmc()
     };
 
     // Build all required components:
-    compile_cpp_dependencies(&genmc_path);
+    compile_cpp_dependencies(&genmc_path, always_configure);
 
     // Only rebuild if anything changes:
     // Note that we don't add the downloaded GenMC repo, since that should never be modified
diff --git a/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp b/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp
index 4484f0b73ca..b0769375843 100644
--- a/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp
+++ b/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp
@@ -33,6 +33,7 @@ struct GenmcScalar;
 struct SchedulingResult;
 struct LoadResult;
 struct StoreResult;
+struct ReadModifyWriteResult;
 
 // GenMC uses `int` for its thread IDs.
 using ThreadId = int;
@@ -90,6 +91,15 @@ struct MiriGenmcShim : private GenMCDriver {
         MemOrdering ord,
         GenmcScalar old_val
     );
+    [[nodiscard]] ReadModifyWriteResult handle_read_modify_write(
+        ThreadId thread_id,
+        uint64_t address,
+        uint64_t size,
+        RMWBinOp rmw_op,
+        MemOrdering ordering,
+        GenmcScalar rhs_value,
+        GenmcScalar old_val
+    );
     [[nodiscard]] StoreResult handle_store(
         ThreadId thread_id,
         uint64_t address,
@@ -99,6 +109,8 @@ struct MiriGenmcShim : private GenMCDriver {
         MemOrdering ord
     );
 
+    void handle_fence(ThreadId thread_id, MemOrdering ord);
+
     /**** Memory (de)allocation ****/
     auto handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment) -> uint64_t;
     void handle_free(ThreadId thread_id, uint64_t address);
@@ -271,4 +283,21 @@ inline StoreResult from_error(std::unique_ptr<std::string> error) {
 }
 } // namespace StoreResultExt
 
+namespace ReadModifyWriteResultExt {
+inline ReadModifyWriteResult
+ok(SVal old_value, SVal new_value, bool is_coherence_order_maximal_write) {
+    return ReadModifyWriteResult { /* error: */ std::unique_ptr<std::string>(nullptr),
+                                   /* old_value: */ GenmcScalarExt::from_sval(old_value),
+                                   /* new_value: */ GenmcScalarExt::from_sval(new_value),
+                                   is_coherence_order_maximal_write };
+}
+
+inline ReadModifyWriteResult from_error(std::unique_ptr<std::string> error) {
+    return ReadModifyWriteResult { /* error: */ std::move(error),
+                                   /* old_value: */ GenmcScalarExt::uninit(),
+                                   /* new_value: */ GenmcScalarExt::uninit(),
+                                   /* is_coherence_order_maximal_write: */ false };
+}
+} // namespace ReadModifyWriteResultExt
+
 #endif /* GENMC_MIRI_INTERFACE_HPP */
diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp
index 7d8f0b16b49..cd28e0d148f 100644
--- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp
+++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp
@@ -89,6 +89,72 @@
     );
 }
 
+void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
+    const auto pos = inc_pos(thread_id);
+    GenMCDriver::handleFence(pos, ord, EventDeps());
+}
+
+[[nodiscard]] auto MiriGenmcShim::handle_read_modify_write(
+    ThreadId thread_id,
+    uint64_t address,
+    uint64_t size,
+    RMWBinOp rmw_op,
+    MemOrdering ordering,
+    GenmcScalar rhs_value,
+    GenmcScalar old_val
+) -> ReadModifyWriteResult {
+    // NOTE: Both the store and load events should get the same `ordering`, it should not be split
+    // into a load and a store component. This means we can have for example `AcqRel` loads and
+    // stores, but this is intended for RMW operations.
+
+    // Somewhat confusingly, the GenMC term for RMW read/write labels is
+    // `FaiRead` and `FaiWrite`.
+    const auto load_ret = handle_load_reset_if_none<EventLabel::EventLabelKind::FaiRead>(
+        thread_id,
+        ordering,
+        SAddr(address),
+        ASize(size),
+        AType::Unsigned, // The type is only used for printing.
+        rmw_op,
+        GenmcScalarExt::to_sval(rhs_value),
+        EventDeps()
+    );
+    if (const auto* err = std::get_if<VerificationError>(&load_ret))
+        return ReadModifyWriteResultExt::from_error(format_error(*err));
+
+    const auto* ret_val = std::get_if<SVal>(&load_ret);
+    if (nullptr == ret_val) {
+        ERROR("Unimplemented: read-modify-write returned unexpected result.");
+    }
+    const auto read_old_val = *ret_val;
+    const auto new_value =
+        executeRMWBinOp(read_old_val, GenmcScalarExt::to_sval(rhs_value), size, rmw_op);
+
+    const auto storePos = inc_pos(thread_id);
+    const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::FaiWrite>(
+        storePos,
+        ordering,
+        SAddr(address),
+        ASize(size),
+        AType::Unsigned, // The type is only used for printing.
+        new_value
+    );
+    if (const auto* err = std::get_if<VerificationError>(&store_ret))
+        return ReadModifyWriteResultExt::from_error(format_error(*err));
+
+    const auto* store_ret_val = std::get_if<std::monostate>(&store_ret);
+    ERROR_ON(nullptr == store_ret_val, "Unimplemented: RMW store returned unexpected result.");
+
+    // FIXME(genmc,mixed-accesses): Use the value that GenMC returns from handleStore (once
+    // available).
+    const auto& g = getExec().getGraph();
+    return ReadModifyWriteResultExt::ok(
+        /* old_value: */ read_old_val,
+        new_value,
+        /* is_coherence_order_maximal_write */ g.co_max(SAddr(address))->getPos() == storePos
+    );
+}
+
 /**** Memory (de)allocation ****/
 
 auto MiriGenmcShim::handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment)
diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp
index 7194ed02da4..5a53fee0592 100644
--- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp
+++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp
@@ -63,9 +63,12 @@ static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel
     auto conf = std::make_shared<Config>();
 
     // Set whether GenMC should print execution graphs after every explored/blocked execution.
-    // FIXME(genmc): pass these settings from Miri.
-    conf->printExecGraphs = false;
-    conf->printBlockedExecs = false;
+    conf->printExecGraphs =
+        (params.print_execution_graphs == ExecutiongraphPrinting::Explored ||
+         params.print_execution_graphs == ExecutiongraphPrinting::ExploredAndBlocked);
+    conf->printBlockedExecs =
+        (params.print_execution_graphs == ExecutiongraphPrinting::Blocked ||
+         params.print_execution_graphs == ExecutiongraphPrinting::ExploredAndBlocked);
 
     // `1024` is the default value that GenMC uses.
     // If any thread has at least this many events, a warning/tip will be printed.
@@ -79,8 +82,8 @@ static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel
     // Miri.
     conf->warnOnGraphSize = 1024 * 1024;
 
-    // We only support the RC11 memory model for Rust.
-    conf->model = ModelType::RC11;
+    // We only support the `RC11` memory model for Rust, and `SC` when weak memory emulation is disabled.
+    conf->model = params.disable_weak_memory_emulation ? ModelType::SC : ModelType::RC11;
 
     // This prints the seed that GenMC picks for randomized scheduling during estimation mode.
     conf->printRandomScheduleSeed = params.print_random_schedule_seed;
diff --git a/src/tools/miri/genmc-sys/src/lib.rs b/src/tools/miri/genmc-sys/src/lib.rs
index 406c90809fc..1de4c4eb5e8 100644
--- a/src/tools/miri/genmc-sys/src/lib.rs
+++ b/src/tools/miri/genmc-sys/src/lib.rs
@@ -53,7 +53,13 @@ impl GenmcScalar {
 
 impl Default for GenmcParams {
     fn default() -> Self {
-        Self { print_random_schedule_seed: false, do_symmetry_reduction: false }
+        Self {
+            print_random_schedule_seed: false,
+            do_symmetry_reduction: false,
+            // GenMC graphs can be quite large since Miri produces a lot of (non-atomic) events.
+            print_execution_graphs: ExecutiongraphPrinting::None,
+            disable_weak_memory_emulation: false,
+        }
     }
 }
 
@@ -91,7 +97,10 @@ mod ffi {
     struct GenmcParams {
         pub print_random_schedule_seed: bool,
         pub do_symmetry_reduction: bool,
-        // FIXME(GenMC): Add remaining parameters.
+        pub print_execution_graphs: ExecutiongraphPrinting,
+        /// Enabling this will set the memory model used by GenMC to "Sequential Consistency" (SC).
+        /// This will disable any weak memory effects, which reduces the number of program executions that will be explored.
+        pub disable_weak_memory_emulation: bool,
     }
 
     /// This is mostly equivalent to GenMC `VerbosityLevel`, but the debug log levels are always present (not conditionally compiled based on `ENABLE_GENMC_DEBUG`).
@@ -120,6 +129,19 @@ mod ffi {
         Debug3ReadsFrom,
     }
 
+    #[derive(Debug)]
+    /// Setting to control which execution graphs GenMC prints after every execution.
+    enum ExecutiongraphPrinting {
+        /// Print no graphs.
+        None,
+        /// Print graphs of all fully explored executions.
+        Explored,
+        /// Print graphs of all blocked executions.
+        Blocked,
+        /// Print graphs of all executions.
+        ExploredAndBlocked,
+    }
+
     /// This type corresponds to `Option<SVal>` (or `std::optional<SVal>`), where `SVal` is the type that GenMC uses for storing values.
     /// CXX doesn't support `std::optional` currently, so we need to use an extra `bool` to define whether this value is initialized or not.
     #[derive(Debug, Clone, Copy)]
@@ -163,7 +185,21 @@ mod ffi {
         is_coherence_order_maximal_write: bool,
     }
 
-    /**** Types shared between Miri/Rust and GenMC/C++ through cxx_bridge: ****/
+    #[must_use]
+    #[derive(Debug)]
+    struct ReadModifyWriteResult {
+        /// If there was an error, it will be stored in `error`, otherwise it is `None`.
+        error: UniquePtr<CxxString>,
+        /// The value that was read by the RMW operation as the left operand.
+        old_value: GenmcScalar,
+        /// The value that was produced by the RMW operation.
+        new_value: GenmcScalar,
+        /// `true` if the write should also be reflected in Miri's memory representation.
+        is_coherence_order_maximal_write: bool,
+    }
+
+    /**** These are GenMC types that we have to copy-paste here since cxx does not support
+    "importing" externally defined C++ types. ****/
 
     #[derive(Debug)]
     /// Corresponds to GenMC's type with the same name.
@@ -188,6 +224,21 @@ mod ffi {
         SequentiallyConsistent = 6,
     }
 
+    #[derive(Debug)]
+    enum RMWBinOp {
+        Xchg = 0,
+        Add = 1,
+        Sub = 2,
+        And = 3,
+        Nand = 4,
+        Or = 5,
+        Xor = 6,
+        Max = 7,
+        Min = 8,
+        UMax = 9,
+        UMin = 10,
+    }
+
     // # Safety
     //
     // This block is unsafe to allow defining safe methods inside.
@@ -202,9 +253,12 @@ mod ffi {
         /**** Types shared between Miri/Rust and Miri/C++: ****/
         type MiriGenmcShim;
 
-        /**** Types shared between Miri/Rust and GenMC/C++: ****/
+        /**** Types shared between Miri/Rust and GenMC/C++:
+        (This tells cxx that the enums defined above are already defined on the C++ side;
+        it will emit assertions to ensure that the two definitions agree.) ****/
         type ActionKind;
         type MemOrdering;
+        type RMWBinOp;
 
         /// Set the log level for GenMC.
         ///
@@ -249,6 +303,16 @@ mod ffi {
             memory_ordering: MemOrdering,
             old_value: GenmcScalar,
         ) -> LoadResult;
+        fn handle_read_modify_write(
+            self: Pin<&mut MiriGenmcShim>,
+            thread_id: i32,
+            address: u64,
+            size: u64,
+            rmw_op: RMWBinOp,
+            ordering: MemOrdering,
+            rhs_value: GenmcScalar,
+            old_value: GenmcScalar,
+        ) -> ReadModifyWriteResult;
         fn handle_store(
             self: Pin<&mut MiriGenmcShim>,
             thread_id: i32,
@@ -258,6 +322,11 @@ mod ffi {
             old_value: GenmcScalar,
             memory_ordering: MemOrdering,
         ) -> StoreResult;
+        fn handle_fence(
+            self: Pin<&mut MiriGenmcShim>,
+            thread_id: i32,
+            memory_ordering: MemOrdering,
+        );
 
         /**** Memory (de)allocation ****/
         fn handle_malloc(
diff --git a/src/tools/miri/src/bin/miri.rs b/src/tools/miri/src/bin/miri.rs
index ff05b4b14c7..731fe283a21 100644
--- a/src/tools/miri/src/bin/miri.rs
+++ b/src/tools/miri/src/bin/miri.rs
@@ -746,24 +746,11 @@ fn main() {
         many_seeds.map(|seeds| ManySeedsConfig { seeds, keep_going: many_seeds_keep_going });
 
     // Validate settings for data race detection and GenMC mode.
-    if miri_config.genmc_config.is_some() {
-        if !miri_config.data_race_detector {
-            fatal_error!("Cannot disable data race detection in GenMC mode");
-        } else if !miri_config.weak_memory_emulation {
-            fatal_error!("Cannot disable weak memory emulation in GenMC mode");
-        } else if !miri_config.native_lib.is_empty() {
-            fatal_error!("native-lib not supported in GenMC mode.");
-        }
-        if miri_config.borrow_tracker.is_some() {
-            eprintln!(
-                "warning: borrow tracking has been disabled, it is not (yet) supported in GenMC mode."
-            );
-            miri_config.borrow_tracker = None;
-        }
-        // We enable fixed scheduling so Miri doesn't randomly yield before a terminator, which anyway
-        // would be a NOP in GenMC mode.
-        miri_config.fixed_scheduling = true;
-    } else if miri_config.weak_memory_emulation && !miri_config.data_race_detector {
+    if let Err(err) = GenmcConfig::validate_genmc_mode_settings(&mut miri_config) {
+        fatal_error!("Invalid settings: {err}");
+    }
+
+    if miri_config.weak_memory_emulation && !miri_config.data_race_detector {
         fatal_error!(
             "Weak memory emulation cannot be enabled when the data race detector is disabled"
         );
diff --git a/src/tools/miri/src/concurrency/data_race.rs b/src/tools/miri/src/concurrency/data_race.rs
index a7822d0d6fa..30061a78594 100644
--- a/src/tools/miri/src/concurrency/data_race.rs
+++ b/src/tools/miri/src/concurrency/data_race.rs
@@ -793,9 +793,9 @@ pub trait EvalContextExt<'tcx>: MiriInterpCxExt<'tcx> {
                 this,
                 place.ptr().addr(),
                 place.layout.size,
+                atomic_op,
                 place.layout.backend_repr.is_signed(),
                 ord,
-                atomic_op,
                 rhs.to_scalar(),
                 old.to_scalar(),
             )?;
@@ -901,7 +901,6 @@ pub trait EvalContextExt<'tcx>: MiriInterpCxExt<'tcx> {
                 can_fail_spuriously,
                 old.to_scalar(),
             )?;
-
             // The store might be the latest store in coherence order (determined by GenMC).
             // If it is, we need to update the value in Miri's memory:
             if let Some(new_value) = new_value {
@@ -961,6 +960,11 @@ pub trait EvalContextExt<'tcx>: MiriInterpCxExt<'tcx> {
     /// The closure will only be invoked if data race handling is on.
     fn release_clock<R>(&self, callback: impl FnOnce(&VClock) -> R) -> Option<R> {
         let this = self.eval_context_ref();
+        // FIXME: make this a proper error instead of ICEing the interpreter.
+        assert!(
+            this.machine.data_race.as_genmc_ref().is_none(),
+            "this operation performs synchronization that is not supported in GenMC mode"
+        );
         Some(
             this.machine.data_race.as_vclocks_ref()?.release_clock(&this.machine.threads, callback),
         )
@@ -973,7 +977,9 @@ pub trait EvalContextExt<'tcx>: MiriInterpCxExt<'tcx> {
         match &this.machine.data_race {
             GlobalDataRaceHandler::None => {}
             GlobalDataRaceHandler::Genmc(_genmc_ctx) =>
-                throw_unsup_format!("acquire_clock is not (yet) supported in GenMC mode."),
+                throw_unsup_format!(
+                    "this operation performs synchronization that is not supported in GenMC mode"
+                ),
             GlobalDataRaceHandler::Vclocks(data_race) =>
                 data_race.acquire_clock(clock, &this.machine.threads),
         }
diff --git a/src/tools/miri/src/concurrency/genmc/config.rs b/src/tools/miri/src/concurrency/genmc/config.rs
index 66116d5cf23..34933d423f0 100644
--- a/src/tools/miri/src/concurrency/genmc/config.rs
+++ b/src/tools/miri/src/concurrency/genmc/config.rs
@@ -1,4 +1,7 @@
-use genmc_sys::{GenmcParams, LogLevel};
+use genmc_sys::LogLevel;
+
+use super::GenmcParams;
+use crate::{IsolatedOp, MiriConfig, RejectOpWith};
 
 /// Configuration for GenMC mode.
 /// The `params` field is shared with the C++ side.
@@ -7,6 +10,9 @@ use genmc_sys::{GenmcParams, LogLevel};
 pub struct GenmcConfig {
     /// Parameters sent to the C++ side to create a new handle to the GenMC model checker.
     pub(super) params: GenmcParams,
+    /// Print the output message that GenMC generates when an error occurs.
+    /// This error message is currently hard to use, since there is no clear mapping between the events that GenMC sees and the Rust code location where this event was produced.
+    pub(super) print_genmc_output: bool,
     /// The log level for GenMC.
     pub(super) log_level: LogLevel,
 }
@@ -36,9 +42,61 @@ impl GenmcConfig {
         };
         if let Some(log_level) = trimmed_arg.strip_prefix("log=") {
             genmc_config.log_level = log_level.parse()?;
+        } else if let Some(trimmed_arg) = trimmed_arg.strip_prefix("print-exec-graphs") {
+            use genmc_sys::ExecutiongraphPrinting;
+            genmc_config.params.print_execution_graphs = match trimmed_arg {
+                "=none" => ExecutiongraphPrinting::None,
+                // Make GenMC print explored executions.
+                "" | "=explored" => ExecutiongraphPrinting::Explored,
+                // Make GenMC print blocked executions.
+                "=blocked" => ExecutiongraphPrinting::Blocked,
+                // Make GenMC print all executions.
+                "=all" => ExecutiongraphPrinting::ExploredAndBlocked,
+                _ =>
+                    return Err(format!(
+                        "Invalid suffix to GenMC argument '-Zmiri-genmc-print-exec-graphs', expected '', '=none', '=explored', '=blocked' or '=all'"
+                    )),
+            }
+        } else if trimmed_arg == "print-genmc-output" {
+            genmc_config.print_genmc_output = true;
         } else {
             return Err(format!("Invalid GenMC argument: \"-Zmiri-genmc-{trimmed_arg}\""));
         }
         Ok(())
     }
+
+    /// Validate settings for GenMC mode (NOP if GenMC mode disabled).
+    ///
+    /// Unsupported configurations return an error.
+    /// Adjusts Miri settings where required, printing a warnings if the change might be unexpected for the user.
+    pub fn validate_genmc_mode_settings(miri_config: &mut MiriConfig) -> Result<(), &'static str> {
+        let Some(genmc_config) = miri_config.genmc_config.as_mut() else {
+            return Ok(());
+        };
+
+        // Check for disallowed configurations.
+        if !miri_config.data_race_detector {
+            return Err("Cannot disable data race detection in GenMC mode");
+        } else if !miri_config.native_lib.is_empty() {
+            return Err("native-lib not supported in GenMC mode.");
+        } else if miri_config.isolated_op != IsolatedOp::Reject(RejectOpWith::Abort) {
+            return Err("Cannot disable isolation in GenMC mode");
+        }
+
+        // Adjust settings where needed.
+        if !miri_config.weak_memory_emulation {
+            genmc_config.params.disable_weak_memory_emulation = true;
+        }
+        if miri_config.borrow_tracker.is_some() {
+            eprintln!(
+                "warning: borrow tracking has been disabled, it is not (yet) supported in GenMC mode."
+            );
+            miri_config.borrow_tracker = None;
+        }
+        // We enable fixed scheduling so Miri doesn't randomly yield before a terminator, which anyway
+        // would be a NOP in GenMC mode.
+        miri_config.fixed_scheduling = true;
+
+        Ok(())
+    }
 }
diff --git a/src/tools/miri/src/concurrency/genmc/dummy.rs b/src/tools/miri/src/concurrency/genmc/dummy.rs
index 7c420961ec5..92b34b83ee0 100644
--- a/src/tools/miri/src/concurrency/genmc/dummy.rs
+++ b/src/tools/miri/src/concurrency/genmc/dummy.rs
@@ -94,9 +94,9 @@ impl GenmcCtx {
         _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
         _address: Size,
         _size: Size,
+        _atomic_op: AtomicRmwOp,
         _is_signed: bool,
         _ordering: AtomicRwOrd,
-        _atomic_op: AtomicRmwOp,
         _rhs_scalar: Scalar,
         _old_value: Scalar,
     ) -> InterpResult<'tcx, (Scalar, Option<Scalar>)> {
@@ -242,4 +242,10 @@ impl GenmcConfig {
             Err(format!("GenMC is not supported on this target"))
         }
     }
+
+    pub fn validate_genmc_mode_settings(
+        _miri_config: &mut crate::MiriConfig,
+    ) -> Result<(), &'static str> {
+        Ok(())
+    }
 }
diff --git a/src/tools/miri/src/concurrency/genmc/helper.rs b/src/tools/miri/src/concurrency/genmc/helper.rs
index b70ca8faadf..2a84ca20366 100644
--- a/src/tools/miri/src/concurrency/genmc/helper.rs
+++ b/src/tools/miri/src/concurrency/genmc/helper.rs
@@ -1,11 +1,16 @@
-use genmc_sys::MemOrdering;
+use genmc_sys::{MemOrdering, RMWBinOp};
 use rustc_abi::Size;
 use rustc_const_eval::interpret::{InterpResult, interp_ok};
+use rustc_middle::mir;
 use rustc_middle::ty::ScalarInt;
 use tracing::debug;
 
 use super::GenmcScalar;
-use crate::{AtomicReadOrd, AtomicWriteOrd, MiriInterpCx, Scalar, throw_unsup_format};
+use crate::intrinsics::AtomicRmwOp;
+use crate::{
+    AtomicFenceOrd, AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd, MiriInterpCx, Scalar,
+    throw_unsup_format,
+};
 
 /// Maximum size memory access in bytes that GenMC supports.
 pub(super) const MAX_ACCESS_SIZE: u64 = 8;
@@ -95,3 +100,48 @@ impl AtomicWriteOrd {
         }
     }
 }
+
+impl AtomicFenceOrd {
+    pub(super) fn to_genmc(self) -> MemOrdering {
+        match self {
+            AtomicFenceOrd::Acquire => MemOrdering::Acquire,
+            AtomicFenceOrd::Release => MemOrdering::Release,
+            AtomicFenceOrd::AcqRel => MemOrdering::AcquireRelease,
+            AtomicFenceOrd::SeqCst => MemOrdering::SequentiallyConsistent,
+        }
+    }
+}
+
+impl AtomicRwOrd {
+    pub(super) fn to_genmc(self) -> MemOrdering {
+        match self {
+            AtomicRwOrd::Relaxed => MemOrdering::Relaxed,
+            AtomicRwOrd::Acquire => MemOrdering::Acquire,
+            AtomicRwOrd::Release => MemOrdering::Release,
+            AtomicRwOrd::AcqRel => MemOrdering::AcquireRelease,
+            AtomicRwOrd::SeqCst => MemOrdering::SequentiallyConsistent,
+        }
+    }
+}
+
+/// Convert an atomic binary operation to its GenMC counterpart.
+pub(super) fn to_genmc_rmw_op(atomic_op: AtomicRmwOp, is_signed: bool) -> RMWBinOp {
+    match (atomic_op, is_signed) {
+        (AtomicRmwOp::Min, true) => RMWBinOp::Min,
+        (AtomicRmwOp::Max, true) => RMWBinOp::Max,
+        (AtomicRmwOp::Min, false) => RMWBinOp::UMin,
+        (AtomicRmwOp::Max, false) => RMWBinOp::UMax,
+        (AtomicRmwOp::MirOp { op, neg }, _is_signed) =>
+            match (op, neg) {
+                (mir::BinOp::Add, false) => RMWBinOp::Add,
+                (mir::BinOp::Sub, false) => RMWBinOp::Sub,
+                (mir::BinOp::BitXor, false) => RMWBinOp::Xor,
+                (mir::BinOp::BitAnd, false) => RMWBinOp::And,
+                (mir::BinOp::BitAnd, true) => RMWBinOp::Nand,
+                (mir::BinOp::BitOr, false) => RMWBinOp::Or,
+                _ => {
+                    panic!("unsupported atomic operation: bin_op: {op:?}, negate: {neg}");
+                }
+            },
+    }
+}
diff --git a/src/tools/miri/src/concurrency/genmc/mod.rs b/src/tools/miri/src/concurrency/genmc/mod.rs
index 26ce0b9c43a..c1da86c6733 100644
--- a/src/tools/miri/src/concurrency/genmc/mod.rs
+++ b/src/tools/miri/src/concurrency/genmc/mod.rs
@@ -2,7 +2,7 @@ use std::cell::{Cell, RefCell};
 use std::sync::Arc;
 
 use genmc_sys::{
-    GENMC_GLOBAL_ADDRESSES_MASK, GenmcScalar, MemOrdering, MiriGenmcShim, UniquePtr,
+    GENMC_GLOBAL_ADDRESSES_MASK, GenmcScalar, MemOrdering, MiriGenmcShim, RMWBinOp, UniquePtr,
     create_genmc_driver_handle,
 };
 use rustc_abi::{Align, Size};
@@ -12,7 +12,9 @@ use rustc_middle::{throw_machine_stop, throw_ub_format, throw_unsup_format};
 use tracing::{debug, info};
 
 use self::global_allocations::{EvalContextExt as _, GlobalAllocationHandler};
-use self::helper::{MAX_ACCESS_SIZE, genmc_scalar_to_scalar, scalar_to_genmc_scalar};
+use self::helper::{
+    MAX_ACCESS_SIZE, genmc_scalar_to_scalar, scalar_to_genmc_scalar, to_genmc_rmw_op,
+};
 use self::thread_id_map::ThreadIdMap;
 use crate::concurrency::genmc::helper::split_access;
 use crate::intrinsics::AtomicRmwOp;
@@ -29,6 +31,8 @@ mod run;
 pub(crate) mod scheduling;
 mod thread_id_map;
 
+pub use genmc_sys::GenmcParams;
+
 pub use self::config::GenmcConfig;
 pub use self::run::run_genmc_mode;
 
@@ -126,22 +130,19 @@ impl GenmcCtx {
 
     /// Get the number of blocked executions encountered by GenMC.
     pub fn get_blocked_execution_count(&self) -> u64 {
-        let mc = self.handle.borrow();
-        mc.as_ref().unwrap().get_blocked_execution_count()
+        self.handle.borrow().get_blocked_execution_count()
     }
 
     /// Get the number of explored executions encountered by GenMC.
     pub fn get_explored_execution_count(&self) -> u64 {
-        let mc = self.handle.borrow();
-        mc.as_ref().unwrap().get_explored_execution_count()
+        self.handle.borrow().get_explored_execution_count()
     }
 
     /// Check if GenMC encountered an error that wasn't immediately returned during execution.
     /// Returns a string representation of the error if one occurred.
     pub fn try_get_error(&self) -> Option<String> {
-        let mc = self.handle.borrow();
-        mc.as_ref()
-            .unwrap()
+        self.handle
+            .borrow()
             .get_error_string()
             .as_ref()
             .map(|error| error.to_string_lossy().to_string())
@@ -150,9 +151,8 @@ impl GenmcCtx {
     /// Check if GenMC encountered an error that wasn't immediately returned during execution.
     /// Returns a string representation of the error if one occurred.
     pub fn get_result_message(&self) -> String {
-        let mc = self.handle.borrow();
-        mc.as_ref()
-            .unwrap()
+        self.handle
+            .borrow()
             .get_result_message()
             .as_ref()
             .map(|error| error.to_string_lossy().to_string())
@@ -163,8 +163,7 @@ impl GenmcCtx {
     ///
     /// In GenMC mode, the input program should be repeatedly executed until this function returns `true` or an error is found.
     pub fn is_exploration_done(&self) -> bool {
-        let mut mc = self.handle.borrow_mut();
-        mc.as_mut().unwrap().is_exploration_done()
+        self.handle.borrow_mut().pin_mut().is_exploration_done()
     }
 
     /// Select whether data race free actions should be allowed. This function should be used carefully!
@@ -196,8 +195,7 @@ impl GenmcCtx {
         // Reset per-execution state.
         self.exec_state.reset();
         // Inform GenMC about the new execution.
-        let mut mc = self.handle.borrow_mut();
-        mc.as_mut().unwrap().handle_execution_start();
+        self.handle.borrow_mut().pin_mut().handle_execution_start();
     }
 
     /// Inform GenMC that the program's execution has ended.
@@ -214,13 +212,11 @@ impl GenmcCtx {
     ///
     /// To get the all messages (warnings, errors) that GenMC produces, use the `get_result_message` method.
     fn handle_execution_end(&self) -> Option<String> {
-        let mut mc = self.handle.borrow_mut();
-        let result = mc.as_mut().unwrap().handle_execution_end();
+        let result = self.handle.borrow_mut().pin_mut().handle_execution_end();
         result.as_ref().map(|msg| msg.to_string_lossy().to_string())?;
 
         // GenMC currently does not return an error value immediately in all cases.
         // We manually query for any errors here to ensure we don't miss any.
-        drop(mc); // `try_get_error` needs access to the `RefCell`.
         self.try_get_error()
     }
 
@@ -282,11 +278,17 @@ impl GenmcCtx {
     /// Inform GenMC about an atomic fence.
     pub(crate) fn atomic_fence<'tcx>(
         &self,
-        _machine: &MiriMachine<'tcx>,
-        _ordering: AtomicFenceOrd,
+        machine: &MiriMachine<'tcx>,
+        ordering: AtomicFenceOrd,
     ) -> InterpResult<'tcx> {
         assert!(!self.get_alloc_data_races(), "atomic fence with data race checking disabled.");
-        throw_unsup_format!("FIXME(genmc): Add support for atomic fences.")
+
+        let thread_infos = self.exec_state.thread_id_manager.borrow();
+        let curr_thread = machine.threads.active_thread();
+        let genmc_tid = thread_infos.get_genmc_tid(curr_thread);
+
+        self.handle.borrow_mut().pin_mut().handle_fence(genmc_tid, ordering.to_genmc());
+        interp_ok(())
     }
 
     /// Inform GenMC about an atomic read-modify-write operation.
@@ -296,20 +298,24 @@ impl GenmcCtx {
     /// `old_value` is the value that a non-atomic load would read here, or `None` if the memory is uninitalized.
     pub(crate) fn atomic_rmw_op<'tcx>(
         &self,
-        _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
-        _address: Size,
-        _size: Size,
-        _is_signed: bool,
-        _ordering: AtomicRwOrd,
-        _atomic_op: AtomicRmwOp,
-        _rhs_scalar: Scalar,
-        _old_value: Scalar,
+        ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
+        address: Size,
+        size: Size,
+        atomic_op: AtomicRmwOp,
+        is_signed: bool,
+        ordering: AtomicRwOrd,
+        rhs_scalar: Scalar,
+        old_value: Scalar,
     ) -> InterpResult<'tcx, (Scalar, Option<Scalar>)> {
-        assert!(
-            !self.get_alloc_data_races(),
-            "atomic read-modify-write operation with data race checking disabled."
-        );
-        throw_unsup_format!("FIXME(genmc): Add support for atomic RMW.")
+        self.handle_atomic_rmw_op(
+            ecx,
+            address,
+            size,
+            ordering,
+            to_genmc_rmw_op(atomic_op, is_signed),
+            scalar_to_genmc_scalar(ecx, rhs_scalar)?,
+            scalar_to_genmc_scalar(ecx, old_value)?,
+        )
     }
 
     /// Returns `(old_val, Option<new_val>)`. `new_val` might not be the latest write in coherence order, which is indicated by `None`.
@@ -317,18 +323,22 @@ impl GenmcCtx {
     /// `old_value` is the value that a non-atomic load would read here, or `None` if the memory is uninitalized.
     pub(crate) fn atomic_exchange<'tcx>(
         &self,
-        _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
-        _address: Size,
-        _size: Size,
-        _rhs_scalar: Scalar,
-        _ordering: AtomicRwOrd,
-        _old_value: Scalar,
+        ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
+        address: Size,
+        size: Size,
+        rhs_scalar: Scalar,
+        ordering: AtomicRwOrd,
+        old_value: Scalar,
     ) -> InterpResult<'tcx, (Scalar, Option<Scalar>)> {
-        assert!(
-            !self.get_alloc_data_races(),
-            "atomic swap operation with data race checking disabled."
-        );
-        throw_unsup_format!("FIXME(genmc): Add support for atomic swap.")
+        self.handle_atomic_rmw_op(
+            ecx,
+            address,
+            size,
+            ordering,
+            /* genmc_rmw_op */ RMWBinOp::Xchg,
+            scalar_to_genmc_scalar(ecx, rhs_scalar)?,
+            scalar_to_genmc_scalar(ecx, old_value)?,
+        )
     }
 
     /// Inform GenMC about an atomic compare-exchange operation.
@@ -493,9 +503,11 @@ impl GenmcCtx {
         // GenMC doesn't support ZSTs, so we set the minimum size to 1 byte
         let genmc_size = size.bytes().max(1);
 
-        let mut mc = self.handle.borrow_mut();
-        let pinned_mc = mc.as_mut().unwrap();
-        let chosen_address = pinned_mc.handle_malloc(genmc_tid, genmc_size, alignment.bytes());
+        let chosen_address = self.handle.borrow_mut().pin_mut().handle_malloc(
+            genmc_tid,
+            genmc_size,
+            alignment.bytes(),
+        );
 
         // Non-global addresses should not be in the global address space or null.
         assert_ne!(0, chosen_address, "GenMC malloc returned nullptr.");
@@ -530,9 +542,7 @@ impl GenmcCtx {
         let curr_thread = machine.threads.active_thread();
         let genmc_tid = thread_infos.get_genmc_tid(curr_thread);
 
-        let mut mc = self.handle.borrow_mut();
-        let pinned_mc = mc.as_mut().unwrap();
-        pinned_mc.handle_free(genmc_tid, address.bytes());
+        self.handle.borrow_mut().pin_mut().handle_free(genmc_tid, address.bytes());
 
         interp_ok(())
     }
@@ -554,9 +564,7 @@ impl GenmcCtx {
         let genmc_parent_tid = thread_infos.get_genmc_tid(curr_thread_id);
         let genmc_new_tid = thread_infos.add_thread(new_thread_id);
 
-        let mut mc = self.handle.borrow_mut();
-        mc.as_mut().unwrap().handle_thread_create(genmc_new_tid, genmc_parent_tid);
-
+        self.handle.borrow_mut().pin_mut().handle_thread_create(genmc_new_tid, genmc_parent_tid);
         interp_ok(())
     }
 
@@ -571,8 +579,7 @@ impl GenmcCtx {
         let genmc_curr_tid = thread_infos.get_genmc_tid(active_thread_id);
         let genmc_child_tid = thread_infos.get_genmc_tid(child_thread_id);
 
-        let mut mc = self.handle.borrow_mut();
-        mc.as_mut().unwrap().handle_thread_join(genmc_curr_tid, genmc_child_tid);
+        self.handle.borrow_mut().pin_mut().handle_thread_join(genmc_curr_tid, genmc_child_tid);
 
         interp_ok(())
     }
@@ -585,9 +592,8 @@ impl GenmcCtx {
         let genmc_tid = thread_infos.get_genmc_tid(curr_thread_id);
 
         debug!("GenMC: thread {curr_thread_id:?} ({genmc_tid:?}) finished.");
-        let mut mc = self.handle.borrow_mut();
         // NOTE: Miri doesn't support return values for threads, but GenMC expects one, so we return 0
-        mc.as_mut().unwrap().handle_thread_finish(genmc_tid, /* ret_val */ 0);
+        self.handle.borrow_mut().pin_mut().handle_thread_finish(genmc_tid, /* ret_val */ 0);
     }
 
     /// Handle a call to `libc::exit` or the exit of the main thread.
@@ -618,8 +624,7 @@ impl GenmcCtx {
             let thread_infos = self.exec_state.thread_id_manager.borrow();
             let genmc_tid = thread_infos.get_genmc_tid(thread);
 
-            let mut mc = self.handle.borrow_mut();
-            mc.as_mut().unwrap().handle_thread_kill(genmc_tid);
+            self.handle.borrow_mut().pin_mut().handle_thread_kill(genmc_tid);
         } else {
             assert_eq!(thread, ThreadId::MAIN_THREAD);
         }
@@ -669,9 +674,7 @@ impl GenmcCtx {
             addr = address.bytes()
         );
 
-        let mut mc = self.handle.borrow_mut();
-        let pinned_mc = mc.as_mut().unwrap();
-        let load_result = pinned_mc.handle_load(
+        let load_result = self.handle.borrow_mut().pin_mut().handle_load(
             genmc_tid,
             address.bytes(),
             size.bytes(),
@@ -722,9 +725,7 @@ impl GenmcCtx {
             addr = address.bytes()
         );
 
-        let mut mc = self.handle.borrow_mut();
-        let pinned_mc = mc.as_mut().unwrap();
-        let store_result = pinned_mc.handle_store(
+        let store_result = self.handle.borrow_mut().pin_mut().handle_store(
             genmc_tid,
             address.bytes(),
             size.bytes(),
@@ -741,6 +742,62 @@ impl GenmcCtx {
         interp_ok(store_result.is_coherence_order_maximal_write)
     }
 
+    /// Inform GenMC about an atomic read-modify-write operation.
+    /// This includes atomic swap (also often called "exchange"), but does *not*
+    /// include compare-exchange (see `RMWBinOp` for full list of operations).
+    /// Returns the previous value at that memory location, and optionally the value that should be written back to Miri's memory.
+    fn handle_atomic_rmw_op<'tcx>(
+        &self,
+        ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
+        address: Size,
+        size: Size,
+        ordering: AtomicRwOrd,
+        genmc_rmw_op: RMWBinOp,
+        genmc_rhs_scalar: GenmcScalar,
+        genmc_old_value: GenmcScalar,
+    ) -> InterpResult<'tcx, (Scalar, Option<Scalar>)> {
+        assert!(
+            !self.get_alloc_data_races(),
+            "atomic read-modify-write operation with data race checking disabled."
+        );
+        assert_ne!(0, size.bytes());
+        assert!(
+            size.bytes() <= MAX_ACCESS_SIZE,
+            "GenMC currently does not support atomic accesses larger than {} bytes (got {} bytes)",
+            MAX_ACCESS_SIZE,
+            size.bytes()
+        );
+
+        let curr_thread_id = ecx.machine.threads.active_thread();
+        let genmc_tid = self.exec_state.thread_id_manager.borrow().get_genmc_tid(curr_thread_id);
+        debug!(
+            "GenMC: atomic_rmw_op, thread: {curr_thread_id:?} ({genmc_tid:?}) (op: {genmc_rmw_op:?}, rhs value: {genmc_rhs_scalar:?}), address: {address:?}, size: {size:?}, ordering: {ordering:?}",
+        );
+        let rmw_result = self.handle.borrow_mut().pin_mut().handle_read_modify_write(
+            genmc_tid,
+            address.bytes(),
+            size.bytes(),
+            genmc_rmw_op,
+            ordering.to_genmc(),
+            genmc_rhs_scalar,
+            genmc_old_value,
+        );
+
+        if let Some(error) = rmw_result.error.as_ref() {
+            // FIXME(genmc): error handling
+            throw_ub_format!("{}", error.to_string_lossy());
+        }
+
+        let old_value_scalar = genmc_scalar_to_scalar(ecx, rmw_result.old_value, size)?;
+
+        let new_value_scalar = if rmw_result.is_coherence_order_maximal_write {
+            Some(genmc_scalar_to_scalar(ecx, rmw_result.new_value, size)?)
+        } else {
+            None
+        };
+        interp_ok((old_value_scalar, new_value_scalar))
+    }
+
     /**** Blocking functionality ****/
 
     /// Handle a user thread getting blocked.
diff --git a/src/tools/miri/src/concurrency/genmc/run.rs b/src/tools/miri/src/concurrency/genmc/run.rs
index 62553297a20..24d13e6375b 100644
--- a/src/tools/miri/src/concurrency/genmc/run.rs
+++ b/src/tools/miri/src/concurrency/genmc/run.rs
@@ -18,6 +18,8 @@ pub fn run_genmc_mode<'tcx>(
     eval_entry: impl Fn(Rc<GenmcCtx>) -> Option<i32>,
     tcx: TyCtxt<'tcx>,
 ) -> Option<i32> {
+    let genmc_config = config.genmc_config.as_ref().unwrap();
+
     // There exists only one `global_state` per full run in GenMC mode.
     // It is shared by all `GenmcCtx` in this run.
     // FIXME(genmc): implement multithreading once GenMC supports it.
@@ -32,8 +34,15 @@ pub fn run_genmc_mode<'tcx>(
         genmc_ctx.prepare_next_execution();
 
         // Execute the program until completion to get the return value, or return if an error happens:
-        // FIXME(genmc): add an option to allow the user to see the GenMC output message when the verification is done.
-        let return_code = eval_entry(genmc_ctx.clone())?;
+        let Some(return_code) = eval_entry(genmc_ctx.clone()) else {
+            // If requested, print the output GenMC produced:
+            if genmc_config.print_genmc_output {
+                eprintln!("== raw GenMC output =========================");
+                eprintln!("{}", genmc_ctx.get_result_message());
+                eprintln!("== end of raw GenMC output ==================");
+            }
+            return None;
+        };
 
         // We inform GenMC that the execution is complete. If there was an error, we print it.
         if let Some(error) = genmc_ctx.handle_execution_end() {
diff --git a/src/tools/miri/tests/genmc/fail/loom/buggy_inc.rs b/src/tools/miri/tests/genmc/fail/loom/buggy_inc.rs
new file mode 100644
index 00000000000..508eae756f3
--- /dev/null
+++ b/src/tools/miri/tests/genmc/fail/loom/buggy_inc.rs
@@ -0,0 +1,66 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+// SPDX-License-Identifier: MIT
+// SPDX-FileCopyrightText: Copyright (c) 2019 Carl Lerche
+
+// This is the test `checks_fail` from loom/test/smoke.rs adapted for Miri-GenMC.
+// https://github.com/tokio-rs/loom/blob/dbf32b04bae821c64be44405a0bb72ca08741558/tests/smoke.rs
+
+// This test checks that an incorrect implementation of an incrementing counter is detected.
+// The counter behaves wrong if two threads try to increment at the same time (increments can be lost).
+
+#![no_main]
+
+#[cfg(not(any(non_genmc_std, genmc_std)))]
+#[path = "../../../utils/genmc.rs"]
+mod genmc;
+
+use std::sync::atomic::AtomicUsize;
+use std::sync::atomic::Ordering::*;
+
+use crate::genmc::*;
+
+struct BuggyInc {
+    num: AtomicUsize,
+}
+
+impl BuggyInc {
+    const fn new() -> BuggyInc {
+        BuggyInc { num: AtomicUsize::new(0) }
+    }
+
+    fn inc(&self) {
+        // The bug is here:
+        // Another thread can increment `self.num` between the next two lines,
+        // which is then overridden by this thread.
+        let curr = self.num.load(Acquire);
+        self.num.store(curr + 1, Release);
+    }
+}
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    unsafe {
+        static BUGGY_INC: BuggyInc = BuggyInc::new();
+        // FIXME(genmc,HACK): remove this initializing write once Miri-GenMC supports mixed atomic-non-atomic accesses.
+        BUGGY_INC.num.store(0, Relaxed);
+
+        let ids = [
+            spawn_pthread_closure(|| {
+                BUGGY_INC.inc();
+            }),
+            spawn_pthread_closure(|| {
+                BUGGY_INC.inc();
+            }),
+        ];
+        // Join so we can read the final values.
+        join_pthreads(ids);
+
+        // We check that we can detect the incorrect counter implementation:
+        if 2 != BUGGY_INC.num.load(Relaxed) {
+            std::process::abort(); //~ ERROR: abnormal termination
+        }
+
+        0
+    }
+}
diff --git a/src/tools/miri/tests/genmc/fail/loom/buggy_inc.stderr b/src/tools/miri/tests/genmc/fail/loom/buggy_inc.stderr
new file mode 100644
index 00000000000..5a8948ff9b4
--- /dev/null
+++ b/src/tools/miri/tests/genmc/fail/loom/buggy_inc.stderr
@@ -0,0 +1,13 @@
+error: abnormal termination: the program aborted execution
+  --> tests/genmc/fail/loom/buggy_inc.rs:LL:CC
+   |
+LL |             std::process::abort();
+   |             ^^^^^^^^^^^^^^^^^^^^^ abnormal termination occurred here
+   |
+   = note: BACKTRACE:
+   = note: inside `miri_start` at tests/genmc/fail/loom/buggy_inc.rs:LL:CC
+
+note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
+
+error: aborting due to 1 previous error
+
diff --git a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.relaxed4.stderr b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.relaxed4.stderr
index e2b114df652..cbfb6ec833e 100644
--- a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.relaxed4.stderr
+++ b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.relaxed4.stderr
@@ -1,11 +1,9 @@
-error: Undefined Behavior: entering unreachable code
+error: abnormal termination: the program aborted execution
   --> tests/genmc/fail/simple/2w2w_weak.rs:LL:CC
    |
-LL |             std::hint::unreachable_unchecked();
-   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Undefined Behavior occurred here
+LL |             std::process::abort();
+   |             ^^^^^^^^^^^^^^^^^^^^^ abnormal termination occurred here
    |
-   = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
-   = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
    = note: BACKTRACE:
    = note: inside `miri_start` at tests/genmc/fail/simple/2w2w_weak.rs:LL:CC
 
diff --git a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.release4.stderr b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.release4.stderr
index e2b114df652..cbfb6ec833e 100644
--- a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.release4.stderr
+++ b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.release4.stderr
@@ -1,11 +1,9 @@
-error: Undefined Behavior: entering unreachable code
+error: abnormal termination: the program aborted execution
   --> tests/genmc/fail/simple/2w2w_weak.rs:LL:CC
    |
-LL |             std::hint::unreachable_unchecked();
-   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Undefined Behavior occurred here
+LL |             std::process::abort();
+   |             ^^^^^^^^^^^^^^^^^^^^^ abnormal termination occurred here
    |
-   = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
-   = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
    = note: BACKTRACE:
    = note: inside `miri_start` at tests/genmc/fail/simple/2w2w_weak.rs:LL:CC
 
diff --git a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.rs b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.rs
index dea2b5f952e..baf3584966e 100644
--- a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.rs
+++ b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.rs
@@ -7,7 +7,7 @@
 // When using any combination of orderings except using all 4 `SeqCst`, the memory model allows the program to result in (X, Y) == (1, 1).
 // The "pass" variants only check that we get the expected number of executions (3 for all SC, 4 otherwise),
 // and a valid outcome every execution, but do not check that we get all allowed results.
-// This "fail" variant ensures we can explore the execution resulting in (1, 1), an incorrect unsafe assumption that the result (1, 1) is impossible.
+// This "fail" variant ensures we can explore the execution resulting in (1, 1), with an incorrect assumption that the result (1, 1) is impossible.
 //
 // Miri without GenMC is unable to produce this program execution and thus detect the incorrect assumption, even with `-Zmiri-many-seeds`.
 //
@@ -61,11 +61,10 @@ fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
         // Join so we can read the final values.
         join_pthreads(ids);
 
-        // We mark the result (1, 1) as unreachable, which is incorrect.
+        // We incorrectly assume that the result (1, 1) as unreachable.
         let result = (X.load(Relaxed), Y.load(Relaxed));
         if result == (1, 1) {
-            // FIXME(genmc): Use `std::process::abort()` once backtraces for that are improved (https://github.com/rust-lang/rust/pull/146118)
-            std::hint::unreachable_unchecked(); //~ ERROR: entering unreachable code
+            std::process::abort(); //~ ERROR: abnormal termination
         }
 
         0
diff --git a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.sc3_rel1.stderr b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.sc3_rel1.stderr
index e2b114df652..cbfb6ec833e 100644
--- a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.sc3_rel1.stderr
+++ b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.sc3_rel1.stderr
@@ -1,11 +1,9 @@
-error: Undefined Behavior: entering unreachable code
+error: abnormal termination: the program aborted execution
   --> tests/genmc/fail/simple/2w2w_weak.rs:LL:CC
    |
-LL |             std::hint::unreachable_unchecked();
-   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Undefined Behavior occurred here
+LL |             std::process::abort();
+   |             ^^^^^^^^^^^^^^^^^^^^^ abnormal termination occurred here
    |
-   = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
-   = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
    = note: BACKTRACE:
    = note: inside `miri_start` at tests/genmc/fail/simple/2w2w_weak.rs:LL:CC
 
diff --git a/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.rs b/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.rs
new file mode 100644
index 00000000000..f48466e8ce1
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.rs
@@ -0,0 +1,91 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+// This test check for correct handling of atomic read-modify-write operations for all integer sizes.
+// Atomic max and min should return the previous value, and store the result in the atomic.
+// Atomic addition and subtraction should have wrapping semantics.
+// `and`, `nand`, `or`, `xor` should behave like their non-atomic counterparts.
+
+// FIXME(genmc): add 128 bit atomics for platforms that support it, once GenMC gets 128 bit atomic support
+
+#![no_main]
+
+use std::sync::atomic::*;
+
+const ORD: Ordering = Ordering::SeqCst;
+
+fn assert_eq<T: Eq>(x: T, y: T) {
+    if x != y {
+        std::process::abort();
+    }
+}
+
+macro_rules! test_rmw_edge_cases {
+    ($int:ty, $atomic:ty) => {{
+        let x = <$atomic>::new(123);
+        // FIXME(genmc,HACK): remove this initializing write once Miri-GenMC supports mixed atomic-non-atomic accesses.
+        x.store(123, ORD);
+
+        // MAX, ADD
+        assert_eq(123, x.fetch_max(0, ORD)); // `max` keeps existing value
+        assert_eq(123, x.fetch_max(<$int>::MAX, ORD)); // `max` stores the new value
+        assert_eq(<$int>::MAX, x.fetch_add(10, ORD)); // `fetch_add` should be wrapping
+        assert_eq(<$int>::MAX.wrapping_add(10), x.load(ORD));
+
+        // MIN, SUB
+        x.store(42, ORD);
+        assert_eq(42, x.fetch_min(<$int>::MAX, ORD)); // `min` keeps existing value
+        assert_eq(42, x.fetch_min(<$int>::MIN, ORD)); // `min` stores the new value
+        assert_eq(<$int>::MIN, x.fetch_sub(10, ORD)); // `fetch_sub` should be wrapping
+        assert_eq(<$int>::MIN.wrapping_sub(10), x.load(ORD));
+
+        // Small enough pattern to work for all integer sizes.
+        let pattern = 0b01010101;
+
+        // AND
+        x.store(!0, ORD);
+        assert_eq(!0, x.fetch_and(pattern, ORD));
+        assert_eq(!0 & pattern, x.load(ORD));
+
+        // NAND
+        x.store(!0, ORD);
+        assert_eq(!0, x.fetch_nand(pattern, ORD));
+        assert_eq(!(!0 & pattern), x.load(ORD));
+
+        // OR
+        x.store(!0, ORD);
+        assert_eq(!0, x.fetch_or(pattern, ORD));
+        assert_eq(!0 | pattern, x.load(ORD));
+
+        // XOR
+        x.store(!0, ORD);
+        assert_eq(!0, x.fetch_xor(pattern, ORD));
+        assert_eq(!0 ^ pattern, x.load(ORD));
+
+        // SWAP
+        x.store(!0, ORD);
+        assert_eq(!0, x.swap(pattern, ORD));
+        assert_eq(pattern, x.load(ORD));
+
+        // Check correct behavior of atomic min/max combined with overflowing add/sub.
+        x.store(10, ORD);
+        assert_eq(10, x.fetch_add(<$int>::MAX, ORD)); // definitely overflows, so new value of x is smaller than 10
+        assert_eq(<$int>::MAX.wrapping_add(10), x.fetch_max(10, ORD)); // new value of x should be 10
+        // assert_eq(10, x.load(ORD)); // FIXME(genmc,#4572): enable this check once GenMC correctly handles min/max truncation.
+    }};
+}
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    test_rmw_edge_cases!(u8, AtomicU8);
+    test_rmw_edge_cases!(u16, AtomicU16);
+    test_rmw_edge_cases!(u32, AtomicU32);
+    test_rmw_edge_cases!(u64, AtomicU64);
+    test_rmw_edge_cases!(usize, AtomicUsize);
+    test_rmw_edge_cases!(i8, AtomicI8);
+    test_rmw_edge_cases!(i16, AtomicI16);
+    test_rmw_edge_cases!(i32, AtomicI32);
+    test_rmw_edge_cases!(i64, AtomicI64);
+    test_rmw_edge_cases!(isize, AtomicIsize);
+
+    0
+}
diff --git a/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.stderr b/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.stderr
new file mode 100644
index 00000000000..3b22247ee44
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.stderr
@@ -0,0 +1,2 @@
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 1
diff --git a/src/tools/miri/tests/genmc/pass/litmus/2w2w_2sc_scf.rs b/src/tools/miri/tests/genmc/pass/litmus/2w2w_2sc_scf.rs
new file mode 100644
index 00000000000..3b3fca02285
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/2w2w_2sc_scf.rs
@@ -0,0 +1,33 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+// Translated from GenMC's test "2+2W+2sc+scf".
+// It tests correct handling of SeqCst fences combined with relaxed accesses.
+
+#![no_main]
+
+#[path = "../../../utils/genmc.rs"]
+mod genmc;
+
+use std::sync::atomic::AtomicU64;
+use std::sync::atomic::Ordering::*;
+
+use crate::genmc::*;
+
+static X: AtomicU64 = AtomicU64::new(0);
+static Y: AtomicU64 = AtomicU64::new(0);
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    unsafe {
+        spawn_pthread_closure(|| {
+            X.store(1, SeqCst);
+            Y.store(2, SeqCst);
+        });
+        spawn_pthread_closure(|| {
+            Y.store(1, Relaxed);
+            std::sync::atomic::fence(SeqCst);
+            X.store(2, Relaxed);
+        });
+        0
+    }
+}
diff --git a/src/tools/miri/tests/genmc/pass/litmus/2w2w_2sc_scf.stderr b/src/tools/miri/tests/genmc/pass/litmus/2w2w_2sc_scf.stderr
new file mode 100644
index 00000000000..115b1986ce5
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/2w2w_2sc_scf.stderr
@@ -0,0 +1,2 @@
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 3
diff --git a/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.rs b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.rs
index bbe9995dea0..f47f5a11c5c 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.rs
+++ b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.rs
@@ -1,9 +1,13 @@
+//@revisions: weak sc
 //@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+//@[sc]compile-flags: -Zmiri-disable-weak-memory-emulation
 
 // Translated from GenMC's test "2+2W".
 //
 // The pass tests "2w2w_3sc_1rel.rs", "2w2w_4rel" and "2w2w_4sc" and the fail test "2w2w_weak.rs" are related.
 // Check "2w2w_weak.rs" for a more detailed description.
+//
+// The `sc` variant of this test checks that without weak memory emulation, only 3 instead of 4 executions are explored (like the `2w2w_4sc.rs` test).
 
 #![no_main]
 
diff --git a/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.sc.stderr b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.sc.stderr
new file mode 100644
index 00000000000..115b1986ce5
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.sc.stderr
@@ -0,0 +1,2 @@
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 3
diff --git a/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.stderr b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.stderr
deleted file mode 100644
index 0667962f99c..00000000000
--- a/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.stderr
+++ /dev/null
@@ -1,2 +0,0 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 4
diff --git a/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.weak.stderr b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.weak.stderr
new file mode 100644
index 00000000000..0667962f99c
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.weak.stderr
@@ -0,0 +1,2 @@
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 4
diff --git a/src/tools/miri/tests/genmc/pass/litmus/IRIW-acq-sc.rs b/src/tools/miri/tests/genmc/pass/litmus/IRIW-acq-sc.rs
index 79e7c7feb7a..1ec62ff2134 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/IRIW-acq-sc.rs
+++ b/src/tools/miri/tests/genmc/pass/litmus/IRIW-acq-sc.rs
@@ -1,6 +1,6 @@
 //@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
 
-// Translated from GenMC's "IRIW-acq-sc" test.
+// Translated from GenMC's "litmus/IRIW-acq-sc" test.
 
 #![no_main]
 
diff --git a/src/tools/miri/tests/genmc/pass/litmus/IRIWish.rs b/src/tools/miri/tests/genmc/pass/litmus/IRIWish.rs
new file mode 100644
index 00000000000..163556dcc89
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/IRIWish.rs
@@ -0,0 +1,66 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+// Translated from GenMC's "litmus/IRIWish" test.
+// This test prints the values read by the different threads to check that we get all the values we expect.
+
+// NOTE: the order of the lines in the output may change with changes to GenMC.
+// Before blessing the new output, ensure that only the order of lines in the output changed, and none of the outputs are missing.
+
+// NOTE: GenMC supports instruction caching and does not need replay completed threads.
+// This means that an identical test in GenMC may output fewer lines (disable instruction caching to see all results).
+
+#![no_main]
+
+#[path = "../../../utils/genmc.rs"]
+mod genmc;
+#[path = "../../../utils/mod.rs"]
+mod utils;
+
+use std::fmt::Write;
+use std::sync::atomic::AtomicU64;
+use std::sync::atomic::Ordering::*;
+
+use crate::genmc::*;
+use crate::utils::*;
+
+static X: AtomicU64 = AtomicU64::new(0);
+static Y: AtomicU64 = AtomicU64::new(0);
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    // FIXME(genmc,HACK): remove these initializing writes once Miri-GenMC supports mixed atomic-non-atomic accesses.
+    X.store(0, Relaxed);
+    Y.store(0, Relaxed);
+
+    unsafe {
+        let mut results = [1234; 5];
+        let ids = [
+            spawn_pthread_closure(|| {
+                X.store(1, Relaxed);
+            }),
+            spawn_pthread_closure(|| {
+                let r1 = X.load(Relaxed);
+                Y.store(r1, Release);
+                results[0] = r1;
+            }),
+            spawn_pthread_closure(|| {
+                results[1] = X.load(Relaxed);
+                std::sync::atomic::fence(AcqRel);
+                results[2] = Y.load(Relaxed);
+            }),
+            spawn_pthread_closure(|| {
+                results[3] = Y.load(Relaxed);
+                std::sync::atomic::fence(AcqRel);
+                results[4] = X.load(Relaxed);
+            }),
+        ];
+        join_pthreads(ids);
+
+        // Print the values to check that we get all of them:
+        if writeln!(MiriStderr, "{results:?}").is_err() {
+            std::process::abort();
+        }
+
+        0
+    }
+}
diff --git a/src/tools/miri/tests/genmc/pass/litmus/IRIWish.stderr b/src/tools/miri/tests/genmc/pass/litmus/IRIWish.stderr
new file mode 100644
index 00000000000..4fc77b63f38
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/IRIWish.stderr
@@ -0,0 +1,30 @@
+[1, 1, 1, 1, 1]
+[1, 1, 1, 0, 1]
+[1, 1, 1, 0, 0]
+[1, 1, 0, 1, 1]
+[1, 1, 0, 0, 1]
+[1, 1, 0, 0, 0]
+[1, 0, 1, 1, 1]
+[1, 0, 1, 0, 1]
+[1, 0, 1, 0, 0]
+[1, 0, 0, 1, 1]
+[1, 0, 0, 0, 1]
+[1, 0, 0, 0, 0]
+[0, 1, 0, 0, 1]
+[0, 1, 0, 0, 0]
+[0, 1, 0, 0, 1]
+[0, 1, 0, 0, 0]
+[0, 1, 0, 0, 1]
+[0, 1, 0, 0, 0]
+[0, 1, 0, 0, 1]
+[0, 1, 0, 0, 0]
+[0, 0, 0, 0, 1]
+[0, 0, 0, 0, 0]
+[0, 0, 0, 0, 1]
+[0, 0, 0, 0, 0]
+[0, 0, 0, 0, 1]
+[0, 0, 0, 0, 0]
+[0, 0, 0, 0, 1]
+[0, 0, 0, 0, 0]
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 28
diff --git a/src/tools/miri/tests/genmc/pass/litmus/LB_incMPs.rs b/src/tools/miri/tests/genmc/pass/litmus/LB_incMPs.rs
new file mode 100644
index 00000000000..e43d92fc6c5
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/LB_incMPs.rs
@@ -0,0 +1,41 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+// Translated from GenMC's "litmus/LB+incMPs" test.
+
+#![no_main]
+
+#[path = "../../../utils/genmc.rs"]
+mod genmc;
+
+use std::sync::atomic::AtomicU64;
+use std::sync::atomic::Ordering::*;
+
+use crate::genmc::*;
+
+static X: AtomicU64 = AtomicU64::new(0);
+static Y: AtomicU64 = AtomicU64::new(0);
+static W: AtomicU64 = AtomicU64::new(0);
+static Z: AtomicU64 = AtomicU64::new(0);
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    unsafe {
+        spawn_pthread_closure(|| {
+            X.load(Acquire);
+            Z.fetch_add(1, AcqRel);
+        });
+        spawn_pthread_closure(|| {
+            Z.fetch_add(1, AcqRel);
+            Y.store(1, Release);
+        });
+        spawn_pthread_closure(|| {
+            Y.load(Acquire);
+            W.fetch_add(1, AcqRel);
+        });
+        spawn_pthread_closure(|| {
+            W.fetch_add(1, AcqRel);
+            X.store(1, Release);
+        });
+        0
+    }
+}
diff --git a/src/tools/miri/tests/genmc/pass/litmus/LB_incMPs.stderr b/src/tools/miri/tests/genmc/pass/litmus/LB_incMPs.stderr
new file mode 100644
index 00000000000..c879e95a170
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/LB_incMPs.stderr
@@ -0,0 +1,2 @@
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 15
diff --git a/src/tools/miri/tests/genmc/pass/litmus/MPU_rels_acq.rs b/src/tools/miri/tests/genmc/pass/litmus/MPU_rels_acq.rs
new file mode 100644
index 00000000000..b36c8a288f4
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/MPU_rels_acq.rs
@@ -0,0 +1,42 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+// Translated from GenMC's "litmus/MPU+rels+acq" test.
+
+#![no_main]
+
+#[path = "../../../utils/genmc.rs"]
+mod genmc;
+
+use std::sync::atomic::AtomicU64;
+use std::sync::atomic::Ordering::*;
+
+// Note: the GenMC equivalent of this test (genmc/tests/correct/litmus/MPU+rels+acq/mpu+rels+acq.c) uses non-atomic accesses for `X` with disabled race detection.
+static X: AtomicU64 = AtomicU64::new(0);
+static Y: AtomicU64 = AtomicU64::new(0);
+
+use crate::genmc::*;
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    // FIXME(genmc,HACK): remove these initializing writes once Miri-GenMC supports mixed atomic-non-atomic accesses.
+    X.store(0, Relaxed);
+    Y.store(0, Relaxed);
+
+    unsafe {
+        spawn_pthread_closure(|| {
+            X.store(1, Relaxed);
+
+            Y.store(0, Release);
+            Y.store(1, Relaxed);
+        });
+        spawn_pthread_closure(|| {
+            Y.fetch_add(1, Relaxed);
+        });
+        spawn_pthread_closure(|| {
+            if Y.load(Acquire) > 1 {
+                X.store(2, Relaxed);
+            }
+        });
+        0
+    }
+}
diff --git a/src/tools/miri/tests/genmc/pass/litmus/MPU_rels_acq.stderr b/src/tools/miri/tests/genmc/pass/litmus/MPU_rels_acq.stderr
new file mode 100644
index 00000000000..c5e34b00642
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/MPU_rels_acq.stderr
@@ -0,0 +1,2 @@
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 13
diff --git a/src/tools/miri/tests/genmc/pass/litmus/MP_incMPs.rs b/src/tools/miri/tests/genmc/pass/litmus/MP_incMPs.rs
new file mode 100644
index 00000000000..a08b7de27d1
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/MP_incMPs.rs
@@ -0,0 +1,36 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+// Translated from GenMC's "litmus/MP+incMP" test.
+
+#![no_main]
+
+#[path = "../../../utils/genmc.rs"]
+mod genmc;
+
+use std::sync::atomic::AtomicU64;
+use std::sync::atomic::Ordering::*;
+
+use crate::genmc::*;
+
+static X: AtomicU64 = AtomicU64::new(0);
+static Y: AtomicU64 = AtomicU64::new(0);
+static Z: AtomicU64 = AtomicU64::new(0);
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    unsafe {
+        spawn_pthread_closure(|| {
+            Y.load(Acquire);
+            Z.fetch_add(1, AcqRel);
+        });
+        spawn_pthread_closure(|| {
+            Z.fetch_add(1, AcqRel);
+            X.load(Acquire);
+        });
+        spawn_pthread_closure(|| {
+            X.store(1, Release);
+            Y.store(1, Release);
+        });
+        0
+    }
+}
diff --git a/src/tools/miri/tests/genmc/pass/litmus/MP_incMPs.stderr b/src/tools/miri/tests/genmc/pass/litmus/MP_incMPs.stderr
new file mode 100644
index 00000000000..2be9a6c7fbd
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/MP_incMPs.stderr
@@ -0,0 +1,2 @@
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 7
diff --git a/src/tools/miri/tests/genmc/pass/litmus/MP_rels_acqf.rs b/src/tools/miri/tests/genmc/pass/litmus/MP_rels_acqf.rs
new file mode 100644
index 00000000000..cf9f5f2dbfa
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/MP_rels_acqf.rs
@@ -0,0 +1,40 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+// Translated from GenMC's "litmus/MP+rels+acqf" test.
+
+#![no_main]
+
+#[path = "../../../utils/genmc.rs"]
+mod genmc;
+
+use std::sync::atomic::AtomicU64;
+use std::sync::atomic::Ordering::*;
+
+// Note: the GenMC equivalent of this test (genmc/tests/correct/litmus/MP+rels+acqf/mp+rels+acqf.c) uses non-atomic accesses for `X` with disabled race detection.
+static X: AtomicU64 = AtomicU64::new(0);
+static Y: AtomicU64 = AtomicU64::new(0);
+
+use crate::genmc::*;
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    // FIXME(genmc,HACK): remove these initializing writes once Miri-GenMC supports mixed atomic-non-atomic accesses.
+    X.store(0, Relaxed);
+    Y.store(0, Relaxed);
+
+    unsafe {
+        spawn_pthread_closure(|| {
+            X.store(1, Relaxed);
+
+            Y.store(0, Release);
+            Y.store(1, Relaxed);
+        });
+        spawn_pthread_closure(|| {
+            if Y.load(Relaxed) != 0 {
+                std::sync::atomic::fence(Acquire);
+                let _x = X.load(Relaxed);
+            }
+        });
+        0
+    }
+}
diff --git a/src/tools/miri/tests/genmc/pass/litmus/MP_rels_acqf.stderr b/src/tools/miri/tests/genmc/pass/litmus/MP_rels_acqf.stderr
new file mode 100644
index 00000000000..0667962f99c
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/MP_rels_acqf.stderr
@@ -0,0 +1,2 @@
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 4
diff --git a/src/tools/miri/tests/genmc/pass/litmus/SB_2sc_scf.rs b/src/tools/miri/tests/genmc/pass/litmus/SB_2sc_scf.rs
new file mode 100644
index 00000000000..ffc44de1bc7
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/SB_2sc_scf.rs
@@ -0,0 +1,32 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+// Translated from GenMC's "litmus/SB+2sc+scf" test.
+
+#![no_main]
+
+#[path = "../../../utils/genmc.rs"]
+mod genmc;
+
+use std::sync::atomic::AtomicU64;
+use std::sync::atomic::Ordering::*;
+
+use crate::genmc::*;
+
+static X: AtomicU64 = AtomicU64::new(0);
+static Y: AtomicU64 = AtomicU64::new(0);
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    unsafe {
+        spawn_pthread_closure(|| {
+            X.store(1, SeqCst);
+            Y.load(SeqCst);
+        });
+        spawn_pthread_closure(|| {
+            Y.store(1, Relaxed);
+            std::sync::atomic::fence(SeqCst);
+            X.load(Relaxed);
+        });
+        0
+    }
+}
diff --git a/src/tools/miri/tests/genmc/pass/litmus/SB_2sc_scf.stderr b/src/tools/miri/tests/genmc/pass/litmus/SB_2sc_scf.stderr
new file mode 100644
index 00000000000..115b1986ce5
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/SB_2sc_scf.stderr
@@ -0,0 +1,2 @@
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 3
diff --git a/src/tools/miri/tests/genmc/pass/litmus/Z6_U.rs b/src/tools/miri/tests/genmc/pass/litmus/Z6_U.rs
new file mode 100644
index 00000000000..ac5c3724254
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/Z6_U.rs
@@ -0,0 +1,65 @@
+//@revisions: weak sc
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+//@[sc]compile-flags: -Zmiri-disable-weak-memory-emulation
+
+// Translated from GenMC's "litmus/Z6.U" test.
+//
+// The `sc` variant of this test checks that we get fewer executions when weak memory emulation is disabled.
+
+// NOTE: the order of the lines in the output may change with changes to GenMC.
+// Before blessing the new output, ensure that only the order of lines in the output changed, and none of the outputs are missing.
+
+// NOTE: GenMC supports instruction caching and does not need replay completed threads.
+// This means that an identical test in GenMC may output fewer lines (disable instruction caching to see all results).
+
+#![no_main]
+
+#[path = "../../../utils/genmc.rs"]
+mod genmc;
+#[path = "../../../utils/mod.rs"]
+mod utils;
+
+use std::fmt::Write;
+use std::sync::atomic::AtomicU64;
+use std::sync::atomic::Ordering::*;
+
+use crate::genmc::*;
+use crate::utils::*;
+
+static X: AtomicU64 = AtomicU64::new(0);
+static Y: AtomicU64 = AtomicU64::new(0);
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    // FIXME(genmc,HACK): remove these initializing writes once Miri-GenMC supports mixed atomic-non-atomic accesses.
+    X.store(0, Relaxed);
+    Y.store(0, Relaxed);
+
+    unsafe {
+        let mut a = 1234;
+        let mut b = 1234;
+        let ids = [
+            spawn_pthread_closure(|| {
+                X.store(1, SeqCst);
+                Y.store(1, Release);
+            }),
+            spawn_pthread_closure(|| {
+                Y.fetch_add(1, SeqCst);
+                a = Y.load(Relaxed);
+            }),
+            spawn_pthread_closure(|| {
+                Y.store(3, SeqCst);
+                b = X.load(SeqCst);
+            }),
+        ];
+        join_pthreads(ids);
+
+        // Print the values to check that we get all of them:
+        if writeln!(MiriStderr, "a={a}, b={b}, X={}, Y={}", X.load(Relaxed), Y.load(Relaxed))
+            .is_err()
+        {
+            std::process::abort();
+        }
+        0
+    }
+}
diff --git a/src/tools/miri/tests/genmc/pass/litmus/Z6_U.sc.stderr b/src/tools/miri/tests/genmc/pass/litmus/Z6_U.sc.stderr
new file mode 100644
index 00000000000..8dd2fbe1b97
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/Z6_U.sc.stderr
@@ -0,0 +1,20 @@
+a=2, b=1, X=1, Y=3
+a=4, b=1, X=1, Y=4
+a=3, b=1, X=1, Y=3
+a=2, b=1, X=1, Y=2
+a=2, b=0, X=1, Y=2
+a=1, b=1, X=1, Y=1
+a=1, b=0, X=1, Y=1
+a=4, b=1, X=1, Y=1
+a=4, b=0, X=1, Y=1
+a=1, b=1, X=1, Y=3
+a=3, b=1, X=1, Y=3
+a=1, b=1, X=1, Y=1
+a=1, b=0, X=1, Y=1
+a=3, b=1, X=1, Y=1
+a=3, b=0, X=1, Y=1
+a=1, b=1, X=1, Y=3
+a=1, b=1, X=1, Y=1
+a=1, b=0, X=1, Y=1
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 18
diff --git a/src/tools/miri/tests/genmc/pass/litmus/Z6_U.weak.stderr b/src/tools/miri/tests/genmc/pass/litmus/Z6_U.weak.stderr
new file mode 100644
index 00000000000..65622575de2
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/Z6_U.weak.stderr
@@ -0,0 +1,24 @@
+a=2, b=1, X=1, Y=3
+a=4, b=1, X=1, Y=4
+a=4, b=0, X=1, Y=4
+a=3, b=1, X=1, Y=3
+a=2, b=1, X=1, Y=2
+a=2, b=0, X=1, Y=2
+a=1, b=1, X=1, Y=1
+a=1, b=0, X=1, Y=1
+a=4, b=1, X=1, Y=1
+a=4, b=0, X=1, Y=1
+a=1, b=1, X=1, Y=3
+a=1, b=0, X=1, Y=3
+a=3, b=1, X=1, Y=3
+a=3, b=0, X=1, Y=3
+a=1, b=1, X=1, Y=1
+a=1, b=0, X=1, Y=1
+a=3, b=1, X=1, Y=1
+a=3, b=0, X=1, Y=1
+a=1, b=1, X=1, Y=3
+a=1, b=0, X=1, Y=3
+a=1, b=1, X=1, Y=1
+a=1, b=0, X=1, Y=1
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 22
diff --git a/src/tools/miri/tests/genmc/pass/litmus/Z6_acq.rs b/src/tools/miri/tests/genmc/pass/litmus/Z6_acq.rs
new file mode 100644
index 00000000000..b00f3a59ce6
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/Z6_acq.rs
@@ -0,0 +1,38 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+// Translated from GenMC's "litmus/Z6+acq" test.
+
+#![no_main]
+
+#[path = "../../../utils/genmc.rs"]
+mod genmc;
+
+use std::sync::atomic::AtomicU64;
+use std::sync::atomic::Ordering::*;
+
+use crate::genmc::*;
+
+static X: AtomicU64 = AtomicU64::new(0);
+static Y: AtomicU64 = AtomicU64::new(0);
+static Z: AtomicU64 = AtomicU64::new(0);
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    unsafe {
+        spawn_pthread_closure(|| {
+            X.store(1, Relaxed);
+            std::sync::atomic::fence(SeqCst);
+            Y.store(1, Relaxed);
+        });
+        spawn_pthread_closure(|| {
+            Y.load(Acquire);
+            Z.store(1, Relaxed);
+        });
+        spawn_pthread_closure(|| {
+            Z.store(2, Relaxed);
+            std::sync::atomic::fence(SeqCst);
+            X.load(Relaxed);
+        });
+        0
+    }
+}
diff --git a/src/tools/miri/tests/genmc/pass/litmus/Z6_acq.stderr b/src/tools/miri/tests/genmc/pass/litmus/Z6_acq.stderr
new file mode 100644
index 00000000000..2be9a6c7fbd
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/Z6_acq.stderr
@@ -0,0 +1,2 @@
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 7
diff --git a/src/tools/miri/tests/genmc/pass/litmus/atomicpo.rs b/src/tools/miri/tests/genmc/pass/litmus/atomicpo.rs
new file mode 100644
index 00000000000..75be89893da
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/atomicpo.rs
@@ -0,0 +1,32 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+// Translated from GenMC's test "litmus/atomicpo".
+
+#![no_main]
+
+#[path = "../../../utils/genmc.rs"]
+mod genmc;
+
+use std::sync::atomic::AtomicU64;
+use std::sync::atomic::Ordering::*;
+
+use crate::genmc::*;
+
+static X: AtomicU64 = AtomicU64::new(0);
+static Y: AtomicU64 = AtomicU64::new(0);
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    unsafe {
+        spawn_pthread_closure(|| {
+            X.store(1, Relaxed);
+            std::sync::atomic::fence(AcqRel);
+            Y.store(1, Relaxed);
+        });
+        spawn_pthread_closure(|| {
+            Y.swap(1, Relaxed);
+            X.swap(1, Relaxed);
+        });
+        0
+    }
+}
diff --git a/src/tools/miri/tests/genmc/pass/litmus/atomicpo.stderr b/src/tools/miri/tests/genmc/pass/litmus/atomicpo.stderr
new file mode 100644
index 00000000000..0667962f99c
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/atomicpo.stderr
@@ -0,0 +1,2 @@
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 4
diff --git a/src/tools/miri/tests/genmc/pass/litmus/cumul-release.rs b/src/tools/miri/tests/genmc/pass/litmus/cumul-release.rs
new file mode 100644
index 00000000000..2387976a8ca
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/cumul-release.rs
@@ -0,0 +1,58 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+// Translated from GenMC's test "litmus/cumul-release".
+
+#![no_main]
+
+#[path = "../../../utils/genmc.rs"]
+mod genmc;
+
+use std::sync::atomic::AtomicU64;
+use std::sync::atomic::Ordering::*;
+
+use crate::genmc::*;
+
+static X: AtomicU64 = AtomicU64::new(0);
+static Y: AtomicU64 = AtomicU64::new(0);
+static Z: AtomicU64 = AtomicU64::new(0);
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    // FIXME(genmc,HACK): remove these initializing writes once Miri-GenMC supports mixed atomic-non-atomic accesses.
+    X.store(0, Relaxed);
+    Y.store(0, Relaxed);
+    Z.store(0, Relaxed);
+
+    unsafe {
+        let mut a = 1234;
+        let mut b = 1234;
+        let mut c = 1234;
+        let ids = [
+            spawn_pthread_closure(|| {
+                X.store(1, Relaxed);
+                Y.store(1, Release);
+            }),
+            spawn_pthread_closure(|| {
+                a = Y.load(Relaxed);
+                Z.store(a, Relaxed);
+            }),
+            spawn_pthread_closure(|| {
+                b = Z.load(Relaxed);
+                std::sync::atomic::fence(AcqRel);
+                c = X.load(Relaxed);
+            }),
+        ];
+        // Join so we can read the final values.
+        join_pthreads(ids);
+
+        // Check that we don't get any unexpected values:
+        if !matches!(
+            (a, b, c),
+            (0, 0, 0) | (0, 0, 1) | (1, 0, 0) | (1, 0, 1) | (1, 1, 0) | (1, 1, 1)
+        ) {
+            std::process::abort();
+        }
+
+        0
+    }
+}
diff --git a/src/tools/miri/tests/genmc/pass/litmus/cumul-release.stderr b/src/tools/miri/tests/genmc/pass/litmus/cumul-release.stderr
new file mode 100644
index 00000000000..00394048ec5
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/cumul-release.stderr
@@ -0,0 +1,2 @@
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 8
diff --git a/src/tools/miri/tests/genmc/pass/litmus/fr_w_w_w_reads.rs b/src/tools/miri/tests/genmc/pass/litmus/fr_w_w_w_reads.rs
index 9a08d517b7c..796ffbf97f9 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/fr_w_w_w_reads.rs
+++ b/src/tools/miri/tests/genmc/pass/litmus/fr_w_w_w_reads.rs
@@ -38,7 +38,6 @@ fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
                 result[3] = X.load(Relaxed);
             }),
         ];
-
         // Join so we can read the final values.
         join_pthreads(ids);
 
diff --git a/src/tools/miri/tests/genmc/pass/litmus/inc2w.rs b/src/tools/miri/tests/genmc/pass/litmus/inc2w.rs
new file mode 100644
index 00000000000..fd8574c4f7c
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/inc2w.rs
@@ -0,0 +1,45 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+// Translated from GenMC's test "litmus/inc2w".
+
+#![no_main]
+
+#[path = "../../../utils/genmc.rs"]
+mod genmc;
+
+use std::sync::atomic::AtomicU64;
+use std::sync::atomic::Ordering::*;
+
+use crate::genmc::*;
+
+static X: AtomicU64 = AtomicU64::new(0);
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    // FIXME(genmc,HACK): remove this initializing write once Miri-GenMC supports mixed atomic-non-atomic accesses.
+    X.store(0, Relaxed);
+
+    unsafe {
+        let ids = [
+            spawn_pthread_closure(|| {
+                X.fetch_add(1, Relaxed);
+            }),
+            spawn_pthread_closure(|| {
+                X.store(4, Release);
+            }),
+            spawn_pthread_closure(|| {
+                X.fetch_add(2, Relaxed);
+            }),
+        ];
+        // Join so we can read the final values.
+        join_pthreads(ids);
+
+        // Check that we don't get any unexpected values:
+        let x = X.load(Relaxed);
+        if !matches!(x, 4..=7) {
+            std::process::abort();
+        }
+
+        0
+    }
+}
diff --git a/src/tools/miri/tests/genmc/pass/litmus/inc2w.stderr b/src/tools/miri/tests/genmc/pass/litmus/inc2w.stderr
new file mode 100644
index 00000000000..be75e68fde7
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/inc2w.stderr
@@ -0,0 +1,2 @@
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 6
diff --git a/src/tools/miri/tests/genmc/pass/litmus/inc_inc_RR_W_RR.rs b/src/tools/miri/tests/genmc/pass/litmus/inc_inc_RR_W_RR.rs
new file mode 100644
index 00000000000..40ca4863185
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/inc_inc_RR_W_RR.rs
@@ -0,0 +1,63 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+#![no_main]
+
+#[path = "../../../utils/genmc.rs"]
+mod genmc;
+
+use std::ffi::c_void;
+use std::sync::atomic::AtomicU64;
+use std::sync::atomic::Ordering::*;
+
+use crate::genmc::*;
+
+static X: AtomicU64 = AtomicU64::new(0);
+
+static mut A: u64 = 0;
+static mut B: u64 = 0;
+static mut C: u64 = 0;
+static mut D: u64 = 0;
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    let thread_order = [thread_1, thread_2, thread_3, thread_4, thread_5];
+    let ids = unsafe { spawn_pthreads_no_params(thread_order) };
+    unsafe { join_pthreads(ids) };
+
+    if unsafe { A == 42 && B == 2 && C == 1 && D == 42 } {
+        std::process::abort();
+    }
+
+    0
+}
+
+pub extern "C" fn thread_1(_value: *mut c_void) -> *mut c_void {
+    X.fetch_add(1, Relaxed);
+    std::ptr::null_mut()
+}
+
+pub extern "C" fn thread_2(_value: *mut c_void) -> *mut c_void {
+    X.fetch_add(1, Relaxed);
+    std::ptr::null_mut()
+}
+
+pub extern "C" fn thread_3(_value: *mut c_void) -> *mut c_void {
+    unsafe {
+        A = X.load(Relaxed);
+        B = X.load(Relaxed);
+    }
+    std::ptr::null_mut()
+}
+
+pub extern "C" fn thread_4(_value: *mut c_void) -> *mut c_void {
+    X.store(42, Relaxed);
+    std::ptr::null_mut()
+}
+
+pub extern "C" fn thread_5(_value: *mut c_void) -> *mut c_void {
+    unsafe {
+        C = X.load(Relaxed);
+        D = X.load(Relaxed);
+    }
+    std::ptr::null_mut()
+}
diff --git a/src/tools/miri/tests/genmc/pass/litmus/inc_inc_RR_W_RR.stderr b/src/tools/miri/tests/genmc/pass/litmus/inc_inc_RR_W_RR.stderr
new file mode 100644
index 00000000000..b5f8cd15b68
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/inc_inc_RR_W_RR.stderr
@@ -0,0 +1,2 @@
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 600
diff --git a/src/tools/miri/tests/genmc/pass/litmus/riwi.rs b/src/tools/miri/tests/genmc/pass/litmus/riwi.rs
new file mode 100644
index 00000000000..49564c8e4fe
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/riwi.rs
@@ -0,0 +1,31 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+// Translated from GenMC's "litmus/riwi" test.
+
+#![no_main]
+
+#[path = "../../../utils/genmc.rs"]
+mod genmc;
+
+use std::sync::atomic::AtomicU64;
+use std::sync::atomic::Ordering::*;
+
+use crate::genmc::*;
+
+static X: AtomicU64 = AtomicU64::new(0);
+static Y: AtomicU64 = AtomicU64::new(0);
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    unsafe {
+        spawn_pthread_closure(|| {
+            Y.load(Relaxed);
+            X.fetch_add(1, Relaxed);
+        });
+        spawn_pthread_closure(|| {
+            X.fetch_add(1, Relaxed);
+            Y.store(1, Release);
+        });
+        0
+    }
+}
diff --git a/src/tools/miri/tests/genmc/pass/litmus/riwi.stderr b/src/tools/miri/tests/genmc/pass/litmus/riwi.stderr
new file mode 100644
index 00000000000..115b1986ce5
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/riwi.stderr
@@ -0,0 +1,2 @@
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 3
diff --git a/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.rs b/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.rs
new file mode 100644
index 00000000000..a193dcf0683
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.rs
@@ -0,0 +1,36 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+// Translated from GenMC's "litmus/viktor-relseq" test.
+
+#![no_main]
+
+#[path = "../../../utils/genmc.rs"]
+mod genmc;
+
+use std::sync::atomic::AtomicU64;
+use std::sync::atomic::Ordering::*;
+
+use crate::genmc::*;
+
+static LOCK: AtomicU64 = AtomicU64::new(0);
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    unsafe {
+        spawn_pthread_closure(|| {
+            LOCK.fetch_add(1, Acquire);
+            LOCK.fetch_add(1, Relaxed);
+        });
+        spawn_pthread_closure(|| {
+            LOCK.fetch_add(1, Relaxed);
+            LOCK.fetch_add(1, Relaxed);
+        });
+        spawn_pthread_closure(|| {
+            LOCK.fetch_add(1, Release);
+        });
+        spawn_pthread_closure(|| {
+            LOCK.fetch_add(1, Relaxed);
+        });
+        0
+    }
+}
diff --git a/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.stderr b/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.stderr
new file mode 100644
index 00000000000..d63ac5199d5
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.stderr
@@ -0,0 +1,2 @@
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 180
diff --git a/src/tools/miri/tests/utils/genmc.rs b/src/tools/miri/tests/utils/genmc.rs
index fb6334bd060..29b3181992b 100644
--- a/src/tools/miri/tests/utils/genmc.rs
+++ b/src/tools/miri/tests/utils/genmc.rs
@@ -51,6 +51,13 @@ pub unsafe fn join_pthread(thread_id: pthread_t) {
     }
 }
 
+/// Spawn `N` threads using `pthread_create` without any arguments, abort the process on any errors.
+pub unsafe fn spawn_pthreads_no_params<const N: usize>(
+    functions: [extern "C" fn(*mut c_void) -> *mut c_void; N],
+) -> [pthread_t; N] {
+    functions.map(|func| spawn_pthread(func, std::ptr::null_mut()))
+}
+
 // Join the `N` given pthreads, abort the process on any errors.
 pub unsafe fn join_pthreads<const N: usize>(thread_ids: [pthread_t; N]) {
     let _ = thread_ids.map(|id| join_pthread(id));
-- 
cgit 1.4.1-3-g733a5


From a70d78a55286a85cf5e06958929f5a6071fa1c67 Mon Sep 17 00:00:00 2001
From: Patrick-6 <pamu99@gmx.ch>
Date: Fri, 14 Mar 2025 09:58:46 +0100
Subject: Implement more features for GenMC mode - 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

---
 .../miri/genmc-sys/cpp/include/MiriInterface.hpp   |  82 +++++++++++-----
 .../cpp/src/MiriInterface/EventHandling.cpp        |  65 ++++++++++++
 .../miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp |   8 +-
 src/tools/miri/genmc-sys/src/lib.rs                |  25 +++++
 src/tools/miri/src/concurrency/genmc/helper.rs     |  82 +++++++++++++++-
 src/tools/miri/src/concurrency/genmc/mod.rs        | 109 ++++++++++++++++++---
 src/tools/miri/src/concurrency/genmc/run.rs        |   4 +-
 src/tools/miri/src/diagnostics.rs                  |  26 +++++
 .../tests/genmc/fail/data_race/mpu2_rels_rlx.rs    |  45 +++++++++
 .../genmc/fail/data_race/mpu2_rels_rlx.stderr      |  19 ++++
 .../genmc/fail/loom/store_buffering.genmc.stderr   |  13 +++
 .../fail/loom/store_buffering.non_genmc.stderr     |  13 +++
 .../miri/tests/genmc/fail/loom/store_buffering.rs  |  57 +++++++++++
 .../pass/atomics/cas_failure_ord_racy_key_init.rs  |  70 +++++++++++++
 .../atomics/cas_failure_ord_racy_key_init.stderr   |  22 +++++
 .../miri/tests/genmc/pass/atomics/cas_simple.rs    |  34 +++++++
 .../tests/genmc/pass/atomics/cas_simple.stderr     |   2 +
 src/tools/miri/tests/genmc/pass/litmus/IRIWish.rs  |   4 +-
 .../miri/tests/genmc/pass/litmus/MPU2_rels_acqf.rs |  67 +++++++++++++
 .../tests/genmc/pass/litmus/MPU2_rels_acqf.stderr  |  38 +++++++
 src/tools/miri/tests/genmc/pass/litmus/Z6_U.rs     |   7 +-
 src/tools/miri/tests/genmc/pass/litmus/casdep.rs   |  37 +++++++
 .../miri/tests/genmc/pass/litmus/casdep.stderr     |   2 +
 src/tools/miri/tests/genmc/pass/litmus/ccr.rs      |  34 +++++++
 src/tools/miri/tests/genmc/pass/litmus/ccr.stderr  |   2 +
 src/tools/miri/tests/genmc/pass/litmus/cii.rs      |  35 +++++++
 src/tools/miri/tests/genmc/pass/litmus/cii.stderr  |   2 +
 27 files changed, 850 insertions(+), 54 deletions(-)
 create mode 100644 src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.rs
 create mode 100644 src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.stderr
 create mode 100644 src/tools/miri/tests/genmc/fail/loom/store_buffering.genmc.stderr
 create mode 100644 src/tools/miri/tests/genmc/fail/loom/store_buffering.non_genmc.stderr
 create mode 100644 src/tools/miri/tests/genmc/fail/loom/store_buffering.rs
 create mode 100644 src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.rs
 create mode 100644 src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.stderr
 create mode 100644 src/tools/miri/tests/genmc/pass/atomics/cas_simple.rs
 create mode 100644 src/tools/miri/tests/genmc/pass/atomics/cas_simple.stderr
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.rs
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.stderr
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/casdep.rs
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/casdep.stderr
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/ccr.rs
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/ccr.stderr
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/cii.rs
 create mode 100644 src/tools/miri/tests/genmc/pass/litmus/cii.stderr

(limited to 'src/tools/miri/genmc-sys/cpp/include')

diff --git a/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp b/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp
index b0769375843..662eb0e173c 100644
--- a/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp
+++ b/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp
@@ -34,6 +34,7 @@ struct SchedulingResult;
 struct LoadResult;
 struct StoreResult;
 struct ReadModifyWriteResult;
+struct CompareExchangeResult;
 
 // GenMC uses `int` for its thread IDs.
 using ThreadId = int;
@@ -100,6 +101,17 @@ struct MiriGenmcShim : private GenMCDriver {
         GenmcScalar rhs_value,
         GenmcScalar old_val
     );
+    [[nodiscard]] CompareExchangeResult handle_compare_exchange(
+        ThreadId thread_id,
+        uint64_t address,
+        uint64_t size,
+        GenmcScalar expected_value,
+        GenmcScalar new_value,
+        GenmcScalar old_val,
+        MemOrdering success_ordering,
+        MemOrdering fail_load_ordering,
+        bool can_fail_spuriously
+    );
     [[nodiscard]] StoreResult handle_store(
         ThreadId thread_id,
         uint64_t address,
@@ -231,15 +243,15 @@ constexpr auto get_global_alloc_static_mask() -> uint64_t {
 namespace GenmcScalarExt {
 inline GenmcScalar uninit() {
     return GenmcScalar {
-        /* value: */ 0,
-        /* is_init: */ false,
+        .value = 0,
+        .is_init = false,
     };
 }
 
 inline GenmcScalar from_sval(SVal sval) {
     return GenmcScalar {
-        /* value: */ sval.get(),
-        /* is_init: */ true,
+        .value = sval.get(),
+        .is_init = true,
     };
 }
 
@@ -252,22 +264,22 @@ inline SVal to_sval(GenmcScalar scalar) {
 namespace LoadResultExt {
 inline LoadResult no_value() {
     return LoadResult {
-        /* error: */ std::unique_ptr<std::string>(nullptr),
-        /* has_value: */ false,
-        /* read_value: */ GenmcScalarExt::uninit(),
+        .error = std::unique_ptr<std::string>(nullptr),
+        .has_value = false,
+        .read_value = GenmcScalarExt::uninit(),
     };
 }
 
 inline LoadResult from_value(SVal read_value) {
-    return LoadResult { /* error: */ std::unique_ptr<std::string>(nullptr),
-                        /* has_value: */ true,
-                        /* read_value: */ GenmcScalarExt::from_sval(read_value) };
+    return LoadResult { .error = std::unique_ptr<std::string>(nullptr),
+                        .has_value = true,
+                        .read_value = GenmcScalarExt::from_sval(read_value) };
 }
 
 inline LoadResult from_error(std::unique_ptr<std::string> error) {
-    return LoadResult { /* error: */ std::move(error),
-                        /* has_value: */ false,
-                        /* read_value: */ GenmcScalarExt::uninit() };
+    return LoadResult { .error = std::move(error),
+                        .has_value = false,
+                        .read_value = GenmcScalarExt::uninit() };
 }
 } // namespace LoadResultExt
 
@@ -278,26 +290,50 @@ inline StoreResult ok(bool is_coherence_order_maximal_write) {
 }
 
 inline StoreResult from_error(std::unique_ptr<std::string> error) {
-    return StoreResult { /* error: */ std::move(error),
-                         /* is_coherence_order_maximal_write: */ false };
+    return StoreResult { .error = std::move(error), .is_coherence_order_maximal_write = false };
 }
 } // namespace StoreResultExt
 
 namespace ReadModifyWriteResultExt {
 inline ReadModifyWriteResult
 ok(SVal old_value, SVal new_value, bool is_coherence_order_maximal_write) {
-    return ReadModifyWriteResult { /* error: */ std::unique_ptr<std::string>(nullptr),
-                                   /* old_value: */ GenmcScalarExt::from_sval(old_value),
-                                   /* new_value: */ GenmcScalarExt::from_sval(new_value),
-                                   is_coherence_order_maximal_write };
+    return ReadModifyWriteResult { .error = std::unique_ptr<std::string>(nullptr),
+                                   .old_value = GenmcScalarExt::from_sval(old_value),
+                                   .new_value = GenmcScalarExt::from_sval(new_value),
+                                   .is_coherence_order_maximal_write =
+                                       is_coherence_order_maximal_write };
 }
 
 inline ReadModifyWriteResult from_error(std::unique_ptr<std::string> error) {
-    return ReadModifyWriteResult { /* error: */ std::move(error),
-                                   /* old_value: */ GenmcScalarExt::uninit(),
-                                   /* new_value: */ GenmcScalarExt::uninit(),
-                                   /* is_coherence_order_maximal_write: */ false };
+    return ReadModifyWriteResult { .error = std::move(error),
+                                   .old_value = GenmcScalarExt::uninit(),
+                                   .new_value = GenmcScalarExt::uninit(),
+                                   .is_coherence_order_maximal_write = false };
 }
 } // namespace ReadModifyWriteResultExt
 
+namespace CompareExchangeResultExt {
+inline CompareExchangeResult success(SVal old_value, bool is_coherence_order_maximal_write) {
+    return CompareExchangeResult { .error = nullptr,
+                                   .old_value = GenmcScalarExt::from_sval(old_value),
+                                   .is_success = true,
+                                   .is_coherence_order_maximal_write =
+                                       is_coherence_order_maximal_write };
+}
+
+inline CompareExchangeResult failure(SVal old_value) {
+    return CompareExchangeResult { .error = nullptr,
+                                   .old_value = GenmcScalarExt::from_sval(old_value),
+                                   .is_success = false,
+                                   .is_coherence_order_maximal_write = false };
+}
+
+inline CompareExchangeResult from_error(std::unique_ptr<std::string> error) {
+    return CompareExchangeResult { .error = std::move(error),
+                                   .old_value = GenmcScalarExt::uninit(),
+                                   .is_success = false,
+                                   .is_coherence_order_maximal_write = false };
+}
+} // namespace CompareExchangeResultExt
+
 #endif /* GENMC_MIRI_INTERFACE_HPP */
diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp
index cd28e0d148f..05c82641df9 100644
--- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp
+++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp
@@ -155,6 +155,71 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
     );
 }
 
+[[nodiscard]] auto MiriGenmcShim::handle_compare_exchange(
+    ThreadId thread_id,
+    uint64_t address,
+    uint64_t size,
+    GenmcScalar expected_value,
+    GenmcScalar new_value,
+    GenmcScalar old_val,
+    MemOrdering success_ordering,
+    MemOrdering fail_load_ordering,
+    bool can_fail_spuriously
+) -> CompareExchangeResult {
+    // NOTE: Both the store and load events should get the same `ordering`, it should not be split
+    // into a load and a store component. This means we can have for example `AcqRel` loads and
+    // stores, but this is intended for CAS operations.
+
+    // FIXME(GenMC): properly handle failure memory ordering.
+
+    auto expectedVal = GenmcScalarExt::to_sval(expected_value);
+    auto new_val = GenmcScalarExt::to_sval(new_value);
+
+    const auto load_ret = handle_load_reset_if_none<EventLabel::EventLabelKind::CasRead>(
+        thread_id,
+        success_ordering,
+        SAddr(address),
+        ASize(size),
+        AType::Unsigned, // The type is only used for printing.
+        expectedVal,
+        new_val
+    );
+    if (const auto* err = std::get_if<VerificationError>(&load_ret))
+        return CompareExchangeResultExt::from_error(format_error(*err));
+    const auto* ret_val = std::get_if<SVal>(&load_ret);
+    ERROR_ON(nullptr == ret_val, "Unimplemented: load returned unexpected result.");
+    const auto read_old_val = *ret_val;
+    if (read_old_val != expectedVal)
+        return CompareExchangeResultExt::failure(read_old_val);
+
+    // FIXME(GenMC): Add support for modelling spurious failures.
+
+    const auto storePos = inc_pos(thread_id);
+    const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::CasWrite>(
+        storePos,
+        success_ordering,
+        SAddr(address),
+        ASize(size),
+        AType::Unsigned, // The type is only used for printing.
+        new_val
+    );
+    if (const auto* err = std::get_if<VerificationError>(&store_ret))
+        return CompareExchangeResultExt::from_error(format_error(*err));
+    const auto* store_ret_val = std::get_if<std::monostate>(&store_ret);
+    ERROR_ON(
+        nullptr == store_ret_val,
+        "Unimplemented: compare-exchange store returned unexpected result."
+    );
+
+    // FIXME(genmc,mixed-accesses): Use the value that GenMC returns from handleStore (once
+    // available).
+    const auto& g = getExec().getGraph();
+    return CompareExchangeResultExt::success(
+        read_old_val,
+        /* is_coherence_order_maximal_write */ g.co_max(SAddr(address))->getPos() == storePos
+    );
+}
+
 /**** Memory (de)allocation ****/
 
 auto MiriGenmcShim::handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment)
diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp
index 5a53fee0592..a17a83aa06e 100644
--- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp
+++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp
@@ -152,10 +152,10 @@ static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel
         // Miri already ensures that memory accesses are valid, so this check doesn't matter.
         // We check that the address is static, but skip checking if it is part of an actual
         // allocation.
-        /* isStaticallyAllocated: */ [](SAddr addr) { return addr.isStatic(); },
+        .isStaticallyAllocated = [](SAddr addr) { return addr.isStatic(); },
         // FIXME(genmc,error reporting): Once a proper a proper API for passing such information is
         // implemented in GenMC, Miri should use it to improve the produced error messages.
-        /* getStaticName: */ [](SAddr addr) { return "[UNKNOWN STATIC]"; },
+        .getStaticName = [](SAddr addr) { return "[UNKNOWN STATIC]"; },
         // This function is called to get the initial value stored at the given address.
         //
         // From a Miri perspective, this API doesn't work very well: most memory starts out
@@ -177,10 +177,10 @@ static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel
         // FIXME(genmc): implement proper support for uninitialized memory in GenMC. Ideally, the
         // initial value getter would return an `optional<SVal>`, since the memory location may be
         // uninitialized.
-        /* initValGetter: */ [](const AAccess& a) { return SVal(0xDEAD); },
+        .initValGetter = [](const AAccess& a) { return SVal(0xDEAD); },
         // Miri serves non-atomic loads from its own memory and these GenMC checks are wrong in
         // that case. This should no longer be required with proper mixed-size access support.
-        /* skipUninitLoadChecks: */ [](MemOrdering ord) { return ord == MemOrdering::NotAtomic; },
+        .skipUninitLoadChecks = [](MemOrdering ord) { return ord == MemOrdering::NotAtomic; },
     };
     driver->setInterpCallbacks(std::move(interpreter_callbacks));
 
diff --git a/src/tools/miri/genmc-sys/src/lib.rs b/src/tools/miri/genmc-sys/src/lib.rs
index 1de4c4eb5e8..31bc2606adc 100644
--- a/src/tools/miri/genmc-sys/src/lib.rs
+++ b/src/tools/miri/genmc-sys/src/lib.rs
@@ -198,6 +198,19 @@ mod ffi {
         is_coherence_order_maximal_write: bool,
     }
 
+    #[must_use]
+    #[derive(Debug)]
+    struct CompareExchangeResult {
+        /// If there was an error, it will be stored in `error`, otherwise it is `None`.
+        error: UniquePtr<CxxString>,
+        /// The value that was read by the compare-exchange.
+        old_value: GenmcScalar,
+        /// `true` if compare_exchange op was successful.
+        is_success: bool,
+        /// `true` if the write should also be reflected in Miri's memory representation.
+        is_coherence_order_maximal_write: bool,
+    }
+
     /**** These are GenMC types that we have to copy-paste here since cxx does not support
     "importing" externally defined C++ types. ****/
 
@@ -313,6 +326,18 @@ mod ffi {
             rhs_value: GenmcScalar,
             old_value: GenmcScalar,
         ) -> ReadModifyWriteResult;
+        fn handle_compare_exchange(
+            self: Pin<&mut MiriGenmcShim>,
+            thread_id: i32,
+            address: u64,
+            size: u64,
+            expected_value: GenmcScalar,
+            new_value: GenmcScalar,
+            old_value: GenmcScalar,
+            success_ordering: MemOrdering,
+            fail_load_ordering: MemOrdering,
+            can_fail_spuriously: bool,
+        ) -> CompareExchangeResult;
         fn handle_store(
             self: Pin<&mut MiriGenmcShim>,
             thread_id: i32,
diff --git a/src/tools/miri/src/concurrency/genmc/helper.rs b/src/tools/miri/src/concurrency/genmc/helper.rs
index 2a84ca20366..48a5ec8bb26 100644
--- a/src/tools/miri/src/concurrency/genmc/helper.rs
+++ b/src/tools/miri/src/concurrency/genmc/helper.rs
@@ -1,20 +1,52 @@
+use std::sync::RwLock;
+
 use genmc_sys::{MemOrdering, RMWBinOp};
 use rustc_abi::Size;
 use rustc_const_eval::interpret::{InterpResult, interp_ok};
+use rustc_data_structures::fx::FxHashSet;
 use rustc_middle::mir;
 use rustc_middle::ty::ScalarInt;
+use rustc_span::Span;
 use tracing::debug;
 
 use super::GenmcScalar;
+use crate::diagnostics::EvalContextExt;
 use crate::intrinsics::AtomicRmwOp;
 use crate::{
-    AtomicFenceOrd, AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd, MiriInterpCx, Scalar,
-    throw_unsup_format,
+    AtomicFenceOrd, AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd, InterpCx, MiriInterpCx,
+    MiriMachine, NonHaltingDiagnostic, Scalar, throw_unsup_format,
 };
 
 /// Maximum size memory access in bytes that GenMC supports.
 pub(super) const MAX_ACCESS_SIZE: u64 = 8;
 
+/// Type for storing spans for already emitted warnings.
+pub(super) type WarningCache = RwLock<FxHashSet<Span>>;
+
+#[derive(Default)]
+pub(super) struct Warnings {
+    pub(super) compare_exchange_failure_ordering: WarningCache,
+    pub(super) compare_exchange_weak: WarningCache,
+}
+
+/// Emit a warning if it hasn't already been reported for current span.
+pub(super) fn emit_warning<'tcx>(
+    ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
+    cache: &WarningCache,
+    diagnostic: impl FnOnce() -> NonHaltingDiagnostic,
+) {
+    let span = ecx.machine.current_span();
+    if cache.read().unwrap().contains(&span) {
+        return;
+    }
+    // This span has not yet been reported, so we insert it into the cache and report it.
+    let mut cache = cache.write().unwrap();
+    if cache.insert(span) {
+        // Some other thread may have added this span while we didn't hold the lock, so we only emit it if the insertions succeeded.
+        ecx.emit_diagnostic(diagnostic());
+    }
+}
+
 /// This function is used to split up a large memory access into aligned, non-overlapping chunks of a limited size.
 /// Returns an iterator over the chunks, yielding `(base address, size)` of each chunk, ordered by address.
 pub fn split_access(address: Size, size: Size) -> impl Iterator<Item = (u64, u64)> {
@@ -112,7 +144,53 @@ impl AtomicFenceOrd {
     }
 }
 
+/// Since GenMC ignores the failure memory ordering and Miri should not detect bugs that don't actually exist, we upgrade the success ordering if required.
+/// This means that Miri running in GenMC mode will not explore all possible executions allowed under the RC11 memory model.
+/// FIXME(genmc): remove this once GenMC properly supports the failure memory ordering.
+pub(super) fn maybe_upgrade_compare_exchange_success_orderings(
+    success: AtomicRwOrd,
+    failure: AtomicReadOrd,
+) -> AtomicRwOrd {
+    use AtomicReadOrd::*;
+    let (success_read, success_write) = success.split_memory_orderings();
+    let upgraded_success_read = match (success_read, failure) {
+        (_, SeqCst) | (SeqCst, _) => SeqCst,
+        (Acquire, _) | (_, Acquire) => Acquire,
+        (Relaxed, Relaxed) => Relaxed,
+    };
+    AtomicRwOrd::from_split_memory_orderings(upgraded_success_read, success_write)
+}
+
 impl AtomicRwOrd {
+    /// Split up an atomic read-write memory ordering into a separate read and write ordering.
+    pub(super) fn split_memory_orderings(self) -> (AtomicReadOrd, AtomicWriteOrd) {
+        match self {
+            AtomicRwOrd::Relaxed => (AtomicReadOrd::Relaxed, AtomicWriteOrd::Relaxed),
+            AtomicRwOrd::Acquire => (AtomicReadOrd::Acquire, AtomicWriteOrd::Relaxed),
+            AtomicRwOrd::Release => (AtomicReadOrd::Relaxed, AtomicWriteOrd::Release),
+            AtomicRwOrd::AcqRel => (AtomicReadOrd::Acquire, AtomicWriteOrd::Release),
+            AtomicRwOrd::SeqCst => (AtomicReadOrd::SeqCst, AtomicWriteOrd::SeqCst),
+        }
+    }
+
+    /// Split up an atomic read-write memory ordering into a separate read and write ordering.
+    fn from_split_memory_orderings(
+        read_ordering: AtomicReadOrd,
+        write_ordering: AtomicWriteOrd,
+    ) -> Self {
+        match (read_ordering, write_ordering) {
+            (AtomicReadOrd::Relaxed, AtomicWriteOrd::Relaxed) => AtomicRwOrd::Relaxed,
+            (AtomicReadOrd::Acquire, AtomicWriteOrd::Relaxed) => AtomicRwOrd::Acquire,
+            (AtomicReadOrd::Relaxed, AtomicWriteOrd::Release) => AtomicRwOrd::Release,
+            (AtomicReadOrd::Acquire, AtomicWriteOrd::Release) => AtomicRwOrd::AcqRel,
+            (AtomicReadOrd::SeqCst, AtomicWriteOrd::SeqCst) => AtomicRwOrd::SeqCst,
+            _ =>
+                panic!(
+                    "Unsupported memory ordering combination ({read_ordering:?}, {write_ordering:?})"
+                ),
+        }
+    }
+
     pub(super) fn to_genmc(self) -> MemOrdering {
         match self {
             AtomicRwOrd::Relaxed => MemOrdering::Relaxed,
diff --git a/src/tools/miri/src/concurrency/genmc/mod.rs b/src/tools/miri/src/concurrency/genmc/mod.rs
index c1da86c6733..7270c668106 100644
--- a/src/tools/miri/src/concurrency/genmc/mod.rs
+++ b/src/tools/miri/src/concurrency/genmc/mod.rs
@@ -13,15 +13,16 @@ use tracing::{debug, info};
 
 use self::global_allocations::{EvalContextExt as _, GlobalAllocationHandler};
 use self::helper::{
-    MAX_ACCESS_SIZE, genmc_scalar_to_scalar, scalar_to_genmc_scalar, to_genmc_rmw_op,
+    MAX_ACCESS_SIZE, Warnings, emit_warning, genmc_scalar_to_scalar,
+    maybe_upgrade_compare_exchange_success_orderings, scalar_to_genmc_scalar, to_genmc_rmw_op,
 };
 use self::thread_id_map::ThreadIdMap;
 use crate::concurrency::genmc::helper::split_access;
 use crate::intrinsics::AtomicRmwOp;
 use crate::{
     AtomicFenceOrd, AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd, MemoryKind, MiriConfig,
-    MiriMachine, MiriMemoryKind, Scalar, TerminationInfo, ThreadId, ThreadManager, VisitProvenance,
-    VisitWith,
+    MiriMachine, MiriMemoryKind, NonHaltingDiagnostic, Scalar, TerminationInfo, ThreadId,
+    ThreadManager, VisitProvenance, VisitWith,
 };
 
 mod config;
@@ -81,16 +82,22 @@ impl PerExecutionState {
     }
 }
 
-#[derive(Debug)]
 struct GlobalState {
     /// Keep track of global allocations, to ensure they keep the same address across different executions, even if the order of allocations changes.
     /// The `AllocId` for globals is stable across executions, so we can use it as an identifier.
     global_allocations: GlobalAllocationHandler,
+
+    /// Cache for which warnings have already been shown to the user.
+    /// `None` if warnings are disabled.
+    warning_cache: Option<Warnings>,
 }
 
 impl GlobalState {
-    fn new(target_usize_max: u64) -> Self {
-        Self { global_allocations: GlobalAllocationHandler::new(target_usize_max) }
+    fn new(target_usize_max: u64, print_warnings: bool) -> Self {
+        Self {
+            global_allocations: GlobalAllocationHandler::new(target_usize_max),
+            warning_cache: print_warnings.then(Default::default),
+        }
     }
 }
 
@@ -348,21 +355,91 @@ impl GenmcCtx {
     /// `old_value` is the value that a non-atomic load would read here, or `None` if the memory is uninitalized.
     pub(crate) fn atomic_compare_exchange<'tcx>(
         &self,
-        _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
-        _address: Size,
-        _size: Size,
-        _expected_old_value: Scalar,
-        _new_value: Scalar,
-        _success: AtomicRwOrd,
-        _fail: AtomicReadOrd,
-        _can_fail_spuriously: bool,
-        _old_value: Scalar,
+        ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
+        address: Size,
+        size: Size,
+        expected_old_value: Scalar,
+        new_value: Scalar,
+        success: AtomicRwOrd,
+        fail: AtomicReadOrd,
+        can_fail_spuriously: bool,
+        old_value: Scalar,
     ) -> InterpResult<'tcx, (Scalar, Option<Scalar>, bool)> {
         assert!(
             !self.get_alloc_data_races(),
             "atomic compare-exchange with data race checking disabled."
         );
-        throw_unsup_format!("FIXME(genmc): Add support for atomic compare_exchange.")
+        assert_ne!(0, size.bytes());
+        assert!(
+            size.bytes() <= MAX_ACCESS_SIZE,
+            "GenMC currently does not support atomic accesses larger than {} bytes (got {} bytes)",
+            MAX_ACCESS_SIZE,
+            size.bytes()
+        );
+
+        // Upgrade the success memory ordering to equal the failure ordering, since GenMC currently ignores the failure ordering.
+        // FIXME(genmc): remove this once GenMC properly supports the failure memory ordering.
+        let upgraded_success_ordering =
+            maybe_upgrade_compare_exchange_success_orderings(success, fail);
+
+        if let Some(warning_cache) = &self.global_state.warning_cache {
+            // FIXME(genmc): remove once GenMC supports failure memory ordering in `compare_exchange`.
+            let (effective_failure_ordering, _) =
+                upgraded_success_ordering.split_memory_orderings();
+            // Return a warning if the actual orderings don't match the upgraded ones.
+            if success != upgraded_success_ordering || effective_failure_ordering != fail {
+                emit_warning(ecx, &warning_cache.compare_exchange_failure_ordering, || {
+                    NonHaltingDiagnostic::GenmcCompareExchangeOrderingMismatch {
+                        success_ordering: success,
+                        upgraded_success_ordering,
+                        failure_ordering: fail,
+                        effective_failure_ordering,
+                    }
+                });
+            }
+            // FIXME(genmc): remove once GenMC implements spurious failures for `compare_exchange_weak`.
+            if can_fail_spuriously {
+                emit_warning(ecx, &warning_cache.compare_exchange_weak, || {
+                    NonHaltingDiagnostic::GenmcCompareExchangeWeak
+                });
+            }
+        }
+
+        debug!(
+            "GenMC: atomic_compare_exchange, address: {address:?}, size: {size:?} (expect: {expected_old_value:?}, new: {new_value:?}, old_value: {old_value:?}, {success:?}, orderings: {fail:?}), can fail spuriously: {can_fail_spuriously}"
+        );
+
+        let thread_infos = self.exec_state.thread_id_manager.borrow();
+        let genmc_tid = thread_infos.get_genmc_tid(ecx.machine.threads.active_thread());
+
+        let cas_result = self.handle.borrow_mut().pin_mut().handle_compare_exchange(
+            genmc_tid,
+            address.bytes(),
+            size.bytes(),
+            scalar_to_genmc_scalar(ecx, expected_old_value)?,
+            scalar_to_genmc_scalar(ecx, new_value)?,
+            scalar_to_genmc_scalar(ecx, old_value)?,
+            upgraded_success_ordering.to_genmc(),
+            fail.to_genmc(),
+            can_fail_spuriously,
+        );
+
+        if let Some(error) = cas_result.error.as_ref() {
+            // FIXME(genmc): error handling
+            throw_ub_format!("{}", error.to_string_lossy());
+        }
+
+        let return_scalar = genmc_scalar_to_scalar(ecx, cas_result.old_value, size)?;
+        debug!(
+            "GenMC: atomic_compare_exchange: result: {cas_result:?}, returning scalar: {return_scalar:?}"
+        );
+        // The write can only be a co-maximal write if the CAS succeeded.
+        assert!(cas_result.is_success || !cas_result.is_coherence_order_maximal_write);
+        interp_ok((
+            return_scalar,
+            cas_result.is_coherence_order_maximal_write.then_some(new_value),
+            cas_result.is_success,
+        ))
     }
 
     /// Inform GenMC about a non-atomic memory load
diff --git a/src/tools/miri/src/concurrency/genmc/run.rs b/src/tools/miri/src/concurrency/genmc/run.rs
index 24d13e6375b..7e4ed816a76 100644
--- a/src/tools/miri/src/concurrency/genmc/run.rs
+++ b/src/tools/miri/src/concurrency/genmc/run.rs
@@ -23,7 +23,9 @@ pub fn run_genmc_mode<'tcx>(
     // There exists only one `global_state` per full run in GenMC mode.
     // It is shared by all `GenmcCtx` in this run.
     // FIXME(genmc): implement multithreading once GenMC supports it.
-    let global_state = Arc::new(GlobalState::new(tcx.target_usize_max()));
+    // FIXME(genmc): disable warnings in estimation mode once it is added.
+    let global_state =
+        Arc::new(GlobalState::new(tcx.target_usize_max(), /* print_warnings */ true));
     let genmc_ctx = Rc::new(GenmcCtx::new(config, global_state));
 
     // `rep` is used to report the progress, Miri will panic on wrap-around.
diff --git a/src/tools/miri/src/diagnostics.rs b/src/tools/miri/src/diagnostics.rs
index 0842307caf9..15f7ccbabca 100644
--- a/src/tools/miri/src/diagnostics.rs
+++ b/src/tools/miri/src/diagnostics.rs
@@ -141,6 +141,13 @@ pub enum NonHaltingDiagnostic {
         ptr: Pointer,
     },
     ExternTypeReborrow,
+    GenmcCompareExchangeWeak,
+    GenmcCompareExchangeOrderingMismatch {
+        success_ordering: AtomicRwOrd,
+        upgraded_success_ordering: AtomicRwOrd,
+        failure_ordering: AtomicReadOrd,
+        effective_failure_ordering: AtomicReadOrd,
+    },
 }
 
 /// Level of Miri specific diagnostics
@@ -637,6 +644,8 @@ impl<'tcx> MiriMachine<'tcx> {
                 ("sharing memory with a native function".to_string(), DiagLevel::Warning),
             ExternTypeReborrow =>
                 ("reborrow of reference to `extern type`".to_string(), DiagLevel::Warning),
+            GenmcCompareExchangeWeak | GenmcCompareExchangeOrderingMismatch { .. } =>
+                ("GenMC might miss possible behaviors of this code".to_string(), DiagLevel::Warning),
             CreatedPointerTag(..)
             | PoppedPointerTag(..)
             | CreatedAlloc(..)
@@ -675,6 +684,23 @@ impl<'tcx> MiriMachine<'tcx> {
                 format!("weak memory emulation: outdated value returned from load at {ptr}"),
             ExternTypeReborrow =>
                 format!("reborrow of a reference to `extern type` is not properly supported"),
+            GenmcCompareExchangeWeak =>
+                "GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures."
+                    .to_string(),
+            GenmcCompareExchangeOrderingMismatch {
+                success_ordering,
+                upgraded_success_ordering,
+                failure_ordering,
+                effective_failure_ordering,
+            } => {
+                let was_upgraded_msg = if success_ordering != upgraded_success_ordering {
+                    format!("Success ordering '{success_ordering:?}' was upgraded to '{upgraded_success_ordering:?}' to match failure ordering '{failure_ordering:?}'")
+                } else {
+                    assert_ne!(failure_ordering, effective_failure_ordering);
+                    format!("Due to success ordering '{success_ordering:?}', the failure ordering '{failure_ordering:?}' is treated like '{effective_failure_ordering:?}'")
+                };
+                format!("GenMC currently does not model the failure ordering for `compare_exchange`. {was_upgraded_msg}. Miri with GenMC might miss bugs related to this memory access.")
+            }
         };
 
         let notes = match &e {
diff --git a/src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.rs b/src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.rs
new file mode 100644
index 00000000000..32954a643b3
--- /dev/null
+++ b/src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.rs
@@ -0,0 +1,45 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+// 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 2.
+//
+// This data race is hard to detect for Miri without GenMC, requiring -Zmiri-many-seeds=0..1024 at the time this test was created.
+
+// FIXME(genmc): once Miri-GenMC error reporting is improved, ensure that it correctly points to the two spans involved in the data race.
+
+#![no_main]
+
+#[path = "../../../utils/genmc.rs"]
+mod genmc;
+
+use std::sync::atomic::AtomicUsize;
+use std::sync::atomic::Ordering::*;
+
+use genmc::spawn_pthread_closure;
+static mut X: u64 = 0;
+static Y: AtomicUsize = AtomicUsize::new(0);
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    unsafe {
+        let _t1 = spawn_pthread_closure(|| {
+            X = 1;
+            Y.store(0, Release);
+            Y.store(1, Relaxed);
+        });
+        let _t2 = spawn_pthread_closure(|| {
+            if Y.load(Relaxed) > 2 {
+                X = 2; //~ ERROR: Undefined Behavior: Non-atomic race
+            }
+        });
+        let _t3 = spawn_pthread_closure(|| {
+            let _ = Y.compare_exchange(2, 3, Relaxed, Relaxed);
+        });
+
+        let _t4 = spawn_pthread_closure(|| {
+            let _ = Y.compare_exchange(1, 2, Relaxed, Relaxed);
+        });
+    }
+    0
+}
diff --git a/src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.stderr b/src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.stderr
new file mode 100644
index 00000000000..946d9a2124b
--- /dev/null
+++ b/src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.stderr
@@ -0,0 +1,19 @@
+error: Undefined Behavior: Non-atomic race
+  --> tests/genmc/fail/data_race/mpu2_rels_rlx.rs:LL:CC
+   |
+LL |                 X = 2;
+   |                 ^^^^^ Undefined Behavior occurred here
+   |
+   = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
+   = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
+   = note: BACKTRACE on thread `unnamed-ID`:
+   = note: inside closure at tests/genmc/fail/data_race/mpu2_rels_rlx.rs:LL:CC
+   = note: inside `<std::boxed::Box<{closure@tests/genmc/fail/data_race/mpu2_rels_rlx.rs:LL:CC}> as std::ops::FnOnce<()>>::call_once` at RUSTLIB/alloc/src/boxed.rs:LL:CC
+note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/fail/data_race/mpu2_rels_rlx.rs:LL:CC}>`
+  --> tests/genmc/fail/data_race/../../../utils/genmc.rs:LL:CC
+   |
+LL |         f();
+   |         ^^^
+
+error: aborting due to 1 previous error
+
diff --git a/src/tools/miri/tests/genmc/fail/loom/store_buffering.genmc.stderr b/src/tools/miri/tests/genmc/fail/loom/store_buffering.genmc.stderr
new file mode 100644
index 00000000000..a6c3ed7055e
--- /dev/null
+++ b/src/tools/miri/tests/genmc/fail/loom/store_buffering.genmc.stderr
@@ -0,0 +1,13 @@
+error: abnormal termination: the program aborted execution
+  --> tests/genmc/fail/loom/store_buffering.rs:LL:CC
+   |
+LL |             std::process::abort();
+   |             ^^^^^^^^^^^^^^^^^^^^^ abnormal termination occurred here
+   |
+   = note: BACKTRACE:
+   = note: inside `miri_start` at tests/genmc/fail/loom/store_buffering.rs:LL:CC
+
+note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
+
+error: aborting due to 1 previous error
+
diff --git a/src/tools/miri/tests/genmc/fail/loom/store_buffering.non_genmc.stderr b/src/tools/miri/tests/genmc/fail/loom/store_buffering.non_genmc.stderr
new file mode 100644
index 00000000000..a6c3ed7055e
--- /dev/null
+++ b/src/tools/miri/tests/genmc/fail/loom/store_buffering.non_genmc.stderr
@@ -0,0 +1,13 @@
+error: abnormal termination: the program aborted execution
+  --> tests/genmc/fail/loom/store_buffering.rs:LL:CC
+   |
+LL |             std::process::abort();
+   |             ^^^^^^^^^^^^^^^^^^^^^ abnormal termination occurred here
+   |
+   = note: BACKTRACE:
+   = note: inside `miri_start` at tests/genmc/fail/loom/store_buffering.rs:LL:CC
+
+note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
+
+error: aborting due to 1 previous error
+
diff --git a/src/tools/miri/tests/genmc/fail/loom/store_buffering.rs b/src/tools/miri/tests/genmc/fail/loom/store_buffering.rs
new file mode 100644
index 00000000000..4955dfd8a77
--- /dev/null
+++ b/src/tools/miri/tests/genmc/fail/loom/store_buffering.rs
@@ -0,0 +1,57 @@
+//@ revisions: non_genmc genmc
+//@[genmc] compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+// SPDX-License-Identifier: MIT
+// SPDX-FileCopyrightText: Copyright (c) 2019 Carl Lerche
+
+// This is the test `store_buffering` from `loom/test/litmus.rs`, adapted for Miri-GenMC.
+// https://github.com/tokio-rs/loom/blob/dbf32b04bae821c64be44405a0bb72ca08741558/tests/litmus.rs
+
+// This test shows the comparison between running Miri with or without GenMC.
+// Without GenMC, Miri requires multiple iterations of the loop to detect the error.
+
+#![no_main]
+
+#[path = "../../../utils/genmc.rs"]
+mod genmc;
+
+use std::sync::atomic::AtomicUsize;
+use std::sync::atomic::Ordering::*;
+
+use crate::genmc::*;
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    // For normal Miri, we need multiple repetitions, but GenMC should find the bug with only 1.
+    const REPS: usize = if cfg!(non_genmc) { 128 } else { 1 };
+    for _ in 0..REPS {
+        // New atomics every iterations, so they don't influence each other.
+        let x = AtomicUsize::new(0);
+        let y = AtomicUsize::new(0);
+
+        // FIXME(genmc,HACK): remove these initializing writes once Miri-GenMC supports mixed atomic-non-atomic accesses.
+        x.store(0, Relaxed);
+        y.store(0, Relaxed);
+
+        let mut a: usize = 1234;
+        let mut b: usize = 1234;
+        unsafe {
+            let ids = [
+                spawn_pthread_closure(|| {
+                    x.store(1, Relaxed);
+                    a = y.load(Relaxed)
+                }),
+                spawn_pthread_closure(|| {
+                    y.store(1, Relaxed);
+                    b = x.load(Relaxed)
+                }),
+            ];
+            join_pthreads(ids);
+        }
+        if (a, b) == (0, 0) {
+            std::process::abort(); //~ ERROR: abnormal termination
+        }
+    }
+
+    0
+}
diff --git a/src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.rs b/src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.rs
new file mode 100644
index 00000000000..8a77d54a64f
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.rs
@@ -0,0 +1,70 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows -Zmiri-ignore-leaks
+
+// Adapted from: `impl LazyKey`, `fn lazy_init`: rust/library/std/src/sys/thread_local/key/racy.rs
+// Two threads race to initialize a key, which is just an index into an array in this test.
+// The (Acquire, Release) orderings on the compare_exchange prevent any data races for reading from `VALUES[key]`.
+
+// FIXME(genmc): GenMC does not model the failure ordering of compare_exchange currently.
+// Miri thus upgrades the success ordering to prevent showing any false data races in cases like this one.
+// Once GenMC supports the failure ordering, this test should work without the upgrading.
+
+#![no_main]
+
+#[path = "../../../utils/genmc.rs"]
+mod genmc;
+
+use std::sync::atomic::AtomicUsize;
+use std::sync::atomic::Ordering::*;
+
+use crate::genmc::*;
+
+const KEY_SENTVAL: usize = usize::MAX;
+
+static KEY: AtomicUsize = AtomicUsize::new(KEY_SENTVAL);
+
+static mut VALUES: [usize; 2] = [0, 0];
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    // FIXME(genmc,HACK): remove this initializing write once Miri-GenMC supports mixed atomic-non-atomic accesses.
+    KEY.store(KEY_SENTVAL, Relaxed);
+
+    unsafe {
+        let mut a = 0;
+        let mut b = 0;
+        let ids = [
+            spawn_pthread_closure(|| {
+                VALUES[0] = 42;
+                let key = get_or_init(0);
+                if key > 2 {
+                    std::process::abort();
+                }
+                a = VALUES[key];
+            }),
+            spawn_pthread_closure(|| {
+                VALUES[1] = 1234;
+                let key = get_or_init(1);
+                if key > 2 {
+                    std::process::abort();
+                }
+                b = VALUES[key];
+            }),
+        ];
+        join_pthreads(ids);
+        if a != b {
+            std::process::abort();
+        }
+    }
+    0
+}
+
+fn get_or_init(key: usize) -> usize {
+    match KEY.compare_exchange(KEY_SENTVAL, key, Release, Acquire) {
+        // The CAS succeeded, so we've created the actual key.
+        Ok(_) => key,
+        // If someone beat us to the punch, use their key instead.
+        // The `Acquire` failure ordering means we synchronized with the `Release` compare_exchange in the thread that wrote the other key.
+        // We can thus read from `VALUES[other_key]` without a data race.
+        Err(other_key) => other_key,
+    }
+}
diff --git a/src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.stderr b/src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.stderr
new file mode 100644
index 00000000000..d97b8b3d92f
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.stderr
@@ -0,0 +1,22 @@
+warning: GenMC currently does not model the failure ordering for `compare_exchange`. Success ordering 'Release' was upgraded to 'AcqRel' to match failure ordering 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
+  --> tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.rs:LL:CC
+   |
+LL |     match KEY.compare_exchange(KEY_SENTVAL, key, Release, Acquire) {
+   |           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
+   |
+   = note: BACKTRACE on thread `unnamed-ID`:
+   = note: inside `get_or_init` at tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.rs:LL:CC
+note: inside closure
+  --> tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.rs:LL:CC
+   |
+LL |                 let key = get_or_init(0);
+   |                           ^^^^^^^^^^^^^^
+   = note: inside `<std::boxed::Box<{closure@tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.rs:LL:CC}> as std::ops::FnOnce<()>>::call_once` at RUSTLIB/alloc/src/boxed.rs:LL:CC
+note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.rs:LL:CC}>`
+  --> tests/genmc/pass/atomics/../../../utils/genmc.rs:LL:CC
+   |
+LL |         f();
+   |         ^^^
+
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 2
diff --git a/src/tools/miri/tests/genmc/pass/atomics/cas_simple.rs b/src/tools/miri/tests/genmc/pass/atomics/cas_simple.rs
new file mode 100644
index 00000000000..e32c7cdf80c
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/atomics/cas_simple.rs
@@ -0,0 +1,34 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+// Test the basic functionality of compare_exchange.
+
+#![no_main]
+
+use std::sync::atomic::AtomicUsize;
+use std::sync::atomic::Ordering::*;
+
+static VALUE: AtomicUsize = AtomicUsize::new(0);
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    VALUE.store(1, SeqCst);
+
+    // Expect success:
+    if VALUE.compare_exchange(1, 2, SeqCst, SeqCst) != Ok(1) {
+        std::process::abort();
+    }
+    // New value should be written:
+    if 2 != VALUE.load(SeqCst) {
+        std::process::abort()
+    }
+
+    // Expect failure:
+    if VALUE.compare_exchange(1234, 42, SeqCst, SeqCst) != Err(2) {
+        std::process::abort();
+    }
+    // Value should be unchanged:
+    if 2 != VALUE.load(SeqCst) {
+        std::process::abort()
+    }
+    0
+}
diff --git a/src/tools/miri/tests/genmc/pass/atomics/cas_simple.stderr b/src/tools/miri/tests/genmc/pass/atomics/cas_simple.stderr
new file mode 100644
index 00000000000..3b22247ee44
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/atomics/cas_simple.stderr
@@ -0,0 +1,2 @@
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 1
diff --git a/src/tools/miri/tests/genmc/pass/litmus/IRIWish.rs b/src/tools/miri/tests/genmc/pass/litmus/IRIWish.rs
index 163556dcc89..c81573d59d1 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/IRIWish.rs
+++ b/src/tools/miri/tests/genmc/pass/litmus/IRIWish.rs
@@ -57,9 +57,7 @@ fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
         join_pthreads(ids);
 
         // Print the values to check that we get all of them:
-        if writeln!(MiriStderr, "{results:?}").is_err() {
-            std::process::abort();
-        }
+        writeln!(MiriStderr, "{results:?}").unwrap_or_else(|_| std::process::abort());
 
         0
     }
diff --git a/src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.rs b/src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.rs
new file mode 100644
index 00000000000..9bb156a9997
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.rs
@@ -0,0 +1,67 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+// Translated from GenMC's "litmus/MPU2+rels+acqf" test.
+
+#![no_main]
+
+#[path = "../../../utils/genmc.rs"]
+mod genmc;
+#[path = "../../../utils/mod.rs"]
+mod utils;
+
+use std::fmt::Write;
+use std::sync::atomic::AtomicU64;
+use std::sync::atomic::Ordering::*;
+
+use crate::genmc::*;
+use crate::utils::*;
+
+// Note: the GenMC equivalent of this test (genmc/tests/correct/litmus/MPU2+rels+acqf/mpu2+rels+acqf.c) uses non-atomic accesses for `X` with disabled race detection.
+static X: AtomicU64 = AtomicU64::new(0);
+static Y: AtomicU64 = AtomicU64::new(0);
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    // FIXME(genmc,HACK): remove these initializing writes once Miri-GenMC supports mixed atomic-non-atomic accesses.
+    X.store(0, Relaxed);
+    Y.store(0, Relaxed);
+
+    unsafe {
+        let mut a = Ok(1234);
+        let mut b = Ok(1234);
+        let mut c = 1234;
+        let ids = [
+            spawn_pthread_closure(|| {
+                X.store(1, Relaxed);
+
+                Y.store(0, Release);
+                Y.store(1, Relaxed);
+            }),
+            spawn_pthread_closure(|| {
+                a = Y.compare_exchange(2, 3, Relaxed, Relaxed);
+            }),
+            spawn_pthread_closure(|| {
+                b = Y.compare_exchange(1, 2, Relaxed, Relaxed);
+            }),
+            spawn_pthread_closure(|| {
+                c = Y.load(Acquire);
+                if c > 2 {
+                    std::sync::atomic::fence(Acquire);
+                    X.store(2, Relaxed);
+                }
+            }),
+        ];
+        join_pthreads(ids);
+
+        // Print the values to check that we get all of them:
+        writeln!(
+            MiriStderr,
+            "X={}, Y={}, a={a:?}, b={b:?}, c={c}",
+            X.load(Relaxed),
+            Y.load(Relaxed)
+        )
+        .unwrap_or_else(|_| std::process::abort());
+
+        0
+    }
+}
diff --git a/src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.stderr b/src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.stderr
new file mode 100644
index 00000000000..4551c00b057
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.stderr
@@ -0,0 +1,38 @@
+X=1, Y=2, a=Err(1), b=Ok(1), c=2
+X=1, Y=2, a=Err(1), b=Ok(1), c=1
+X=1, Y=2, a=Err(1), b=Ok(1), c=0
+X=1, Y=2, a=Err(1), b=Ok(1), c=0
+X=2, Y=3, a=Ok(2), b=Ok(1), c=3
+X=1, Y=3, a=Ok(2), b=Ok(1), c=3
+X=1, Y=3, a=Ok(2), b=Ok(1), c=2
+X=1, Y=3, a=Ok(2), b=Ok(1), c=1
+X=1, Y=3, a=Ok(2), b=Ok(1), c=0
+X=1, Y=3, a=Ok(2), b=Ok(1), c=0
+X=1, Y=1, a=Err(1), b=Err(0), c=1
+X=1, Y=1, a=Err(1), b=Err(0), c=0
+X=1, Y=1, a=Err(1), b=Err(0), c=0
+X=1, Y=1, a=Err(1), b=Err(0), c=1
+X=1, Y=1, a=Err(1), b=Err(0), c=0
+X=1, Y=1, a=Err(1), b=Err(0), c=0
+X=1, Y=2, a=Err(0), b=Ok(1), c=2
+X=1, Y=2, a=Err(0), b=Ok(1), c=1
+X=1, Y=2, a=Err(0), b=Ok(1), c=0
+X=1, Y=2, a=Err(0), b=Ok(1), c=0
+X=1, Y=1, a=Err(0), b=Err(0), c=1
+X=1, Y=1, a=Err(0), b=Err(0), c=0
+X=1, Y=1, a=Err(0), b=Err(0), c=0
+X=1, Y=1, a=Err(0), b=Err(0), c=1
+X=1, Y=1, a=Err(0), b=Err(0), c=0
+X=1, Y=1, a=Err(0), b=Err(0), c=0
+X=1, Y=2, a=Err(0), b=Ok(1), c=2
+X=1, Y=2, a=Err(0), b=Ok(1), c=1
+X=1, Y=2, a=Err(0), b=Ok(1), c=0
+X=1, Y=2, a=Err(0), b=Ok(1), c=0
+X=1, Y=1, a=Err(0), b=Err(0), c=1
+X=1, Y=1, a=Err(0), b=Err(0), c=0
+X=1, Y=1, a=Err(0), b=Err(0), c=0
+X=1, Y=1, a=Err(0), b=Err(0), c=1
+X=1, Y=1, a=Err(0), b=Err(0), c=0
+X=1, Y=1, a=Err(0), b=Err(0), c=0
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 36
diff --git a/src/tools/miri/tests/genmc/pass/litmus/Z6_U.rs b/src/tools/miri/tests/genmc/pass/litmus/Z6_U.rs
index ac5c3724254..f96679b23a5 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/Z6_U.rs
+++ b/src/tools/miri/tests/genmc/pass/litmus/Z6_U.rs
@@ -55,11 +55,8 @@ fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
         join_pthreads(ids);
 
         // Print the values to check that we get all of them:
-        if writeln!(MiriStderr, "a={a}, b={b}, X={}, Y={}", X.load(Relaxed), Y.load(Relaxed))
-            .is_err()
-        {
-            std::process::abort();
-        }
+        writeln!(MiriStderr, "a={a}, b={b}, X={}, Y={}", X.load(Relaxed), Y.load(Relaxed))
+            .unwrap_or_else(|_| std::process::abort());
         0
     }
 }
diff --git a/src/tools/miri/tests/genmc/pass/litmus/casdep.rs b/src/tools/miri/tests/genmc/pass/litmus/casdep.rs
new file mode 100644
index 00000000000..c376d96b111
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/casdep.rs
@@ -0,0 +1,37 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+// Translated from GenMC's test "litmus/casdep".
+
+#![no_main]
+
+#[path = "../../../utils/genmc.rs"]
+mod genmc;
+
+use std::sync::atomic::AtomicU64;
+use std::sync::atomic::Ordering::*;
+
+use crate::genmc::*;
+
+static X: AtomicU64 = AtomicU64::new(0);
+static Y: AtomicU64 = AtomicU64::new(0);
+static Z: AtomicU64 = AtomicU64::new(0);
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    // FIXME(genmc,HACK): remove these initializing writes once Miri-GenMC supports mixed atomic-non-atomic accesses.
+    X.store(0, Relaxed);
+    Y.store(0, Relaxed);
+    Z.store(0, Relaxed);
+
+    unsafe {
+        spawn_pthread_closure(|| {
+            let a = X.load(Relaxed);
+            let _b = Y.compare_exchange(a, 1, Relaxed, Relaxed);
+            Z.store(a, Relaxed);
+        });
+        spawn_pthread_closure(|| {
+            Y.store(2, Relaxed);
+        });
+        0
+    }
+}
diff --git a/src/tools/miri/tests/genmc/pass/litmus/casdep.stderr b/src/tools/miri/tests/genmc/pass/litmus/casdep.stderr
new file mode 100644
index 00000000000..01701dfe691
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/casdep.stderr
@@ -0,0 +1,2 @@
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 2
diff --git a/src/tools/miri/tests/genmc/pass/litmus/ccr.rs b/src/tools/miri/tests/genmc/pass/litmus/ccr.rs
new file mode 100644
index 00000000000..865895b4dcd
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/ccr.rs
@@ -0,0 +1,34 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+// Translated from GenMC's test "litmus/ccr".
+
+#![no_main]
+
+#[path = "../../../utils/genmc.rs"]
+mod genmc;
+
+use std::sync::atomic::AtomicU64;
+use std::sync::atomic::Ordering::*;
+
+use crate::genmc::*;
+
+static X: AtomicU64 = AtomicU64::new(0);
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    // FIXME(genmc,HACK): remove this initializing write once Miri-GenMC supports mixed atomic-non-atomic accesses.
+    X.store(0, Relaxed);
+
+    unsafe {
+        spawn_pthread_closure(|| {
+            let expected = 0;
+            let _ = X.compare_exchange(expected, 42, Relaxed, Relaxed);
+        });
+        spawn_pthread_closure(|| {
+            let expected = 0;
+            let _ = X.compare_exchange(expected, 17, Relaxed, Relaxed);
+            X.load(Relaxed);
+        });
+        0
+    }
+}
diff --git a/src/tools/miri/tests/genmc/pass/litmus/ccr.stderr b/src/tools/miri/tests/genmc/pass/litmus/ccr.stderr
new file mode 100644
index 00000000000..01701dfe691
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/ccr.stderr
@@ -0,0 +1,2 @@
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 2
diff --git a/src/tools/miri/tests/genmc/pass/litmus/cii.rs b/src/tools/miri/tests/genmc/pass/litmus/cii.rs
new file mode 100644
index 00000000000..663c806e667
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/cii.rs
@@ -0,0 +1,35 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+// Translated from GenMC's test "litmus/cii".
+
+#![no_main]
+
+#[path = "../../../utils/genmc.rs"]
+mod genmc;
+
+use std::sync::atomic::AtomicU64;
+use std::sync::atomic::Ordering::*;
+
+use crate::genmc::*;
+
+static X: AtomicU64 = AtomicU64::new(0);
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    // FIXME(genmc,HACK): remove this initializing write once Miri-GenMC supports mixed atomic-non-atomic accesses.
+    X.store(0, Relaxed);
+
+    unsafe {
+        spawn_pthread_closure(|| {
+            let expected = 1;
+            let _ = X.compare_exchange(expected, 2, Relaxed, Relaxed);
+        });
+        spawn_pthread_closure(|| {
+            X.fetch_add(1, Relaxed);
+        });
+        spawn_pthread_closure(|| {
+            X.fetch_add(1, Relaxed);
+        });
+        0
+    }
+}
diff --git a/src/tools/miri/tests/genmc/pass/litmus/cii.stderr b/src/tools/miri/tests/genmc/pass/litmus/cii.stderr
new file mode 100644
index 00000000000..be75e68fde7
--- /dev/null
+++ b/src/tools/miri/tests/genmc/pass/litmus/cii.stderr
@@ -0,0 +1,2 @@
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 6
-- 
cgit 1.4.1-3-g733a5


From 2c1f1f0e9bb706d9adbb71e0bc33923c4478eb85 Mon Sep 17 00:00:00 2001
From: Patrick-6 <pamu99@gmx.ch>
Date: Mon, 8 Sep 2025 10:17:14 +0200
Subject: Add GenMC estimation mode. Improve error handling and output
 printing.

---
 src/tools/miri/doc/genmc.md                        |   3 +
 .../miri/genmc-sys/cpp/include/MiriInterface.hpp   |   8 +-
 .../cpp/src/MiriInterface/Exploration.cpp          |  14 ++
 .../miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp |  23 ++-
 src/tools/miri/genmc-sys/src/lib.rs                |  55 +++++++-
 src/tools/miri/src/bin/miri.rs                     |   9 +-
 src/tools/miri/src/concurrency/genmc/config.rs     |  17 +++
 src/tools/miri/src/concurrency/genmc/dummy.rs      |  12 --
 src/tools/miri/src/concurrency/genmc/mod.rs        |  61 +++++---
 src/tools/miri/src/concurrency/genmc/run.rs        | 156 ++++++++++++++++-----
 .../genmc/fail/data_race/mpu2_rels_rlx.stderr      |   2 +
 .../fail/data_race/weak_orderings.rel_rlx.stderr   |   2 +
 .../fail/data_race/weak_orderings.rlx_acq.stderr   |   2 +
 .../fail/data_race/weak_orderings.rlx_rlx.stderr   |   2 +
 .../miri/tests/genmc/fail/loom/buggy_inc.stderr    |   2 +
 .../genmc/fail/loom/store_buffering.genmc.stderr   |   2 +
 .../genmc/fail/simple/2w2w_weak.relaxed4.stderr    |   2 +
 .../genmc/fail/simple/2w2w_weak.release4.stderr    |   2 +
 .../genmc/fail/simple/2w2w_weak.sc3_rel1.stderr    |   2 +
 .../atomics/cas_failure_ord_racy_key_init.stderr   |   4 +-
 .../tests/genmc/pass/atomics/cas_simple.stderr     |   4 +-
 .../miri/tests/genmc/pass/atomics/rmw_ops.stderr   |   4 +-
 .../miri/tests/genmc/pass/litmus/2cowr.stderr      |   4 +-
 .../tests/genmc/pass/litmus/2w2w_2sc_scf.stderr    |   4 +-
 .../pass/litmus/2w2w_3sc_1rel.release1.stderr      |   4 +-
 .../pass/litmus/2w2w_3sc_1rel.release2.stderr      |   4 +-
 .../tests/genmc/pass/litmus/2w2w_4rel.sc.stderr    |   4 +-
 .../tests/genmc/pass/litmus/2w2w_4rel.weak.stderr  |   4 +-
 .../miri/tests/genmc/pass/litmus/2w2w_4sc.stderr   |   4 +-
 .../tests/genmc/pass/litmus/IRIW-acq-sc.stderr     |   4 +-
 .../miri/tests/genmc/pass/litmus/IRIWish.stderr    |   4 +-
 src/tools/miri/tests/genmc/pass/litmus/LB.stderr   |   4 +-
 .../miri/tests/genmc/pass/litmus/LB_incMPs.stderr  |   4 +-
 src/tools/miri/tests/genmc/pass/litmus/MP.stderr   |   4 +-
 .../tests/genmc/pass/litmus/MPU2_rels_acqf.stderr  |   4 +-
 .../tests/genmc/pass/litmus/MPU_rels_acq.stderr    |   4 +-
 .../miri/tests/genmc/pass/litmus/MP_incMPs.stderr  |   4 +-
 .../tests/genmc/pass/litmus/MP_rels_acqf.stderr    |   4 +-
 src/tools/miri/tests/genmc/pass/litmus/SB.stderr   |   4 +-
 .../miri/tests/genmc/pass/litmus/SB_2sc_scf.stderr |   4 +-
 .../miri/tests/genmc/pass/litmus/Z6_U.sc.stderr    |   4 +-
 .../miri/tests/genmc/pass/litmus/Z6_U.weak.stderr  |   4 +-
 .../miri/tests/genmc/pass/litmus/Z6_acq.stderr     |   4 +-
 .../miri/tests/genmc/pass/litmus/atomicpo.stderr   |   4 +-
 .../miri/tests/genmc/pass/litmus/casdep.stderr     |   4 +-
 src/tools/miri/tests/genmc/pass/litmus/ccr.stderr  |   4 +-
 src/tools/miri/tests/genmc/pass/litmus/cii.stderr  |   4 +-
 src/tools/miri/tests/genmc/pass/litmus/corr.stderr |   4 +-
 .../miri/tests/genmc/pass/litmus/corr0.stderr      |   4 +-
 .../miri/tests/genmc/pass/litmus/corr1.stderr      |   4 +-
 .../miri/tests/genmc/pass/litmus/corr2.stderr      |   4 +-
 src/tools/miri/tests/genmc/pass/litmus/corw.stderr |   4 +-
 src/tools/miri/tests/genmc/pass/litmus/cowr.stderr |   4 +-
 .../tests/genmc/pass/litmus/cumul-release.stderr   |   4 +-
 .../miri/tests/genmc/pass/litmus/default.stderr    |   4 +-
 .../tests/genmc/pass/litmus/detour.join.stderr     |   4 +-
 .../tests/genmc/pass/litmus/detour.no_join.stderr  |   4 +-
 .../tests/genmc/pass/litmus/fr_w_w_w_reads.stderr  |   4 +-
 .../miri/tests/genmc/pass/litmus/inc2w.stderr      |   4 +-
 .../tests/genmc/pass/litmus/inc_inc_RR_W_RR.stderr |   4 +-
 src/tools/miri/tests/genmc/pass/litmus/riwi.stderr |   4 +-
 .../miri/tests/genmc/pass/litmus/viktor-relseq.rs  |   4 +-
 .../tests/genmc/pass/litmus/viktor-relseq.stderr   |   6 +-
 src/tools/miri/tests/ui.rs                         |   2 +
 64 files changed, 386 insertions(+), 170 deletions(-)

(limited to 'src/tools/miri/genmc-sys/cpp/include')

diff --git a/src/tools/miri/doc/genmc.md b/src/tools/miri/doc/genmc.md
index 8af697be34a..44e11dcbec4 100644
--- a/src/tools/miri/doc/genmc.md
+++ b/src/tools/miri/doc/genmc.md
@@ -24,6 +24,8 @@ Note that `cargo miri test` in GenMC mode is currently not supported.
 ### Supported Parameters
 
 - `-Zmiri-genmc`: Enable GenMC mode (not required if any other GenMC options are used).
+- `-Zmiri-genmc-estimate`: This enables estimation of the concurrent execution space and verification time, before running the full verification. This should help users detect when their program is too complex to fully verify in a reasonable time. This will explore enough executions to make a good estimation, but at least 10 and at most `estimation-max` executions.
+- `-Zmiri-genmc-estimation-max={MAX_ITERATIONS}`: Set the maximum number of executions that will be explored during estimation (default: 1000).
 - `-Zmiri-genmc-print-exec-graphs={none,explored,blocked,all}`: Make GenMC print the execution graph of the program after every explored, every blocked, or after every execution (default: None).
 - `-Zmiri-genmc-print-exec-graphs`: Shorthand for suffix `=explored`.
 - `-Zmiri-genmc-print-genmc-output`: Print the output that GenMC provides. NOTE: this output is quite verbose and the events in the printed execution graph are hard to map back to the Rust code location they originate from.
@@ -36,6 +38,7 @@ Note that `cargo miri test` in GenMC mode is currently not supported.
     - `debug1`:   Print revisits considered by GenMC.
     - `debug2`:   Print the execution graph after every memory access.
     - `debug3`:   Print reads-from values considered by GenMC.
+- `-Zmiri-genmc-verbose`: Show more information, such as estimated number of executions, and time taken for verification.
 
 #### Regular Miri parameters useful for GenMC mode
 
diff --git a/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp b/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp
index 662eb0e173c..444c9375319 100644
--- a/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp
+++ b/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp
@@ -31,6 +31,7 @@ enum class LogLevel : std::uint8_t;
 
 struct GenmcScalar;
 struct SchedulingResult;
+struct EstimationResult;
 struct LoadResult;
 struct StoreResult;
 struct ReadModifyWriteResult;
@@ -66,7 +67,7 @@ struct MiriGenmcShim : private GenMCDriver {
     /// `logLevel`, causing a data race. The safest way to use these functions is to call
     /// `set_log_level_raw` once, and only then start creating handles. There should not be any
     /// other (safe) way to create a `MiriGenmcShim`.
-    /* unsafe */ static auto create_handle(const GenmcParams& params)
+    /* unsafe */ static auto create_handle(const GenmcParams& params, bool estimation_mode)
         -> std::unique_ptr<MiriGenmcShim>;
 
     virtual ~MiriGenmcShim() {}
@@ -183,6 +184,11 @@ struct MiriGenmcShim : private GenMCDriver {
         return nullptr;
     }
 
+    /**** Printing and estimation mode functionality. ****/
+
+    /// Get the results of a run in estimation mode.
+    auto get_estimation_results() const -> EstimationResult;
+
   private:
     /** Increment the event index in the given thread by 1 and return the new event. */
     [[nodiscard]] inline auto inc_pos(ThreadId tid) -> Event {
diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp
index c51b59e8651..5e7188f17e0 100644
--- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp
+++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp
@@ -10,7 +10,9 @@
 #include "Support/Verbosity.hpp"
 
 // C++ headers:
+#include <cmath>
 #include <cstdint>
+#include <limits>
 
 auto MiriGenmcShim::schedule_next(
     const int curr_thread_id,
@@ -40,3 +42,15 @@ auto MiriGenmcShim::handle_execution_end() -> std::unique_ptr<std::string> {
     GenMCDriver::handleExecutionEnd();
     return {};
 }
+
+/**** Estimation mode result ****/
+
+auto MiriGenmcShim::get_estimation_results() const -> EstimationResult {
+    const auto& res = getResult();
+    return EstimationResult {
+        .mean = static_cast<double>(res.estimationMean),
+        .sd = static_cast<double>(std::sqrt(res.estimationVariance)),
+        .explored_execs = static_cast<uint64_t>(res.explored),
+        .blocked_execs = static_cast<uint64_t>(res.exploredBlocked),
+    };
+}
diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp
index a17a83aa06e..af13f0d0774 100644
--- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp
+++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp
@@ -58,7 +58,7 @@ static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel
     logLevel = to_genmc_verbosity_level(log_level);
 }
 
-/* unsafe */ auto MiriGenmcShim::create_handle(const GenmcParams& params)
+/* unsafe */ auto MiriGenmcShim::create_handle(const GenmcParams& params, bool estimation_mode)
     -> std::unique_ptr<MiriGenmcShim> {
     auto conf = std::make_shared<Config>();
 
@@ -82,7 +82,8 @@ static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel
     // Miri.
     conf->warnOnGraphSize = 1024 * 1024;
 
-    // We only support the `RC11` memory model for Rust, and `SC` when weak memory emulation is disabled.
+    // We only support the `RC11` memory model for Rust, and `SC` when weak memory emulation is
+    // disabled.
     conf->model = params.disable_weak_memory_emulation ? ModelType::SC : ModelType::RC11;
 
     // This prints the seed that GenMC picks for randomized scheduling during estimation mode.
@@ -119,12 +120,20 @@ static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel
     );
     conf->symmetryReduction = params.do_symmetry_reduction;
 
-    // FIXME(genmc): expose this setting to Miri (useful for testing Miri-GenMC).
-    conf->schedulePolicy = SchedulePolicy::WF;
-
+    // Set the scheduling policy. GenMC uses `WFR` for estimation mode.
+    // For normal verification, `WF` has the best performance and is the GenMC default.
+    // Other scheduling policies are used by GenMC for testing and for modes currently
+    // unsupported with Miri such as bounding, which uses LTR.
+    conf->schedulePolicy = estimation_mode ? SchedulePolicy::WFR : SchedulePolicy::WF;
+
+    // Set the min and max number of executions tested in estimation mode.
+    conf->estimationMin = 10; // default taken from GenMC
+    conf->estimationMax = params.estimation_max;
+    // Deviation threshold % under which estimation is deemed good enough.
+    conf->sdThreshold = 10; // default taken from GenMC
     // Set the mode used for this driver, either estimation or verification.
-    // FIXME(genmc): implement estimation mode.
-    const auto mode = GenMCDriver::Mode(GenMCDriver::VerificationMode {});
+    const auto mode = estimation_mode ? GenMCDriver::Mode(GenMCDriver::EstimationMode {})
+                                      : GenMCDriver::Mode(GenMCDriver::VerificationMode {});
 
     // Running Miri-GenMC without race detection is not supported.
     // Disabling this option also changes the behavior of the replay scheduler to only schedule
diff --git a/src/tools/miri/genmc-sys/src/lib.rs b/src/tools/miri/genmc-sys/src/lib.rs
index 31bc2606adc..733b3d780b1 100644
--- a/src/tools/miri/genmc-sys/src/lib.rs
+++ b/src/tools/miri/genmc-sys/src/lib.rs
@@ -27,6 +27,7 @@ static GENMC_LOG_LEVEL: OnceLock<LogLevel> = OnceLock::new();
 pub fn create_genmc_driver_handle(
     params: &GenmcParams,
     genmc_log_level: LogLevel,
+    do_estimation: bool,
 ) -> UniquePtr<MiriGenmcShim> {
     // SAFETY: Only setting the GenMC log level once is guaranteed by the `OnceLock`.
     // No other place calls `set_log_level_raw`, so the `logLevel` value in GenMC will not change once we initialize it once.
@@ -40,7 +41,7 @@ pub fn create_genmc_driver_handle(
         }),
         "Attempt to change the GenMC log level after it was already set"
     );
-    unsafe { MiriGenmcShim::create_handle(params) }
+    unsafe { MiriGenmcShim::create_handle(params, do_estimation) }
 }
 
 impl GenmcScalar {
@@ -54,6 +55,7 @@ impl GenmcScalar {
 impl Default for GenmcParams {
     fn default() -> Self {
         Self {
+            estimation_max: 1000, // default taken from GenMC
             print_random_schedule_seed: false,
             do_symmetry_reduction: false,
             // GenMC graphs can be quite large since Miri produces a lot of (non-atomic) events.
@@ -70,6 +72,20 @@ impl Default for LogLevel {
     }
 }
 
+impl FromStr for SchedulePolicy {
+    type Err = &'static str;
+
+    fn from_str(s: &str) -> Result<Self, Self::Err> {
+        Ok(match s {
+            "wf" => SchedulePolicy::WF,
+            "wfr" => SchedulePolicy::WFR,
+            "arbitrary" | "random" => SchedulePolicy::Arbitrary,
+            "ltr" => SchedulePolicy::LTR,
+            _ => return Err("invalid scheduling policy"),
+        })
+    }
+}
+
 impl FromStr for LogLevel {
     type Err = &'static str;
 
@@ -92,9 +108,12 @@ mod ffi {
     /**** Types shared between Miri/Rust and Miri/C++ through cxx_bridge: ****/
 
     /// Parameters that will be given to GenMC for setting up the model checker.
-    /// (The fields of this struct are visible to both Rust and C++)
+    /// The fields of this struct are visible to both Rust and C++.
+    /// Note that this struct is #[repr(C)], so the order of fields matters.
     #[derive(Clone, Debug)]
     struct GenmcParams {
+        /// Maximum number of executions explored in estimation mode.
+        pub estimation_max: u32,
         pub print_random_schedule_seed: bool,
         pub do_symmetry_reduction: bool,
         pub print_execution_graphs: ExecutiongraphPrinting,
@@ -165,6 +184,19 @@ mod ffi {
         next_thread: i32,
     }
 
+    #[must_use]
+    #[derive(Debug)]
+    struct EstimationResult {
+        /// Expected number of total executions.
+        mean: f64,
+        /// Standard deviation of the total executions estimate.
+        sd: f64,
+        /// Number of explored executions during the estimation.
+        explored_execs: u64,
+        /// Number of encounteded blocked executions during the estimation.
+        blocked_execs: u64,
+    }
+
     #[must_use]
     #[derive(Debug)]
     struct LoadResult {
@@ -214,6 +246,14 @@ mod ffi {
     /**** These are GenMC types that we have to copy-paste here since cxx does not support
     "importing" externally defined C++ types. ****/
 
+    #[derive(Clone, Copy, Debug)]
+    enum SchedulePolicy {
+        LTR,
+        WF,
+        WFR,
+        Arbitrary,
+    }
+
     #[derive(Debug)]
     /// Corresponds to GenMC's type with the same name.
     /// Should only be modified if changed by GenMC.
@@ -272,6 +312,7 @@ mod ffi {
         type ActionKind;
         type MemOrdering;
         type RMWBinOp;
+        type SchedulePolicy;
 
         /// Set the log level for GenMC.
         ///
@@ -295,7 +336,10 @@ mod ffi {
         /// start creating handles.
         /// There should not be any other (safe) way to create a `MiriGenmcShim`.
         #[Self = "MiriGenmcShim"]
-        unsafe fn create_handle(params: &GenmcParams) -> UniquePtr<MiriGenmcShim>;
+        unsafe fn create_handle(
+            params: &GenmcParams,
+            estimation_mode: bool,
+        ) -> UniquePtr<MiriGenmcShim>;
         /// Get the bit mask that GenMC expects for global memory allocations.
         fn get_global_alloc_static_mask() -> u64;
 
@@ -403,5 +447,10 @@ mod ffi {
         fn get_result_message(self: &MiriGenmcShim) -> UniquePtr<CxxString>;
         /// If an error occurred, return a string describing the error, otherwise, return `nullptr`.
         fn get_error_string(self: &MiriGenmcShim) -> UniquePtr<CxxString>;
+
+        /**** Printing functionality. ****/
+
+        /// Get the results of a run in estimation mode.
+        fn get_estimation_results(self: &MiriGenmcShim) -> EstimationResult;
     }
 }
diff --git a/src/tools/miri/src/bin/miri.rs b/src/tools/miri/src/bin/miri.rs
index 731fe283a21..8b15a786347 100644
--- a/src/tools/miri/src/bin/miri.rs
+++ b/src/tools/miri/src/bin/miri.rs
@@ -186,18 +186,17 @@ impl rustc_driver::Callbacks for MiriCompilerCalls {
                     optimizations is usually marginal at best.");
         }
 
-        if let Some(_genmc_config) = &config.genmc_config {
+        // Run in GenMC mode if enabled.
+        if config.genmc_config.is_some() {
+            // This is the entry point used in GenMC mode.
+            // This closure will be called multiple times to explore the concurrent execution space of the program.
             let eval_entry_once = |genmc_ctx: Rc<GenmcCtx>| {
                 miri::eval_entry(tcx, entry_def_id, entry_type, &config, Some(genmc_ctx))
             };
-
-            // FIXME(genmc): add estimation mode here.
-
             let return_code = run_genmc_mode(&config, eval_entry_once, tcx).unwrap_or_else(|| {
                 tcx.dcx().abort_if_errors();
                 rustc_driver::EXIT_FAILURE
             });
-
             exit(return_code);
         };
 
diff --git a/src/tools/miri/src/concurrency/genmc/config.rs b/src/tools/miri/src/concurrency/genmc/config.rs
index 34933d423f0..c7cfa6012b8 100644
--- a/src/tools/miri/src/concurrency/genmc/config.rs
+++ b/src/tools/miri/src/concurrency/genmc/config.rs
@@ -10,11 +10,15 @@ use crate::{IsolatedOp, MiriConfig, RejectOpWith};
 pub struct GenmcConfig {
     /// Parameters sent to the C++ side to create a new handle to the GenMC model checker.
     pub(super) params: GenmcParams,
+    pub(super) do_estimation: bool,
     /// Print the output message that GenMC generates when an error occurs.
     /// This error message is currently hard to use, since there is no clear mapping between the events that GenMC sees and the Rust code location where this event was produced.
     pub(super) print_genmc_output: bool,
     /// The log level for GenMC.
     pub(super) log_level: LogLevel,
+    /// Enable more verbose output, such as number of executions estimate
+    /// and time to completion of verification step.
+    pub(super) verbose_output: bool,
 }
 
 impl GenmcConfig {
@@ -57,8 +61,21 @@ impl GenmcConfig {
                         "Invalid suffix to GenMC argument '-Zmiri-genmc-print-exec-graphs', expected '', '=none', '=explored', '=blocked' or '=all'"
                     )),
             }
+        } else if trimmed_arg == "estimate" {
+            // FIXME(genmc): should this be on by default (like for GenMC)?
+            // Enable estimating the execution space and require time before running the actual verification.
+            genmc_config.do_estimation = true;
+        } else if let Some(estimation_max_str) = trimmed_arg.strip_prefix("estimation-max=") {
+            // Set the maximum number of executions to explore during estimation.
+            genmc_config.params.estimation_max = estimation_max_str.parse().ok().filter(|estimation_max| *estimation_max > 0).ok_or_else(|| {
+                format!(
+                    "'-Zmiri-genmc-estimation-max=...' expects a positive integer argument, but got '{estimation_max_str}'"
+                )
+            })?;
         } else if trimmed_arg == "print-genmc-output" {
             genmc_config.print_genmc_output = true;
+        } else if trimmed_arg == "verbose" {
+            genmc_config.verbose_output = true;
         } else {
             return Err(format!("Invalid GenMC argument: \"-Zmiri-genmc-{trimmed_arg}\""));
         }
diff --git a/src/tools/miri/src/concurrency/genmc/dummy.rs b/src/tools/miri/src/concurrency/genmc/dummy.rs
index 92b34b83ee0..c28984cef35 100644
--- a/src/tools/miri/src/concurrency/genmc/dummy.rs
+++ b/src/tools/miri/src/concurrency/genmc/dummy.rs
@@ -39,18 +39,6 @@ mod run {
 impl GenmcCtx {
     // We don't provide the `new` function in the dummy module.
 
-    pub fn get_blocked_execution_count(&self) -> usize {
-        unreachable!()
-    }
-
-    pub fn get_explored_execution_count(&self) -> usize {
-        unreachable!()
-    }
-
-    pub fn is_exploration_done(&self) -> bool {
-        unreachable!()
-    }
-
     /**** Memory access handling ****/
 
     pub(super) fn set_ongoing_action_data_race_free(&self, _enable: bool) {
diff --git a/src/tools/miri/src/concurrency/genmc/mod.rs b/src/tools/miri/src/concurrency/genmc/mod.rs
index 7270c668106..0086d3f2bf0 100644
--- a/src/tools/miri/src/concurrency/genmc/mod.rs
+++ b/src/tools/miri/src/concurrency/genmc/mod.rs
@@ -2,8 +2,8 @@ use std::cell::{Cell, RefCell};
 use std::sync::Arc;
 
 use genmc_sys::{
-    GENMC_GLOBAL_ADDRESSES_MASK, GenmcScalar, MemOrdering, MiriGenmcShim, RMWBinOp, UniquePtr,
-    create_genmc_driver_handle,
+    EstimationResult, GENMC_GLOBAL_ADDRESSES_MASK, GenmcScalar, MemOrdering, MiriGenmcShim,
+    RMWBinOp, UniquePtr, create_genmc_driver_handle,
 };
 use rustc_abi::{Align, Size};
 use rustc_const_eval::interpret::{AllocId, InterpCx, InterpResult, interp_ok};
@@ -16,6 +16,7 @@ use self::helper::{
     MAX_ACCESS_SIZE, Warnings, emit_warning, genmc_scalar_to_scalar,
     maybe_upgrade_compare_exchange_success_orderings, scalar_to_genmc_scalar, to_genmc_rmw_op,
 };
+use self::run::GenmcMode;
 use self::thread_id_map::ThreadIdMap;
 use crate::concurrency::genmc::helper::split_access;
 use crate::intrinsics::AtomicRmwOp;
@@ -37,6 +38,16 @@ pub use genmc_sys::GenmcParams;
 pub use self::config::GenmcConfig;
 pub use self::run::run_genmc_mode;
 
+#[derive(Debug)]
+pub enum ExecutionEndResult {
+    /// An error occurred at the end of the execution.
+    Error(String),
+    /// No errors occurred, and there are more executions to explore.
+    Continue,
+    /// No errors occurred and we are finished.
+    Stop,
+}
+
 #[derive(Clone, Copy, Debug)]
 pub enum ExitType {
     MainThreadFinish,
@@ -128,26 +139,33 @@ pub struct GenmcCtx {
 /// GenMC Context creation and administrative / query actions
 impl GenmcCtx {
     /// Create a new `GenmcCtx` from a given config.
-    fn new(miri_config: &MiriConfig, global_state: Arc<GlobalState>) -> Self {
+    fn new(miri_config: &MiriConfig, global_state: Arc<GlobalState>, mode: GenmcMode) -> Self {
         let genmc_config = miri_config.genmc_config.as_ref().unwrap();
-        let handle =
-            RefCell::new(create_genmc_driver_handle(&genmc_config.params, genmc_config.log_level));
+        let handle = RefCell::new(create_genmc_driver_handle(
+            &genmc_config.params,
+            genmc_config.log_level,
+            /* do_estimation: */ mode == GenmcMode::Estimation,
+        ));
         Self { handle, exec_state: Default::default(), global_state }
     }
 
+    fn get_estimation_results(&self) -> EstimationResult {
+        self.handle.borrow().get_estimation_results()
+    }
+
     /// Get the number of blocked executions encountered by GenMC.
-    pub fn get_blocked_execution_count(&self) -> u64 {
+    fn get_blocked_execution_count(&self) -> u64 {
         self.handle.borrow().get_blocked_execution_count()
     }
 
     /// Get the number of explored executions encountered by GenMC.
-    pub fn get_explored_execution_count(&self) -> u64 {
+    fn get_explored_execution_count(&self) -> u64 {
         self.handle.borrow().get_explored_execution_count()
     }
 
     /// Check if GenMC encountered an error that wasn't immediately returned during execution.
     /// Returns a string representation of the error if one occurred.
-    pub fn try_get_error(&self) -> Option<String> {
+    fn try_get_error(&self) -> Option<String> {
         self.handle
             .borrow()
             .get_error_string()
@@ -157,7 +175,7 @@ impl GenmcCtx {
 
     /// Check if GenMC encountered an error that wasn't immediately returned during execution.
     /// Returns a string representation of the error if one occurred.
-    pub fn get_result_message(&self) -> String {
+    fn get_result_message(&self) -> String {
         self.handle
             .borrow()
             .get_result_message()
@@ -166,13 +184,6 @@ impl GenmcCtx {
             .expect("there should always be a message")
     }
 
-    /// This function determines if we should continue exploring executions or if we are done.
-    ///
-    /// In GenMC mode, the input program should be repeatedly executed until this function returns `true` or an error is found.
-    pub fn is_exploration_done(&self) -> bool {
-        self.handle.borrow_mut().pin_mut().is_exploration_done()
-    }
-
     /// Select whether data race free actions should be allowed. This function should be used carefully!
     ///
     /// If `true` is passed, allow for data races to happen without triggering an error, until this function is called again with argument `false`.
@@ -218,13 +229,25 @@ impl GenmcCtx {
     /// This function will also check for those, and return their error description.
     ///
     /// To get the all messages (warnings, errors) that GenMC produces, use the `get_result_message` method.
-    fn handle_execution_end(&self) -> Option<String> {
+    fn handle_execution_end(&self) -> ExecutionEndResult {
         let result = self.handle.borrow_mut().pin_mut().handle_execution_end();
-        result.as_ref().map(|msg| msg.to_string_lossy().to_string())?;
+        if let Some(error) = result.as_ref() {
+            return ExecutionEndResult::Error(error.to_string_lossy().to_string());
+        }
+
+        // GenMC decides if there is more to explore:
+        let exploration_done = self.handle.borrow_mut().pin_mut().is_exploration_done();
 
         // GenMC currently does not return an error value immediately in all cases.
+        // Both `handle_execution_end` and `is_exploration_done` can produce such errors.
         // We manually query for any errors here to ensure we don't miss any.
-        self.try_get_error()
+        if let Some(error) = self.try_get_error() {
+            ExecutionEndResult::Error(error)
+        } else if exploration_done {
+            ExecutionEndResult::Stop
+        } else {
+            ExecutionEndResult::Continue
+        }
     }
 
     /**** Memory access handling ****/
diff --git a/src/tools/miri/src/concurrency/genmc/run.rs b/src/tools/miri/src/concurrency/genmc/run.rs
index 7e4ed816a76..bc2f5f7b79e 100644
--- a/src/tools/miri/src/concurrency/genmc/run.rs
+++ b/src/tools/miri/src/concurrency/genmc/run.rs
@@ -1,32 +1,65 @@
 use std::rc::Rc;
 use std::sync::Arc;
+use std::time::Instant;
 
+use genmc_sys::EstimationResult;
 use rustc_middle::ty::TyCtxt;
 
 use super::GlobalState;
+use crate::concurrency::genmc::ExecutionEndResult;
 use crate::rustc_const_eval::interpret::PointerArithmetic;
-use crate::{GenmcCtx, MiriConfig};
+use crate::{GenmcConfig, GenmcCtx, MiriConfig};
+
+#[derive(Clone, Copy, PartialEq, Eq)]
+pub(super) enum GenmcMode {
+    Estimation,
+    Verification,
+}
+
+impl GenmcMode {
+    /// Return whether warnings on unsupported features should be printed in this mode.
+    fn print_unsupported_warnings(self) -> bool {
+        self == GenmcMode::Verification
+    }
+}
 
 /// Do a complete run of the program in GenMC mode.
 /// This will call `eval_entry` multiple times, until either:
 /// - An error is detected (indicated by a `None` return value)
 /// - All possible executions are explored.
 ///
-/// FIXME(genmc): add estimation mode setting.
+/// Returns `None` is an error is detected, or `Some(return_value)` with the return value of the last run of the program.
 pub fn run_genmc_mode<'tcx>(
     config: &MiriConfig,
     eval_entry: impl Fn(Rc<GenmcCtx>) -> Option<i32>,
     tcx: TyCtxt<'tcx>,
 ) -> Option<i32> {
     let genmc_config = config.genmc_config.as_ref().unwrap();
+    // Run in Estimation mode if requested.
+    if genmc_config.do_estimation {
+        eprintln!("Estimating GenMC verification time...");
+        run_genmc_mode_impl(config, &eval_entry, tcx, GenmcMode::Estimation)?;
+    }
+    // Run in Verification mode.
+    eprintln!("Running GenMC Verification...");
+    run_genmc_mode_impl(config, &eval_entry, tcx, GenmcMode::Verification)
+}
+
+fn run_genmc_mode_impl<'tcx>(
+    config: &MiriConfig,
+    eval_entry: &impl Fn(Rc<GenmcCtx>) -> Option<i32>,
+    tcx: TyCtxt<'tcx>,
+    mode: GenmcMode,
+) -> Option<i32> {
+    let time_start = Instant::now();
+    let genmc_config = config.genmc_config.as_ref().unwrap();
 
     // There exists only one `global_state` per full run in GenMC mode.
     // It is shared by all `GenmcCtx` in this run.
     // FIXME(genmc): implement multithreading once GenMC supports it.
-    // FIXME(genmc): disable warnings in estimation mode once it is added.
     let global_state =
-        Arc::new(GlobalState::new(tcx.target_usize_max(), /* print_warnings */ true));
-    let genmc_ctx = Rc::new(GenmcCtx::new(config, global_state));
+        Arc::new(GlobalState::new(tcx.target_usize_max(), mode.print_unsupported_warnings()));
+    let genmc_ctx = Rc::new(GenmcCtx::new(config, global_state, mode));
 
     // `rep` is used to report the progress, Miri will panic on wrap-around.
     for rep in 0u64.. {
@@ -37,46 +70,97 @@ pub fn run_genmc_mode<'tcx>(
 
         // Execute the program until completion to get the return value, or return if an error happens:
         let Some(return_code) = eval_entry(genmc_ctx.clone()) else {
-            // If requested, print the output GenMC produced:
-            if genmc_config.print_genmc_output {
-                eprintln!("== raw GenMC output =========================");
-                eprintln!("{}", genmc_ctx.get_result_message());
-                eprintln!("== end of raw GenMC output ==================");
-            }
+            genmc_ctx.print_genmc_output(genmc_config);
             return None;
         };
 
-        // We inform GenMC that the execution is complete. If there was an error, we print it.
-        if let Some(error) = genmc_ctx.handle_execution_end() {
-            // This can be reached for errors that affect the entire execution, not just a specific event.
-            // For instance, linearizability checking and liveness checking report their errors this way.
-            // Neither are supported by Miri-GenMC at the moment though. However, GenMC also
-            // treats races on deallocation as global errors, so this code path is still reachable.
-            // Since we don't have any span information for the error at this point,
-            // we just print GenMC's error message.
-            eprintln!("(GenMC) Error detected: {error}");
-            eprintln!();
-            eprintln!("{}", genmc_ctx.get_result_message());
-            return None;
+        // We inform GenMC that the execution is complete.
+        // If there was an error, we print it.
+        match genmc_ctx.handle_execution_end() {
+            ExecutionEndResult::Continue => continue,
+            ExecutionEndResult::Stop => {
+                let elapsed_time_sec = Instant::now().duration_since(time_start).as_secs_f64();
+                // Print the output for the current mode.
+                if mode == GenmcMode::Estimation {
+                    genmc_ctx.print_estimation_output(genmc_config, elapsed_time_sec);
+                } else {
+                    genmc_ctx.print_verification_output(genmc_config, elapsed_time_sec);
+                }
+                // Return the return code of the last execution.
+                return Some(return_code);
+            }
+            ExecutionEndResult::Error(error) => {
+                // This can be reached for errors that affect the entire execution, not just a specific event.
+                // For instance, linearizability checking and liveness checking report their errors this way.
+                // Neither are supported by Miri-GenMC at the moment though. However, GenMC also
+                // treats races on deallocation as global errors, so this code path is still reachable.
+                // Since we don't have any span information for the error at this point,
+                // we just print GenMC's error string, and the full GenMC output if requested.
+                eprintln!("(GenMC) Error detected: {error}");
+                genmc_ctx.print_genmc_output(genmc_config);
+                return None;
+            }
         }
+    }
+    unreachable!()
+}
 
-        // Check if we've explored enough executions:
-        if !genmc_ctx.is_exploration_done() {
-            continue;
+impl GenmcCtx {
+    /// Print the full output message produced by GenMC if requested, or a hint on how to enable it.
+    ///
+    /// This message can be very verbose and is likely not useful for the average user.
+    /// This function should be called *after* Miri has printed all of its output.
+    fn print_genmc_output(&self, genmc_config: &GenmcConfig) {
+        if genmc_config.print_genmc_output {
+            eprintln!("GenMC error report:");
+            eprintln!("{}", self.get_result_message());
+        } else {
+            eprintln!(
+                "(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)"
+            );
         }
+    }
 
-        eprintln!("(GenMC) Verification complete. No errors were detected.");
-
-        let explored_execution_count = genmc_ctx.get_explored_execution_count();
-        let blocked_execution_count = genmc_ctx.get_blocked_execution_count();
+    /// Given the time taken for the estimation mode run, print the expected time range for verification.
+    /// Verbose output also includes information about the expected number of executions and how many estimation rounds were explored or got blocked.
+    fn print_estimation_output(&self, genmc_config: &GenmcConfig, elapsed_time_sec: f64) {
+        let EstimationResult { mean, sd, explored_execs, blocked_execs } =
+            self.get_estimation_results();
+        #[allow(clippy::as_conversions)]
+        let time_per_exec_sec = elapsed_time_sec / (explored_execs as f64 + blocked_execs as f64);
+        let estimated_mean_sec = time_per_exec_sec * mean;
+        let estimated_sd_sec = time_per_exec_sec * sd;
 
-        eprintln!("Number of complete executions explored: {explored_execution_count}");
-        if blocked_execution_count > 0 {
-            eprintln!("Number of blocked executions seen: {blocked_execution_count}");
+        if genmc_config.verbose_output {
+            eprintln!("Finished estimation in {elapsed_time_sec:.2?}s");
+            if blocked_execs != 0 {
+                eprintln!("  Explored executions: {explored_execs}");
+                eprintln!("  Blocked  executions: {blocked_execs}");
+            }
+            eprintln!("Expected number of executions: {mean:.0} ± {sd:.0}");
+        }
+        // The estimation can be out-of-bounds of an `f64`.
+        if !(mean.is_finite() && mean >= 0.0 && sd.is_finite() && sd >= 0.0) {
+            eprintln!("WARNING: Estimation gave weird results, there may have been an overflow.");
         }
+        eprintln!("Expected verification time: {estimated_mean_sec:.2}s ± {estimated_sd_sec:.2}s");
+    }
 
-        // Return the return code of the last execution.
-        return Some(return_code);
+    /// Given the time taken for the verification mode run, print the expected time range for verification.
+    /// Verbose output also includes information about the expected number of executions and how many estimation rounds were explored or got blocked.
+    fn print_verification_output(&self, genmc_config: &GenmcConfig, elapsed_time_sec: f64) {
+        let explored_execution_count = self.get_explored_execution_count();
+        let blocked_execution_count = self.get_blocked_execution_count();
+        eprintln!(
+            "Verification complete with {} executions. No errors found.",
+            explored_execution_count + blocked_execution_count
+        );
+        if genmc_config.verbose_output {
+            if blocked_execution_count > 0 {
+                eprintln!("Number of complete executions explored: {explored_execution_count}");
+                eprintln!("Number of blocked executions seen: {blocked_execution_count}");
+            }
+            eprintln!("Verification took {elapsed_time_sec:.2?}s.");
+        }
     }
-    unreachable!()
 }
diff --git a/src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.stderr b/src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.stderr
index 946d9a2124b..00de74009d9 100644
--- a/src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.stderr
+++ b/src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 error: Undefined Behavior: Non-atomic race
   --> tests/genmc/fail/data_race/mpu2_rels_rlx.rs:LL:CC
    |
@@ -15,5 +16,6 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/f
 LL |         f();
    |         ^^^
 
+(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
 error: aborting due to 1 previous error
 
diff --git a/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rel_rlx.stderr b/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rel_rlx.stderr
index 121ded2a181..501957a90d3 100644
--- a/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rel_rlx.stderr
+++ b/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rel_rlx.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 error: Undefined Behavior: Non-atomic race
   --> tests/genmc/fail/data_race/weak_orderings.rs:LL:CC
    |
@@ -15,5 +16,6 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/f
 LL |         f();
    |         ^^^
 
+(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
 error: aborting due to 1 previous error
 
diff --git a/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_acq.stderr b/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_acq.stderr
index 121ded2a181..501957a90d3 100644
--- a/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_acq.stderr
+++ b/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_acq.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 error: Undefined Behavior: Non-atomic race
   --> tests/genmc/fail/data_race/weak_orderings.rs:LL:CC
    |
@@ -15,5 +16,6 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/f
 LL |         f();
    |         ^^^
 
+(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
 error: aborting due to 1 previous error
 
diff --git a/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_rlx.stderr b/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_rlx.stderr
index 121ded2a181..501957a90d3 100644
--- a/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_rlx.stderr
+++ b/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_rlx.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 error: Undefined Behavior: Non-atomic race
   --> tests/genmc/fail/data_race/weak_orderings.rs:LL:CC
    |
@@ -15,5 +16,6 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/f
 LL |         f();
    |         ^^^
 
+(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
 error: aborting due to 1 previous error
 
diff --git a/src/tools/miri/tests/genmc/fail/loom/buggy_inc.stderr b/src/tools/miri/tests/genmc/fail/loom/buggy_inc.stderr
index 5a8948ff9b4..9c3ba1d4c59 100644
--- a/src/tools/miri/tests/genmc/fail/loom/buggy_inc.stderr
+++ b/src/tools/miri/tests/genmc/fail/loom/buggy_inc.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 error: abnormal termination: the program aborted execution
   --> tests/genmc/fail/loom/buggy_inc.rs:LL:CC
    |
@@ -9,5 +10,6 @@ LL |             std::process::abort();
 
 note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
 
+(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
 error: aborting due to 1 previous error
 
diff --git a/src/tools/miri/tests/genmc/fail/loom/store_buffering.genmc.stderr b/src/tools/miri/tests/genmc/fail/loom/store_buffering.genmc.stderr
index a6c3ed7055e..db92d0573fa 100644
--- a/src/tools/miri/tests/genmc/fail/loom/store_buffering.genmc.stderr
+++ b/src/tools/miri/tests/genmc/fail/loom/store_buffering.genmc.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 error: abnormal termination: the program aborted execution
   --> tests/genmc/fail/loom/store_buffering.rs:LL:CC
    |
@@ -9,5 +10,6 @@ LL |             std::process::abort();
 
 note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
 
+(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
 error: aborting due to 1 previous error
 
diff --git a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.relaxed4.stderr b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.relaxed4.stderr
index cbfb6ec833e..773f86a9759 100644
--- a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.relaxed4.stderr
+++ b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.relaxed4.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 error: abnormal termination: the program aborted execution
   --> tests/genmc/fail/simple/2w2w_weak.rs:LL:CC
    |
@@ -9,5 +10,6 @@ LL |             std::process::abort();
 
 note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
 
+(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
 error: aborting due to 1 previous error
 
diff --git a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.release4.stderr b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.release4.stderr
index cbfb6ec833e..773f86a9759 100644
--- a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.release4.stderr
+++ b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.release4.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 error: abnormal termination: the program aborted execution
   --> tests/genmc/fail/simple/2w2w_weak.rs:LL:CC
    |
@@ -9,5 +10,6 @@ LL |             std::process::abort();
 
 note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
 
+(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
 error: aborting due to 1 previous error
 
diff --git a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.sc3_rel1.stderr b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.sc3_rel1.stderr
index cbfb6ec833e..773f86a9759 100644
--- a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.sc3_rel1.stderr
+++ b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.sc3_rel1.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 error: abnormal termination: the program aborted execution
   --> tests/genmc/fail/simple/2w2w_weak.rs:LL:CC
    |
@@ -9,5 +10,6 @@ LL |             std::process::abort();
 
 note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
 
+(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
 error: aborting due to 1 previous error
 
diff --git a/src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.stderr b/src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.stderr
index d97b8b3d92f..31438f9352f 100644
--- a/src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.stderr
+++ b/src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 warning: GenMC currently does not model the failure ordering for `compare_exchange`. Success ordering 'Release' was upgraded to 'AcqRel' to match failure ordering 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
   --> tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.rs:LL:CC
    |
@@ -18,5 +19,4 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/p
 LL |         f();
    |         ^^^
 
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 2
+Verification complete with 2 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/atomics/cas_simple.stderr b/src/tools/miri/tests/genmc/pass/atomics/cas_simple.stderr
index 3b22247ee44..7867be2dbe8 100644
--- a/src/tools/miri/tests/genmc/pass/atomics/cas_simple.stderr
+++ b/src/tools/miri/tests/genmc/pass/atomics/cas_simple.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 1
+Running GenMC Verification...
+Verification complete with 1 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.stderr b/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.stderr
index 3b22247ee44..7867be2dbe8 100644
--- a/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.stderr
+++ b/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 1
+Running GenMC Verification...
+Verification complete with 1 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/2cowr.stderr b/src/tools/miri/tests/genmc/pass/litmus/2cowr.stderr
index 0667962f99c..a67635dee1b 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/2cowr.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/2cowr.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 4
+Running GenMC Verification...
+Verification complete with 4 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/2w2w_2sc_scf.stderr b/src/tools/miri/tests/genmc/pass/litmus/2w2w_2sc_scf.stderr
index 115b1986ce5..485142e945a 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/2w2w_2sc_scf.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/2w2w_2sc_scf.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 3
+Running GenMC Verification...
+Verification complete with 3 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/2w2w_3sc_1rel.release1.stderr b/src/tools/miri/tests/genmc/pass/litmus/2w2w_3sc_1rel.release1.stderr
index 0667962f99c..a67635dee1b 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/2w2w_3sc_1rel.release1.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/2w2w_3sc_1rel.release1.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 4
+Running GenMC Verification...
+Verification complete with 4 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/2w2w_3sc_1rel.release2.stderr b/src/tools/miri/tests/genmc/pass/litmus/2w2w_3sc_1rel.release2.stderr
index 0667962f99c..a67635dee1b 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/2w2w_3sc_1rel.release2.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/2w2w_3sc_1rel.release2.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 4
+Running GenMC Verification...
+Verification complete with 4 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.sc.stderr b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.sc.stderr
index 115b1986ce5..485142e945a 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.sc.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.sc.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 3
+Running GenMC Verification...
+Verification complete with 3 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.weak.stderr b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.weak.stderr
index 0667962f99c..a67635dee1b 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.weak.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.weak.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 4
+Running GenMC Verification...
+Verification complete with 4 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/2w2w_4sc.stderr b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4sc.stderr
index 115b1986ce5..485142e945a 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/2w2w_4sc.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4sc.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 3
+Running GenMC Verification...
+Verification complete with 3 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/IRIW-acq-sc.stderr b/src/tools/miri/tests/genmc/pass/litmus/IRIW-acq-sc.stderr
index c760b446051..d6ec73a8c66 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/IRIW-acq-sc.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/IRIW-acq-sc.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 16
+Running GenMC Verification...
+Verification complete with 16 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/IRIWish.stderr b/src/tools/miri/tests/genmc/pass/litmus/IRIWish.stderr
index 4fc77b63f38..7ea2dd50851 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/IRIWish.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/IRIWish.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 [1, 1, 1, 1, 1]
 [1, 1, 1, 0, 1]
 [1, 1, 1, 0, 0]
@@ -26,5 +27,4 @@
 [0, 0, 0, 0, 0]
 [0, 0, 0, 0, 1]
 [0, 0, 0, 0, 0]
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 28
+Verification complete with 28 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/LB.stderr b/src/tools/miri/tests/genmc/pass/litmus/LB.stderr
index 115b1986ce5..485142e945a 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/LB.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/LB.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 3
+Running GenMC Verification...
+Verification complete with 3 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/LB_incMPs.stderr b/src/tools/miri/tests/genmc/pass/litmus/LB_incMPs.stderr
index c879e95a170..e414cd5e064 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/LB_incMPs.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/LB_incMPs.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 15
+Running GenMC Verification...
+Verification complete with 15 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/MP.stderr b/src/tools/miri/tests/genmc/pass/litmus/MP.stderr
index 115b1986ce5..485142e945a 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/MP.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/MP.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 3
+Running GenMC Verification...
+Verification complete with 3 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.stderr b/src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.stderr
index 4551c00b057..29b59ce3bc1 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 X=1, Y=2, a=Err(1), b=Ok(1), c=2
 X=1, Y=2, a=Err(1), b=Ok(1), c=1
 X=1, Y=2, a=Err(1), b=Ok(1), c=0
@@ -34,5 +35,4 @@ X=1, Y=1, a=Err(0), b=Err(0), c=0
 X=1, Y=1, a=Err(0), b=Err(0), c=1
 X=1, Y=1, a=Err(0), b=Err(0), c=0
 X=1, Y=1, a=Err(0), b=Err(0), c=0
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 36
+Verification complete with 36 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/MPU_rels_acq.stderr b/src/tools/miri/tests/genmc/pass/litmus/MPU_rels_acq.stderr
index c5e34b00642..423ee6dc399 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/MPU_rels_acq.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/MPU_rels_acq.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 13
+Running GenMC Verification...
+Verification complete with 13 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/MP_incMPs.stderr b/src/tools/miri/tests/genmc/pass/litmus/MP_incMPs.stderr
index 2be9a6c7fbd..f527b612023 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/MP_incMPs.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/MP_incMPs.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 7
+Running GenMC Verification...
+Verification complete with 7 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/MP_rels_acqf.stderr b/src/tools/miri/tests/genmc/pass/litmus/MP_rels_acqf.stderr
index 0667962f99c..a67635dee1b 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/MP_rels_acqf.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/MP_rels_acqf.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 4
+Running GenMC Verification...
+Verification complete with 4 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/SB.stderr b/src/tools/miri/tests/genmc/pass/litmus/SB.stderr
index 0667962f99c..a67635dee1b 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/SB.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/SB.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 4
+Running GenMC Verification...
+Verification complete with 4 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/SB_2sc_scf.stderr b/src/tools/miri/tests/genmc/pass/litmus/SB_2sc_scf.stderr
index 115b1986ce5..485142e945a 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/SB_2sc_scf.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/SB_2sc_scf.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 3
+Running GenMC Verification...
+Verification complete with 3 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/Z6_U.sc.stderr b/src/tools/miri/tests/genmc/pass/litmus/Z6_U.sc.stderr
index 8dd2fbe1b97..c8fbb8951a3 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/Z6_U.sc.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/Z6_U.sc.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 a=2, b=1, X=1, Y=3
 a=4, b=1, X=1, Y=4
 a=3, b=1, X=1, Y=3
@@ -16,5 +17,4 @@ a=3, b=0, X=1, Y=1
 a=1, b=1, X=1, Y=3
 a=1, b=1, X=1, Y=1
 a=1, b=0, X=1, Y=1
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 18
+Verification complete with 18 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/Z6_U.weak.stderr b/src/tools/miri/tests/genmc/pass/litmus/Z6_U.weak.stderr
index 65622575de2..72c59d33f77 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/Z6_U.weak.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/Z6_U.weak.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 a=2, b=1, X=1, Y=3
 a=4, b=1, X=1, Y=4
 a=4, b=0, X=1, Y=4
@@ -20,5 +21,4 @@ a=1, b=1, X=1, Y=3
 a=1, b=0, X=1, Y=3
 a=1, b=1, X=1, Y=1
 a=1, b=0, X=1, Y=1
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 22
+Verification complete with 22 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/Z6_acq.stderr b/src/tools/miri/tests/genmc/pass/litmus/Z6_acq.stderr
index 2be9a6c7fbd..f527b612023 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/Z6_acq.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/Z6_acq.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 7
+Running GenMC Verification...
+Verification complete with 7 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/atomicpo.stderr b/src/tools/miri/tests/genmc/pass/litmus/atomicpo.stderr
index 0667962f99c..a67635dee1b 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/atomicpo.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/atomicpo.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 4
+Running GenMC Verification...
+Verification complete with 4 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/casdep.stderr b/src/tools/miri/tests/genmc/pass/litmus/casdep.stderr
index 01701dfe691..bde951866d0 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/casdep.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/casdep.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 2
+Running GenMC Verification...
+Verification complete with 2 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/ccr.stderr b/src/tools/miri/tests/genmc/pass/litmus/ccr.stderr
index 01701dfe691..bde951866d0 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/ccr.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/ccr.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 2
+Running GenMC Verification...
+Verification complete with 2 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/cii.stderr b/src/tools/miri/tests/genmc/pass/litmus/cii.stderr
index be75e68fde7..b9bdf2245ae 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/cii.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/cii.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 6
+Running GenMC Verification...
+Verification complete with 6 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/corr.stderr b/src/tools/miri/tests/genmc/pass/litmus/corr.stderr
index be75e68fde7..b9bdf2245ae 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/corr.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/corr.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 6
+Running GenMC Verification...
+Verification complete with 6 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/corr0.stderr b/src/tools/miri/tests/genmc/pass/litmus/corr0.stderr
index 0667962f99c..a67635dee1b 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/corr0.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/corr0.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 4
+Running GenMC Verification...
+Verification complete with 4 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/corr1.stderr b/src/tools/miri/tests/genmc/pass/litmus/corr1.stderr
index f6d07e9c77b..384425fc43c 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/corr1.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/corr1.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 36
+Running GenMC Verification...
+Verification complete with 36 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/corr2.stderr b/src/tools/miri/tests/genmc/pass/litmus/corr2.stderr
index 78a90b63fea..07fd2d4de18 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/corr2.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/corr2.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 72
+Running GenMC Verification...
+Verification complete with 72 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/corw.stderr b/src/tools/miri/tests/genmc/pass/litmus/corw.stderr
index 115b1986ce5..485142e945a 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/corw.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/corw.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 3
+Running GenMC Verification...
+Verification complete with 3 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/cowr.stderr b/src/tools/miri/tests/genmc/pass/litmus/cowr.stderr
index 115b1986ce5..485142e945a 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/cowr.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/cowr.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 3
+Running GenMC Verification...
+Verification complete with 3 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/cumul-release.stderr b/src/tools/miri/tests/genmc/pass/litmus/cumul-release.stderr
index 00394048ec5..a031dfc8977 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/cumul-release.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/cumul-release.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 8
+Running GenMC Verification...
+Verification complete with 8 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/default.stderr b/src/tools/miri/tests/genmc/pass/litmus/default.stderr
index e0313930282..87d38d25041 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/default.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/default.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 12
+Running GenMC Verification...
+Verification complete with 12 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/detour.join.stderr b/src/tools/miri/tests/genmc/pass/litmus/detour.join.stderr
index 15017249dc3..5006f11fefb 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/detour.join.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/detour.join.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 9
+Running GenMC Verification...
+Verification complete with 9 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/detour.no_join.stderr b/src/tools/miri/tests/genmc/pass/litmus/detour.no_join.stderr
index 15017249dc3..5006f11fefb 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/detour.no_join.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/detour.no_join.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 9
+Running GenMC Verification...
+Verification complete with 9 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/fr_w_w_w_reads.stderr b/src/tools/miri/tests/genmc/pass/litmus/fr_w_w_w_reads.stderr
index 3b6ba238f53..c09b50e282f 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/fr_w_w_w_reads.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/fr_w_w_w_reads.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 210
+Running GenMC Verification...
+Verification complete with 210 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/inc2w.stderr b/src/tools/miri/tests/genmc/pass/litmus/inc2w.stderr
index be75e68fde7..b9bdf2245ae 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/inc2w.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/inc2w.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 6
+Running GenMC Verification...
+Verification complete with 6 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/inc_inc_RR_W_RR.stderr b/src/tools/miri/tests/genmc/pass/litmus/inc_inc_RR_W_RR.stderr
index b5f8cd15b68..770fb7ef880 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/inc_inc_RR_W_RR.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/inc_inc_RR_W_RR.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 600
+Running GenMC Verification...
+Verification complete with 600 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/riwi.stderr b/src/tools/miri/tests/genmc/pass/litmus/riwi.stderr
index 115b1986ce5..485142e945a 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/riwi.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/riwi.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 3
+Running GenMC Verification...
+Verification complete with 3 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.rs b/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.rs
index a193dcf0683..3256c9f4211 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.rs
+++ b/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.rs
@@ -1,6 +1,8 @@
-//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows -Zmiri-genmc-estimate
 
 // Translated from GenMC's "litmus/viktor-relseq" test.
+//
+// This test also checks that we can run the GenMC estimation mode.
 
 #![no_main]
 
diff --git a/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.stderr b/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.stderr
index d63ac5199d5..c53d5c569b9 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.stderr
@@ -1,2 +1,4 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 180
+Estimating GenMC verification time...
+Expected verification time: [MEAN] ± [SD]
+Running GenMC Verification...
+Verification complete with 180 executions. No errors found.
diff --git a/src/tools/miri/tests/ui.rs b/src/tools/miri/tests/ui.rs
index b7286d9a367..efaaf9fc841 100644
--- a/src/tools/miri/tests/ui.rs
+++ b/src/tools/miri/tests/ui.rs
@@ -277,6 +277,8 @@ regexes! {
     r"\bsys/([a-z_]+)/[a-z]+\b"     => "sys/$1/PLATFORM",
     // erase paths into the crate registry
     r"[^ ]*/\.?cargo/registry/.*/(.*\.rs)"  => "CARGO_REGISTRY/.../$1",
+    // remove time print from GenMC estimation mode output.
+    "\nExpected verification time: .* ± .*" => "\nExpected verification time: [MEAN] ± [SD]",
 }
 
 enum Dependencies {
-- 
cgit 1.4.1-3-g733a5