Stacked Borrows: Handling of two-phase borrows

[RalfJung]

Basically just a reference to rust-lang/rust#56254, so that we have all Stacked Borrows issues in one place.

Since that issue was created, I decided to basically give up on two-phase borrows in Stacked Borrows, and treat them like raw pointers. That is the only way I found to accept the safe code allowed by two-phase borrows.

[RalfJung]

rust-lang/miri#1878 contains an interesting example of code that we really ought to reject, but currently accept due to two-phase borrows.

[CAD97]

I had a proposal for how to handle two-phase borrows: https://rust-lang.zulipchat.com/#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/can.20.26mut.20just.20always.20be.20two-phase

Collecting some relevant details here for reference purposes:

[Could we] "just" always treat &mut in the two-phase manner? Informally sketching out a patch to SB:

• When SB 2021 would push a Uniq tag to the borrow stack, instead push a new DelayUniq tag.
• Reading through DelayUniq or other tags treats DelayUniq as Shr (frozen-read-only, &T).
• Writing through other tags treats DelayUniq as Uniq.
• A write operation using DelayUniq replaces it with Uniq (resolving the write as a write with Uniq).
• [Remove current two-phase-is-raw-ShrRW] with using DelayUniq.

Mario Carneiro notes that

One interesting side effect of this implementation (I'm not making a value judgment) is that DelayUniq would enable byte-wise two-phase borrows: you could have shared access to the first byte and mutable access to the second through the same &mut borrow.

There's also an unanswered question of what reborrowing DelayUniq looks like. The two main contenders is that this does a write access (turning the DelayUniq into Uniq) or that it creates a new "entangled" DelayUniq (and splits the stack into a tree) such that the new tag and the parent tag get converted into Uniq together (pruning the other tree branches).

In that thread Ralf said

Once we have a satisfying model of two-phase borrows, and we have a proof that this supports the optimizations &mut is supposed to enable, then yeah this could be a reasonable option.

[RalfJung]

FWIW I still think it would be useful to know that the &mut we get as a function argument is not "delayed". That is probably needed for some optimizations.

[CAD97]

I agree that this seems very reasonable, potentially as part of the protectors also introduced by the function boundary.

[RalfJung]

Closing as resolved by tree borrows.