Skip to content

Commit 52b02f9

Browse files
committed
Add a data race test
1 parent 4e806fb commit 52b02f9

File tree

3 files changed

+106
-0
lines changed

3 files changed

+106
-0
lines changed
Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
//@revisions: stack tree
2+
//@[tree]compile-flags: -Zmiri-tree-borrows-strong
3+
use std::sync::{Arc, Barrier};
4+
5+
#[derive(Copy, Clone)]
6+
struct SendPtr(*const u32);
7+
8+
unsafe impl Send for SendPtr {}
9+
10+
type IdxBarrier = (usize, Arc<Barrier>);
11+
12+
// Barriers to enforce the interleaving.
13+
// This macro expects `synchronized!(thread, msg)` where `thread` is a `IdxBarrier`,
14+
// and `msg` is the message to be displayed when the thread reaches this point in the execution.
15+
macro_rules! synchronized {
16+
($thread:expr, $msg:expr) => {{
17+
let (thread_id, barrier) = &$thread;
18+
eprintln!("Thread {} executing: {}", thread_id, $msg);
19+
barrier.wait();
20+
}};
21+
}
22+
23+
fn may_insert_spurious_write(_x: &mut u32, b: IdxBarrier) {
24+
synchronized!(b, "after enter");
25+
synchronized!(b, "before exit");
26+
}
27+
28+
fn main() {
29+
let target = &mut 42;
30+
let target_alias = &*target;
31+
let target_alias_ptr = SendPtr(target_alias as *const _);
32+
33+
let barrier = Arc::new(Barrier::new(2));
34+
let bx = (1, Arc::clone(&barrier));
35+
let by = (2, Arc::clone(&barrier));
36+
37+
let join_handle = std::thread::spawn(move || {
38+
synchronized!(bx, "before read");
39+
let ptr = target_alias_ptr;
40+
// now `target_alias` is invalid
41+
let _val = unsafe { *ptr.0 };
42+
//~[stack]^ ERROR: /read access .* tag does not exist in the borrow stack/
43+
//~[tree]| ERROR: /read access through .* is forbidden/
44+
synchronized!(bx, "after read");
45+
});
46+
47+
may_insert_spurious_write(target, by);
48+
let _ = join_handle.join();
49+
}
Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
Thread 2 executing: after enter
2+
Thread 1 executing: before read
3+
error: Undefined Behavior: attempting a read access using <TAG> at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
4+
--> tests/fail/both_borrows/spurious_write_may_be_added_data_race.rs:LL:CC
5+
|
6+
LL | let _val = unsafe { *ptr.0 };
7+
| ^^^^^^ this error occurs as part of an access at ALLOC[0x0..0x4]
8+
|
9+
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
10+
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
11+
help: <TAG> was created by a SharedReadOnly retag at offsets [0x0..0x4]
12+
--> tests/fail/both_borrows/spurious_write_may_be_added_data_race.rs:LL:CC
13+
|
14+
LL | let target_alias_ptr = SendPtr(target_alias as *const _);
15+
| ^^^^^^^^^^^^
16+
help: <TAG> was later invalidated at offsets [0x0..0x4] by a Unique function-entry retag inside this call
17+
--> tests/fail/both_borrows/spurious_write_may_be_added_data_race.rs:LL:CC
18+
|
19+
LL | may_insert_spurious_write(target, by);
20+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
21+
= note: BACKTRACE (of the first span) on thread `unnamed-ID`:
22+
= note: inside closure at tests/fail/both_borrows/spurious_write_may_be_added_data_race.rs:LL:CC
23+
24+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
25+
26+
error: aborting due to 1 previous error
27+
Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
Thread 2 executing: after enter
2+
Thread 1 executing: before read
3+
error: Undefined Behavior: read access through <TAG> at ALLOC[0x0] is forbidden
4+
--> tests/fail/both_borrows/spurious_write_may_be_added_data_race.rs:LL:CC
5+
|
6+
LL | let _val = unsafe { *ptr.0 };
7+
| ^^^^^^ Undefined Behavior occurred here
8+
|
9+
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
10+
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/tree-borrows.md for further information
11+
= help: the accessed tag <TAG> is foreign to the protected tag <TAG> (i.e., it is not a child)
12+
= help: this foreign read access would cause the protected tag <TAG> (currently Active) to become Disabled
13+
= help: protected tags must never be Disabled
14+
help: the accessed tag <TAG> was created here
15+
--> tests/fail/both_borrows/spurious_write_may_be_added_data_race.rs:LL:CC
16+
|
17+
LL | let target_alias = &*target;
18+
| ^^^^^^^^
19+
help: the protected tag <TAG> was created here, in the initial state Active
20+
--> tests/fail/both_borrows/spurious_write_may_be_added_data_race.rs:LL:CC
21+
|
22+
LL | fn may_insert_spurious_write(_x: &mut u32, b: IdxBarrier) {
23+
| ^^
24+
= note: BACKTRACE (of the first span) on thread `unnamed-ID`:
25+
= note: inside closure at tests/fail/both_borrows/spurious_write_may_be_added_data_race.rs:LL:CC
26+
27+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
28+
29+
error: aborting due to 1 previous error
30+

0 commit comments

Comments
 (0)