Skip to content

Commit

Permalink
miri: no longer complain about read-read races
Browse files Browse the repository at this point in the history
  • Loading branch information
RalfJung committed Aug 7, 2024
1 parent 704210e commit 24c19b8
Show file tree
Hide file tree
Showing 6 changed files with 44 additions and 123 deletions.
23 changes: 6 additions & 17 deletions src/tools/miri/src/concurrency/data_race.rs
Original file line number Diff line number Diff line change
Expand Up @@ -498,7 +498,7 @@ impl MemoryCellClocks {
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,
Expand All @@ -509,12 +509,8 @@ impl MemoryCellClocks {
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
Expand Down Expand Up @@ -551,11 +547,9 @@ impl MemoryCellClocks {
}
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
};
Expand Down Expand Up @@ -955,9 +949,7 @@ impl VClockAlloc {
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)
Expand Down Expand Up @@ -1005,10 +997,7 @@ impl VClockAlloc {
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
};
Expand Down
30 changes: 0 additions & 30 deletions src/tools/miri/tests/fail/data_race/read_read_race1.rs

This file was deleted.

22 changes: 0 additions & 22 deletions src/tools/miri/tests/fail/data_race/read_read_race1.stderr

This file was deleted.

30 changes: 0 additions & 30 deletions src/tools/miri/tests/fail/data_race/read_read_race2.rs

This file was deleted.

22 changes: 0 additions & 22 deletions src/tools/miri/tests/fail/data_race/read_read_race2.stderr

This file was deleted.

40 changes: 38 additions & 2 deletions src/tools/miri/tests/pass/concurrency/data_race.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0

use std::sync::atomic::{fence, AtomicUsize, Ordering};
use std::thread::spawn;
use std::sync::atomic::*;
use std::thread::{self, spawn};

#[derive(Copy, Clone)]
struct EvilSend<T>(pub T);
Expand Down Expand Up @@ -112,9 +112,45 @@ pub fn test_simple_release() {
}
}

// 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_read_read_race1();
test_read_read_race2();
}

0 comments on commit 24c19b8

Please sign in to comment.