Verifying Resource Bounds of Programs with Lazy Evaluation and Memoization

Abstract

We present a new approach for specifying and verifying resource utilization of higher-order functional programs that use lazy eval- uation 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 ac- curately models the higher-order control flow and the effects of memoization on resources using sets, algebraic datatypes and mu- tual 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 struc- tures 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 rep- resentations 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 esti- mating the number of evaluation steps, and is 88% for the number of heap-allocated objects.