Multivariate amortized resource analysis

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 paper we generalize this to arbitrary multivariate polynomial functions thus allowing bounds of the form mn which had to be grossly overestimated by m²+n² 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 super-linear 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 super-linear 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.

References

1. E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini. Cost Analysis of Java Bytecode. In 16th Euro. Symp. on Prog. (ESOP'07), pages 157--172, 2007.
2. E. Albert, P. Arenas, S. Genaim, and G. Puebla. Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis. In 15th Static Analysis Symp. (SAS'08), pages 221-- 237, 2008.
3. E. Albert, P. Arenas, S. Genaim, M. G´omez-Zamalloa, G. Puebla, D. Ram´1rez, G. Rom´an, and D. Zanardini. Termination and Cost Analysis with COSTA and its User Interfaces. Electr. Notes Theor. Comput. Sci., 258(1):109--121, 2009.
4. R. Atkey. Amortised Resource Analysis with Separation Logic. In 19th Euro. Symp. on Prog. (ESOP'10), pages 85-- 103, 2010.
5. R. Benzinger. Automated Higher-Order Complexity Analysis. Theor. Comput. Sci., 318(1--2):79--103, 2004.
6. L. Beringer, M. Hofmann, A. Momigliano, and O. Shkaravska. Automatic Certification of Heap Consumption. In Log. f. Prog., AI, and Reas., 11th Conf. (LPAR'04), pages 347--362, 2004.
7. B. Campbell. Amortised Memory Analysis using the Depth of Data Structures. In 18th Euro. Symp. on Prog. (ESOP'09), pages 190--204, 2009.
8. W.-N. Chin and S.-C. Khoo. Calculating Sized Types. High.- Ord. and Symb. Comp., 14(2--3):261--300, 2001.
9. K. Crary and S. Weirich. Resource Bound Certification. In 27th ACM Symp. on Principles of Prog. Langs. (POPL'00), pages 184--198, 2000.
10. N. A. Danielsson. Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In 35th ACM Symp. on Principles Prog. Langs. (POPL'08), pages 133--144, 2008.
11. P. Flajolet, B. Salvy, and P. Zimmermann. Automatic Average-case Analysis of Algorithms. Theoret. Comput. Sci., 79(1):37--109, 1991.
12. B. Grobauer. Cost Recurrences for DML Programs. In 6th Int. Conf. on Funct. Prog. (ICFP'01), pages 253--264, 2001.
13. B. S. Gulavani and S. Gulwani. A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis. In Comp. Aid. Verification, 20th Int. Conf. (CAV '08), pages 370--384, 2008.
14. S. Gulwani and F. Zuleger. The Reachability-Bound Problem. In Conf. on Prog. Lang. Design and Impl. (PLDI'10), pages 292--304, 2010.
15. S. Gulwani, K. K. Mehra, and T. M. Chilimbi. SPEED: Precise and Efficient Static Estimation of Program Computational Complexity. In 36th ACM Symp. on Principles of Prog. Langs. (POPL'09), pages 127--139, 2009.
16. J. Hoffmann and M. Hofmann. Amortized Resource Analysis with Polynomial Potential. In 19th Euro. Symp. on Prog. (ESOP'10), pages 287--306, 2010.
17. J. Hoffmann and M. Hofmann. Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics. In 8th Asian Symp. on Prog. Langs. (APLAS'10), 2010. To appear.
18. M. Hofmann and S. Jost. Static Prediction of Heap Space Usage for First-Order Functional Programs. In 30th ACM Symp. on Principles of Prog. Langs. (POPL'03), pages 185-- 197, 2003.
19. M. Hofmann and S. Jost. Type-Based Amortised Heap-Space Analysis. In 15th Euro. Symp. on Prog. (ESOP'06), pages 22--37, 2006.
20. M. Hofmann and D. Rodriguez. Efficient Type-Checking for Amortised Heap-Space Analysis. In 18th Conf. on Comp. Science Logic (CSL'09). LNCS, 2009.
21. J. Hughes and L. Pareto. Recursion and Dynamic Datastructures in Bounded Space: Towards Embedded ML Programming. In 4th Int. Conf. on Funct. Prog. (ICFP'99), pages 70--81, 1999.
22. J. Hughes, L. Pareto, and A. Sabry. Proving the Correctness of Reactive Systems Using Sized Types. In 23th ACM Symp. on Principles of Prog. Langs. (POPL'96), pages 410--423, 1996.
23. S. Jost, H.-W. Loidl, K. Hammond, N. Scaife, and M. Hofmann. Carbon Credits for Resource-Bounded Computations using Amortised Analysis. In 16th Symp. on Form. Meth. (FM'09), pages 354--369, 2009.
24. S. Jost, K. Hammond, H.-W. Loidl, and M. Hofmann. Static Determination of Quantitative Resource Usage for Higher- Order Programs. In 37th ACM Symp. on Principles of Prog. Langs. (POPL'10), pages 223--236, 2010.
25. O. Shkaravska, R. van Kesteren, and M. C. van Eekelen. Polynomial Size Analysis of First-Order Functions. In Typed Lambda Calc. Apps. (TLCA'07), pages 351--365, 2007.
26. R. E. Tarjan. Amortized Computational Complexity. SIAM J. Algebraic Discrete Methods, 6(2):306--318, 1985.
27. R. Wilhelm et al. The Worst-Case Execution-Time Problem Overview of Methods and Survey of Tools. ACM Trans. Embedded Comput. Syst., 7(3), 2008.

Index Terms

• Theory of computation

  • Logic

  • Semantics and reasoning

    • Program reasoning

      • Program analysis

    • Program semantics