Tree Borrows: How would more precise UnsafeCell tracking work?

[RalfJung]

One of the key differences between Stacked Borrows and Tree Borrows is that &(i32, Cell<i32>) in SB enforces that the first component of the pair is read-only, while TB does not (UnsafeCell is "maximally infectious" in TB). This seems to be one of the most controversial parts of TB.

Leaving aside the question of which of these behaviors is preferable -- what would TB with more precise UnsafeCell even look like? In TB, creating a &!Freeze from a mutable reference is simply a NOP -- the original tag is also used for the new reference, allowing arbitrary aliasing between parent and child. Clearly that does not work any more if some bytes of an &!Freeze can have immutability guarantees: the child pointer needs a new tag which, on the readonly locations, is in Frozen state to ensure that writes to foreign pointers (parents/uncles/...) invalidate the tag. But on readwrite locations, we need a state that allows foreign writes, which does not currently exist.

So, we need a new possible state for tags in TB, Aliased or so, which presumably allows arbitrary foreign (and child) accesses. It should be the case that it never makes a difference whether an access is performed with a tag in Aliased state, or its parent tag.

Is that it? Or are there more challenges?
@Vanille-N would having such a state violate any of the assumptions that various parts of Tree Borrows are making?

[RalfJung]

Ah, one thing I forgot about: even for mutable references, Freeze makes a difference in TB, due to two-phase borrows. For reserved (not-yet-activated) references, foreign writes are okay if and only if the reference is !Freeze.

So reborrowing for mutable references would also need to be aware of where the UnsafeCell are, and initialize locations with ReservedFrozen/ReservedUnfrozen, respectively.

[Vanille-N]

Indeed, if Aliased is added then all that needs to be done is that whenever an Aliased is the starting point of an access, we first climb towards the root and compute the access as if it was done on the nearest non-Aliased parent. EDIT: after discussion it seems this would not even be needed.

Raw pointers could have been alternatively represented as new nodes with fully Aliased permissions, and the current implementation of not creating a new node for them is an easy optimization of that.

Note that currently Reserved already has a ty_is_freeze: bool field; presumably all that would happen for more granular tracking of Cells is that we would replace

let ty_is_freeze = ty.is_freeze();
for each loc {
    loc.perm ← Reserved { ty_is_freeze };
}

with instead

for each loc {
    let loc_is_freeze = ty.is_freeze(loc);
    loc.perm ← Reserved { loc_is_freeze };
}

and probably no update rule would have to change.

[RalfJung]

(After some further discussion with @Vanille-N)

One concern I had was that when we have an Aliased child of an Active tag, and a write happens that is foreign to both, then the next use of the Aliased should be UB. This is indeed the case because the use of the Aliased is also a child access relative to the formerly Active, which at that point is Disabled and hence causes UB.

[Vanille-N]

(already discussed in person, included here for completeness)

This concern is not new, it is already the case for Reserved + UnsafeCell / Active.

-- ...
   |-- x: Active
       |-- y: Reserved { ty_is_freeze: false }

Assume a write occurs that is foreign to both (through ...), then the state becomes

-- ...
    |-- x: Frozen
        |-- y: Reserved { ty_is_freeze: false }

The issue here could be that Frozen forbids write accesses, but Reserved allows them. Will a write access through y be properly forbidden ? The answer is yes because a child write for y is also a child write for x.

Bonus: in part by coincidence, this makes the error messages clearer because if a write is attempted through y the error message will point to x as the nearest problematic ancestor.