Tree Borrows

The Semantics, The Program Logic, And All The Rest

Tree Borrows is an aliasing model for Rust, and the successor of Stacked Borrows. As an aliasing model, it makes defines operations on references to have Undefined Behavior, which unlocks powerful compiler optimizations.

Actually, rustc was already performing these optimizations before Tree (or even Stacked) Borrows existed, but with these definitions, we are able to put the optimizations on a secure foundation and are able to give programmers the tools they need to understand them.

A Brief Summary of Tree Borrows

Tree Borrows (like its predecessor, Stacked Borrows) is part of the Operational Semantics of Rust. The Operational Semantics define how Rust programs are supposed to evaluate, thereby giving a specification to the Rust compiler. Sometimes, the Operational Semantics say that something is Undefined Behavior, (“UB”) which means that the program behaved illegaly, and releases the Rust compiler from its usual obligation to generate a well-behaving program.

Undefined Behavior is a powerful tool, because when the compiler can prove that it occurs, it is allowed to compile the program in an arbitrary way. This is often dangerous, but in Rust we want to use it for good, namely to optimize the following example:

fn example(x: &mut i32, y: &mut i32) -> i32 {
    *x = 42;
    *y = 25;
    *x // optimization: hard-code returning 42 here
}

This program is one such program we want to optimize, by replacing the load *x with a hard-coded constant. This optimization is only legal when x and y do not point to the same memory (do not alias), which is usually guaranteed by the type system. But Rust has unsafe code which can circumvent the restrictions of the type system, which requires us to use a stronger tool to justify this optimization. (See Example 2 in the paper for a more elaborate discussion of this.) This is where Undefined Behavior comes in: By defining such aliasing to be UB, we even disallow unsafe code from creating them. (Safe code was already forbidden from doing so by the Borrow Checker.)

Tree Borrows now defines the rules for when precisely such references are “illegal,” and this is where it differs from Stacked Borrows. Tree Borrows maintains a tree that tracks how references are derived from each other: each reborrow inserts the new reference as a direct child of the parent reference. Each node in the tree then also maintains a state machine, which defines what this node is allowed to do and when UB is triggered.

I will not explain Tree Borrows here, and instead refer you to the paper, or the PLDI talk about that paper, or just the slides from that talk, or some older slides, or this blog post of mine.

The Story of the Paper

Tree Borrows originally started as the Internship Project of Neven, during his internship at MPI-SWS. The intenship was with Derek, and while Ralf had already left the MPI at that point, he was still supervising Neven.

As part of the internship, Neven and Ralf came up with most of the semantics of Tree Borrows, and implemented it in Miri.

The next step was to prove that these semantics actually allow the optimizations alluded to earlier. We wanted this proof to be rock-solid, and thus chose to carry it out in the Rocq proof assistant. This is where I got involved: Neven’s internship had finished at this point, and the Rocq proofs were turning out to be harder than expected.

After a few months of toiling, I had finished the Rocq proofs. These Rocq proofs are not very well-engineered, since they use an ad-hoc definition of trees that turned out to very annoying to work with. The proofs were also useful because they found bugs in the definition of Tree Borrows, where we sometimes did the wrong thing and were unable to justify the desired optimizations.

Since we still had some time left before the deadline, we decided to do some real science and see if our claim that “Tree Borrows is more permissive than Stacked Borrows” holds up in practice. To do so, I ran a large amount of code from the Rust ecosystem under both Tree and Stacked Borrows, and saw that Tree Borrows was indeed more than twice as permissive.

The paper was received very well, and got a Distinguished Paper Award. The Rust community also likes it, and it quickly became the most downloaded PACMPL paper of all time. (PACMPL is the journal that publishes papers from ACM SIGPLAN’s conferences, i.e. PLDI, POPL, OOPSLA, …)

Beyond the First Paper

While Neven has now stopped working on Tree Borrows after we published the first paper, I have not. There are still so many things to do with Tree Borrows, like:

  • Building a Program Logic for it
  • Applying the ideas behind it to other programming languages, notably LLVM’s noalias
  • Tweaking it further to allow more optimizations

I’ll try to keep the next sections updated as the projects we’re working on there progress.

Program Logic

The reason we wanted to add Tree Borrows to Rust is to allow the compiler to optimize programs, by adding UB. Programmers now have to avoid this UB, because otherwise the compiler is going to wreak havoc to their program. In Rust, avoiding UB is supposed to be easy: never use unsafe code, and then there is no UB.

But since we are tweaking the definition of what is UB, we need to be careful to not break this promise about safe code. Ideally, we would want to prove that all safe code satisfies Tree Borrows. To do so, we would like to update the logical relation of RustBelt by enriching it with Tree Borrows information. Additionally, there is quite some unsafe code out there, and the authors of it also need tools to ensure their code is compatible with Tree Borrows.

Both of these aims need a Program Logic for Tree Borrows, which allows reasoning about whethe a program is correct under Tree Borrows in the first place. We are currently developing such a program logic, and I will give a talk about it at the Rust Verification Workshop.

Tree Borrows for Other Languages

LLVM is gaining a formal specification, and it has a feature (noalias) that is very similar to Tree Borrows; so that a formalization can probably build on our work. I already wrote a blog post about this.

Further Tweaks

I am supervising a number of ETH students who make changes to Tree Borrows. This includes:

  • Xinglu Chen’s Bachelor Thesis on more finely-grained interior mutability.
  • Dominik schwaiger’s in-progress Bachelor Thesis on write-inserting optimizations.
  • …

References