一句话：提出资源分解，将多种资源分析技术组合，并证明组合得到的成本界可靠。
资源分析旨在导出程序的符号资源界，但静态、动态、手动等技术各有长短。本文提出资源分解这一程序翻译方法：用用户指定的资源组件标注程序作为分析技术间的接口，再生成资源守卫程序，让一种分析推断以资源组件为参数的总成本界，让其他分析推断这些组件的符号界并代入。作者基于指称成本语义和二元逻辑关系证明，组合可靠分量得到的界对原程序可靠。文中实例化静态、数据驱动与手动分析的三种组合，其中数据驱动部分用贝叶斯方法推断递归深度的线性与对数界。实验表明，该方法能为多个此前方法难以处理的基准推断出可靠且渐近紧的成本界。
Resource analysis aims to derive symbolic resource bounds of programs. Although numerous resource-analysis techniques have been developed—ranging from static to dynamic and manual to automated techniques—they each come with their own distinct strengths and weaknesses. To overcome the limitations of individual resource-analysis techniques, a promising approach is to combine them in such a way that retains their complementary strengths while mitigating their respective weaknesses. This article proposes a novel program translation method called resource decomposition that facilitates the combination of different resource-analysis techniques. The key idea of resource decomposition is to first identify and annotate the program with resource components , which are user-specified variables that serve as an interface between different analysis techniques. Using these resource components, our method generates a resource-guarded program , where one analysis technique is used to infer an overall cost bound parametric in the resource components, and other analysis techniques are used to infer symbolic bounds to be substituted for the resource components. We establish the soundness of resource decomposition using a denotational cost semantics and a binary logical relation. It states that composing sound bounds results in a sound bound for the original program. Furthermore, we present three instantiations of the resource-decomposition framework, each representing distinct combinations of static, data-driven, and manual resource analyses. The data-driven part of these instantiations is a novel Bayesian approach to inferring linear and logarithmic bounds of recursion depths. An implementation and empirical evaluation of resource decomposition demonstrates that it can effectively infer sound and asymptotically tight cost bounds for a number of challenging benchmarks that are beyond the reach of previous analysis methods.
@article{paperbot3013,
title = {Integrating Resource Analyses via Resource Decomposition},
author = {Long Pham and Yue Niu and Nathan Glover and Feras Saad and Jan Hoffmann},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763798}
}