Automatic Amortised Analysis of Dynamic Memory Allocation for Lazy Functional Programs

• Tipo: Artigo em Revista Científica Internacional
• Data: 2012

Autores

Hugo Simoes (Autor) Outra; Pedro Vasconcelos (Autor) FCUP; Mario Florido (Autor) FCUP; Steffen Jost (Autor) Outra; Kevin Hammond (Autor) Outra

Revista

Título: SIGPLAN Notices (ACM Special Interest Group on Programming Languages)

Vol. 47

Páginas: 165-176

ISSN: 0362-1340

Editora: Special Interest Group on Computer Graphics, Association for Computing Machinery

Indexação

ISI Web of Knowledge - 15 Citações

Scopus - 9 Citações

Classificação Científica

FOS: Ciências exactas e naturais > Ciências da computação e da informação

Outras Informações

ID Authenticus: P-002-5N6

DOI: 10.1145/2398856.2364575

Abstract (EN): This paper describes the first successful attempt, of which we are aware, to define an automatic, type-based static analysis of resource bounds for lazy functional programs. Our analysis uses the automatic amortisation approach developed by Hofmann and Jost, which was previously restricted to eager evaluation. In this paper, we extend this work to a lazy setting by capturing the costs of unevaluated expressions in type annotations and by amortising the payment of these costs using a notion of lazy potential. We present our analysis as a proof system for predicting heap allocations of a minimal functional language (including higher-order functions and recursive data types) and define a formal cost model based on Launchbury's natural semantics for lazy evaluation. We prove the soundness of our analysis with respect to the cost model. Our approach is illustrated by a number of representative and non-trivial examples that have been analysed using a prototype implementation of our analysis.

Idioma: Inglês

Tipo (Avaliação Docente): Científica

Nº de páginas: 12