A new aliasing model for Rust
Jan. 2024
There are several ways in which interior mutable types break some of the assumptions made so far.
& reference//+ This is safe code that compiles, it MUST NOT BE UB.
fn set(u: &Cell<u8>) {
u.set(42); // This performs a write access, but the parent is a `&` which should be `Frozen` ?
}The complete version of this code is available as a miri test case
//+ This is safe code that compiles, it MUST NOT BE UB.
fn mutation_during_two_phase(u: &mut Cell<u8>) {
let x = &u;
u.something({ // Start a two-phase borrow of `u`
// Several foreign accesses (both reads and writes) to the location
// being reborrowed. The two-phase borrow of `u` must not be invalidated at any point.
u.set(3);
x.set(4);
u.get() + x.get()
});
}[Note: Stacked Borrows] Stacked Borrows incorrectly allows writes to non-interior-mutable two-phase borrows, but both Stacked and Tree Borrows must allow writes to interior-mutable two-phase borrows.
The above two examples would be UB if interior mutable references
were treated regularly, because an & reference of a
type with interior mutability allows things that a Frozen
does not. In Tree Borrows we choose the following
& reference are counted as accesses through the parent
reference;Reserved pointers with interior mutability are
unaffected by foreign writes in addition to being normally unaffected by
foreign reads.Just like raw pointers, shared reborrows of types with interior mutability are invalidated when their parent reference is invalidated. This lets us mix together alternating writes from shared interior mutable references from the same level, i.e. that were derived from the same reference.
In order to still preserve some guarantees, the following aspects are unchanged from how normal references behave:
Reserved no
longer allow foreign reads;Reserved still become
Active upon a child write, so that
&mut Cell<_> is properly unique.[Note: Stacked Borrows] By allowing both foreign reads and foreign writes, an interior-mutable unprotected
Reservedbehaves very similarly to a raw pointer, which coincidentally matches Stacked Borrows’ modeling of two-phase borrows with a raw pointer.
[Summary] Interior mutability inherently breaks some assumptions of immutability and uniqueness. Several shared reborrows of the same pointer can coexist and mutate the data. The guarantees of protectors supercede the modifications made to interior mutable two-phase borrows.
With protectors and interior mutability the model is now complete, and we summarize it here:
When creating a new pointer z from an existing
y
z is a Unpin mutable reference
yy in the treeReservedty_is_freezeconflicted as falsez is a non-interior-mutable shared reference
yy in the treeFrozenz the same tag as y, they
are indistinguishable from now onWhen entering a function
When exiting a function
Box argument and the location was deallocatedWhen reading through a pointer y
x of y (including
y), this is a child read
x is readable (i.e. is Frozen
or Reserved or Active)x is Disabled) this is
UBz of y (excluding
y), this is a foreign read
Active into Frozen; this is UB if
z is protectedz is protected and Reserved, set its
conflicted flag to trueWhen writing through a pointer y
x of y (including
y), this is a child write
Reserved into ActiveDisabled or Frozen
or a protected Reserved { conflicted: true }z of y (excluding
y), this is a foreign write
z is protected this is always UB; otherwisez is Reserved and has interior
mutability it is unchanged; otherwiseReserved and Active and
Frozen into Disabled