1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
|
// We ensure a deterministic execution.
// Note that we are *also* using barriers: the barriers enforce the
// specific interleaving of operations that we want, but only the preemption
// rate guarantees that the error message is also deterministic.
//@compile-flags: -Zmiri-deterministic-concurrency
//@compile-flags: -Zmiri-tree-borrows
use std::sync::{Arc, Barrier};
use std::thread;
// A way to send raw pointers across threads.
// Note that when using this in closures will require explicit copying
// `let ptr = ptr;` to force the borrow checker to copy the `Send` wrapper
// instead of just copying the inner `!Send` field.
#[derive(Copy, Clone)]
struct SendPtr(*mut u8);
unsafe impl Send for SendPtr {}
fn main() {
retagx_retagy_spuriousx_retx_rety_writey();
}
// We're going to enforce a specific interleaving of two
// threads, we use this macro in an effort to make it feasible
// to check in the output that the execution is properly synchronized.
//
// Provide `synchronized!(thread, msg)` where thread is
// a `(thread_id: usize, barrier: Arc<Barrier>)`, and `msg` the message
// to be displayed when the thread reaches this point in the execution.
macro_rules! synchronized {
($thread:expr, $msg:expr) => {{
let (thread_id, barrier) = &$thread;
eprintln!("Thread {} executing: {}", thread_id, $msg);
barrier.wait();
}};
}
// Interleaving:
// retag x (protect)
// retag y (protect)
// spurious read x (target only, which we are executing)
// ret x
// ret y
// write y
//
// This is an interleaving that will never have UB in the source
// (`x` is never accessed for the entire time that `y` is protected).
// For the spurious read to be allowed, we need to check that there is
// no UB in the target (i.e., *with* the spurious read).
//
// The interleaving differs from the one in `tests/fail/tree_borrows/spurious_read.rs` only
// in that it has the `write y` while `y` is no longer protected.
// When the write occurs after protection ends, both source and target are fine
// (checked by this test); when the write occurs during protection, both source
// and target are UB (checked by the `fail` test).
fn retagx_retagy_spuriousx_retx_rety_writey() {
let mut data = 0u8;
let ptr = SendPtr(std::ptr::addr_of_mut!(data));
let barrier = Arc::new(Barrier::new(2));
let bx = Arc::clone(&barrier);
let by = Arc::clone(&barrier);
// This thread only needs to
// - retag `x` protected
// - do a read through `x`
// - remove `x`'s protector
// Most of the complexity here is synchronization.
let thread_x = thread::spawn(move || {
let b = (1, bx);
synchronized!(b, "start");
let ptr = ptr;
synchronized!(b, "retag x (&mut, protect)");
fn as_mut(x: &mut u8, b: (usize, Arc<Barrier>)) -> *mut u8 {
synchronized!(b, "retag y (&mut, protect)");
synchronized!(b, "spurious read x");
let _v = *x;
synchronized!(b, "ret x");
let x = x as *mut u8;
x
}
let _x = as_mut(unsafe { &mut *ptr.0 }, b.clone());
synchronized!(b, "ret y");
synchronized!(b, "write y");
synchronized!(b, "end");
});
// This thread's job is to
// - retag `y` protected
// - (wait a bit that the other thread performs its spurious read)
// - remove `y`'s protector
// - attempt a write through `y`.
let thread_y = thread::spawn(move || {
let b = (2, by);
synchronized!(b, "start");
let ptr = ptr;
synchronized!(b, "retag x (&mut, protect)");
synchronized!(b, "retag y (&mut, protect)");
fn as_mut(y: &mut u8, b: (usize, Arc<Barrier>)) -> *mut u8 {
synchronized!(b, "spurious read x");
synchronized!(b, "ret x");
let y = y as *mut u8;
y
}
let y = as_mut(unsafe { &mut *ptr.0 }, b.clone());
synchronized!(b, "ret y");
synchronized!(b, "write y");
unsafe {
*y = 2;
}
synchronized!(b, "end");
});
thread_x.join().unwrap();
thread_y.join().unwrap();
}
|
