Merge pull request #4575 from RalfJung/weakmem-origin

weak memory tests: add more info on where they come from, and test list of behaviors more thoroughly

Author: RalfJung

tests/pass/0weak_memory_consistency.rs renamed to tests/pass/0weak_memory/consistency.rs

@@ -1,6 +1,7 @@
-//@compile-flags: -Zmiri-ignore-leaks -Zmiri-disable-stacked-borrows -Zmiri-disable-validation -Zmiri-provenance-gc=10000
+//@compile-flags: -Zmiri-ignore-leaks -Zmiri-disable-stacked-borrows -Zmiri-disable-validation
 // 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.
+//@compile-flags: -Zmiri-provenance-gc=10000
 
 // The following tests check whether our weak memory emulation produces
 // any inconsistent execution outcomes
@@ -14,13 +15,6 @@
 // To mitigate this, each test is ran enough times such that the chance
 // of spurious success is very low. These tests never spuriously fail.
 
-// Test cases and their consistent outcomes are from
-// http://svr-pes20-cppmem.cl.cam.ac.uk/cppmem/
-// Based on
-// M. Batty, S. Owens, S. Sarkar, P. Sewell and T. Weber,
-// "Mathematizing C++ concurrency", ACM SIGPLAN Notices, vol. 46, no. 1, pp. 55-66, 2011.
-// Available: https://ss265.host.cs.st-andrews.ac.uk/papers/n3132.pdf.
-
 use std::sync::atomic::Ordering::*;
 use std::sync::atomic::{AtomicBool, AtomicI32, Ordering, fence};
 use std::thread::spawn;
@@ -56,6 +50,8 @@ fn spin_until_bool(loc: &AtomicBool, ord: Ordering, val: bool) -> bool {
     val
 }
 
+/// Test matching https://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2017/POPL.pdf, Figure 7.
+/// (The Figure 8 test is in `weak.rs`.)
 fn test_corr() {
     let x = static_atomic(0);
     let y = static_atomic(0);
@@ -75,19 +71,25 @@ fn test_corr() {
     let j3 = spawn(move || { //                      |                    |
         spin_until_i32(&y, Acquire, 1); // <---------+                    |
         x.load(Relaxed) // <----------------------------------------------+
-        // The two reads on x are ordered by hb, so they cannot observe values
-        // differently from the modification order. If the first read observed
-        // 2, then the second read must observe 2 as well.
     });
 
     j1.join().unwrap();
     let r2 = j2.join().unwrap();
     let r3 = j3.join().unwrap();
+    // The two reads on x are ordered by hb, so they cannot observe values
+    // differently from the modification order. If the first read observed
+    // 2, then the second read must observe 2 as well.
     if r2 == 2 {
         assert_eq!(r3, 2);
     }
 }
 
+/// This test case is from:
+/// http://svr-pes20-cppmem.cl.cam.ac.uk/cppmem/, "WRC"
+/// Based on
+/// M. Batty, S. Owens, S. Sarkar, P. Sewell and T. Weber,
+/// "Mathematizing C++ concurrency", ACM SIGPLAN Notices, vol. 46, no. 1, pp. 55-66, 2011.
+/// Available: https://www.cl.cam.ac.uk/~pes20/cpp/popl085ap-sewell.pdf.
 fn test_wrc() {
     let x = static_atomic(0);
     let y = static_atomic(0);
@@ -114,6 +116,8 @@ fn test_wrc() {
     assert_eq!(r3, 1);
 }
 
+/// Another test from http://svr-pes20-cppmem.cl.cam.ac.uk/cppmem/:
+/// MP (na_rel+acq_na)
 fn test_message_passing() {
     let mut var = 0u32;
     let ptr = &mut var as *mut u32;
@@ -139,7 +143,8 @@ fn test_message_passing() {
     assert_eq!(r2, 1);
 }
 
-// LB+acq_rel+acq_rel
+/// Another test from http://svr-pes20-cppmem.cl.cam.ac.uk/cppmem/:
+/// LB+acq_rel+acq_rel
 fn test_load_buffering_acq_rel() {
     let x = static_atomic(0);
     let y = static_atomic(0);

tests/pass/0weak_memory_consistency_sc.rs renamed to tests/pass/0weak_memory/consistency_sc.rs

@@ -1,6 +1,7 @@
-//@compile-flags: -Zmiri-ignore-leaks -Zmiri-disable-stacked-borrows -Zmiri-disable-validation -Zmiri-provenance-gc=10000
+//@compile-flags: -Zmiri-ignore-leaks -Zmiri-disable-stacked-borrows -Zmiri-disable-validation
 // 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.
+//@compile-flags: -Zmiri-provenance-gc=10000
 
 // The following tests check whether our weak memory emulation produces
 // any inconsistent execution outcomes
@@ -348,7 +349,7 @@ fn test_sc_relaxed() {
 }
 
 pub fn main() {
-    for _ in 0..50 {
+    for _ in 0..32 {
         test_sc_store_buffering();
         test_iriw_sc_rlx();
         test_cpp20_sc_fence_fix();

tests/pass/weak_memory/extra_cpp.rs renamed to tests/pass/0weak_memory/extra_cpp.rs

@@ -0,0 +1,208 @@
+//@compile-flags: -Zmiri-ignore-leaks -Zmiri-fixed-schedule
+// 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.
+//@compile-flags: -Zmiri-provenance-gc=10000
+
+// Tests showing weak memory behaviours are exhibited, even with a fixed scheule.
+// We run all tests a number of times and then check that we see the desired list of outcomes.
+
+// Spurious failure is possible, if you are really unlucky with
+// the RNG and always read the latest value from the store buffer.
+
+use std::sync::atomic::Ordering::*;
+use std::sync::atomic::{AtomicUsize, fence};
+use std::thread::spawn;
+
+#[allow(dead_code)]
+#[derive(Copy, Clone)]
+struct EvilSend<T>(pub T);
+
+unsafe impl<T> Send for EvilSend<T> {}
+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: usize) -> &'static AtomicUsize {
+    Box::leak(Box::new(AtomicUsize::new(val)))
+}
+
+// Spins until it reads the given value
+fn spin_until(loc: &AtomicUsize, val: usize) -> usize {
+    while loc.load(Relaxed) != val {
+        std::hint::spin_loop();
+    }
+    val
+}
+
+/// Check that the function produces the intended set of outcomes.
+#[track_caller]
+fn check_all_outcomes<T: Eq + std::hash::Hash + std::fmt::Debug>(
+    expected: impl IntoIterator<Item = T>,
+    generate: impl Fn() -> T,
+) {
+    use std::collections::HashSet;
+
+    let expected: HashSet<T> = HashSet::from_iter(expected);
+    let mut seen = HashSet::new();
+    // Let's give it N times as many tries as we are expecting values.
+    let tries = expected.len() * 12;
+    for i in 0..tries {
+        let val = generate();
+        assert!(expected.contains(&val), "got an unexpected value: {val:?}");
+        seen.insert(val);
+        if i > tries / 2 && expected.len() == seen.len() {
+            // We saw everything and we did quite a few tries, let's avoid wasting time.
+            return;
+        }
+    }
+    // Let's see if we saw them all.
+    for val in expected {
+        if !seen.contains(&val) {
+            panic!("did not get value that should be possible: {val:?}");
+        }
+    }
+}
+
+fn relaxed() {
+    check_all_outcomes([0, 1, 2], || {
+        let x = static_atomic(0);
+        let j1 = spawn(move || {
+            x.store(1, Relaxed);
+            // Preemption is disabled, so the store above will never be the
+            // latest store visible to another thread.
+            x.store(2, Relaxed);
+        });
+
+        let j2 = spawn(move || x.load(Relaxed));
+
+        j1.join().unwrap();
+        let r2 = j2.join().unwrap();
+
+        // There are three possible values here: 0 (from the initial read), 1 (from the first relaxed
+        // read), and 2 (the last read).
+        r2
+    });
+}
+
+// https://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2017/POPL.pdf Figure 8
+fn seq_cst() {
+    check_all_outcomes([1, 3], || {
+        let x = static_atomic(0);
+
+        let j1 = spawn(move || {
+            x.store(1, Relaxed);
+        });
+
+        let j2 = spawn(move || {
+            x.store(2, SeqCst);
+            x.store(3, SeqCst);
+        });
+
+        let j3 = spawn(move || x.load(SeqCst));
+
+        j1.join().unwrap();
+        j2.join().unwrap();
+        let r3 = j3.join().unwrap();
+
+        // Even though we force t3 to run last, it can still see the value 1.
+        // And it can *never* see the value 2!
+        r3
+    });
+}
+
+fn initialization_write(add_fence: bool) {
+    check_all_outcomes([11, 22], || {
+        let x = static_atomic(11);
+
+        let wait = static_atomic(0);
+
+        let j1 = spawn(move || {
+            x.store(22, Relaxed);
+            // Relaxed is intentional. We want to test if the thread 2 reads the initialisation write
+            // after a relaxed write
+            wait.store(1, Relaxed);
+        });
+
+        let j2 = spawn(move || {
+            spin_until(wait, 1);
+            if add_fence {
+                fence(AcqRel);
+            }
+            x.load(Relaxed)
+        });
+
+        j1.join().unwrap();
+        let r2 = j2.join().unwrap();
+
+        r2
+    });
+}
+
+fn faa_replaced_by_load() {
+    check_all_outcomes([true, false], || {
+        // Example from https://github.com/llvm/llvm-project/issues/56450#issuecomment-1183695905
+        pub fn rdmw(storing: &AtomicUsize, sync: &AtomicUsize, loading: &AtomicUsize) -> usize {
+            storing.store(1, Relaxed);
+            fence(Release);
+            // sync.fetch_add(0, Relaxed);
+            sync.load(Relaxed);
+            fence(Acquire);
+            loading.load(Relaxed)
+        }
+
+        let x = static_atomic(0);
+        let y = static_atomic(0);
+        let z = static_atomic(0);
+
+        let t1 = spawn(move || rdmw(y, x, z));
+
+        let t2 = spawn(move || rdmw(z, x, y));
+
+        let a = t1.join().unwrap();
+        let b = t2.join().unwrap();
+        (a, b) == (0, 0)
+    });
+}
+
+/// Checking that the weaker release sequence example from
+/// <https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0982r0.html> can actually produce the
+/// new behavior (`Some(0)` in our version).
+fn weaker_release_sequences() {
+    check_all_outcomes([None, Some(0), Some(1)], || {
+        let x = static_atomic(0);
+        let y = static_atomic(0);
+
+        let t1 = spawn(move || {
+            x.store(2, Relaxed);
+        });
+        let t2 = spawn(move || {
+            y.store(1, Relaxed);
+            x.store(1, Release);
+            x.store(3, Relaxed);
+        });
+        let t3 = spawn(move || {
+            if x.load(Acquire) == 3 {
+                // In C++11, if we read the 3 here, and if the store of 1 was just before the store
+                // of 3 in mo order (which it is because we fix the schedule), this forms a release
+                // sequence, meaning we acquire the release store of 1, and we can thus never see
+                // the value 0.
+                // In C++20, this is no longer a release sequence, so 0 can now be observed.
+                Some(y.load(Relaxed))
+            } else {
+                None
+            }
+        });
+
+        t1.join().unwrap();
+        t2.join().unwrap();
+        t3.join().unwrap()
+    });
+}
+
+pub fn main() {
+    relaxed();
+    seq_cst();
+    initialization_write(false);
+    initialization_write(true);
+    faa_replaced_by_load();
+    weaker_release_sequences();
+}