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

clean up imperfect overlap detection in weak-mem emulation

Browse source
This commit is contained in:
Ralf Jung 2023-10-23 12:29:03 +02:00
parent 1e5f9eb331
commit 369c6d180c
6 changed files with 28 additions and 90 deletions
Download patch file Download diff file Expand all files Collapse all files

38
src/tools/miri/src/concurrency/data_race.rs
View file

@ -339,15 +339,6 @@ impl MemoryCellClocks {
Ok(())
}
/// Checks if the memory cell access is ordered with all prior atomic reads and writes
fn race_free_with_atomic(&self, thread_clocks: &ThreadClockSet) -> bool {
if let Some(atomic) = self.atomic() {
atomic.read_vector <= thread_clocks.clock && atomic.write_vector <= thread_clocks.clock
} else {
true
}
}
/// Update memory cell data-race tracking for atomic
/// load relaxed semantics, is a no-op if this memory was
/// not used previously as atomic memory.
@ -542,7 +533,6 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
// the *value* (including the associated provenance if this is an AtomicPtr) at this location.
// Only metadata on the location itself is used.
let scalar = this.allow_data_races_ref(move |this| this.read_scalar(place))?;
this.validate_overlapping_atomic(place)?;
this.buffered_atomic_read(place, atomic, scalar, || {
this.validate_atomic_load(place, atomic)
})
@ -558,7 +548,6 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
let this = self.eval_context_mut();
this.atomic_access_check(dest)?;
this.validate_overlapping_atomic(dest)?;
this.allow_data_races_mut(move |this| this.write_scalar(val, dest))?;
this.validate_atomic_store(dest, atomic)?;
// FIXME: it's not possible to get the value before write_scalar. A read_scalar will cause
@ -581,7 +570,6 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
let this = self.eval_context_mut();
this.atomic_access_check(place)?;
this.validate_overlapping_atomic(place)?;
let old = this.allow_data_races_mut(|this| this.read_immediate(place))?;
// Atomics wrap around on overflow.
@ -606,7 +594,6 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
let this = self.eval_context_mut();
this.atomic_access_check(place)?;
this.validate_overlapping_atomic(place)?;
let old = this.allow_data_races_mut(|this| this.read_scalar(place))?;
this.allow_data_races_mut(|this| this.write_scalar(new, place))?;
@ -628,7 +615,6 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
let this = self.eval_context_mut();
this.atomic_access_check(place)?;
this.validate_overlapping_atomic(place)?;
let old = this.allow_data_races_mut(|this| this.read_immediate(place))?;
let lt = this.wrapping_binary_op(mir::BinOp::Lt, &old, &rhs)?.to_scalar().to_bool()?;
@ -668,7 +654,6 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
let this = self.eval_context_mut();
this.atomic_access_check(place)?;
this.validate_overlapping_atomic(place)?;
// Failure ordering cannot be stronger than success ordering, therefore first attempt
// to read with the failure ordering and if successful then try again with the success
// read ordering and write in the success case.
@ -927,26 +912,6 @@ impl VClockAlloc {
}))?
}
/// Detect racing atomic read and writes (not data races)
/// on every byte of the current access range
pub(super) fn race_free_with_atomic(
&self,
range: AllocRange,
global: &GlobalState,
thread_mgr: &ThreadManager<'_, '_>,
) -> bool {
if global.race_detecting() {
let (_, thread_clocks) = global.current_thread_state(thread_mgr);
let alloc_ranges = self.alloc_ranges.borrow();
for (_, mem_clocks) in alloc_ranges.iter(range.start, range.size) {
if !mem_clocks.race_free_with_atomic(&thread_clocks) {
return false;
}
}
}
true
}
/// Detect data-races for an unsynchronized read operation, will not perform
/// data-race detection if `race_detecting()` is false, either due to no threads
/// being created or if it is temporarily disabled during a racy read or write
@ -1138,7 +1103,6 @@ trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
atomic: AtomicReadOrd,
) -> InterpResult<'tcx> {
let this = self.eval_context_ref();
this.validate_overlapping_atomic(place)?;
this.validate_atomic_op(
place,
atomic,
@ -1161,7 +1125,6 @@ trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
atomic: AtomicWriteOrd,
) -> InterpResult<'tcx> {
let this = self.eval_context_mut();
this.validate_overlapping_atomic(place)?;
this.validate_atomic_op(
place,
atomic,
@ -1187,7 +1150,6 @@ trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
let acquire = matches!(atomic, Acquire | AcqRel | SeqCst);
let release = matches!(atomic, Release | AcqRel | SeqCst);
let this = self.eval_context_mut();
this.validate_overlapping_atomic(place)?;
this.validate_atomic_op(place, atomic, "Atomic RMW", move |memory, clocks, index, _| {
if acquire {
memory.load_acquire(clocks, index, place.layout.size)?;

44
src/tools/miri/src/concurrency/weak_memory.rs
View file

@ -169,14 +169,6 @@ impl StoreBufferAlloc {
Self { store_buffers: RefCell::new(RangeObjectMap::new()) }
}
/// Checks if the range imperfectly overlaps with existing buffers
/// Used to determine if mixed-size atomic accesses
fn is_overlapping(&self, range: AllocRange) -> bool {
let buffers = self.store_buffers.borrow();
let access_type = buffers.access_type(range);
matches!(access_type, AccessType::ImperfectlyOverlapping(_))
}
/// When a non-atomic access happens on a location that has been atomically accessed
/// before without data race, we can determine that the non-atomic access fully happens
/// after all the prior atomic accesses so the location no longer needs to exhibit
@ -190,6 +182,8 @@ impl StoreBufferAlloc {
buffers.remove_from_pos(pos);
}
AccessType::ImperfectlyOverlapping(pos_range) => {
// We rely on the data-race check making sure this is synchronized.
// Therefore we can forget about the old data here.
buffers.remove_pos_range(pos_range);
}
AccessType::Empty(_) => {
@ -215,7 +209,7 @@ impl StoreBufferAlloc {
pos
}
AccessType::ImperfectlyOverlapping(pos_range) => {
// Once we reach here we would've already checked that this access is not racy
// Once we reach here we would've already checked that this access is not racy.
let mut buffers = self.store_buffers.borrow_mut();
buffers.remove_pos_range(pos_range.clone());
buffers.insert_at_pos(pos_range.start, range, StoreBuffer::new(init));
@ -240,6 +234,7 @@ impl StoreBufferAlloc {
pos
}
AccessType::ImperfectlyOverlapping(pos_range) => {
// Once we reach here we would've already checked that this access is not racy.
buffers.remove_pos_range(pos_range.clone());
buffers.insert_at_pos(pos_range.start, range, StoreBuffer::new(init));
pos_range.start
@ -473,37 +468,6 @@ impl<'mir, 'tcx: 'mir> EvalContextExt<'mir, 'tcx> for crate::MiriInterpCx<'mir,
pub(super) trait EvalContextExt<'mir, 'tcx: 'mir>:
crate::MiriInterpCxExt<'mir, 'tcx>
{
// If weak memory emulation is enabled, check if this atomic op imperfectly overlaps with a previous
// atomic read or write. If it does, then we require it to be ordered (non-racy) with all previous atomic
// accesses on all the bytes in range
fn validate_overlapping_atomic(
&self,
place: &MPlaceTy<'tcx, Provenance>,
) -> InterpResult<'tcx> {
let this = self.eval_context_ref();
let (alloc_id, base_offset, ..) = this.ptr_get_alloc_id(place.ptr())?;
if let crate::AllocExtra {
weak_memory: Some(alloc_buffers),
data_race: Some(alloc_clocks),
..
} = this.get_alloc_extra(alloc_id)?
{
let range = alloc_range(base_offset, place.layout.size);
if alloc_buffers.is_overlapping(range)
&& !alloc_clocks.race_free_with_atomic(
range,
this.machine.data_race.as_ref().unwrap(),
&this.machine.threads,
)
{
throw_unsup_format!(
"racy imperfectly overlapping atomic access is not possible in the C++20 memory model, and not supported by Miri's weak memory emulation"
);
}
}
Ok(())
}
fn buffered_atomic_rmw(
&mut self,
new_val: Scalar<Provenance>,

4
src/tools/miri/tests/fail/weak_memory/racing_mixed_size.rs
View file

@ -19,7 +19,7 @@ fn split_u32_ptr(dword: *const u32) -> *const [u16; 2] {
// Wine's SRWLock implementation does this, which is definitely undefined in C++ memory model
// https://github.com/wine-mirror/wine/blob/303f8042f9db508adaca02ef21f8de4992cb9c03/dlls/ntdll/sync.c#L543-L566
// Though it probably works just fine on x86
// It probably works just fine on x86, but Intel does document this as "don't do it!"
pub fn main() {
let x = static_atomic_u32(0);
let j1 = spawn(move || {
@ -31,7 +31,7 @@ pub fn main() {
let x_split = split_u32_ptr(x_ptr);
unsafe {
let hi = ptr::addr_of!((*x_split)[0]);
std::intrinsics::atomic_load_relaxed(hi); //~ ERROR: imperfectly overlapping
std::intrinsics::atomic_load_relaxed(hi); //~ ERROR: different-size
}
});

14
src/tools/miri/tests/fail/weak_memory/racing_mixed_size.stderr
View file

@ -1,11 +1,17 @@
error: unsupported operation: racy imperfectly overlapping atomic access is not possible in the C++20 memory model, and not supported by Miri's weak memory emulation
error: Undefined Behavior: Data race detected between (1) 4-byte Atomic Store on thread `<unnamed>` and (2) 2-byte (different-size) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
--> $DIR/racing_mixed_size.rs:LL:CC
|
LL | std::intrinsics::atomic_load_relaxed(hi);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ racy imperfectly overlapping atomic access is not possible in the C++20 memory model, and not supported by Miri's weak memory emulation
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between (1) 4-byte Atomic Store on thread `<unnamed>` and (2) 2-byte (different-size) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
|
= help: this is likely not a bug in the program; it indicates that the program performed an operation that the interpreter does not support
= note: BACKTRACE:
help: and (1) occurred earlier here
--> $DIR/racing_mixed_size.rs:LL:CC
|
LL | x.store(1, Relaxed);
| ^^^^^^^^^^^^^^^^^^^
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
= note: BACKTRACE (of the first span):
= note: inside closure at $DIR/racing_mixed_size.rs:LL:CC
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace

4
src/tools/miri/tests/fail/weak_memory/racing_mixed_size_read.rs
View file

@ -16,7 +16,7 @@ fn split_u32_ptr(dword: *const u32) -> *const [u16; 2] {
// Racing mixed size reads may cause two loads to read-from
// the same store but observe different values, which doesn't make
// sense under the formal model so we forbade this.
// sense under the formal model so we forbid this.
pub fn main() {
let x = static_atomic(0);
@ -29,7 +29,7 @@ pub fn main() {
let x_split = split_u32_ptr(x_ptr);
unsafe {
let hi = x_split as *const u16 as *const AtomicU16;
(*hi).load(Relaxed); //~ ERROR: imperfectly overlapping
(*hi).load(Relaxed); //~ ERROR: different-size
}
});

14
src/tools/miri/tests/fail/weak_memory/racing_mixed_size_read.stderr
View file

@ -1,11 +1,17 @@
error: unsupported operation: racy imperfectly overlapping atomic access is not possible in the C++20 memory model, and not supported by Miri's weak memory emulation
error: Undefined Behavior: Data race detected between (1) 4-byte Atomic Load on thread `<unnamed>` and (2) 2-byte (different-size) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
--> $DIR/racing_mixed_size_read.rs:LL:CC
|
LL | (*hi).load(Relaxed);
| ^^^^^^^^^^^^^^^^^^^ racy imperfectly overlapping atomic access is not possible in the C++20 memory model, and not supported by Miri's weak memory emulation
| ^^^^^^^^^^^^^^^^^^^ Data race detected between (1) 4-byte Atomic Load on thread `<unnamed>` and (2) 2-byte (different-size) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
|
= help: this is likely not a bug in the program; it indicates that the program performed an operation that the interpreter does not support
= note: BACKTRACE:
help: and (1) occurred earlier here
--> $DIR/racing_mixed_size_read.rs:LL:CC
|
LL | x.load(Relaxed);
| ^^^^^^^^^^^^^^^
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
= note: BACKTRACE (of the first span):
= note: inside closure at $DIR/racing_mixed_size_read.rs:LL:CC
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace