paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Tree Borrows

Tree Borrows(树状借用)
PLDI 9(PLDI)2025匹配度 4/10 · 论文属于 Rust 形式语义与别名模型,涉及形式化证明和编译器优化,与用户对 PL 形式化的兴趣有交集;但不涉及 LLM/Agent、静态分析、浮点程序分析或贝叶斯程序分析,也不是 AI 辅助 PL,因此与核心研究方向距离较远。引用 8 inbox
Neven Villani, Johannes Hostert, Derek Dreyer, Ralf Jung
crossref: 2026-09-10

AI 速览

一句话:用树结构替代栈定义 Rust 别名模型 Tree Borrows,更精确刻画 unsafe 代码行为,大幅减少误报并保留与新增编译器优化。

Rust 的所有权类型系统提供内存安全与无数据竞争保证,但 unsafe 代码可绕过这些保证,因此要让编译器放心利用指针别名信息做过程内优化,就必须明确定义什么样的 unsafe 代码是“行为不良”的。此前提出的 Stacked Borrows 规则虽给出了这样的定义,却排除了许多真实 unsafe Rust 代码中常见的模式,也未覆盖借用检查器后来引入的新特性。本文提出 Tree Borrows:其名称即表明核心做法是把 Stacked Borrows 中的栈替换为树,从而放宽了上述限制。作者在 30000 个最广泛使用的 Rust crate 上评估,发现 Tree Borrows 拒绝的测试用例比 Stacked Borrows 少 54%;同时用 Rocq 机器化证明:它保留了 Stacked Borrows 的大部分优化能力,并支持一些重要的新优化,尤其是读-读重排(read-read reordering)。

问题
Rust 的 unsafe 代码可能违反别名规则,而为保证编译器基于别名的优化正确,必须精确定义 unsafe 代码的合法行为;现有 Stacked Borrows 过于严格,排除了真实代码中常见模式,且未涵盖较新的借用检查器特性。
方法
将 Stacked Borrows 核心的栈结构替换为树结构,给出 Tree Borrows 的别名/借用模型规则,并在 Rocq 证明助手中机器化验证其优化正确性。
评估
在 30000 个最常用 Rust crate 上比较被拒绝的测试用例数量(比 Stacked Borrows 少 54%),并用 Rocq 证明其保留大多数 Stacked Borrows 优化且新增 read-read 重排等优化。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot3141,
  title = {Tree Borrows},
  author = {Neven Villani and Johannes Hostert and Derek Dreyer and Ralf Jung},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {PLDI},
  year = {2025},
  doi = {10.1145/3735592}
}