Links und Funktionen

You are here: Home / Publikationen / Static determination of quantitative resource usage for higher-order programs


Steffen Jost, Kevin Hammond, Hans-Wolfgang Loidl, and Martin Hofmann (2010)

Static determination of quantitative resource usage for higher-order programs

In: POPL, pp. 223-236.

We describe a new automatic static analysis for determining upper-bound functions on the use of quantitative resources for strict, higher-order, polymorphic, recursive programs dealing$~$ with possibly-aliased data. Our analysis is a variant of Tarjanʼs manual amortised cost analysis technique. We use a type-based approach, exploiting linearity to allow inference, and$~$ place a new emphasis on the number of references to a data object. The bounds we infer depend on the sizes of the various inputs to a program. They thus expose the impact of specific inputs on the overall cost behaviour. The key novel aspect of our work is that it deals directly with polymorphic higher-order functions without requiring source-level transformations that could alter resource usage. We thus$~$ obtain safe and accurate compile-time bounds. Our work is generic in that it deals with a variety of quantitative resources. We illustrate our approach with reference to dynamic memory$~$ allocations / deallocations, stack usage, and worst-case execution time, using metrics taken from a real implementation on a simple micro-controller platform that is used in safety-critical$~$ automotive applications.

Theory, Functional Programming, Resource Analysis, Languages, Reliability, Performance, Types

Document Actions