clean up imperfect overlap detection in weak-mem emulation

Author: RalfJung

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.
@@ -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)?;

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<Provenance>,

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
         }
     });
 

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 `<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

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
         }
     });
 

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 `<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