Skip to content
This repository was archived by the owner on May 28, 2025. It is now read-only.

Commit c2f459c

Browse files
saethlinsaethlin
committed
Clean up implementation, deduplicate in errors
1 parent 749b2b0 commit c2f459c

31 files changed

+103
-255
lines changed

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

Lines changed: 10 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -358,15 +358,9 @@ impl MemoryCellClocks {
358358
index: VectorIdx,
359359
) -> Result<(), DataRace> {
360360
log::trace!("Atomic read with vectors: {:#?} :: {:#?}", self, clocks);
361-
if self.write <= clocks.clock[self.write_index] {
362-
let atomic = self.atomic_mut();
363-
atomic.read_vector.set_at_index(&clocks.clock, index);
364-
Ok(())
365-
} else {
366-
let atomic = self.atomic_mut();
367-
atomic.read_vector.set_at_index(&clocks.clock, index);
368-
Err(DataRace)
369-
}
361+
let atomic = self.atomic_mut();
362+
atomic.read_vector.set_at_index(&clocks.clock, index);
363+
if self.write <= clocks.clock[self.write_index] { Ok(()) } else { Err(DataRace) }
370364
}
371365

372366
/// Detect data-races with an atomic write, either with a non-atomic read or with
@@ -377,13 +371,11 @@ impl MemoryCellClocks {
377371
index: VectorIdx,
378372
) -> Result<(), DataRace> {
379373
log::trace!("Atomic write with vectors: {:#?} :: {:#?}", self, clocks);
374+
let atomic = self.atomic_mut();
375+
atomic.write_vector.set_at_index(&clocks.clock, index);
380376
if self.write <= clocks.clock[self.write_index] && self.read <= clocks.clock {
381-
let atomic = self.atomic_mut();
382-
atomic.write_vector.set_at_index(&clocks.clock, index);
383377
Ok(())
384378
} else {
385-
let atomic = self.atomic_mut();
386-
atomic.write_vector.set_at_index(&clocks.clock, index);
387379
Err(DataRace)
388380
}
389381
}
@@ -635,6 +627,7 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
635627
if let Some(data_race) = &mut this.machine.data_race {
636628
data_race.maybe_perform_sync_operation(
637629
&this.machine.threads,
630+
current_span,
638631
|index, mut clocks| {
639632
log::trace!("Atomic fence on {:?} with ordering {:?}", index, atomic);
640633

@@ -658,7 +651,6 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
658651
// Increment timestamp in case of release semantics.
659652
Ok(atomic != AtomicFenceOrd::Acquire)
660653
},
661-
current_span,
662654
)
663655
} else {
664656
Ok(())
@@ -721,7 +713,7 @@ impl VClockAlloc {
721713
| MiriMemoryKind::ExternStatic
722714
| MiriMemoryKind::Tls,
723715
)
724-
| MemoryKind::CallerLocation => (VTimestamp::NONE, VectorIdx::MAX_INDEX),
716+
| MemoryKind::CallerLocation => (VTimestamp::ZERO, VectorIdx::MAX_INDEX),
725717
};
726718
VClockAlloc {
727719
alloc_ranges: RefCell::new(RangeMap::new(
@@ -752,7 +744,7 @@ impl VClockAlloc {
752744
let idx = l_remainder_slice
753745
.iter()
754746
.enumerate()
755-
.find_map(|(idx, &r)| if r == VTimestamp::NONE { None } else { Some(idx) })
747+
.find_map(|(idx, &r)| if r == VTimestamp::ZERO { None } else { Some(idx) })
756748
.expect("Invalid VClock Invariant");
757749
Some(idx + r_slice.len())
758750
} else {
@@ -1132,6 +1124,7 @@ trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
11321124
// Perform the atomic operation.
11331125
data_race.maybe_perform_sync_operation(
11341126
&this.machine.threads,
1127+
current_span,
11351128
|index, mut clocks| {
11361129
for (offset, range) in
11371130
alloc_meta.alloc_ranges.borrow_mut().iter_mut(base_offset, size)
@@ -1153,7 +1146,6 @@ trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
11531146
// This conservatively assumes all operations have release semantics
11541147
Ok(true)
11551148
},
1156-
current_span,
11571149
)?;
11581150

11591151
// Log changes to atomic memory.
@@ -1497,8 +1489,8 @@ impl GlobalState {
14971489
fn maybe_perform_sync_operation<'tcx>(
14981490
&self,
14991491
thread_mgr: &ThreadManager<'_, '_>,
1500-
op: impl FnOnce(VectorIdx, RefMut<'_, ThreadClockSet>) -> InterpResult<'tcx, bool>,
15011492
current_span: Span,
1493+
op: impl FnOnce(VectorIdx, RefMut<'_, ThreadClockSet>) -> InterpResult<'tcx, bool>,
15021494
) -> InterpResult<'tcx> {
15031495
if self.multi_threaded.get() {
15041496
let (index, clocks) = self.current_thread_state_mut(thread_mgr);

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

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -48,14 +48,14 @@ const SMALL_VECTOR: usize = 4;
4848
/// The time-stamps recorded in the data-race detector consist of both
4949
/// a 32-bit unsigned integer which is the actual timestamp, and a `Span`
5050
/// so that diagnostics can report what code was responsible for an operation.
51-
#[derive(Clone, Copy, Debug, Eq)]
51+
#[derive(Clone, Copy, Debug)]
5252
pub struct VTimestamp {
5353
time: u32,
5454
pub span: Span,
5555
}
5656

5757
impl VTimestamp {
58-
pub const NONE: VTimestamp = VTimestamp { time: 0, span: DUMMY_SP };
58+
pub const ZERO: VTimestamp = VTimestamp { time: 0, span: DUMMY_SP };
5959

6060
pub fn span_data(&self) -> SpanData {
6161
self.span.data()
@@ -68,6 +68,8 @@ impl PartialEq for VTimestamp {
6868
}
6969
}
7070

71+
impl Eq for VTimestamp {}
72+
7173
impl PartialOrd for VTimestamp {
7274
fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
7375
Some(self.cmp(other))
@@ -98,7 +100,7 @@ impl VClock {
98100
/// for a value at the given index
99101
pub fn new_with_index(index: VectorIdx, timestamp: VTimestamp) -> VClock {
100102
let len = index.index() + 1;
101-
let mut vec = smallvec::smallvec![VTimestamp::NONE; len];
103+
let mut vec = smallvec::smallvec![VTimestamp::ZERO; len];
102104
vec[index.index()] = timestamp;
103105
VClock(vec)
104106
}
@@ -115,7 +117,7 @@ impl VClock {
115117
#[inline]
116118
fn get_mut_with_min_len(&mut self, min_len: usize) -> &mut [VTimestamp] {
117119
if self.0.len() < min_len {
118-
self.0.resize(min_len, VTimestamp::NONE);
120+
self.0.resize(min_len, VTimestamp::ZERO);
119121
}
120122
assert!(self.0.len() >= min_len);
121123
self.0.as_mut_slice()
@@ -361,7 +363,7 @@ impl Index<VectorIdx> for VClock {
361363

362364
#[inline]
363365
fn index(&self, index: VectorIdx) -> &VTimestamp {
364-
self.as_slice().get(index.to_u32() as usize).unwrap_or(&VTimestamp::NONE)
366+
self.as_slice().get(index.to_u32() as usize).unwrap_or(&VTimestamp::ZERO)
365367
}
366368
}
367369

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -258,7 +258,7 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
258258
// The thread index and timestamp of the initialisation write
259259
// are never meaningfully used, so it's fine to leave them as 0
260260
store_index: VectorIdx::from(0),
261-
timestamp: VTimestamp::NONE,
261+
timestamp: VTimestamp::ZERO,
262262
val: init,
263263
is_seqcst: false,
264264
load_info: RefCell::new(LoadInfo::default()),

‎src/tools/miri/src/diagnostics.rs‎

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -69,8 +69,8 @@ impl fmt::Display for TerminationInfo {
6969
DataRace { ptr, op1, op2 } =>
7070
write!(
7171
f,
72-
"Data race detected between {} on {} and {} on {} at {:?}",
73-
op1.action, op1.thread_info, op2.action, op2.thread_info, ptr,
72+
"Data race detected between {} on {} and {} on {} at {:?}. The {} is here",
73+
op1.action, op1.thread_info, op2.action, op2.thread_info, ptr, op1.action
7474
),
7575
}
7676
}
@@ -222,10 +222,9 @@ pub fn report_error<'tcx, 'mir>(
222222
vec![(Some(*span), format!("the `{link_name}` symbol is defined here"))],
223223
Int2PtrWithStrictProvenance =>
224224
vec![(None, format!("use Strict Provenance APIs (https://doc.rust-lang.org/nightly/std/ptr/index.html#strict-provenance, https://crates.io/crates/sptr) instead"))],
225-
DataRace { ptr: _, op1, op2 } =>
225+
DataRace { op2, .. } =>
226226
vec![
227-
(Some(op1.span), format!("The {} on {} is here", op1.action, op1.thread_info)),
228-
(Some(op2.span), format!("The {} on {} is here", op2.action, op2.thread_info)),
227+
(Some(op2.span), format!("and {} on {}, which is here", op2.action, op2.thread_info)),
229228
(None, format!("this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior")),
230229
(None, format!("see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information")),
231230
],

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

Lines changed: 3 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,10 @@
1-
error: Undefined Behavior: Data race detected between Read on thread `<unnamed>` and Allocate on thread `<unnamed>` at ALLOC
1+
error: Undefined Behavior: Data race detected between Read on thread `<unnamed>` and Allocate on thread `<unnamed>` at ALLOC. The Read is here
22
--> $DIR/alloc_read_race.rs:LL:CC
33
|
44
LL | *pointer.load(Ordering::Relaxed)
5-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between Read on thread `<unnamed>` and Allocate on thread `<unnamed>` at ALLOC
5+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between Read on thread `<unnamed>` and Allocate on thread `<unnamed>` at ALLOC. The Read is here
66
|
7-
help: The Read on thread `<unnamed>` is here
8-
--> $DIR/alloc_read_race.rs:LL:CC
9-
|
10-
LL | ... *pointer.load(Ordering::Relaxed)
11-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
12-
help: The Allocate on thread `<unnamed>` is here
7+
help: and Allocate on thread `<unnamed>`, which is here
138
--> $DIR/alloc_read_race.rs:LL:CC
149
|
1510
LL | pointer.store(Box::into_raw(Box::new_uninit()), Ordering::Relaxed);

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

Lines changed: 3 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,10 @@
1-
error: Undefined Behavior: Data race detected between Write on thread `<unnamed>` and Allocate on thread `<unnamed>` at ALLOC
1+
error: Undefined Behavior: Data race detected between Write on thread `<unnamed>` and Allocate on thread `<unnamed>` at ALLOC. The Write is here
22
--> $DIR/alloc_write_race.rs:LL:CC
33
|
44
LL | *pointer.load(Ordering::Relaxed) = 2;
5-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between Write on thread `<unnamed>` and Allocate on thread `<unnamed>` at ALLOC
5+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between Write on thread `<unnamed>` and Allocate on thread `<unnamed>` at ALLOC. The Write is here
66
|
7-
help: The Write on thread `<unnamed>` is here
8-
--> $DIR/alloc_write_race.rs:LL:CC
9-
|
10-
LL | ... *pointer.load(Ordering::Relaxed) = 2;
11-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
12-
help: The Allocate on thread `<unnamed>` is here
7+
help: and Allocate on thread `<unnamed>`, which is here
138
--> $DIR/alloc_write_race.rs:LL:CC
149
|
1510
LL | .store(Box::into_raw(Box::<usize>::new_uninit()) as *mut usize, Ordering::Relaxed);

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

Lines changed: 3 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,10 @@
1-
error: Undefined Behavior: Data race detected between Atomic Load on thread `<unnamed>` and Write on thread `<unnamed>` at ALLOC
1+
error: Undefined Behavior: Data race detected between Atomic Load on thread `<unnamed>` and Write on thread `<unnamed>` at ALLOC. The Atomic Load is here
22
--> $DIR/atomic_read_na_write_race1.rs:LL:CC
33
|
44
LL | (&*c.0).load(Ordering::SeqCst)
5-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between Atomic Load on thread `<unnamed>` and Write on thread `<unnamed>` at ALLOC
5+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between Atomic Load on thread `<unnamed>` and Write on thread `<unnamed>` at ALLOC. The Atomic Load is here
66
|
7-
help: The Atomic Load on thread `<unnamed>` is here
8-
--> $DIR/atomic_read_na_write_race1.rs:LL:CC
9-
|
10-
LL | ... (&*c.0).load(Ordering::SeqCst)
11-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
12-
help: The Write on thread `<unnamed>` is here
7+
help: and Write on thread `<unnamed>`, which is here
138
--> $DIR/atomic_read_na_write_race1.rs:LL:CC
149
|
1510
LL | *(c.0 as *mut usize) = 32;

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

Lines changed: 3 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,10 @@
1-
error: Undefined Behavior: Data race detected between Write on thread `<unnamed>` and Atomic Load on thread `<unnamed>` at ALLOC
1+
error: Undefined Behavior: Data race detected between Write on thread `<unnamed>` and Atomic Load on thread `<unnamed>` at ALLOC. The Write is here
22
--> $DIR/atomic_read_na_write_race2.rs:LL:CC
33
|
44
LL | *atomic_ref.get_mut() = 32;
5-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between Write on thread `<unnamed>` and Atomic Load on thread `<unnamed>` at ALLOC
5+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between Write on thread `<unnamed>` and Atomic Load on thread `<unnamed>` at ALLOC. The Write is here
66
|
7-
help: The Write on thread `<unnamed>` is here
8-
--> $DIR/atomic_read_na_write_race2.rs:LL:CC
9-
|
10-
LL | ... *atomic_ref.get_mut() = 32;
11-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^
12-
help: The Atomic Load on thread `<unnamed>` is here
7+
help: and Atomic Load on thread `<unnamed>`, which is here
138
--> $DIR/atomic_read_na_write_race2.rs:LL:CC
149
|
1510
LL | atomic_ref.load(Ordering::SeqCst)

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

Lines changed: 3 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,10 @@
1-
error: Undefined Behavior: Data race detected between Read on thread `<unnamed>` and Atomic Store on thread `<unnamed>` at ALLOC
1+
error: Undefined Behavior: Data race detected between Read on thread `<unnamed>` and Atomic Store on thread `<unnamed>` at ALLOC. The Read is here
22
--> $DIR/atomic_write_na_read_race1.rs:LL:CC
33
|
44
LL | *atomic_ref.get_mut()
5-
| ^^^^^^^^^^^^^^^^^^^^^ Data race detected between Read on thread `<unnamed>` and Atomic Store on thread `<unnamed>` at ALLOC
5+
| ^^^^^^^^^^^^^^^^^^^^^ Data race detected between Read on thread `<unnamed>` and Atomic Store on thread `<unnamed>` at ALLOC. The Read is here
66
|
7-
help: The Read on thread `<unnamed>` is here
8-
--> $DIR/atomic_write_na_read_race1.rs:LL:CC
9-
|
10-
LL | *atomic_ref.get_mut()
11-
| ^^^^^^^^^^^^^^^^^^^^^
12-
help: The Atomic Store on thread `<unnamed>` is here
7+
help: and Atomic Store on thread `<unnamed>`, which is here
138
--> $DIR/atomic_write_na_read_race1.rs:LL:CC
149
|
1510
LL | atomic_ref.store(32, Ordering::SeqCst)

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

Lines changed: 3 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,10 @@
1-
error: Undefined Behavior: Data race detected between Atomic Store on thread `<unnamed>` and Read on thread `<unnamed>` at ALLOC
1+
error: Undefined Behavior: Data race detected between Atomic Store on thread `<unnamed>` and Read on thread `<unnamed>` at ALLOC. The Atomic Store is here
22
--> $DIR/atomic_write_na_read_race2.rs:LL:CC
33
|
44
LL | (&*c.0).store(32, Ordering::SeqCst);
5-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between Atomic Store on thread `<unnamed>` and Read on thread `<unnamed>` at ALLOC
5+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between Atomic Store on thread `<unnamed>` and Read on thread `<unnamed>` at ALLOC. The Atomic Store is here
66
|
7-
help: The Atomic Store on thread `<unnamed>` is here
8-
--> $DIR/atomic_write_na_read_race2.rs:LL:CC
9-
|
10-
LL | ... (&*c.0).store(32, Ordering::SeqCst);
11-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
12-
help: The Read on thread `<unnamed>` is here
7+
help: and Read on thread `<unnamed>`, which is here
138
--> $DIR/atomic_write_na_read_race2.rs:LL:CC
149
|
1510
LL | let _val = *(c.0 as *mut usize);

0 commit comments

Comments
 (0)