Detect mixed-size and mixed-atomicity non-synchronized accesses

ci.sh

@@ -108,7 +108,7 @@ case $HOST_TARGET in
     MIRI_TEST_TARGET=aarch64-unknown-linux-gnu run_tests
     MIRI_TEST_TARGET=aarch64-apple-darwin run_tests
     MIRI_TEST_TARGET=i686-pc-windows-gnu run_tests
-    MIRI_TEST_TARGET=x86_64-unknown-freebsd run_tests_minimal hello integer vec panic/panic concurrency/simple atomic data_race env/var
+    MIRI_TEST_TARGET=x86_64-unknown-freebsd run_tests_minimal hello integer vec panic/panic concurrency/simple atomic env/var
     MIRI_TEST_TARGET=aarch64-linux-android run_tests_minimal hello integer vec panic/panic
     MIRI_TEST_TARGET=wasm32-wasi run_tests_minimal no_std integer strings wasm
     MIRI_TEST_TARGET=wasm32-unknown-unknown run_tests_minimal no_std integer strings wasm

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

src/diagnostics.rs

@@ -43,9 +43,10 @@ pub enum TerminationInfo {
         span: SpanData,
     },
     DataRace {
+        involves_non_atomic: bool,
+        ptr: Pointer,
         op1: RacingOp,
         op2: RacingOp,
-        ptr: Pointer,
     },
 }
 
@@ -74,11 +75,15 @@ impl fmt::Display for TerminationInfo {
                 write!(f, "multiple definitions of symbol `{link_name}`"),
             SymbolShimClashing { link_name, .. } =>
                 write!(f, "found `{link_name}` symbol definition that clashes with a built-in shim",),
-            DataRace { ptr, op1, op2 } =>
+            DataRace { involves_non_atomic, ptr, op1, op2 } =>
                 write!(
                     f,
-                    "Data race detected between (1) {} on {} and (2) {} on {} at {ptr:?}. (2) just happened here",
-                    op1.action, op1.thread_info, op2.action, op2.thread_info
+                    "{} detected between (1) {} on {} and (2) {} on {} at {ptr:?}. (2) just happened here",
+                    if *involves_non_atomic { "Data race" } else { "Race condition" },
+                    op1.action,
+                    op1.thread_info,
+                    op2.action,
+                    op2.thread_info
                 ),
         }
     }

tests/fail/data_race/mixed_size_read.rs

@@ -0,0 +1,25 @@
+//@compile-flags: -Zmiri-preemption-rate=0.0 -Zmiri-disable-weak-memory-emulation
+use std::sync::atomic::{AtomicU16, AtomicU8, Ordering};
+use std::thread;
+
+fn convert(a: &AtomicU16) -> &[AtomicU8; 2] {
+    unsafe { std::mem::transmute(a) }
+}
+
+// We can't allow mixed-size accesses; they are not possible in C++ and even
+// Intel says you shouldn't do it.
+fn main() {
+    let a = AtomicU16::new(0);
+    let a16 = &a;
+    let a8 = convert(a16);
+
+    thread::scope(|s| {
+        s.spawn(|| {
+            a16.load(Ordering::SeqCst);
+        });
+        s.spawn(|| {
+            a8[0].load(Ordering::SeqCst);
+            //~^ ERROR: Race condition detected between (1) 2-byte Atomic Load on thread `<unnamed>` and (2) 1-byte (different-size) Atomic Load on thread `<unnamed>`
+        });
+    });
+}

tests/fail/data_race/mixed_size_read.stderr

@@ -0,0 +1,20 @@
+error: Undefined Behavior: Race condition detected between (1) 2-byte Atomic Load on thread `<unnamed>` and (2) 1-byte (different-size) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
+  --> $DIR/mixed_size_read.rs:LL:CC
+   |
+LL |             a8[0].load(Ordering::SeqCst);
+   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Race condition detected between (1) 2-byte Atomic Load on thread `<unnamed>` and (2) 1-byte (different-size) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
+   |
+help: and (1) occurred earlier here
+  --> $DIR/mixed_size_read.rs:LL:CC
+   |
+LL |             a16.load(Ordering::SeqCst);
+   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^
+   = 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/mixed_size_read.rs:LL:CC
+
+note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
+
+error: aborting due to previous error
+

tests/fail/data_race/mixed_size_write.rs

@@ -0,0 +1,25 @@
+//@compile-flags: -Zmiri-preemption-rate=0.0 -Zmiri-disable-weak-memory-emulation
+use std::sync::atomic::{AtomicU16, AtomicU8, Ordering};
+use std::thread;
+
+fn convert(a: &AtomicU16) -> &[AtomicU8; 2] {
+    unsafe { std::mem::transmute(a) }
+}
+
+// We can't allow mixed-size accesses; they are not possible in C++ and even
+// Intel says you shouldn't do it.
+fn main() {
+    let a = AtomicU16::new(0);
+    let a16 = &a;
+    let a8 = convert(a16);
+
+    thread::scope(|s| {
+        s.spawn(|| {
+            a16.store(1, Ordering::SeqCst);
+        });
+        s.spawn(|| {
+            a8[0].store(1, Ordering::SeqCst);
+            //~^ ERROR: Race condition detected between (1) 2-byte Atomic Store on thread `<unnamed>` and (2) 1-byte (different-size) Atomic Store on thread `<unnamed>`
+        });
+    });
+}

tests/fail/data_race/mixed_size_write.stderr

@@ -0,0 +1,20 @@
+error: Undefined Behavior: Race condition detected between (1) 2-byte Atomic Store on thread `<unnamed>` and (2) 1-byte (different-size) Atomic Store on thread `<unnamed>` at ALLOC. (2) just happened here
+  --> $DIR/mixed_size_write.rs:LL:CC
+   |
+LL |             a8[0].store(1, Ordering::SeqCst);
+   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Race condition detected between (1) 2-byte Atomic Store on thread `<unnamed>` and (2) 1-byte (different-size) Atomic Store on thread `<unnamed>` at ALLOC. (2) just happened here
+   |
+help: and (1) occurred earlier here
+  --> $DIR/mixed_size_write.rs:LL:CC
+   |
+LL |             a16.store(1, Ordering::SeqCst);
+   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   = 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/mixed_size_write.rs:LL:CC
+
+note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
+
+error: aborting due to previous error
+

tests/fail/data_race/read_read_race1.rs

@@ -0,0 +1,27 @@
+//@compile-flags: -Zmiri-preemption-rate=0.0
+use std::sync::atomic::{AtomicU16, Ordering};
+use std::thread;
+
+// Make sure races between atomic and non-atomic reads are detected.
+// This seems harmless but C++ does not allow them, so we can't allow them for now either.
+// This test coverse the case where the non-atomic access come first.
+fn main() {
+    let a = AtomicU16::new(0);
+
+    thread::scope(|s| {
+        s.spawn(|| {
+            let ptr = &a as *const AtomicU16 as *mut u16;
+            unsafe { ptr.read() };
+        });
+        s.spawn(|| {
+            thread::yield_now();
+
+            // We also put a non-atomic access here, but that should *not* be reported.
+            let ptr = &a as *const AtomicU16 as *mut u16;
+            unsafe { ptr.read() };
+            // Then do the atomic access.
+            a.load(Ordering::SeqCst);
+            //~^ ERROR: Data race detected between (1) Read on thread `<unnamed>` and (2) Atomic Load on thread `<unnamed>`
+        });
+    });
+}

tests/fail/data_race/read_read_race1.stderr

@@ -0,0 +1,20 @@
+error: Undefined Behavior: Data race detected between (1) Read on thread `<unnamed>` and (2) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
+  --> $DIR/read_read_race1.rs:LL:CC
+   |
+LL |             a.load(Ordering::SeqCst);
+   |             ^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between (1) Read on thread `<unnamed>` and (2) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
+   |
+help: and (1) occurred earlier here
+  --> $DIR/read_read_race1.rs:LL:CC
+   |
+LL |             unsafe { ptr.read() };
+   |                      ^^^^^^^^^^
+   = 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/read_read_race1.rs:LL:CC
+
+note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
+
+error: aborting due to previous error
+

tests/fail/data_race/read_read_race2.rs

@@ -0,0 +1,27 @@
+//@compile-flags: -Zmiri-preemption-rate=0.0
+use std::sync::atomic::{AtomicU16, Ordering};
+use std::thread;
+
+// Make sure races between atomic and non-atomic reads are detected.
+// This seems harmless but C++ does not allow them, so we can't allow them for now either.
+// This test coverse the case where the atomic access come first.
+fn main() {
+    let a = AtomicU16::new(0);
+
+    thread::scope(|s| {
+        s.spawn(|| {
+            // We also put a non-atomic access here, but that should *not* be reported.
+            let ptr = &a as *const AtomicU16 as *mut u16;
+            unsafe { ptr.read() };
+            // Then do the atomic access.
+            a.load(Ordering::SeqCst);
+        });
+        s.spawn(|| {
+            thread::yield_now();
+
+            let ptr = &a as *const AtomicU16 as *mut u16;
+            unsafe { ptr.read() };
+            //~^ ERROR: Data race detected between (1) Atomic Load on thread `<unnamed>` and (2) Read on thread `<unnamed>`
+        });
+    });
+}

tests/fail/data_race/read_read_race2.stderr

@@ -0,0 +1,20 @@
+error: Undefined Behavior: Data race detected between (1) Atomic Load on thread `<unnamed>` and (2) Read on thread `<unnamed>` at ALLOC. (2) just happened here
+  --> $DIR/read_read_race2.rs:LL:CC
+   |
+LL |             unsafe { ptr.read() };
+   |                      ^^^^^^^^^^ Data race detected between (1) Atomic Load on thread `<unnamed>` and (2) Read on thread `<unnamed>` at ALLOC. (2) just happened here
+   |
+help: and (1) occurred earlier here
+  --> $DIR/read_read_race2.rs:LL:CC
+   |
+LL |             a.load(Ordering::SeqCst);
+   |             ^^^^^^^^^^^^^^^^^^^^^^^^
+   = 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/read_read_race2.rs:LL:CC
+
+note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
+
+error: aborting due to previous error
+

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: Race condition 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
+   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Race condition 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: Race condition 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
+   |             ^^^^^^^^^^^^^^^^^^^ Race condition 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