Skip to content

Commit 052539e

Browse files
RalfJungRalfJung
committed
data-race: preserve structured access information longer, and don't upper-case access types
1 parent 51ae1fe commit 052539e

File tree

70 files changed

+196
-154
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

70 files changed

+196
-154
lines changed

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

+92-50
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,6 @@
4141
//! on the data-race detection code.
4242
4343
use std::{
44-
borrow::Cow,
4544
cell::{Cell, Ref, RefCell, RefMut},
4645
fmt::Debug,
4746
mem,
@@ -199,7 +198,7 @@ struct AtomicMemoryCellClocks {
199198
/// are all treated as writes for the purpose
200199
/// of the data-race detector.
201200
#[derive(Copy, Clone, PartialEq, Eq, Debug)]
202-
enum WriteType {
201+
enum NaWriteType {
203202
/// Allocate memory.
204203
Allocate,
205204

@@ -212,12 +211,41 @@ enum WriteType {
212211
/// (Same for `Allocate` above.)
213212
Deallocate,
214213
}
215-
impl WriteType {
216-
fn get_descriptor(self) -> &'static str {
214+
215+
impl NaWriteType {
216+
fn description(self) -> &'static str {
217+
match self {
218+
NaWriteType::Allocate => "creating a new allocation",
219+
NaWriteType::Write => "non-atomic write",
220+
NaWriteType::Deallocate => "deallocation",
221+
}
222+
}
223+
}
224+
225+
#[derive(Copy, Clone, PartialEq, Eq, Debug)]
226+
enum AccessType {
227+
NaRead,
228+
NaWrite(NaWriteType),
229+
AtomicLoad,
230+
AtomicStore,
231+
AtomicRmw,
232+
}
233+
234+
impl AccessType {
235+
fn description(self) -> &'static str {
236+
match self {
237+
AccessType::NaRead => "non-atomic read",
238+
AccessType::NaWrite(w) => w.description(),
239+
AccessType::AtomicLoad => "atomic load",
240+
AccessType::AtomicStore => "atomic store",
241+
AccessType::AtomicRmw => "atomic read-modify-write",
242+
}
243+
}
244+
245+
fn is_atomic(self) -> bool {
217246
match self {
218-
WriteType::Allocate => "Allocate",
219-
WriteType::Write => "Write",
220-
WriteType::Deallocate => "Deallocate",
247+
AccessType::AtomicLoad | AccessType::AtomicStore | AccessType::AtomicRmw => true,
248+
AccessType::NaRead | AccessType::NaWrite(_) => false,
221249
}
222250
}
223251
}
@@ -234,7 +262,7 @@ struct MemoryCellClocks {
234262
/// The type of operation that the write index represents,
235263
/// either newly allocated memory, a non-atomic write or
236264
/// a deallocation of memory.
237-
write_type: WriteType,
265+
write_type: NaWriteType,
238266

239267
/// The vector-clock of all non-atomic reads that happened since the last non-atomic write
240268
/// (i.e., we join together the "singleton" clocks corresponding to each read). It is reset to
@@ -265,7 +293,7 @@ impl MemoryCellClocks {
265293
MemoryCellClocks {
266294
read: VClock::default(),
267295
write: (alloc_index, alloc),
268-
write_type: WriteType::Allocate,
296+
write_type: NaWriteType::Allocate,
269297
atomic_ops: None,
270298
}
271299
}
@@ -488,7 +516,7 @@ impl MemoryCellClocks {
488516
&mut self,
489517
thread_clocks: &mut ThreadClockSet,
490518
index: VectorIdx,
491-
write_type: WriteType,
519+
write_type: NaWriteType,
492520
current_span: Span,
493521
) -> Result<(), DataRace> {
494522
log::trace!("Unsynchronized write with vectors: {:#?} :: {:#?}", self, thread_clocks);
@@ -838,48 +866,47 @@ impl VClockAlloc {
838866
global: &GlobalState,
839867
thread_mgr: &ThreadManager<'_, '_>,
840868
mem_clocks: &MemoryCellClocks,
841-
action: &str,
842-
is_atomic: bool,
869+
access: AccessType,
843870
access_size: Size,
844871
ptr_dbg: Pointer<AllocId>,
845872
) -> InterpResult<'tcx> {
846873
let (current_index, current_clocks) = global.current_thread_state(thread_mgr);
847-
let mut action = Cow::Borrowed(action);
874+
let mut other_size = None; // if `Some`, this was a size-mismatch race
848875
let mut involves_non_atomic = true;
849876
let write_clock;
850877
let (other_action, other_thread, other_clock) =
851878
// First check the atomic-nonatomic cases. If it looks like multiple
852879
// cases apply, this one should take precedence, else it might look like
853880
// we are reporting races between two non-atomic reads.
854-
if !is_atomic &&
881+
if !access.is_atomic() &&
855882
let Some(atomic) = mem_clocks.atomic() &&
856883
let Some(idx) = Self::find_gt_index(&atomic.write_vector, &current_clocks.clock)
857884
{
858-
(format!("Atomic Store"), idx, &atomic.write_vector)
859-
} else if !is_atomic &&
885+
(AccessType::AtomicStore, idx, &atomic.write_vector)
886+
} else if !access.is_atomic() &&
860887
let Some(atomic) = mem_clocks.atomic() &&
861888
let Some(idx) = Self::find_gt_index(&atomic.read_vector, &current_clocks.clock)
862889
{
863-
(format!("Atomic Load"), idx, &atomic.read_vector)
890+
(AccessType::AtomicLoad, idx, &atomic.read_vector)
864891
// Then check races with non-atomic writes/reads.
865892
} else if mem_clocks.write.1 > current_clocks.clock[mem_clocks.write.0] {
866893
write_clock = mem_clocks.write();
867-
(mem_clocks.write_type.get_descriptor().to_owned(), mem_clocks.write.0, &write_clock)
894+
(AccessType::NaWrite(mem_clocks.write_type), mem_clocks.write.0, &write_clock)
868895
} else if let Some(idx) = Self::find_gt_index(&mem_clocks.read, &current_clocks.clock) {
869-
(format!("Read"), idx, &mem_clocks.read)
896+
(AccessType::NaRead, idx, &mem_clocks.read)
870897
// Finally, mixed-size races.
871-
} else if is_atomic && let Some(atomic) = mem_clocks.atomic() && atomic.size != access_size {
898+
} else if access.is_atomic() && let Some(atomic) = mem_clocks.atomic() && atomic.size != access_size {
872899
// This is only a race if we are not synchronized with all atomic accesses, so find
873900
// the one we are not synchronized with.
874901
involves_non_atomic = false;
875-
action = format!("{}-byte (different-size) {action}", access_size.bytes()).into();
902+
other_size = Some(atomic.size);
876903
if let Some(idx) = Self::find_gt_index(&atomic.write_vector, &current_clocks.clock)
877904
{
878-
(format!("{}-byte Atomic Store", atomic.size.bytes()), idx, &atomic.write_vector)
905+
(AccessType::AtomicStore, idx, &atomic.write_vector)
879906
} else if let Some(idx) =
880907
Self::find_gt_index(&atomic.read_vector, &current_clocks.clock)
881908
{
882-
(format!("{}-byte Atomic Load", atomic.size.bytes()), idx, &atomic.read_vector)
909+
(AccessType::AtomicLoad, idx, &atomic.read_vector)
883910
} else {
884911
unreachable!(
885912
"Failed to report data-race for mixed-size access: no race found"
@@ -898,12 +925,24 @@ impl VClockAlloc {
898925
involves_non_atomic,
899926
ptr: ptr_dbg,
900927
op1: RacingOp {
901-
action: other_action.to_string(),
928+
action: if let Some(other_size) = other_size {
929+
format!("{}-byte {}", other_size.bytes(), other_action.description())
930+
} else {
931+
other_action.description().to_owned()
932+
},
902933
thread_info: other_thread_info,
903934
span: other_clock.as_slice()[other_thread.index()].span_data(),
904935
},
905936
op2: RacingOp {
906-
action: action.to_string(),
937+
action: if other_size.is_some() {
938+
format!(
939+
"{}-byte (different-size) {}",
940+
access_size.bytes(),
941+
access.description()
942+
)
943+
} else {
944+
access.description().to_owned()
945+
},
907946
thread_info: current_thread_info,
908947
span: current_clocks.clock.as_slice()[current_index.index()].span_data(),
909948
},
@@ -938,8 +977,7 @@ impl VClockAlloc {
938977
global,
939978
&machine.threads,
940979
mem_clocks,
941-
"Read",
942-
/* is_atomic */ false,
980+
AccessType::NaRead,
943981
access_range.size,
944982
Pointer::new(alloc_id, Size::from_bytes(mem_clocks_range.start)),
945983
);
@@ -956,7 +994,7 @@ impl VClockAlloc {
956994
&mut self,
957995
alloc_id: AllocId,
958996
access_range: AllocRange,
959-
write_type: WriteType,
997+
write_type: NaWriteType,
960998
machine: &mut MiriMachine<'_, '_>,
961999
) -> InterpResult<'tcx> {
9621000
let current_span = machine.current_span();
@@ -978,8 +1016,7 @@ impl VClockAlloc {
9781016
global,
9791017
&machine.threads,
9801018
mem_clocks,
981-
write_type.get_descriptor(),
982-
/* is_atomic */ false,
1019+
AccessType::NaWrite(write_type),
9831020
access_range.size,
9841021
Pointer::new(alloc_id, Size::from_bytes(mem_clocks_range.start)),
9851022
);
@@ -1001,7 +1038,7 @@ impl VClockAlloc {
10011038
range: AllocRange,
10021039
machine: &mut MiriMachine<'_, '_>,
10031040
) -> InterpResult<'tcx> {
1004-
self.unique_access(alloc_id, range, WriteType::Write, machine)
1041+
self.unique_access(alloc_id, range, NaWriteType::Write, machine)
10051042
}
10061043

10071044
/// Detect data-races for an unsynchronized deallocate operation, will not perform
@@ -1014,7 +1051,7 @@ impl VClockAlloc {
10141051
range: AllocRange,
10151052
machine: &mut MiriMachine<'_, '_>,
10161053
) -> InterpResult<'tcx> {
1017-
self.unique_access(alloc_id, range, WriteType::Deallocate, machine)
1054+
self.unique_access(alloc_id, range, NaWriteType::Deallocate, machine)
10181055
}
10191056
}
10201057

@@ -1104,7 +1141,7 @@ trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
11041141
this.validate_atomic_op(
11051142
place,
11061143
atomic,
1107-
"Atomic Load",
1144+
AccessType::AtomicLoad,
11081145
move |memory, clocks, index, atomic| {
11091146
if atomic == AtomicReadOrd::Relaxed {
11101147
memory.load_relaxed(&mut *clocks, index, place.layout.size)
@@ -1126,7 +1163,7 @@ trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
11261163
this.validate_atomic_op(
11271164
place,
11281165
atomic,
1129-
"Atomic Store",
1166+
AccessType::AtomicStore,
11301167
move |memory, clocks, index, atomic| {
11311168
if atomic == AtomicWriteOrd::Relaxed {
11321169
memory.store_relaxed(clocks, index, place.layout.size)
@@ -1148,26 +1185,31 @@ trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
11481185
let acquire = matches!(atomic, Acquire | AcqRel | SeqCst);
11491186
let release = matches!(atomic, Release | AcqRel | SeqCst);
11501187
let this = self.eval_context_mut();
1151-
this.validate_atomic_op(place, atomic, "Atomic RMW", move |memory, clocks, index, _| {
1152-
if acquire {
1153-
memory.load_acquire(clocks, index, place.layout.size)?;
1154-
} else {
1155-
memory.load_relaxed(clocks, index, place.layout.size)?;
1156-
}
1157-
if release {
1158-
memory.rmw_release(clocks, index, place.layout.size)
1159-
} else {
1160-
memory.rmw_relaxed(clocks, index, place.layout.size)
1161-
}
1162-
})
1188+
this.validate_atomic_op(
1189+
place,
1190+
atomic,
1191+
AccessType::AtomicRmw,
1192+
move |memory, clocks, index, _| {
1193+
if acquire {
1194+
memory.load_acquire(clocks, index, place.layout.size)?;
1195+
} else {
1196+
memory.load_relaxed(clocks, index, place.layout.size)?;
1197+
}
1198+
if release {
1199+
memory.rmw_release(clocks, index, place.layout.size)
1200+
} else {
1201+
memory.rmw_relaxed(clocks, index, place.layout.size)
1202+
}
1203+
},
1204+
)
11631205
}
11641206

11651207
/// Generic atomic operation implementation
11661208
fn validate_atomic_op<A: Debug + Copy>(
11671209
&self,
11681210
place: &MPlaceTy<'tcx, Provenance>,
11691211
atomic: A,
1170-
description: &str,
1212+
access: AccessType,
11711213
mut op: impl FnMut(
11721214
&mut MemoryCellClocks,
11731215
&mut ThreadClockSet,
@@ -1176,6 +1218,7 @@ trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
11761218
) -> Result<(), DataRace>,
11771219
) -> InterpResult<'tcx> {
11781220
let this = self.eval_context_ref();
1221+
assert!(access.is_atomic());
11791222
if let Some(data_race) = &this.machine.data_race {
11801223
if data_race.race_detecting() {
11811224
let size = place.layout.size;
@@ -1185,7 +1228,7 @@ trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
11851228
let alloc_meta = this.get_alloc_extra(alloc_id)?.data_race.as_ref().unwrap();
11861229
log::trace!(
11871230
"Atomic op({}) with ordering {:?} on {:?} (size={})",
1188-
description,
1231+
access.description(),
11891232
&atomic,
11901233
place.ptr(),
11911234
size.bytes()
@@ -1207,8 +1250,7 @@ trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
12071250
data_race,
12081251
&this.machine.threads,
12091252
mem_clocks,
1210-
description,
1211-
/* is_atomic */ true,
1253+
access,
12121254
place.layout.size,
12131255
Pointer::new(
12141256
alloc_id,

‎src/tools/miri/tests/fail/both_borrows/retag_data_race_write.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ fn thread_1(p: SendPtr) {
1717
fn thread_2(p: SendPtr) {
1818
let p = p.0;
1919
unsafe {
20-
*p = 5; //~ ERROR: /Data race detected between \(1\) (Read|Write) on thread `<unnamed>` and \(2\) Write on thread `<unnamed>`/
20+
*p = 5; //~ ERROR: /Data race detected between \(1\) non-atomic (read|write) on thread `<unnamed>` and \(2\) non-atomic write on thread `<unnamed>`/
2121
}
2222
}
2323

‎src/tools/miri/tests/fail/both_borrows/retag_data_race_write.stack.stderr

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
error: Undefined Behavior: Data race detected between (1) Write on thread `<unnamed>` and (2) Write on thread `<unnamed>` at ALLOC. (2) just happened here
1+
error: Undefined Behavior: Data race detected between (1) non-atomic write on thread `<unnamed>` and (2) non-atomic write on thread `<unnamed>` at ALLOC. (2) just happened here
22
--> $DIR/retag_data_race_write.rs:LL:CC
33
|
44
LL | *p = 5;
5-
| ^^^^^^ Data race detected between (1) Write on thread `<unnamed>` and (2) Write on thread `<unnamed>` at ALLOC. (2) just happened here
5+
| ^^^^^^ Data race detected between (1) non-atomic write on thread `<unnamed>` and (2) non-atomic write on thread `<unnamed>` at ALLOC. (2) just happened here
66
|
77
help: and (1) occurred earlier here
88
--> $DIR/retag_data_race_write.rs:LL:CC

‎src/tools/miri/tests/fail/both_borrows/retag_data_race_write.tree.stderr

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
error: Undefined Behavior: Data race detected between (1) Read on thread `<unnamed>` and (2) Write on thread `<unnamed>` at ALLOC. (2) just happened here
1+
error: Undefined Behavior: Data race detected between (1) non-atomic read on thread `<unnamed>` and (2) non-atomic write on thread `<unnamed>` at ALLOC. (2) just happened here
22
--> $DIR/retag_data_race_write.rs:LL:CC
33
|
44
LL | *p = 5;
5-
| ^^^^^^ Data race detected between (1) Read on thread `<unnamed>` and (2) Write on thread `<unnamed>` at ALLOC. (2) just happened here
5+
| ^^^^^^ Data race detected between (1) non-atomic read on thread `<unnamed>` and (2) non-atomic write on thread `<unnamed>` at ALLOC. (2) just happened here
66
|
77
help: and (1) occurred earlier here
88
--> $DIR/retag_data_race_write.rs:LL:CC

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ pub fn main() {
3939
let pointer = &*ptr.0;
4040

4141
// Note: could also error due to reading uninitialized memory, but the data-race detector triggers first.
42-
*pointer.load(Ordering::Relaxed) //~ ERROR: Data race detected between (1) Allocate on thread `<unnamed>` and (2) Read on thread `<unnamed>`
42+
*pointer.load(Ordering::Relaxed) //~ ERROR: Data race detected between (1) creating a new allocation on thread `<unnamed>` and (2) non-atomic read on thread `<unnamed>`
4343
});
4444

4545
j1.join().unwrap();

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

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
error: Undefined Behavior: Data race detected between (1) Allocate on thread `<unnamed>` and (2) Read on thread `<unnamed>` at ALLOC. (2) just happened here
1+
error: Undefined Behavior: Data race detected between (1) creating a new allocation on thread `<unnamed>` and (2) non-atomic read on thread `<unnamed>` at ALLOC. (2) just happened here
22
--> $DIR/alloc_read_race.rs:LL:CC
33
|
44
LL | *pointer.load(Ordering::Relaxed)
5-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between (1) Allocate on thread `<unnamed>` and (2) Read on thread `<unnamed>` at ALLOC. (2) just happened here
5+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between (1) creating a new allocation on thread `<unnamed>` and (2) non-atomic read on thread `<unnamed>` at ALLOC. (2) just happened here
66
|
77
help: and (1) occurred earlier here
88
--> $DIR/alloc_read_race.rs:LL:CC

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ pub fn main() {
3737
let j2 = spawn(move || {
3838
let ptr = ptr; // avoid field capturing
3939
let pointer = &*ptr.0;
40-
*pointer.load(Ordering::Relaxed) = 2; //~ ERROR: Data race detected between (1) Allocate on thread `<unnamed>` and (2) Write on thread `<unnamed>`
40+
*pointer.load(Ordering::Relaxed) = 2; //~ ERROR: Data race detected between (1) creating a new allocation on thread `<unnamed>` and (2) non-atomic write on thread `<unnamed>`
4141
});
4242

4343
j1.join().unwrap();

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

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
error: Undefined Behavior: Data race detected between (1) Allocate on thread `<unnamed>` and (2) Write on thread `<unnamed>` at ALLOC. (2) just happened here
1+
error: Undefined Behavior: Data race detected between (1) creating a new allocation on thread `<unnamed>` and (2) non-atomic write on thread `<unnamed>` at ALLOC. (2) just happened here
22
--> $DIR/alloc_write_race.rs:LL:CC
33
|
44
LL | *pointer.load(Ordering::Relaxed) = 2;
5-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between (1) Allocate on thread `<unnamed>` and (2) Write on thread `<unnamed>` at ALLOC. (2) just happened here
5+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between (1) creating a new allocation on thread `<unnamed>` and (2) non-atomic write on thread `<unnamed>` at ALLOC. (2) just happened here
66
|
77
help: and (1) occurred earlier here
88
--> $DIR/alloc_write_race.rs:LL:CC

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ pub fn main() {
2222

2323
let j2 = spawn(move || {
2424
let c = c; // avoid field capturing
25-
(&*c.0).load(Ordering::SeqCst) //~ ERROR: Data race detected between (1) Write on thread `<unnamed>` and (2) Atomic Load on thread `<unnamed>`
25+
(&*c.0).load(Ordering::SeqCst) //~ ERROR: Data race detected between (1) non-atomic write on thread `<unnamed>` and (2) atomic load on thread `<unnamed>`
2626
});
2727

2828
j1.join().unwrap();

0 commit comments

Comments
 (0)