Continuation of #3054: enable spurious reads in TB

[Vanille-N]

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:

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.

[RalfJung]

@rustbot author

[Vanille-N]

@rustbot ready

[RalfJung]

@rustbot author

[Vanille-N]

The fail test in the last commit is technically redundant since it's a subpattern of our spurious read test.
I added it because I think it's helpfull to diff it with the pass test to see the difference, but it shouldn't be required.

[Vanille-N]

@rustbot ready

[RalfJung]

@rustbot author

[RalfJung]

Here it's not clear which operation happens in which thread.

[RalfJung]

In fact the comments in this file are not coherent... first it says

// read x     || retag y (&mut, protect)
//        -- sync --
//            || write y

but later it says

//      read y
//      retag x
//      write x

Is this mixing up x and y? Something doesn't check out.

[Vanille-N]

Oops, I was planning to make the names consistent across read_retag_no_race and spurious_read
(x in thread 1, y in thread 2, x gets read, y gets written), but it looks like I started in and didn't finish the process.

[RalfJung]

Great, thanks. :)
Please rebase, fix the build, and squash.

[RalfJung]

Looking great!
@bors r+

[bors]

📌 Commit f95bcbb has been approved by RalfJung

It is now in the queue for this repository.

[bors]

⌛ Testing commit f95bcbb with merge 4e4426b...

[bors]

☀️ Test successful - checks-actions
Approved by: RalfJung
Pushing 4e4426b to master...