Static Determination of Quantitative Resource Usage for Higher-Order Programs

Steffen Jost, Kevin Hammond, Hans-Wolfgang Loidl, Martin Hofmann

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 languageEnglish
Title of host publicationPOPL'10 Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
Place of PublicationNew York
PublisherACM
Pages223-236
Number of pages14
ISBN (Print)978-1-60558-479-9
DOIs
Publication statusPublished - 2010
Event37th ACM-SIGPLAN-SIGACT Symposium on Principles of Programming Languages - Madrid, Spain
Duration: 17 Jan 201023 Jan 2010

Conference

Conference37th ACM-SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Country/TerritorySpain
CityMadrid
Period17/01/1023/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.

Cite this