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

6 files changed, 375 insertions, 343 deletions

diff --git a/src/tools/miri/tests/pass/0weak_memory_consistency.rs b/src/tools/miri/tests/pass/0weak_memory/consistency.rs
index e4ed9675de8..16a38ebd9d4 100644
--- a/src/tools/miri/tests/pass/0weak_memory_consistency.rs
+++ b/src/tools/miri/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);
diff --git a/src/tools/miri/tests/pass/0weak_memory_consistency_sc.rs b/src/tools/miri/tests/pass/0weak_memory/consistency_sc.rs
index 937c2a8cf28..cb8535b8ad7 100644
--- a/src/tools/miri/tests/pass/0weak_memory_consistency_sc.rs
+++ b/src/tools/miri/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();
diff --git a/src/tools/miri/tests/pass/weak_memory/extra_cpp.rs b/src/tools/miri/tests/pass/0weak_memory/extra_cpp.rs
index 94df7308080..94df7308080 100644
--- a/src/tools/miri/tests/pass/weak_memory/extra_cpp.rs
+++ b/src/tools/miri/tests/pass/0weak_memory/extra_cpp.rs
diff --git a/src/tools/miri/tests/pass/0weak_memory/weak.rs b/src/tools/miri/tests/pass/0weak_memory/weak.rs
new file mode 100644
index 00000000000..75c6e8f1a87
--- /dev/null
+++ b/src/tools/miri/tests/pass/0weak_memory/weak.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();
+}
diff --git a/src/tools/miri/tests/pass/float_nan.rs b/src/tools/miri/tests/pass/float_nan.rs
index 3ffdb6868ac..90281630740 100644
--- a/src/tools/miri/tests/pass/float_nan.rs
+++ b/src/tools/miri/tests/pass/float_nan.rs
@@ -1,7 +1,8 @@
+// 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
 #![feature(float_gamma, portable_simd, core_intrinsics)]
-use std::collections::HashSet;
 use std::fmt;
-use std::hash::Hash;
 use std::hint::black_box;
 
 fn ldexp(a: f64, b: i32) -> f64 {
@@ -25,15 +26,26 @@ enum NaNKind {
 }
 use NaNKind::*;
 
+/// Check that the function produces the intended set of outcomes.
 #[track_caller]
-fn check_all_outcomes<T: Eq + Hash + fmt::Display>(expected: HashSet<T>, generate: impl Fn() -> T) {
+fn check_all_outcomes<T: Eq + std::hash::Hash + fmt::Display>(
+    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 sixteen times as many tries as we are expecting values.
-    let tries = expected.len() * 16;
-    for _ in 0..tries {
+    // 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 {
@@ -193,51 +205,50 @@ impl F64 {
 
 fn test_f32() {
     // Freshly generated NaNs can have either sign.
-    check_all_outcomes(
-        HashSet::from_iter([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)]),
-        || F32::from(0.0 / black_box(0.0)),
-    );
+    check_all_outcomes([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)], || {
+        F32::from(0.0 / black_box(0.0))
+    });
     // When there are NaN inputs, their payload can be propagated, with any sign.
     let all1_payload = u32_ones(22);
     let all1 = F32::nan(Pos, Quiet, all1_payload).as_f32();
     check_all_outcomes(
-        HashSet::from_iter([
+        [
             F32::nan(Pos, Quiet, 0),
             F32::nan(Neg, Quiet, 0),
             F32::nan(Pos, Quiet, all1_payload),
             F32::nan(Neg, Quiet, all1_payload),
-        ]),
+        ],
         || F32::from(0.0 + all1),
     );
     // When there are two NaN inputs, the output can be either one, or the preferred NaN.
     let just1 = F32::nan(Neg, Quiet, 1).as_f32();
     check_all_outcomes(
-        HashSet::from_iter([
+        [
             F32::nan(Pos, Quiet, 0),
             F32::nan(Neg, Quiet, 0),
             F32::nan(Pos, Quiet, 1),
             F32::nan(Neg, Quiet, 1),
             F32::nan(Pos, Quiet, all1_payload),
             F32::nan(Neg, Quiet, all1_payload),
-        ]),
+        ],
         || F32::from(just1 - all1),
     );
     // When there are *signaling* NaN inputs, they might be quieted or not.
     let all1_snan = F32::nan(Pos, Signaling, all1_payload).as_f32();
     check_all_outcomes(
-        HashSet::from_iter([
+        [
             F32::nan(Pos, Quiet, 0),
             F32::nan(Neg, Quiet, 0),
             F32::nan(Pos, Quiet, all1_payload),
             F32::nan(Neg, Quiet, all1_payload),
             F32::nan(Pos, Signaling, all1_payload),
             F32::nan(Neg, Signaling, all1_payload),
-        ]),
+        ],
         || F32::from(0.0 * all1_snan),
     );
     // Mix signaling and non-signaling NaN.
     check_all_outcomes(
-        HashSet::from_iter([
+        [
             F32::nan(Pos, Quiet, 0),
             F32::nan(Neg, Quiet, 0),
             F32::nan(Pos, Quiet, 1),
@@ -246,35 +257,26 @@ fn test_f32() {
             F32::nan(Neg, Quiet, all1_payload),
             F32::nan(Pos, Signaling, all1_payload),
             F32::nan(Neg, Signaling, all1_payload),
-        ]),
+        ],
         || F32::from(just1 % all1_snan),
     );
 
     // Unary `-` must preserve payloads exactly.
-    check_all_outcomes(HashSet::from_iter([F32::nan(Neg, Quiet, all1_payload)]), || {
-        F32::from(-all1)
-    });
-    check_all_outcomes(HashSet::from_iter([F32::nan(Neg, Signaling, all1_payload)]), || {
-        F32::from(-all1_snan)
-    });
+    check_all_outcomes([F32::nan(Neg, Quiet, all1_payload)], || F32::from(-all1));
+    check_all_outcomes([F32::nan(Neg, Signaling, all1_payload)], || F32::from(-all1_snan));
 
     // Intrinsics
     let nan = F32::nan(Neg, Quiet, 0).as_f32();
     let snan = F32::nan(Neg, Signaling, 1).as_f32();
+    check_all_outcomes([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)], || {
+        F32::from(f32::min(nan, nan))
+    });
+    check_all_outcomes([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)], || {
+        F32::from(nan.floor())
+    });
+    check_all_outcomes([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)], || F32::from(nan.sin()));
     check_all_outcomes(
-        HashSet::from_iter([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)]),
-        || F32::from(f32::min(nan, nan)),
-    );
-    check_all_outcomes(
-        HashSet::from_iter([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)]),
-        || F32::from(nan.floor()),
-    );
-    check_all_outcomes(
-        HashSet::from_iter([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)]),
-        || F32::from(nan.sin()),
-    );
-    check_all_outcomes(
-        HashSet::from_iter([
+        [
             F32::nan(Pos, Quiet, 0),
             F32::nan(Neg, Quiet, 0),
             F32::nan(Pos, Quiet, 1),
@@ -285,37 +287,32 @@ fn test_f32() {
             F32::nan(Neg, Quiet, all1_payload),
             F32::nan(Pos, Signaling, all1_payload),
             F32::nan(Neg, Signaling, all1_payload),
-        ]),
+        ],
         || F32::from(just1.mul_add(F32::nan(Neg, Quiet, 2).as_f32(), all1_snan)),
     );
+    check_all_outcomes([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)], || {
+        F32::from(nan.powf(nan))
+    });
     check_all_outcomes(
-        HashSet::from_iter([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)]),
-        || F32::from(nan.powf(nan)),
-    );
-    check_all_outcomes(
-        HashSet::from_iter([1.0f32.into()]),
+        [1.0f32.into()],
         || F32::from(1.0f32.powf(nan)), // special `pow` rule
     );
-    check_all_outcomes(
-        HashSet::from_iter([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)]),
-        || F32::from(nan.powi(1)),
-    );
+    check_all_outcomes([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)], || {
+        F32::from(nan.powi(1))
+    });
 
     // libm functions
+    check_all_outcomes([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)], || {
+        F32::from(nan.sinh())
+    });
+    check_all_outcomes([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)], || {
+        F32::from(nan.atan2(nan))
+    });
+    check_all_outcomes([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)], || {
+        F32::from(nan.ln_gamma().0)
+    });
     check_all_outcomes(
-        HashSet::from_iter([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)]),
-        || F32::from(nan.sinh()),
-    );
-    check_all_outcomes(
-        HashSet::from_iter([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)]),
-        || F32::from(nan.atan2(nan)),
-    );
-    check_all_outcomes(
-        HashSet::from_iter([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)]),
-        || F32::from(nan.ln_gamma().0),
-    );
-    check_all_outcomes(
-        HashSet::from_iter([
+        [
             F32::from(1.0),
             F32::nan(Pos, Quiet, 0),
             F32::nan(Neg, Quiet, 0),
@@ -323,58 +320,57 @@ fn test_f32() {
             F32::nan(Neg, Quiet, 1),
             F32::nan(Pos, Signaling, 1),
             F32::nan(Neg, Signaling, 1),
-        ]),
+        ],
         || F32::from(snan.powf(0.0)),
     );
 }
 
 fn test_f64() {
     // Freshly generated NaNs can have either sign.
-    check_all_outcomes(
-        HashSet::from_iter([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)]),
-        || F64::from(0.0 / black_box(0.0)),
-    );
+    check_all_outcomes([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)], || {
+        F64::from(0.0 / black_box(0.0))
+    });
     // When there are NaN inputs, their payload can be propagated, with any sign.
     let all1_payload = u64_ones(51);
     let all1 = F64::nan(Pos, Quiet, all1_payload).as_f64();
     check_all_outcomes(
-        HashSet::from_iter([
+        [
             F64::nan(Pos, Quiet, 0),
             F64::nan(Neg, Quiet, 0),
             F64::nan(Pos, Quiet, all1_payload),
             F64::nan(Neg, Quiet, all1_payload),
-        ]),
+        ],
         || F64::from(0.0 + all1),
     );
     // When there are two NaN inputs, the output can be either one, or the preferred NaN.
     let just1 = F64::nan(Neg, Quiet, 1).as_f64();
     check_all_outcomes(
-        HashSet::from_iter([
+        [
             F64::nan(Pos, Quiet, 0),
             F64::nan(Neg, Quiet, 0),
             F64::nan(Pos, Quiet, 1),
             F64::nan(Neg, Quiet, 1),
             F64::nan(Pos, Quiet, all1_payload),
             F64::nan(Neg, Quiet, all1_payload),
-        ]),
+        ],
         || F64::from(just1 - all1),
     );
     // When there are *signaling* NaN inputs, they might be quieted or not.
     let all1_snan = F64::nan(Pos, Signaling, all1_payload).as_f64();
     check_all_outcomes(
-        HashSet::from_iter([
+        [
             F64::nan(Pos, Quiet, 0),
             F64::nan(Neg, Quiet, 0),
             F64::nan(Pos, Quiet, all1_payload),
             F64::nan(Neg, Quiet, all1_payload),
             F64::nan(Pos, Signaling, all1_payload),
             F64::nan(Neg, Signaling, all1_payload),
-        ]),
+        ],
         || F64::from(0.0 * all1_snan),
     );
     // Mix signaling and non-signaling NaN.
     check_all_outcomes(
-        HashSet::from_iter([
+        [
             F64::nan(Pos, Quiet, 0),
             F64::nan(Neg, Quiet, 0),
             F64::nan(Pos, Quiet, 1),
@@ -383,27 +379,22 @@ fn test_f64() {
             F64::nan(Neg, Quiet, all1_payload),
             F64::nan(Pos, Signaling, all1_payload),
             F64::nan(Neg, Signaling, all1_payload),
-        ]),
+        ],
         || F64::from(just1 % all1_snan),
     );
 
     // Intrinsics
     let nan = F64::nan(Neg, Quiet, 0).as_f64();
     let snan = F64::nan(Neg, Signaling, 1).as_f64();
+    check_all_outcomes([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)], || {
+        F64::from(f64::min(nan, nan))
+    });
+    check_all_outcomes([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)], || {
+        F64::from(nan.floor())
+    });
+    check_all_outcomes([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)], || F64::from(nan.sin()));
     check_all_outcomes(
-        HashSet::from_iter([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)]),
-        || F64::from(f64::min(nan, nan)),
-    );
-    check_all_outcomes(
-        HashSet::from_iter([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)]),
-        || F64::from(nan.floor()),
-    );
-    check_all_outcomes(
-        HashSet::from_iter([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)]),
-        || F64::from(nan.sin()),
-    );
-    check_all_outcomes(
-        HashSet::from_iter([
+        [
             F64::nan(Pos, Quiet, 0),
             F64::nan(Neg, Quiet, 0),
             F64::nan(Pos, Quiet, 1),
@@ -414,41 +405,35 @@ fn test_f64() {
             F64::nan(Neg, Quiet, all1_payload),
             F64::nan(Pos, Signaling, all1_payload),
             F64::nan(Neg, Signaling, all1_payload),
-        ]),
+        ],
         || F64::from(just1.mul_add(F64::nan(Neg, Quiet, 2).as_f64(), all1_snan)),
     );
+    check_all_outcomes([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)], || {
+        F64::from(nan.powf(nan))
+    });
     check_all_outcomes(
-        HashSet::from_iter([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)]),
-        || F64::from(nan.powf(nan)),
-    );
-    check_all_outcomes(
-        HashSet::from_iter([1.0f64.into()]),
+        [1.0f64.into()],
         || F64::from(1.0f64.powf(nan)), // special `pow` rule
     );
-    check_all_outcomes(
-        HashSet::from_iter([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)]),
-        || F64::from(nan.powi(1)),
-    );
+    check_all_outcomes([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)], || {
+        F64::from(nan.powi(1))
+    });
 
     // libm functions
+    check_all_outcomes([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)], || {
+        F64::from(nan.sinh())
+    });
+    check_all_outcomes([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)], || {
+        F64::from(nan.atan2(nan))
+    });
+    check_all_outcomes([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)], || {
+        F64::from(ldexp(nan, 1))
+    });
+    check_all_outcomes([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)], || {
+        F64::from(nan.ln_gamma().0)
+    });
     check_all_outcomes(
-        HashSet::from_iter([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)]),
-        || F64::from(nan.sinh()),
-    );
-    check_all_outcomes(
-        HashSet::from_iter([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)]),
-        || F64::from(nan.atan2(nan)),
-    );
-    check_all_outcomes(
-        HashSet::from_iter([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)]),
-        || F64::from(ldexp(nan, 1)),
-    );
-    check_all_outcomes(
-        HashSet::from_iter([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)]),
-        || F64::from(nan.ln_gamma().0),
-    );
-    check_all_outcomes(
-        HashSet::from_iter([
+        [
             F64::from(1.0),
             F64::nan(Pos, Quiet, 0),
             F64::nan(Neg, Quiet, 0),
@@ -456,7 +441,7 @@ fn test_f64() {
             F64::nan(Neg, Quiet, 1),
             F64::nan(Pos, Signaling, 1),
             F64::nan(Neg, Signaling, 1),
-        ]),
+        ],
         || F64::from(snan.powf(0.0)),
     );
 }
@@ -467,82 +452,79 @@ fn test_casts() {
     let left1_payload_64 = (all1_payload_32 as u64) << (51 - 22);
 
     // 64-to-32
-    check_all_outcomes(
-        HashSet::from_iter([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)]),
-        || F32::from(F64::nan(Pos, Quiet, 0).as_f64() as f32),
-    );
+    check_all_outcomes([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)], || {
+        F32::from(F64::nan(Pos, Quiet, 0).as_f64() as f32)
+    });
     // The preferred payload is always a possibility.
     check_all_outcomes(
-        HashSet::from_iter([
+        [
             F32::nan(Pos, Quiet, 0),
             F32::nan(Neg, Quiet, 0),
             F32::nan(Pos, Quiet, all1_payload_32),
             F32::nan(Neg, Quiet, all1_payload_32),
-        ]),
+        ],
         || F32::from(F64::nan(Pos, Quiet, all1_payload_64).as_f64() as f32),
     );
     // If the input is signaling, then the output *may* also be signaling.
     check_all_outcomes(
-        HashSet::from_iter([
+        [
             F32::nan(Pos, Quiet, 0),
             F32::nan(Neg, Quiet, 0),
             F32::nan(Pos, Quiet, all1_payload_32),
             F32::nan(Neg, Quiet, all1_payload_32),
             F32::nan(Pos, Signaling, all1_payload_32),
             F32::nan(Neg, Signaling, all1_payload_32),
-        ]),
+        ],
         || F32::from(F64::nan(Pos, Signaling, all1_payload_64).as_f64() as f32),
     );
     // Check that the low bits are gone (not the high bits).
+    check_all_outcomes([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)], || {
+        F32::from(F64::nan(Pos, Quiet, 1).as_f64() as f32)
+    });
     check_all_outcomes(
-        HashSet::from_iter([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)]),
-        || F32::from(F64::nan(Pos, Quiet, 1).as_f64() as f32),
-    );
-    check_all_outcomes(
-        HashSet::from_iter([
+        [
             F32::nan(Pos, Quiet, 0),
             F32::nan(Neg, Quiet, 0),
             F32::nan(Pos, Quiet, 1),
             F32::nan(Neg, Quiet, 1),
-        ]),
+        ],
         || F32::from(F64::nan(Pos, Quiet, 1 << (51 - 22)).as_f64() as f32),
     );
     check_all_outcomes(
-        HashSet::from_iter([
+        [
             F32::nan(Pos, Quiet, 0),
             F32::nan(Neg, Quiet, 0),
             // The `1` payload becomes `0`, and the `0` payload cannot be signaling,
             // so these are the only options.
-        ]),
+        ],
         || F32::from(F64::nan(Pos, Signaling, 1).as_f64() as f32),
     );
 
     // 32-to-64
-    check_all_outcomes(
-        HashSet::from_iter([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)]),
-        || F64::from(F32::nan(Pos, Quiet, 0).as_f32() as f64),
-    );
+    check_all_outcomes([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)], || {
+        F64::from(F32::nan(Pos, Quiet, 0).as_f32() as f64)
+    });
     // The preferred payload is always a possibility.
     // Also checks that 0s are added on the right.
     check_all_outcomes(
-        HashSet::from_iter([
+        [
             F64::nan(Pos, Quiet, 0),
             F64::nan(Neg, Quiet, 0),
             F64::nan(Pos, Quiet, left1_payload_64),
             F64::nan(Neg, Quiet, left1_payload_64),
-        ]),
+        ],
         || F64::from(F32::nan(Pos, Quiet, all1_payload_32).as_f32() as f64),
     );
     // If the input is signaling, then the output *may* also be signaling.
     check_all_outcomes(
-        HashSet::from_iter([
+        [
             F64::nan(Pos, Quiet, 0),
             F64::nan(Neg, Quiet, 0),
             F64::nan(Pos, Quiet, left1_payload_64),
             F64::nan(Neg, Quiet, left1_payload_64),
             F64::nan(Pos, Signaling, left1_payload_64),
             F64::nan(Neg, Signaling, left1_payload_64),
-        ]),
+        ],
         || F64::from(F32::nan(Pos, Signaling, all1_payload_32).as_f32() as f64),
     );
 }
@@ -552,48 +534,35 @@ fn test_simd() {
     use std::simd::*;
 
     let nan = F32::nan(Neg, Quiet, 0).as_f32();
-    check_all_outcomes(
-        HashSet::from_iter([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)]),
-        || F32::from(unsafe { simd_div(f32x4::splat(0.0), f32x4::splat(0.0)) }[0]),
-    );
-    check_all_outcomes(
-        HashSet::from_iter([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)]),
-        || F32::from(unsafe { simd_fmin(f32x4::splat(nan), f32x4::splat(nan)) }[0]),
-    );
-    check_all_outcomes(
-        HashSet::from_iter([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)]),
-        || F32::from(unsafe { simd_fmax(f32x4::splat(nan), f32x4::splat(nan)) }[0]),
-    );
-    check_all_outcomes(
-        HashSet::from_iter([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)]),
-        || {
-            F32::from(
-                unsafe { simd_fma(f32x4::splat(nan), f32x4::splat(nan), f32x4::splat(nan)) }[0],
-            )
-        },
-    );
-    check_all_outcomes(
-        HashSet::from_iter([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)]),
-        || F32::from(unsafe { simd_reduce_add_ordered::<_, f32>(f32x4::splat(nan), nan) }),
-    );
-    check_all_outcomes(
-        HashSet::from_iter([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)]),
-        || F32::from(unsafe { simd_reduce_max::<_, f32>(f32x4::splat(nan)) }),
-    );
-    check_all_outcomes(
-        HashSet::from_iter([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)]),
-        || F32::from(unsafe { simd_fsqrt(f32x4::splat(nan)) }[0]),
-    );
-    check_all_outcomes(
-        HashSet::from_iter([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)]),
-        || F32::from(unsafe { simd_ceil(f32x4::splat(nan)) }[0]),
-    );
+    check_all_outcomes([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)], || {
+        F32::from(unsafe { simd_div(f32x4::splat(0.0), f32x4::splat(0.0)) }[0])
+    });
+    check_all_outcomes([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)], || {
+        F32::from(unsafe { simd_fmin(f32x4::splat(nan), f32x4::splat(nan)) }[0])
+    });
+    check_all_outcomes([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)], || {
+        F32::from(unsafe { simd_fmax(f32x4::splat(nan), f32x4::splat(nan)) }[0])
+    });
+    check_all_outcomes([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)], || {
+        F32::from(unsafe { simd_fma(f32x4::splat(nan), f32x4::splat(nan), f32x4::splat(nan)) }[0])
+    });
+    check_all_outcomes([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)], || {
+        F32::from(unsafe { simd_reduce_add_ordered::<_, f32>(f32x4::splat(nan), nan) })
+    });
+    check_all_outcomes([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)], || {
+        F32::from(unsafe { simd_reduce_max::<_, f32>(f32x4::splat(nan)) })
+    });
+    check_all_outcomes([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)], || {
+        F32::from(unsafe { simd_fsqrt(f32x4::splat(nan)) }[0])
+    });
+    check_all_outcomes([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)], || {
+        F32::from(unsafe { simd_ceil(f32x4::splat(nan)) }[0])
+    });
 
     // Casts
-    check_all_outcomes(
-        HashSet::from_iter([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)]),
-        || F64::from(unsafe { simd_cast::<f32x4, f64x4>(f32x4::splat(nan)) }[0]),
-    );
+    check_all_outcomes([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)], || {
+        F64::from(unsafe { simd_cast::<f32x4, f64x4>(f32x4::splat(nan)) }[0])
+    });
 }
 
 fn main() {
diff --git a/src/tools/miri/tests/pass/weak_memory/weak.rs b/src/tools/miri/tests/pass/weak_memory/weak.rs
deleted file mode 100644
index 199f83f0528..00000000000
--- a/src/tools/miri/tests/pass/weak_memory/weak.rs
+++ /dev/null
@@ -1,151 +0,0 @@
-//@compile-flags: -Zmiri-ignore-leaks -Zmiri-fixed-schedule
-
-// Tests showing weak memory behaviours are exhibited. All tests
-// return true when the desired behaviour is seen.
-// This is scheduler and pseudo-RNG dependent, so each test is
-// run multiple times until one try returns true.
-// 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
-}
-
-fn relaxed(initial_read: bool) -> bool {
-    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). The last case is boring and we cover the other two.
-    r2 == if initial_read { 0 } else { 1 }
-}
-
-// https://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2017/POPL.pdf Figure 8
-fn seq_cst() -> bool {
-    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();
-
-    r3 == 1
-}
-
-fn initialization_write(add_fence: bool) -> bool {
-    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 == 11
-}
-
-fn faa_replaced_by_load() -> bool {
-    // Example from https://github.com/llvm/llvm-project/issues/56450#issuecomment-1183695905
-    #[no_mangle]
-    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);
-
-    // Since each thread is so short, we need to make sure that they truely run at the same time
-    // Otherwise t1 will finish before t2 even starts
-    let go = static_atomic(0);
-
-    let t1 = spawn(move || {
-        spin_until(go, 1);
-        rdmw(y, x, z)
-    });
-
-    let t2 = spawn(move || {
-        spin_until(go, 1);
-        rdmw(z, x, y)
-    });
-
-    go.store(1, Relaxed);
-
-    let a = t1.join().unwrap();
-    let b = t2.join().unwrap();
-    (a, b) == (0, 0)
-}
-
-/// Asserts that the function returns true at least once in 100 runs
-#[track_caller]
-fn assert_once(f: fn() -> bool) {
-    assert!(std::iter::repeat_with(|| f()).take(100).any(|x| x));
-}
-
-pub fn main() {
-    assert_once(|| relaxed(false));
-    assert_once(|| relaxed(true));
-    assert_once(seq_cst);
-    assert_once(|| initialization_write(false));
-    assert_once(|| initialization_write(true));
-    assert_once(faa_replaced_by_load);
-}