data_race: detect races between atomic and non-atomic accesses, even if both are reads

Author: RalfJung

src/tools/miri/src/concurrency/data_race.rs

@@ -374,7 +374,7 @@ impl MemoryCellClocks {
         Ok(())
     }
 
-    /// Detect data-races with an atomic read, caused by a non-atomic write that does
+    /// Detect data-races with an atomic read, caused by a non-atomic access that does
     /// not happen-before the atomic-read.
     fn atomic_read_detect(
         &mut self,
@@ -384,7 +384,12 @@ impl MemoryCellClocks {
         log::trace!("Atomic read with vectors: {:#?} :: {:#?}", self, thread_clocks);
         let atomic = self.atomic_mut();
         atomic.read_vector.set_at_index(&thread_clocks.clock, index);
-        if self.write_was_before(&thread_clocks.clock) { Ok(()) } else { Err(DataRace) }
+        // Make sure the last non-atomic write and all non-atomic reads were before this access.
+        if self.write_was_before(&thread_clocks.clock) && self.read <= thread_clocks.clock {
+            Ok(())
+        } else {
+            Err(DataRace)
+        }
     }
 
     /// Detect data-races with an atomic write, either with a non-atomic read or with
@@ -397,6 +402,7 @@ impl MemoryCellClocks {
         log::trace!("Atomic write with vectors: {:#?} :: {:#?}", self, thread_clocks);
         let atomic = self.atomic_mut();
         atomic.write_vector.set_at_index(&thread_clocks.clock, index);
+        // Make sure the last non-atomic write and all non-atomic reads were before this access.
         if self.write_was_before(&thread_clocks.clock) && self.read <= thread_clocks.clock {
             Ok(())
         } else {
@@ -418,7 +424,10 @@ impl MemoryCellClocks {
         }
         if self.write_was_before(&thread_clocks.clock) {
             let race_free = if let Some(atomic) = self.atomic() {
+                // We must be ordered-after all atomic accesses, reads and writes.
+                // This ensures we don't mix atomic and non-atomic accesses.
                 atomic.write_vector <= thread_clocks.clock
+                    && atomic.read_vector <= thread_clocks.clock
             } else {
                 true
             };

src/tools/miri/tests/fail/data_race/read_read_race1.rs

@@ -0,0 +1,22 @@
+//@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();
+            a.load(Ordering::SeqCst);
+            //~^ ERROR: Data race detected between (1) Read on thread `<unnamed>` and (2) Atomic Load on thread `<unnamed>`
+        });
+    });
+}

src/tools/miri/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
+

src/tools/miri/tests/fail/data_race/read_read_race2.rs

@@ -0,0 +1,22 @@
+//@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(|| {
+            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>`
+        });
+    });
+}

src/tools/miri/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
+