Stacked Borrows, Tree Borrows and Miri

Item 17.13 gave you the aliasing rule. This page is about the two candidate formalisations of it, the tool that implements them, and the uncomfortable fact that neither is normative.

It is also the page that turns “my code is undefined behaviour” into “my code is undefined behaviour because“ — which is the difference between someone who can read a Miri error and someone who can only stare at it.

Why a model is needed at all

“&mut T is unique” is a slogan. To check it you need a mechanical rule that says, for every operation in a program, whether it invalidates some other reference. That rule has to be precise enough to implement and permissive enough not to reject the standard library.

Nobody has finished writing it. There are two serious candidates.

Stacked Borrows

Jung et al.’s model, and the first one to be implemented.

Every allocation carries a stack of tags. Every reference gets a tag when it is created. The rules:

• borrowing pushes a new tag onto the stack;
• using a pointer pops everything above its tag;
• using a pointer whose tag has been popped is undefined behaviour.

That single mechanism explains the canonical example:

let mut x = 0;
let r = &mut x;
let p = r as *mut i32;
*r = 1;          // using `r` pops `p`'s tag
unsafe { *p = 2 };   // UB: `p`'s tag is gone

and it explains why the reverse order is fine:

let mut x = 0;
let r = &mut x;
let p = r as *mut i32;
unsafe { *p = 2 };   // fine: `p` is on top
*r = 1;              // fine: using `r` pops nothing that matters

$ cargo +nightly miri run
error: Undefined Behavior: attempting a write access using <tag> but that tag does not exist
in the borrow stack for this location

💡The two snippets differ only in the order of the last two lines. Why should order matter when both pointers point at the same i32? click to reveal

Because the model tracks derivation, not identity, and using a parent invalidates its children.

p was derived from r. Stacked Borrows reads that as: p is a child permission, valid only while nobody has gone back to the parent. Writing through r is an assertion that r is exclusive — which, if it is true, means every permission derived from it is no longer live.

This is exactly the guarantee the optimiser wants. If writing through r did not invalidate p, then a store through p could be observed by a later load through r, and noalias on r would be a lie.

The practical rule that falls out: once you have taken a raw pointer from a reference, do not touch the reference again until you are finished with the pointer. That is not a style preference; under this model it is the difference between defined and undefined.

Tree Borrows

Villani et al., PLDI 2025. It replaces the stack with a tree of derived pointers, each node in one of four permission states:

state	meaning
Reserved	a &mut that has not been written through yet
Unique	a &mut that has been written through — genuinely exclusive
Frozen	a shared reference — readable, not writable
Disabled	invalidated; any use is undefined behaviour

The tree shape means a use of one child does not automatically destroy its siblings — only the operations that genuinely conflict do. The result is meaningfully more permissive: the paper reports it rejects 54% fewer test cases across the 30 000 most-used crates. A great deal of existing, careful, real-world unsafe code that Stacked Borrows called undefined is accepted by Tree Borrows.

As of Miri’s late-2025 and 2026 releases, Tree Borrows is the model Miri leads with, and it now tracks UnsafeCell precisely rather than approximating it. Stacked Borrows remains selectable.

Neither model is normative

Say this out loud, because a lot of writing on this topic does not.

Rust has no ratified memory model. The opsem team is still working. Code that Miri accepts today could in principle be declared undefined later, and code it rejects could be declared fine.

And because the two models disagree, code can pass one and fail the other. There is no single answer to “is this allowed?” — there is “Stacked Borrows says no, Tree Borrows says yes, and the language has not decided”.

The engineering response is not paralysis. It is: stay well inside the conservative core. Write code both models accept, prefer patterns the standard library uses, and treat “only Tree Borrows accepts this” as a reason to restructure rather than a licence.

💡Both models constrain references, not raw pointers. What follows for how you write unsafe code? click to reveal

Keep it in raw pointers and mint references late. That is the standard survival tactic, and it is why &raw exists as an operator.

A *mut T has no tag, no permission state, no position in a tree. Storing one, copying it, offsetting it, passing it to another function — none of that touches the model at all. Only the moment you write &*p or &mut *p does a retag happen, and a retag is what can invalidate siblings.

So the shape of robust unsafe code is: raw pointers in your struct fields; raw pointers across the parts of the algorithm that shuffle things around; and a reference created for the shortest window in which you actually need one, ideally at the boundary where you hand a value back to safe code.

This also explains why &raw const x and &x as *const T are not interchangeable. The second creates a reference first, which performs a retag, which can invalidate a sibling pointer you were relying on — and then immediately throws the reference away. All of the cost, none of the benefit. Item 17.6 is that lesson.

What Miri detects

Miri is an interpreter for Rust’s MIR that models the abstract machine rather than the hardware. It catches:

• out-of-bounds accesses;
• use-after-free;
• invalid use of uninitialised data;
• misaligned accesses;
• invalid values (the table in item 17.11);
• violated intrinsic preconditions;
• data races and some weak-memory effects;
• memory leaks;
• aliasing violations, under whichever model you select.

What Miri does not detect

This list is more important than the previous one.

• Anything on a path the test did not execute. Miri runs your program; it does not analyse it.
• Layout-dependent bugs, because Miri’s layout choices need not match the real target’s.
• Most platform APIs, and all real FFI — there is no C to interpret.
• Anything about performance, and anything about your logic.

And the sentence to memorise:

Miri proves nothing about soundness. It tells you that one execution of one test contained no undefined behaviour.

Soundness is a claim about all safe callers. No execution-based tool can establish it. Miri is a spectacularly good bug-finder and not a verifier — and this site’s own harness has the same limitation, plus it cannot run Miri at all.

Running it yourself

Every snippet on this page is copy-pasteable into a scratch crate:

cargo new miri-scratch && cd miri-scratch
rustup toolchain install nightly
rustup +nightly component add miri
# paste the snippet into src/main.rs
cargo +nightly miri run

Useful flags, set through MIRIFLAGS:

flag	effect
-Zmiri-tree-borrows	select Tree Borrows (the current default)
-Zmiri-stacked-borrows	select Stacked Borrows — run both
-Zmiri-disable-isolation	allow real time, real randomness, real files
-Zmiri-many-seeds	re-run with many schedules, to shake out races

MIRIFLAGS=-Zmiri-stacked-borrows cargo +nightly miri run

Running both models on the same test is the single highest-value habit here. Agreement is strong evidence; disagreement tells you exactly where you are relying on an unsettled question.

💡Your crate's whole test suite passes under Miri, both models. How much have you established? click to reveal

That those particular executions, on those particular inputs, contained no detectable undefined behaviour. That is a floor, not a ceiling.

What it does not establish: that the untested branches are fine; that a different input would not violate an aliasing rule; that a future opsem decision will not reclassify something you did; that your unsafe fn contracts are stated correctly; or — most importantly — that the safe code in your module cannot break the invariant the unsafe code trusts. Item 17.20 is that last one, and no dynamic tool can address it.

Treat a clean Miri run the way you treat a clean test run: necessary, informative, and not a proof. The proof is the safety comment, and the safety comment is only as good as the argument in it.

What to carry forward

1. Two models, Stacked Borrows (stack of tags, restrictive) and Tree Borrows (tree of permission states, ~54% more permissive). Miri leads with Tree Borrows; run both.
2. Neither is normative. Rust has no ratified memory model, and the models disagree.
3. Both constrain references, not raw pointers — hence keep it raw, mint late.
4. Miri detects a great deal and proves nothing. “Miri is clean” is a floor.