一句话:用树结构替代栈定义 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)。
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.