about summary refs log tree commit diff
path: root/src/tools
diff options
context:
space:
mode:
authorRalf Jung <post@ralfj.de>2023-10-23 11:34:15 +0200
committerRalf Jung <post@ralfj.de>2023-10-23 11:35:12 +0200
commitf99566ec4d4f7162739b07836fb6df589cb70d60 (patch)
tree5280e67f00b861ea537454f523601b6578183601 /src/tools
parenta4e42ad185aa0dd904d892de14b27e0a9bc36c18 (diff)
data_race: detect races between atomic and non-atomic accesses, even if both are reads
Diffstat (limited to 'src/tools')
-rw-r--r--src/tools/miri/src/concurrency/data_race.rs13
-rw-r--r--src/tools/miri/tests/fail/data_race/read_read_race1.rs22
-rw-r--r--src/tools/miri/tests/fail/data_race/read_read_race1.stderr20
-rw-r--r--src/tools/miri/tests/fail/data_race/read_read_race2.rs22
-rw-r--r--src/tools/miri/tests/fail/data_race/read_read_race2.stderr20
5 files changed, 95 insertions, 2 deletions
diff --git a/src/tools/miri/src/concurrency/data_race.rs b/src/tools/miri/src/concurrency/data_race.rs
index 0ef1f1442ee..5c346283d6b 100644
--- a/src/tools/miri/src/concurrency/data_race.rs
+++ b/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
             };
diff --git a/src/tools/miri/tests/fail/data_race/read_read_race1.rs b/src/tools/miri/tests/fail/data_race/read_read_race1.rs
new file mode 100644
index 00000000000..295121f5765
--- /dev/null
+++ b/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>`
+        });
+    });
+}
diff --git a/src/tools/miri/tests/fail/data_race/read_read_race1.stderr b/src/tools/miri/tests/fail/data_race/read_read_race1.stderr
new file mode 100644
index 00000000000..158b438bd0d
--- /dev/null
+++ b/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
+
diff --git a/src/tools/miri/tests/fail/data_race/read_read_race2.rs b/src/tools/miri/tests/fail/data_race/read_read_race2.rs
new file mode 100644
index 00000000000..bf180a1543e
--- /dev/null
+++ b/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>`
+        });
+    });
+}
diff --git a/src/tools/miri/tests/fail/data_race/read_read_race2.stderr b/src/tools/miri/tests/fail/data_race/read_read_race2.stderr
new file mode 100644
index 00000000000..7f867b9edbb
--- /dev/null
+++ b/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
+