Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Weak memory emulation using store buffers #1963

Merged
merged 46 commits into from
Jun 6, 2022
Merged
Changes from 1 commit
Commits
Show all changes
46 commits
Select commit Hold shift + click to select a range
8d36e8b
Add weak memory config option
cbeuw Dec 25, 2021
16315b1
Add test cases
cbeuw Jan 17, 2022
e7698f4
Implement weak memory emulation
cbeuw Dec 27, 2021
aca3b3a
set_at_index sets the default value (0) if index doesn't exist in the…
cbeuw Apr 15, 2022
cf26658
Comment out and provide context to C++20 test
cbeuw Apr 16, 2022
ecdab5f
Clearer boundries between alloc metadata with multiple buffers and an…
cbeuw May 1, 2022
53f4887
Use a new AllocationMap to store store buffers in the same allocation
cbeuw May 6, 2022
a71b103
Add imperfectly overlapping test
cbeuw May 6, 2022
bf7fe68
Add -Zmiri-disable-weak-memory-emulation to README
cbeuw May 6, 2022
11ca975
Move type definitions together and clarify fetch_store on empty buffer
cbeuw May 7, 2022
32627d5
Disable weak memory emulation on scheduler-dependent data race tests
cbeuw May 7, 2022
f729f28
Move cpp20_rwc_syncs into compile-fail
cbeuw May 7, 2022
89138a6
Add more top-level comments
cbeuw May 10, 2022
62b514e
Update README
cbeuw May 10, 2022
773131b
Improve privacy and comments
cbeuw May 11, 2022
7d874db
Add tests showing weak memory behaviours
cbeuw May 12, 2022
6040c9f
Refactor store buffer search conditions
cbeuw May 12, 2022
13e3465
Reduce the number of runs in consistency tests
cbeuw May 12, 2022
8739e45
Move data_race and weak_memory into a submodule
cbeuw May 13, 2022
335667c
Move buffered functions into their own ext trait
cbeuw May 14, 2022
5a4a1bf
Remove incorrect comment
cbeuw May 15, 2022
6b54c92
Throw UB on imperfectly overlapping access
cbeuw May 16, 2022
577054c
Rename variables in AllocationMap
cbeuw May 16, 2022
9214537
Put the initialisation value into the store buffer
cbeuw May 16, 2022
e2002b4
Amend experimental thread support warnings
cbeuw May 16, 2022
31c0141
Replace yield_now() with spin loop hint
cbeuw May 17, 2022
5ddd4ef
Spelling, punctuation and grammar
cbeuw May 19, 2022
6d27f18
Update src/concurrency/weak_memory.rs
cbeuw May 22, 2022
dafd813
Move transmute into a separate function
cbeuw May 22, 2022
7dcb19e
Add rust-only operation tests
cbeuw May 23, 2022
2321b15
Differentiate between not multithreading and temp disabling race dete…
cbeuw May 24, 2022
226ed41
Destroy store buffers on non-racy non-atomic accesses
cbeuw May 24, 2022
613d60d
Allow non-racy mixed size accesses
cbeuw May 25, 2022
bfa5645
Split extra_cpp tests into sound and unsafe
cbeuw May 25, 2022
6a73ded
Update experimental threading warning
cbeuw May 25, 2022
a7c832b
Wording improvements
cbeuw May 29, 2022
ceb173d
Move logic out of machine.rs
cbeuw May 29, 2022
4a07f78
Forbade all racing mixed size atomic accesses
cbeuw May 29, 2022
8215702
Refer to GitHub issue on overwritten init value
cbeuw May 29, 2022
c731071
Give flag temp disabling race detector a better name
cbeuw May 29, 2022
6d0c76e
Specify only perfectly overlapping accesses can race
cbeuw May 29, 2022
65f39bd
Move tests to new directories
cbeuw Jun 4, 2022
1379036
Simplify known C++20 inconsistency test
cbeuw Jun 5, 2022
6fb7c13
Remove unused lifetimes
cbeuw Jun 5, 2022
bf7a5c4
Add more backgrounds on lazy store buffers
cbeuw Jun 5, 2022
1b32d14
Make racy imperfectly overlapping atomic access unsupported instead o…
cbeuw Jun 5, 2022
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Give flag temp disabling race detector a better name
cbeuw committed Jun 6, 2022

Verified

This commit was signed with the committer’s verified signature.
cbeuw Andy Wang
commit c73107164089249477d56fbc580104231459a2a6
25 changes: 13 additions & 12 deletions src/concurrency/data_race.rs
Original file line number Diff line number Diff line change
@@ -455,11 +455,11 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
fn allow_data_races_ref<R>(&self, op: impl FnOnce(&MiriEvalContext<'mir, 'tcx>) -> R) -> R {
let this = self.eval_context_ref();
if let Some(data_race) = &this.machine.data_race {
data_race.ongoing_atomic_access.set(true);
data_race.ongoing_action_data_race_free.set(true);
}
let result = op(this);
if let Some(data_race) = &this.machine.data_race {
data_race.ongoing_atomic_access.set(false);
data_race.ongoing_action_data_race_free.set(false);
}
result
}
@@ -474,11 +474,11 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
) -> R {
let this = self.eval_context_mut();
if let Some(data_race) = &this.machine.data_race {
data_race.ongoing_atomic_access.set(true);
data_race.ongoing_action_data_race_free.set(true);
}
let result = op(this);
if let Some(data_race) = &this.machine.data_race {
data_race.ongoing_atomic_access.set(false);
data_race.ongoing_action_data_race_free.set(false);
}
result
}
@@ -1151,8 +1151,9 @@ pub struct GlobalState {
multi_threaded: Cell<bool>,

/// A flag to mark we are currently performing
/// an atomic access to supress data race detection
ongoing_atomic_access: Cell<bool>,
/// a data race free action (such as atomic access)
/// to supress the race detector
ongoing_action_data_race_free: Cell<bool>,

/// Mapping of a vector index to a known set of thread
/// clocks, this is not directly mapping from a thread id
@@ -1205,7 +1206,7 @@ impl GlobalState {
pub fn new() -> Self {
let mut global_state = GlobalState {
multi_threaded: Cell::new(false),
ongoing_atomic_access: Cell::new(false),
ongoing_action_data_race_free: Cell::new(false),
vector_clocks: RefCell::new(IndexVec::new()),
vector_info: RefCell::new(IndexVec::new()),
thread_info: RefCell::new(IndexVec::new()),
@@ -1232,14 +1233,14 @@ impl GlobalState {
}

// We perform data race detection when there are more than 1 active thread
// and we are not currently in the middle of an atomic acces where data race
// is impossible
// and we have not temporarily disabled race detection to perform something
// data race free
fn race_detecting(&self) -> bool {
self.multi_threaded.get() && !self.ongoing_atomic_access.get()
self.multi_threaded.get() && !self.ongoing_action_data_race_free.get()
}

pub fn ongoing_atomic_access(&self) -> bool {
self.ongoing_atomic_access.get()
pub fn ongoing_action_data_race_free(&self) -> bool {
self.ongoing_action_data_race_free.get()
}

// Try to find vector index values that can potentially be re-used
6 changes: 4 additions & 2 deletions src/concurrency/weak_memory.rs
Original file line number Diff line number Diff line change
@@ -139,7 +139,7 @@ impl StoreBufferAlloc {
/// after all the prior atomic accesses so the location no longer needs to exhibit
/// any weak memory behaviours until further atomic accesses.
pub fn memory_accessed<'tcx>(&self, range: AllocRange, global: &GlobalState) {
if !global.ongoing_atomic_access() {
if !global.ongoing_action_data_race_free() {
let mut buffers = self.store_buffers.borrow_mut();
let access_type = buffers.access_type(range);
match access_type {
@@ -420,7 +420,9 @@ pub(super) trait EvalContextExt<'mir, 'tcx: 'mir>:
&& !alloc_clocks
.race_free_with_atomic(range, this.machine.data_race.as_ref().unwrap())
{
throw_ub_format!("racy imperfectly overlapping atomic access is not possible in the C++20 memory model");
throw_ub_format!(
"racy imperfectly overlapping atomic access is not possible in the C++20 memory model"
);
}
}
Ok(())