don't talk about 'Data race' when both accesses are atomic

This commit is contained in:
Ralf Jung 2023-10-23 12:38:33 +02:00
parent 369c6d180c
commit e94c18ea87
8 changed files with 22 additions and 14 deletions

View file

@ -845,6 +845,7 @@ impl VClockAlloc {
) -> InterpResult<'tcx> {
let (current_index, current_clocks) = global.current_thread_state(thread_mgr);
let mut action = Cow::Borrowed(action);
let mut involves_non_atomic = true;
let write_clock;
#[rustfmt::skip]
let (other_action, other_thread, other_clock) =
@ -856,6 +857,7 @@ impl VClockAlloc {
} else if is_atomic && let Some(atomic) = mem_clocks.atomic() && atomic.size != access_size {
// This is only a race if we are not synchronized with all atomic accesses, so find
// the one we are not synchronized with.
involves_non_atomic = false;
action = format!("{}-byte (different-size) {action}", access_size.bytes()).into();
if let Some(idx) = Self::find_gt_index(&atomic.write_vector, &current_clocks.clock)
{
@ -898,6 +900,7 @@ impl VClockAlloc {
// Throw the data-race detection.
Err(err_machine_stop!(TerminationInfo::DataRace {
involves_non_atomic,
ptr: ptr_dbg,
op1: RacingOp {
action: other_action.to_string(),

View file

@ -43,9 +43,10 @@ pub enum TerminationInfo {
span: SpanData,
},
DataRace {
involves_non_atomic: bool,
ptr: Pointer,
op1: RacingOp,
op2: RacingOp,
ptr: Pointer,
},
}
@ -74,11 +75,15 @@ impl fmt::Display for TerminationInfo {
write!(f, "multiple definitions of symbol `{link_name}`"),
SymbolShimClashing { link_name, .. } =>
write!(f, "found `{link_name}` symbol definition that clashes with a built-in shim",),
DataRace { ptr, op1, op2 } =>
DataRace { involves_non_atomic, ptr, op1, op2 } =>
write!(
f,
"Data race detected between (1) {} on {} and (2) {} on {} at {ptr:?}. (2) just happened here",
op1.action, op1.thread_info, op2.action, op2.thread_info
"{} detected between (1) {} on {} and (2) {} on {} at {ptr:?}. (2) just happened here",
if *involves_non_atomic { "Data race" } else { "Race condition" },
op1.action,
op1.thread_info,
op2.action,
op2.thread_info
),
}
}

View file

@ -19,7 +19,7 @@ fn main() {
});
s.spawn(|| {
a8[0].load(Ordering::SeqCst);
//~^ ERROR: Data race detected between (1) 2-byte Atomic Load on thread `<unnamed>` and (2) 1-byte (different-size) Atomic Load on thread `<unnamed>`
//~^ ERROR: Race condition detected between (1) 2-byte Atomic Load on thread `<unnamed>` and (2) 1-byte (different-size) Atomic Load on thread `<unnamed>`
});
});
}

View file

@ -1,8 +1,8 @@
error: Undefined Behavior: Data race detected between (1) 2-byte Atomic Load on thread `<unnamed>` and (2) 1-byte (different-size) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
error: Undefined Behavior: Race condition detected between (1) 2-byte Atomic Load on thread `<unnamed>` and (2) 1-byte (different-size) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
--> $DIR/mixed_size_read.rs:LL:CC
|
LL | a8[0].load(Ordering::SeqCst);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between (1) 2-byte Atomic Load on thread `<unnamed>` and (2) 1-byte (different-size) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Race condition detected between (1) 2-byte Atomic Load on thread `<unnamed>` and (2) 1-byte (different-size) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
|
help: and (1) occurred earlier here
--> $DIR/mixed_size_read.rs:LL:CC

View file

@ -19,7 +19,7 @@ fn main() {
});
s.spawn(|| {
a8[0].store(1, Ordering::SeqCst);
//~^ ERROR: Data race detected between (1) 2-byte Atomic Store on thread `<unnamed>` and (2) 1-byte (different-size) Atomic Store on thread `<unnamed>`
//~^ ERROR: Race condition detected between (1) 2-byte Atomic Store on thread `<unnamed>` and (2) 1-byte (different-size) Atomic Store on thread `<unnamed>`
});
});
}

View file

@ -1,8 +1,8 @@
error: Undefined Behavior: Data race detected between (1) 2-byte Atomic Store on thread `<unnamed>` and (2) 1-byte (different-size) Atomic Store on thread `<unnamed>` at ALLOC. (2) just happened here
error: Undefined Behavior: Race condition detected between (1) 2-byte Atomic Store on thread `<unnamed>` and (2) 1-byte (different-size) Atomic Store on thread `<unnamed>` at ALLOC. (2) just happened here
--> $DIR/mixed_size_write.rs:LL:CC
|
LL | a8[0].store(1, Ordering::SeqCst);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between (1) 2-byte Atomic Store on thread `<unnamed>` and (2) 1-byte (different-size) Atomic Store on thread `<unnamed>` at ALLOC. (2) just happened here
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Race condition detected between (1) 2-byte Atomic Store on thread `<unnamed>` and (2) 1-byte (different-size) Atomic Store on thread `<unnamed>` at ALLOC. (2) just happened here
|
help: and (1) occurred earlier here
--> $DIR/mixed_size_write.rs:LL:CC

View file

@ -1,8 +1,8 @@
error: Undefined Behavior: Data race detected between (1) 4-byte Atomic Store on thread `<unnamed>` and (2) 2-byte (different-size) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
error: Undefined Behavior: Race condition detected between (1) 4-byte Atomic Store on thread `<unnamed>` and (2) 2-byte (different-size) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
--> $DIR/racing_mixed_size.rs:LL:CC
|
LL | std::intrinsics::atomic_load_relaxed(hi);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between (1) 4-byte Atomic Store on thread `<unnamed>` and (2) 2-byte (different-size) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Race condition detected between (1) 4-byte Atomic Store on thread `<unnamed>` and (2) 2-byte (different-size) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
|
help: and (1) occurred earlier here
--> $DIR/racing_mixed_size.rs:LL:CC

View file

@ -1,8 +1,8 @@
error: Undefined Behavior: Data race detected between (1) 4-byte Atomic Load on thread `<unnamed>` and (2) 2-byte (different-size) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
error: Undefined Behavior: Race condition detected between (1) 4-byte Atomic Load on thread `<unnamed>` and (2) 2-byte (different-size) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
--> $DIR/racing_mixed_size_read.rs:LL:CC
|
LL | (*hi).load(Relaxed);
| ^^^^^^^^^^^^^^^^^^^ Data race detected between (1) 4-byte Atomic Load on thread `<unnamed>` and (2) 2-byte (different-size) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
| ^^^^^^^^^^^^^^^^^^^ Race condition detected between (1) 4-byte Atomic Load on thread `<unnamed>` and (2) 2-byte (different-size) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
|
help: and (1) occurred earlier here
--> $DIR/racing_mixed_size_read.rs:LL:CC