Skip to content

Commit ed417f4

Browse files
committed
miri: no longer complain about read-read races
1 parent 76bce58 commit ed417f4

6 files changed

Lines changed: 43 additions & 122 deletions

File tree

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

Lines changed: 6 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -499,7 +499,7 @@ impl MemoryCellClocks {
499499
Ok(())
500500
}
501501

502-
/// Detect data-races with an atomic read, caused by a non-atomic access that does
502+
/// Detect data-races with an atomic read, caused by a non-atomic write that does
503503
/// not happen-before the atomic-read.
504504
fnatomic_read_detect(
505505
&mutself,
@@ -510,12 +510,8 @@ impl MemoryCellClocks {
510510
trace!("Atomic read with vectors: {:#?} :: {:#?}",self, thread_clocks);
511511
let atomic = self.atomic_access(thread_clocks, access_size)?;
512512
atomic.read_vector.set_at_index(&thread_clocks.clock, index);
513-
// Make sure the last non-atomic write and all non-atomic reads were before this access.
514-
ifself.write_was_before(&thread_clocks.clock) && self.read <= thread_clocks.clock{
515-
Ok(())
516-
}else{
517-
Err(DataRace)
518-
}
513+
// Make sure the last non-atomic write was before this access.
514+
ifself.write_was_before(&thread_clocks.clock){Ok(())}else{Err(DataRace)}
519515
}
520516

521517
/// Detect data-races with an atomic write, either with a non-atomic read or with
@@ -552,11 +548,9 @@ impl MemoryCellClocks {
552548
}
553549
thread_clocks.clock.index_mut(index).set_read_type(read_type);
554550
ifself.write_was_before(&thread_clocks.clock){
551+
// We must be ordered-after all atomic writes.
555552
let race_free = ifletSome(atomic) = self.atomic(){
556-
// We must be ordered-after all atomic accesses, reads and writes.
557-
// This ensures we don't mix atomic and non-atomic accesses.
558553
atomic.write_vector <= thread_clocks.clock
559-
&& atomic.read_vector <= thread_clocks.clock
560554
}else{
561555
true
562556
};
@@ -957,9 +951,7 @@ impl VClockAlloc {
957951
letmut other_size = None;// if `Some`, this was a size-mismatch race
958952
let write_clock;
959953
let(other_access, other_thread, other_clock) =
960-
// First check the atomic-nonatomic cases. If it looks like multiple
961-
// cases apply, this one should take precedence, else it might look like
962-
// we are reporting races between two non-atomic reads.
954+
// First check the atomic-nonatomic cases.
963955
if !access.is_atomic() &&
964956
letSome(atomic) = mem_clocks.atomic() &&
965957
letSome(idx) = Self::find_gt_index(&atomic.write_vector,&active_clocks.clock)
@@ -1007,10 +999,7 @@ impl VClockAlloc {
1007999
assert!(!involves_non_atomic);
10081000
Some("overlapping unsynchronized atomic accesses must use the same access size")
10091001
}elseif access.is_read() && other_access.is_read(){
1010-
assert!(involves_non_atomic);
1011-
Some(
1012-
"overlapping atomic and non-atomic accesses must be synchronized, even if both are read-only",
1013-
)
1002+
panic!("there should be no same-size read-read races")
10141003
}else{
10151004
None
10161005
};

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

Lines changed: 0 additions & 30 deletions
This file was deleted.

‎src/tools/miri/tests/fail/data_race/read_read_race1.stderr‎

Lines changed: 0 additions & 22 deletions
This file was deleted.

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

Lines changed: 0 additions & 30 deletions
This file was deleted.

‎src/tools/miri/tests/fail/data_race/read_read_race2.stderr‎

Lines changed: 0 additions & 22 deletions
This file was deleted.

‎src/tools/miri/tests/pass/concurrency/data_race.rs‎

Lines changed: 37 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0
22

33
use std::sync::atomic::*;
4-
use std::thread::spawn;
4+
use std::thread::{self,spawn};
55

66
#[derive(Copy,Clone)]
77
structEvilSend<T>(pubT);
@@ -143,10 +143,46 @@ fn test_local_variable_lazy_write() {
143143
assert_eq!(val,127);
144144
}
145145

146+
// This test coverse the case where the non-atomic access come first.
147+
fntest_read_read_race1(){
148+
let a = AtomicU16::new(0);
149+
150+
thread::scope(|s| {
151+
s.spawn(|| {
152+
let ptr = &a as*constAtomicU16as*mutu16;
153+
unsafe{ ptr.read()};
154+
});
155+
s.spawn(|| {
156+
thread::yield_now();
157+
158+
a.load(Ordering::SeqCst);
159+
});
160+
});
161+
}
162+
163+
// This test coverse the case where the atomic access come first.
164+
fntest_read_read_race2(){
165+
let a = AtomicU16::new(0);
166+
167+
thread::scope(|s| {
168+
s.spawn(|| {
169+
a.load(Ordering::SeqCst);
170+
});
171+
s.spawn(|| {
172+
thread::yield_now();
173+
174+
let ptr = &a as*constAtomicU16as*mutu16;
175+
unsafe{ ptr.read()};
176+
});
177+
});
178+
}
179+
146180
pubfnmain(){
147181
test_fence_sync();
148182
test_multiple_reads();
149183
test_rmw_no_block();
150184
test_simple_release();
151185
test_local_variable_lazy_write();
186+
test_read_read_race1();
187+
test_read_read_race2();
152188
}

0 commit comments

Comments
 (0)