在刚刚结束的第 40 届程序设计语言领域会议 OOPSLA(SPLASH) 2025 上，北京大学计算机学院程序设计语言研究室关于Rust程序资源消耗分析的工作《Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials》荣获杰出论文奖（Distinguished Paper Award）。

面向对象程序设计语言大会 OOPSLA (ACM international conference on Object oriented programming systems languages and applications) 是计算机协会 ACM 的重要年度性会议，是在程序设计语言领域最高水平的学术会议之一。大会主题为程序语言的设计（类型系统、程序语义与逻辑）、语言运行环境支撑 （编译器与运行时技术）及其应用 （如程序分析、程序验证与程序合成）。

这是北京大学第一篇获得 OOPSLA 杰出论文奖的论文。论文的第一作者为北京大学计算机学院 2023 级博士生练琪灏（导师：王迪），通讯作者为北京大学王迪助理教授。

Rust 是一种兼顾高性能与内存安全的系统级编程语言。其类型系统通过在编译期实施严格的内存安全检查，实现了零运行时开销的安全保障机制。然而值得注意的是，仅满足内存安全性并不足以确保程序的高性能表现。本次获奖论文提出了一种基于 Rust 类型系统信息的资源分析方法，首次为 Rust 程序建立了静态性能分析的理论框架与实践路径。

论文信息：Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials, Qihao Lian, Di Wang, Proceedings of the ACM on Programming Languages, Volume 9, Issue OOPSLA1, Article No.: 130, Pages 1406 - 1433, https://doi.org/10.1145/3720492

论文提出了一种为 Rust 语言进行静态资源分析的实用方法，即通过结合 Rust 语言的类型系统与工具链进行资源分析。

传统基于势能方法的资源分析在应对可变数据与别名问题时面临显著挑战：当同一数据存在多个别名引用时，这些引用均可自由访问原始数据并共享其携带的势能，而现有分析技术难以有效同步不同别名间的势能信息。

本研究聚焦于利用Rust语言特有的内存安全机制——所有权与借用系统，开展程序的资源分析。Rust的所有权与借用机制通过为可变引用引入互斥约束，为资源分析提供了独特优势。基于这一性质，文章提出了RaRust，这是一种面向安全 Rust程序的线性资源界限分析技术，其遵循自动摊销资源分析的方法论，构建了一个资源感知的类型系统，用于分析类型安全的Rust程序。针对Rust借用机制的特殊性，特别是可变借用的互斥性，RaRust引入了预言势能（prophecy potential）来组合地自动分析借用的资源消耗情况。

为了评估方法的理论可靠性与实际可行性，论文形式化描述了这套方法并证明了其可靠性，同时提供了一个基于 Rust 编译器及编译器前端插件 Charon 的原型实现。基准测试实验表明其支持 Rust 语言机制中嵌套借用、递归函数与循环结构、用户自定义数据类型等场景。这一原型实现基于 Rust 编译器的设计，不仅充分复用了现有 Rust 生态组件，更为后续工具链集成奠定了基础。