We submitted the Tree Borrows paper!

We submitted our paper on Tree Borrows, you can find it here. Tree Borrows is a new aliasing model for Rust—read the paper to find out what that means. The model itself was developed by Neven, Ralf, and Derek. I only got involved later, initially starting as a “Coq gremlin” to help out with the proofs of section 5. As part of this, we discovered and fixed several “model bugs,” where corner cases of the model did not behave as we expected it to.

Eventually, I also started working on the Miri implementation, running the experiment described in section 4. As part of it, we realized that enabling Tree Borrows makes Miri quite a bit slower, so I spend a lot of time on improving the performance of Tree Borrows in Miri. While it is now a lot faster, it is not fast enough yet (as briefly discussed in section 4.3). So, I’m planning to work more in this in the next few weeks. In general, we are not “done” with Tree Borrows—we think that the aliasing model does many things right, and that we could use the same approach to e.g. handle noalias in LLVM. Stay tuned!