diff --git a/tests/pass/0weak_memory_consistency.rs b/tests/pass/0weak_memory_consistency.rs index ce5b8be07f..b33aefaf1d 100644 --- a/tests/pass/0weak_memory_consistency.rs +++ b/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 . -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(); } } diff --git a/tests/pass/0weak_memory_consistency_sc.rs b/tests/pass/0weak_memory_consistency_sc.rs new file mode 100644 index 0000000000..bde3eda313 --- /dev/null +++ b/tests/pass/0weak_memory_consistency_sc.rs @@ -0,0 +1,311 @@ +//@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. + +// The following tests check whether our weak memory emulation produces +// any inconsistent execution outcomes +// This file here focuses on SC accesses and fences. + +use std::sync::atomic::Ordering::*; +use std::sync::atomic::{AtomicBool, AtomicI32, Ordering, fence}; +use std::thread::spawn; + +// We can't create static items because we need to run each test +// multiple times +fn static_atomic(val: i32) -> &'static AtomicI32 { + Box::leak(Box::new(AtomicI32::new(val))) +} +fn static_atomic_bool(val: bool) -> &'static AtomicBool { + Box::leak(Box::new(AtomicBool::new(val))) +} + +/// 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(); + } + val +} + +// Test case SB taken from Repairing Sequential Consistency in C/C++11 +// by Lahav et al. +// https://plv.mpi-sws.org/scfix/paper.pdf +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)); +} + +// 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 . +/// Test by Ori Lahav. +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); // bad case: loads 1 + let yval = y.load(Relaxed); // bad case: loads 0 + (kval, yval) + }); + let j4 = spawn(move || { + let zval = z.load(Acquire); // bad case: loads 1 + let xval = x.load(Relaxed); // bad case: loads 0 + (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. +/// Test by Ori Lahav. +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); + // If this sees a 0, the fence must have been *before* the x.store(1). + x.load(Relaxed) + }); + + let yval = j1.join().unwrap(); + let xval = j2.join().unwrap(); + let bad = yval == 0 && xval == 0; + assert!(!bad); +} + +/// Test that SC fences and accesses sync correctly with each other +/// when mediated by a release-acquire pair. +/// Test by Ori Lahav. +fn test_sc_fence_access_relacq() { + let x = static_atomic(0); + let y = static_atomic(0); + let z = static_atomic(0); + + let j1 = spawn(move || { + x.store(1, SeqCst); + y.load(SeqCst) // bad case: loads 0 + }); + let j2 = spawn(move || { + y.store(1, Relaxed); + z.store(1, Release) + }); + let j3 = spawn(move || { + let zval = z.load(Acquire); // bad case: loads 1 + // If we see 1 here, the rel-acq pair makes the fence happen after the z.store(1). + fence(SeqCst); + // If this sees a 0, the fence must have been *before* the x.store(1). + let xval = x.load(Relaxed); // bad case: loads 0 + (zval, xval) + }); + + let yval = j1.join().unwrap(); + j2.join().unwrap(); + let (zval, xval) = j3.join().unwrap(); + let bad = yval == 0 && zval == 1 && xval == 0; + assert!(!bad); +} + +/// A test that involves multiple SC fences and accesses. +/// Test by Ori Lahav. +fn test_sc_multi_fence() { + let x = static_atomic(0); + let y = static_atomic(0); + let z = static_atomic(0); + + let j1 = spawn(move || { + x.store(1, SeqCst); + y.load(SeqCst) // bad case: loads 0 + }); + let j2 = spawn(move || { + y.store(1, Relaxed); + // In the bad case this fence is *after* the j1 y.load, since + // otherwise that load would pick up the 1 we just stored. + fence(SeqCst); + z.load(Relaxed) // bad case: loads 0 + }); + let j3 = spawn(move || { + z.store(1, Relaxed); + }); + let j4 = spawn(move || { + let zval = z.load(Relaxed); // bad case: loads 1 + // In the bad case this fence is *after* the one above since + // otherwise, the j2 load of z would load 1. + fence(SeqCst); + // Since that fence is in turn after the j1 y.load, our fence is + // after the j1 x.store, which means we must pick up that store. + let xval = x.load(Relaxed); // bad case: loads 0 + (zval, xval) + }); + + let yval = j1.join().unwrap(); + let zval1 = j2.join().unwrap(); + j3.join().unwrap(); + let (zval2, xval) = j4.join().unwrap(); + let bad = yval == 0 && zval1 == 0 && zval2 == 1 && xval == 0; + assert!(!bad); +} + +pub fn main() { + for _ in 0..50 { + test_sc_store_buffering(); + test_iriw_sc_rlx(); + test_cpp20_sc_fence_fix(); + test_cpp20_rwc_syncs(); + test_sc_fence_release(); + test_sc_fence_access(); + test_sc_fence_access_relacq(); + test_sc_multi_fence(); + } +}