diff options
| author | Ralf Jung <post@ralfj.de> | 2023-10-23 12:38:33 +0200 |
|---|---|---|
| committer | Ralf Jung <post@ralfj.de> | 2023-10-23 12:38:39 +0200 |
| commit | e94c18ea872ce2ffefd6995bc435948e494612cc (patch) | |
| tree | 704ba17fdbdfef64c9a8fed38281e4b31a809f3a | |
| parent | 369c6d180c2c2c5ba15f1fb66994d1d6d409d56b (diff) | |
| download | rust-e94c18ea872ce2ffefd6995bc435948e494612cc.tar.gz rust-e94c18ea872ce2ffefd6995bc435948e494612cc.zip | |
don't talk about 'Data race' when both accesses are atomic
8 files changed, 22 insertions, 14 deletions
diff --git a/src/tools/miri/src/concurrency/data_race.rs b/src/tools/miri/src/concurrency/data_race.rs index 303e179f297..d9bc043225d 100644 --- a/src/tools/miri/src/concurrency/data_race.rs +++ b/src/tools/miri/src/concurrency/data_race.rs @@ -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, ¤t_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(), diff --git a/src/tools/miri/src/diagnostics.rs b/src/tools/miri/src/diagnostics.rs index cb095f94f35..9b8f263b7ce 100644 --- a/src/tools/miri/src/diagnostics.rs +++ b/src/tools/miri/src/diagnostics.rs @@ -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 ), } } diff --git a/src/tools/miri/tests/fail/data_race/mixed_size_read.rs b/src/tools/miri/tests/fail/data_race/mixed_size_read.rs index 9a087c17c6d..d530ed2f5a4 100644 --- a/src/tools/miri/tests/fail/data_race/mixed_size_read.rs +++ b/src/tools/miri/tests/fail/data_race/mixed_size_read.rs @@ -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>` }); }); } diff --git a/src/tools/miri/tests/fail/data_race/mixed_size_read.stderr b/src/tools/miri/tests/fail/data_race/mixed_size_read.stderr index 23b136e6c5f..06944a11db8 100644 --- a/src/tools/miri/tests/fail/data_race/mixed_size_read.stderr +++ b/src/tools/miri/tests/fail/data_race/mixed_size_read.stderr @@ -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 diff --git a/src/tools/miri/tests/fail/data_race/mixed_size_write.rs b/src/tools/miri/tests/fail/data_race/mixed_size_write.rs index 47d54e3acf3..df3551612c3 100644 --- a/src/tools/miri/tests/fail/data_race/mixed_size_write.rs +++ b/src/tools/miri/tests/fail/data_race/mixed_size_write.rs @@ -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>` }); }); } diff --git a/src/tools/miri/tests/fail/data_race/mixed_size_write.stderr b/src/tools/miri/tests/fail/data_race/mixed_size_write.stderr index 019a65d9c86..4bb949175bf 100644 --- a/src/tools/miri/tests/fail/data_race/mixed_size_write.stderr +++ b/src/tools/miri/tests/fail/data_race/mixed_size_write.stderr @@ -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 diff --git a/src/tools/miri/tests/fail/weak_memory/racing_mixed_size.stderr b/src/tools/miri/tests/fail/weak_memory/racing_mixed_size.stderr index 6823042d281..055585ab96f 100644 --- a/src/tools/miri/tests/fail/weak_memory/racing_mixed_size.stderr +++ b/src/tools/miri/tests/fail/weak_memory/racing_mixed_size.stderr @@ -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 diff --git a/src/tools/miri/tests/fail/weak_memory/racing_mixed_size_read.stderr b/src/tools/miri/tests/fail/weak_memory/racing_mixed_size_read.stderr index edddf4bc26c..2eefa0a87b4 100644 --- a/src/tools/miri/tests/fail/weak_memory/racing_mixed_size_read.stderr +++ b/src/tools/miri/tests/fail/weak_memory/racing_mixed_size_read.stderr @@ -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 |
