blob: d9897a1033fbeb5418869b22b6a415abc98393f5 [file] [log] [blame]
//@compile-flags: -Zmiri-tree-borrows
// This test relies on a specific interleaving that cannot be enforced
// with just barriers. We must remove preemption so that the execution and the
// error messages are deterministic.
//@compile-flags: -Zmiri-preemption-rate=0
use std::ptr::addr_of_mut;
use std::sync::{Arc, Barrier};
use std::thread;
#[derive(Copy, Clone)]
struct SendPtr(*mut u8);
unsafe impl Send for SendPtr {}
// This test features the problematic pattern
//
// read x || retag y (&mut, protect)
// -- sync --
// || write y
//
// In which
// - one interleaving (`1:read; 2:retag; 2:write`) does not have UB if retags
// count only as reads for the data race model,
// - the other interleaving (`2:retag; 1:read; 2:write`) has UB (`noalias` violation).
//
// The interleaving executed here is the one that does not have UB,
// i.e.
// 1:read x
// 2:retag y
// 2:write y
//
// Tree Borrows considers that the read of `x` cannot be in conflict
// with `y` because `y` did not even exist yet when `x` was accessed.
//
// As long as we are not emitting any writes for the data race model
// upon retags of mutable references, it should not have any issue with
// this code either.
// We do not want to emit a write for the data race model, because
// although there is race-like behavior going on in this pattern
// (where some but not all interleavings contain UB), making this an actual
// data race has the confusing consequence of one single access being treated
// as being of different `AccessKind`s by different parts of Miri
// (a retag would be always a read for the aliasing model, and sometimes a write
// for the data race model).
// The other interleaving is a subsequence of `tests/fail/tree_borrows/spurious_read.rs`
// which asserts that
// 2:retag y
// 1:read x
// 2:write y
// is UB.
type IdxBarrier = (usize, Arc<Barrier>);
// 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();
}};
}
fn thread_1(x: SendPtr, barrier: IdxBarrier) {
let x = unsafe { &mut *x.0 };
synchronized!(barrier, "spawn");
synchronized!(barrier, "read x || retag y");
// This is the interleaving without UB: by the time
// the other thread starts retagging, this thread
// has already finished all its work using `y`.
let _v = *x;
synchronized!(barrier, "write y");
synchronized!(barrier, "exit");
}
fn thread_2(y: SendPtr, barrier: IdxBarrier) {
let y = unsafe { &mut *y.0 };
synchronized!(barrier, "spawn");
fn write(y: &mut u8, v: u8, barrier: &IdxBarrier) {
synchronized!(barrier, "write y");
*y = v;
}
synchronized!(barrier, "read x || retag y");
// We don't use a barrier here so that *if* the retag counted as a write
// for the data race model, then it would be UB.
// We still want to make sure that the other thread goes first as per the
// interleaving that we are testing, so we use `yield_now + preemption-rate=0`
// which has the effect of forcing a specific interleaving while still
// not counting as "synchronization" from the point of view of the data
// race model.
thread::yield_now();
write(&mut *y, 42, &barrier);
synchronized!(barrier, "exit");
}
fn main() {
let mut data = 0u8;
let p = SendPtr(addr_of_mut!(data));
let barrier = Arc::new(Barrier::new(2));
let b1 = (1, Arc::clone(&barrier));
let b2 = (2, Arc::clone(&barrier));
let h1 = thread::spawn(move || thread_1(p, b1));
let h2 = thread::spawn(move || thread_2(p, b2));
h1.join().unwrap();
h2.join().unwrap();
}