Projects per year
Abstract
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.
Original language | English |
---|---|
Title of host publication | POPL'10 Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages |
Place of Publication | New York |
Publisher | ACM |
Pages | 223-236 |
Number of pages | 14 |
ISBN (Print) | 978-1-60558-479-9 |
DOIs | |
Publication status | Published - 2010 |
Event | 37th ACM-SIGPLAN-SIGACT Symposium on Principles of Programming Languages - Madrid, Spain Duration: 17 Jan 2010 → 23 Jan 2010 |
Conference
Conference | 37th ACM-SIGPLAN-SIGACT Symposium on Principles of Programming Languages |
---|---|
Country/Territory | Spain |
City | Madrid |
Period | 17/01/10 → 23/01/10 |
Keywords
- Functional Programming
- Resource Analysis
- Types
- POLYMORPHIC RECURSION
- COMPLEXITY
Fingerprint
Dive into the research topics of 'Static Determination of Quantitative Resource Usage for Higher-Order Programs'. Together they form a unique fingerprint.Projects
- 1 Finished
-
EP/F030657/1 Adaptive Hardware Systems: Copy of Adaptive Hardware Systems with Novel Algorithmic Design and Guaranteed Resource Bounds
Hammond, K. (PI)
1/09/08 → 31/08/11
Project: Standard