Tree Borrows – Dealing with Cells

A new aliasing model for Rust

Neven Villani

Mar. 2023

[ Prev | Up | Next ]

Why interior mutable types need special attention

There are several ways in which interior mutable types break some of the assumptions made so far.

Example: mutation is possible through an & 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` ?
}

Example: mutation is allowed during a two-phase borrow

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.

Additions to the model

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

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:

[Note: Stacked Borrows] By allowing both foreign reads and foreign writes, an interior-mutable unprotected Reserved behaves 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.

Complete summary

With protectors and interior mutability the model is now complete, and we summarize it with the following automaton:

State automaton of pointer permissions. During its lifetime each pointer is subjected to a number of child/foreign read/write accesses, and each of them can update the permission associated with the pointer on some bytes of memory.

When creating a new pointer z from an existing y

When reading through a pointer y

When writing through a pointer y


[ Prev | Up | Next ]