Jan Hoffmann
Ankush Das
Skip Abstract Section
Abstract
This article presents a resource analysis system for OCaml programs. The system automatically derives worst-case resource bounds for higher-order polymorphic programs with user-defined inductive types. The technique is parametric in the resource and can derive bounds for time, memory allocations and energy usage. The derived bounds are multivariate resource polynomials which are functions of different size parameters that depend on the standard OCaml types. Bound inference is fully automatic and reduced to a linear optimization problem that is passed to an off-the-shelf LP solver. Technically, the analysis system is based on a novel multivariate automatic amortized resource analysis (AARA). It builds on existing work on linear AARA for higher-order programs with user-defined inductive types and on multivariate AARA for first-order programs with built-in lists and binary trees. This is the first amortized analysis, that automatically derives polynomial bounds for higher-order functions and polynomial bounds that depend on user-defined inductive types. Moreover, the analysis handles a limited form of side effects and even outperforms the linear bound inference of previous systems. At the same time, it preserves the expressivity and efficiency of existing AARA techniques. The practicality of the analysis system is demonstrated with an implementation and integration with Inria's OCaml compiler. The implementation is used to automatically derive resource bounds for 411 functions and 6018 lines of code derived from OCaml libraries, the CompCert compiler, and implementations of textbook algorithms. In a case study, the system infers bounds on the number of queries that are sent by OCaml programs to DynamoDB, a commercial NoSQL cloud database service.
- E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini. Cost Analysis of Java Bytecode. In 16th European Symposium on Programming (ESOP’07), pages 157–172, 2007. Google Scholar
Digital Library
- E. Albert, P. Arenas, S. Genaim, and G. Puebla. Closed-Form Upper Bounds in Static Cost Analysis. Journal of Automated Reasoning, pages 161–203, 2011. Google ScholarDigital Library
- E. Albert, P. Arenas, S. Genaim, M. Gómez-Zamalloa, and G. Puebla. Automatic Inference of Resource Consumption Bounds. In Logic for Programming, Artificial Intelligence, and Reasoning, 18th Conference (LPAR’12), pages 1–11, 2012. Google ScholarDigital Library
- E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini. Cost Analysis of Object-Oriented Bytecode Programs. Theoretical Computer Science, 413(1):142 – 159, 2012. Google ScholarDigital Library
- E. Albert, J. C. Fernández, and G. Román-Díez. Non-cumulative Resource Analysis. In Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, (TACAS’15), pages 85–100, 2015. Google ScholarDigital Library
- C. Alias, A. Darte, P. Feautrier, and L. Gonnord. Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs. In 17th International Static Analysis Symposium (SAS’10), pages 117–133, 2010. Google ScholarDigital Library
- D. E. Alonso-Blas and S. Genaim. On the limits of the classical approach to cost analysis. In 19th International Static Analysis Symposium (SAS’12), pages 405–421, 2012. Google ScholarDigital Library
- R. Atkey. Amortised Resource Analysis with Separation Logic. In 19th European Symposium on Programming (ESOP’10), pages 85–103, 2010. Google ScholarDigital Library
- M. Avanzini and G. Moser. A Combination Framework for Complexity. In 24th International Conference on Rewriting Techniques and Applications (RTA’13), pages 55–70, 2013.Google Scholar
- M. Avanzini, U. D. Lago, and G. Moser. Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order. In 29th International Conference on Functional Programming (ICFP’15), pages 152–164, 2012. Google ScholarDigital Library
- R. Benzinger. Automated Higher-Order Complexity Analysis. Theoretical Computer Science, 318(1-2):79–103, 2004. Google ScholarDigital Library
- R. Blanc, T. A. Henzinger, T. Hottelier, and L. Kovács. ABC: Algebraic Bound Computation for Loops. In Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference (LPAR’10), pages 103–118, 2010. Google ScholarDigital Library
- G. E. Blelloch and J. Greiner. A Provable Time and Space Efficient Implementation of NESL. In First International Conference on Functional Programming (ICFP’96), pages 213–225, 1996. Google ScholarDigital Library
- G. E. Blelloch and R. Harper. Cache and I/O Efficent Functional Algorithms. In 40th Symposium on Principles of Programming Languages (POPL’13), pages 39–50, 2013. Google ScholarDigital Library
- M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl. Alternating Runtime and Size Complexity Analysis of Integer Programs. In Tools and Algorithms for the Construction and Analysis of Systems: 20th International Conference (TACAS’14), pages 140–155, 2014.Google Scholar
- B. Campbell. Amortised Memory Analysis using the Depth of Data Structures. In 18th European Symposium on Programming (ESOP’09), pages 190–204, 2009. Google ScholarDigital Library
- Q. Carbonneaux, J. Hoffmann, and Z. Shao. Compositional Certified Resource Bounds. In 36th Conference on Programming Language Design and Implementation (PLDI’15), pages 467–478, 2015. Google ScholarDigital Library
- P. Cerný, T. A. Henzinger, L. Kovács, A. Radhakrishna, and J. Zwirchmayr. Segment Abstraction for Worst-Case Execution Time Analysis. In 24th European Symposium on Programming (ESOP’15), pages 105– 131, 2015.Google Scholar
- E. Çiçek, D. Garg, and U. A. Acar. Refinement Types for Incremental Computational Complexity. In 24th European Symposium on Programming (ESOP’15), pages 406–431, 2015.Google Scholar
- K. Crary and S. Weirich. Resource Bound Certification. In 27th Symposium on Principles of Programming Languages (POPL’00), pages 184–198, 2000. Google ScholarDigital Library
- S. A. Crosby and D. S. Wallach. Denial of service via algorithmic complexity attacks. In 12th USENIX Security Symposium (USENIX’12), pages 3–3, 2003. Google ScholarDigital Library
- N. A. Danielsson. Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In 35th Symposium on Principles of Programming Languauges (POPL’08), pages 133–144, 2008. Google ScholarDigital Library
- N. Danner, D. R. Licata, and R. Ramyaa. Denotational Cost Semantics for Functional Languages with Inductive Types. In 29th International Conference on Functional Programming (ICFP’15), pages 140–151, 2012. Google ScholarDigital Library
- N. Danner, J. Paykin, and J. S. Royer. A Static Cost Analysis for a Higher-Order Language. In 7th Workshop on Programming Languages Meets Program Verification (PLPV’13), pages 25–34, 2013. Google ScholarDigital Library
- A. Flores-Montoya and R. Hähnle. Resource Analysis of Complex Programs with Cost Equations. In Programming Languages and Systems - 12th Asian Symposium (APLAS’14), pages 275–295, 2014.Google ScholarCross Ref
- B. Grobauer. Cost Recurrences for DML Programs. In 6th International Conference on Functional Programming (ICFP’01), pages 253–264, 2001. Google ScholarDigital Library
- S. Gulwani, K. K. Mehra, and T. M. Chilimbi. SPEED: Precise and Efficient Static Estimation of Program Computational Complexity. In 36th Symposium on Principles of Programming Languauges (POPL’09), pages 127–139, 2009. Google ScholarDigital Library
- J. Hoffmann. RAML Web Site. http://raml.co, 2016.Google Scholar
- J. Hoffmann and M. Hofmann. Amortized Resource Analysis with Polynomial Potential. In 19th European Symposium on Programming (ESOP’10), pages 287–306, 2010. Google ScholarDigital Library
- J. Hoffmann and M. Hofmann. Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics. In Programming Languages and Systems - 8th Asian Symposium (APLAS’10), pages 172–187, 2010. Google ScholarDigital Library
- J. Hoffmann, K. Aehlig, and M. Hofmann. Multivariate Amortized Resource Analysis. In 38th Symposium on Principles of Programming Languages (POPL’11), pages 357–370, 2011. Google ScholarDigital Library
- J. Hoffmann, K. Aehlig, and M. Hofmann. Multivariate Amortized Resource Analysis. ACM Transactions on Programming Languages and Systems, 34:14:1–14:62, 2012. Google ScholarDigital Library
- J. Hoffmann, A. Das, and S.-C. Weng. Towards Automatic Resource Bound Analysis for OCaml. ArXiv e-prints, 2016.Google Scholar
- M. Hofmann and S. Jost. Static Prediction of Heap Space Usage for First-Order Functional Programs. In 30th Symposium on Principles of Programming Languages (POPL’03), pages 185–197, 2003. Google ScholarDigital Library
- M. Hofmann and S. Jost. Type-Based Amortised Heap-Space Analysis. In 15th European Symposium on Programming (ESOP’06), pages 22– 37, 2006. Google ScholarDigital Library
- M. Hofmann and G. Moser. Amortised Resource Analysis and Typed Polynomial Interpretations. In Rewriting and Typed Lambda Calculi (RTA-TLCA;14), pages 272–286, 2014.Google ScholarCross Ref
- M. Hofmann and G. Moser. Multivariate Amortised Resource Analysis for Term Rewrite Systems. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA’15), pages 241–256, 2015.Google Scholar
- M. Hofmann and D. Rodriguez. Automatic Type Inference for Amortised Heap-Space Analysis. In 22nd European Symposium on Programming (ESOP’13), pages 593–613, 2013. Google ScholarDigital Library
- J. Hughes, L. Pareto, and A. Sabry. Proving the Correctness of Reactive Systems Using Sized Types. In 23rd Symposium on Principles of Programming Languages (POPL’96), pages 410–423, 1996. Google ScholarDigital Library
- G. Jin, L. Song, X. Shi, J. Scherpelz, and S. Lu. Understanding and Detecting Real-World Performance Bugs. In 33rd Conference on Programming Language Design and Implementation PLDI’12, pages 77–88, 2012. Google ScholarDigital Library
- S. Jost, K. Hammond, H.-W. Loidl, and M. Hofmann. Static Determination of Quantitative Resource Usage for Higher-Order Programs. In 37th Symposium on Principles of Programming Languages (POPL’10), pages 223–236, 2010. Google ScholarDigital Library
- P. C. Kocher. Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems. In Advances in Cryptology - 16th Annual International Cryptology Conference (CRYPTO’96), pages 104– 113, 1996. Google ScholarDigital Library
- U. D. Lago and M. Gaboardi. Linear Dependent Types and Relative Completeness. In 26th IEEE Symposium on Logic in Computer Science (LICS’11), pages 133–142, 2011. Google ScholarDigital Library
- U. D. Lago and B. Petit. The Geometry of Types. In 40th Symposium on Principles of Programming Languages (POPL’13), pages 167–178, 2013. Google ScholarDigital Library
- X. Leroy. The ZINC Experiment: An Economical Implementation of the ML Language. Technical report 117, INRIA, 1990.Google Scholar
- X. Leroy. From Krivine’s Machine to the Caml Implementation. http://pauillac.inria.fr/~xleroy/talks/zam-kazam05.pdf, 2005. Invited talk, May 17, Workshop on the Krivine and ZINC Abstract Machines.Google Scholar
- X. Leroy. Formal Verification of a Realistic Compiler. Communications of the ACM, 52(7):107–115, 2009. Google ScholarDigital Library
- X. Leroy, D. Doligez, A. Frisch, J. Garrigue, D. Rémy, and J. Vouillon. The OCaml system release 4.02. Technical report, Institut National de Recherche en Informatique et en Automatique, 2014.Google Scholar
- V. Nicollet. 99 problems (solved) in ocaml. https://ocaml.org/ learn/tutorials/99problems.html, 2016.Google Scholar
- L. Noschinski, F. Emmes, and J. Giesl. Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs. Journal of Automated Reasoning, 51(1):27–56, 2013.Google ScholarCross Ref
- O. Olivo, I. Dillig, and C. Lin. Static Detection of Asymptotic Performance Bugs in Collection Traversals. In Conference on Programming Language Design and Implementation (PLDI’15), pages 369–378, 2015. Google ScholarDigital Library
- H. R. Simões, P. B. Vasconcelos, M. Florido, S. Jost, and K. Hammond. Automatic Amortised Analysis of Dynamic Memory Allocation for Lazy Functional Programs. In 17th International Conference on Functional Programming (ICFP’12), pages 165–176, 2012. Google ScholarDigital Library
- M. Sinn, F. Zuleger, and H. Veith. A Simple and Scalable Approach to Bound Analysis and Amortized Complexity Analysis. In Computer Aided Verification - 26th International Conference (CAV’14), page 743–759, 2014. Google ScholarDigital Library
- R. E. Tarjan. Amortized Computational Complexity. SIAM J. Algebraic Discrete Methods, 6(2):306–318, 1985.Google ScholarDigital Library
- R. J. Vanderbei. Linear Programming: Foundations and Extensions. Springer US, 2001.Google ScholarCross Ref
- P. Vasconcelos. Space Cost Analysis Using Sized Types. PhD thesis, School of Computer Science, University of St Andrews, 2008.Google Scholar
- P. B. Vasconcelos and K. Hammond. Inferring Costs for Recursive, Polymorphic and Higher-Order Functional Programs. In 15th International Conference on Implementation of Functional Languages (IFL’03), pages 86–101, 2003. Google ScholarDigital Library
- P. B. Vasconcelos, S. Jost, M. Florido, and K. Hammond. Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages. In 24th European Symposium on Programming (ESOP’15), pages 787– 811, 2015.Google Scholar
- B. Wegbreit. Mechanical Program Analysis. Communications of the ACM, 18(9):528–539, 1975. Google ScholarDigital Library
- F. Zuleger, M. Sinn, S. Gulwani, and H. Veith. Bound Analysis of Imperative Programs with the Size-change Abstraction. In 18th International Static Analysis Symposium (SAS’11), pages 280–297, 2011. Google ScholarDigital Library
- E. Çiçek, G. Barthe, M. Gaboardi, D. Garg, and J. Hoffmann. Relational Cost Analysis. In 44th Symposium on Principles of Programming Languages (POPL’17), 2017. Forthcoming. Google ScholarDigital Library
Index Terms
- Towards automatic resource bound analysis for OCaml
Recommendations
Towards automatic resource bound analysis for OCaml
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesThis article presents a resource analysis system for OCaml programs. The system automatically derives worst-case resource bounds for higher-order polymorphic programs with user-defined inductive types. The technique is parametric in the resource and ...
Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints
Difference constraints have been used for termination analysis in the literature, where they denote relational inequalities of the form $$x' \le y + c$$xź≤y+c, and describe that the value of x in the current state is at most the value of y in the ...
Type-guided worst-case input generation
This paper presents a novel technique for type-guided worst-case input generation for functional programs. The technique builds on automatic amortized resource analysis (AARA), a type-based technique for deriving symbolic bounds on the resource usage of ...
Comments