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 @@ fn rmw_relaxed( 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 @@ fn atomic_read_detect( 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 @@ fn atomic_write_detect( 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 @@ fn read_race_detect( } 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 `` and (2) Atomic Load on thread `` + }); + }); +} 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 `` and (2) Atomic Load on thread `` 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 `` and (2) Atomic Load on thread `` 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 `` and (2) Read on thread `` + }); + }); +} 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 `` and (2) Read on thread `` 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 `` and (2) Read on thread `` 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 +