Add a (1) and (2) to the data race errors

Author: saethlin

src/tools/miri/src/diagnostics.rs

@@ -69,8 +69,8 @@ impl fmt::Display for TerminationInfo {
             DataRace { ptr, op1, op2 } =>
                 write!(
                     f,
-                    "Data race detected between {} on {} and {} on {} at {:?}. The {} is here",
-                    op1.action, op1.thread_info, op2.action, op2.thread_info, ptr, op1.action
+                    "Data race detected between (1) {} on {} and (2) {} on {} at {ptr:?}. (1) just happened here",
+                    op1.action, op1.thread_info, op2.action, op2.thread_info
                 ),
         }
     }
@@ -224,7 +224,7 @@ pub fn report_error<'tcx, 'mir>(
                 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 { op2, .. } =>
                 vec![
-                    (Some(op2.span), format!("and the {} on {} is here", op2.action, op2.thread_info)),
+                    (Some(op2.span), format!("and (2) 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")),
                 ],

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

@@ -37,7 +37,7 @@ pub fn main() {
             let pointer = &*ptr.0;
 
             // Note: could also error due to reading uninitialized memory, but the data-race detector triggers first.
-            *pointer.load(Ordering::Relaxed) //~ ERROR: Data race detected between Read on thread `<unnamed>` and Allocate on thread `<unnamed>`
+            *pointer.load(Ordering::Relaxed) //~ ERROR: Data race detected between (1) Read on thread `<unnamed>` and (2) Allocate on thread `<unnamed>`
         });
 
         j1.join().unwrap();

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

@@ -1,10 +1,10 @@
-error: Undefined Behavior: Data race detected between Read on thread `<unnamed>` and Allocate on thread `<unnamed>` at ALLOC. The Read is here
+error: Undefined Behavior: Data race detected between (1) Read on thread `<unnamed>` and (2) Allocate on thread `<unnamed>` at ALLOC. (1) just happened here
   --> $DIR/alloc_read_race.rs:LL:CC
    |
 LL |             *pointer.load(Ordering::Relaxed)
-   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between Read on thread `<unnamed>` and Allocate on thread `<unnamed>` at ALLOC. The Read is here
+   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between (1) Read on thread `<unnamed>` and (2) Allocate on thread `<unnamed>` at ALLOC. (1) just happened here
    |
-help: and the Allocate on thread `<unnamed>` is here
+help: and (2) occurred earlier here
   --> $DIR/alloc_read_race.rs:LL:CC
    |
 LL |             pointer.store(Box::into_raw(Box::new_uninit()), Ordering::Relaxed);

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

@@ -35,7 +35,7 @@ pub fn main() {
 
         let j2 = spawn(move || {
             let pointer = &*ptr.0;
-            *pointer.load(Ordering::Relaxed) = 2; //~ ERROR: Data race detected between Write on thread `<unnamed>` and Allocate on thread `<unnamed>`
+            *pointer.load(Ordering::Relaxed) = 2; //~ ERROR: Data race detected between (1) Write on thread `<unnamed>` and (2) Allocate on thread `<unnamed>`
         });
 
         j1.join().unwrap();

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

@@ -1,10 +1,10 @@
-error: Undefined Behavior: Data race detected between Write on thread `<unnamed>` and Allocate on thread `<unnamed>` at ALLOC. The Write is here
+error: Undefined Behavior: Data race detected between (1) Write on thread `<unnamed>` and (2) Allocate on thread `<unnamed>` at ALLOC. (1) just happened here
   --> $DIR/alloc_write_race.rs:LL:CC
    |
 LL |             *pointer.load(Ordering::Relaxed) = 2;
-   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between Write on thread `<unnamed>` and Allocate on thread `<unnamed>` at ALLOC. The Write is here
+   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between (1) Write on thread `<unnamed>` and (2) Allocate on thread `<unnamed>` at ALLOC. (1) just happened here
    |
-help: and the Allocate on thread `<unnamed>` is here
+help: and (2) occurred earlier here
   --> $DIR/alloc_write_race.rs:LL:CC
    |
 LL |                 .store(Box::into_raw(Box::<usize>::new_uninit()) as *mut usize, Ordering::Relaxed);

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

@@ -20,7 +20,7 @@ pub fn main() {
         });
 
         let j2 = spawn(move || {
-            (&*c.0).load(Ordering::SeqCst) //~ ERROR: Data race detected between Atomic Load on thread `<unnamed>` and Write on thread `<unnamed>`
+            (&*c.0).load(Ordering::SeqCst) //~ ERROR: Data race detected between (1) Atomic Load on thread `<unnamed>` and (2) Write on thread `<unnamed>`
         });
 
         j1.join().unwrap();

src/tools/miri/tests/fail/data_race/atomic_read_na_write_race1.stderr

@@ -1,10 +1,10 @@
-error: Undefined Behavior: Data race detected between Atomic Load on thread `<unnamed>` and Write on thread `<unnamed>` at ALLOC. The Atomic Load is here
+error: Undefined Behavior: Data race detected between (1) Atomic Load on thread `<unnamed>` and (2) Write on thread `<unnamed>` at ALLOC. (1) just happened here
   --> $DIR/atomic_read_na_write_race1.rs:LL:CC
    |
 LL |             (&*c.0).load(Ordering::SeqCst)
-   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between Atomic Load on thread `<unnamed>` and Write on thread `<unnamed>` at ALLOC. The Atomic Load is here
+   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between (1) Atomic Load on thread `<unnamed>` and (2) Write on thread `<unnamed>` at ALLOC. (1) just happened here
    |
-help: and the Write on thread `<unnamed>` is here
+help: and (2) occurred earlier here
   --> $DIR/atomic_read_na_write_race1.rs:LL:CC
    |
 LL |             *(c.0 as *mut usize) = 32;

src/tools/miri/tests/fail/data_race/atomic_read_na_write_race2.rs

@@ -23,7 +23,7 @@ pub fn main() {
 
         let j2 = spawn(move || {
             let atomic_ref = &mut *c.0;
-            *atomic_ref.get_mut() = 32; //~ ERROR: Data race detected between Write on thread `<unnamed>` and Atomic Load on thread `<unnamed>`
+            *atomic_ref.get_mut() = 32; //~ ERROR: Data race detected between (1) Write on thread `<unnamed>` and (2) Atomic Load on thread `<unnamed>`
         });
 
         j1.join().unwrap();

src/tools/miri/tests/fail/data_race/atomic_read_na_write_race2.stderr

@@ -1,10 +1,10 @@
-error: Undefined Behavior: Data race detected between Write on thread `<unnamed>` and Atomic Load on thread `<unnamed>` at ALLOC. The Write is here
+error: Undefined Behavior: Data race detected between (1) Write on thread `<unnamed>` and (2) Atomic Load on thread `<unnamed>` at ALLOC. (1) just happened here
   --> $DIR/atomic_read_na_write_race2.rs:LL:CC
    |
 LL |             *atomic_ref.get_mut() = 32;
-   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between Write on thread `<unnamed>` and Atomic Load on thread `<unnamed>` at ALLOC. The Write is here
+   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between (1) Write on thread `<unnamed>` and (2) Atomic Load on thread `<unnamed>` at ALLOC. (1) just happened here
    |
-help: and the Atomic Load on thread `<unnamed>` is here
+help: and (2) occurred earlier here
   --> $DIR/atomic_read_na_write_race2.rs:LL:CC
    |
 LL |             atomic_ref.load(Ordering::SeqCst)

src/tools/miri/tests/fail/data_race/atomic_write_na_read_race1.rs

@@ -23,7 +23,7 @@ pub fn main() {
 
         let j2 = spawn(move || {
             let atomic_ref = &mut *c.0;
-            *atomic_ref.get_mut() //~ ERROR: Data race detected between Read on thread `<unnamed>` and Atomic Store on thread `<unnamed>`
+            *atomic_ref.get_mut() //~ ERROR: Data race detected between (1) Read on thread `<unnamed>` and (2) Atomic Store on thread `<unnamed>`
         });
 
         j1.join().unwrap();