Add support for temporal mixing of atomic and non-atomic accesses in GenMC mode

genmc-sys/build.rs

@@ -28,7 +28,7 @@ mod downloading {
     /// The GenMC repository the we get our commit from.
     pub(crate) const GENMC_GITHUB_URL: &str = "https://gitlab.inf.ethz.ch/public-plf/genmc.git";
     /// The GenMC commit we depend on. It must be available on the specified GenMC repository.
-    pub(crate) const GENMC_COMMIT: &str = "cd01c12032bdd71df742b41c7817f99acc72e7ab";
+    pub(crate) const GENMC_COMMIT: &str = "ce775ccd7866db820fa12ffca66463087a11dd96";
 
     /// 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.

genmc-sys/cpp/include/MiriInterface.hpp

@@ -214,9 +214,10 @@ struct MiriGenmcShim : private GenMCDriver {
      * Automatically calls `inc_pos` and `dec_pos` where needed for the given thread.
      */
     template <EventLabel::EventLabelKind k, typename... Ts>
-    auto handle_load_reset_if_none(ThreadId tid, Ts&&... params) -> HandleResult<SVal> {
+    auto handle_load_reset_if_none(ThreadId tid, std::optional<SVal> old_val, Ts&&... params)
+        -> HandleResult<SVal> {
         const auto pos = inc_pos(tid);
-        const auto ret = GenMCDriver::handleLoad<k>(pos, std::forward<Ts>(params)...);
+        const auto ret = GenMCDriver::handleLoad<k>(pos, old_val, std::forward<Ts>(params)...);
         // If we didn't get a value, we have to reset the index of the current thread.
         if (!std::holds_alternative<SVal>(ret)) {
             dec_pos(tid);
@@ -274,6 +275,12 @@ inline SVal to_sval(GenmcScalar scalar) {
     ERROR_ON(!scalar.is_init, "Cannot convert an uninitialized `GenmcScalar` into an `SVal`\n");
     return SVal(scalar.value, scalar.extra);
 }
+
+inline std::optional<SVal> try_to_sval(GenmcScalar scalar) {
+    if (scalar.is_init)
+        return { SVal(scalar.value, scalar.extra) };
+    return std::nullopt;
+}
 } // namespace GenmcScalarExt
 
 namespace LoadResultExt {

genmc-sys/cpp/src/MiriInterface/EventHandling.cpp

@@ -49,6 +49,7 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id) {
     const auto type = AType::Unsigned;
     const auto ret = handle_load_reset_if_none<EventLabel::EventLabelKind::Read>(
         thread_id,
+        GenmcScalarExt::try_to_sval(old_val),
         ord,
         SAddr(address),
         ASize(size),
@@ -74,6 +75,7 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id) {
     const auto pos = inc_pos(thread_id);
     const auto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::Write>(
         pos,
+        GenmcScalarExt::try_to_sval(old_val),
         ord,
         SAddr(address),
         ASize(size),
@@ -84,15 +86,13 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id) {
 
     if (const auto* err = std::get_if<VerificationError>(&ret))
         return StoreResultExt::from_error(format_error(*err));
-    if (!std::holds_alternative<std::monostate>(ret))
-        ERROR("store returned unexpected result");
 
-    // FIXME(genmc,mixed-accesses): Use the value that GenMC returns from handleStore (once
-    // available).
-    const auto& g = getExec().getGraph();
-    return StoreResultExt::ok(
-        /* is_coherence_order_maximal_write */ g.co_max(SAddr(address))->getPos() == pos
+    const bool* is_coherence_order_maximal_write = std::get_if<bool>(&ret);
+    ERROR_ON(
+        nullptr == is_coherence_order_maximal_write,
+        "Unimplemented: Store returned unexpected result."
     );
+    return StoreResultExt::ok(*is_coherence_order_maximal_write);
 }
 
 void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
@@ -117,6 +117,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
     // `FaiRead` and `FaiWrite`.
     const auto load_ret = handle_load_reset_if_none<EventLabel::EventLabelKind::FaiRead>(
         thread_id,
+        GenmcScalarExt::try_to_sval(old_val),
         ordering,
         SAddr(address),
         ASize(size),
@@ -139,6 +140,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
     const auto storePos = inc_pos(thread_id);
     const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::FaiWrite>(
         storePos,
+        GenmcScalarExt::try_to_sval(old_val),
         ordering,
         SAddr(address),
         ASize(size),
@@ -148,16 +150,15 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
     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();
+    const bool* is_coherence_order_maximal_write = std::get_if<bool>(&store_ret);
+    ERROR_ON(
+        nullptr == is_coherence_order_maximal_write,
+        "Unimplemented: RMW store returned unexpected result."
+    );
     return ReadModifyWriteResultExt::ok(
         /* old_value: */ read_old_val,
         new_value,
-        /* is_coherence_order_maximal_write */ g.co_max(SAddr(address))->getPos() == storePos
+        *is_coherence_order_maximal_write
     );
 }
 
@@ -183,6 +184,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
 
     const auto load_ret = handle_load_reset_if_none<EventLabel::EventLabelKind::CasRead>(
         thread_id,
+        GenmcScalarExt::try_to_sval(old_val),
         success_ordering,
         SAddr(address),
         ASize(size),
@@ -203,6 +205,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
     const auto storePos = inc_pos(thread_id);
     const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::CasWrite>(
         storePos,
+        GenmcScalarExt::try_to_sval(old_val),
         success_ordering,
         SAddr(address),
         ASize(size),
@@ -211,19 +214,12 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
     );
     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);
+    const bool* is_coherence_order_maximal_write = std::get_if<bool>(&store_ret);
     ERROR_ON(
-        nullptr == store_ret_val,
+        nullptr == is_coherence_order_maximal_write,
         "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
-    );
+    return CompareExchangeResultExt::success(read_old_val, *is_coherence_order_maximal_write);
 }
 
 /**** Memory (de)allocation ****/

tests/genmc/fail/atomics/atomic_ptr_double_free.rs

@@ -22,9 +22,6 @@ unsafe fn free(ptr: *mut u64) {
 
 #[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(std::ptr::null_mut(), SeqCst);
-
     unsafe {
         let ids = [
             spawn_pthread_closure(|| {

tests/genmc/fail/data_race/atomic_ptr_alloc_race.rs

@@ -23,9 +23,6 @@ static X: AtomicPtr<u64> = AtomicPtr::new(std::ptr::null_mut());
 
 #[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(std::ptr::null_mut(), SeqCst);
-
     unsafe {
         let ids = [
             spawn_pthread_closure(|| {

tests/genmc/fail/data_race/atomic_ptr_dealloc_write_race.rs

@@ -20,9 +20,6 @@ static mut Y: u64 = 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(std::ptr::null_mut(), SeqCst);
-
     unsafe {
         let ids = [
             spawn_pthread_closure(|| {

tests/genmc/fail/data_race/atomic_ptr_write_dealloc_race.rs

@@ -24,9 +24,6 @@ static Y: AtomicPtr<u64> = AtomicPtr::new(std::ptr::null_mut());
 
 #[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(std::ptr::null_mut(), SeqCst);
-
     unsafe {
         let ids = [
             spawn_pthread_closure(|| {

tests/genmc/fail/loom/buggy_inc.rs

@@ -42,9 +42,6 @@ impl BuggyInc {
 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();

tests/genmc/pass/atomics/atomic_ptr_ops.rs

@@ -37,46 +37,54 @@ unsafe fn pointers_equal(a: *mut u64, b: *mut u64) {
 
 unsafe fn test_load_store_exchange() {
     let atomic_ptr: AtomicPtr<u64> = AtomicPtr::new(&raw mut X);
-    // FIXME(genmc,HACK): remove this initializing write once Miri-GenMC supports mixed atomic-non-atomic accesses.
-    // FIXME(genmc): Add test cases with temporal mixing of atomics/non-atomics.
-    atomic_ptr.store(&raw mut X, SeqCst);
 
-    // Load can read the initial value.
+    // Atomic load can read the initial value.
     pointers_equal(atomic_ptr.load(SeqCst), &raw mut X);
-    // Store works as expected.
+    // Atomic store works as expected.
     atomic_ptr.store(&raw mut Y, SeqCst);
     pointers_equal(atomic_ptr.load(SeqCst), &raw mut Y);
+    // We can read the value of the atomic store non-atomically.
+    pointers_equal(*atomic_ptr.as_ptr(), &raw mut Y);
+    // We can read the value of a non-atomic store atomically.
+    *atomic_ptr.as_ptr() = &raw mut X;
+    pointers_equal(atomic_ptr.load(SeqCst), &raw mut X);
 
     // Atomic swap must return the old value and store the new one.
+    *atomic_ptr.as_ptr() = &raw mut Y; // Test that we can read this non-atomic store using `swap`.
     pointers_equal(atomic_ptr.swap(&raw mut X, SeqCst), &raw mut Y);
+    pointers_equal(*atomic_ptr.as_ptr(), &raw mut X);
     pointers_equal(atomic_ptr.load(SeqCst), &raw mut X);
 
     // Failing compare_exchange (wrong expected pointer).
     match atomic_ptr.compare_exchange(&raw mut Y, std::ptr::null_mut(), SeqCst, SeqCst) {
         Ok(_ptr) => std::process::abort(),
         Err(ptr) => pointers_equal(ptr, &raw mut X),
     }
+    // Non-atomic read value should also be unchanged by a failing compare_exchange.
+    pointers_equal(*atomic_ptr.as_ptr(), &raw mut X);
+
     // Failing compare_exchange (null).
     match atomic_ptr.compare_exchange(std::ptr::null_mut(), std::ptr::null_mut(), SeqCst, SeqCst) {
         Ok(_ptr) => std::process::abort(),
         Err(ptr) => pointers_equal(ptr, &raw mut X),
     }
+    // Non-atomic read value should also be unchanged by a failing compare_exchange.
+    pointers_equal(*atomic_ptr.as_ptr(), &raw mut X);
+
     // Successful compare_exchange.
     match atomic_ptr.compare_exchange(&raw mut X, &raw mut Y, SeqCst, SeqCst) {
         Ok(ptr) => pointers_equal(ptr, &raw mut X),
         Err(_ptr) => std::process::abort(),
     }
     // compare_exchange should update the pointer.
     pointers_equal(atomic_ptr.load(SeqCst), &raw mut Y);
+    pointers_equal(*atomic_ptr.as_ptr(), &raw mut Y);
 }
 
 unsafe fn test_add_sub() {
     const LEN: usize = 16;
     let mut array: [u64; LEN] = std::array::from_fn(|i| i as u64);
-
     let atomic_ptr: AtomicPtr<u64> = AtomicPtr::new(&raw mut array[0]);
-    // FIXME(genmc,HACK): remove this initializing write once Miri-GenMC supports mixed atomic-non-atomic accesses.
-    atomic_ptr.store(&raw mut array[0], SeqCst);
 
     // Each element of the array should be reachable using `fetch_ptr_add`.
     // All pointers must stay valid.
@@ -110,10 +118,7 @@ unsafe fn test_and_or_xor() {
 
     let mut array = AlignedArray(std::array::from_fn(|i| i as u64 * 10));
     let array_ptr = &raw mut array.0[0];
-
     let atomic_ptr: AtomicPtr<u64> = AtomicPtr::new(array_ptr);
-    // FIXME(genmc,HACK): remove this initializing write once Miri-GenMC supports mixed atomic-non-atomic accesses.
-    atomic_ptr.store(array_ptr, SeqCst);
 
     // Test no-op arguments.
     assert_equals(array_ptr, atomic_ptr.fetch_or(0, SeqCst));

tests/genmc/pass/atomics/atomic_ptr_roundtrip.rs

@@ -23,9 +23,6 @@ static mut X: [u8; 16] = [0; 16];
 
 #[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.
-    PTR.store(std::ptr::null_mut(), SeqCst);
-
     unsafe {
         let ids = [
             spawn_pthread_closure(|| {

tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.rs

@@ -26,9 +26,6 @@ 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;

tests/genmc/pass/atomics/mixed_atomic_non_atomic.rs

@@ -0,0 +1,41 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+// Test that we can read the value of a non-atomic store atomically and an of an atomic value non-atomically.
+
+#![no_main]
+
+use std::sync::atomic::Ordering::*;
+use std::sync::atomic::{AtomicI8, AtomicU64};
+
+static X: AtomicU64 = AtomicU64::new(1234);
+static Y: AtomicI8 = AtomicI8::new(0xB);
+
+fn assert_equals<T: Eq>(a: T, b: T) {
+    if a != b {
+        std::process::abort();
+    }
+}
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    // 8 byte unsigned integer:
+    // Read initial value.
+    assert_equals(1234, X.load(Relaxed));
+    // Atomic store, non-atomic load.
+    X.store(0xFFFF, Relaxed);
+    assert_equals(0xFFFF, unsafe { *X.as_ptr() });
+    // Non-atomic store, atomic load.
+    unsafe { *X.as_ptr() = 0xAAAA };
+    assert_equals(0xAAAA, X.load(Relaxed));
+
+    // 1 byte signed integer:
+    // Read initial value.
+    assert_equals(0xB, Y.load(Relaxed));
+    // Atomic store, non-atomic load.
+    Y.store(42, Relaxed);
+    assert_equals(42, unsafe { *Y.as_ptr() });
+    // Non-atomic store, atomic load.
+    unsafe { *Y.as_ptr() = -42 };
+    assert_equals(-42, Y.load(Relaxed));
+    0
+}

tests/genmc/pass/atomics/mixed_atomic_non_atomic.stderr

@@ -0,0 +1,2 @@
+Running GenMC Verification...
+Verification complete with 1 executions. No errors found.

tests/genmc/pass/atomics/read_initial_value.rs

@@ -0,0 +1,41 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+// Test that we can read the initial value of global, heap and stack allocations in GenMC mode.
+
+#![no_main]
+
+use std::sync::atomic::AtomicU64;
+use std::sync::atomic::Ordering::*;
+
+static X: AtomicU64 = AtomicU64::new(1234);
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    // Read initial value of global allocation.
+    if 1234 != unsafe { *X.as_ptr() } {
+        std::process::abort();
+    }
+    if 1234 != X.load(SeqCst) {
+        std::process::abort();
+    }
+
+    // Read initial value of stack allocation.
+    let a = AtomicU64::new(0xBB);
+    if 0xBB != unsafe { *a.as_ptr() } {
+        std::process::abort();
+    }
+    if 0xBB != a.load(SeqCst) {
+        std::process::abort();
+    }
+
+    // Read initial value of heap allocation.
+    let b = Box::new(AtomicU64::new(0xCCC));
+    if 0xCCC != unsafe { *b.as_ptr() } {
+        std::process::abort();
+    }
+    if 0xCCC != b.load(SeqCst) {
+        std::process::abort();
+    }
+
+    0
+}

tests/genmc/pass/atomics/read_initial_value.stderr

@@ -0,0 +1,2 @@
+Running GenMC Verification...
+Verification complete with 1 executions. No errors found.

tests/genmc/pass/atomics/rmw_ops.rs

@@ -21,11 +21,8 @@ fn assert_eq<T: Eq>(x: T, y: T) {
 
 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
+        let x = <$atomic>::new(123);
         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