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>

58 files changed, 1431 insertions, 136 deletions

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.weak.stderr
index 0667962f99c..0667962f99c 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.weak.stderr
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));