user0/rust
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor weak-mem test to list all expected executions

Browse source
This commit is contained in:
Ralf Jung 2025-09-10 16:31:29 +02:00
parent 0e0b254df9
commit 21e3111ef9
3 changed files with 125 additions and 114 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/tools/miri/tests/pass/0weak_memory_consistency.rs
View file

@ -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

3
src/tools/miri/tests/pass/0weak_memory_consistency_sc.rs
View file

@ -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

233
src/tools/miri/tests/pass/weak_memory/weak.rs
View file

@ -1,9 +1,11 @@
//@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.
// 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.
@ -31,129 +33,136 @@ fn spin_until(loc: &AtomicUsize, val: usize) -> usize {
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);
/// Check that the function produces the intended set of outcomes.
#[track_caller]
fn check_all_outcomes<T: Eq + std::hash::Hash + std::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 N times as many tries as we are expecting values.
let tries = expected.len() * 8;
for _ in 0..tries {
let val = generate();
assert!(expected.contains(&val), "got an unexpected value: {val}");
seen.insert(val);
}
// 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
});
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);
fn seq_cst() {
check_all_outcomes([1, 3], || {
let x = static_atomic(0);
let j1 = spawn(move || {
x.store(1, Relaxed);
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
});
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!
assert!(r3 == 1 || r3 == 3);
r3 == 1
}
fn initialization_write(add_fence: bool) -> bool {
let x = static_atomic(11);
fn initialization_write(add_fence: bool) {
check_all_outcomes([11, 22], || {
let x = static_atomic(11);
let wait = static_atomic(0);
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 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
});
}
let j2 = spawn(move || {
spin_until(wait, 1);
if add_fence {
fence(AcqRel);
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)
}
x.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)
});
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);
// Run seq_cst a few more times since it has an assertion we want to ensure holds always.
for _ in 0..50 {
seq_cst();
}
relaxed();
seq_cst();
initialization_write(false);
initialization_write(true);
faa_replaced_by_load();
}