Abstract
We present a new approach for specifying and verifying resource utilization of higher-order functional programs that use lazy evaluation and memoization. In our approach, users can specify the desired resource bound as templates with numerical holes e.g. as steps ≤ ? * size(l) + ? in the contracts of functions. They can also express invariants necessary for establishing the bounds that may depend on the state of memoization. Our approach operates in two phases: first generating an instrumented first-order program that accurately models the higher-order control flow and the effects of memoization on resources using sets, algebraic datatypes and mutual recursion, and then verifying the contracts of the first-order program by producing verification conditions of the form ∃ ∀ using an extended assume/guarantee reasoning. We use our approach to verify precise bounds on resources such as evaluation steps and number of heap-allocated objects on 17 challenging data structures and algorithms. Our benchmarks, comprising of 5K lines of functional Scala code, include lazy mergesort, Okasaki's real-time queue and deque data structures that rely on aliasing of references to first-class functions; lazy data structures based on numerical representations such as the conqueue data structure of Scala's data-parallel library, cyclic streams, as well as dynamic programming algorithms such as knapsack and Viterbi. Our evaluations show that when averaged over all benchmarks the actual runtime resource consumption is 80% of the value inferred by our tool when estimating the number of evaluation steps, and is 88% for the number of heap-allocated objects.
- E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini. Cost analysis of object-oriented bytecode programs. Theor. Comput. Sci., 413(1):142–159, 2012. Google ScholarDigital Library
- C. Alias, A. Darte, P. Feautrier, and L. Gonnord. Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In Static Analysis Symposium, SAS, 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 Static Analysis Symposium, SAS, pages 405–421, 2012. Google ScholarDigital Library
- H. Apfelmus. Quicksort and k-th smallest elements. 2009.Google Scholar
- A. W. Appel. Intensional equality ;=) for continuations. SIGPLAN Not., 31(2), Feb. 1996. Google ScholarDigital Library
- Arvind, R. S. Nikhil, and K. K. Pingali. I-structures: Data structures for parallel computing. ACM Trans. Program. Lang. Syst., 11(4):598– 632, Oct. 1989. Google ScholarDigital Library
- M. Avanzini, U. D. Lago, and G. Moser. Analysing the complexity of functional programs: higher-order meets first-order. In International Conference on Functional Programming, ICFP, pages 152–164, 2015. Google ScholarDigital Library
- C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovi´c, T. King, A. Reynolds, and C. Tinelli. CVC4. In Computer Aided Verification, CAV, pages 171–177, 2011. Google ScholarDigital Library
- R. Benzinger. Automated higher-order complexity analysis. Theoretical Computer Science, 318(1):79 – 103, 2004. Google ScholarDigital Library
- Y. Bertot and P. Castéran. Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, 2004. Google ScholarDigital Library
- T. A. Beyene, C. Popeea, and A. Rybalchenko. Solving existentially quantified horn clauses. In Computer Aided Verification, CAV, 2013.Google Scholar
- R. Bird and P. Wadler. An Introduction to Functional Programming. Prentice Hall International (UK) Ltd., 1988. Google ScholarDigital Library
- R. W. Blanc, E. Kneuss, V. Kuncak, and P. Suter. An overview of the Leon verification system. In Scala Workshop, 2013. Google ScholarDigital Library
- J. C. Blanchette, A. Popescu, and D. Traytel. Foundational extensible corecursion: a proof assistant perspective. In International Conference on Functional Programming, ICFP, pages 192–204, 2015. Google ScholarDigital Library
- J. C. Blanchette, A. Popescu, and D. Traytel. Witnessing (co)datatypes. In European Symposium on Programming, ESOP, pages 359–382, 2015.Google ScholarCross Ref
- I. Bogudlov, T. Lev-Ami, T. W. Reps, and M. Sagiv. Revamping TVLA: making parametric shape analysis competitive. In Computer Aided Verification, CAV, pages 221–225, 2007. Google ScholarDigital Library
- M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl. Analyzing runtime and size complexity of integer programs. ACM Trans. Program. Lang. Syst., pages 13:1–13:50, 2016. Google ScholarDigital Library
- Q. Carbonneaux, J. Hoffmann, T. Ramananandro, and Z. Shao. Endto-end verification of stack-space bounds for C programs. In Programming Language Design and Implementation, PLDI, 2014. Google ScholarDigital Library
- A. Chlipala. Mostly-automated verification of low-level programs in computational separation logic. In Programming Language Design and Implementation, PLDI, pages 234–245, 2011. Google ScholarDigital Library
- M. Col´on, S. Sankaranarayanan, and H. Sipma. Linear invariant generation using non-linear constraint solving. In Computer Aided Verification, CAV, 2003.Google Scholar
- T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein. Introduction to Algorithms (Second Edition). MIT Press and McGraw-Hill, 2001. Google ScholarDigital Library
- N. A. Danielsson. Lightweight semiformal time complexity analysis for purely functional data structures. In Principles of Programming Languages, POPL, pages 133–144, 2008. Google ScholarDigital Library
- N. Danner, J. Paykin, and J. S. Royer. A static cost analysis for a higher-order language. In Workshop on Programming languages meets program verification, PLPV, pages 25–34, 2013. Google ScholarDigital Library
- S. Dasgupta, C. H. Papadimitriou, and U. V. Vazirani. Algorithms. McGraw-Hill, 2008. Google ScholarDigital Library
- L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems TACAS, pages 337–340, 2008. Google ScholarDigital Library
- D. Distefano and M. J. Parkinson J. jStar: Towards practical verification for java. In Object-oriented Programming Systems Languages and Applications, OOPSLA, pages 213–226, 2008. Google ScholarDigital Library
- M. Fähndrich and K. R. M. Leino. Heap monotonic typestates. In International Workshop on Aliasing, Confinement and Ownership in Object-oriented Programming, IWACO, page 58, 2003.Google Scholar
- R. B. Findler and M. Felleisen. Contracts for higher-order functions. In International Conference on Functional Programming, ICFP, pages 48–59, 2002. 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, pages 275–295, 2014.Google Scholar
- B. Ford. Packrat parsing: Simple, powerful, lazy, linear time, functional pearl. In International Conference on Functional Programming ICFP, pages 36–47, 2002. Google ScholarDigital Library
- J. Giesl, M. Raffelsieper, P. Schneider-Kamp, S. Swiderski, and R. Thiemann. Automated termination proofs for haskell by term rewriting. ACM Trans. Program. Lang. Syst., 33(2):7:1–7:39, Feb. 2011. Google ScholarDigital Library
- S. Gulwani, K. K. Mehra, and T. M. Chilimbi. SPEED: precise and efficient static estimation of program computational complexity. In Principles of Programming Languages, POPL, 2009. Google ScholarDigital Library
- A. Gurfinkel, T. Kahsai, A. Komuravelli, and J. A. Navas. The SeaHorn verification framework. In Compuer Aided Verification, CAV, 2015.Google Scholar
- J. Harrison. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009. Google ScholarCross Ref
- J. Hoffmann, K. Aehlig, and M. Hofmann. Resource Aware ML. In Computer Aided Verification, CAV, pages 781–786, 2012. Google ScholarDigital Library
- B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx, and F. Piessens. VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In Proceedings of NASA Formal Methods, NFM, pages 41–55, 2011. Google ScholarDigital Library
- N. D. Jones and N. Bohr. Termination analysis of the untyped lambacalculus. In Rewriting Techniques and Applications, RTA, pages 1–23, 2004.Google Scholar
- S. Jost, K. Hammond, H. Loidl, and M. Hofmann. Static determination of quantitative resource usage for higher-order programs. In Principles of Programming Languages, POPL, pages 223–236, 2010. Google ScholarDigital Library
- D. Kapur, R. Majumdar, and C. G. Zarba. Interpolation for data structures. In Foundations of Software Engineering, FSE, pages 105– 116, 2006. Google ScholarDigital Library
- M. Kaufmann, J. S. Moore, and P. Manolios. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Norwell, MA, USA, 2000. Google ScholarDigital Library
- G. Klein, P. Derrin, and K. Elphinstone. Experience report: Sel4: Formally verifying a high-performance microkernel. In International Conference on Functional Programming, ICFP, pages 91–96, 2009. Google ScholarDigital Library
- K. Knowles and C. Flanagan. Hybrid type checking. ACM Trans. Program. Lang. Syst., 32(2):6:1–6:34, Feb. 2010. Google ScholarDigital Library
- N. Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In Principles of Programming Languages, POPL, pages 416–428, 2009. Google ScholarDigital Library
- N. Kobayashi, R. Sato, and H. Unno. Predicate abstraction and CEGAR for higher-order model checking. In Programming Language Design and Implementation, PLDI, pages 222–233, 2011. Google ScholarDigital Library
- J. Launchbury. A natural semantics for lazy evaluation. In Principles of Programming Languages, POPL, 1993. Google ScholarDigital Library
- D. Le Métayer. Ace: An automatic complexity evaluator. ACM Trans. Program. Lang. Syst., 10(2):248–266, Apr. 1988. Google ScholarDigital Library
- K. R. M. Leino. Dafny: An automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning, pages 348–370, 2010. Google ScholarDigital Library
- K. R. M. Leino and M. Moskal. Co-induction simply - automatic coinductive proofs in a program verifier. In Formal Methods, FM, pages 382–398, 2014. Google ScholarDigital Library
- X. Leroy. Formal verification of a realistic compiler. Commun. ACM, 52(7):107–115, July 2009. Google ScholarDigital Library
- R. Madhavan, S. Kulal, and V. Kuncak. Verifying resource bounds of programs with lazy evaluation and memoization, EPFL-REPORT- 215783. Technical report, EPFL, 2016.Google Scholar
- R. Madhavan and V. Kuncak. Symbolic resource bound inference, EPFL-REPORT-190578. Technical report, EPFL, 2014.Google Scholar
- R. Madhavan and V. Kuncak. Symbolic resource bound inference for functional programs. In Computer Aided Verification, CAV, pages 762–778, 2014. Google ScholarDigital Library
- J. A. Navas, E. Mera, P. L´opez-Garc´ıa, and M. V. Hermenegildo. User-definable resource bounds analysis for logic programs. In International Conference on Logic Programming, ICLP, pages 348–363, 2007. Google ScholarDigital Library
- P. C. Nguyen and D. V. Horn. Relatively complete counterexamples for higher-order programs. In Programming Language Design and Implementation, PLDI, pages 446–456, 2015. Google ScholarDigital Library
- P. C. Nguyen, S. Tobin-Hochstadt, and D. V. Horn. Soft contract verification. In international conference on Functional programming, ICFP, pages 139–152, 2014. Google ScholarDigital Library
- T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. Google ScholarDigital Library
- M. Odersky, L. Spoon, and B. Venners. Programming in Scala: a comprehensive step-by-step guide. Artima Press, 2008. Google ScholarDigital Library
- C. Okasaki. Simple and efficient purely functional queues and deques. Journal of Functional Programming, 5:583–592, 10 1995.Google ScholarCross Ref
- C. Okasaki. Purely Functional Data Structures. Cambridge University Press, 1998. Google ScholarDigital Library
- R. Piskac, T. Wies, and D. Zufferey. Grasshopper - complete heap verification with mixed specifications. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS, pages 124–139, 2014.Google Scholar
- A. Prokopec. Data Structures and Algorithms for Data-Parallel Computing in a Managed Runtime. PhD thesis, EPFL, 2014.Google Scholar
- A. Prokopec and M. Odersky. Conc-trees for functional and parallel programming. In Languages and Compilers for Parallel Computing, LCPC, pages 254–268, 2015. Google ScholarDigital Library
- A. Reynolds and V. Kuncak. Induction for SMT solvers. In Verification, Model Checking, and Abstract Interpretation, VMCAI, pages 80–98, 2015. Google ScholarDigital Library
- J. C. Reynolds. Definitional interpreters for higher-order programming languages. Higher-Order and Symbolic Computation, 11(4):363–397, 1998. Google ScholarDigital Library
- M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3valued logic. In Principles of Programming Languages, POPL, pages 105–118, 1999. Google ScholarDigital Library
- D. Sands. Calculi for Time Anlaysis of Functional Programs. PhD thesis, Imperial College, University of London, 1990.Google Scholar
- D. Sands. Complexity analysis for a lazy higher-order language. In European Symposium on Programming, ESOP, pages 361–376, 1990. Google ScholarDigital Library
- D. Sereni. Termination analysis of higher-order functional programs. PhD thesis, University of Oxford, UK, 2006.Google Scholar
- H. R. Sim˜oes, P. B. Vasconcelos, M. Florido, S. Jost, and K. Hammond. Automatic amortised analysis of dynamic memory allocation for lazy functional programs. In International Conference on Functional Programming, ICFP, pages 165–176, 2012. Google ScholarDigital Library
- M. Sinn, F. Zuleger, and H. Veith. A simple and scalable static analysis for bound analysis and amortized complexity analysis. In Computer Aided Verification CAV, pages 745–761, 2014. Google ScholarDigital Library
- P. Suter, A. S. Köksal, and V. Kuncak. Satisfiability modulo recursive programs. In Symposium on Static Analysis SAS, 2011. Google ScholarDigital Library
- W. Swierstra. Stream: A library for manipulating infinite lists. https://hackage.haskell.org/package/Stream-0.4.7.2/ docs/Data-Stream.html. 2015.Google Scholar
- S. Tobin-Hochstadt and D. V. Horn. Higher-order symbolic execution via contracts. In Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA, pages 537–554, 2012. 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 European Symposium on Programming, ESOP, 2015.Google ScholarCross Ref
- N. Vazou, E. L. Seidel, R. Jhala, D. Vytiniotis, and S. Peyton-Jones. Refinement types for haskell. In International Conference on Functional Programming, ICFP, pages 269–282, 2014. Google ScholarDigital Library
- A. Viterbi. Error bounds for convolutional codes and an asymptotically optimum decoding algorithm. IEEE Transactions on Information Theory, 13(2):260–269, April 1967. Google ScholarDigital Library
- N. Voirol, E. Kneuss, and V. Kuncak. Counter-example complete verification for higher-order functions. In Symposium on Scala, pages 18–29, 2015. Google ScholarDigital Library
- N. Voirol and V. Kuncak. Automating verification of functional programs with quantified invariants, EPFL-REPORT-222712. Technical report, EPFL, 2016.Google Scholar
- D. Vytiniotis, S. Peyton Jones, K. Claessen, and D. Rosén. HALO: Haskell to logic through denotational semantics. In Principles of Programming Languages, POPL, pages 431–442, 2013. Google ScholarDigital Library
- R. Wilhelm, J. Engblom, A. Ermedahl, N. Holsti, S. Thesing, D. Whalley, G. Bernat, C. Ferdinand, R. Heckmann, T. Mitra, F. Mueller, I. Puaut, P. Puschner, J. Staschulat, and P. Stenström. The worst-case execution-time problem—overview of methods and survey of tools. ACM Trans. Embed. Comput. Syst., 7(3):36:1–36:53, May 2008. Google ScholarDigital Library
- D. N. Xu. Hybrid contract checking via symbolic simplification. In Workshop on Partial Evaluation and Program Manipulation, PEPM, pages 107–116, 2012. Google ScholarDigital Library
- D. N. Xu, S. Peyton Jones, and K. Claessen. Static contract checking for haskell. In Principles of Programming Languages, POPL, pages 41–52, 2009. Google ScholarDigital Library
- K. Zee, V. Kuncak, and M. C. Rinard. Full functional verification of linked data structures. In Programming Language Design and Implementation, PLDI, 2008. Google ScholarDigital Library
- F. Zuleger, S. Gulwani, M. Sinn, and H. Veith. Bound analysis of imperative programs with the size-change abstraction. In Static Analysis Symposium, SAS, pages 280–297, 2011. Google ScholarDigital Library
- Introduction Language and Semantics Generating Model Programs Model Verification and Inference Evaluation Related WorkGoogle Scholar
Index Terms
- Contract-based resource verification for higher-order functions with memoization
Recommendations
Contract-based resource verification for higher-order functions with memoization
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesWe present a new approach for specifying and verifying resource utilization of higher-order functional programs that use lazy evaluation and memoization. In our approach, users can specify the desired resource bound as templates with numerical holes ...
Flow analysis of lazy higher-order functional programs
In recent years much interest has been shown in a class of functional languages including HASKELL, lazy ML, SASL/KRC/MIRANDA, ALFL, ORWELL, and PONDER. It has been seen that their expressive power is great, programs are compact, and program manipulation ...
Types and higher-order recursion schemes for verification of higher-order programs
POPL '09We propose a new verification method for temporal properties of higher-order functional programs, which takes advantage of Ong's recent result on the decidability of the model-checking problem for higher-order recursion schemes (HORS's). A program is ...
Comments