Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials

TL;DR

This paper introduces RaRust, a novel static analysis tool that uses type-based linear resource bounds and prophecy potentials to accurately analyze resource consumption in Rust programs, including complex borrow scenarios.

Contribution

RaRust is the first resource-bound analysis for Rust that leverages its unique borrow mechanisms using prophecy potentials within a type-based framework.

Findings

RaRust infers symbolic linear resource bounds for complex Rust programs.

RaRust effectively handles shared and mutable borrows, reborrows, and heap-allocated data.

Experimental results show RaRust's capability to analyze real-world Rust code.

Abstract

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.