Stacked Borrows, Tree Borrows and Miri

Unsafe code must follow Rust's aliasing rules: roughly, a &mut T is the only way to reach its target while it is in use, and a &T does not see the target change (except inside UnsafeCell). Aliasing, mutable references and unsafe code describes those rules informally. This article covers two precise proposals for them, Stacked Borrows and Tree Borrows, and Miri, the tool that checks programs against them.

Miri is an interpreter for MIR, the mid-level intermediate representation that rustc produces. It runs your program on Rust's abstract machine (the model the language rules are written for) instead of on the hardware, and it stops with an error when an operation breaks one of the rules it checks. An aliasing model is the part of those rules that decides which pointers may still be used after other pointers to the same memory have been used.

Why a precise model is needed

"&mut T is exclusive" is easy to state but not precise enough to check. A checker needs a rule that says, for each read or write in a program, whether it is allowed and which other pointers it invalidates. The rule must be strict enough to justify the optimizations the compiler wants to make, and permissive enough to accept code that real libraries, including the standard library, rely on.

The Rust Reference states that Rust does not yet have a defined memory model. (Atomic operations are specified separately: Rust's atomics currently follow the C++20 rules.) The aliasing rules for references are one of the unsettled parts. Stacked Borrows and Tree Borrows are research proposals for them; neither has been adopted as the official rule.

Stacked Borrows

Stacked Borrows was introduced by Ralf Jung, Hoang-Hai Dang, Jeehoon Kang and Derek Dreyer (POPL 2020). It is the model Miri uses by default.

In simplified form:

• Each memory location carries a stack of permission entries.
• Creating a reference, or a raw pointer from a reference, gives the new pointer a tag and pushes an entry for that tag onto the stack.
• Writing through a pointer removes every entry above that pointer's entry. Reading invalidates only the exclusive (&mut) entries above it.
• Using a pointer whose entry is no longer on the stack is undefined behavior.
• An entry created from a shared reference grants read access only (except for data inside UnsafeCell), so writing through a pointer derived from &T is also undefined behavior.

Here a raw pointer p is derived from r, then r is written before p:

fn main() {
    let mut x = 0;
    let r = &mut x;
    let p = r as *mut i32;
    *r = 1; // removes p's entry from the stack
    unsafe { *p = 2 }; // Stacked Borrows: undefined behavior
}

Running it with cargo +nightly miri run (Miri nightly of 2026-10-05) reports:

error: Undefined Behavior: attempting a write access using <551> at alloc196[0x0],
but that tag does not exist in the borrow stack for this location

The numbers in angle brackets and after alloc identify the tag and the allocation; they vary between runs and versions. Miri also points to the line that created the tag and the line that invalidated it.

Swapping the last two accesses is accepted:

fn main() {
    let mut x = 0;
    let r = &mut x;
    let p = r as *mut i32;
    unsafe { *p = 2 }; // p's entry is still on the stack
    *r = 1; // removes p's entry, but p is not used again
    assert_eq!(x, 1);
}

So is reading through r before writing through p, because a read does not remove a raw pointer's entry:

fn main() {
    let mut x = 0;
    let r = &mut x;
    let p = r as *mut i32;
    let _seen = *r; // a read leaves p's entry in place
    unsafe { *p = 2 };
    assert_eq!(x, 2);
}

Tree Borrows

Tree Borrows was introduced by Neven Villani, Johannes Hostert, Derek Dreyer and Ralf Jung (PLDI 2025). It records the pointers derived from each allocation as a tree: each reference is a child of the pointer it was created from. An access through one pointer is a child access for that pointer and its ancestors, and a foreign access for every other node. Each node holds a permission per memory location. The four main states are:

Miri also tracks variants of these states for data inside UnsafeCell and for references passed to functions. Raw pointers do not get their own node; they share the node of the reference they were derived from.

That last point means Tree Borrows accepts the first program above: p and r share a node, so writing through r and then through p is two child accesses to one node. With MIRIFLAGS=-Zmiri-tree-borrows the program runs to completion. This is a concrete case where the two models disagree.

Both models reject conflicting use of two independently created mutable borrows. Here the temporary &mut x that produced p and the later r are siblings in the tree:

fn main() {
    let mut x = 0;
    let p = &mut x as *mut i32;
    let r = &mut x; // a second, independent mutable borrow of x
    *r = 1; // foreign write for p's node: Reserved becomes Disabled
    unsafe { *p = 2 }; // undefined behavior under both models
}

Tree Borrows reports:

error: Undefined Behavior: write access through <528> at alloc196[0x0] is forbidden
  = help: the accessed tag <528> has state Disabled which forbids this child write access

Stacked Borrows rejects it too, but at an earlier point: creating r already removes p's entry from the stack, so the write through p finds no entry.

The Tree Borrows paper evaluated both models on the test suites of the 30 000 most widely used crates and reports that Tree Borrows rejects 54% fewer test cases than Stacked Borrows. That is a count of rejected test cases in one evaluation, not a general measure of how much more code the model allows.

Which model to rely on

Because the models disagree, a program can pass one and fail the other. For the first example the honest answer to "is this allowed?" is: Stacked Borrows rejects it, Tree Borrows accepts it, and the language has not decided. Miri labels both models experimental in its error messages, and code it accepts today could still be ruled undefined by a future decision.

The practical response is to write code that both models accept, prefer patterns the standard library documents, and treat "only Tree Borrows accepts this" as a reason to restructure the code rather than as permission.

fn main() {
    let mut a = [0i32; 4];
    let p = (&raw mut a).cast::<i32>();
    let q = p;
    unsafe {
        *q.add(1) = 5;
        *p.add(3) = 7;
    }
    assert_eq!(a, [0, 5, 0, 7]);
}

fn main() {
    let mut x = 0;
    let p = &raw mut x;
    let r1 = unsafe { &mut *p };
    let r2 = unsafe { &mut *p };
    *r2 = 1;
    *r1 = 2; // undefined behavior under both models
}

fn main() {
    let mut x = 0;
    let p = &raw mut x;
    unsafe { *(&mut *p) += 1 };
    unsafe { *(&mut *p) += 1 };
    unsafe { *p += 1 };
    assert_eq!(x, 3);
}

What Miri detects

Miri detects many kinds of undefined behavior on the paths a program actually executes, including:

• out-of-bounds memory accesses;
• use after free;
• reading uninitialized memory as a value that must be initialized, such as an integer;
• misaligned accesses;
• invalid values, such as a bool holding the byte 2 (see What is Undefined Behaviour? The complete list);
• violated preconditions of unsafe operations and intrinsics, such as unchecked_add overflowing;
• data races, plus some effects of weak memory ordering;
• aliasing violations, under the selected model.

It also reports memory leaks at program exit. A leak is not undefined behavior, and -Zmiri-ignore-leaks turns the report off.

What Miri does not detect

• Code that did not run. Miri checks one execution. Undefined behavior on a branch your test never takes is not reported.
• Foreign code. A call to a C function is normally rejected as an unsupported operation. Miri provides its own implementations of many common standard library and operating system functions, and has experimental support for calling native libraries, but it cannot check what the foreign code itself does.
• Other layouts. Miri uses the type layouts the current compiler chose for the target it is interpreting. Code that depends on an unspecified layout, such as the field order of a struct without #[repr(C)], can pass and still break with another compiler version or target.
• Some pointer misuse. Miri warns that integer-to-pointer casts can make it miss pointer bugs, and Tree Borrows does not support them.
• Logic errors and performance problems, which are not undefined behavior.

A clean Miri run therefore does not prove that code is sound. An API is sound when no safe caller can cause undefined behavior through it, with any input and any schedule. Miri reports that the executions it ran contained no undefined behavior it could detect. That makes it a strong bug-finding tool, not a verifier. Ordinary test runs, including the graded exercises on this site, do not perform these checks at all.

Running it yourself

Miri requires a nightly toolchain. Each complete program on this page can be pasted into src/main.rs of a scratch crate:

cargo new miri-scratch && cd miri-scratch
rustup toolchain install nightly
rustup +nightly component add miri
# paste a program into src/main.rs
cargo +nightly miri run                              # Stacked Borrows (default)
MIRIFLAGS=-Zmiri-tree-borrows cargo +nightly miri run # Tree Borrows

For a library, use cargo +nightly miri test in the same way.

Useful flags, set through the MIRIFLAGS environment variable:

Running your tests under both models is worthwhile, although Miri runs far slower than a native test run. If both models accept an execution, the result does not depend on which of the two you pick. If only one does, Miri's output shows the access where your code relies on a rule the models disagree about. Miri's own documentation adds that the final rules are likely to be stricter than Tree Borrows, so code that only Tree Borrows accepts is the riskier kind.

Summary

1. Stacked Borrows (a stack of permissions per location, Miri's default) and Tree Borrows (a tree of derived references with permission states, enabled by -Zmiri-tree-borrows) are two precise proposals for Rust's aliasing rules. Tree Borrows accepts some programs Stacked Borrows rejects.
2. Neither is official. Rust does not yet have a defined memory model, and the two models can disagree about the same program. Write code both accept.
3. Both models attach permissions when references are created, so keep pointers raw and create references late and briefly.
4. Miri checks the executions it runs. A clean run is evidence, not a proof of soundness.