SPEED: Precise and Efficient Static Estimation of Program Computational Complexity
SPEED: Precise and Efficient Static Estimation of Program Computational Complexity
复制标题
DOI：
10.1145/1594834.1480898
复制
发表时间：
2009-01-01
影响因子：
--
通讯作者：
Chilimbi, Trishul
中科院分区：
文献类型：
--
作者：
Gulwani, Sumit;Mehra, Krishna K.;Chilimbi, Trishul
本文描述了一种过程间的技术，用于计算一个过程执行的语句数量的符号界限，在其标量输入和用户定义的定量功能的输入数据结构。这种计算复杂性的界限，即使是简单的程序通常是析取的，非线性的，并涉及堆的数值属性。我们使用两个新的想法来解决这些边界生成的挑战。我们引入了一种基于多个计数器检测（每个计数器可以初始化和递增在潜在的多个程序位置），允许一个给定的线性不变生成工具来计算线性边界的证明方法，这些计数器变量。然后将这些计数器上的边界组合在一起，以生成非线性和析取的总边界。我们还给出了一个算法，自动化这种证明方法。我们的算法产生的复杂性边界通常是精确的，不仅在计算复杂性方面，而且在常数因子方面。接下来，我们引入了用户定义的定量函数的概念，可以与抽象的数据结构，例如。例如，在一个实施例中，一个列表的长度，树的高度等，我们展示了如何计算这些定量函数的边界使用线性不变生成工具，支持处理未解释的功能。我们展示了这种方法的应用程序，常用的数据结构（即列表，列表，树，位向量）使用的例子，从微软的产品代码。我们观察到，每个数据结构的几个定量函数通常足以允许生成在这些数据结构上循环的各种循环的符号复杂性界限，这些技术的结合使得能够为现实世界的例子生成精确的计算复杂度界限（从Microsoft产品代码和C++ STL库代码中提取），其中一些甚至证明终止也是不平凡的。这种自动生成的边界对于早期检测大型模块化代码库中的惊人性能问题非常有用，这些代码库经常被多个开发人员更改，这些开发人员大量使用其他人编写的代码，而没有很好地理解其实现复杂性。
This paper describes an inter-procedural technique for computing symbolic bounds on the number of statements a procedure executes in terms of its scalar inputs and user-defined quantitative functions of input data-structures. Such computational complexity bounds for even simple programs are usually disjunctive, non-linear, and involve numerical properties of heaps. We address the challenges of generating these bounds using two novel ideas.We introduce a proof methodology based on multiple counter instrumentation (each counter can be initialized and incremented at potentially multiple program locations) that allows a given linear invariant generation tool to compute linear bounds individually on these counter variables. The bounds on these counters are then composed together to generate total bounds that are non-linear and disjunctive. We also give an algorithm for automating this proof methodology. Our algorithm generates complexity bounds that are usually precise not only in terms of the computational complexity, but also in terms of the constant factors.Next, we introduce the notion of user-defined quantitative functions that can be associated with abstract data-structures, e. g., length of a list, height of a tree, etc. We show how to compute bounds in terms of these quantitative functions using a linear invariant generation tool that has support for handling uninterpreted functions. We show application of this methodology to commonly used data-structures (namely lists, list of lists, trees, bit-vectors) using examples from Microsoft product code. We observe that a few quantitative functions for each data-structure are usually sufficient to allow generation of symbolic complexity bounds of a variety of loops that iterate over these data-structures, and that it is straightforward to define these quantitative functions.The combination of these techniques enables generation of precise computational complexity bounds for real-world examples (drawn from Microsoft product code and C++ STL library code) for some of which it is non-trivial to even prove termination. Such automatically generated bounds are very useful for early detection of egregious performance problems in large modular codebases that are constantly being changed by multiple developers who make heavy use of code written by others without a good understanding of their implementation complexity.