Tree Borrows
Neven Villani, Johannes Hostert, Derek Dreyer, Ralf Jung
摘要
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, 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.
问问这篇 Paper
智能体会读完全文。
Lune 把这篇 Paper 索引到了每一个公式,引用它的顶会 Paper 也一样。你提问,回答直接引用原文。
引用它的顶会 Paper6
- Miri: Practical Undefined Behavior Detection for RustRalf Jung, Benjamin Kimock, Christian Poveda, Eduardo Sánchez Muñoz 等POPL 2026 · 被引用 8 次
- From Linearity to BorrowingAndrew Wagner, Olek Gierczak, Brianna Marshall, John M. Li 等OOPSLA 2025 · 被引用 1 次
- Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing GuaranteesZachary Grannan, Aurel Bílý, Jonás Fiala, Jasper Geer 等OOPSLA 2025 · 被引用 1 次
- Tracking Borrows with Regular ExpressionsTodd Nowacki, Sam Blackshear, John Mitchell, Shaz Qadeer 等OOPSLA 2026
- Soteria: Efficient Symbolic Execution as a Functional Library: Perhaps You Should Write Your Own Symbolic Execution Engine!Sacha-Élie Ayoun, Opale Sjöstedt, Azalea RaadPLDI 2026
它引用的顶会 Paper4
- Alive2: bounded translation validation for LLVMNuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu 等PLDI 2021 · 被引用 109 次
- Stacked borrows: an aliasing model for RustRalf Jung, Hoang-Hai Dang, Jeehoon Kang, Derek DreyerPOPL 2020 · 被引用 67 次
- Simuliris: a separation logic framework for verifying concurrent program optimizationsLennard Gäher, Michael Sammler, Simon Spies, Ralf Jung 等POPL 2022 · 被引用 33 次
- A Study of Undefined Behavior Across Foreign Function Boundaries in Rust LibrariesIan McCormack, Joshua Sunshine, Jonathan AldrichICSE 2025 · 被引用 5 次
相关 Paper
- How do programmers use unsafe rust?Vytautas Astrauskas, Christoph Matheja, Federico Poli, Peter Müller 等OOPSLA 2020 · 被引用 78 次
- Is rust used safely by software developers?Ana Nora Evans, Bradford Campbell, Mary Lou SoffaICSE 2020 · 被引用 57 次
- Automatic Linear Resource Bound Analysis for Rust via Prophecy PotentialsQihao Lian, Di WangOOPSLA 2025 · 被引用 1 次
- Aliasing Limits on Translating C to Safe RustMehmet Emre, Peter Boyland, Aesha Parekh, Ryan Schroeder 等OOPSLA 2023 · 被引用 32 次
- Flux: Liquid Types for RustNico Lehmann, Adam T. Geller, Niki Vazou, Ranjit JhalaPLDI 2023 · 被引用 29 次
