Issue discovered in TB: spurious reads are not (yet) possible in a concurrent setting #3054

Vanille-N · 2023-09-07T18:15:27Z

We discovered a week ago that in general, the current model of TB does not allow spurious reads because although reads provably never invalidate other reads, they migh invalidate writes.

Consider the code

fn f1(x: &u8) {}
fn f2(y: &mut u8) -> &mut u8 { &mut *y }

let mut data = 0;
let _ = thread::spawn(|| {
    f1(&mut data)
};
let _ = thread::spawn(|| {
    let y = f2(&mut data);
    *y = 42;
});

of which one possible interleaving is

1: retag x (&, protect) // x: [P]Frozen
2: retag y (&mut, protect) // y: [P]Reserved, x: [P]Frozen
1: return f1 // x: [P]Frozen -> Frozen, y: [P]Reserved
2: return f2 // x: Frozen, y: [P]Reserved -> Reserved
2: write y // x: Disabled, y: Active

that does not have UB.

Assume enough barriers to force this specific interleaving, and consider that the compiler could choose to insert a spurious read throug x during the call to f1 which would produce

1: retag x (&, protect) // x: [P]Frozen
2: retag y (&mut, protect) // y: [P]Reserved, x: [P]Frozen
1: spurious read x // x:  [P]Frozen, y: [P]Reserved -> [P]Frozen
1: return f1 // x: [P]Frozen -> Frozen, y: [P]Frozen
2: return f2 // x: Frozen, y: [P]Frozen -> Frozen
2: write y // UB

Thus the target of the optimization (with a spurious read) has UB when the source did not.

This is bad.

SB is not affected because the code would be UB as early as retag y, this happens because we're trying to be a bit more subtle than that, and because the effects of a foreign read on a protected &mut bleed outside of the boundaries of the protector. Fortunately we have a fix planned, but in the meantime here are some #[should_panic] exhaustive tests to illustrate the issue.

The error message printed by the #[should_panic] tests flags the present issue in slightly more general terms: it says that the sequence retag x (&, protect); retag y (&mut, protect); produces the configuration C_source := x: [P]Frozen, x: [P]Reserved, and that inserting a spurious read through x turns it into C_target := x: [P]Frozen, y: [P]Reserved.
It then says that C_source is distinguishable from C_target, which means that there exists a sequence of instructions applied to both that triggers UB in C_target but not in C_source.
It happens that one such sequence is 1: return f1; 2: return f2; 2: write y; as shown above, but it is not the only one, as for example the interleaving 1: return f1; 2: write y; is also problematic.

src/borrow_tracker/tree_borrows/perms.rs

src/borrow_tracker/tree_borrows/tree.rs

src/borrow_tracker/tree_borrows/diagnostics.rs

src/borrow_tracker/tree_borrows/tree/mod.rs

src/borrow_tracker/tree_borrows/tree/tests.rs

RalfJung · 2023-09-19T15:11:50Z

Just one last comment nit. :) Then please squash the commits and we're good to go.

RalfJung · 2023-09-19T15:12:27Z

r=me after squashing and fixing that comment.
@bors delegate+

bors · 2023-09-19T15:12:30Z

✌️ @Vanille-N, you can now approve this pull request!

If @RalfJung told you to "r=me" after making some further change, please make that change, then do @bors r=@RalfJung

This occurs because in some interleavings, inserting a spurious read turns a Reserved into Frozen. We show here an exhaustive test (including arbitrary unknown code in two different threads) that makes this issue observable.

Vanille-N · 2023-09-19T15:46:22Z

@bors r=@RalfJung

bors · 2023-09-19T15:46:24Z

📌 Commit 69272a8 has been approved by RalfJung

It is now in the queue for this repository.

bors · 2023-09-19T15:46:31Z

⌛ Testing commit 69272a8 with merge 401d897...

bors · 2023-09-19T16:24:21Z

☀️ Test successful - checks-actions
Approved by: RalfJung
Pushing 401d897 to master...

Continuation of #3054: enable spurious reads in TB The last additions to the test suite of TB left some unresolved `#[should_panic]` that these new modifications solve. ## Problem Recall that the issues were arising from the interleavings that follow. ### A. `Reserved -> Frozen` has visible effects after function exit The transition `Reserved -> Frozen` irreversibly blocks write accesses to the tag, so in the interleaving below `y` initially `Reserved` becomes `Frozen` only in the target where a spurious read through `x` is inserted. This makes the later write through `y` UB only in the target and not in the source. ``` 1: retag x (&, protect) 2: retag y (&mut, protect) 1: spurious read x 1: ret x 2: ret y 2: write y ``` ### B. Protectors only announce their presence on retag There is a read-on-reborrow for protected locations, but if the retag of `x` occurs before that of `y` and there is no explicit access through `x`, then `y` is unaware of the existence of `x`. This is problematic because a spurious read inserted through `x` between the retag of `y` and the return of the function protecting `x` is a noalias violation in the target without UB in the source. ``` 1: retag x (&, protect) 2: retag y (&mut, protect) 1: spurious read x 1: ret x 2: write y 2: ret y ``` ## Step 1: Finer behavior for `Reserved` Since one problem is that `Reserved -> Frozen` has consequences beyond function exit, we decide to remove this transition entirely. To replace it we introduce a new subtype of `Reserved` with the extra boolean `aliased` set. `Reserved { aliased: true }` forbids child accesses, but only temporarily: it has no effect on activation once the tag is no longer protected. This makes the semantics of Tree Borrows slightly weaker in favor of being more similar to noalias. This solves interleaving **A.**, but **B.** is still a problem and the exhaustive tests do not pass yet. ## Step 2: Read on function exit Protected tags issue a "reminder" that they are protected until this instant inclusive, in the form of an implicit read (symmetrically to the implicit read on retag). This ensures that if the periods on which two tags `x` and `y` are protected overlap then no matter the interleaving of retags and returns, there is either a protector currently active or a read that has been emitted, both of which temporarily block activation. This makes the exhaustive test designed previously pass, but it has an effect on the ability to return an activated pointer that I had not foreseen before implementing it. ## Step 2': Do not propagate to children A naive implementation of **Step 2** makes the following code UB: ```rs fn reborrow(x: &mut u8) -> &mut u8 { let y = &mut *x; *y = *y; y // callee returns `y: Active`... } let x = &mut 0u8; let y = reborrow(x); // ... and caller receives `y: Frozen` *y = 1; // UB ``` This is unacceptable, and a simple fix is to make this implicit read visible only to foreign tags. We still lack hindsight on the ramifications of this decision, and the fact that the problematic pattern was only discovered because it occured in one completely unrelated test (with a cryptic error message) is worrying. We should be vigilant as to how this interacts with the rest of the model. ## TODO As of commit #281c30, the data race model has not been fully updated. We have removed the reborrow of mutable references counting as a write access, but we still need the implicit read of function exit to count as a read.

Vanille-N force-pushed the spurious-fail branch 2 times, most recently from f9b83a0 to ca60656 Compare September 7, 2023 20:18

RalfJung reviewed Sep 11, 2023

View reviewed changes

RalfJung reviewed Sep 12, 2023

View reviewed changes