give some more help for the unusual data races

RalfJung · RalfJung · commit 278965a0c496 · 2023-10-27T12:46:59.000+02:00
diff --git a/src/tools/miri/src/concurrency/data_race.rs b/src/tools/miri/src/concurrency/data_race.rs
@@ -248,6 +248,13 @@ impl AccessType {
             AccessType::NaRead | AccessType::NaWrite(_) => false,
         }
     }
+
+    fn is_read(self) -> bool {
+        match self {
+            AccessType::AtomicLoad | AccessType::NaRead => true,
+            AccessType::NaWrite(_) | AccessType::AtomicStore | AccessType::AtomicRmw => false,
+        }
+    }
 }
 
 /// Memory Cell vector clock metadata
@@ -872,9 +879,8 @@ impl VClockAlloc {
     ) -> InterpResult<'tcx> {
         let (current_index, current_clocks) = global.current_thread_state(thread_mgr);
         let mut other_size = None; // if `Some`, this was a size-mismatch race
-        let mut involves_non_atomic = true;
         let write_clock;
-        let (other_action, other_thread, other_clock) =
+        let (other_access, other_thread, other_clock) =
             // First check the atomic-nonatomic cases. If it looks like multiple
             // cases apply, this one should take precedence, else it might look like
             // we are reporting races between two non-atomic reads.
@@ -898,7 +904,6 @@ impl VClockAlloc {
             } else if access.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;
                 other_size = Some(atomic.size);
                 if let Some(idx) = Self::find_gt_index(&atomic.write_vector, &current_clocks.clock)
                     {
@@ -919,27 +924,36 @@ impl VClockAlloc {
         // Load elaborated thread information about the racing thread actions.
         let current_thread_info = global.print_thread_metadata(thread_mgr, current_index);
         let other_thread_info = global.print_thread_metadata(thread_mgr, other_thread);
+        let involves_non_atomic = !access.is_atomic() || !other_access.is_atomic();
 
         // Throw the data-race detection.
+        let extra = if other_size.is_some() {
+            assert!(!involves_non_atomic);
+            Some("overlapping unsynchronized atomic accesses must use the same access size")
+        } else if access.is_read() && other_access.is_read() {
+            assert!(involves_non_atomic);
+            Some(
+                "overlapping atomic and non-atomic accesses must be synchronized, even if both are read-only",
+            )
+        } else {
+            None
+        };
         Err(err_machine_stop!(TerminationInfo::DataRace {
             involves_non_atomic,
+            extra,
             ptr: ptr_dbg,
             op1: RacingOp {
                 action: if let Some(other_size) = other_size {
-                    format!("{}-byte {}", other_size.bytes(), other_action.description())
+                    format!("{}-byte {}", other_size.bytes(), other_access.description())
                 } else {
-                    other_action.description().to_owned()
+                    other_access.description().to_owned()
                 },
                 thread_info: other_thread_info,
                 span: other_clock.as_slice()[other_thread.index()].span_data(),
             },
             op2: RacingOp {
                 action: if other_size.is_some() {
-                    format!(
-                        "{}-byte (different-size) {}",
-                        access_size.bytes(),
-                        access.description()
-                    )
+                    format!("{}-byte {}", access_size.bytes(), access.description())
                 } else {
                     access.description().to_owned()
                 },
diff --git a/src/tools/miri/src/diagnostics.rs b/src/tools/miri/src/diagnostics.rs
@@ -47,6 +47,7 @@ pub enum TerminationInfo {
         ptr: Pointer,
         op1: RacingOp,
         op2: RacingOp,
+        extra: Option<&'static str>,
     },
 }
 
@@ -75,7 +76,7 @@ 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 { involves_non_atomic, ptr, op1, op2 } =>
+            DataRace { involves_non_atomic, ptr, op1, op2, .. } =>
                 write!(
                     f,
                     "{} detected between (1) {} on {} and (2) {} on {} at {ptr:?}. (2) just happened here",
@@ -266,12 +267,16 @@ pub fn report_error<'tcx, 'mir>(
                 vec![(Some(*span), format!("the `{link_name}` symbol is defined here"))],
             Int2PtrWithStrictProvenance =>
                 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"))],
-            DataRace { op1, .. } =>
-                vec![
-                    (Some(op1.span), format!("and (1) occurred earlier here")),
-                    (None, format!("this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior")),
-                    (None, format!("see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information")),
-                ],
+            DataRace { op1, extra, .. } => {
+                let mut helps = vec![(Some(op1.span), format!("and (1) occurred earlier here"))];
+                if let Some(extra) = extra {
+                    helps.push((None, format!("{extra}")))
+                }
+                helps.push((None, format!("this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior")));
+                helps.push((None, format!("see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information")));
+                helps
+            }
+                ,
             _ => vec![],
         };
         (title, helps)
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
@@ -19,7 +19,7 @@ fn main() {
         });
         s.spawn(|| {
             a8[0].load(Ordering::SeqCst);
-            //~^ ERROR: Race condition 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 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
@@ -1,14 +1,15 @@
-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
+error: Undefined Behavior: Race condition detected between (1) 2-byte atomic load on thread `<unnamed>` and (2) 1-byte atomic load on thread `<unnamed>` at ALLOC. (2) just happened here
   --> $DIR/mixed_size_read.rs:LL:CC
    |
 LL |             a8[0].load(Ordering::SeqCst);
-   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 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
+   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Race condition detected between (1) 2-byte atomic load on thread `<unnamed>` and (2) 1-byte atomic load on thread `<unnamed>` at ALLOC. (2) just happened here
    |
 help: and (1) occurred earlier here
   --> $DIR/mixed_size_read.rs:LL:CC
    |
 LL |             a16.load(Ordering::SeqCst);
    |             ^^^^^^^^^^^^^^^^^^^^^^^^^^
+   = help: overlapping unsynchronized atomic accesses must use the same access size
    = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
    = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
    = note: BACKTRACE (of the first span):
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
@@ -19,7 +19,7 @@ fn main() {
         });
         s.spawn(|| {
             a8[0].store(1, Ordering::SeqCst);
-            //~^ ERROR: Race condition 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 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
@@ -1,14 +1,15 @@
-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
+error: Undefined Behavior: Race condition detected between (1) 2-byte atomic store on thread `<unnamed>` and (2) 1-byte 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);
-   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 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
+   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Race condition detected between (1) 2-byte atomic store on thread `<unnamed>` and (2) 1-byte atomic store on thread `<unnamed>` at ALLOC. (2) just happened here
    |
 help: and (1) occurred earlier here
   --> $DIR/mixed_size_write.rs:LL:CC
    |
 LL |             a16.store(1, Ordering::SeqCst);
    |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   = help: overlapping unsynchronized atomic accesses must use the same access size
    = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
    = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
    = note: BACKTRACE (of the first span):
diff --git a/src/tools/miri/tests/fail/data_race/read_read_race1.stderr b/src/tools/miri/tests/fail/data_race/read_read_race1.stderr
@@ -9,6 +9,7 @@ help: and (1) occurred earlier here
    |
 LL |             unsafe { ptr.read() };
    |                      ^^^^^^^^^^
+   = help: overlapping atomic and non-atomic accesses must be synchronized, even if both are read-only
    = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
    = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
    = note: BACKTRACE (of the first span):
diff --git a/src/tools/miri/tests/fail/data_race/read_read_race2.stderr b/src/tools/miri/tests/fail/data_race/read_read_race2.stderr
@@ -9,6 +9,7 @@ help: and (1) occurred earlier here
    |
 LL |             a.load(Ordering::SeqCst);
    |             ^^^^^^^^^^^^^^^^^^^^^^^^
+   = help: overlapping atomic and non-atomic accesses must be synchronized, even if both are read-only
    = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
    = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
    = note: BACKTRACE (of the first span):
diff --git a/src/tools/miri/tests/fail/weak_memory/racing_mixed_size.rs b/src/tools/miri/tests/fail/weak_memory/racing_mixed_size.rs
@@ -31,7 +31,7 @@ pub fn main() {
         let x_split = split_u32_ptr(x_ptr);
         unsafe {
             let hi = ptr::addr_of!((*x_split)[0]);
-            std::intrinsics::atomic_load_relaxed(hi); //~ ERROR: different-size
+            std::intrinsics::atomic_load_relaxed(hi); //~ ERROR: (1) 4-byte atomic store on thread `<unnamed>` and (2) 2-byte atomic load
         }
     });
 
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
@@ -1,14 +1,15 @@
-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
+error: Undefined Behavior: Race condition detected between (1) 4-byte atomic store on thread `<unnamed>` and (2) 2-byte 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);
-   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 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
+   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Race condition detected between (1) 4-byte atomic store on thread `<unnamed>` and (2) 2-byte atomic load on thread `<unnamed>` at ALLOC. (2) just happened here
    |
 help: and (1) occurred earlier here
   --> $DIR/racing_mixed_size.rs:LL:CC
    |
 LL |         x.store(1, Relaxed);
    |         ^^^^^^^^^^^^^^^^^^^
+   = help: overlapping unsynchronized atomic accesses must use the same access size
    = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
    = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
    = note: BACKTRACE (of the first span):
diff --git a/src/tools/miri/tests/fail/weak_memory/racing_mixed_size_read.rs b/src/tools/miri/tests/fail/weak_memory/racing_mixed_size_read.rs
@@ -29,7 +29,7 @@ pub fn main() {
         let x_split = split_u32_ptr(x_ptr);
         unsafe {
             let hi = x_split as *const u16 as *const AtomicU16;
-            (*hi).load(Relaxed); //~ ERROR: different-size
+            (*hi).load(Relaxed); //~ ERROR: (1) 4-byte atomic load on thread `<unnamed>` and (2) 2-byte atomic load
         }
     });
 
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
@@ -1,14 +1,15 @@
-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
+error: Undefined Behavior: Race condition detected between (1) 4-byte atomic load on thread `<unnamed>` and (2) 2-byte atomic load on thread `<unnamed>` at ALLOC. (2) just happened here
   --> $DIR/racing_mixed_size_read.rs:LL:CC
    |
 LL |             (*hi).load(Relaxed);
-   |             ^^^^^^^^^^^^^^^^^^^ 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
+   |             ^^^^^^^^^^^^^^^^^^^ Race condition detected between (1) 4-byte atomic load on thread `<unnamed>` and (2) 2-byte 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
    |
 LL |         x.load(Relaxed);
    |         ^^^^^^^^^^^^^^^
+   = help: overlapping unsynchronized atomic accesses must use the same access size
    = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
    = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
    = note: BACKTRACE (of the first span):

Original file line number	Diff line number	Diff line change
`@@ -19,7 +19,7 @@ fn main() {`
`19`	`19`	`});`
`20`	`20`	`s.spawn(\|\| {`
`21`	`21`	`a8[0].load(Ordering::SeqCst);`
`22`		- //~^ ERROR: Race condition detected between (1) 2-byte atomic load on thread `<unnamed>` and (2) 1-byte (different-size) atomic load on thread `<unnamed>`
	`22`	+ //~^ ERROR: Race condition detected between (1) 2-byte atomic load on thread `<unnamed>` and (2) 1-byte atomic load on thread `<unnamed>`
`23`	`23`	`});`
`24`	`24`	`});`
`25`	`25`	`}`
Original file line number	Diff line number	Diff line change
`@@ -1,14 +1,15 @@`
`1`		-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
	`1`	+error: Undefined Behavior: Race condition detected between (1) 2-byte atomic load on thread `<unnamed>` and (2) 1-byte atomic load on thread `<unnamed>` at ALLOC. (2) just happened here
`2`	`2`	`--> $DIR/mixed_size_read.rs:LL:CC`
`3`	`3`	`\|`
`4`	`4`	`LL \| a8[0].load(Ordering::SeqCst);`
`5`		- \| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 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
	`5`	+ \| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Race condition detected between (1) 2-byte atomic load on thread `<unnamed>` and (2) 1-byte atomic load on thread `<unnamed>` at ALLOC. (2) just happened here
`6`	`6`	`\|`
`7`	`7`	`help: and (1) occurred earlier here`
`8`	`8`	`--> $DIR/mixed_size_read.rs:LL:CC`
`9`	`9`	`\|`
`10`	`10`	`LL \| a16.load(Ordering::SeqCst);`
`11`	`11`	`\| ^^^^^^^^^^^^^^^^^^^^^^^^^^`
	`12`	`+ = help: overlapping unsynchronized atomic accesses must use the same access size`
`12`	`13`	`= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior`
`13`	`14`	`= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information`
`14`	`15`	`= note: BACKTRACE (of the first span):`
Original file line number	Diff line number	Diff line change
`@@ -9,6 +9,7 @@ help: and (1) occurred earlier here`
`9`	`9`	`\|`
`10`	`10`	`LL \| unsafe { ptr.read() };`
`11`	`11`	`\| ^^^^^^^^^^`
	`12`	`+ = help: overlapping atomic and non-atomic accesses must be synchronized, even if both are read-only`
`12`	`13`	`= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior`
`13`	`14`	`= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information`
`14`	`15`	`= note: BACKTRACE (of the first span):`
Original file line number	Diff line number	Diff line change
`@@ -31,7 +31,7 @@ pub fn main() {`
`31`	`31`	`let x_split = split_u32_ptr(x_ptr);`
`32`	`32`	`unsafe {`
`33`	`33`	`let hi = ptr::addr_of!((*x_split)[0]);`
`34`		`- std::intrinsics::atomic_load_relaxed(hi); //~ ERROR: different-size`
	`34`	+ std::intrinsics::atomic_load_relaxed(hi); //~ ERROR: (1) 4-byte atomic store on thread `<unnamed>` and (2) 2-byte atomic load
`35`	`35`	`}`
`36`	`36`	`});`
`37`	`37`
Original file line number	Diff line number	Diff line change
`@@ -29,7 +29,7 @@ pub fn main() {`
`29`	`29`	`let x_split = split_u32_ptr(x_ptr);`
`30`	`30`	`unsafe {`
`31`	`31`	`let hi = x_split as const u16 as const AtomicU16;`
`32`		`- (*hi).load(Relaxed); //~ ERROR: different-size`
	`32`	+ (*hi).load(Relaxed); //~ ERROR: (1) 4-byte atomic load on thread `<unnamed>` and (2) 2-byte atomic load
`33`	`33`	`}`
`34`	`34`	`});`
`35`	`35`