Merge pull request #4076 from RalfJung/sc-fence

fix SC fence logic

Author: RalfJung

src/tools/miri/src/concurrency/data_race.rs

@@ -874,23 +874,27 @@ pub trait EvalContextExt<'tcx>: MiriInterpCxExt<'tcx> {
                         // Either Acquire | AcqRel | SeqCst
                         clocks.apply_acquire_fence();
                     }
-                    if atomic != AtomicFenceOrd::Acquire {
-                        // Either Release | AcqRel | SeqCst
-                        clocks.apply_release_fence();
-                    }
                     if atomic == AtomicFenceOrd::SeqCst {
                         // Behave like an RMW on the global fence location. This takes full care of
                         // all the SC fence requirements, including C++17 §32.4 [atomics.order]
                         // paragraph 6 (which would limit what future reads can see). It also rules
                         // out many legal behaviors, but we don't currently have a model that would
                         // be more precise.
+                        // Also see the second bullet on page 10 of
+                        // <https://www.cs.tau.ac.il/~orilahav/papers/popl21_robustness.pdf>.
                         let mut sc_fence_clock = data_race.last_sc_fence.borrow_mut();
                         sc_fence_clock.join(&clocks.clock);
                         clocks.clock.join(&sc_fence_clock);
                         // Also establish some sort of order with the last SC write that happened, globally
                         // (but this is only respected by future reads).
                         clocks.write_seqcst.join(&data_race.last_sc_write_per_thread.borrow());
                     }
+                    // The release fence is last, since both of the above could alter our clock,
+                    // which should be part of what is being released.
+                    if atomic != AtomicFenceOrd::Acquire {
+                        // Either Release | AcqRel | SeqCst
+                        clocks.apply_release_fence();
+                    }
 
                     // Increment timestamp in case of release semantics.
                     interp_ok(atomic != AtomicFenceOrd::Acquire)

src/tools/miri/tests/pass/0weak_memory_consistency.rs

@@ -1,4 +1,4 @@
-//@compile-flags: -Zmiri-ignore-leaks -Zmiri-disable-stacked-borrows -Zmiri-provenance-gc=10000
+//@compile-flags: -Zmiri-ignore-leaks -Zmiri-disable-stacked-borrows -Zmiri-disable-validation -Zmiri-provenance-gc=10000
 // This test's runtime explodes if the GC interval is set to 1 (which we do in CI), so we
 // override it internally back to the default frequency.
 
@@ -34,14 +34,10 @@ unsafe impl<T> Sync for EvilSend<T> {}
 // We can't create static items because we need to run each test
 // multiple times
 fn static_atomic(val: i32) -> &'static AtomicI32 {
-    let ret = Box::leak(Box::new(AtomicI32::new(val)));
-    ret.store(val, Relaxed); // work around https://github.com/rust-lang/miri/issues/2164
-    ret
+    Box::leak(Box::new(AtomicI32::new(val)))
 }
 fn static_atomic_bool(val: bool) -> &'static AtomicBool {
-    let ret = Box::leak(Box::new(AtomicBool::new(val)));
-    ret.store(val, Relaxed); // work around https://github.com/rust-lang/miri/issues/2164
-    ret
+    Box::leak(Box::new(AtomicBool::new(val)))
 }
 
 // Spins until it acquires a pre-determined value.
@@ -365,6 +361,45 @@ fn test_cpp20_rwc_syncs() {
     assert!((b, c) != (0, 0));
 }
 
+/// This checks that the *last* thing the SC fence does is act like a release fence.
+/// See <https://github.com/rust-lang/miri/pull/4057#issuecomment-2522296601>.
+fn test_sc_fence_release() {
+    let x = static_atomic(0);
+    let y = static_atomic(0);
+    let z = static_atomic(0);
+    let k = static_atomic(0);
+
+    let j1 = spawn(move || {
+        x.store(1, Relaxed);
+        fence(SeqCst);
+        k.store(1, Relaxed);
+    });
+    let j2 = spawn(move || {
+        y.store(1, Relaxed);
+        fence(SeqCst);
+        z.store(1, Relaxed);
+    });
+
+    let j3 = spawn(move || {
+        let kval = k.load(Acquire);
+        let yval = y.load(Relaxed);
+        (kval, yval)
+    });
+    let j4 = spawn(move || {
+        let zval = z.load(Acquire);
+        let xval = x.load(Relaxed);
+        (zval, xval)
+    });
+
+    j1.join().unwrap();
+    j2.join().unwrap();
+    let (kval, yval) = j3.join().unwrap();
+    let (zval, xval) = j4.join().unwrap();
+
+    let bad = kval == 1 && yval == 0 && zval == 1 && xval == 0;
+    assert!(!bad);
+}
+
 pub fn main() {
     for _ in 0..50 {
         test_single_thread();
@@ -378,5 +413,6 @@ pub fn main() {
         test_iriw_sc_rlx();
         test_cpp20_sc_fence_fix();
         test_cpp20_rwc_syncs();
+        test_sc_fence_release();
     }
 }