一句话：提出 RaRust，一种利用共享势与预言势的 Rust 类型化线性资源界分析，可处理借用、重借用、堆结构与递归。
Rust 类型系统保证内存安全，但良类型程序未必高效，因此需静态分析资源消耗；利用借用机制辅助资源界分析仍属空白。本文提出 RaRust，一种面向良类型 Rust 程序的基于类型的线性资源界分析。它沿用自动摊销资源分析（AARA）构建资源感知类型系统，并引入共享势和预言势，以组合方式处理共享与可变借用。为证明可靠性，作者提出 Resource-Aware Borrow Calculus（RABC），作为 LLBC 的变体。原型实验表明，RaRust 能为含共享/可变借用、重借用、堆分配数据结构、循环和递归的程序推断符号线性资源界。
Rust has become a popular system programming language that strikes a balance between memory safety and performance. Rust’s type system ensures the safety of low-level memory controls; however, a well-typed Rust program is not guaranteed to enjoy high performance. This article studies static analysis for resource consumption of Rust programs, aiming at understanding the performance of Rust programs. Although there have been tons of studies on static resource analysis, exploiting Rust’s memory safety—especially the borrow mechanisms and their properties—to aid resource-bound analysis, remains unexplored. This article presents RaRust , a type-based linear resource-bound analysis for well-typed Rust programs. RaRust follows the methodology of automatic amortized resource analysis (AARA) to build a resource-aware type system. To support Rust’s borrow mechanisms, including shared and mutable borrows, RaRust introduces shared and novel prophecy potentials to reason about borrows compositionally. To prove the soundness of RaRust , this article proposes Resource-Aware Borrow Calculus (RABC) as a variant of recently proposed Low-Level Borrow Calculus (LLBC). The experimental evaluation of a prototype implementation of RaRust demonstrates that RaRust is capable of inferring symbolic linear resource bounds for Rust programs featuring shared and mutable borrows, reborrows, heap-allocated data structures, loops, and recursion.
@article{paperbot3210,
title = {Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials},
author = {Qihao Lian and Di Wang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720492}
}