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

Add compare_exchange support for GenMC mode

Author: RalfJung

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 */

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)

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));
 

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,

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,