Skip to content

Commit 2ef639d

Browse files
committed
Auto merge of #3145 - RalfJung:data-race-error, r=RalfJung
give some more help for the unusual data races Fixes rust-lang/miri#3142
2 parents 1b2e4a9 + 278965a commit 2ef639d

File tree

73 files changed

+233
-166
lines changed

Some content is hidden

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

73 files changed

+233
-166
lines changed

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

+109-53
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,
@@ -206,7 +205,7 @@ enum AtomicAccessType {
206205
/// are all treated as writes for the purpose
207206
/// of the data-race detector.
208207
#[derive(Copy, Clone, PartialEq, Eq, Debug)]
209-
enum WriteType {
208+
enum NaWriteType {
210209
/// Allocate memory.
211210
Allocate,
212211

@@ -219,12 +218,48 @@ enum WriteType {
219218
/// (Same for `Allocate` above.)
220219
Deallocate,
221220
}
222-
impl WriteType {
223-
fn get_descriptor(self) -> &'static str {
221+
222+
impl NaWriteType {
223+
fn description(self) -> &'static str {
224224
match self {
225-
WriteType::Allocate => "Allocate",
226-
WriteType::Write => "Write",
227-
WriteType::Deallocate => "Deallocate",
225+
NaWriteType::Allocate => "creating a new allocation",
226+
NaWriteType::Write => "non-atomic write",
227+
NaWriteType::Deallocate => "deallocation",
228+
}
229+
}
230+
}
231+
232+
#[derive(Copy, Clone, PartialEq, Eq, Debug)]
233+
enum AccessType {
234+
NaRead,
235+
NaWrite(NaWriteType),
236+
AtomicLoad,
237+
AtomicStore,
238+
AtomicRmw,
239+
}
240+
241+
impl AccessType {
242+
fn description(self) -> &'static str {
243+
match self {
244+
AccessType::NaRead => "non-atomic read",
245+
AccessType::NaWrite(w) => w.description(),
246+
AccessType::AtomicLoad => "atomic load",
247+
AccessType::AtomicStore => "atomic store",
248+
AccessType::AtomicRmw => "atomic read-modify-write",
249+
}
250+
}
251+
252+
fn is_atomic(self) -> bool {
253+
match self {
254+
AccessType::AtomicLoad | AccessType::AtomicStore | AccessType::AtomicRmw => true,
255+
AccessType::NaRead | AccessType::NaWrite(_) => false,
256+
}
257+
}
258+
259+
fn is_read(self) -> bool {
260+
match self {
261+
AccessType::AtomicLoad | AccessType::NaRead => true,
262+
AccessType::NaWrite(_) | AccessType::AtomicStore | AccessType::AtomicRmw => false,
228263
}
229264
}
230265
}
@@ -241,7 +276,7 @@ struct MemoryCellClocks {
241276
/// The type of operation that the write index represents,
242277
/// either newly allocated memory, a non-atomic write or
243278
/// a deallocation of memory.
244-
write_type: WriteType,
279+
write_type: NaWriteType,
245280

246281
/// The vector-clock of all non-atomic reads that happened since the last non-atomic write
247282
/// (i.e., we join together the "singleton" clocks corresponding to each read). It is reset to
@@ -272,7 +307,7 @@ impl MemoryCellClocks {
272307
MemoryCellClocks {
273308
read: VClock::default(),
274309
write: (alloc_index, alloc),
275-
write_type: WriteType::Allocate,
310+
write_type: NaWriteType::Allocate,
276311
atomic_ops: None,
277312
}
278313
}
@@ -495,7 +530,7 @@ impl MemoryCellClocks {
495530
&mut self,
496531
thread_clocks: &mut ThreadClockSet,
497532
index: VectorIdx,
498-
write_type: WriteType,
533+
write_type: NaWriteType,
499534
current_span: Span,
500535
) -> Result<(), DataRace> {
501536
log::trace!("Unsynchronized write with vectors: {:#?} :: {:#?}", self, thread_clocks);
@@ -845,48 +880,45 @@ impl VClockAlloc {
845880
global: &GlobalState,
846881
thread_mgr: &ThreadManager<'_, '_>,
847882
mem_clocks: &MemoryCellClocks,
848-
action: &str,
849-
is_atomic: bool,
883+
access: AccessType,
850884
access_size: Size,
851885
ptr_dbg: Pointer<AllocId>,
852886
) -> InterpResult<'tcx> {
853887
let (current_index, current_clocks) = global.current_thread_state(thread_mgr);
854-
let mut action = Cow::Borrowed(action);
855-
let mut involves_non_atomic = true;
888+
let mut other_size = None; // if `Some`, this was a size-mismatch race
856889
let write_clock;
857-
let (other_action, other_thread, other_clock) =
890+
let (other_access, other_thread, other_clock) =
858891
// First check the atomic-nonatomic cases. If it looks like multiple
859892
// cases apply, this one should take precedence, else it might look like
860893
// we are reporting races between two non-atomic reads.
861-
if !is_atomic &&
894+
if !access.is_atomic() &&
862895
let Some(atomic) = mem_clocks.atomic() &&
863896
let Some(idx) = Self::find_gt_index(&atomic.write_vector, &current_clocks.clock)
864897
{
865-
(format!("Atomic Store"), idx, &atomic.write_vector)
866-
} else if !is_atomic &&
898+
(AccessType::AtomicStore, idx, &atomic.write_vector)
899+
} else if !access.is_atomic() &&
867900
let Some(atomic) = mem_clocks.atomic() &&
868901
let Some(idx) = Self::find_gt_index(&atomic.read_vector, &current_clocks.clock)
869902
{
870-
(format!("Atomic Load"), idx, &atomic.read_vector)
903+
(AccessType::AtomicLoad, idx, &atomic.read_vector)
871904
// Then check races with non-atomic writes/reads.
872905
} else if mem_clocks.write.1 > current_clocks.clock[mem_clocks.write.0] {
873906
write_clock = mem_clocks.write();
874-
(mem_clocks.write_type.get_descriptor().to_owned(), mem_clocks.write.0, &write_clock)
907+
(AccessType::NaWrite(mem_clocks.write_type), mem_clocks.write.0, &write_clock)
875908
} else if let Some(idx) = Self::find_gt_index(&mem_clocks.read, &current_clocks.clock) {
876-
(format!("Read"), idx, &mem_clocks.read)
909+
(AccessType::NaRead, idx, &mem_clocks.read)
877910
// Finally, mixed-size races.
878-
} else if is_atomic && let Some(atomic) = mem_clocks.atomic() && atomic.size != access_size {
911+
} else if access.is_atomic() && let Some(atomic) = mem_clocks.atomic() && atomic.size != access_size {
879912
// This is only a race if we are not synchronized with all atomic accesses, so find
880913
// the one we are not synchronized with.
881-
involves_non_atomic = false;
882-
action = format!("{}-byte (different-size) {action}", access_size.bytes()).into();
914+
other_size = Some(atomic.size);
883915
if let Some(idx) = Self::find_gt_index(&atomic.write_vector, &current_clocks.clock)
884916
{
885-
(format!("{}-byte Atomic Store", atomic.size.bytes()), idx, &atomic.write_vector)
917+
(AccessType::AtomicStore, idx, &atomic.write_vector)
886918
} else if let Some(idx) =
887919
Self::find_gt_index(&atomic.read_vector, &current_clocks.clock)
888920
{
889-
(format!("{}-byte Atomic Load", atomic.size.bytes()), idx, &atomic.read_vector)
921+
(AccessType::AtomicLoad, idx, &atomic.read_vector)
890922
} else {
891923
unreachable!(
892924
"Failed to report data-race for mixed-size access: no race found"
@@ -899,18 +931,39 @@ impl VClockAlloc {
899931
// Load elaborated thread information about the racing thread actions.
900932
let current_thread_info = global.print_thread_metadata(thread_mgr, current_index);
901933
let other_thread_info = global.print_thread_metadata(thread_mgr, other_thread);
934+
let involves_non_atomic = !access.is_atomic() || !other_access.is_atomic();
902935

903936
// Throw the data-race detection.
937+
let extra = if other_size.is_some() {
938+
assert!(!involves_non_atomic);
939+
Some("overlapping unsynchronized atomic accesses must use the same access size")
940+
} else if access.is_read() && other_access.is_read() {
941+
assert!(involves_non_atomic);
942+
Some(
943+
"overlapping atomic and non-atomic accesses must be synchronized, even if both are read-only",
944+
)
945+
} else {
946+
None
947+
};
904948
Err(err_machine_stop!(TerminationInfo::DataRace {
905949
involves_non_atomic,
950+
extra,
906951
ptr: ptr_dbg,
907952
op1: RacingOp {
908-
action: other_action.to_string(),
953+
action: if let Some(other_size) = other_size {
954+
format!("{}-byte {}", other_size.bytes(), other_access.description())
955+
} else {
956+
other_access.description().to_owned()
957+
},
909958
thread_info: other_thread_info,
910959
span: other_clock.as_slice()[other_thread.index()].span_data(),
911960
},
912961
op2: RacingOp {
913-
action: action.to_string(),
962+
action: if other_size.is_some() {
963+
format!("{}-byte {}", access_size.bytes(), access.description())
964+
} else {
965+
access.description().to_owned()
966+
},
914967
thread_info: current_thread_info,
915968
span: current_clocks.clock.as_slice()[current_index.index()].span_data(),
916969
},
@@ -945,8 +998,7 @@ impl VClockAlloc {
945998
global,
946999
&machine.threads,
9471000
mem_clocks,
948-
"Read",
949-
/* is_atomic */ false,
1001+
AccessType::NaRead,
9501002
access_range.size,
9511003
Pointer::new(alloc_id, Size::from_bytes(mem_clocks_range.start)),
9521004
);
@@ -963,7 +1015,7 @@ impl VClockAlloc {
9631015
&mut self,
9641016
alloc_id: AllocId,
9651017
access_range: AllocRange,
966-
write_type: WriteType,
1018+
write_type: NaWriteType,
9671019
machine: &mut MiriMachine<'_, '_>,
9681020
) -> InterpResult<'tcx> {
9691021
let current_span = machine.current_span();
@@ -985,8 +1037,7 @@ impl VClockAlloc {
9851037
global,
9861038
&machine.threads,
9871039
mem_clocks,
988-
write_type.get_descriptor(),
989-
/* is_atomic */ false,
1040+
AccessType::NaWrite(write_type),
9901041
access_range.size,
9911042
Pointer::new(alloc_id, Size::from_bytes(mem_clocks_range.start)),
9921043
);
@@ -1008,7 +1059,7 @@ impl VClockAlloc {
10081059
range: AllocRange,
10091060
machine: &mut MiriMachine<'_, '_>,
10101061
) -> InterpResult<'tcx> {
1011-
self.unique_access(alloc_id, range, WriteType::Write, machine)
1062+
self.unique_access(alloc_id, range, NaWriteType::Write, machine)
10121063
}
10131064

10141065
/// Detect data-races for an unsynchronized deallocate operation, will not perform
@@ -1021,7 +1072,7 @@ impl VClockAlloc {
10211072
range: AllocRange,
10221073
machine: &mut MiriMachine<'_, '_>,
10231074
) -> InterpResult<'tcx> {
1024-
self.unique_access(alloc_id, range, WriteType::Deallocate, machine)
1075+
self.unique_access(alloc_id, range, NaWriteType::Deallocate, machine)
10251076
}
10261077
}
10271078

@@ -1134,7 +1185,7 @@ trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
11341185
this.validate_atomic_op(
11351186
place,
11361187
atomic,
1137-
"Atomic Load",
1188+
AccessType::AtomicLoad,
11381189
move |memory, clocks, index, atomic| {
11391190
if atomic == AtomicReadOrd::Relaxed {
11401191
memory.load_relaxed(&mut *clocks, index, place.layout.size)
@@ -1156,7 +1207,7 @@ trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
11561207
this.validate_atomic_op(
11571208
place,
11581209
atomic,
1159-
"Atomic Store",
1210+
AccessType::AtomicStore,
11601211
move |memory, clocks, index, atomic| {
11611212
if atomic == AtomicWriteOrd::Relaxed {
11621213
memory.store_relaxed(clocks, index, place.layout.size)
@@ -1178,26 +1229,31 @@ trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
11781229
let acquire = matches!(atomic, Acquire | AcqRel | SeqCst);
11791230
let release = matches!(atomic, Release | AcqRel | SeqCst);
11801231
let this = self.eval_context_mut();
1181-
this.validate_atomic_op(place, atomic, "Atomic RMW", move |memory, clocks, index, _| {
1182-
if acquire {
1183-
memory.load_acquire(clocks, index, place.layout.size)?;
1184-
} else {
1185-
memory.load_relaxed(clocks, index, place.layout.size)?;
1186-
}
1187-
if release {
1188-
memory.rmw_release(clocks, index, place.layout.size)
1189-
} else {
1190-
memory.rmw_relaxed(clocks, index, place.layout.size)
1191-
}
1192-
})
1232+
this.validate_atomic_op(
1233+
place,
1234+
atomic,
1235+
AccessType::AtomicRmw,
1236+
move |memory, clocks, index, _| {
1237+
if acquire {
1238+
memory.load_acquire(clocks, index, place.layout.size)?;
1239+
} else {
1240+
memory.load_relaxed(clocks, index, place.layout.size)?;
1241+
}
1242+
if release {
1243+
memory.rmw_release(clocks, index, place.layout.size)
1244+
} else {
1245+
memory.rmw_relaxed(clocks, index, place.layout.size)
1246+
}
1247+
},
1248+
)
11931249
}
11941250

11951251
/// Generic atomic operation implementation
11961252
fn validate_atomic_op<A: Debug + Copy>(
11971253
&self,
11981254
place: &MPlaceTy<'tcx, Provenance>,
11991255
atomic: A,
1200-
description: &str,
1256+
access: AccessType,
12011257
mut op: impl FnMut(
12021258
&mut MemoryCellClocks,
12031259
&mut ThreadClockSet,
@@ -1206,6 +1262,7 @@ trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
12061262
) -> Result<(), DataRace>,
12071263
) -> InterpResult<'tcx> {
12081264
let this = self.eval_context_ref();
1265+
assert!(access.is_atomic());
12091266
if let Some(data_race) = &this.machine.data_race {
12101267
if data_race.race_detecting() {
12111268
let size = place.layout.size;
@@ -1215,7 +1272,7 @@ trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
12151272
let alloc_meta = this.get_alloc_extra(alloc_id)?.data_race.as_ref().unwrap();
12161273
log::trace!(
12171274
"Atomic op({}) with ordering {:?} on {:?} (size={})",
1218-
description,
1275+
access.description(),
12191276
&atomic,
12201277
place.ptr(),
12211278
size.bytes()
@@ -1237,8 +1294,7 @@ trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
12371294
data_race,
12381295
&this.machine.threads,
12391296
mem_clocks,
1240-
description,
1241-
/* is_atomic */ true,
1297+
access,
12421298
place.layout.size,
12431299
Pointer::new(
12441300
alloc_id,

src/tools/miri/src/diagnostics.rs

+12-7
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,7 @@ pub enum TerminationInfo {
4747
ptr: Pointer,
4848
op1: RacingOp,
4949
op2: RacingOp,
50+
extra: Option<&'static str>,
5051
},
5152
}
5253

@@ -75,7 +76,7 @@ impl fmt::Display for TerminationInfo {
7576
write!(f, "multiple definitions of symbol `{link_name}`"),
7677
SymbolShimClashing { link_name, .. } =>
7778
write!(f, "found `{link_name}` symbol definition that clashes with a built-in shim",),
78-
DataRace { involves_non_atomic, ptr, op1, op2 } =>
79+
DataRace { involves_non_atomic, ptr, op1, op2, .. } =>
7980
write!(
8081
f,
8182
"{} detected between (1) {} on {} and (2) {} on {} at {ptr:?}. (2) just happened here",
@@ -266,12 +267,16 @@ pub fn report_error<'tcx, 'mir>(
266267
vec![(Some(*span), format!("the `{link_name}` symbol is defined here"))],
267268
Int2PtrWithStrictProvenance =>
268269
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"))],
269-
DataRace { op1, .. } =>
270-
vec![
271-
(Some(op1.span), format!("and (1) occurred earlier here")),
272-
(None, format!("this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior")),
273-
(None, format!("see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information")),
274-
],
270+
DataRace { op1, extra, .. } => {
271+
let mut helps = vec![(Some(op1.span), format!("and (1) occurred earlier here"))];
272+
if let Some(extra) = extra {
273+
helps.push((None, format!("{extra}")))
274+
}
275+
helps.push((None, format!("this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior")));
276+
helps.push((None, format!("see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information")));
277+
helps
278+
}
279+
,
275280
_ => vec![],
276281
};
277282
(title, helps)

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

0 commit comments

Comments
 (0)