-
Notifications
You must be signed in to change notification settings - Fork 356
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Auto merge of #3742 - Vanille-N:master, r=RalfJung
TB: Reserved + Protected + IM + lazy is a horrible combination that should not exist As discovered by `@JoJoDeveloping,` the result of having both Protector exceptions on lazy locations (protectors only protect initialized bytes) and interior mutability exceptions for protected tags (Reserved IM does not accept foreign writes when protected) leads to some very undesirable results, namely that we cannot do spurious writes even on protected activated locations. We propose that Protected Reserved IM should no longer exist and instead when a type is retagged as part of a `FnEntry` it is assumed to lose interior mutability. In fact, this was already being done implicitly because relevant transitions were guarded by an `if protected`, but the difference is that now it also applies to transitions that occur after the end of the protector.
- Loading branch information
Showing
7 changed files
with
211 additions
and
6 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,107 @@ | ||
| // Illustrating a problematic interaction between Reserved, interior mutability, | ||
| // and protectors, that makes spurious writes fail in the previous model of Tree Borrows. | ||
| // As for all similar tests, we disable preemption so that the error message is deterministic. | ||
| //@compile-flags: -Zmiri-tree-borrows -Zmiri-preemption-rate=0 | ||
| // | ||
| // One revision without spurious read (default source code) and one with spurious read. | ||
| // Both are expected to be UB. Both revisions are expected to have the *same* error | ||
| // because we are aligning the behavior of `without` to that of `with` so that the | ||
| // spurious write is effectively a noop in the long term. | ||
| //@revisions: without with | ||
|
|
||
| use std::cell::Cell; | ||
| use std::sync::{Arc, Barrier}; | ||
| use std::thread; | ||
|
|
||
| // Here is the problematic interleaving: | ||
| // - thread 1: retag and activate `x` (protected) | ||
| // - thread 2: retag but do not initialize (lazy) `y` as Reserved with interior mutability | ||
| // - thread 1: spurious write through `x` would go here | ||
| // - thread 2: function exit (noop due to lazyness) | ||
| // - thread 1: function exit (no permanent effect on `y` because it is now Reserved IM unprotected) | ||
| // - thread 2: write through `y` | ||
| // In the source code nothing happens to `y` | ||
|
|
||
| // `Send`able raw pointer wrapper. | ||
| #[derive(Copy, Clone)] | ||
| struct SendPtr(*mut u8); | ||
| unsafe impl Send for SendPtr {} | ||
|
|
||
| type IdxBarrier = (usize, Arc<Barrier>); | ||
|
|
||
| // Barriers to enforce the interleaving. | ||
| // This macro expects `synchronized!(thread, msg)` where `thread` is a `IdxBarrier`, | ||
| // and `msg` is 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 main() { | ||
| // The conflict occurs on one single location but the example involves | ||
| // lazily initialized permissions. We will use `&mut Cell<()>` references | ||
| // to `data` to achieve this. | ||
| 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); | ||
|
|
||
| // Retag and activate `x`, wait until the other thread creates a lazy permission. | ||
| // Then do a spurious write. Finally exit the function after the other thread. | ||
| let thread_1 = thread::spawn(move || { | ||
| let b = (1, bx); | ||
| synchronized!(b, "start"); | ||
| let ptr = ptr; | ||
| synchronized!(b, "retag x (&mut, protect)"); | ||
| fn inner(x: &mut u8, b: IdxBarrier) { | ||
| *x = 42; // activate immediately | ||
| synchronized!(b, "[lazy] retag y (&mut, protect, IM)"); | ||
| // A spurious write should be valid here because `x` is | ||
| // `Active` and protected. | ||
| if cfg!(with) { | ||
| synchronized!(b, "spurious write x (executed)"); | ||
| *x = 64; | ||
| } else { | ||
| synchronized!(b, "spurious write x (skipped)"); | ||
| } | ||
| synchronized!(b, "ret y"); | ||
| synchronized!(b, "ret x"); | ||
| } | ||
| inner(unsafe { &mut *ptr.0 }, b.clone()); | ||
| synchronized!(b, "write y"); | ||
| synchronized!(b, "end"); | ||
| }); | ||
|
|
||
| // Create a lazy Reserved with interior mutability. | ||
| // Wait for the other thread's spurious write then observe the side effects | ||
| // of that write. | ||
| let thread_2 = thread::spawn(move || { | ||
| let b = (2, by); | ||
| synchronized!(b, "start"); | ||
| let ptr = ptr; | ||
| synchronized!(b, "retag x (&mut, protect)"); | ||
| synchronized!(b, "[lazy] retag y (&mut, protect, IM)"); | ||
| fn inner(y: &mut Cell<()>, b: IdxBarrier) -> *mut u8 { | ||
| synchronized!(b, "spurious write x"); | ||
| synchronized!(b, "ret y"); | ||
| // `y` is not retagged for any bytes, so the pointer we return | ||
| // has its permission lazily initialized. | ||
| y as *mut Cell<()> as *mut u8 | ||
| } | ||
| // Currently `ptr` points to `data`. | ||
| // We do a zero-sized retag so that its permission is lazy. | ||
| let y_zst = unsafe { &mut *(ptr.0 as *mut Cell<()>) }; | ||
| let y = inner(y_zst, b.clone()); | ||
| synchronized!(b, "ret x"); | ||
| synchronized!(b, "write y"); | ||
| unsafe { *y = 13 } //~ERROR: /write access through .* is forbidden/ | ||
| synchronized!(b, "end"); | ||
| }); | ||
|
|
||
| thread_1.join().unwrap(); | ||
| thread_2.join().unwrap(); | ||
| } |
40 changes: 40 additions & 0 deletions
40
tests/fail/tree_borrows/reservedim_spurious_write.with.stderr
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,40 @@ | ||
| 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: [lazy] retag y (&mut, protect, IM) | ||
| Thread 2 executing: [lazy] retag y (&mut, protect, IM) | ||
| Thread 2 executing: spurious write x | ||
| Thread 1 executing: spurious write x (executed) | ||
| Thread 1 executing: ret y | ||
| Thread 2 executing: ret y | ||
| Thread 2 executing: ret x | ||
| Thread 1 executing: ret x | ||
| Thread 1 executing: write y | ||
| Thread 2 executing: write y | ||
| error: Undefined Behavior: write access through <TAG> at ALLOC[0x0] is forbidden | ||
| --> $DIR/reservedim_spurious_write.rs:LL:CC | ||
| | | ||
| LL | unsafe { *y = 13 } | ||
| | ^^^^^^^ write access through <TAG> at ALLOC[0x0] 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 Disabled which forbids this child write access | ||
| help: the accessed tag <TAG> was created here, in the initial state Reserved | ||
| --> $DIR/reservedim_spurious_write.rs:LL:CC | ||
| | | ||
| LL | fn inner(y: &mut Cell<()>, b: IdxBarrier) -> *mut u8 { | ||
| | ^ | ||
| help: the accessed tag <TAG> later transitioned to Disabled due to a foreign write access at offsets [0x0..0x1] | ||
| --> $DIR/reservedim_spurious_write.rs:LL:CC | ||
| | | ||
| LL | *x = 64; | ||
| | ^^^^^^^ | ||
| = help: this transition corresponds to a loss of read and write permissions | ||
| = note: BACKTRACE (of the first span) on thread `unnamed-ID`: | ||
| = note: inside closure at $DIR/reservedim_spurious_write.rs:LL:CC | ||
|
|
||
| note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace | ||
|
|
||
| error: aborting due to 1 previous error | ||
|
|
40 changes: 40 additions & 0 deletions
40
tests/fail/tree_borrows/reservedim_spurious_write.without.stderr
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,40 @@ | ||
| 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: [lazy] retag y (&mut, protect, IM) | ||
| Thread 2 executing: [lazy] retag y (&mut, protect, IM) | ||
| Thread 2 executing: spurious write x | ||
| Thread 1 executing: spurious write x (skipped) | ||
| Thread 1 executing: ret y | ||
| Thread 2 executing: ret y | ||
| Thread 2 executing: ret x | ||
| Thread 1 executing: ret x | ||
| Thread 1 executing: write y | ||
| Thread 2 executing: write y | ||
| error: Undefined Behavior: write access through <TAG> at ALLOC[0x0] is forbidden | ||
| --> $DIR/reservedim_spurious_write.rs:LL:CC | ||
| | | ||
| LL | unsafe { *y = 13 } | ||
| | ^^^^^^^ write access through <TAG> at ALLOC[0x0] 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 Disabled which forbids this child write access | ||
| help: the accessed tag <TAG> was created here, in the initial state Reserved | ||
| --> $DIR/reservedim_spurious_write.rs:LL:CC | ||
| | | ||
| LL | fn inner(y: &mut Cell<()>, b: IdxBarrier) -> *mut u8 { | ||
| | ^ | ||
| help: the accessed tag <TAG> later transitioned to Disabled due to a protector release (acting as a foreign write access) on every location previously accessed by this tag | ||
| --> $DIR/reservedim_spurious_write.rs:LL:CC | ||
| | | ||
| LL | } | ||
| | ^ | ||
| = help: this transition corresponds to a loss of read and write permissions | ||
| = note: BACKTRACE (of the first span) on thread `unnamed-ID`: | ||
| = note: inside closure at $DIR/reservedim_spurious_write.rs:LL:CC | ||
|
|
||
| note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace | ||
|
|
||
| error: aborting due to 1 previous error | ||
|
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters