Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore a 14-minute conference presentation from OOPSLA 2025 that introduces RaRust, a groundbreaking type-based linear resource-bound analysis system for Rust programs. Learn how researchers Qihao Lian and Di Wang from Peking University developed an innovative approach to static resource analysis that leverages Rust's unique memory safety features, particularly its borrow mechanisms, to understand program performance characteristics. Discover the novel concept of "prophecy potentials" alongside shared potentials that enable compositional reasoning about both shared and mutable borrows in Rust's ownership system. Understand how RaRust follows the automatic amortized resource analysis (AARA) methodology to construct a resource-aware type system specifically tailored for Rust's safety guarantees. Examine the theoretical foundation through the Resource-Aware Borrow Calculus (RABC), a variant of the Low-Level Borrow Calculus that proves the soundness of the approach. See experimental results demonstrating RaRust's capability to infer symbolic linear resource bounds for complex Rust programs featuring shared and mutable borrows, reborrows, heap-allocated data structures, loops, and recursion, bridging the gap between Rust's memory safety guarantees and performance analysis.
