From ced50a6037b56f5b935f77fe2b72e9d16ae03b9b Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 23 Oct 2023 12:29:03 +0200 Subject: [PATCH] clean up imperfect overlap detection in weak-mem emulation --- src/concurrency/data_race.rs | 38 ---------------- src/concurrency/weak_memory.rs | 44 ++----------------- tests/fail/weak_memory/racing_mixed_size.rs | 4 +- .../fail/weak_memory/racing_mixed_size.stderr | 14 ++++-- .../weak_memory/racing_mixed_size_read.rs | 4 +- .../weak_memory/racing_mixed_size_read.stderr | 14 ++++-- 6 files changed, 28 insertions(+), 90 deletions(-) diff --git a/src/concurrency/data_race.rs b/src/concurrency/data_race.rs index 8319a50466..56b5069491 100644 --- a/src/concurrency/data_race.rs +++ b/src/concurrency/data_race.rs @@ -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. @@ -543,7 +534,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) }) @@ -559,7 +549,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 @@ -582,7 +571,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. @@ -607,7 +595,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))?; @@ -629,7 +616,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()?; @@ -669,7 +655,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. @@ -928,26 +913,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 @@ -1139,7 +1104,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, @@ -1162,7 +1126,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, @@ -1188,7 +1151,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)?; diff --git a/src/concurrency/weak_memory.rs b/src/concurrency/weak_memory.rs index 6781b1f6dd..2ff344bb1a 100644 --- a/src/concurrency/weak_memory.rs +++ b/src/concurrency/weak_memory.rs @@ -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, diff --git a/tests/fail/weak_memory/racing_mixed_size.rs b/tests/fail/weak_memory/racing_mixed_size.rs index 7bbb7f9fe7..36dc0d5f3f 100644 --- a/tests/fail/weak_memory/racing_mixed_size.rs +++ b/tests/fail/weak_memory/racing_mixed_size.rs @@ -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 } }); diff --git a/tests/fail/weak_memory/racing_mixed_size.stderr b/tests/fail/weak_memory/racing_mixed_size.stderr index dda22ac9ce..6823042d28 100644 --- a/tests/fail/weak_memory/racing_mixed_size.stderr +++ b/tests/fail/weak_memory/racing_mixed_size.stderr @@ -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 `` and (2) 2-byte (different-size) Atomic Load on thread `` 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 `` and (2) 2-byte (different-size) Atomic Load on thread `` 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 diff --git a/tests/fail/weak_memory/racing_mixed_size_read.rs b/tests/fail/weak_memory/racing_mixed_size_read.rs index 73178980b7..5cd14540ca 100644 --- a/tests/fail/weak_memory/racing_mixed_size_read.rs +++ b/tests/fail/weak_memory/racing_mixed_size_read.rs @@ -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 } }); diff --git a/tests/fail/weak_memory/racing_mixed_size_read.stderr b/tests/fail/weak_memory/racing_mixed_size_read.stderr index 59fa5c7410..edddf4bc26 100644 --- a/tests/fail/weak_memory/racing_mixed_size_read.stderr +++ b/tests/fail/weak_memory/racing_mixed_size_read.stderr @@ -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 `` and (2) 2-byte (different-size) Atomic Load on thread `` 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 `` and (2) 2-byte (different-size) Atomic Load on thread `` 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