-
Notifications
You must be signed in to change notification settings - Fork 13k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
miri: treat non-memory local variables properly for data race detection
- Loading branch information
Showing
15 changed files
with
411 additions
and
13 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
57 changes: 57 additions & 0 deletions
57
src/tools/miri/tests/fail/data_race/local_variable_alloc_race.rs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,57 @@ | ||
//@compile-flags: -Zmiri-preemption-rate=0.0 -Zmiri-disable-weak-memory-emulation | ||
#![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() | ||
} | ||
} | ||
} |
Oops, something went wrong.