From 0e0b254df9b6f7abe4aa0efa8617ac97baa2bea7 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Wed, 10 Sep 2025 16:16:49 +0200 Subject: [PATCH] ensure we do not see the inconsistent execution from Figure 8 --- src/tools/miri/tests/pass/0weak_memory_consistency.rs | 3 ++- src/tools/miri/tests/pass/weak_memory/weak.rs | 8 ++++++++ 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/src/tools/miri/tests/pass/0weak_memory_consistency.rs b/src/tools/miri/tests/pass/0weak_memory_consistency.rs index 16969d9649c9..142080c1372d 100644 --- a/src/tools/miri/tests/pass/0weak_memory_consistency.rs +++ b/src/tools/miri/tests/pass/0weak_memory_consistency.rs @@ -49,7 +49,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 +/// Test matching https://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2017/POPL.pdf, Figure 7. +/// (The Figure 8 test is in `weak_memory/weak.rs`.) fn test_corr() { let x = static_atomic(0); let y = static_atomic(0); diff --git a/src/tools/miri/tests/pass/weak_memory/weak.rs b/src/tools/miri/tests/pass/weak_memory/weak.rs index 199f83f05286..6794b43bfb37 100644 --- a/src/tools/miri/tests/pass/weak_memory/weak.rs +++ b/src/tools/miri/tests/pass/weak_memory/weak.rs @@ -69,6 +69,9 @@ fn seq_cst() -> bool { 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! + assert!(r3 == 1 || r3 == 3); r3 == 1 } @@ -148,4 +151,9 @@ pub fn main() { assert_once(|| initialization_write(false)); assert_once(|| initialization_write(true)); assert_once(faa_replaced_by_load); + + // Run seq_cst a few more times since it has an assertion we want to ensure holds always. + for _ in 0..50 { + seq_cst(); + } }