forked from rust-lang/rust
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Rollup merge of rust-lang#128942 - RalfJung:interpret-weak-memory, r=…
…saethlin miri weak memory emulation: put previous value into initial store buffer Fixes rust-lang/miri#2164 by doing a read before each atomic write so that we can initialize the store buffer. The read suppresses memory access hooks and UB exceptions, to avoid otherwise influencing the program behavior. If the read fails, we store that as `None` in the store buffer, so that when an atomic read races with the first atomic write to some memory and previously the memory was uninitialized, we can report UB due to reading uninit memory. `@cbeuw` this changes a bit the way we initialize the store buffers. Not sure if you still remember all this code, but if you could have a look to make sure this still makes sense, that would be great. :) r? `@saethlin`
- Loading branch information
Showing
6 changed files
with
153 additions
and
109 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,43 @@ | ||
//@compile-flags: -Zmiri-ignore-leaks -Zmiri-preemption-rate=0 | ||
|
||
// Tests showing weak memory behaviours are exhibited. All tests | ||
// return true when the desired behaviour is seen. | ||
// This is scheduler and pseudo-RNG dependent, so each test is | ||
// run multiple times until one try returns true. | ||
// Spurious failure is possible, if you are really unlucky with | ||
// the RNG and always read the latest value from the store buffer. | ||
#![feature(new_uninit)] | ||
|
||
use std::sync::atomic::*; | ||
use std::thread::spawn; | ||
|
||
#[allow(dead_code)] | ||
#[derive(Copy, Clone)] | ||
struct EvilSend<T>(pub T); | ||
|
||
unsafe impl<T> Send for EvilSend<T> {} | ||
unsafe impl<T> Sync for EvilSend<T> {} | ||
|
||
// We can't create static items because we need to run each test multiple times. | ||
fn static_uninit_atomic() -> &'static AtomicUsize { | ||
unsafe { Box::leak(Box::new_uninit()).assume_init_ref() } | ||
} | ||
|
||
fn relaxed() { | ||
let x = static_uninit_atomic(); | ||
let j1 = spawn(move || { | ||
x.store(1, Ordering::Relaxed); | ||
}); | ||
|
||
let j2 = spawn(move || x.load(Ordering::Relaxed)); //~ERROR: using uninitialized data | ||
|
||
j1.join().unwrap(); | ||
j2.join().unwrap(); | ||
} | ||
|
||
pub fn main() { | ||
// If we try often enough, we should hit UB. | ||
for _ in 0..100 { | ||
relaxed(); | ||
} | ||
} |
Oops, something went wrong.