blob: 647f209e8bf889c3338f00550c778ddba62d96bc [file] [log] [blame]
//@compile-flags:-Zmiri-deterministic-concurrency
#![feature(core_intrinsics)]
#![feature(custom_mir)]
use std::intrinsics::mir::*;
use std::sync::atomic::Ordering::*;
use std::sync::atomic::*;
use std::thread::JoinHandle;
static P: AtomicPtr<u8> = AtomicPtr::new(core::ptr::null_mut());
fn spawn_thread() -> JoinHandle<()> {
std::thread::spawn(|| {
while P.load(Relaxed).is_null() {
std::hint::spin_loop();
}
unsafe {
// Initialize `*P`.
let ptr = P.load(Relaxed);
*ptr = 127;
//~^ ERROR: Data race detected between (1) creating a new allocation on thread `main` and (2) non-atomic write on thread `unnamed-1`
}
})
}
fn finish(t: JoinHandle<()>, val_ptr: *mut u8) {
P.store(val_ptr, Relaxed);
// Wait for the thread to be done.
t.join().unwrap();
// Read initialized value.
assert_eq!(unsafe { *val_ptr }, 127);
}
#[custom_mir(dialect = "runtime", phase = "optimized")]
fn main() {
mir! {
let t;
let val;
let val_ptr;
let _ret;
{
Call(t = spawn_thread(), ReturnTo(after_spawn), UnwindContinue())
}
after_spawn = {
// This races with the write in the other thread.
StorageLive(val);
val_ptr = &raw mut val;
Call(_ret = finish(t, val_ptr), ReturnTo(done), UnwindContinue())
}
done = {
Return()
}
}
}