Multivariate amortized resource analysis
Top Cited Papers
Open Access
- 1 October 2012
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems
- Vol. 34 (3), 1-62
- https://doi.org/10.1145/2362389.2362393
Abstract
We study the problem of automatically analyzing the worst-case resource usage of procedures with several arguments. Existing automatic analyses based on amortization or sized types bound the resource usage or result size of such a procedure by a sum of unary functions of the sizes of the arguments. In this article we generalize this to arbitrary multivariate polynomial functions thus allowing bounds of the form mn which had to be grossly overestimated by m 2 + n 2 before. Our framework even encompasses bounds like ∑ i,j≤ n m i m j where the m i are the sizes of the entries of a list of length n . This allows us for the first time to derive useful resource bounds for operations on matrices that are represented as lists of lists and to considerably improve bounds on other superlinear operations on lists such as longest common subsequence and removal of duplicates from lists of lists. Furthermore, resource bounds are now closed under composition which improves accuracy of the analysis of composed programs when some or all of the components exhibit superlinear resource or size behavior. The analysis is based on a novel multivariate amortized resource analysis. We present it in form of a type system for a simple first-order functional language with lists and trees, prove soundness, and describe automatic type inference based on linear programming. We have experimentally validated the automatic analysis on a wide range of examples from functional programming with lists and trees. The obtained bounds were compared with actual resource consumption. All bounds were asymptotically tight, and the constants were close or even identical to the optimal ones.Keywords
Funding Information
- Defense Advanced Research Projects Agency (FA8750-10-2-0254)
- Division of Computer and Network Systems (CNS-0910670)
This publication has 41 references indexed in Scilit:
- Termination and Cost Analysis with COSTA and its User InterfacesElectronic Notes in Theoretical Computer Science, 2009
- The worst-case execution-time problem—overview of methods and survey of toolsACM Transactions on Embedded Computing Systems, 2008
- Automated higher-order complexity analysisTheoretical Computer Science, 2004
- Automated complexity analysis of Nuprl extracted programsJournal of Functional Programming, 2001
- Cost analysis of logic programsACM Transactions on Programming Languages and Systems, 1993
- Automatic average-case analysis of algorithmsTheoretical Computer Science, 1991
- ACE: an automatic complexity evaluatorACM Transactions on Programming Languages and Systems, 1988
- Automating program analysisJournal of the ACM, 1988
- Amortized Computational ComplexitySIAM Journal on Algebraic Discrete Methods, 1985
- Mechanical program analysisCommunications of the ACM, 1975