Merge pull request #4578 from Patrick-6/miri-genmc-cas

Add compare_exchange support for GenMC mode

27 files changed, 850 insertions, 54 deletions

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