mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

miri: no longer complain about read-read races

Browse Source
This commit is contained in:
Ralf Jung 2024-08-07 14:50:34 +02:00
parent 76bce58b7a
commit ed417f44f8
6 changed files with 43 additions and 122 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
src/tools/miri/src/concurrency/data_race.rs
View File

@ -499,7 +499,7 @@ fn rmw_relaxed(
Ok(())
}
/// Detect data-races with an atomic read, caused by a non-atomic access that does
/// Detect data-races with an atomic read, caused by a non-atomic write that does
/// not happen-before the atomic-read.
fn atomic_read_detect(
&mut self,
@ -510,12 +510,8 @@ fn atomic_read_detect(
trace!("Atomic read with vectors: {:#?} :: {:#?}", self, thread_clocks);
let atomic = self.atomic_access(thread_clocks, access_size)?;
atomic.read_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 {
Err(DataRace)
}
// Make sure the last non-atomic write was before this access.
if self.write_was_before(&thread_clocks.clock) { Ok(()) } else { Err(DataRace) }
}
/// Detect data-races with an atomic write, either with a non-atomic read or with
@ -552,11 +548,9 @@ fn read_race_detect(
}
thread_clocks.clock.index_mut(index).set_read_type(read_type);
if self.write_was_before(&thread_clocks.clock) {
// We must be ordered-after all atomic writes.
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
};
@ -957,9 +951,7 @@ fn report_data_race<'tcx>(
let mut other_size = None; // if `Some`, this was a size-mismatch race
let write_clock;
let (other_access, other_thread, other_clock) =
// First check the atomic-nonatomic cases. If it looks like multiple
// cases apply, this one should take precedence, else it might look like
// we are reporting races between two non-atomic reads.
// First check the atomic-nonatomic cases.
if !access.is_atomic() &&
let Some(atomic) = mem_clocks.atomic() &&
let Some(idx) = Self::find_gt_index(&atomic.write_vector, &active_clocks.clock)
@ -1007,10 +999,7 @@ fn report_data_race<'tcx>(
assert!(!involves_non_atomic);
Some("overlapping unsynchronized atomic accesses must use the same access size")
} else if access.is_read() && other_access.is_read() {
assert!(involves_non_atomic);
Some(
"overlapping atomic and non-atomic accesses must be synchronized, even if both are read-only",
)
panic!("there should be no same-size read-read races")
} else {
None
};

30
src/tools/miri/tests/fail/data_race/read_read_race1.rs
View File

@ -1,30 +0,0 @@
//@compile-flags: -Zmiri-preemption-rate=0.0
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=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) non-atomic read on thread `unnamed-1` and (2) atomic load on thread `unnamed-2`
});
});
}

22
src/tools/miri/tests/fail/data_race/read_read_race1.stderr
View File

@ -1,22 +0,0 @@
error: Undefined Behavior: Data race detected between (1) non-atomic read on thread `unnamed-ID` and (2) atomic load on thread `unnamed-ID` at ALLOC. (2) just happened here
--> tests/fail/data_race/read_read_race1.rs:LL:CC
|
LL | a.load(Ordering::SeqCst);
| ^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between (1) non-atomic read on thread `unnamed-ID` and (2) atomic load on thread `unnamed-ID` at ALLOC. (2) just happened here
|
help: and (1) occurred earlier here
--> tests/fail/data_race/read_read_race1.rs:LL:CC
|
LL | unsafe { ptr.read() };
| ^^^^^^^^^^
= help: overlapping atomic and non-atomic accesses must be synchronized, even if both are read-only
= help: see https://doc.rust-lang.org/nightly/std/sync/atomic/index.html#memory-model-for-atomic-accesses for more information about the Rust memory model
= 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) on thread `unnamed-ID`:
= note: inside closure at tests/fail/data_race/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 1 previous error

30
src/tools/miri/tests/fail/data_race/read_read_race2.rs
View File

@ -1,30 +0,0 @@
//@compile-flags: -Zmiri-preemption-rate=0.0
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=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-1` and (2) non-atomic read on thread `unnamed-2`
});
});
}

22
src/tools/miri/tests/fail/data_race/read_read_race2.stderr
View File

@ -1,22 +0,0 @@
error: Undefined Behavior: Data race detected between (1) atomic load on thread `unnamed-ID` and (2) non-atomic read on thread `unnamed-ID` at ALLOC. (2) just happened here
--> tests/fail/data_race/read_read_race2.rs:LL:CC
|
LL | unsafe { ptr.read() };
| ^^^^^^^^^^ Data race detected between (1) atomic load on thread `unnamed-ID` and (2) non-atomic read on thread `unnamed-ID` at ALLOC. (2) just happened here
|
help: and (1) occurred earlier here
--> tests/fail/data_race/read_read_race2.rs:LL:CC
|
LL | a.load(Ordering::SeqCst);
| ^^^^^^^^^^^^^^^^^^^^^^^^
= help: overlapping atomic and non-atomic accesses must be synchronized, even if both are read-only
= help: see https://doc.rust-lang.org/nightly/std/sync/atomic/index.html#memory-model-for-atomic-accesses for more information about the Rust memory model
= 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) on thread `unnamed-ID`:
= note: inside closure at tests/fail/data_race/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 1 previous error

38
src/tools/miri/tests/pass/concurrency/data_race.rs
View File

@ -1,7 +1,7 @@
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0
use std::sync::atomic::*;
use std::thread::spawn;
use std::thread::{self, spawn};
#[derive(Copy, Clone)]
struct EvilSend<T>(pub T);
@ -143,10 +143,46 @@ fn test_local_variable_lazy_write() {
assert_eq!(val, 127);
}
// This test coverse the case where the non-atomic access come first.
fn test_read_read_race1() {
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);
});
});
}
// This test coverse the case where the atomic access come first.
fn test_read_read_race2() {
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() };
});
});
}
pub fn main() {
test_fence_sync();
test_multiple_reads();
test_rmw_no_block();
test_simple_release();
test_local_variable_lazy_write();
test_read_read_race1();
test_read_read_race2();
}