Skip to content

Commit f746dba

Browse files
committed
fix miri weak memory tests
1 parent 6e2d4b7 commit f746dba

File tree

3 files changed

+44
-44
lines changed

3 files changed

+44
-44
lines changed

src/tools/miri/tests/fail/weak_memory/weak_uninit.rs

+3-6
Original file line numberDiff line numberDiff line change
@@ -24,14 +24,11 @@ fn static_uninit_atomic() -> &'static AtomicUsize {
2424

2525
fn relaxed() {
2626
let x = static_uninit_atomic();
27-
let j1 = spawn(move || {
28-
x.store(1, Ordering::Relaxed);
29-
});
27+
let j = spawn(move || x.load(Ordering::Relaxed)); //~ERROR: using uninitialized data
3028

31-
let j2 = spawn(move || x.load(Ordering::Relaxed)); //~ERROR: using uninitialized data
29+
x.store(1, Ordering::Relaxed);
3230

33-
j1.join().unwrap();
34-
j2.join().unwrap();
31+
j.join().unwrap();
3532
}
3633

3734
pub fn main() {

src/tools/miri/tests/fail/weak_memory/weak_uninit.stderr

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
error: Undefined Behavior: using uninitialized data, but this operation requires initialized memory
22
--> tests/fail/weak_memory/weak_uninit.rs:LL:CC
33
|
4-
LL | let j2 = spawn(move || x.load(Ordering::Relaxed));
5-
| ^^^^^^^^^^^^^^^^^^^^^^^^^ using uninitialized data, but this operation requires initialized memory
4+
LL | let j = spawn(move || x.load(Ordering::Relaxed));
5+
| ^^^^^^^^^^^^^^^^^^^^^^^^^ using uninitialized data, but this operation requires initialized memory
66
|
77
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
88
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information

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

+39-36
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;
12+
use std::thread::{spawn, yield_now};
1313

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

3434
fn relaxed(initial_read: bool) -> bool {
3535
let x = static_atomic(0);
36-
let j1 = spawn(move || {
37-
x.store(1, Relaxed);
38-
// Preemption is disabled, so the store above will never be the
39-
// latest store visible to another thread.
40-
x.store(2, Relaxed);
41-
});
36+
let j = spawn(move || x.load(Relaxed));
4237

43-
let j2 = spawn(move || x.load(Relaxed));
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);
4442

45-
j1.join().unwrap();
46-
let r2 = j2.join().unwrap();
43+
let r = j.join().unwrap();
4744

4845
// There are three possible values here: 0 (from the initial read), 1 (from the first relaxed
4946
// read), and 2 (the last read). The last case is boring and we cover the other two.
50-
r2 == if initial_read { 0 } else { 1 }
47+
r == if initial_read { 0 } else { 1 }
5148
}
5249

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

5754
let j1 = spawn(move || {
58-
x.store(1, Relaxed);
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)
5961
});
62+
let j2 = spawn(move || x.store(1, Relaxed));
6063

61-
let j2 = spawn(move || {
62-
x.store(2, SeqCst);
63-
x.store(3, SeqCst);
64-
});
64+
// Make the first thread execute.
65+
yield_now();
66+
x.store(2, SeqCst);
67+
x.store(3, SeqCst);
6568

66-
let j3 = spawn(move || x.load(SeqCst));
67-
68-
j1.join().unwrap();
6969
j2.join().unwrap();
70-
let r3 = j3.join().unwrap();
70+
let r = j1.join().unwrap();
7171

72-
r3 == 1
72+
assert_ne!(r, 2);
73+
r == if relaxed_write { 1 } else { 3 }
7374
}
7475

7576
fn initialization_write(add_fence: bool) -> bool {
7677
let x = static_atomic(11);
7778

7879
let wait = static_atomic(0);
7980

80-
let j1 = spawn(move || {
81-
x.store(22, Relaxed);
82-
// Relaxed is intentional. We want to test if the thread 2 reads the initialisation write
83-
// after a relaxed write
84-
wait.store(1, Relaxed);
85-
});
86-
87-
let j2 = spawn(move || {
81+
let j = spawn(move || {
8882
reads_value(wait, 1);
8983
if add_fence {
9084
fence(AcqRel);
9185
}
9286
x.load(Relaxed)
9387
});
9488

95-
j1.join().unwrap();
96-
let r2 = j2.join().unwrap();
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();
9795

98-
r2 == 11
96+
r == 11
9997
}
10098

10199
fn faa_replaced_by_load() -> bool {
@@ -119,12 +117,16 @@ fn faa_replaced_by_load() -> bool {
119117
let go = static_atomic(0);
120118

121119
let t1 = spawn(move || {
122-
while go.load(Relaxed) == 0 {}
120+
while go.load(Relaxed) == 0 {
121+
yield_now();
122+
}
123123
rdmw(y, x, z)
124124
});
125125

126126
let t2 = spawn(move || {
127-
while go.load(Relaxed) == 0 {}
127+
while go.load(Relaxed) == 0 {
128+
yield_now();
129+
}
128130
rdmw(z, x, y)
129131
});
130132

@@ -144,7 +146,8 @@ fn assert_once(f: fn() -> bool) {
144146
pub fn main() {
145147
assert_once(|| relaxed(false));
146148
assert_once(|| relaxed(true));
147-
assert_once(seq_cst);
149+
assert_once(|| seq_cst(false));
150+
assert_once(|| seq_cst(true));
148151
assert_once(|| initialization_write(false));
149152
assert_once(|| initialization_write(true));
150153
assert_once(faa_replaced_by_load);

0 commit comments

Comments
 (0)