Skip to content

Commit ed32b26

Browse files
JCTyblaiddJCTyblaidd
committed
Add tests, and fix bug in atomic RMW relaxed stores
1 parent 89814f1 commit ed32b26

File tree

16 files changed

+315
-11
lines changed

16 files changed

+315
-11
lines changed

‎src/data_race.rs‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -404,8 +404,9 @@ impl AtomicReleaseSequences {
404404
fn clear_and_retain(&mut self, thread: ThreadId) {
405405
match self {
406406
Self::ReleaseOneOrEmpty(id, rel_clock) => {
407-
// Keep or forget depending on id
408-
if *id == Some(thread) {
407+
// If the id is the same, then reatin the value
408+
// otherwise delete and clear the release vector clock
409+
if *id != Some(thread) {
409410
*id = None;
410411
rel_clock.set_zero_vector();
411412
}

‎src/shims/posix/thread.rs‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,7 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
1515
let this = self.eval_context_mut();
1616

1717
this.tcx.sess.warn(
18-
"thread support is experimental. \
19-
For example, Miri does not detect data races yet.",
18+
"thread support is experimental.",
2019
);
2120

2221
// Create the new thread

‎tests/compile-fail/data_race/read_write_race.rs‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
2+
use std::thread::spawn;
3+
4+
#[derive(Copy, Clone)]
5+
struct EvilSend<T>(pub T);
6+
7+
unsafe impl<T> Send for EvilSend<T> {}
8+
unsafe impl<T> Sync for EvilSend<T> {}
9+
10+
pub fn main() {
11+
let mut a = 0u32;
12+
let b = &mut a as *mut u32;
13+
let c = EvilSend(b);
14+
unsafe {
15+
let j1 = spawn(move || {
16+
*c.0
17+
});
18+
19+
let j2 = spawn(move || {
20+
*c.0 = 64; //~ ERROR Data race
21+
});
22+
23+
j1.join().unwrap();
24+
j2.join().unwrap();
25+
}
26+
}

‎tests/compile-fail/data_race/relax_acquire_race.rs‎

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
2+
use std::thread::spawn;
3+
use std::sync::atomic::{AtomicUsize, Ordering};
4+
5+
#[derive(Copy, Clone)]
6+
struct EvilSend<T>(pub T);
7+
8+
unsafe impl<T> Send for EvilSend<T> {}
9+
unsafe impl<T> Sync for EvilSend<T> {}
10+
11+
static SYNC: AtomicUsize = AtomicUsize::new(0);
12+
13+
pub fn main() {
14+
let mut a = 0u32;
15+
let b = &mut a as *mut u32;
16+
let c = EvilSend(b);
17+
18+
unsafe {
19+
let j1 = spawn(move || {
20+
*c.0 = 1;
21+
SYNC.store(1, Ordering::Release);
22+
});
23+
24+
let j2 = spawn(move || {
25+
if SYNC.load(Ordering::Acquire) == 1 {
26+
SYNC.store(2, Ordering::Relaxed);
27+
}
28+
});
29+
30+
let j3 = spawn(move || {
31+
if SYNC.load(Ordering::Acquire) == 2 {
32+
*c.0 //~ ERROR Data race
33+
}else{
34+
0
35+
}
36+
});
37+
38+
j1.join().unwrap();
39+
j2.join().unwrap();
40+
j3.join().unwrap();
41+
}
42+
}

‎tests/compile-fail/data_race/release_seq_race.rs‎

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
// compile-flags: -Zmiri-disable-isolation
2+
3+
use std::thread::{spawn, sleep};
4+
use std::sync::atomic::{AtomicUsize, Ordering};
5+
use std::time::Duration;
6+
7+
#[derive(Copy, Clone)]
8+
struct EvilSend<T>(pub T);
9+
10+
unsafe impl<T> Send for EvilSend<T> {}
11+
unsafe impl<T> Sync for EvilSend<T> {}
12+
13+
static SYNC: AtomicUsize = AtomicUsize::new(0);
14+
15+
pub fn main() {
16+
let mut a = 0u32;
17+
let b = &mut a as *mut u32;
18+
let c = EvilSend(b);
19+
20+
unsafe {
21+
let j1 = spawn(move || {
22+
*c.0 = 1;
23+
SYNC.store(1, Ordering::Release);
24+
sleep(Duration::from_millis(100));
25+
SYNC.store(3, Ordering::Relaxed);
26+
});
27+
28+
let j2 = spawn(move || {
29+
// Blocks the acquire-release sequence
30+
SYNC.store(2, Ordering::Relaxed);
31+
});
32+
33+
let j3 = spawn(move || {
34+
sleep(Duration::from_millis(1000));
35+
if SYNC.load(Ordering::Acquire) == 3 {
36+
*c.0 //~ ERROR Data race
37+
}else{
38+
0
39+
}
40+
});
41+
42+
j1.join().unwrap();
43+
j2.join().unwrap();
44+
j3.join().unwrap();
45+
}
46+
}

‎tests/compile-fail/data_race/rmw_race.rs‎

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
2+
use std::thread::spawn;
3+
use std::sync::atomic::{AtomicUsize, Ordering};
4+
5+
#[derive(Copy, Clone)]
6+
struct EvilSend<T>(pub T);
7+
8+
unsafe impl<T> Send for EvilSend<T> {}
9+
unsafe impl<T> Sync for EvilSend<T> {}
10+
11+
static SYNC: AtomicUsize = AtomicUsize::new(0);
12+
13+
pub fn main() {
14+
let mut a = 0u32;
15+
let b = &mut a as *mut u32;
16+
let c = EvilSend(b);
17+
18+
unsafe {
19+
let j1 = spawn(move || {
20+
*c.0 = 1;
21+
SYNC.store(1, Ordering::Release);
22+
});
23+
24+
let j2 = spawn(move || {
25+
if SYNC.swap(2, Ordering::Relaxed) == 1 {
26+
// Blocks the acquire-release sequence
27+
SYNC.store(3, Ordering::Relaxed);
28+
}
29+
});
30+
31+
let j3 = spawn(move || {
32+
if SYNC.load(Ordering::Acquire) == 3 {
33+
*c.0 //~ ERROR Data race
34+
}else{
35+
0
36+
}
37+
});
38+
39+
j1.join().unwrap();
40+
j2.join().unwrap();
41+
j3.join().unwrap();
42+
}
43+
}

‎tests/compile-fail/data_race/write_write_race.rs‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
2+
use std::thread::spawn;
3+
4+
#[derive(Copy, Clone)]
5+
struct EvilSend<T>(pub T);
6+
7+
unsafe impl<T> Send for EvilSend<T> {}
8+
unsafe impl<T> Sync for EvilSend<T> {}
9+
10+
pub fn main() {
11+
let mut a = 0u32;
12+
let b = &mut a as *mut u32;
13+
let c = EvilSend(b);
14+
unsafe {
15+
let j1 = spawn(move || {
16+
*c.0 = 32;
17+
});
18+
19+
let j2 = spawn(move || {
20+
*c.0 = 64; //~ ERROR Data race
21+
});
22+
23+
j1.join().unwrap();
24+
j2.join().unwrap();
25+
}
26+
}

‎tests/run-pass/concurrency/data_race.rs‎

Lines changed: 119 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,119 @@
1+
use std::sync::atomic::{AtomicUsize, fence, Ordering};
2+
use std::thread::spawn;
3+
4+
#[derive(Copy, Clone)]
5+
struct EvilSend<T>(pub T);
6+
7+
unsafe impl<T> Send for EvilSend<T> {}
8+
unsafe impl<T> Sync for EvilSend<T> {}
9+
10+
static SYNC: AtomicUsize = AtomicUsize::new(0);
11+
12+
fn test_fence_sync() {
13+
let mut var = 0u32;
14+
let ptr = &mut var as *mut u32;
15+
let evil_ptr = EvilSend(ptr);
16+
17+
18+
let j1 = spawn(move || {
19+
unsafe { *evil_ptr.0 = 1; }
20+
fence(Ordering::Release);
21+
SYNC.store(1, Ordering::Relaxed)
22+
});
23+
24+
let j2 = spawn(move || {
25+
if SYNC.load(Ordering::Relaxed) == 1 {
26+
fence(Ordering::Acquire);
27+
unsafe { *evil_ptr.0 }
28+
}else{
29+
0
30+
}
31+
});
32+
33+
j1.join().unwrap();
34+
j2.join().unwrap();
35+
}
36+
37+
38+
fn test_multiple_reads() {
39+
let mut var = 42u32;
40+
let ptr = &mut var as *mut u32;
41+
let evil_ptr = EvilSend(ptr);
42+
43+
let j1 = spawn(move || unsafe {*evil_ptr.0});
44+
let j2 = spawn(move || unsafe {*evil_ptr.0});
45+
let j3 = spawn(move || unsafe {*evil_ptr.0});
46+
let j4 = spawn(move || unsafe {*evil_ptr.0});
47+
48+
assert_eq!(j1.join().unwrap(), 42);
49+
assert_eq!(j2.join().unwrap(), 42);
50+
assert_eq!(j3.join().unwrap(), 42);
51+
assert_eq!(j4.join().unwrap(), 42);
52+
53+
var = 10;
54+
assert_eq!(var, 10);
55+
}
56+
57+
pub fn test_rmw_no_block() {
58+
let mut a = 0u32;
59+
let b = &mut a as *mut u32;
60+
let c = EvilSend(b);
61+
62+
unsafe {
63+
let j1 = spawn(move || {
64+
*c.0 = 1;
65+
SYNC.store(1, Ordering::Release);
66+
});
67+
68+
let j2 = spawn(move || {
69+
if SYNC.swap(2, Ordering::Relaxed) == 1 {
70+
//No op, blocking store removed
71+
}
72+
});
73+
74+
let j3 = spawn(move || {
75+
if SYNC.load(Ordering::Acquire) == 2 {
76+
*c.0
77+
}else{
78+
0
79+
}
80+
});
81+
82+
j1.join().unwrap();
83+
j2.join().unwrap();
84+
let v = j3.join().unwrap();
85+
assert!(v == 1 || v == 2);
86+
}
87+
}
88+
89+
pub fn test_release_no_block() {
90+
let mut a = 0u32;
91+
let b = &mut a as *mut u32;
92+
let c = EvilSend(b);
93+
94+
unsafe {
95+
let j1 = spawn(move || {
96+
*c.0 = 1;
97+
SYNC.store(1, Ordering::Release);
98+
SYNC.store(3, Ordering::Relaxed);
99+
});
100+
101+
let j2 = spawn(move || {
102+
if SYNC.load(Ordering::Acquire) == 3 {
103+
*c.0
104+
}else{
105+
0
106+
}
107+
});
108+
109+
j1.join().unwrap();
110+
assert_eq!(j2.join().unwrap(),1);
111+
}
112+
}
113+
114+
pub fn main() {
115+
test_fence_sync();
116+
test_multiple_reads();
117+
test_rmw_no_block();
118+
test_release_no_block();
119+
}

‎tests/run-pass/concurrency/data_race.stderr‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
warning: thread support is experimental.
2+

‎tests/run-pass/concurrency/linux-futex.stderr‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,2 @@
1-
warning: thread support is experimental. For example, Miri does not detect data races yet.
1+
warning: thread support is experimental.
22

0 commit comments

Comments
 (0)