Sciweavers

Share
POPL
2010
ACM

Static Determination of Quantitative Resource Usage for Higher-Order Programs

9 years 5 months ago
Static Determination of Quantitative Resource Usage for Higher-Order Programs
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 ...
Steffen Jost, Hans-Wolfgang Loidl, Kevin Hammond,
Added 01 Mar 2010
Updated 02 Mar 2010
Type Conference
Year 2010
Where POPL
Authors Steffen Jost, Hans-Wolfgang Loidl, Kevin Hammond, Martin Hofmann
Comments (0)
books