https://plf.inf.ethz.ch/research/pldi25-tree-borrows.html

  * Homepage
  * Navigation
  * Search
  * Content
  * Footer
  * Contact
  * Sitemap

 

Programming Language Foundations Lab

---------------------------------------------------------------------

Services

  * Student portal
  * Alumni association
  * Staffnet
  * Contact
  * Login

Search

 
EN

Departments

  * ETH Zurich
  * D-INFK
  * Institute for Programming Languages and Systems
  * Programming Language Foundations Lab

Language Selection

  * English

You are here

  * Homepage chevron_right
  * Research chevron_right
  * Tree Borrows

Tree Borrows

external page Neven Villani, external page Johannes Hostert, external
page Derek Dreyer, external page Ralf Jung

Fig.1 from the paper, showing the Tree Borrows state machine
The state machine at the heart of Tree Borrows.

The Rust programming language is well known for its ownership-based
type system, which offers strong guarantees like memory safety and
data race freedom. However, Rust also provides unsafe escape hatches,
for which safety is not guaranteed automatically and must instead be
manually upheld by the programmer. This creates a tension. On the one
hand, compilers would like to exploit the strong guarantees of the
type system--particularly those pertaining to aliasing of pointers--in
order to unlock powerful intraprocedural optimizations. On the other
hand, those optimizations are easily invalidated by "badly behaved"
unsafe code. To ensure correctness of such optimizations, it thus
becomes necessary to clearly define what unsafe code is "badly
behaved." In prior work, external page Stacked Borrows defined a set
of rules achieving this goal. However, Stacked Borrows rules out
several patterns that turn out to be common in real-world unsafe Rust
code, and it does not account for advanced features of the Rust
borrow checker that were introduced more recently.

To resolve these issues, we present Tree Borrows. As the name
suggests, Tree Borrows is defined by replacing the stack at the heart
of Stacked Borrows with a tree. This overcomes the aforementioned
limitations: our evaluation on the 30 000 most widely used Rust
crates shows that Tree Borrows rejects 54% fewer test cases than
Stacked Borrows does. Additionally, we prove (in Rocq) that it
retains most of the Stacked Borrows optimizations and also enables
important new ones, notably read-read reorderings.

  * external page Paper (PDF)
  * external page Artifact
  * external page Source code

Received a Distinguished Paper Award at PLDI'25

Footer

Search

Keyword or person [                    ] 
Services

  * Student portal
  * Alumni association
  * Staffnet
  * Contact
  * Login

Departments

  * D-ARCH Architecture
  * D-BAUG Civil, Environmental and Geomatic Engineering
  * D-BIOL Biology
  * D-BSSE Biosystems Science and Engineering
  * D-CHAB Chemistry and Applied Biosciences
  * D-EAPS Earth and Planetary Sciences
  * D-GESS Humanities, Social and Political Sciences
  * D-HEST Health Sciences and Technology
  * D-INFK Computer Science
  * D-ITET Information Technology and Electrical Engineering
  * D-MATH Mathematics
  * D-MATL Department of Materials
  * D-MAVT Mechanical and Process Engineering
  * D-MTEC Management, Technology and Economics
  * D-PHYS Physics
  * D-USYS Environmental Systems Science

Table of contents and legal

  * Sitemap
  * Imprint
  * Accessibility Statement
  * Disclaimer & Copyright
  * Privacy Policy

(c) 2025  Eidgenossische Technische Hochschule Zurich
JavaScript has been disabled in your browser