Retag rename and note

src/borrow_tracker/stacked_borrows/mod.rs

@@ -755,7 +755,7 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
                         data_race.write(
                             alloc_id,
                             range,
-                            NaWriteType::UniqueMemory,
+                            NaWriteType::Retag,
                             Some(place.layout.ty),
                             machine,
                         )?;
@@ -804,7 +804,7 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
                             data_race.read(
                                 alloc_id,
                                 range,
-                                NaReadType::ImmutableMemory,
+                                NaReadType::Retag,
                                 Some(place.layout.ty),
                                 &this.machine,
                             )?;

src/borrow_tracker/tree_borrows/mod.rs

@@ -318,7 +318,7 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
                 data_race.read(
                     alloc_id,
                     range,
-                    NaReadType::ImmutableMemory,
+                    NaReadType::Retag,
                     Some(place.layout.ty),
                     &this.machine,
                 )?;

src/concurrency/data_race.rs

@@ -209,15 +209,14 @@ pub enum NaReadType {
     /// Standard unsynchronized write.
     Read,
 
-    /// Immutable memory due to shared reference invariants.
-    ImmutableMemory,
+    Retag,
 }
 
 impl NaReadType {
     fn description(self) -> &'static str {
         match self {
             NaReadType::Read => "non-atomic read",
-            NaReadType::ImmutableMemory => "shared reference invariant",
+            NaReadType::Retag => "retag read",
         }
     }
 }
@@ -234,8 +233,7 @@ pub enum NaWriteType {
     /// Standard unsynchronized write.
     Write,
 
-    /// Unique memory due to mutable reference invariants.
-    UniqueMemory,
+    Retag,
 
     /// Deallocate memory.
     /// Note that when memory is deallocated first, later non-atomic accesses
@@ -249,7 +247,7 @@ impl NaWriteType {
         match self {
             NaWriteType::Allocate => "creating a new allocation",
             NaWriteType::Write => "non-atomic write",
-            NaWriteType::UniqueMemory => "mutable reference invariant",
+            NaWriteType::Retag => "retag write",
             NaWriteType::Deallocate => "deallocation",
         }
     }
@@ -300,6 +298,14 @@ impl AccessType {
             AccessType::NaWrite(_) | AccessType::AtomicStore | AccessType::AtomicRmw => false,
         }
     }
+
+    fn is_retag(self) -> bool {
+        match self {
+            AccessType::NaRead(NaReadType::Retag) => true,
+            AccessType::NaWrite(NaWriteType::Retag) => true,
+            _ => false,
+        }
+    }
 }
 
 /// Memory Cell vector clock metadata
@@ -995,6 +1001,7 @@ impl VClockAlloc {
         Err(err_machine_stop!(TerminationInfo::DataRace {
             involves_non_atomic,
             extra,
+            retag_explain: access.is_retag() || other_access.is_retag(),
             ptr: ptr_dbg,
             op1: RacingOp {
                 action: other_access.description(None, other_size),

src/concurrency/vector_clock.rs

@@ -220,16 +220,14 @@ impl PartialOrd for VClock {
         for (l, r) in iter {
             match order {
                 Ordering::Equal => order = l.cmp(r),
-                Ordering::Less => {
+                Ordering::Less =>
                     if l > r {
                         return None;
-                    }
-                }
-                Ordering::Greater => {
+                    },
+                Ordering::Greater =>
                     if l < r {
                         return None;
-                    }
-                }
+                    },
             }
         }
 
@@ -244,16 +242,18 @@ impl PartialOrd for VClock {
             Ordering::Equal => Some(order),
             // Right has at least 1 element > than the implicit 0,
             // so the only valid values are Ordering::Less or None.
-            Ordering::Less => match order {
-                Ordering::Less | Ordering::Equal => Some(Ordering::Less),
-                Ordering::Greater => None,
-            },
+            Ordering::Less =>
+                match order {
+                    Ordering::Less | Ordering::Equal => Some(Ordering::Less),
+                    Ordering::Greater => None,
+                },
             // Left has at least 1 element > than the implicit 0,
             // so the only valid values are Ordering::Greater or None.
-            Ordering::Greater => match order {
-                Ordering::Greater | Ordering::Equal => Some(Ordering::Greater),
-                Ordering::Less => None,
-            },
+            Ordering::Greater =>
+                match order {
+                    Ordering::Greater | Ordering::Equal => Some(Ordering::Greater),
+                    Ordering::Less => None,
+                },
         }
     }
 

src/diagnostics.rs

@@ -46,6 +46,7 @@ pub enum TerminationInfo {
         op1: RacingOp,
         op2: RacingOp,
         extra: Option<&'static str>,
+        retag_explain: bool,
     },
 }
 
@@ -211,10 +212,12 @@ pub fn report_error<'tcx, 'mir>(
         let title = match info {
             Exit { code, leak_check } => return Some((*code, *leak_check)),
             Abort(_) => Some("abnormal termination"),
-            UnsupportedInIsolation(_) | Int2PtrWithStrictProvenance =>
-                Some("unsupported operation"),
-            StackedBorrowsUb { .. } | TreeBorrowsUb { .. } | DataRace { .. } =>
-                Some("Undefined Behavior"),
+            UnsupportedInIsolation(_) | Int2PtrWithStrictProvenance => {
+                Some("unsupported operation")
+            }
+            StackedBorrowsUb { .. } | TreeBorrowsUb { .. } | DataRace { .. } => {
+                Some("Undefined Behavior")
+            }
             Deadlock => Some("deadlock"),
             MultipleSymbolDefinitions { .. } | SymbolShimClashing { .. } => None,
         };
@@ -263,12 +266,14 @@ 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, extra, .. } => {
+            DataRace { op1, extra, retag_explain, .. } => {
                 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!("see https://doc.rust-lang.org/nightly/std/sync/atomic/index.html#memory-model-for-atomic-accesses for more information about the Rust memory model")));
-                }
+                }  if *retag_explain {
+                    helps.push((None, "retags permit optimizations that insert speculative (or loop-hoisted) reads/writes. Therefore from the perspective of data races, a retag has the same implications as a read/write.".to_owned()));
+                 }
                 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
@@ -531,8 +536,9 @@ impl<'mir, 'tcx> MiriMachine<'mir, 'tcx> {
         let (stacktrace, _was_pruned) = prune_stacktrace(stacktrace, self);
 
         let (title, diag_level) = match &e {
-            RejectedIsolatedOp(_) =>
-                ("operation rejected by isolation".to_string(), DiagLevel::Warning),
+            RejectedIsolatedOp(_) => {
+                ("operation rejected by isolation".to_string(), DiagLevel::Warning)
+            }
             Int2Ptr { .. } => ("integer-to-pointer cast".to_string(), DiagLevel::Warning),
             CreatedPointerTag(..)
             | PoppedPointerTag(..)