forked from rust-lang/rust
-
Notifications
You must be signed in to change notification settings - Fork 0
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 rust-lang#3067 - Vanille-N:spurious-incremental, r=Ralf…
…Jung Continuation of rust-lang#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.
- Loading branch information
Showing
37 changed files
with
1,097 additions
and
481 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
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
Oops, something went wrong.