Tree Borrows

A new aliasing model for Rust

Neven Villani

Mar. 2023

Tree Borrows is a proposed alternative to Stacked Borrows that fulfills the same role: to analyse the execution of Rust code at runtime and define the precise requirements of the aliasing constraints. When these aliasing constraints are violated, the code is declared Undefined Behavior (UB). This enables optimizations that would otherwise be unsound in the presence of unsafe code.

[Note: Stacked Borrows] When the document makes a comparison between Stacked Borrows and Tree Borrows, it will be formatted like this. If you know nothing about Stacked Borrows, skipping these explanations should not impede your understanding.


(Oct. 2023) During the ongoing project of formalizing Tree Borrows, we have discovered insufficiencies regarding spurious reads under concurrency. This leads to the introduction of the conflicted flag and implicit reads on function exit for protected locations.
If you’re new to Tree Borrows you can continue reading as normal. If you know the basics of Tree Borrows and want to know specifically what changed, you can consult the diff.

(Jul. 2024) As formalization progresses, Johannes Hostert (who joined the project) found other bugs, also related to Reserved and spurious reads. These are fixed by making Active protected locations get an implicit write (instead of read) on function exit.
If you’re new to Tree Borrows you can continue reading as normal. If you know the basics of Tree Borrows and want to know specifically what changed, you can consult the diff.

(Nov. 2024) Tree Borrows has been submitted for publication! You may read a preprint here.
An alternative mirror can be found on J. Hostert’s website, who joined the project to work on several aspects, from proving some of Tree Borrows’ claims in Coq and fixing bugs in the core model, to improving performance in Miri.
In related news, the formalization of Tree Borrows in Coq is complete, significantly increasing our confidence in the claims we have made.


The current version of Tree Borrows is implemented in the Miri interpreter. Compared to another description, this document is more example-oriented.

Table of contents

See also some References. Suggest modifications to this document by opening a pull request.