about summary refs log tree commit diff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/tools/miri/src/borrow_tracker/mod.rs20
-rw-r--r--src/tools/miri/src/borrow_tracker/stacked_borrows/diagnostics.rs3
-rw-r--r--src/tools/miri/src/borrow_tracker/stacked_borrows/mod.rs8
-rw-r--r--src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs21
-rw-r--r--src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs57
-rw-r--r--src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs186
-rw-r--r--src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs380
-rw-r--r--src/tools/miri/src/borrow_tracker/tree_borrows/tree/tests.rs25
-rw-r--r--src/tools/miri/src/borrow_tracker/tree_borrows/unimap.rs7
-rw-r--r--src/tools/miri/src/machine.rs30
-rw-r--r--src/tools/miri/tests/fail/both_borrows/aliasing_mut1.tree.stderr6
-rw-r--r--src/tools/miri/tests/fail/both_borrows/aliasing_mut2.tree.stderr6
-rw-r--r--src/tools/miri/tests/fail/both_borrows/aliasing_mut3.tree.stderr6
-rw-r--r--src/tools/miri/tests/fail/both_borrows/newtype_pair_retagging.tree.stderr6
-rw-r--r--src/tools/miri/tests/fail/both_borrows/newtype_retagging.tree.stderr6
-rw-r--r--src/tools/miri/tests/fail/both_borrows/retag_data_race_protected_read.rs29
-rw-r--r--src/tools/miri/tests/fail/both_borrows/retag_data_race_protected_read.tree.stderr25
-rw-r--r--src/tools/miri/tests/fail/stacked_borrows/retag_data_race_protected_read.rs30
-rw-r--r--src/tools/miri/tests/fail/stacked_borrows/retag_data_race_protected_read.stderr (renamed from src/tools/miri/tests/fail/both_borrows/retag_data_race_protected_read.stack.stderr)0
-rw-r--r--src/tools/miri/tests/fail/tree_borrows/reserved/cell-protected-write.stderr14
-rw-r--r--src/tools/miri/tests/fail/tree_borrows/reserved/int-protected-write.stderr14
-rw-r--r--src/tools/miri/tests/fail/tree_borrows/spurious_read.rs117
-rw-r--r--src/tools/miri/tests/fail/tree_borrows/spurious_read.stderr44
-rw-r--r--src/tools/miri/tests/pass/tree_borrows/cell-alternate-writes.stderr12
-rw-r--r--src/tools/miri/tests/pass/tree_borrows/end-of-protector.stderr48
-rw-r--r--src/tools/miri/tests/pass/tree_borrows/formatting.stderr50
-rw-r--r--src/tools/miri/tests/pass/tree_borrows/read_retag_no_race.rs114
-rw-r--r--src/tools/miri/tests/pass/tree_borrows/read_retag_no_race.stderr8
-rw-r--r--src/tools/miri/tests/pass/tree_borrows/reborrow-is-read.stderr18
-rw-r--r--src/tools/miri/tests/pass/tree_borrows/reserved.stderr68
-rw-r--r--src/tools/miri/tests/pass/tree_borrows/spurious_read.rs115
-rw-r--r--src/tools/miri/tests/pass/tree_borrows/spurious_read.stderr16
-rw-r--r--src/tools/miri/tests/pass/tree_borrows/tree-borrows.rs19
-rw-r--r--src/tools/miri/tests/pass/tree_borrows/unique.default.stderr24
-rw-r--r--src/tools/miri/tests/pass/tree_borrows/unique.uniq.stderr30
-rw-r--r--src/tools/miri/tests/pass/tree_borrows/vec_unique.default.stderr6
-rw-r--r--src/tools/miri/tests/pass/tree_borrows/vec_unique.uniq.stderr10
37 files changed, 1097 insertions, 481 deletions
diff --git a/src/tools/miri/src/borrow_tracker/mod.rs b/src/tools/miri/src/borrow_tracker/mod.rs
index 1951cf87f2f..a95571572d6 100644
--- a/src/tools/miri/src/borrow_tracker/mod.rs
+++ b/src/tools/miri/src/borrow_tracker/mod.rs
@@ -66,10 +66,13 @@ pub struct FrameState {
     /// `stacked_borrows::GlobalState` upon function return, and if we attempt to pop a protected
     /// tag, to identify which call is responsible for protecting the tag.
     /// See `Stack::item_popped` for more explanation.
+    /// Tree Borrows also needs to know which allocation these tags
+    /// belong to so that it can perform a read through them immediately before
+    /// the frame gets popped.
     ///
     /// This will contain one tag per reference passed to the function, so
     /// a size of 2 is enough for the vast majority of functions.
-    pub protected_tags: SmallVec<[BorTag; 2]>,
+    pub protected_tags: SmallVec<[(AllocId, BorTag); 2]>,
 }
 
 impl VisitTags for FrameState {
@@ -208,7 +211,7 @@ impl GlobalStateInner {
     }
 
     pub fn end_call(&mut self, frame: &machine::FrameExtra<'_>) {
-        for tag in &frame
+        for (_, tag) in &frame
             .borrow_tracker
             .as_ref()
             .expect("we should have borrow tracking data")
@@ -453,6 +456,19 @@ impl AllocState {
             AllocState::TreeBorrows(tb) => tb.borrow_mut().remove_unreachable_tags(tags),
         }
     }
+
+    /// Tree Borrows needs to be told when a tag stops being protected.
+    pub fn release_protector<'tcx>(
+        &self,
+        machine: &MiriMachine<'_, 'tcx>,
+        global: &GlobalState,
+        tag: BorTag,
+    ) -> InterpResult<'tcx> {
+        match self {
+            AllocState::StackedBorrows(_sb) => Ok(()),
+            AllocState::TreeBorrows(tb) => tb.borrow_mut().release_protector(machine, global, tag),
+        }
+    }
 }
 
 impl VisitTags for AllocState {
diff --git a/src/tools/miri/src/borrow_tracker/stacked_borrows/diagnostics.rs b/src/tools/miri/src/borrow_tracker/stacked_borrows/diagnostics.rs
index 1ef30cb9fad..1a11879fa90 100644
--- a/src/tools/miri/src/borrow_tracker/stacked_borrows/diagnostics.rs
+++ b/src/tools/miri/src/borrow_tracker/stacked_borrows/diagnostics.rs
@@ -436,6 +436,7 @@ impl<'history, 'ecx, 'mir, 'tcx> DiagnosticCx<'history, 'ecx, 'mir, 'tcx> {
             ProtectorKind::WeakProtector => "weakly protected",
             ProtectorKind::StrongProtector => "strongly protected",
         };
+        let item_tag = item.tag();
         let call_id = self
             .machine
             .threads
@@ -444,7 +445,7 @@ impl<'history, 'ecx, 'mir, 'tcx> DiagnosticCx<'history, 'ecx, 'mir, 'tcx> {
             .map(|frame| {
                 frame.extra.borrow_tracker.as_ref().expect("we should have borrow tracking data")
             })
-            .find(|frame| frame.protected_tags.contains(&item.tag()))
+            .find(|frame| frame.protected_tags.iter().any(|(_, tag)| tag == &item_tag))
             .map(|frame| frame.call_id)
             .unwrap(); // FIXME: Surely we should find something, but a panic seems wrong here?
         match self.operation {
diff --git a/src/tools/miri/src/borrow_tracker/stacked_borrows/mod.rs b/src/tools/miri/src/borrow_tracker/stacked_borrows/mod.rs
index a440ee720c7..66b729fb166 100644
--- a/src/tools/miri/src/borrow_tracker/stacked_borrows/mod.rs
+++ b/src/tools/miri/src/borrow_tracker/stacked_borrows/mod.rs
@@ -719,7 +719,13 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
 
         if let Some(protect) = new_perm.protector() {
             // See comment in `Stack::item_invalidated` for why we store the tag twice.
-            this.frame_mut().extra.borrow_tracker.as_mut().unwrap().protected_tags.push(new_tag);
+            this.frame_mut()
+                .extra
+                .borrow_tracker
+                .as_mut()
+                .unwrap()
+                .protected_tags
+                .push((alloc_id, new_tag));
             this.machine
                 .borrow_tracker
                 .as_mut()
diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs
index fd45671ba29..b3001b5b88c 100644
--- a/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs
+++ b/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs
@@ -19,6 +19,7 @@ pub enum AccessCause {
     Explicit(AccessKind),
     Reborrow,
     Dealloc,
+    FnExit,
 }
 
 impl fmt::Display for AccessCause {
@@ -27,6 +28,7 @@ impl fmt::Display for AccessCause {
             Self::Explicit(kind) => write!(f, "{kind}"),
             Self::Reborrow => write!(f, "reborrow"),
             Self::Dealloc => write!(f, "deallocation"),
+            Self::FnExit => write!(f, "protector release"),
         }
     }
 }
@@ -38,6 +40,7 @@ impl AccessCause {
             Self::Explicit(kind) => format!("{rel} {kind}"),
             Self::Reborrow => format!("reborrow (acting as a {rel} read access)"),
             Self::Dealloc => format!("deallocation (acting as a {rel} write access)"),
+            Self::FnExit => format!("protector release (acting as a {rel} read access)"),
         }
     }
 }
@@ -52,7 +55,9 @@ pub struct Event {
     /// Relative position of the tag to the one used for the access.
     pub is_foreign: bool,
     /// User-visible range of the access.
-    pub access_range: AllocRange,
+    /// `None` means that this is an implicit access to the entire allocation
+    /// (used for the implicit read on protector release).
+    pub access_range: Option<AllocRange>,
     /// The transition recorded by this event only occured on a subrange of
     /// `access_range`: a single access on `access_range` triggers several events,
     /// each with their own mutually disjoint `transition_range`. No-op transitions
@@ -123,7 +128,17 @@ impl HistoryData {
             // NOTE: `transition_range` is explicitly absent from the error message, it has no significance
             // to the user. The meaningful one is `access_range`.
             let access = access_cause.print_as_access(is_foreign);
-            self.events.push((Some(span.data()), format!("{this} later transitioned to {endpoint} due to a {access} at offsets {access_range:?}", endpoint = transition.endpoint())));
+            let access_range_text = match access_range {
+                Some(r) => format!("at offsets {r:?}"),
+                None => format!("on every location previously accessed by this tag"),
+            };
+            self.events.push((
+                Some(span.data()),
+                format!(
+                    "{this} later transitioned to {endpoint} due to a {access} {access_range_text}",
+                    endpoint = transition.endpoint()
+                ),
+            ));
             self.events
                 .push((None, format!("this transition corresponds to {}", transition.summary())));
         }
@@ -745,7 +760,7 @@ const DEFAULT_FORMATTER: DisplayFmt = DisplayFmt {
         bot: '─',
         warning_text: "Warning: this tree is indicative only. Some tags may have been hidden.",
     },
-    perm: DisplayFmtPermission { open: "|", sep: "|", close: "|", uninit: "---", range_sep: ".." },
+    perm: DisplayFmtPermission { open: "|", sep: "|", close: "|", uninit: "----", range_sep: ".." },
     padding: DisplayFmtPadding {
         join_middle: "├",
         join_last: "└",
diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs
index 68bc4a415c6..6d4c573a35c 100644
--- a/src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs
+++ b/src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs
@@ -2,7 +2,9 @@ use log::trace;
 
 use rustc_target::abi::{Abi, Align, Size};
 
-use crate::borrow_tracker::{AccessKind, GlobalStateInner, ProtectorKind, RetagFields};
+use crate::borrow_tracker::{
+    AccessKind, GlobalState, GlobalStateInner, ProtectorKind, RetagFields,
+};
 use rustc_middle::{
     mir::{Mutability, RetagKind},
     ty::{
@@ -70,7 +72,7 @@ impl<'tcx> Tree {
         self.perform_access(
             access_kind,
             tag,
-            range,
+            Some(range),
             global,
             span,
             diagnostics::AccessCause::Explicit(access_kind),
@@ -99,6 +101,29 @@ impl<'tcx> Tree {
     pub fn expose_tag(&mut self, _tag: BorTag) {
         // TODO
     }
+
+    /// A tag just lost its protector.
+    ///
+    /// This emits a special kind of access that is only applied
+    /// to initialized locations, as a protection against other
+    /// tags not having been made aware of the existence of this
+    /// protector.
+    pub fn release_protector(
+        &mut self,
+        machine: &MiriMachine<'_, 'tcx>,
+        global: &GlobalState,
+        tag: BorTag,
+    ) -> InterpResult<'tcx> {
+        let span = machine.current_span();
+        self.perform_access(
+            AccessKind::Read,
+            tag,
+            None, // no specified range because it occurs on the entire allocation
+            global,
+            span,
+            diagnostics::AccessCause::FnExit,
+        )
+    }
 }
 
 /// Policy for a new borrow.
@@ -248,7 +273,13 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
             // We register the protection in two different places.
             // This makes creating a protector slower, but checking whether a tag
             // is protected faster.
-            this.frame_mut().extra.borrow_tracker.as_mut().unwrap().protected_tags.push(new_tag);
+            this.frame_mut()
+                .extra
+                .borrow_tracker
+                .as_mut()
+                .unwrap()
+                .protected_tags
+                .push((alloc_id, new_tag));
             this.machine
                 .borrow_tracker
                 .as_mut()
@@ -275,7 +306,7 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
         tree_borrows.perform_access(
             AccessKind::Read,
             orig_tag,
-            range,
+            Some(range),
             this.machine.borrow_tracker.as_ref().unwrap(),
             this.machine.current_span(),
             diagnostics::AccessCause::Reborrow,
@@ -287,21 +318,7 @@ 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() {
-                // We sometimes need to make it a write, since not all retags commute with reads!
-                // FIXME: Is that truly the semantics we want? Some optimizations are likely to be
-                // very unhappy without this. We'd tsill ge some UB just by picking a suitable
-                // interleaving, but wether UB happens can depend on whether a write occurs in the
-                // future...
-                let is_write = new_perm.initial_state.is_active()
-                    || (new_perm.initial_state.is_reserved(None) && new_perm.protector.is_some());
-                if is_write {
-                    // Need to get mutable access to alloc_extra.
-                    // (Cannot always do this as we can do read-only reborrowing on read-only allocations.)
-                    let (alloc_extra, machine) = this.get_alloc_extra_mut(alloc_id)?;
-                    alloc_extra.data_race.as_mut().unwrap().write(alloc_id, range, machine)?;
-                } else {
-                    data_race.read(alloc_id, range, &this.machine)?;
-                }
+                data_race.read(alloc_id, range, &this.machine)?;
             }
         }
 
@@ -532,7 +549,7 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriInterpCxExt<'mir, 'tcx> {
                 // if converting this alloc_id from a global to a local one
                 // uncovers a non-supported `extern static`.
                 let alloc_extra = this.get_alloc_extra(alloc_id)?;
-                trace!("Stacked Borrows tag {tag:?} exposed in {alloc_id:?}");
+                trace!("Tree Borrows tag {tag:?} exposed in {alloc_id:?}");
                 alloc_extra.borrow_tracker_tb().borrow_mut().expose_tag(tag);
             }
             AllocKind::Function | AllocKind::VTable | AllocKind::Dead => {
diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs
index 3e019356ca7..bf72e902993 100644
--- a/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs
+++ b/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs
@@ -10,9 +10,18 @@ use crate::borrow_tracker::AccessKind;
 enum PermissionPriv {
     /// represents: a local reference that has not yet been written to;
     /// allows: child reads, foreign reads, foreign writes if type is freeze;
-    /// rejects: child writes (Active), foreign writes (Disabled, except if type is not freeze).
-    /// special case: behaves differently when protected to adhere more closely to noalias
-    Reserved { ty_is_freeze: bool },
+    /// affected by: child writes (becomes Active),
+    /// rejects: foreign writes (Disabled, except if type is not freeze).
+    ///
+    /// special case: behaves differently when protected, which is where `conflicted`
+    /// is relevant
+    /// - `conflicted` is set on foreign reads,
+    /// - `conflicted` must not be set on child writes (there is UB otherwise).
+    /// This is so that the behavior of `Reserved` adheres to the rules of `noalias`:
+    /// - foreign-read then child-write is UB due to `conflicted`,
+    /// - child-write then foreign-read is UB since child-write will activate and then
+    ///   foreign-read disables a protected `Active`, which is UB.
+    Reserved { ty_is_freeze: bool, conflicted: bool },
     /// represents: a unique pointer;
     /// allows: child reads, child writes;
     /// rejects: foreign reads (Frozen), foreign writes (Disabled).
@@ -29,10 +38,11 @@ enum PermissionPriv {
 use PermissionPriv::*;
 
 impl PartialOrd for PermissionPriv {
-    /// PermissionPriv is ordered as follows:
-    /// - Reserved(_) < Active < Frozen < Disabled;
-    /// - different kinds of `Reserved` (with or without interior mutability)
-    /// are incomparable to each other.
+    /// PermissionPriv is ordered by the reflexive transitive closure of
+    /// `Reserved(conflicted=false) < Reserved(conflicted=true) < Active < Frozen < Disabled`.
+    /// `Reserved` that have incompatible `ty_is_freeze` are incomparable to each other.
+    /// This ordering matches the reachability by transitions, as asserted by the exhaustive test
+    /// `permissionpriv_partialord_is_reachability`.
     fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
         use Ordering::*;
         Some(match (self, other) {
@@ -43,7 +53,17 @@ impl PartialOrd for PermissionPriv {
             (_, Frozen) => Less,
             (Active, _) => Greater,
             (_, Active) => Less,
-            (Reserved { .. }, Reserved { .. }) => return None,
+            (
+                Reserved { ty_is_freeze: f1, conflicted: c1 },
+                Reserved { ty_is_freeze: f2, conflicted: c2 },
+            ) => {
+                // No transition ever changes `ty_is_freeze`.
+                if f1 != f2 {
+                    return None;
+                }
+                // `bool` is ordered such that `false <= true`, so this works as intended.
+                c1.cmp(c2)
+            }
         })
     }
 }
@@ -51,7 +71,7 @@ impl PartialOrd for PermissionPriv {
 impl PermissionPriv {
     /// Check if `self` can be the initial state of a pointer.
     fn is_initial(&self) -> bool {
-        matches!(self, Reserved { ty_is_freeze: _ } | Frozen)
+        matches!(self, Reserved { conflicted: false, .. } | Frozen)
     }
 }
 
@@ -66,12 +86,13 @@ mod transition {
         Some(match state {
             Disabled => return None,
             // The inner data `ty_is_freeze` of `Reserved` is always irrelevant for Read
-            // accesses, since the data is not being mutated. Hence the `{ .. }`
+            // accesses, since the data is not being mutated. Hence the `{ .. }`.
             readable @ (Reserved { .. } | Active | Frozen) => readable,
         })
     }
 
-    /// A non-child node was read-accessed: noop on non-protected Reserved, advance to Frozen otherwise.
+    /// A non-child node was read-accessed: keep `Reserved` but mark it as `conflicted` if it
+    /// is protected; invalidate `Active`.
     fn foreign_read(state: PermissionPriv, protected: bool) -> Option<PermissionPriv> {
         Some(match state {
             // Non-writeable states just ignore foreign reads.
@@ -79,16 +100,14 @@ mod transition {
             // Writeable states are more tricky, and depend on whether things are protected.
             // The inner data `ty_is_freeze` of `Reserved` is always irrelevant for Read
             // accesses, since the data is not being mutated. Hence the `{ .. }`
-            res @ Reserved { .. } =>
-                if protected {
-                    // Someone else read, make sure we won't write.
-                    // We could make this `Disabled` but it doesn't look like we get anything out of that extra UB.
-                    Frozen
-                } else {
-                    // Before activation and without protectors, foreign reads are fine.
-                    // That's the entire point of 2-phase borrows.
-                    res
-                },
+
+            // Someone else read. To make sure we won't write before function exit,
+            // we set the "conflicted" flag, which will disallow writes while we are protected.
+            Reserved { ty_is_freeze, .. } if protected =>
+                Reserved { ty_is_freeze, conflicted: true },
+            // Before activation and without protectors, foreign reads are fine.
+            // That's the entire point of 2-phase borrows.
+            res @ Reserved { .. } => res,
             Active =>
                 if protected {
                     // We wrote, someone else reads -- that's bad.
@@ -104,8 +123,12 @@ mod transition {
 
     /// A child node was write-accessed: `Reserved` must become `Active` to obtain
     /// write permissions, `Frozen` and `Disabled` cannot obtain such permissions and produce UB.
-    fn child_write(state: PermissionPriv, _protected: bool) -> Option<PermissionPriv> {
+    fn child_write(state: PermissionPriv, protected: bool) -> Option<PermissionPriv> {
         Some(match state {
+            // If the `conflicted` flag is set, then there was a foreign read during
+            // the function call that is still ongoing (still `protected`),
+            // this is UB (`noalias` violation).
+            Reserved { conflicted: true, .. } if protected => return None,
             // A write always activates the 2-phase borrow, even with interior
             // mutability
             Reserved { .. } | Active => Active,
@@ -117,7 +140,8 @@ mod transition {
     /// non-protected interior mutable `Reserved` which stay the same.
     fn foreign_write(state: PermissionPriv, protected: bool) -> Option<PermissionPriv> {
         Some(match state {
-            cell @ Reserved { ty_is_freeze: false } if !protected => cell,
+            Reserved { .. } if protected => Disabled,
+            res @ Reserved { ty_is_freeze: false, .. } => res,
             _ => Disabled,
         })
     }
@@ -166,7 +190,7 @@ impl Permission {
 
     /// Default initial permission of a reborrowed mutable reference.
     pub fn new_reserved(ty_is_freeze: bool) -> Self {
-        Self { inner: Reserved { ty_is_freeze } }
+        Self { inner: Reserved { ty_is_freeze, conflicted: false } }
     }
 
     /// Default initial permission of a reborrowed shared reference
@@ -174,28 +198,6 @@ impl Permission {
         Self { inner: Frozen }
     }
 
-    pub fn is_active(self) -> bool {
-        matches!(self.inner, Active)
-    }
-
-    // Leave `interior_mut` as `None` if interior mutability
-    // is irrelevant.
-    pub fn is_reserved(self, interior_mut: Option<bool>) -> bool {
-        match (interior_mut, self.inner) {
-            (None, Reserved { .. }) => true,
-            (Some(b1), Reserved { ty_is_freeze: b2 }) => b1 == b2,
-            _ => false,
-        }
-    }
-
-    pub fn is_frozen(self) -> bool {
-        matches!(self.inner, Frozen)
-    }
-
-    pub fn is_disabled(self) -> bool {
-        matches!(self.inner, Disabled)
-    }
-
     /// Apply the transition to the inner PermissionPriv.
     pub fn perform_access(
         kind: AccessKind,
@@ -251,8 +253,12 @@ pub mod diagnostics {
                 f,
                 "{}",
                 match self {
-                    Reserved { ty_is_freeze: true } => "Reserved",
-                    Reserved { ty_is_freeze: false } => "Reserved (interior mutable)",
+                    Reserved { ty_is_freeze: true, conflicted: false } => "Reserved",
+                    Reserved { ty_is_freeze: true, conflicted: true } => "Reserved (conflicted)",
+                    Reserved { ty_is_freeze: false, conflicted: false } =>
+                        "Reserved (interior mutable)",
+                    Reserved { ty_is_freeze: false, conflicted: true } =>
+                        "Reserved (interior mutable, conflicted)",
                     Active => "Active",
                     Frozen => "Frozen",
                     Disabled => "Disabled",
@@ -280,11 +286,13 @@ pub mod diagnostics {
             // and also as `diagnostics::DisplayFmtPermission.uninit` otherwise
             // alignment will be incorrect.
             match self.inner {
-                Reserved { ty_is_freeze: true } => "Res",
-                Reserved { ty_is_freeze: false } => "Re*",
-                Active => "Act",
-                Frozen => "Frz",
-                Disabled => "Dis",
+                Reserved { ty_is_freeze: true, conflicted: false } => "Rs  ",
+                Reserved { ty_is_freeze: true, conflicted: true } => "RsC ",
+                Reserved { ty_is_freeze: false, conflicted: false } => "RsM ",
+                Reserved { ty_is_freeze: false, conflicted: true } => "RsCM",
+                Active => "Act ",
+                Frozen => "Frz ",
+                Disabled => "Dis ",
             }
         }
     }
@@ -292,15 +300,13 @@ pub mod diagnostics {
     impl PermTransition {
         /// Readable explanation of the consequences of an event.
         /// Fits in the sentence "This accessed caused {trans.summary()}".
-        ///
-        /// Important: for the purposes of this explanation, `Reserved` is considered
-        /// to have write permissions, because that's what the diagnostics care about
-        /// (otherwise `Reserved -> Frozen` would be considered a noop).
         pub fn summary(&self) -> &'static str {
             assert!(self.is_possible());
             match (self.from, self.to) {
                 (_, Active) => "the first write to a 2-phase borrowed mutable reference",
                 (_, Frozen) => "a loss of write permissions",
+                (Reserved { conflicted: false, .. }, Reserved { conflicted: true, .. }) =>
+                    "a temporary loss of write permissions until function exit",
                 (Frozen, Disabled) => "a loss of read permissions",
                 (_, Disabled) => "a loss of read and write permissions",
                 (old, new) =>
@@ -315,7 +321,7 @@ pub mod diagnostics {
         /// Irrelevant events:
         /// - modifications of write permissions when the error is related to read permissions
         ///   (on failed reads and protected `Frozen -> Disabled`, ignore `Reserved -> Active`,
-        ///   `Reserved -> Frozen`, and `Active -> Frozen`)
+        ///   `Reserved(conflicted=false) -> Reserved(conflicted=true)`, and `Active -> Frozen`)
         /// - all transitions for attempts to deallocate strongly protected tags
         ///
         /// # Panics
@@ -326,8 +332,9 @@ pub mod diagnostics {
         /// (Reserved < Active < Frozen < Disabled);
         /// - between `self` and `err` the permission should also be increasing,
         /// so all permissions inside `err` should be greater than `self.1`;
-        /// - `Active` and `Reserved` cannot cause an error due to insufficient permissions,
-        /// so `err` cannot be a `ChildAccessForbidden(_)` of either of them;
+        /// - `Active` and `Reserved(conflicted=false)` cannot cause an error
+        /// due to insufficient permissions, so `err` cannot be a `ChildAccessForbidden(_)`
+        /// of either of them;
         /// - `err` should not be `ProtectedDisabled(Disabled)`, because the protected
         /// tag should not have been `Disabled` in the first place (if this occurs it means
         /// we have unprotected tags that become protected)
@@ -347,23 +354,28 @@ pub mod diagnostics {
                         (Frozen, Frozen) => true,
                         (Active, Frozen) => true,
                         (Disabled, Disabled) => true,
+                        (Reserved { conflicted: true, .. }, Reserved { conflicted: true, .. }) =>
+                            true,
                         // A pointer being `Disabled` is a strictly stronger source of
                         // errors than it being `Frozen`. If we try to access a `Disabled`,
-                        // then where it became `Frozen` (or `Active`) is the least of our concerns for now.
-                        (Active | Frozen, Disabled) => false,
+                        // then where it became `Frozen` (or `Active` or `Reserved`) is the least
+                        // of our concerns for now.
+                        (Reserved { conflicted: true, .. } | Active | Frozen, Disabled) => false,
+                        (Reserved { conflicted: true, .. }, Frozen) => false,
 
                         // `Active` and `Reserved` have all permissions, so a
                         // `ChildAccessForbidden(Reserved | Active)` can never exist.
-                        (_, Active) | (_, Reserved { .. }) =>
+                        (_, Active) | (_, Reserved { conflicted: false, .. }) =>
                             unreachable!("this permission cannot cause an error"),
-                        // No transition has `Reserved` as its `.to` unless it's a noop.
-                        (Reserved { .. }, _) => unreachable!("self is a noop transition"),
+                        // No transition has `Reserved(conflicted=false)` as its `.to` unless it's a noop.
+                        (Reserved { conflicted: false, .. }, _) =>
+                            unreachable!("self is a noop transition"),
                         // All transitions produced in normal executions (using `apply_access`)
                         // change permissions in the order `Reserved -> Active -> Frozen -> Disabled`.
                         // We assume that the error was triggered on the same location that
                         // the transition `self` applies to, so permissions found must be increasing
                         // in the order `self.from < self.to <= insufficient.inner`
-                        (Disabled, Frozen) =>
+                        (Active | Frozen | Disabled, Reserved { .. }) | (Disabled, Frozen) =>
                             unreachable!("permissions between self and err must be increasing"),
                     }
                 }
@@ -373,25 +385,34 @@ pub mod diagnostics {
                     // This eliminates transitions like `Reserved -> Active`
                     // when the error is a `Frozen -> Disabled`.
                     match (self.to, before_disabled.inner) {
-                        // We absolutely want to know where it was activated.
+                        // We absolutely want to know where it was activated/frozen/marked
+                        // conflicted.
                         (Active, Active) => true,
-                        // And knowing where it became Frozen is also important.
                         (Frozen, Frozen) => true,
+                        (Reserved { conflicted: true, .. }, Reserved { conflicted: true, .. }) =>
+                            true,
                         // If the error is a transition `Frozen -> Disabled`, then we don't really
                         // care whether before that was `Reserved -> Active -> Frozen` or
-                        // `Reserved -> Frozen` or even `Frozen` directly.
+                        // `Frozen` directly.
                         // The error will only show either
-                        // - created as Frozen, then Frozen -> Disabled is forbidden
-                        // - created as Reserved, later became Frozen, then Frozen -> Disabled is forbidden
-                        // In both cases the `Reserved -> Active` part is inexistant or irrelevant.
+                        // - created as Reserved { conflicted: false },
+                        //   then Reserved { .. } -> Disabled is forbidden
+                        // - created as Reserved { conflicted: false },
+                        //   then Active -> Disabled is forbidden
+                        // A potential `Reserved { conflicted: false }
+                        //   -> Reserved { conflicted: true }` is inexistant or irrelevant,
+                        // and so is the `Reserved { conflicted: false } -> Active`
                         (Active, Frozen) => false,
+                        (Reserved { conflicted: true, .. }, _) => false,
 
                         (_, Disabled) =>
                             unreachable!(
                                 "permission that results in Disabled should not itself be Disabled in the first place"
                             ),
-                        // No transition has `Reserved` as its `.to` unless it's a noop.
-                        (Reserved { .. }, _) => unreachable!("self is a noop transition"),
+                        // No transition has `Reserved { conflicted: false }` as its `.to`
+                        // unless it's a noop.
+                        (Reserved { conflicted: false, .. }, _) =>
+                            unreachable!("self is a noop transition"),
 
                         // Permissions only evolve in the order `Reserved -> Active -> Frozen -> Disabled`,
                         // so permissions found must be increasing in the order
@@ -418,6 +439,16 @@ pub mod diagnostics {
 }
 
 #[cfg(test)]
+impl Permission {
+    pub fn is_reserved_with_conflicted(&self, expected_conflicted: bool) -> bool {
+        match self.inner {
+            Reserved { conflicted, .. } => conflicted == expected_conflicted,
+            _ => false,
+        }
+    }
+}
+
+#[cfg(test)]
 mod propagation_optimization_checks {
     pub use super::*;
     use crate::borrow_tracker::tree_borrows::exhaustive::{precondition, Exhaustive};
@@ -425,9 +456,10 @@ mod propagation_optimization_checks {
     impl Exhaustive for PermissionPriv {
         fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
             Box::new(
-                vec![Active, Frozen, Disabled]
-                    .into_iter()
-                    .chain(bool::exhaustive().map(|ty_is_freeze| Reserved { ty_is_freeze })),
+                vec![Active, Frozen, Disabled].into_iter().chain(
+                    <[bool; 2]>::exhaustive()
+                        .map(|[ty_is_freeze, conflicted]| Reserved { ty_is_freeze, conflicted }),
+                ),
             )
         }
     }
diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs
index eb466f89a84..b63b0bdff12 100644
--- a/src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs
+++ b/src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs
@@ -282,6 +282,113 @@ enum ContinueTraversal {
     SkipChildren,
 }
 
+/// Stack of nodes left to explore in a tree traversal.
+struct TreeVisitorStack<NodeApp, ErrHandler> {
+    /// Identifier of the original access.
+    initial: UniIndex,
+    /// Function to apply to each tag.
+    f_propagate: NodeApp,
+    /// Handler to add the required context to diagnostics.
+    err_builder: ErrHandler,
+    /// Mutable state of the visit: the tags left to handle.
+    /// Every tag pushed should eventually be handled,
+    /// and the precise order is relevant for diagnostics.
+    stack: Vec<(UniIndex, AccessRelatedness)>,
+}
+
+impl<NodeApp, InnErr, OutErr, ErrHandler> TreeVisitorStack<NodeApp, ErrHandler>
+where
+    NodeApp: Fn(NodeAppArgs<'_>) -> Result<ContinueTraversal, InnErr>,
+    ErrHandler: Fn(ErrHandlerArgs<'_, InnErr>) -> OutErr,
+{
+    /// Apply the function to the current `tag`, and push its children
+    /// to the stack of future tags to visit.
+    fn exec_and_visit(
+        &mut self,
+        this: &mut TreeVisitor<'_>,
+        idx: UniIndex,
+        exclude: Option<UniIndex>,
+        rel_pos: AccessRelatedness,
+    ) -> Result<(), OutErr> {
+        // 1. apply the propagation function
+        let node = this.nodes.get_mut(idx).unwrap();
+        let recurse =
+            (self.f_propagate)(NodeAppArgs { node, perm: this.perms.entry(idx), rel_pos })
+                .map_err(|error_kind| {
+                    (self.err_builder)(ErrHandlerArgs {
+                        error_kind,
+                        conflicting_info: &this.nodes.get(idx).unwrap().debug_info,
+                        accessed_info: &this.nodes.get(self.initial).unwrap().debug_info,
+                    })
+                })?;
+        let node = this.nodes.get(idx).unwrap();
+        // 2. add the children to the stack for future traversal
+        if matches!(recurse, ContinueTraversal::Recurse) {
+            let general_child_rel = rel_pos.for_child();
+            for &child in node.children.iter() {
+                // Some child might be excluded from here and handled separately,
+                // e.g. the initially accessed tag.
+                if Some(child) != exclude {
+                    // We should still ensure that if we don't skip the initially accessed
+                    // it will receive the proper `AccessRelatedness`.
+                    let this_child_rel = if child == self.initial {
+                        AccessRelatedness::This
+                    } else {
+                        general_child_rel
+                    };
+                    self.stack.push((child, this_child_rel));
+                }
+            }
+        }
+        Ok(())
+    }
+
+    fn new(initial: UniIndex, f_propagate: NodeApp, err_builder: ErrHandler) -> Self {
+        Self { initial, f_propagate, err_builder, stack: Vec::new() }
+    }
+
+    /// Finish the exploration by applying `exec_and_visit` until
+    /// the stack is empty.
+    fn finish(&mut self, visitor: &mut TreeVisitor<'_>) -> Result<(), OutErr> {
+        while let Some((idx, rel_pos)) = self.stack.pop() {
+            self.exec_and_visit(visitor, idx, /* no children to exclude */ None, rel_pos)?;
+        }
+        Ok(())
+    }
+
+    /// Push all ancestors to the exploration stack in order of nearest ancestor
+    /// towards the top.
+    fn push_and_visit_strict_ancestors(
+        &mut self,
+        visitor: &mut TreeVisitor<'_>,
+    ) -> Result<(), OutErr> {
+        let mut path_ascend = Vec::new();
+        // First climb to the root while recording the path
+        let mut curr = self.initial;
+        while let Some(ancestor) = visitor.nodes.get(curr).unwrap().parent {
+            path_ascend.push((ancestor, curr));
+            curr = ancestor;
+        }
+        // Then descend:
+        // - execute f_propagate on each node
+        // - record children in visit
+        while let Some((ancestor, next_in_path)) = path_ascend.pop() {
+            // Explore ancestors in descending order.
+            // `next_in_path` is excluded from the recursion because it
+            // will be the `ancestor` of the next iteration.
+            // It also needs a different `AccessRelatedness` than the other
+            // children of `ancestor`.
+            self.exec_and_visit(
+                visitor,
+                ancestor,
+                Some(next_in_path),
+                AccessRelatedness::StrictChildAccess,
+            )?;
+        }
+        Ok(())
+    }
+}
+
 impl<'tree> TreeVisitor<'tree> {
     // Applies `f_propagate` to every vertex of the tree top-down in the following order: first
     // all ancestors of `start`, then `start` itself, then children of `start`, then the rest.
@@ -298,107 +405,40 @@ impl<'tree> TreeVisitor<'tree> {
         start: BorTag,
         f_propagate: impl Fn(NodeAppArgs<'_>) -> Result<ContinueTraversal, InnErr>,
         err_builder: impl Fn(ErrHandlerArgs<'_, InnErr>) -> OutErr,
-    ) -> Result<(), OutErr>
-where {
-        struct TreeVisitAux<NodeApp, ErrHandler> {
-            accessed_tag: UniIndex,
-            f_propagate: NodeApp,
-            err_builder: ErrHandler,
-            stack: Vec<(UniIndex, AccessRelatedness)>,
-        }
-        impl<NodeApp, InnErr, OutErr, ErrHandler> TreeVisitAux<NodeApp, ErrHandler>
-        where
-            NodeApp: Fn(NodeAppArgs<'_>) -> Result<ContinueTraversal, InnErr>,
-            ErrHandler: Fn(ErrHandlerArgs<'_, InnErr>) -> OutErr,
-        {
-            fn pop(&mut self) -> Option<(UniIndex, AccessRelatedness)> {
-                self.stack.pop()
-            }
-
-            /// Apply the function to the current `tag`, and push its children
-            /// to the stack of future tags to visit.
-            fn exec_and_visit(
-                &mut self,
-                this: &mut TreeVisitor<'_>,
-                tag: UniIndex,
-                exclude: Option<UniIndex>,
-                rel_pos: AccessRelatedness,
-            ) -> Result<(), OutErr> {
-                // 1. apply the propagation function
-                let node = this.nodes.get_mut(tag).unwrap();
-                let recurse =
-                    (self.f_propagate)(NodeAppArgs { node, perm: this.perms.entry(tag), rel_pos })
-                        .map_err(|error_kind| {
-                            (self.err_builder)(ErrHandlerArgs {
-                                error_kind,
-                                conflicting_info: &this.nodes.get(tag).unwrap().debug_info,
-                                accessed_info: &this
-                                    .nodes
-                                    .get(self.accessed_tag)
-                                    .unwrap()
-                                    .debug_info,
-                            })
-                        })?;
-                let node = this.nodes.get(tag).unwrap();
-                // 2. add the children to the stack for future traversal
-                if matches!(recurse, ContinueTraversal::Recurse) {
-                    let child_rel = rel_pos.for_child();
-                    for &child in node.children.iter() {
-                        // some child might be excluded from here and handled separately
-                        if Some(child) != exclude {
-                            self.stack.push((child, child_rel));
-                        }
-                    }
-                }
-                Ok(())
-            }
-        }
+    ) -> Result<(), OutErr> {
+        let start_idx = self.tag_mapping.get(&start).unwrap();
+        let mut stack = TreeVisitorStack::new(start_idx, f_propagate, err_builder);
+        stack.push_and_visit_strict_ancestors(&mut self)?;
+        // All (potentially zero) ancestors have been explored,
+        // it's time to explore the `start` tag.
+        stack.exec_and_visit(
+            &mut self,
+            start_idx,
+            /* no children to exclude */ None,
+            AccessRelatedness::This,
+        )?;
+        // Then finish with a normal DFS.
+        stack.finish(&mut self)
+    }
 
+    // Applies `f_propagate` to every non-child vertex of the tree (ancestors first).
+    //
+    // `f_propagate` should follow the following format: for a given `Node` it updates its
+    // `Permission` depending on the position relative to `start` (given by an
+    // `AccessRelatedness`).
+    // It outputs whether the tree traversal for this subree should continue or not.
+    fn traverse_nonchildren<InnErr, OutErr>(
+        mut self,
+        start: BorTag,
+        f_propagate: impl Fn(NodeAppArgs<'_>) -> Result<ContinueTraversal, InnErr>,
+        err_builder: impl Fn(ErrHandlerArgs<'_, InnErr>) -> OutErr,
+    ) -> Result<(), OutErr> {
         let start_idx = self.tag_mapping.get(&start).unwrap();
-        let mut stack =
-            TreeVisitAux { accessed_tag: start_idx, f_propagate, err_builder, stack: Vec::new() };
-        {
-            let mut path_ascend = Vec::new();
-            // First climb to the root while recording the path
-            let mut curr = start_idx;
-            while let Some(ancestor) = self.nodes.get(curr).unwrap().parent {
-                path_ascend.push((ancestor, curr));
-                curr = ancestor;
-            }
-            // Then descend:
-            // - execute f_propagate on each node
-            // - record children in visit
-            while let Some((ancestor, next_in_path)) = path_ascend.pop() {
-                // Explore ancestors in descending order.
-                // `next_in_path` is excluded from the recursion because it
-                // will be the `ancestor` of the next iteration.
-                // It also needs a different `AccessRelatedness` than the other
-                // children of `ancestor`.
-                stack.exec_and_visit(
-                    &mut self,
-                    ancestor,
-                    Some(next_in_path),
-                    AccessRelatedness::StrictChildAccess,
-                )?;
-            }
-        };
-        // All (potentially zero) ancestors have been explored, call f_propagate on start
-        stack.exec_and_visit(&mut self, start_idx, None, AccessRelatedness::This)?;
-        // up to this point we have never popped from `stack`, hence if the
-        // path to the root is `root = p(n) <- p(n-1)... <- p(1) <- p(0) = start`
-        // then now `stack` contains
-        // `[<children(p(n)) except p(n-1)> ... <children(p(1)) except p(0)> <children(p(0))>]`,
-        // all of which are for now unexplored.
-        // This is the starting point of a standard DFS which will thus
-        // explore all non-ancestors of `start` in the following order:
-        // - all descendants of `start`;
-        // - then the unexplored descendants of `parent(start)`;
-        // ...
-        // - until finally the unexplored descendants of `root`.
-        while let Some((tag, rel_pos)) = stack.pop() {
-            stack.exec_and_visit(&mut self, tag, None, rel_pos)?;
-        }
-        Ok(())
+        let mut stack = TreeVisitorStack::new(start_idx, f_propagate, err_builder);
+        stack.push_and_visit_strict_ancestors(&mut self)?;
+        // We *don't* visit the `start` tag, and we don't push its children.
+        // Only finish the DFS with the cousins.
+        stack.finish(&mut self)
     }
 }
 
@@ -482,7 +522,7 @@ impl<'tcx> Tree {
         self.perform_access(
             AccessKind::Write,
             tag,
-            access_range,
+            Some(access_range),
             global,
             span,
             diagnostics::AccessCause::Dealloc,
@@ -520,6 +560,11 @@ impl<'tcx> Tree {
     /// Map the per-node and per-location `LocationState::perform_access`
     /// to each location of `access_range`, on every tag of the allocation.
     ///
+    /// If `access_range` is `None`, this is interpreted as the special
+    /// access that is applied on protector release:
+    /// - the access will be applied only to initialized locations of the allocation,
+    /// - and it will not be visible to children.
+    ///
     /// `LocationState::perform_access` will take care of raising transition
     /// errors and updating the `initialized` status of each location,
     /// this traversal adds to that:
@@ -530,56 +575,105 @@ impl<'tcx> Tree {
         &mut self,
         access_kind: AccessKind,
         tag: BorTag,
-        access_range: AllocRange,
+        access_range: Option<AllocRange>,
         global: &GlobalState,
         span: Span,                             // diagnostics
         access_cause: diagnostics::AccessCause, // diagnostics
     ) -> InterpResult<'tcx> {
-        for (perms_range, perms) in self.rperms.iter_mut(access_range.start, access_range.size) {
-            TreeVisitor { nodes: &mut self.nodes, tag_mapping: &self.tag_mapping, perms }
-                .traverse_parents_this_children_others(
-                    tag,
-                    |args: NodeAppArgs<'_>| -> Result<ContinueTraversal, TransitionError> {
-                        let NodeAppArgs { node, mut perm, rel_pos } = args;
+        use std::ops::Range;
+        // Performs the per-node work:
+        // - insert the permission if it does not exist
+        // - perform the access
+        // - record the transition
+        // to which some optimizations are added:
+        // - skip the traversal of the children in some cases
+        // - do not record noop transitions
+        //
+        // `perms_range` is only for diagnostics (it is the range of
+        // the `RangeMap` on which we are currently working).
+        let node_app = |perms_range: Range<u64>,
+                        args: NodeAppArgs<'_>|
+         -> Result<ContinueTraversal, TransitionError> {
+            let NodeAppArgs { node, mut perm, rel_pos } = args;
+
+            let old_state = perm.or_insert(LocationState::new(node.default_initial_perm));
+
+            match old_state.skip_if_known_noop(access_kind, rel_pos) {
+                ContinueTraversal::SkipChildren => return Ok(ContinueTraversal::SkipChildren),
+                _ => {}
+            }
 
-                        let old_state =
-                            perm.or_insert_with(|| LocationState::new(node.default_initial_perm));
+            let protected = global.borrow().protected_tags.contains_key(&node.tag);
+            let transition = old_state.perform_access(access_kind, rel_pos, protected)?;
+
+            // Record the event as part of the history
+            if !transition.is_noop() {
+                node.debug_info.history.push(diagnostics::Event {
+                    transition,
+                    is_foreign: rel_pos.is_foreign(),
+                    access_cause,
+                    access_range,
+                    transition_range: perms_range.clone(),
+                    span,
+                });
+            }
+            Ok(ContinueTraversal::Recurse)
+        };
 
-                        match old_state.skip_if_known_noop(access_kind, rel_pos) {
-                            ContinueTraversal::SkipChildren =>
-                                return Ok(ContinueTraversal::SkipChildren),
-                            _ => {}
-                        }
+        // Error handler in case `node_app` goes wrong.
+        // Wraps the faulty transition in more context for diagnostics.
+        let err_handler = |perms_range: Range<u64>,
+                           args: ErrHandlerArgs<'_, TransitionError>|
+         -> InterpError<'tcx> {
+            let ErrHandlerArgs { error_kind, conflicting_info, accessed_info } = args;
+            TbError {
+                conflicting_info,
+                access_cause,
+                error_offset: perms_range.start,
+                error_kind,
+                accessed_info,
+            }
+            .build()
+        };
 
-                        let protected = global.borrow().protected_tags.contains_key(&node.tag);
-                        let transition =
-                            old_state.perform_access(access_kind, rel_pos, protected)?;
-
-                        // Record the event as part of the history
-                        if !transition.is_noop() {
-                            node.debug_info.history.push(diagnostics::Event {
-                                transition,
-                                is_foreign: rel_pos.is_foreign(),
-                                access_cause,
-                                access_range,
-                                transition_range: perms_range.clone(),
-                                span,
-                            });
-                        }
-                        Ok(ContinueTraversal::Recurse)
-                    },
-                    |args: ErrHandlerArgs<'_, TransitionError>| -> InterpError<'tcx> {
-                        let ErrHandlerArgs { error_kind, conflicting_info, accessed_info } = args;
-                        TbError {
-                            conflicting_info,
-                            access_cause,
-                            error_offset: perms_range.start,
-                            error_kind,
-                            accessed_info,
-                        }
-                        .build()
-                    },
-                )?;
+        if let Some(access_range) = access_range {
+            // Default branch: this is a "normal" access through a known range.
+            // We iterate over affected locations and traverse the tree for each of them.
+            for (perms_range, perms) in self.rperms.iter_mut(access_range.start, access_range.size)
+            {
+                TreeVisitor { nodes: &mut self.nodes, tag_mapping: &self.tag_mapping, perms }
+                    .traverse_parents_this_children_others(
+                        tag,
+                        |args| node_app(perms_range.clone(), args),
+                        |args| err_handler(perms_range.clone(), args),
+                    )?;
+            }
+        } else {
+            // This is a special access through the entire allocation.
+            // It actually only affects `initialized` locations, so we need
+            // to filter on those before initiating the traversal.
+            //
+            // In addition this implicit access should not be visible to children,
+            // thus the use of `traverse_nonchildren`.
+            // See the test case `returned_mut_is_usable` from
+            // `tests/pass/tree_borrows/tree-borrows.rs` for an example of
+            // why this is important.
+            for (perms_range, perms) in self.rperms.iter_mut_all() {
+                let idx = self.tag_mapping.get(&tag).unwrap();
+                // Only visit initialized permissions
+                if let Some(p) = perms.get(idx) && p.initialized {
+                    TreeVisitor {
+                        nodes: &mut self.nodes,
+                        tag_mapping: &self.tag_mapping,
+                        perms,
+                    }
+                    .traverse_nonchildren(
+                        tag,
+                        |args| node_app(perms_range.clone(), args),
+                        |args| err_handler(perms_range.clone(), args),
+                    )?;
+                }
+            }
         }
         Ok(())
     }
diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/tree/tests.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/tree/tests.rs
index 11c06d0b763..35f3b53afdb 100644
--- a/src/tools/miri/src/borrow_tracker/tree_borrows/tree/tests.rs
+++ b/src/tools/miri/src/borrow_tracker/tree_borrows/tree/tests.rs
@@ -302,6 +302,9 @@ mod spurious_read {
             Ok(Self { state, prot: self.prot })
         }
 
+        /// Remove the protector.
+        /// This does not perform the implicit read on function exit because
+        /// `LocStateProt` does not have enough context to apply its effect.
         fn end_protector(&self) -> Self {
             Self { prot: false, state: self.state }
         }
@@ -351,7 +354,8 @@ mod spurious_read {
         }
 
         /// Perform a read on the given pointer if its state is `initialized`.
-        /// Must be called just after reborrowing a pointer.
+        /// Must be called just after reborrowing a pointer, and just after
+        /// removing a protector.
         fn read_if_initialized(self, ptr: PtrSelector) -> Result<Self, ()> {
             let initialized = match ptr {
                 PtrSelector::X => self.x.state.initialized,
@@ -368,14 +372,16 @@ mod spurious_read {
             }
         }
 
+        /// Remove the protector of `x`, including the implicit read on function exit.
         fn end_protector_x(self) -> Result<Self, ()> {
             let x = self.x.end_protector();
-            Ok(Self { x, ..self })
+            Self { x, ..self }.read_if_initialized(PtrSelector::X)
         }
 
+        /// Remove the protector of `y`, including the implicit read on function exit.
         fn end_protector_y(self) -> Result<Self, ()> {
             let y = self.y.end_protector();
-            Ok(Self { y, ..self })
+            Self { y, ..self }.read_if_initialized(PtrSelector::Y)
         }
 
         fn retag_y(self, new_y: LocStateProt) -> Result<Self, ()> {
@@ -504,11 +510,9 @@ mod spurious_read {
     }
 
     #[test]
-    #[should_panic]
-    // This is why `Reserved -> Frozen` on foreign read for protected references
-    // prevents the insertion of spurious reads: the transition can cause UB in the target
-    // later down the line.
-    fn reserved_frozen_protected_distinguishable() {
+    // `Reserved(aliased=false)` and `Reserved(aliased=true)` are properly indistinguishable
+    // under the conditions where we want to insert a spurious read.
+    fn reserved_aliased_protected_indistinguishable() {
         let source = LocStateProtPair {
             xy_rel: RelPosXY::MutuallyForeign,
             x: LocStateProt {
@@ -522,8 +526,8 @@ mod spurious_read {
         };
         let acc = TestAccess { ptr: PtrSelector::X, kind: AccessKind::Read };
         let target = source.clone().perform_test_access(&acc).unwrap();
-        assert!(source.y.state.permission.is_reserved(None));
-        assert!(target.y.state.permission.is_frozen());
+        assert!(source.y.state.permission.is_reserved_with_conflicted(false));
+        assert!(target.y.state.permission.is_reserved_with_conflicted(true));
         assert!(!source.distinguishable::<(), ()>(&target))
     }
 
@@ -599,7 +603,6 @@ mod spurious_read {
     }
 
     #[test]
-    #[should_panic]
     /// For each of the patterns described above, execute it once
     /// as-is, and once with a spurious read inserted. Report any UB
     /// in the target but not in the source.
diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/unimap.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/unimap.rs
index 58af32385c5..d9cad9c8e0b 100644
--- a/src/tools/miri/src/borrow_tracker/tree_borrows/unimap.rs
+++ b/src/tools/miri/src/borrow_tracker/tree_borrows/unimap.rs
@@ -212,12 +212,9 @@ impl<'a, V> UniValMap<V> {
 
 impl<'a, V> UniEntry<'a, V> {
     /// Insert in the map and get the value.
-    pub fn or_insert_with<F>(&mut self, default: F) -> &mut V
-    where
-        F: FnOnce() -> V,
-    {
+    pub fn or_insert(&mut self, default: V) -> &mut V {
         if self.inner.is_none() {
-            *self.inner = Some(default());
+            *self.inner = Some(default);
         }
         self.inner.as_mut().unwrap()
     }
diff --git a/src/tools/miri/src/machine.rs b/src/tools/miri/src/machine.rs
index bd7ec88fc1c..930fa053d20 100644
--- a/src/tools/miri/src/machine.rs
+++ b/src/tools/miri/src/machine.rs
@@ -1387,8 +1387,34 @@ impl<'mir, 'tcx> Machine<'mir, 'tcx> for MiriMachine<'mir, 'tcx> {
     ) -> InterpResult<'tcx> {
         // We want this *before* the return value copy, because the return place itself is protected
         // until we do `end_call` here.
-        if let Some(borrow_tracker) = &ecx.machine.borrow_tracker {
-            borrow_tracker.borrow_mut().end_call(&frame.extra);
+        if let Some(global_borrow_tracker) = &ecx.machine.borrow_tracker {
+            // The body of this loop needs `global_borrow_tracker` immutably
+            // so we can't move this code inside the following `end_call`.
+            for (alloc_id, tag) in &frame
+                .extra
+                .borrow_tracker
+                .as_ref()
+                .expect("we should have borrow tracking data")
+                .protected_tags
+            {
+                // Just because the tag is protected doesn't guarantee that
+                // the allocation still exists (weak protectors allow deallocations)
+                // so we must check that the allocation exists.
+                // If it does exist, then we have the guarantee that the
+                // pointer is readable, and the implicit read access inserted
+                // will never cause UB on the pointer itself.
+                let (_, _, kind) = ecx.get_alloc_info(*alloc_id);
+                if matches!(kind, AllocKind::LiveData) {
+                    let alloc_extra = ecx.get_alloc_extra(*alloc_id).unwrap();
+                    let alloc_borrow_tracker = &alloc_extra.borrow_tracker.as_ref().unwrap();
+                    alloc_borrow_tracker.release_protector(
+                        &ecx.machine,
+                        global_borrow_tracker,
+                        *tag,
+                    )?;
+                }
+            }
+            global_borrow_tracker.borrow_mut().end_call(&frame.extra);
         }
         Ok(())
     }
diff --git a/src/tools/miri/tests/fail/both_borrows/aliasing_mut1.tree.stderr b/src/tools/miri/tests/fail/both_borrows/aliasing_mut1.tree.stderr
index 2a9b4d688a9..3271a04eae7 100644
--- a/src/tools/miri/tests/fail/both_borrows/aliasing_mut1.tree.stderr
+++ b/src/tools/miri/tests/fail/both_borrows/aliasing_mut1.tree.stderr
@@ -5,18 +5,18 @@ LL |     *x = 1;
    |     ^^^^^^ write access through <TAG> is forbidden
    |
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
-   = help: the accessed tag <TAG> has state Frozen which forbids this child write access
+   = help: the accessed tag <TAG> has state Reserved (conflicted) which forbids this child write access
 help: the accessed tag <TAG> was created here, in the initial state Reserved
   --> $DIR/aliasing_mut1.rs:LL:CC
    |
 LL | pub fn safe(x: &mut i32, y: &mut i32) {
    |             ^
-help: the accessed tag <TAG> later transitioned to Frozen due to a reborrow (acting as a foreign read access) at offsets [0x0..0x4]
+help: the accessed tag <TAG> later transitioned to Reserved (conflicted) due to a reborrow (acting as a foreign read access) at offsets [0x0..0x4]
   --> $DIR/aliasing_mut1.rs:LL:CC
    |
 LL | pub fn safe(x: &mut i32, y: &mut i32) {
    |                          ^
-   = help: this transition corresponds to a loss of write permissions
+   = help: this transition corresponds to a temporary loss of write permissions until function exit
    = note: BACKTRACE (of the first span):
    = note: inside `safe` at $DIR/aliasing_mut1.rs:LL:CC
 note: inside `main`
diff --git a/src/tools/miri/tests/fail/both_borrows/aliasing_mut2.tree.stderr b/src/tools/miri/tests/fail/both_borrows/aliasing_mut2.tree.stderr
index d4858975ef1..f2694b51ca4 100644
--- a/src/tools/miri/tests/fail/both_borrows/aliasing_mut2.tree.stderr
+++ b/src/tools/miri/tests/fail/both_borrows/aliasing_mut2.tree.stderr
@@ -5,18 +5,18 @@ LL |     *y = 2;
    |     ^^^^^^ write access through <TAG> is forbidden
    |
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
-   = help: the accessed tag <TAG> has state Frozen which forbids this child write access
+   = help: the accessed tag <TAG> has state Reserved (conflicted) which forbids this child write access
 help: the accessed tag <TAG> was created here, in the initial state Reserved
   --> $DIR/aliasing_mut2.rs:LL:CC
    |
 LL | pub fn safe(x: &i32, y: &mut i32) {
    |                      ^
-help: the accessed tag <TAG> later transitioned to Frozen due to a foreign read access at offsets [0x0..0x4]
+help: the accessed tag <TAG> later transitioned to Reserved (conflicted) due to a foreign read access at offsets [0x0..0x4]
   --> $DIR/aliasing_mut2.rs:LL:CC
    |
 LL |     let _v = *x;
    |              ^^
-   = help: this transition corresponds to a loss of write permissions
+   = help: this transition corresponds to a temporary loss of write permissions until function exit
    = note: BACKTRACE (of the first span):
    = note: inside `safe` at $DIR/aliasing_mut2.rs:LL:CC
 note: inside `main`
diff --git a/src/tools/miri/tests/fail/both_borrows/aliasing_mut3.tree.stderr b/src/tools/miri/tests/fail/both_borrows/aliasing_mut3.tree.stderr
index d1afca84a8b..595381c16ad 100644
--- a/src/tools/miri/tests/fail/both_borrows/aliasing_mut3.tree.stderr
+++ b/src/tools/miri/tests/fail/both_borrows/aliasing_mut3.tree.stderr
@@ -5,18 +5,18 @@ LL |     *x = 1;
    |     ^^^^^^ write access through <TAG> is forbidden
    |
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
-   = help: the accessed tag <TAG> has state Frozen which forbids this child write access
+   = help: the accessed tag <TAG> has state Reserved (conflicted) which forbids this child write access
 help: the accessed tag <TAG> was created here, in the initial state Reserved
   --> $DIR/aliasing_mut3.rs:LL:CC
    |
 LL | pub fn safe(x: &mut i32, y: &i32) {
    |             ^
-help: the accessed tag <TAG> later transitioned to Frozen due to a reborrow (acting as a foreign read access) at offsets [0x0..0x4]
+help: the accessed tag <TAG> later transitioned to Reserved (conflicted) due to a reborrow (acting as a foreign read access) at offsets [0x0..0x4]
   --> $DIR/aliasing_mut3.rs:LL:CC
    |
 LL | pub fn safe(x: &mut i32, y: &i32) {
    |                          ^
-   = help: this transition corresponds to a loss of write permissions
+   = help: this transition corresponds to a temporary loss of write permissions until function exit
    = note: BACKTRACE (of the first span):
    = note: inside `safe` at $DIR/aliasing_mut3.rs:LL:CC
 note: inside `main`
diff --git a/src/tools/miri/tests/fail/both_borrows/newtype_pair_retagging.tree.stderr b/src/tools/miri/tests/fail/both_borrows/newtype_pair_retagging.tree.stderr
index 19a05ec5dd3..456af0f1eac 100644
--- a/src/tools/miri/tests/fail/both_borrows/newtype_pair_retagging.tree.stderr
+++ b/src/tools/miri/tests/fail/both_borrows/newtype_pair_retagging.tree.stderr
@@ -6,7 +6,7 @@ LL |     unsafe { __rust_dealloc(ptr, layout.size(), layout.align()) }
    |
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
    = help: the accessed tag <TAG> is foreign to the protected tag <TAG> (i.e., it is not a child)
-   = help: this deallocation (acting as a foreign write access) would cause the protected tag <TAG> (currently Frozen) to become Disabled
+   = help: this deallocation (acting as a foreign write access) would cause the protected tag <TAG> (currently Reserved (conflicted)) to become Disabled
    = help: protected tags must never be Disabled
 help: the accessed tag <TAG> was created here
   --> $DIR/newtype_pair_retagging.rs:LL:CC
@@ -18,12 +18,12 @@ help: the protected tag <TAG> was created here, in the initial state Reserved
    |
 LL | fn dealloc_while_running(_n: Newtype<'_>, dealloc: impl FnOnce()) {
    |                          ^^
-help: the protected tag <TAG> later transitioned to Frozen due to a reborrow (acting as a foreign read access) at offsets [0x0..0x4]
+help: the protected tag <TAG> later transitioned to Reserved (conflicted) due to a reborrow (acting as a foreign read access) at offsets [0x0..0x4]
   --> $DIR/newtype_pair_retagging.rs:LL:CC
    |
 LL |             || drop(Box::from_raw(ptr)),
    |                     ^^^^^^^^^^^^^^^^^^
-   = help: this transition corresponds to a loss of write permissions
+   = help: this transition corresponds to a temporary loss of write permissions until function exit
    = note: BACKTRACE (of the first span):
    = note: inside `std::alloc::dealloc` at RUSTLIB/alloc/src/alloc.rs:LL:CC
    = note: inside `<std::alloc::Global as std::alloc::Allocator>::deallocate` at RUSTLIB/alloc/src/alloc.rs:LL:CC
diff --git a/src/tools/miri/tests/fail/both_borrows/newtype_retagging.tree.stderr b/src/tools/miri/tests/fail/both_borrows/newtype_retagging.tree.stderr
index 6364c51122a..d21ec9eddc2 100644
--- a/src/tools/miri/tests/fail/both_borrows/newtype_retagging.tree.stderr
+++ b/src/tools/miri/tests/fail/both_borrows/newtype_retagging.tree.stderr
@@ -6,7 +6,7 @@ LL |     unsafe { __rust_dealloc(ptr, layout.size(), layout.align()) }
    |
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
    = help: the accessed tag <TAG> is foreign to the protected tag <TAG> (i.e., it is not a child)
-   = help: this deallocation (acting as a foreign write access) would cause the protected tag <TAG> (currently Frozen) to become Disabled
+   = help: this deallocation (acting as a foreign write access) would cause the protected tag <TAG> (currently Reserved (conflicted)) to become Disabled
    = help: protected tags must never be Disabled
 help: the accessed tag <TAG> was created here
   --> $DIR/newtype_retagging.rs:LL:CC
@@ -18,12 +18,12 @@ help: the protected tag <TAG> was created here, in the initial state Reserved
    |
 LL | fn dealloc_while_running(_n: Newtype<'_>, dealloc: impl FnOnce()) {
    |                          ^^
-help: the protected tag <TAG> later transitioned to Frozen due to a reborrow (acting as a foreign read access) at offsets [0x0..0x4]
+help: the protected tag <TAG> later transitioned to Reserved (conflicted) due to a reborrow (acting as a foreign read access) at offsets [0x0..0x4]
   --> $DIR/newtype_retagging.rs:LL:CC
    |
 LL |             || drop(Box::from_raw(ptr)),
    |                     ^^^^^^^^^^^^^^^^^^
-   = help: this transition corresponds to a loss of write permissions
+   = help: this transition corresponds to a temporary loss of write permissions until function exit
    = note: BACKTRACE (of the first span):
    = note: inside `std::alloc::dealloc` at RUSTLIB/alloc/src/alloc.rs:LL:CC
    = note: inside `<std::alloc::Global as std::alloc::Allocator>::deallocate` at RUSTLIB/alloc/src/alloc.rs:LL:CC
diff --git a/src/tools/miri/tests/fail/both_borrows/retag_data_race_protected_read.rs b/src/tools/miri/tests/fail/both_borrows/retag_data_race_protected_read.rs
deleted file mode 100644
index f192e76de13..00000000000
--- a/src/tools/miri/tests/fail/both_borrows/retag_data_race_protected_read.rs
+++ /dev/null
@@ -1,29 +0,0 @@
-//@revisions: stack tree
-//@compile-flags: -Zmiri-preemption-rate=0
-//@[tree]compile-flags: -Zmiri-tree-borrows
-use std::thread;
-
-#[derive(Copy, Clone)]
-struct SendPtr(*mut i32);
-unsafe impl Send for SendPtr {}
-
-fn main() {
-    let mut mem = 0;
-    let ptr = SendPtr(&mut mem as *mut _);
-
-    let t = thread::spawn(move || {
-        let ptr = ptr;
-        // We do a protected 2phase retag (but no write!) in this thread.
-        fn retag(_x: &mut i32) {} //~[tree]ERROR: Data race detected between (1) Read on thread `main` and (2) Write on thread `<unnamed>`
-        retag(unsafe { &mut *ptr.0 }); //~[stack]ERROR: Data race detected between (1) Read on thread `main` and (2) Write on thread `<unnamed>`
-    });
-
-    // We do a read in the main thread.
-    unsafe { ptr.0.read() };
-
-    // These two operations do not commute -- if the read happens after the retag, the retagged pointer
-    // gets frozen! So we want this to be considered UB so that we can still freely move the read around
-    // in this thread without worrying about reordering with retags in other threads.
-
-    t.join().unwrap();
-}
diff --git a/src/tools/miri/tests/fail/both_borrows/retag_data_race_protected_read.tree.stderr b/src/tools/miri/tests/fail/both_borrows/retag_data_race_protected_read.tree.stderr
deleted file mode 100644
index 173acf4b96c..00000000000
--- a/src/tools/miri/tests/fail/both_borrows/retag_data_race_protected_read.tree.stderr
+++ /dev/null
@@ -1,25 +0,0 @@
-error: Undefined Behavior: Data race detected between (1) Read on thread `main` and (2) Write on thread `<unnamed>` at ALLOC. (2) just happened here
-  --> $DIR/retag_data_race_protected_read.rs:LL:CC
-   |
-LL |         fn retag(_x: &mut i32) {}
-   |                  ^^ Data race detected between (1) Read on thread `main` and (2) Write on thread `<unnamed>` 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: 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):
-   = note: inside `main::{closure#0}::retag` at $DIR/retag_data_race_protected_read.rs:LL:CC
-note: inside closure
-  --> $DIR/retag_data_race_protected_read.rs:LL:CC
-   |
-LL | ...   retag(unsafe { &mut *ptr.0 });
-   |       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
-
-error: aborting due to previous error
-
diff --git 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
new file mode 100644
index 00000000000..670fe9858ed
--- /dev/null
+++ b/src/tools/miri/tests/fail/stacked_borrows/retag_data_race_protected_read.rs
@@ -0,0 +1,30 @@
+//@compile-flags: -Zmiri-preemption-rate=0
+use std::thread;
+
+#[derive(Copy, Clone)]
+struct SendPtr(*mut i32);
+unsafe impl Send for SendPtr {}
+
+fn main() {
+    let mut mem = 0;
+    let ptr = SendPtr(&mut mem as *mut _);
+
+    let t = thread::spawn(move || {
+        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) Read on thread `main` and (2) Write on thread `<unnamed>`
+    });
+
+    // We do a read in the main thread.
+    unsafe { ptr.0.read() };
+
+    // These two operations do not commute!
+    // - In Stacked Borrows, if the read happens after the retag it will `Disable` the pointer.
+    // - In Tree Borrows, if the read happens after the retag, the retagged pointer gets frozen!
+    // Ideally we would want this to be considered UB so that we can still freely move the read around
+    // in this thread without worrying about reordering with retags in other threads,
+    // but in Tree Borrows we have found worse issues that occur if we make this a data race.
+
+    t.join().unwrap();
+}
diff --git a/src/tools/miri/tests/fail/both_borrows/retag_data_race_protected_read.stack.stderr b/src/tools/miri/tests/fail/stacked_borrows/retag_data_race_protected_read.stderr
index 10fb1dece2a..10fb1dece2a 100644
--- a/src/tools/miri/tests/fail/both_borrows/retag_data_race_protected_read.stack.stderr
+++ b/src/tools/miri/tests/fail/stacked_borrows/retag_data_race_protected_read.stderr
diff --git a/src/tools/miri/tests/fail/tree_borrows/reserved/cell-protected-write.stderr b/src/tools/miri/tests/fail/tree_borrows/reserved/cell-protected-write.stderr
index 998ab956e1a..fc92770ed16 100644
--- a/src/tools/miri/tests/fail/tree_borrows/reserved/cell-protected-write.stderr
+++ b/src/tools/miri/tests/fail/tree_borrows/reserved/cell-protected-write.stderr
@@ -1,12 +1,12 @@
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  1
-| Act|    └─┬──<TAG=root of the allocation>
-| Re*|      └─┬──<TAG=base>
-| Re*|        ├─┬──<TAG=x>
-| Re*|        │ └─┬──<TAG=caller:x>
-| Re*|        │   └────<TAG=callee:x> Strongly protected
-| Re*|        └────<TAG=y, callee:y, caller:y>
+0..   1
+| Act |    └─┬──<TAG=root of the allocation>
+| RsM |      └─┬──<TAG=base>
+| RsM |        ├─┬──<TAG=x>
+| RsM |        │ └─┬──<TAG=caller:x>
+| RsM |        │   └────<TAG=callee:x> Strongly protected
+| RsM |        └────<TAG=y, callee:y, caller:y>
 ──────────────────────────────────────────────────
 error: Undefined Behavior: write access through <TAG> (y, callee:y, caller:y) is forbidden
   --> $DIR/cell-protected-write.rs:LL:CC
diff --git a/src/tools/miri/tests/fail/tree_borrows/reserved/int-protected-write.stderr b/src/tools/miri/tests/fail/tree_borrows/reserved/int-protected-write.stderr
index f7e9fb9e3c3..4b4b8f24a68 100644
--- a/src/tools/miri/tests/fail/tree_borrows/reserved/int-protected-write.stderr
+++ b/src/tools/miri/tests/fail/tree_borrows/reserved/int-protected-write.stderr
@@ -1,12 +1,12 @@
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  1
-| Act|    └─┬──<TAG=root of the allocation>
-| Res|      └─┬──<TAG=n>
-| Res|        ├─┬──<TAG=x>
-| Res|        │ └─┬──<TAG=caller:x>
-| Res|        │   └────<TAG=callee:x> Strongly protected
-| Res|        └────<TAG=y, callee:y, caller:y>
+0..   1
+| Act |    └─┬──<TAG=root of the allocation>
+| Rs  |      └─┬──<TAG=n>
+| Rs  |        ├─┬──<TAG=x>
+| Rs  |        │ └─┬──<TAG=caller:x>
+| Rs  |        │   └────<TAG=callee:x> Strongly protected
+| Rs  |        └────<TAG=y, callee:y, caller:y>
 ──────────────────────────────────────────────────
 error: Undefined Behavior: write access through <TAG> (y, callee:y, caller:y) is forbidden
   --> $DIR/int-protected-write.rs:LL:CC
diff --git a/src/tools/miri/tests/fail/tree_borrows/spurious_read.rs b/src/tools/miri/tests/fail/tree_borrows/spurious_read.rs
new file mode 100644
index 00000000000..3f39dcb4b76
--- /dev/null
+++ b/src/tools/miri/tests/fail/tree_borrows/spurious_read.rs
@@ -0,0 +1,117 @@
+// We ensure a deterministic execution.
+// Note that we are *also* using barriers: the barriers enforce the
+// specific interleaving of operations that we want, but only the preemption
+// rate guarantees that the error message is also deterministic.
+//@compile-flags: -Zmiri-preemption-rate=0
+//@compile-flags: -Zmiri-tree-borrows
+
+use std::sync::{Arc, Barrier};
+use std::thread;
+
+// A way to send raw pointers across threads.
+// Note that when using this in closures will require explicit copying
+// `let ptr = ptr;` to force the borrow checker to copy the `Send` wrapper
+// instead of just copying the inner `!Send` field.
+#[derive(Copy, Clone)]
+struct SendPtr(*mut u8);
+unsafe impl Send for SendPtr {}
+
+fn main() {
+    retagx_retagy_retx_writey_rety();
+}
+
+// We're going to enforce a specific interleaving of two
+// threads, we use this macro in an effort to make it feasible
+// to check in the output that the execution is properly synchronized.
+//
+// Provide `synchronized!(thread, msg)` where thread is
+// a `(thread_id: usize, barrier: Arc<Barrier>)`, and `msg` the message
+// to be displayed when the thread reaches this point in the execution.
+macro_rules! synchronized {
+    ($thread:expr, $msg:expr) => {{
+        let (thread_id, barrier) = &$thread;
+        eprintln!("Thread {} executing: {}", thread_id, $msg);
+        barrier.wait();
+    }};
+}
+
+// Interleaving:
+//   retag x (protect)
+//   retag y (protect)
+//   spurious read x (target only, which we are *not* executing)
+//   ret x
+//   write y
+//   ret y
+//
+// This is an interleaving that will never *not* have UB in the target
+// (`noalias` violation on `y`).
+// For the spurious read to be allowed, we need to ensure there *is* UB
+// in the source (i.e., without the spurious read).
+//
+// The interleaving differs from the one in `tests/pass/tree_borrows/spurious_read.rs` only
+// in that it has the `write y` while `y` is still protected.
+// When the write occurs after protection ends, both source and target are fine
+// (checked by the `pass` test); when the write occurs during protection, both source
+// and target are UB (checked by this test).
+fn retagx_retagy_retx_writey_rety() {
+    let mut data = 0u8;
+    let ptr = SendPtr(std::ptr::addr_of_mut!(data));
+    let barrier = Arc::new(Barrier::new(2));
+    let bx = Arc::clone(&barrier);
+    let by = Arc::clone(&barrier);
+
+    // This thread only needs to
+    // - retag `x` protected
+    // - do a read through `x`
+    // - remove `x`'s protector
+    // Most of the complexity here is synchronization.
+    let thread_x = thread::spawn(move || {
+        let b = (1, bx);
+        synchronized!(b, "start");
+        let ptr = ptr;
+        synchronized!(b, "retag x (&mut, protect)");
+        fn as_mut(x: &mut u8, b: (usize, Arc<Barrier>)) -> *mut u8 {
+            synchronized!(b, "retag y (&mut, protect)");
+            synchronized!(b, "location where spurious read of x would happen in the target");
+            // This is ensuring taht we have UB *without* the spurious read,
+            // so we don't read here.
+            synchronized!(b, "ret x");
+            synchronized!(b, "write y");
+            let x = x as *mut u8;
+            x
+        }
+        let _x = as_mut(unsafe { &mut *ptr.0 }, b.clone());
+        synchronized!(b, "ret y");
+        synchronized!(b, "end");
+    });
+
+    // This thread's job is to
+    // - retag `y` protected
+    // - (wait for the other thread to return so that there is no foreign protector when we write)
+    // - attempt a write through `y`.
+    // - (UB should have occured by now, but the next step would be to
+    //    remove `y`'s protector)
+    let thread_y = thread::spawn(move || {
+        let b = (2, by);
+        synchronized!(b, "start");
+        let ptr = ptr;
+        synchronized!(b, "retag x (&mut, protect)");
+        synchronized!(b, "retag y (&mut, protect)");
+        fn as_mut(y: &mut u8, b: (usize, Arc<Barrier>)) -> *mut u8 {
+            synchronized!(b, "location where spurious read of x would happen in the target");
+            synchronized!(b, "ret x");
+            let y = y as *mut u8;
+            synchronized!(b, "write y");
+            unsafe {
+                *y = 2; //~ERROR: /write access through .* is forbidden/
+            }
+            synchronized!(b, "ret y");
+            y
+        }
+        let _y = as_mut(unsafe { &mut *ptr.0 }, b.clone());
+        synchronized!(b, "end");
+    });
+
+    thread_x.join().unwrap();
+    thread_y.join().unwrap();
+}
diff --git a/src/tools/miri/tests/fail/tree_borrows/spurious_read.stderr b/src/tools/miri/tests/fail/tree_borrows/spurious_read.stderr
new file mode 100644
index 00000000000..99ffb849339
--- /dev/null
+++ b/src/tools/miri/tests/fail/tree_borrows/spurious_read.stderr
@@ -0,0 +1,44 @@
+Thread 1 executing: start
+Thread 2 executing: start
+Thread 2 executing: retag x (&mut, protect)
+Thread 1 executing: retag x (&mut, protect)
+Thread 1 executing: retag y (&mut, protect)
+Thread 2 executing: retag y (&mut, protect)
+Thread 2 executing: location where spurious read of x would happen in the target
+Thread 1 executing: location where spurious read of x would happen in the target
+Thread 1 executing: ret x
+Thread 2 executing: ret x
+Thread 2 executing: write y
+Thread 1 executing: write y
+Thread 1 executing: ret y
+error: Undefined Behavior: write access through <TAG> is forbidden
+  --> $DIR/spurious_read.rs:LL:CC
+   |
+LL |                 *y = 2;
+   |                 ^^^^^^ write access through <TAG> is forbidden
+   |
+   = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
+   = help: the accessed tag <TAG> has state Reserved (conflicted) which forbids this child write access
+help: the accessed tag <TAG> was created here, in the initial state Reserved
+  --> $DIR/spurious_read.rs:LL:CC
+   |
+LL |         fn as_mut(y: &mut u8, b: (usize, Arc<Barrier>)) -> *mut u8 {
+   |                   ^
+help: the accessed tag <TAG> later transitioned to Reserved (conflicted) due to a protector release (acting as a foreign read access) on every location previously accessed by this tag
+  --> $DIR/spurious_read.rs:LL:CC
+   |
+LL |         }
+   |          ^
+   = help: this transition corresponds to a temporary loss of write permissions until function exit
+   = note: BACKTRACE (of the first span):
+   = note: inside `retagx_retagy_retx_writey_rety::{closure#1}::as_mut` at $DIR/spurious_read.rs:LL:CC
+note: inside closure
+  --> $DIR/spurious_read.rs:LL:CC
+   |
+LL |         let _y = as_mut(unsafe { &mut *ptr.0 }, b.clone());
+   |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
+
+error: aborting due to previous error
+
diff --git a/src/tools/miri/tests/pass/tree_borrows/cell-alternate-writes.stderr b/src/tools/miri/tests/pass/tree_borrows/cell-alternate-writes.stderr
index f464e0b4f49..57caa09c888 100644
--- a/src/tools/miri/tests/pass/tree_borrows/cell-alternate-writes.stderr
+++ b/src/tools/miri/tests/pass/tree_borrows/cell-alternate-writes.stderr
@@ -1,12 +1,12 @@
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  1
-| Act|    └─┬──<TAG=root of the allocation>
-| Re*|      └────<TAG=data, x, y>
+0..   1
+| Act |    └─┬──<TAG=root of the allocation>
+| RsM |      └────<TAG=data, x, y>
 ──────────────────────────────────────────────────
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  1
-| Act|    └─┬──<TAG=root of the allocation>
-| Act|      └────<TAG=data, x, y>
+0..   1
+| Act |    └─┬──<TAG=root of the allocation>
+| Act |      └────<TAG=data, x, y>
 ──────────────────────────────────────────────────
diff --git a/src/tools/miri/tests/pass/tree_borrows/end-of-protector.stderr b/src/tools/miri/tests/pass/tree_borrows/end-of-protector.stderr
index 265f6dfc9c8..69b8a17dc5e 100644
--- a/src/tools/miri/tests/pass/tree_borrows/end-of-protector.stderr
+++ b/src/tools/miri/tests/pass/tree_borrows/end-of-protector.stderr
@@ -1,36 +1,36 @@
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  1
-| Act|    └─┬──<TAG=root of the allocation>
-| Res|      └─┬──<TAG=data>
-| Res|        └────<TAG=x>
+0..   1
+| Act |    └─┬──<TAG=root of the allocation>
+| Rs  |      └─┬──<TAG=data>
+| Rs  |        └────<TAG=x>
 ──────────────────────────────────────────────────
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  1
-| Act|    └─┬──<TAG=root of the allocation>
-| Res|      └─┬──<TAG=data>
-| Res|        └─┬──<TAG=x>
-| Res|          └─┬──<TAG=caller:x>
-| Res|            └────<TAG=callee:x> Strongly protected
+0..   1
+| Act |    └─┬──<TAG=root of the allocation>
+| Rs  |      └─┬──<TAG=data>
+| Rs  |        └─┬──<TAG=x>
+| Rs  |          └─┬──<TAG=caller:x>
+| Rs  |            └────<TAG=callee:x> Strongly protected
 ──────────────────────────────────────────────────
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  1
-| Act|    └─┬──<TAG=root of the allocation>
-| Res|      └─┬──<TAG=data>
-| Res|        ├─┬──<TAG=x>
-| Res|        │ └─┬──<TAG=caller:x>
-| Res|        │   └────<TAG=callee:x>
-| Res|        └────<TAG=y>
+0..   1
+| Act |    └─┬──<TAG=root of the allocation>
+| Rs  |      └─┬──<TAG=data>
+| Rs  |        ├─┬──<TAG=x>
+| Rs  |        │ └─┬──<TAG=caller:x>
+| Rs  |        │   └────<TAG=callee:x>
+| Rs  |        └────<TAG=y>
 ──────────────────────────────────────────────────
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  1
-| Act|    └─┬──<TAG=root of the allocation>
-| Act|      └─┬──<TAG=data>
-| Dis|        ├─┬──<TAG=x>
-| Dis|        │ └─┬──<TAG=caller:x>
-| Dis|        │   └────<TAG=callee:x>
-| Act|        └────<TAG=y>
+0..   1
+| Act |    └─┬──<TAG=root of the allocation>
+| Act |      └─┬──<TAG=data>
+| Dis |        ├─┬──<TAG=x>
+| Dis |        │ └─┬──<TAG=caller:x>
+| Dis |        │   └────<TAG=callee:x>
+| Act |        └────<TAG=y>
 ──────────────────────────────────────────────────
diff --git a/src/tools/miri/tests/pass/tree_borrows/formatting.stderr b/src/tools/miri/tests/pass/tree_borrows/formatting.stderr
index 673dae6210d..235ab68fe01 100644
--- a/src/tools/miri/tests/pass/tree_borrows/formatting.stderr
+++ b/src/tools/miri/tests/pass/tree_borrows/formatting.stderr
@@ -1,31 +1,31 @@
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  1..  2.. 10.. 11..100..101..1000..1001..1024
-| Act| Act| Act| Act| Act| Act|  Act|  Act|  Act|    └─┬──<TAG=root of the allocation>
-| Res| Act| Res| Act| Res| Act|  Res|  Act|  Res|      └─┬──<TAG=data, data>
-|----| Act|----|?Dis|----|?Dis| ----| ?Dis| ----|        ├────<TAG=data[1]>
-|----|----|----| Act|----|?Dis| ----| ?Dis| ----|        ├────<TAG=data[10]>
-|----|----|----|----|----| Frz| ----| ?Dis| ----|        ├────<TAG=data[100]>
-|----|----|----|----|----|----| ----|  Act| ----|        └────<TAG=data[1000]>
+0..   1..   2..  10..  11.. 100.. 101..1000..1001..1024
+| Act | Act | Act | Act | Act | Act | Act | Act | Act |    └─┬──<TAG=root of the allocation>
+| Rs  | Act | Rs  | Act | Rs  | Act | Rs  | Act | Rs  |      └─┬──<TAG=data, data>
+|-----| Act |-----|?Dis |-----|?Dis |-----|?Dis |-----|        ├────<TAG=data[1]>
+|-----|-----|-----| Act |-----|?Dis |-----|?Dis |-----|        ├────<TAG=data[10]>
+|-----|-----|-----|-----|-----| Frz |-----|?Dis |-----|        ├────<TAG=data[100]>
+|-----|-----|-----|-----|-----|-----|-----| Act |-----|        └────<TAG=data[1000]>
 ──────────────────────────────────────────────────
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  1
-| Act|    └─┬──<TAG=root of the allocation>
-| Frz|      └─┬──<TAG=x>
-| Frz|        ├─┬──<TAG=xa>
-| Frz|        │ ├────<TAG=xaa>
-| Frz|        │ └────<TAG=xab>
-| Frz|        ├─┬──<TAG=xb>
-| Frz|        │ └─┬──<TAG=xba>
-| Frz|        │   └─┬──<TAG=xbaa>
-| Frz|        │     └─┬──<TAG=xbaaa>
-| Frz|        │       └────<TAG=xbaaaa>
-| Frz|        └─┬──<TAG=xc>
-| Frz|          ├─┬──<TAG=xca>
-| Frz|          │ ├────<TAG=xcaa>
-| Frz|          │ └────<TAG=xcab>
-| Frz|          └─┬──<TAG=xcb>
-| Frz|            ├────<TAG=xcba>
-| Frz|            └────<TAG=xcbb>
+0..   1
+| Act |    └─┬──<TAG=root of the allocation>
+| Frz |      └─┬──<TAG=x>
+| Frz |        ├─┬──<TAG=xa>
+| Frz |        │ ├────<TAG=xaa>
+| Frz |        │ └────<TAG=xab>
+| Frz |        ├─┬──<TAG=xb>
+| Frz |        │ └─┬──<TAG=xba>
+| Frz |        │   └─┬──<TAG=xbaa>
+| Frz |        │     └─┬──<TAG=xbaaa>
+| Frz |        │       └────<TAG=xbaaaa>
+| Frz |        └─┬──<TAG=xc>
+| Frz |          ├─┬──<TAG=xca>
+| Frz |          │ ├────<TAG=xcaa>
+| Frz |          │ └────<TAG=xcab>
+| Frz |          └─┬──<TAG=xcb>
+| Frz |            ├────<TAG=xcba>
+| Frz |            └────<TAG=xcbb>
 ──────────────────────────────────────────────────
diff --git a/src/tools/miri/tests/pass/tree_borrows/read_retag_no_race.rs b/src/tools/miri/tests/pass/tree_borrows/read_retag_no_race.rs
new file mode 100644
index 00000000000..d9897a1033f
--- /dev/null
+++ b/src/tools/miri/tests/pass/tree_borrows/read_retag_no_race.rs
@@ -0,0 +1,114 @@
+//@compile-flags: -Zmiri-tree-borrows
+// This test relies on a specific interleaving that cannot be enforced
+// with just barriers. We must remove preemption so that the execution and the
+// error messages are deterministic.
+//@compile-flags: -Zmiri-preemption-rate=0
+use std::ptr::addr_of_mut;
+use std::sync::{Arc, Barrier};
+use std::thread;
+
+#[derive(Copy, Clone)]
+struct SendPtr(*mut u8);
+
+unsafe impl Send for SendPtr {}
+
+// This test features the problematic pattern
+//
+// read x     || retag y (&mut, protect)
+//        -- sync --
+//            || write y
+//
+// In which
+// - one interleaving (`1:read; 2:retag; 2:write`) does not have UB if retags
+//   count only as reads for the data race model,
+// - the other interleaving (`2:retag; 1:read; 2:write`) has UB (`noalias` violation).
+//
+// The interleaving executed here is the one that does not have UB,
+// i.e.
+//      1:read x
+//      2:retag y
+//      2:write y
+//
+// Tree Borrows considers that the read of `x` cannot be in conflict
+// with `y` because `y` did not even exist yet when `x` was accessed.
+//
+// As long as we are not emitting any writes for the data race model
+// upon retags of mutable references, it should not have any issue with
+// this code either.
+// We do not want to emit a write for the data race model, because
+// although there is race-like behavior going on in this pattern
+// (where some but not all interleavings contain UB), making this an actual
+// data race has the confusing consequence of one single access being treated
+// as being of different `AccessKind`s by different parts of Miri
+// (a retag would be always a read for the aliasing model, and sometimes a write
+// for the data race model).
+
+// The other interleaving is a subsequence of `tests/fail/tree_borrows/spurious_read.rs`
+// which asserts that
+//      2:retag y
+//      1:read x
+//      2:write y
+// is UB.
+
+type IdxBarrier = (usize, Arc<Barrier>);
+// We're going to enforce a specific interleaving of two
+// threads, we use this macro in an effort to make it feasible
+// to check in the output that the execution is properly synchronized.
+//
+// Provide `synchronized!(thread, msg)` where thread is
+// a `(thread_id: usize, barrier: Arc<Barrier>)`, and `msg` the message
+// to be displayed when the thread reaches this point in the execution.
+macro_rules! synchronized {
+    ($thread:expr, $msg:expr) => {{
+        let (thread_id, barrier) = &$thread;
+        eprintln!("Thread {} executing: {}", thread_id, $msg);
+        barrier.wait();
+    }};
+}
+
+fn thread_1(x: SendPtr, barrier: IdxBarrier) {
+    let x = unsafe { &mut *x.0 };
+    synchronized!(barrier, "spawn");
+
+    synchronized!(barrier, "read x || retag y");
+    // This is the interleaving without UB: by the time
+    // the other thread starts retagging, this thread
+    // has already finished all its work using `y`.
+    let _v = *x;
+    synchronized!(barrier, "write y");
+    synchronized!(barrier, "exit");
+}
+
+fn thread_2(y: SendPtr, barrier: IdxBarrier) {
+    let y = unsafe { &mut *y.0 };
+    synchronized!(barrier, "spawn");
+
+    fn write(y: &mut u8, v: u8, barrier: &IdxBarrier) {
+        synchronized!(barrier, "write y");
+        *y = v;
+    }
+    synchronized!(barrier, "read x || retag y");
+    // We don't use a barrier here so that *if* the retag counted as a write
+    // for the data race model, then it would be UB.
+    // We still want to make sure that the other thread goes first as per the
+    // interleaving that we are testing, so we use `yield_now + preemption-rate=0`
+    // which has the effect of forcing a specific interleaving while still
+    // not counting as "synchronization" from the point of view of the data
+    // race model.
+    thread::yield_now();
+    write(&mut *y, 42, &barrier);
+    synchronized!(barrier, "exit");
+}
+
+fn main() {
+    let mut data = 0u8;
+    let p = SendPtr(addr_of_mut!(data));
+    let barrier = Arc::new(Barrier::new(2));
+    let b1 = (1, Arc::clone(&barrier));
+    let b2 = (2, Arc::clone(&barrier));
+
+    let h1 = thread::spawn(move || thread_1(p, b1));
+    let h2 = thread::spawn(move || thread_2(p, b2));
+    h1.join().unwrap();
+    h2.join().unwrap();
+}
diff --git a/src/tools/miri/tests/pass/tree_borrows/read_retag_no_race.stderr b/src/tools/miri/tests/pass/tree_borrows/read_retag_no_race.stderr
new file mode 100644
index 00000000000..f0903008511
--- /dev/null
+++ b/src/tools/miri/tests/pass/tree_borrows/read_retag_no_race.stderr
@@ -0,0 +1,8 @@
+Thread 1 executing: spawn
+Thread 2 executing: spawn
+Thread 2 executing: read x || retag y
+Thread 1 executing: read x || retag y
+Thread 1 executing: write y
+Thread 2 executing: write y
+Thread 2 executing: exit
+Thread 1 executing: exit
diff --git a/src/tools/miri/tests/pass/tree_borrows/reborrow-is-read.stderr b/src/tools/miri/tests/pass/tree_borrows/reborrow-is-read.stderr
index b23d78a7156..f09aa52f1a1 100644
--- a/src/tools/miri/tests/pass/tree_borrows/reborrow-is-read.stderr
+++ b/src/tools/miri/tests/pass/tree_borrows/reborrow-is-read.stderr
@@ -1,15 +1,15 @@
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  1
-| Act|    └─┬──<TAG=root of the allocation>
-| Act|      └─┬──<TAG=parent>
-| Act|        └────<TAG=x>
+0..   1
+| Act |    └─┬──<TAG=root of the allocation>
+| Act |      └─┬──<TAG=parent>
+| Act |        └────<TAG=x>
 ──────────────────────────────────────────────────
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  1
-| Act|    └─┬──<TAG=root of the allocation>
-| Act|      └─┬──<TAG=parent>
-| Frz|        ├────<TAG=x>
-| Res|        └────<TAG=y>
+0..   1
+| Act |    └─┬──<TAG=root of the allocation>
+| Act |      └─┬──<TAG=parent>
+| Frz |        ├────<TAG=x>
+| Rs  |        └────<TAG=y>
 ──────────────────────────────────────────────────
diff --git a/src/tools/miri/tests/pass/tree_borrows/reserved.stderr b/src/tools/miri/tests/pass/tree_borrows/reserved.stderr
index 691fe8b7744..0d0d52c717f 100644
--- a/src/tools/miri/tests/pass/tree_borrows/reserved.stderr
+++ b/src/tools/miri/tests/pass/tree_borrows/reserved.stderr
@@ -1,58 +1,58 @@
 [interior mut + protected] Foreign Read: Re* -> Frz
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  1
-| Act|    └─┬──<TAG=root of the allocation>
-| Re*|      └─┬──<TAG=base>
-| Re*|        ├─┬──<TAG=x>
-| Re*|        │ └─┬──<TAG=caller:x>
-| Frz|        │   └────<TAG=callee:x>
-| Re*|        └────<TAG=y, caller:y, callee:y>
+0..   1
+| Act |    └─┬──<TAG=root of the allocation>
+| RsM |      └─┬──<TAG=base>
+| RsM |        ├─┬──<TAG=x>
+| RsM |        │ └─┬──<TAG=caller:x>
+| RsCM|        │   └────<TAG=callee:x>
+| RsM |        └────<TAG=y, caller:y, callee:y>
 ──────────────────────────────────────────────────
 [interior mut] Foreign Read: Re* -> Re*
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  8
-| Act|    └─┬──<TAG=root of the allocation>
-| Re*|      └─┬──<TAG=base>
-| Re*|        ├────<TAG=x>
-| Re*|        └────<TAG=y>
+0..   8
+| Act |    └─┬──<TAG=root of the allocation>
+| RsM |      └─┬──<TAG=base>
+| RsM |        ├────<TAG=x>
+| RsM |        └────<TAG=y>
 ──────────────────────────────────────────────────
 [interior mut] Foreign Write: Re* -> Re*
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  8
-| Act|    └─┬──<TAG=root of the allocation>
-| Act|      └─┬──<TAG=base>
-| Re*|        ├────<TAG=x>
-| Act|        └────<TAG=y>
+0..   8
+| Act |    └─┬──<TAG=root of the allocation>
+| Act |      └─┬──<TAG=base>
+| RsM |        ├────<TAG=x>
+| Act |        └────<TAG=y>
 ──────────────────────────────────────────────────
 [protected] Foreign Read: Res -> Frz
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  1
-| Act|    └─┬──<TAG=root of the allocation>
-| Res|      └─┬──<TAG=base>
-| Res|        ├─┬──<TAG=x>
-| Res|        │ └─┬──<TAG=caller:x>
-| Frz|        │   └────<TAG=callee:x>
-| Res|        └────<TAG=y, caller:y, callee:y>
+0..   1
+| Act |    └─┬──<TAG=root of the allocation>
+| Rs  |      └─┬──<TAG=base>
+| Rs  |        ├─┬──<TAG=x>
+| Rs  |        │ └─┬──<TAG=caller:x>
+| RsC |        │   └────<TAG=callee:x>
+| Rs  |        └────<TAG=y, caller:y, callee:y>
 ──────────────────────────────────────────────────
 [] Foreign Read: Res -> Res
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  1
-| Act|    └─┬──<TAG=root of the allocation>
-| Res|      └─┬──<TAG=base>
-| Res|        ├────<TAG=x>
-| Res|        └────<TAG=y>
+0..   1
+| Act |    └─┬──<TAG=root of the allocation>
+| Rs  |      └─┬──<TAG=base>
+| Rs  |        ├────<TAG=x>
+| Rs  |        └────<TAG=y>
 ──────────────────────────────────────────────────
 [] Foreign Write: Res -> Dis
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  1
-| Act|    └─┬──<TAG=root of the allocation>
-| Act|      └─┬──<TAG=base>
-| Dis|        ├────<TAG=x>
-| Act|        └────<TAG=y>
+0..   1
+| Act |    └─┬──<TAG=root of the allocation>
+| Act |      └─┬──<TAG=base>
+| Dis |        ├────<TAG=x>
+| Act |        └────<TAG=y>
 ──────────────────────────────────────────────────
diff --git a/src/tools/miri/tests/pass/tree_borrows/spurious_read.rs b/src/tools/miri/tests/pass/tree_borrows/spurious_read.rs
new file mode 100644
index 00000000000..71e93d2f84f
--- /dev/null
+++ b/src/tools/miri/tests/pass/tree_borrows/spurious_read.rs
@@ -0,0 +1,115 @@
+// We ensure a deterministic execution.
+// Note that we are *also* using barriers: the barriers enforce the
+// specific interleaving of operations that we want, but only the preemption
+// rate guarantees that the error message is also deterministic.
+//@compile-flags: -Zmiri-preemption-rate=0
+//@compile-flags: -Zmiri-tree-borrows
+
+use std::sync::{Arc, Barrier};
+use std::thread;
+
+// A way to send raw pointers across threads.
+// Note that when using this in closures will require explicit copying
+// `let ptr = ptr;` to force the borrow checker to copy the `Send` wrapper
+// instead of just copying the inner `!Send` field.
+#[derive(Copy, Clone)]
+struct SendPtr(*mut u8);
+unsafe impl Send for SendPtr {}
+
+fn main() {
+    retagx_retagy_spuriousx_retx_rety_writey();
+}
+
+// We're going to enforce a specific interleaving of two
+// threads, we use this macro in an effort to make it feasible
+// to check in the output that the execution is properly synchronized.
+//
+// Provide `synchronized!(thread, msg)` where thread is
+// a `(thread_id: usize, barrier: Arc<Barrier>)`, and `msg` the message
+// to be displayed when the thread reaches this point in the execution.
+macro_rules! synchronized {
+    ($thread:expr, $msg:expr) => {{
+        let (thread_id, barrier) = &$thread;
+        eprintln!("Thread {} executing: {}", thread_id, $msg);
+        barrier.wait();
+    }};
+}
+
+// Interleaving:
+//   retag x (protect)
+//   retag y (protect)
+//   spurious read x (target only, which we are executing)
+//   ret x
+//   ret y
+//   write y
+//
+// This is an interleaving that will never have UB in the source
+// (`x` is never accessed for the entire time that `y` is protected).
+// For the spurious read to be allowed, we need to check that there is
+// no UB in the target (i.e., *with* the spurious read).
+//
+// The interleaving differs from the one in `tests/fail/tree_borrows/spurious_read.rs` only
+// in that it has the `write y` while `y` is no longer protected.
+// When the write occurs after protection ends, both source and target are fine
+// (checked by this test); when the write occurs during protection, both source
+// and target are UB (checked by the `fail` test).
+fn retagx_retagy_spuriousx_retx_rety_writey() {
+    let mut data = 0u8;
+    let ptr = SendPtr(std::ptr::addr_of_mut!(data));
+    let barrier = Arc::new(Barrier::new(2));
+    let bx = Arc::clone(&barrier);
+    let by = Arc::clone(&barrier);
+
+    // This thread only needs to
+    // - retag `x` protected
+    // - do a read through `x`
+    // - remove `x`'s protector
+    // Most of the complexity here is synchronization.
+    let thread_x = thread::spawn(move || {
+        let b = (1, bx);
+        synchronized!(b, "start");
+        let ptr = ptr;
+        synchronized!(b, "retag x (&mut, protect)");
+        fn as_mut(x: &mut u8, b: (usize, Arc<Barrier>)) -> *mut u8 {
+            synchronized!(b, "retag y (&mut, protect)");
+            synchronized!(b, "spurious read x");
+            let _v = *x;
+            synchronized!(b, "ret x");
+            let x = x as *mut u8;
+            x
+        }
+        let _x = as_mut(unsafe { &mut *ptr.0 }, b.clone());
+        synchronized!(b, "ret y");
+        synchronized!(b, "write y");
+        synchronized!(b, "end");
+    });
+
+    // This thread's job is to
+    // - retag `y` protected
+    // - (wait a bit that the other thread performs its spurious read)
+    // - remove `y`'s protector
+    // - attempt a write through `y`.
+    let thread_y = thread::spawn(move || {
+        let b = (2, by);
+        synchronized!(b, "start");
+        let ptr = ptr;
+        synchronized!(b, "retag x (&mut, protect)");
+        synchronized!(b, "retag y (&mut, protect)");
+        fn as_mut(y: &mut u8, b: (usize, Arc<Barrier>)) -> *mut u8 {
+            synchronized!(b, "spurious read x");
+            synchronized!(b, "ret x");
+            let y = y as *mut u8;
+            y
+        }
+        let y = as_mut(unsafe { &mut *ptr.0 }, b.clone());
+        synchronized!(b, "ret y");
+        synchronized!(b, "write y");
+        unsafe {
+            *y = 2;
+        }
+        synchronized!(b, "end");
+    });
+
+    thread_x.join().unwrap();
+    thread_y.join().unwrap();
+}
diff --git a/src/tools/miri/tests/pass/tree_borrows/spurious_read.stderr b/src/tools/miri/tests/pass/tree_borrows/spurious_read.stderr
new file mode 100644
index 00000000000..45191eaf9c4
--- /dev/null
+++ b/src/tools/miri/tests/pass/tree_borrows/spurious_read.stderr
@@ -0,0 +1,16 @@
+Thread 1 executing: start
+Thread 2 executing: start
+Thread 2 executing: retag x (&mut, protect)
+Thread 1 executing: retag x (&mut, protect)
+Thread 1 executing: retag y (&mut, protect)
+Thread 2 executing: retag y (&mut, protect)
+Thread 2 executing: spurious read x
+Thread 1 executing: spurious read x
+Thread 1 executing: ret x
+Thread 2 executing: ret x
+Thread 2 executing: ret y
+Thread 1 executing: ret y
+Thread 1 executing: write y
+Thread 2 executing: write y
+Thread 2 executing: end
+Thread 1 executing: end
diff --git a/src/tools/miri/tests/pass/tree_borrows/tree-borrows.rs b/src/tools/miri/tests/pass/tree_borrows/tree-borrows.rs
index 531543441c2..89752bffe9f 100644
--- a/src/tools/miri/tests/pass/tree_borrows/tree-borrows.rs
+++ b/src/tools/miri/tests/pass/tree_borrows/tree-borrows.rs
@@ -12,6 +12,7 @@ fn main() {
     two_mut_protected_same_alloc();
     direct_mut_to_const_raw();
     local_addr_of_mut();
+    returned_mut_is_usable();
 
     // Stacked Borrows tests
     read_does_not_invalidate1();
@@ -93,6 +94,24 @@ fn two_mut_protected_same_alloc() {
     write_second(&mut data.0, &mut data.1);
 }
 
+// This checks that a reborrowed mutable reference returned from a function
+// is actually writeable.
+// The fact that this is not obvious is due to the addition of
+// implicit reads on function exit that might freeze the return value.
+fn returned_mut_is_usable() {
+    fn reborrow(x: &mut u8) -> &mut u8 {
+        let y = &mut *x;
+        // Activate the reference so that it is vulnerable to foreign reads.
+        *y = *y;
+        y
+        // An implicit read through `x` is inserted here.
+    }
+    let mut data = 0;
+    let x = &mut data;
+    let y = reborrow(x);
+    *y = 1;
+}
+
 // ----- The tests below were taken from Stacked Borrows ----
 
 // Make sure that reading from an `&mut` does, like reborrowing to `&`,
diff --git a/src/tools/miri/tests/pass/tree_borrows/unique.default.stderr b/src/tools/miri/tests/pass/tree_borrows/unique.default.stderr
index f870d3bdec0..6e774e5014d 100644
--- a/src/tools/miri/tests/pass/tree_borrows/unique.default.stderr
+++ b/src/tools/miri/tests/pass/tree_borrows/unique.default.stderr
@@ -1,21 +1,21 @@
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  1
-| Act|    └─┬──<TAG=root of the allocation>
-| Res|      └─┬──<TAG=base>
-| Res|        └────<TAG=raw, uniq, uniq>
+0..   1
+| Act |    └─┬──<TAG=root of the allocation>
+| Rs  |      └─┬──<TAG=base>
+| Rs  |        └────<TAG=raw, uniq, uniq>
 ──────────────────────────────────────────────────
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  1
-| Act|    └─┬──<TAG=root of the allocation>
-| Act|      └─┬──<TAG=base>
-| Act|        └────<TAG=raw, uniq, uniq>
+0..   1
+| Act |    └─┬──<TAG=root of the allocation>
+| Act |      └─┬──<TAG=base>
+| Act |        └────<TAG=raw, uniq, uniq>
 ──────────────────────────────────────────────────
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  1
-| Act|    └─┬──<TAG=root of the allocation>
-| Act|      └─┬──<TAG=base>
-| Act|        └────<TAG=raw, uniq, uniq>
+0..   1
+| Act |    └─┬──<TAG=root of the allocation>
+| Act |      └─┬──<TAG=base>
+| Act |        └────<TAG=raw, uniq, uniq>
 ──────────────────────────────────────────────────
diff --git a/src/tools/miri/tests/pass/tree_borrows/unique.uniq.stderr b/src/tools/miri/tests/pass/tree_borrows/unique.uniq.stderr
index 9ab6b879aa7..26d9ad2ad38 100644
--- a/src/tools/miri/tests/pass/tree_borrows/unique.uniq.stderr
+++ b/src/tools/miri/tests/pass/tree_borrows/unique.uniq.stderr
@@ -1,24 +1,24 @@
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  1
-| Act|    └─┬──<TAG=root of the allocation>
-| Res|      └─┬──<TAG=base>
-| Res|        └─┬──<TAG=raw>
-|----|          └────<TAG=uniq, uniq>
+0..   1
+| Act |    └─┬──<TAG=root of the allocation>
+| Rs  |      └─┬──<TAG=base>
+| Rs  |        └─┬──<TAG=raw>
+|-----|          └────<TAG=uniq, uniq>
 ──────────────────────────────────────────────────
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  1
-| Act|    └─┬──<TAG=root of the allocation>
-| Act|      └─┬──<TAG=base>
-| Act|        └─┬──<TAG=raw>
-| Act|          └────<TAG=uniq, uniq>
+0..   1
+| Act |    └─┬──<TAG=root of the allocation>
+| Act |      └─┬──<TAG=base>
+| Act |        └─┬──<TAG=raw>
+| Act |          └────<TAG=uniq, uniq>
 ──────────────────────────────────────────────────
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  1
-| Act|    └─┬──<TAG=root of the allocation>
-| Act|      └─┬──<TAG=base>
-| Act|        └─┬──<TAG=raw>
-| Dis|          └────<TAG=uniq, uniq>
+0..   1
+| Act |    └─┬──<TAG=root of the allocation>
+| Act |      └─┬──<TAG=base>
+| Act |        └─┬──<TAG=raw>
+| Dis |          └────<TAG=uniq, uniq>
 ──────────────────────────────────────────────────
diff --git a/src/tools/miri/tests/pass/tree_borrows/vec_unique.default.stderr b/src/tools/miri/tests/pass/tree_borrows/vec_unique.default.stderr
index a7712ae91fb..f63aa1f6834 100644
--- a/src/tools/miri/tests/pass/tree_borrows/vec_unique.default.stderr
+++ b/src/tools/miri/tests/pass/tree_borrows/vec_unique.default.stderr
@@ -1,6 +1,6 @@
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  2
-| Act|    └─┬──<TAG=root of the allocation>
-| Res|      └────<TAG=base.as_ptr(), base.as_ptr(), raw_parts.0, reconstructed.as_ptr(), reconstructed.as_ptr()>
+0..   2
+| Act |    └─┬──<TAG=root of the allocation>
+| Rs  |      └────<TAG=base.as_ptr(), base.as_ptr(), raw_parts.0, reconstructed.as_ptr(), reconstructed.as_ptr()>
 ──────────────────────────────────────────────────
diff --git a/src/tools/miri/tests/pass/tree_borrows/vec_unique.uniq.stderr b/src/tools/miri/tests/pass/tree_borrows/vec_unique.uniq.stderr
index e9f1cb3b1ed..7942e9884f4 100644
--- a/src/tools/miri/tests/pass/tree_borrows/vec_unique.uniq.stderr
+++ b/src/tools/miri/tests/pass/tree_borrows/vec_unique.uniq.stderr
@@ -1,8 +1,8 @@
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
-0..  2
-| Act|    └─┬──<TAG=root of the allocation>
-|----|      └─┬──<TAG=base.as_ptr(), base.as_ptr()>
-|----|        └─┬──<TAG=raw_parts.0>
-|----|          └────<TAG=reconstructed.as_ptr(), reconstructed.as_ptr()>
+0..   2
+| Act |    └─┬──<TAG=root of the allocation>
+|-----|      └─┬──<TAG=base.as_ptr(), base.as_ptr()>
+|-----|        └─┬──<TAG=raw_parts.0>
+|-----|          └────<TAG=reconstructed.as_ptr(), reconstructed.as_ptr()>
 ──────────────────────────────────────────────────