Rust in Depth

Stacked Borrows and Miri

/ Miri -> "MEER-ee" /

Safe Rust's aliasing-XOR-mutability rule is checked by the borrow checker, but unsafe code with raw pointers steps outside that check — and yet there are still rules. If you create a &mut T, the optimiser is allowed to ASSUME nothing else touches that data while the reference is live, so it can cache values in registers and reorder reads and writes. If your unsafe code secretly aliases that &mut through a raw pointer, you have lied to the optimiser, and the result is undefined behaviour even though no safe rule was visibly broken. The problem: what exactly counts as 'aliasing a &mut' at the level of raw pointers needs a precise definition. Stacked Borrows is a proposed formal model that gives that definition, and Miri is the interpreter that checks your program against it.

Stacked Borrows works, roughly and at a glance, like this. Every byte of memory carries an imaginary stack of 'tags', one per reference or pointer currently allowed to access it. When you create a new reference from an existing one, its tag is pushed onto the stack; when you use a reference, the model checks its tag is still somewhere valid on the stack; and using an OLD reference after a newer one has been pushed effectively pops everything above it, invalidating those newer borrows. The single rule that falls out is the one you already know: while a &mut is the active (top) tag, accessing the same memory through any other pointer is illegal and pops the &mut, making its later use UB. It formalises 'a &mut means exclusive access' down to the level of raw pointers, so the optimiser's assumption is always honoured. (Tree Borrows is a newer, more permissive refinement of the same idea; you do not need the details, only that an aliasing model exists.) Miri is an interpreter that runs your Rust on a virtual machine, watching every memory operation and every borrow, and reports the instant your unsafe code violates the model, dereferences a dangling pointer, reads uninitialised memory, or hits a data race — undefined behaviour that a normal run might hide.

Why this matters: in C, undefined behaviour from aliasing violations is famously invisible — the program might work today, on this compiler, and corrupt silently tomorrow. Stacked Borrows plus Miri give Rust's unsafe code something C lacks: a checkable definition of what aliasing is allowed, and a tool that catches violations deterministically in tests. The honest caveats: Miri is an interpreter, so it is far slower than native and only checks the code paths your tests actually execute — it finds UB it sees, not UB you never ran. And the aliasing model is still being finalised, so Stacked Borrows is the working definition rather than a frozen language guarantee. Still, if you write any unsafe code, running your tests under Miri (cargo +nightly miri test) is the single highest-value habit for catching the UB the compiler cannot.

// This LOOKS fine and may print 1, 2 on a normal build... let mut n = 0i32; let r = &mut n; // &mut: r has exclusive access let p = r as *mut i32; // a raw pointer aliasing the same data *r = 1; let bad = unsafe { *p }; // using p while r is active: aliasing violation *r = 2; println!("{bad} {n}"); // ... but `cargo +nightly miri run` reports it as undefined behaviour.

A normal build may hide an aliasing violation; Miri, checking against the Stacked Borrows model, flags it deterministically.

Miri only catches UB on the paths your tests actually run, and it is much slower than native. Stacked Borrows is the working aliasing model, not yet a frozen guarantee (Tree Borrows refines it). Even so, running unsafe code under Miri is the best way to catch the UB the compiler cannot.

Also called
Stacked BorrowsTree BorrowsMirithe aliasing modelRust aliasing model別名模型