Skip to content

Commit bf6ad4f

Browse files
committed
simplify miri weak memory test
1 parent f746dba commit bf6ad4f

File tree

1 file changed

+72
-43
lines changed
  • src/tools/miri/tests/pass/weak_memory

1 file changed

+72
-43
lines changed

src/tools/miri/tests/pass/weak_memory/weak.rs

+72-43
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@
99

1010
use std::sync::atomic::Ordering::*;
1111
use std::sync::atomic::{AtomicUsize, fence};
12-
use std::thread::{spawn, yield_now};
12+
use std::thread::{spawn, scope, yield_now};
1313

1414
#[allow(dead_code)]
1515
#[derive(Copy, Clone)]
@@ -31,67 +31,97 @@ fn reads_value(loc: &AtomicUsize, val: usize) -> usize {
3131
val
3232
}
3333

34+
/// Runs a, b and c in order, but without establishing any synchronization
35+
/// between them.
36+
fn execute_unsynchronized<R: Send>(
37+
a: impl FnOnce() + Send,
38+
b: impl FnOnce() + Send,
39+
c: impl FnOnce() -> R + Send,
40+
) -> R {
41+
scope(|s| {
42+
let t1 = s.spawn(|| {
43+
// Make sure that T2 starts...
44+
yield_now();
45+
a();
46+
// ... and run T2.
47+
yield_now();
48+
});
49+
let t2 = s.spawn(|| {
50+
// Make sure that T2 starts...
51+
yield_now();
52+
b();
53+
// ... and run T2.
54+
yield_now();
55+
});
56+
let t3 = s.spawn(|| {
57+
// Continue with T1.
58+
yield_now();
59+
c()
60+
});
61+
62+
// This will cause T1 to be run.
63+
t1.join().unwrap();
64+
t2.join().unwrap();
65+
t3.join().unwrap()
66+
})
67+
}
68+
3469
fn relaxed(initial_read: bool) -> bool {
3570
let x = static_atomic(0);
36-
let j = spawn(move || x.load(Relaxed));
3771

38-
x.store(1, Relaxed);
39-
// Preemption is disabled, so the store above will never be the
40-
// latest store visible to the other thread.
41-
x.store(2, Relaxed);
42-
43-
let r = j.join().unwrap();
72+
let r = execute_unsynchronized(
73+
|| {
74+
x.store(1, Relaxed);
75+
// Preemption is disabled, so the store above will never be the
76+
// latest store visible to the other thread.
77+
x.store(2, Relaxed);
78+
},
79+
|| {},
80+
|| x.load(Relaxed)
81+
);
4482

4583
// There are three possible values here: 0 (from the initial read), 1 (from the first relaxed
4684
// read), and 2 (the last read). The last case is boring and we cover the other two.
4785
r == if initial_read { 0 } else { 1 }
4886
}
4987

5088
// https://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2017/POPL.pdf Figure 8
51-
fn seq_cst(relaxed_write: bool) -> bool {
89+
fn seq_cst() -> bool {
5290
let x = static_atomic(0);
5391

54-
let j1 = spawn(move || {
55-
// Make the second thread execute without synchronizing with it.
56-
// After that, the initial thread will continue executing.
57-
yield_now();
58-
// This can either load the relaxed write or the second SC-write, but
59-
// not the first, as that would violate the ordering guarantee.
60-
x.load(SeqCst)
61-
});
62-
let j2 = spawn(move || x.store(1, Relaxed));
63-
64-
// Make the first thread execute.
65-
yield_now();
66-
x.store(2, SeqCst);
67-
x.store(3, SeqCst);
68-
69-
j2.join().unwrap();
70-
let r = j1.join().unwrap();
92+
let r = execute_unsynchronized(
93+
|| x.store(1, Relaxed),
94+
|| {
95+
x.store(2, SeqCst);
96+
x.store(3, SeqCst);
97+
},
98+
|| x.load(SeqCst),
99+
);
71100

72-
assert_ne!(r, 2);
73-
r == if relaxed_write { 1 } else { 3 }
101+
r == 1
74102
}
75103

76104
fn initialization_write(add_fence: bool) -> bool {
77105
let x = static_atomic(11);
78106

79107
let wait = static_atomic(0);
80108

81-
let j = spawn(move || {
82-
reads_value(wait, 1);
83-
if add_fence {
84-
fence(AcqRel);
109+
let r = execute_unsynchronized(
110+
|| {
111+
x.store(22, Relaxed);
112+
// Relaxed is intentional. We want to test if the other thread reads
113+
// the initialisation write after a relaxed write
114+
wait.store(1, Relaxed);
115+
},
116+
|| {},
117+
|| {
118+
reads_value(wait, 1);
119+
if add_fence {
120+
fence(AcqRel);
121+
}
122+
x.load(Relaxed)
85123
}
86-
x.load(Relaxed)
87-
});
88-
89-
x.store(22, Relaxed);
90-
// Relaxed is intentional. We want to test if the thread 2 reads the initialisation write
91-
// after a relaxed write
92-
wait.store(1, Relaxed);
93-
94-
let r = j.join().unwrap();
124+
);
95125

96126
r == 11
97127
}
@@ -146,8 +176,7 @@ fn assert_once(f: fn() -> bool) {
146176
pub fn main() {
147177
assert_once(|| relaxed(false));
148178
assert_once(|| relaxed(true));
149-
assert_once(|| seq_cst(false));
150-
assert_once(|| seq_cst(true));
179+
assert_once(seq_cst);
151180
assert_once(|| initialization_write(false));
152181
assert_once(|| initialization_write(true));
153182
assert_once(faa_replaced_by_load);

0 commit comments

Comments
 (0)