Compositional Certified Resource Bounds
Compositional Certified Resource Bounds
复制标题
DOI：
10.1145/2737924.2737955
复制
发表时间：
2015-06-01
影响因子：
--
通讯作者：
Shao, Zhong
中科院分区：
文献类型：
--
作者：
Carbonneaux, Quentin;Hoffmann, Jan;Shao, Zhong
本文提出了一种自动生成C程序最坏情况资源界的新方法。所描述的技术将摊销分析和抽象解释的思想结合在一个统一的框架中，以解决最先进技术的四个挑战：组合性、用户交互、证明证书的生成和可伸缩性。组合性是通过结合潜在的摊销分析方法来实现的。通过自然地跟踪顺序循环和函数调用中变量的大小变化，它能够使用局部派生规则来派生全局整个程序边界。抽象地描述了函数的资源消耗，并且可以在不访问函数体的情况下分析函数调用。支持用户交互的新机制清楚地将定性验证和定量验证分开。用户可以通过使用辅助变量和断言来引导分析得出复杂的非线性界限。这些断言分别使用抽象解释或霍尔逻辑等既定的定性技术进行证明。证明证书从本地派生规则自动生成。派生系统相对于形式成本语义的可靠性证明保证了证书的有效性。可伸缩性是通过有效地减少对可以由现成的线性规划解算器解决的线性优化问题的界限推理来实现的。该分析框架在公开可用的工具(CB)-B-4中实现。通过(CB)-B-4与现有工具在挑战微基准测试方面的比较，以及对cBtch基准测试套件中2900多行C代码的分析，实验评估展示了新技术的优势。
This paper presents a new approach for automatically deriving worst-case resource bounds for C programs. The described technique combines ideas from amortized analysis and abstract interpretation in a unified framework to address four challenges for state-of-the-art techniques: compositionality, user interaction, generation of proof certificates, and scalability. Compositionality is achieved by incorporating the potential method of amortized analysis. It enables the derivation of global whole-program bounds with local derivation rules by naturally tracking size changes of variables in sequenced loops and function calls. The resource consumption of functions is described abstractly and a function call can be analyzed without access to the function body. User interaction is supported with a new mechanism that clearly separates qualitative and quantitative verification. A user can guide the analysis to derive complex non-linear bounds by using auxiliary variables and assertions. The assertions are separately proved using established qualitative techniques such as abstract interpretation or Hoare logic. Proof certificates are automatically generated from the local derivation rules. A soundness proof of the derivation system with respect to a formal cost semantics guarantees the validity of the certificates. Scalability is attained by an efficient reduction of bound inference to a linear optimization problem that can be solved by off-the-shelf LP solvers. The analysis framework is implemented in the publicly-available tool (CB)-B-4. An experimental evaluation demonstrates the advantages of the new technique with a comparison of (CB)-B-4 with existing tools on challenging micro benchmarks and the analysis of more than 2900 lines of C code from the cBench benchmark suite.