Auto merge of #3385 - Zoxc:read-types, r=RalfJung

Report retags as distinct from real memory accesses for data races This changes the error reporting for data races such that reference invariants are no longer reported as real read and writes. Before: ``` Data race detected between (1) non-atomic write on thread `unnamed-6` and (2) non-atomic read on thread `unnamed-5` at alloc1034971+0x10c. (2) just happened here ``` After: ``` Data race detected between (1) non-atomic write on thread `unnamed-8` and (2) shared reference invariant on thread `unnamed-6` at alloc1018329+0x190. (2) just happened here ``` Non-atomic read accesses from the *other* thread don't have this information tracked so those are called `some potential non-atomic read access` here.
2024-11-27 01:04:03 +00:00 · 2024-03-23 15:37:02 +00:00 · 2024-03-23 15:37:02 +00:00 · 59b29455c1
commit 59b29455c1
parent e19cc5e922 2d610f7473
14 changed files with 202 additions and 89 deletions
--- a/src/tools/miri/src/borrow_tracker/stacked_borrows/mod.rs
+++ b/src/tools/miri/src/borrow_tracker/stacked_borrows/mod.rs
@ -18,6 +18,7 @@ use crate::borrow_tracker::{
    stacked_borrows::diagnostics::{AllocHistory, DiagnosticCx, DiagnosticCxBuilder},
    GlobalStateInner, ProtectorKind,
 };
+use crate::concurrency::data_race::{NaReadType, NaWriteType};
 use crate::*;

 use diagnostics::{RetagCause, RetagInfo};
@ -751,7 +752,13 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
                    assert_eq!(access, AccessKind::Write);
                    // Make sure the data race model also knows about this.
                    if let Some(data_race) = alloc_extra.data_race.as_mut() {
-                        data_race.write(alloc_id, range, machine)?;
+                        data_race.write(
+                            alloc_id,
+                            range,
+                            NaWriteType::Retag,
+                            Some(place.layout.ty),
+                            machine,
+                        )?;
                    }
                }
            }
@ -794,7 +801,13 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
                        assert_eq!(access, AccessKind::Read);
                        // Make sure the data race model also knows about this.
                        if let Some(data_race) = alloc_extra.data_race.as_ref() {
-                            data_race.read(alloc_id, range, &this.machine)?;
+                            data_race.read(
+                                alloc_id,
+                                range,
+                                NaReadType::Retag,
+                                Some(place.layout.ty),
+                                &this.machine,
+                            )?;
                        }
                    }
                    Ok(())
--- a/src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs
+++ b/src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs
@ -9,8 +9,11 @@ use rustc_middle::{
 use rustc_span::def_id::DefId;
 use rustc_target::abi::{Abi, Size};

-use crate::borrow_tracker::{GlobalState, GlobalStateInner, ProtectorKind};
 use crate::*;
+use crate::{
+    borrow_tracker::{GlobalState, GlobalStateInner, ProtectorKind},
+    concurrency::data_race::NaReadType,
+};

 pub mod diagnostics;
 mod perms;
@ -312,7 +315,13 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
        // Also inform the data race model (but only if any bytes are actually affected).
        if range.size.bytes() > 0 {
            if let Some(data_race) = alloc_extra.data_race.as_ref() {
-                data_race.read(alloc_id, range, &this.machine)?;
+                data_race.read(
+                    alloc_id,
+                    range,
+                    NaReadType::Retag,
+                    Some(place.layout.ty),
+                    &this.machine,
+                )?;
            }
        }

--- a/src/tools/miri/src/concurrency/data_race.rs
+++ b/src/tools/miri/src/concurrency/data_race.rs
@ -49,7 +49,7 @@ use std::{
 use rustc_ast::Mutability;
 use rustc_data_structures::fx::{FxHashMap, FxHashSet};
 use rustc_index::{Idx, IndexVec};
-use rustc_middle::mir;
+use rustc_middle::{mir, ty::Ty};
 use rustc_span::Span;
 use rustc_target::abi::{Align, HasDataLayout, Size};

@ -200,18 +200,38 @@ enum AtomicAccessType {
    Rmw,
 }

-/// Type of write operation: allocating memory
-/// non-atomic writes and deallocating memory
-/// are all treated as writes for the purpose
-/// of the data-race detector.
+/// Type of a non-atomic read operation.
 #[derive(Copy, Clone, PartialEq, Eq, Debug)]
-enum NaWriteType {
+pub enum NaReadType {
+    /// Standard unsynchronized write.
+    Read,
+
+    // An implicit read generated by a retag.
+    Retag,
+}
+
+impl NaReadType {
+    fn description(self) -> &'static str {
+        match self {
+            NaReadType::Read => "non-atomic read",
+            NaReadType::Retag => "retag read",
+        }
+    }
+}
+
+/// Type of a non-atomic write operation: allocating memory, non-atomic writes, and
+/// deallocating memory are all treated as writes for the purpose of the data-race detector.
+#[derive(Copy, Clone, PartialEq, Eq, Debug)]
+pub enum NaWriteType {
    /// Allocate memory.
    Allocate,

    /// Standard unsynchronized write.
    Write,

+    // An implicit write generated by a retag.
+    Retag,
+
    /// Deallocate memory.
    /// Note that when memory is deallocated first, later non-atomic accesses
    /// will be reported as use-after-free, not as data races.
@ -224,6 +244,7 @@ impl NaWriteType {
        match self {
            NaWriteType::Allocate => "creating a new allocation",
            NaWriteType::Write => "non-atomic write",
+            NaWriteType::Retag => "retag write",
            NaWriteType::Deallocate => "deallocation",
        }
    }
@ -231,7 +252,7 @@ impl NaWriteType {

 #[derive(Copy, Clone, PartialEq, Eq, Debug)]
 enum AccessType {
-    NaRead,
+    NaRead(NaReadType),
    NaWrite(NaWriteType),
    AtomicLoad,
    AtomicStore,
@ -239,29 +260,48 @@ enum AccessType {
 }

 impl AccessType {
-    fn description(self) -> &'static str {
-        match self {
-            AccessType::NaRead => "non-atomic read",
+    fn description(self, ty: Option<Ty<'_>>, size: Option<Size>) -> String {
+        let mut msg = String::new();
+
+        if let Some(size) = size {
+            msg.push_str(&format!("{}-byte {}", size.bytes(), msg))
+        }
+
+        msg.push_str(match self {
+            AccessType::NaRead(w) => w.description(),
            AccessType::NaWrite(w) => w.description(),
            AccessType::AtomicLoad => "atomic load",
            AccessType::AtomicStore => "atomic store",
            AccessType::AtomicRmw => "atomic read-modify-write",
+        });
+
+        if let Some(ty) = ty {
+            msg.push_str(&format!(" of type `{}`", ty));
        }
+
+        msg
    }

    fn is_atomic(self) -> bool {
        match self {
            AccessType::AtomicLoad | AccessType::AtomicStore | AccessType::AtomicRmw => true,
-            AccessType::NaRead | AccessType::NaWrite(_) => false,
+            AccessType::NaRead(_) | AccessType::NaWrite(_) => false,
        }
    }

    fn is_read(self) -> bool {
        match self {
-            AccessType::AtomicLoad | AccessType::NaRead => true,
+            AccessType::AtomicLoad | AccessType::NaRead(_) => true,
            AccessType::NaWrite(_) | AccessType::AtomicStore | AccessType::AtomicRmw => false,
        }
    }
+
+    fn is_retag(self) -> bool {
+        matches!(
+            self,
+            AccessType::NaRead(NaReadType::Retag) | AccessType::NaWrite(NaWriteType::Retag)
+        )
+    }
 }

 /// Memory Cell vector clock metadata
@ -502,12 +542,14 @@ impl MemoryCellClocks {
        &mut self,
        thread_clocks: &mut ThreadClockSet,
        index: VectorIdx,
+        read_type: NaReadType,
        current_span: Span,
    ) -> Result<(), DataRace> {
        trace!("Unsynchronized read with vectors: {:#?} :: {:#?}", self, thread_clocks);
        if !current_span.is_dummy() {
            thread_clocks.clock[index].span = current_span;
        }
+        thread_clocks.clock[index].set_read_type(read_type);
        if self.write_was_before(&thread_clocks.clock) {
            let race_free = if let Some(atomic) = self.atomic() {
                // We must be ordered-after all atomic accesses, reads and writes.
@ -875,7 +917,8 @@ impl VClockAlloc {
    /// This finds the two racing threads and the type
    /// of data-race that occurred. This will also
    /// return info about the memory location the data-race
-    /// occurred in.
+    /// occurred in. The `ty` parameter is used for diagnostics, letting
+    /// the user know which type was involved in the access.
    #[cold]
    #[inline(never)]
    fn report_data_race<'tcx>(
@ -885,6 +928,7 @@ impl VClockAlloc {
        access: AccessType,
        access_size: Size,
        ptr_dbg: Pointer<AllocId>,
+        ty: Option<Ty<'_>>,
    ) -> 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
@ -908,7 +952,7 @@ impl VClockAlloc {
                write_clock = mem_clocks.write();
                (AccessType::NaWrite(mem_clocks.write_type), mem_clocks.write.0, &write_clock)
            } else if let Some(idx) = Self::find_gt_index(&mem_clocks.read, &current_clocks.clock) {
-                (AccessType::NaRead, idx, &mem_clocks.read)
+                (AccessType::NaRead(mem_clocks.read[idx].read_type()), idx, &mem_clocks.read)
            // Finally, mixed-size races.
            } 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
@ -950,37 +994,33 @@ 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: if let Some(other_size) = other_size {
-                    format!("{}-byte {}", other_size.bytes(), other_access.description())
-                } else {
-                    other_access.description().to_owned()
-                },
+                action: other_access.description(None, other_size),
                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 {}", access_size.bytes(), access.description())
-                } else {
-                    access.description().to_owned()
-                },
+                action: access.description(ty, other_size.map(|_| access_size)),
                thread_info: current_thread_info,
                span: current_clocks.clock.as_slice()[current_index.index()].span_data(),
            },
        }))?
    }

-    /// Detect data-races for an unsynchronized read operation, will not perform
+    /// Detect data-races for an unsynchronized read operation. It will not perform
    /// data-race detection if `race_detecting()` is false, either due to no threads
    /// being created or if it is temporarily disabled during a racy read or write
    /// operation for which data-race detection is handled separately, for example
-    /// atomic read operations.
+    /// atomic read operations. The `ty` parameter is used for diagnostics, letting
+    /// the user know which type was read.
    pub fn read<'tcx>(
        &self,
        alloc_id: AllocId,
        access_range: AllocRange,
+        read_type: NaReadType,
+        ty: Option<Ty<'_>>,
        machine: &MiriMachine<'_, '_>,
    ) -> InterpResult<'tcx> {
        let current_span = machine.current_span();
@ -992,7 +1032,7 @@ impl VClockAlloc {
                alloc_ranges.iter_mut(access_range.start, access_range.size)
            {
                if let Err(DataRace) =
-                    mem_clocks.read_race_detect(&mut thread_clocks, index, current_span)
+                    mem_clocks.read_race_detect(&mut thread_clocks, index, read_type, current_span)
                {
                    drop(thread_clocks);
                    // Report data-race.
@ -1000,9 +1040,10 @@ impl VClockAlloc {
                        global,
                        &machine.threads,
                        mem_clocks,
-                        AccessType::NaRead,
+                        AccessType::NaRead(read_type),
                        access_range.size,
                        Pointer::new(alloc_id, Size::from_bytes(mem_clocks_range.start)),
+                        ty,
                    );
                }
            }
@ -1012,12 +1053,17 @@ impl VClockAlloc {
        }
    }

-    // Shared code for detecting data-races on unique access to a section of memory
-    fn unique_access<'tcx>(
+    /// Detect data-races for an unsynchronized write operation. It will not perform
+    /// data-race detection if `race_detecting()` is false, either due to no threads
+    /// being created or if it is temporarily disabled during a racy read or write
+    /// operation. The `ty` parameter is used for diagnostics, letting
+    /// the user know which type was written.
+    pub fn write<'tcx>(
        &mut self,
        alloc_id: AllocId,
        access_range: AllocRange,
        write_type: NaWriteType,
+        ty: Option<Ty<'_>>,
        machine: &mut MiriMachine<'_, '_>,
    ) -> InterpResult<'tcx> {
        let current_span = machine.current_span();
@ -1042,6 +1088,7 @@ impl VClockAlloc {
                        AccessType::NaWrite(write_type),
                        access_range.size,
                        Pointer::new(alloc_id, Size::from_bytes(mem_clocks_range.start)),
+                        ty,
                    );
                }
            }
@ -1050,37 +1097,6 @@ impl VClockAlloc {
            Ok(())
        }
    }
-
-    /// Detect data-races for an unsynchronized write operation, will not perform
-    /// data-race threads if `race_detecting()` is false, either due to no threads
-    /// being created or if it is temporarily disabled during a racy read or write
-    /// operation
-    pub fn write<'tcx>(
-        &mut self,
-        alloc_id: AllocId,
-        range: AllocRange,
-        machine: &mut MiriMachine<'_, '_>,
-    ) -> InterpResult<'tcx> {
-        self.unique_access(alloc_id, range, NaWriteType::Write, machine)
-    }
-
-    /// Detect data-races for an unsynchronized deallocate operation, will not perform
-    /// data-race threads if `race_detecting()` is false, either due to no threads
-    /// being created or if it is temporarily disabled during a racy read or write
-    /// operation
-    pub fn deallocate<'tcx>(
-        &mut self,
-        alloc_id: AllocId,
-        size: Size,
-        machine: &mut MiriMachine<'_, '_>,
-    ) -> InterpResult<'tcx> {
-        self.unique_access(
-            alloc_id,
-            alloc_range(Size::ZERO, size),
-            NaWriteType::Deallocate,
-            machine,
-        )
-    }
 }

 impl<'mir, 'tcx: 'mir> EvalContextPrivExt<'mir, 'tcx> for MiriInterpCx<'mir, 'tcx> {}
@ -1279,7 +1295,7 @@ trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
                let alloc_meta = this.get_alloc_extra(alloc_id)?.data_race.as_ref().unwrap();
                trace!(
                    "Atomic op({}) with ordering {:?} on {:?} (size={})",
-                    access.description(),
+                    access.description(None, None),
                    &atomic,
                    place.ptr(),
                    size.bytes()
@ -1307,6 +1323,7 @@ trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
                                        alloc_id,
                                        Size::from_bytes(mem_clocks_range.start),
                                    ),
+                                    None,
                                )
                                .map(|_| true);
                            }
--- a/src/tools/miri/src/concurrency/vector_clock.rs
+++ b/src/tools/miri/src/concurrency/vector_clock.rs
@ -4,9 +4,11 @@ use smallvec::SmallVec;
 use std::{
    cmp::Ordering,
    fmt::Debug,
-    ops::{Index, IndexMut},
+    ops::{Index, IndexMut, Shr},
 };

+use super::data_race::NaReadType;
+
 /// A vector clock index, this is associated with a thread id
 /// but in some cases one vector index may be shared with
 /// multiple thread ids if it's safe to do so.
@ -50,13 +52,51 @@ const SMALL_VECTOR: usize = 4;
 /// so that diagnostics can report what code was responsible for an operation.
 #[derive(Clone, Copy, Debug)]
 pub struct VTimestamp {
-    time: u32,
+    /// The lowest bit indicates read type, the rest is the time.
+    /// `1` indicates a retag read, `0` a regular read.
+    time_and_read_type: u32,
    pub span: Span,
 }

 impl VTimestamp {
-    pub const ZERO: VTimestamp = VTimestamp { time: 0, span: DUMMY_SP };
+    pub const ZERO: VTimestamp = VTimestamp::new(0, NaReadType::Read, DUMMY_SP);

+    #[inline]
+    const fn encode_time_and_read_type(time: u32, read_type: NaReadType) -> u32 {
+        let read_type_bit = match read_type {
+            NaReadType::Read => 0,
+            NaReadType::Retag => 1,
+        };
+        // Put the `read_type` in the lowest bit and `time` in the rest
+        read_type_bit | time.checked_mul(2).expect("Vector clock overflow")
+    }
+
+    #[inline]
+    const fn new(time: u32, read_type: NaReadType, span: Span) -> Self {
+        Self { time_and_read_type: Self::encode_time_and_read_type(time, read_type), span }
+    }
+
+    #[inline]
+    fn time(&self) -> u32 {
+        self.time_and_read_type.shr(1)
+    }
+
+    #[inline]
+    fn set_time(&mut self, time: u32) {
+        self.time_and_read_type = Self::encode_time_and_read_type(time, self.read_type());
+    }
+
+    #[inline]
+    pub fn read_type(&self) -> NaReadType {
+        if self.time_and_read_type & 1 == 0 { NaReadType::Read } else { NaReadType::Retag }
+    }
+
+    #[inline]
+    pub fn set_read_type(&mut self, read_type: NaReadType) {
+        self.time_and_read_type = Self::encode_time_and_read_type(self.time(), read_type);
+    }
+
+    #[inline]
    pub fn span_data(&self) -> SpanData {
        self.span.data()
    }
@ -64,7 +104,7 @@ impl VTimestamp {

 impl PartialEq for VTimestamp {
    fn eq(&self, other: &Self) -> bool {
-        self.time == other.time
+        self.time() == other.time()
    }
 }

@ -78,7 +118,7 @@ impl PartialOrd for VTimestamp {

 impl Ord for VTimestamp {
    fn cmp(&self, other: &Self) -> Ordering {
-        self.time.cmp(&other.time)
+        self.time().cmp(&other.time())
    }
 }

@ -130,7 +170,7 @@ impl VClock {
        let idx = idx.index();
        let mut_slice = self.get_mut_with_min_len(idx + 1);
        let idx_ref = &mut mut_slice[idx];
-        idx_ref.time = idx_ref.time.checked_add(1).expect("Vector clock overflow");
+        idx_ref.set_time(idx_ref.time().checked_add(1).expect("Vector clock overflow"));
        if !current_span.is_dummy() {
            idx_ref.span = current_span;
        }
@ -379,8 +419,8 @@ impl IndexMut<VectorIdx> for VClock {
 ///  test suite
 #[cfg(test)]
 mod tests {
-
    use super::{VClock, VTimestamp, VectorIdx};
+    use crate::concurrency::data_race::NaReadType;
    use rustc_span::DUMMY_SP;
    use std::cmp::Ordering;

@ -448,7 +488,13 @@ mod tests {
        while let Some(0) = slice.last() {
            slice = &slice[..slice.len() - 1]
        }
-        VClock(slice.iter().copied().map(|time| VTimestamp { time, span: DUMMY_SP }).collect())
+        VClock(
+            slice
+                .iter()
+                .copied()
+                .map(|time| VTimestamp::new(time, NaReadType::Read, DUMMY_SP))
+                .collect(),
+        )
    }

    fn assert_order(l: &[u32], r: &[u32], o: Option<Ordering>) {
--- a/src/tools/miri/src/diagnostics.rs
+++ b/src/tools/miri/src/diagnostics.rs
@ -46,6 +46,7 @@ pub enum TerminationInfo {
        op1: RacingOp,
        op2: RacingOp,
        extra: Option<&'static str>,
+        retag_explain: bool,
    },
 }

@ -263,12 +264,17 @@ 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 occur on all (re)borrows and as well as when references are copied or moved".to_owned()));
+                    helps.push((None, "retags permit optimizations that insert speculative reads or writes".to_owned()));
+                    helps.push((None, "therefore from the perspective of data races, a retag has the same implications as a read or 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
--- a/src/tools/miri/src/lib.rs
+++ b/src/tools/miri/src/lib.rs
@ -1,5 +1,6 @@
 #![feature(rustc_private)]
 #![feature(cell_update)]
+#![feature(const_option)]
 #![feature(float_gamma)]
 #![feature(generic_nonzero)]
 #![feature(map_try_insert)]
--- a/src/tools/miri/src/machine.rs
+++ b/src/tools/miri/src/machine.rs
@ -35,6 +35,9 @@ use crate::{
    *,
 };

+use self::concurrency::data_race::NaReadType;
+use self::concurrency::data_race::NaWriteType;
+
 /// First real-time signal.
 /// `signal(7)` says this must be between 32 and 64 and specifies 34 or 35
 /// as typical values.
@ -1238,7 +1241,7 @@ impl<'mir, 'tcx> Machine<'mir, 'tcx> for MiriMachine<'mir, 'tcx> {
                .emit_diagnostic(NonHaltingDiagnostic::AccessedAlloc(alloc_id, AccessKind::Read));
        }
        if let Some(data_race) = &alloc_extra.data_race {
-            data_race.read(alloc_id, range, machine)?;
+            data_race.read(alloc_id, range, NaReadType::Read, None, machine)?;
        }
        if let Some(borrow_tracker) = &alloc_extra.borrow_tracker {
            borrow_tracker.before_memory_read(alloc_id, prov_extra, range, machine)?;
@ -1262,7 +1265,7 @@ impl<'mir, 'tcx> Machine<'mir, 'tcx> for MiriMachine<'mir, 'tcx> {
                .emit_diagnostic(NonHaltingDiagnostic::AccessedAlloc(alloc_id, AccessKind::Write));
        }
        if let Some(data_race) = &mut alloc_extra.data_race {
-            data_race.write(alloc_id, range, machine)?;
+            data_race.write(alloc_id, range, NaWriteType::Write, None, machine)?;
        }
        if let Some(borrow_tracker) = &mut alloc_extra.borrow_tracker {
            borrow_tracker.before_memory_write(alloc_id, prov_extra, range, machine)?;
@ -1286,7 +1289,13 @@ impl<'mir, 'tcx> Machine<'mir, 'tcx> for MiriMachine<'mir, 'tcx> {
            machine.emit_diagnostic(NonHaltingDiagnostic::FreedAlloc(alloc_id));
        }
        if let Some(data_race) = &mut alloc_extra.data_race {
-            data_race.deallocate(alloc_id, size, machine)?;
+            data_race.write(
+                alloc_id,
+                alloc_range(Size::ZERO, size),
+                NaWriteType::Deallocate,
+                None,
+                machine,
+            )?;
        }
        if let Some(borrow_tracker) = &mut alloc_extra.borrow_tracker {
            borrow_tracker.before_memory_deallocation(alloc_id, prove_extra, size, machine)?;
--- a/src/tools/miri/tests/fail/both_borrows/retag_data_race_write.rs
+++ b/src/tools/miri/tests/fail/both_borrows/retag_data_race_write.rs
@ -17,7 +17,7 @@ fn thread_1(p: SendPtr) {
 fn thread_2(p: SendPtr) {
    let p = p.0;
    unsafe {
-        *p = 5; //~ ERROR: /Data race detected between \(1\) non-atomic (read|write) on thread `unnamed-[0-9]+` and \(2\) non-atomic write on thread `unnamed-[0-9]+`/
+        *p = 5; //~ ERROR: /Data race detected between \(1\) retag (read|write) on thread `unnamed-[0-9]+` and \(2\) non-atomic write on thread `unnamed-[0-9]+`/
    }
 }

--- a/src/tools/miri/tests/fail/both_borrows/retag_data_race_write.stack.stderr
+++ b/src/tools/miri/tests/fail/both_borrows/retag_data_race_write.stack.stderr
@ -1,14 +1,17 @@
-error: Undefined Behavior: Data race detected between (1) non-atomic write on thread `unnamed-ID` and (2) non-atomic write on thread `unnamed-ID` at ALLOC. (2) just happened here
+error: Undefined Behavior: Data race detected between (1) retag write on thread `unnamed-ID` and (2) non-atomic write on thread `unnamed-ID` at ALLOC. (2) just happened here
  --> $DIR/retag_data_race_write.rs:LL:CC
   |
 LL |         *p = 5;
-   |         ^^^^^^ Data race detected between (1) non-atomic write on thread `unnamed-ID` and (2) non-atomic write on thread `unnamed-ID` at ALLOC. (2) just happened here
+   |         ^^^^^^ Data race detected between (1) retag write on thread `unnamed-ID` and (2) non-atomic write on thread `unnamed-ID` at ALLOC. (2) just happened here
   |
 help: and (1) occurred earlier here
  --> $DIR/retag_data_race_write.rs:LL:CC
   |
 LL |         let _r = &mut *p;
   |                  ^^^^^^^
+   = help: retags occur on all (re)borrows and as well as when references are copied or moved
+   = help: retags permit optimizations that insert speculative reads or writes
+   = help: therefore from the perspective of data races, a retag has the same implications as a read or write
   = 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) on thread `unnamed-ID`:
--- a/src/tools/miri/tests/fail/both_borrows/retag_data_race_write.tree.stderr
+++ b/src/tools/miri/tests/fail/both_borrows/retag_data_race_write.tree.stderr
@ -1,14 +1,17 @@
-error: Undefined Behavior: Data race detected between (1) non-atomic read on thread `unnamed-ID` and (2) non-atomic write on thread `unnamed-ID` at ALLOC. (2) just happened here
+error: Undefined Behavior: Data race detected between (1) retag read on thread `unnamed-ID` and (2) non-atomic write on thread `unnamed-ID` at ALLOC. (2) just happened here
  --> $DIR/retag_data_race_write.rs:LL:CC
   |
 LL |         *p = 5;
-   |         ^^^^^^ Data race detected between (1) non-atomic read on thread `unnamed-ID` and (2) non-atomic write on thread `unnamed-ID` at ALLOC. (2) just happened here
+   |         ^^^^^^ Data race detected between (1) retag read on thread `unnamed-ID` and (2) non-atomic write on thread `unnamed-ID` at ALLOC. (2) just happened here
   |
 help: and (1) occurred earlier here
  --> $DIR/retag_data_race_write.rs:LL:CC
   |
 LL |         let _r = &mut *p;
   |                  ^^^^^^^
+   = help: retags occur on all (re)borrows and as well as when references are copied or moved
+   = help: retags permit optimizations that insert speculative reads or writes
+   = help: therefore from the perspective of data races, a retag has the same implications as a read or write
   = 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) on thread `unnamed-ID`:
--- a/src/tools/miri/tests/fail/stacked_borrows/retag_data_race_protected_read.rs
+++ b/src/tools/miri/tests/fail/stacked_borrows/retag_data_race_protected_read.rs
@ -13,7 +13,7 @@ fn main() {
        let ptr = ptr;
        // We do a protected mutable retag (but no write!) in this thread.
        fn retag(_x: &mut i32) {}
-        retag(unsafe { &mut *ptr.0 }); //~ERROR: Data race detected between (1) non-atomic read on thread `main` and (2) non-atomic write on thread `unnamed-1`
+        retag(unsafe { &mut *ptr.0 }); //~ERROR: Data race detected between (1) non-atomic read on thread `main` and (2) retag write of type `i32` on thread `unnamed-1`
    });

    // We do a read in the main thread.
--- a/src/tools/miri/tests/fail/stacked_borrows/retag_data_race_protected_read.stderr
+++ b/src/tools/miri/tests/fail/stacked_borrows/retag_data_race_protected_read.stderr
@ -1,14 +1,17 @@
-error: Undefined Behavior: Data race detected between (1) non-atomic read on thread `main` and (2) non-atomic write on thread `unnamed-ID` at ALLOC. (2) just happened here
+error: Undefined Behavior: Data race detected between (1) non-atomic read on thread `main` and (2) retag write of type `i32` on thread `unnamed-ID` at ALLOC. (2) just happened here
  --> $DIR/retag_data_race_protected_read.rs:LL:CC
   |
 LL |         retag(unsafe { &mut *ptr.0 });
-   |                        ^^^^^^^^^^^ Data race detected between (1) non-atomic read on thread `main` and (2) non-atomic write on thread `unnamed-ID` at ALLOC. (2) just happened here
+   |                        ^^^^^^^^^^^ Data race detected between (1) non-atomic read on thread `main` and (2) retag write of type `i32` on thread `unnamed-ID` at ALLOC. (2) just happened here
   |
 help: and (1) occurred earlier here
  --> $DIR/retag_data_race_protected_read.rs:LL:CC
   |
 LL |     unsafe { ptr.0.read() };
   |              ^^^^^^^^^^^^
+   = help: retags occur on all (re)borrows and as well as when references are copied or moved
+   = help: retags permit optimizations that insert speculative reads or writes
+   = help: therefore from the perspective of data races, a retag has the same implications as a read or write
   = 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) on thread `unnamed-ID`:
--- a/src/tools/miri/tests/fail/stacked_borrows/retag_data_race_read.rs
+++ b/src/tools/miri/tests/fail/stacked_borrows/retag_data_race_read.rs
@ -15,7 +15,7 @@ fn thread_1(p: SendPtr) {
 fn thread_2(p: SendPtr) {
    let p = p.0;
    unsafe {
-        *p = 5; //~ ERROR: Data race detected between (1) non-atomic read on thread `unnamed-1` and (2) non-atomic write on thread `unnamed-2`
+        *p = 5; //~ ERROR: Data race detected between (1) retag read on thread `unnamed-1` and (2) non-atomic write on thread `unnamed-2`
    }
 }

--- a/src/tools/miri/tests/fail/stacked_borrows/retag_data_race_read.stderr
+++ b/src/tools/miri/tests/fail/stacked_borrows/retag_data_race_read.stderr
@ -1,14 +1,17 @@
-error: Undefined Behavior: Data race detected between (1) non-atomic read on thread `unnamed-ID` and (2) non-atomic write on thread `unnamed-ID` at ALLOC. (2) just happened here
+error: Undefined Behavior: Data race detected between (1) retag read on thread `unnamed-ID` and (2) non-atomic write on thread `unnamed-ID` at ALLOC. (2) just happened here
  --> $DIR/retag_data_race_read.rs:LL:CC
   |
 LL |         *p = 5;
-   |         ^^^^^^ Data race detected between (1) non-atomic read on thread `unnamed-ID` and (2) non-atomic write on thread `unnamed-ID` at ALLOC. (2) just happened here
+   |         ^^^^^^ Data race detected between (1) retag read on thread `unnamed-ID` and (2) non-atomic write on thread `unnamed-ID` at ALLOC. (2) just happened here
   |
 help: and (1) occurred earlier here
  --> $DIR/retag_data_race_read.rs:LL:CC
   |
 LL |         let _r = &*p;
   |                  ^^^
+   = help: retags occur on all (re)borrows and as well as when references are copied or moved
+   = help: retags permit optimizations that insert speculative reads or writes
+   = help: therefore from the perspective of data races, a retag has the same implications as a read or write
   = 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) on thread `unnamed-ID`: