about summary refs log tree commit diff
path: root/src/tools/miri/tests/fail
diff options
context:
space:
mode:
authorNeven Villani <vanille@crans.org>2023-09-20 14:27:20 +0200
committerVanille-N <neven.villani@crans.org>2023-10-06 14:37:07 +0200
commitbf1356efc3d3d2c6b5c3fb3157d234f7a0901bc8 (patch)
tree8336be6e3e1e90ec9adb3a21d8cce3eeb5e0f9f8 /src/tools/miri/tests/fail
parent4587c7c1c044652a89104b8dccfd8e025aea177f (diff)
downloadrust-bf1356efc3d3d2c6b5c3fb3157d234f7a0901bc8.tar.gz
rust-bf1356efc3d3d2c6b5c3fb3157d234f7a0901bc8.zip
Fix problems of Reserved -> Frozen
Reserved loses permissions too quickly.
Adding more fine-grained behavior of Reserved lets it lose
write permissions only temporarily.
Protected tags receive a read access on initialized locations.
Diffstat (limited to 'src/tools/miri/tests/fail')
-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
13 files changed, 220 insertions, 83 deletions
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
+