Merge pull request #4090 from RalfJung/sc-test

add more tests for SC access/fence consistency

Author: RalfJung

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

@@ -40,7 +40,7 @@ fn static_atomic_bool(val: bool) -> &'static AtomicBool {
     Box::leak(Box::new(AtomicBool::new(val)))
 }
 
-// Spins until it acquires a pre-determined value.
+/// Spins until it acquires a pre-determined value.
 fn loads_value(loc: &AtomicI32, ord: Ordering, val: i32) -> i32 {
     while loc.load(ord) != val {
         std::hint::spin_loop();
@@ -186,31 +186,6 @@ fn test_mixed_access() {
     assert_eq!(r2, 2);
 }
 
-// The following two tests are taken from Repairing Sequential Consistency in C/C++11
-// by Lahav et al.
-// https://plv.mpi-sws.org/scfix/paper.pdf
-
-// Test case SB
-fn test_sc_store_buffering() {
-    let x = static_atomic(0);
-    let y = static_atomic(0);
-
-    let j1 = spawn(move || {
-        x.store(1, SeqCst);
-        y.load(SeqCst)
-    });
-
-    let j2 = spawn(move || {
-        y.store(1, SeqCst);
-        x.load(SeqCst)
-    });
-
-    let a = j1.join().unwrap();
-    let b = j2.join().unwrap();
-
-    assert_ne!((a, b), (0, 0));
-}
-
 fn test_single_thread() {
     let x = AtomicI32::new(42);
 
@@ -257,178 +232,6 @@ fn test_sync_through_rmw_and_fences() {
     assert_ne!((a, b), (0, 0));
 }
 
-// Test case by @SabrinaJewson
-// https://github.com/rust-lang/miri/issues/2301#issuecomment-1221502757
-// Demonstrating C++20 SC access changes
-fn test_iriw_sc_rlx() {
-    let x = static_atomic_bool(false);
-    let y = static_atomic_bool(false);
-
-    let a = spawn(move || x.store(true, Relaxed));
-    let b = spawn(move || y.store(true, Relaxed));
-    let c = spawn(move || {
-        while !x.load(SeqCst) {}
-        y.load(SeqCst)
-    });
-    let d = spawn(move || {
-        while !y.load(SeqCst) {}
-        x.load(SeqCst)
-    });
-
-    a.join().unwrap();
-    b.join().unwrap();
-    let c = c.join().unwrap();
-    let d = d.join().unwrap();
-
-    assert!(c || d);
-}
-
-// Similar to `test_iriw_sc_rlx` but with fences instead of SC accesses.
-fn test_cpp20_sc_fence_fix() {
-    let x = static_atomic_bool(false);
-    let y = static_atomic_bool(false);
-
-    let thread1 = spawn(|| {
-        let a = x.load(Relaxed);
-        fence(SeqCst);
-        let b = y.load(Relaxed);
-        (a, b)
-    });
-
-    let thread2 = spawn(|| {
-        x.store(true, Relaxed);
-    });
-    let thread3 = spawn(|| {
-        y.store(true, Relaxed);
-    });
-
-    let thread4 = spawn(|| {
-        let c = y.load(Relaxed);
-        fence(SeqCst);
-        let d = x.load(Relaxed);
-        (c, d)
-    });
-
-    let (a, b) = thread1.join().unwrap();
-    thread2.join().unwrap();
-    thread3.join().unwrap();
-    let (c, d) = thread4.join().unwrap();
-    let bad = a == true && b == false && c == true && d == false;
-    assert!(!bad);
-}
-
-// https://plv.mpi-sws.org/scfix/paper.pdf
-// 2.2 Second Problem: SC Fences are Too Weak
-fn test_cpp20_rwc_syncs() {
-    /*
-    int main() {
-        atomic_int x = 0;
-        atomic_int y = 0;
-        {{{ x.store(1,mo_relaxed);
-        ||| { r1=x.load(mo_relaxed).readsvalue(1);
-              fence(mo_seq_cst);
-              r2=y.load(mo_relaxed); }
-        ||| { y.store(1,mo_relaxed);
-              fence(mo_seq_cst);
-              r3=x.load(mo_relaxed); }
-        }}}
-        return 0;
-    }
-    */
-    let x = static_atomic(0);
-    let y = static_atomic(0);
-
-    let j1 = spawn(move || {
-        x.store(1, Relaxed);
-    });
-
-    let j2 = spawn(move || {
-        loads_value(&x, Relaxed, 1);
-        fence(SeqCst);
-        y.load(Relaxed)
-    });
-
-    let j3 = spawn(move || {
-        y.store(1, Relaxed);
-        fence(SeqCst);
-        x.load(Relaxed)
-    });
-
-    j1.join().unwrap();
-    let b = j2.join().unwrap();
-    let c = j3.join().unwrap();
-
-    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);
-}
-
-/// Test that SC fences and accesses sync correctly with each other.
-fn test_sc_fence_access() {
-    /*
-        Wx1 sc
-        Ry0 sc
-        ||
-        Wy1 rlx
-        SC-fence
-        Rx0 rlx
-    */
-    let x = static_atomic(0);
-    let y = static_atomic(0);
-
-    let j1 = spawn(move || {
-        x.store(1, SeqCst);
-        y.load(SeqCst)
-    });
-    let j2 = spawn(move || {
-        y.store(1, Relaxed);
-        fence(SeqCst);
-        x.load(Relaxed)
-    });
-
-    let v1 = j1.join().unwrap();
-    let v2 = j2.join().unwrap();
-    let bad = v1 == 0 && v2 == 0;
-    assert!(!bad);
-}
-
 pub fn main() {
     for _ in 0..50 {
         test_single_thread();
@@ -437,12 +240,6 @@ pub fn main() {
         test_message_passing();
         test_wrc();
         test_corr();
-        test_sc_store_buffering();
         test_sync_through_rmw_and_fences();
-        test_iriw_sc_rlx();
-        test_cpp20_sc_fence_fix();
-        test_cpp20_rwc_syncs();
-        test_sc_fence_release();
-        test_sc_fence_access();
     }
 }