一句话：提出 Hybrid AARA，将类型化静态资源分析与贝叶斯推断融合，得到统计可靠且更鲁棒的最坏情况资源界。
自动推导程序符号化最坏情况资源界有两条路线：对源码做静态分析，以及对程序运行得到的代价测量做数据驱动分析。静态资源分析通常可靠（sound）但不完备，而数据驱动分析虽总能给出结果，却因缺乏鲁棒性而常导致不可靠（unsound）的结论。本文设计、实现并实证评估了一类紧耦合两者优点的混合资源界分析。其静态部分建立在自动摊销资源分析（AARA）之上——这是一种基于类型、通过线性优化进行代价界推断的先进方法；数据驱动部分则基于新颖的贝叶斯建模与推断技术，能够报告关于可能资源代价界的完整概率分布，优于以往的数据驱动方法。核心创新是称为 Hybrid AARA 的新型类型推断系统，它将贝叶斯推断一致地融入传统 AARA。作者证明，在关于运行时代价数据的标准假设下，Hybrid AARA 是统计可靠（statistically sound）的；在一组有挑战性的基准上的实验表明，它既有效缓解了纯静态资源分析的不完备性，又比纯数据驱动分析更准确、更鲁棒。
There are two approaches to automatically deriving symbolic worst-case resource bounds for programs: static analysis of the source code and data-driven analysis of cost measurements obtained by running the program. Static resource analysis is usually sound but incomplete. Data-driven analysis can always return a result, but its lack of robustness often leads to unsound results. This paper presents the design, implementation, and empirical evaluation of hybrid resource bound analyses that tightly integrate static analysis and data-driven analysis. The static analysis part builds on automatic amortized resource analysis (AARA), a state-of-the-art type-based resource analysis method that performs cost bound inference using linear optimization. The data-driven part is rooted in novel Bayesian modeling and inference techniques that improve upon previous data-driven analysis methods by reporting an entire probability distribution over likely resource cost bounds. A key innovation is a new type inference system called Hybrid AARA that coherently integrates Bayesian inference into conventional AARA, combining the strengths of both approaches. Hybrid AARA is proven to be statistically sound under standard assumptions on the runtime cost data. An experimental evaluation on a challenging set of benchmarks shows that Hybrid AARA (i) effectively mitigates the incompleteness of purely static resource analysis; and (ii) is more accurate and robust than purely data-driven resource analysis.
@article{PhamSH24,
title = {Robust Resource Bounds with Static Analysis and Bayesian Inference},
author = {Long Pham and Feras A. Saad and Jan Hoffmann},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656380}
}