user0/rust
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Make allow_data_races_* public to silence data races during cleanup

Browse source
This commit is contained in:
Ben Kimock 2022-05-21 13:37:41 -04:00
parent b96610b3de
commit 3cfce6ffb2
2 changed files with 49 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

84
src/data_race.rs
View file

@ -437,6 +437,49 @@ impl MemoryCellClocks {
/// Evaluation context extensions.
impl<'mir, 'tcx: 'mir> EvalContextExt<'mir, 'tcx> for MiriEvalContext<'mir, 'tcx> {}
pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
/// Temporarily allow data-races to occur. This should only be used in
/// one of these cases:
/// - One of the appropriate `validate_atomic` functions will be called to
/// to treat a memory access as atomic.
/// - The memory being accessed should be treated as internal state, that
/// cannot be accessed by the interpreted program.
/// - Execution of the interpreted program execution has halted.
#[inline]
fn allow_data_races_ref<R>(&self, op: impl FnOnce(&MiriEvalContext<'mir, 'tcx>) -> R) -> R {
let this = self.eval_context_ref();
let old = if let Some(data_race) = &this.machine.data_race {
data_race.multi_threaded.replace(false)
} else {
false
};
let result = op(this);
if let Some(data_race) = &this.machine.data_race {
data_race.multi_threaded.set(old);
}
result
}
/// Same as `allow_data_races_ref`, this temporarily disables any data-race detection and
/// so should only be used for atomic operations or internal state that the program cannot
/// access.
#[inline]
fn allow_data_races_mut<R>(
&mut self,
op: impl FnOnce(&mut MiriEvalContext<'mir, 'tcx>) -> R,
) -> R {
let this = self.eval_context_mut();
let old = if let Some(data_race) = &this.machine.data_race {
data_race.multi_threaded.replace(false)
} else {
false
};
let result = op(this);
if let Some(data_race) = &this.machine.data_race {
data_race.multi_threaded.set(old);
}
result
}
/// Atomic variant of read_scalar_at_offset.
fn read_scalar_at_offset_atomic(
&self,
@ -927,47 +970,6 @@ impl VClockAlloc {
impl<'mir, 'tcx: 'mir> EvalContextPrivExt<'mir, 'tcx> for MiriEvalContext<'mir, 'tcx> {}
trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
// Temporarily allow data-races to occur, this should only be
// used if either one of the appropriate `validate_atomic` functions
// will be called to treat a memory access as atomic or if the memory
// being accessed should be treated as internal state, that cannot be
// accessed by the interpreted program.
#[inline]
fn allow_data_races_ref<R>(&self, op: impl FnOnce(&MiriEvalContext<'mir, 'tcx>) -> R) -> R {
let this = self.eval_context_ref();
let old = if let Some(data_race) = &this.machine.data_race {
data_race.multi_threaded.replace(false)
} else {
false
};
let result = op(this);
if let Some(data_race) = &this.machine.data_race {
data_race.multi_threaded.set(old);
}
result
}
/// Same as `allow_data_races_ref`, this temporarily disables any data-race detection and
/// so should only be used for atomic operations or internal state that the program cannot
/// access.
#[inline]
fn allow_data_races_mut<R>(
&mut self,
op: impl FnOnce(&mut MiriEvalContext<'mir, 'tcx>) -> R,
) -> R {
let this = self.eval_context_mut();
let old = if let Some(data_race) = &this.machine.data_race {
data_race.multi_threaded.replace(false)
} else {
false
};
let result = op(this);
if let Some(data_race) = &this.machine.data_race {
data_race.multi_threaded.set(old);
}
result
}
/// Generic atomic operation implementation
fn validate_atomic_op<A: Debug + Copy>(
&self,

7
src/eval.rs
View file

@ -344,7 +344,12 @@ pub fn eval_entry<'tcx>(
})();
// Machine cleanup.
EnvVars::cleanup(&mut ecx).unwrap();
// Execution of the program has halted so any memory access we do here
// cannot produce a real data race. If we do not do something to disable
// data race detection here, some uncommon combination of errors will
// cause a data race to be detected:
// https://github.com/rust-lang/miri/issues/2020
ecx.allow_data_races_mut(|ecx| EnvVars::cleanup(ecx).unwrap());
// Process the result.
match res {