Amortised Memory Analysis Using the Depth of Data Structures

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

Abstract

Hofmann and Jost have presented a heap space analysis [1] that finds linear space bounds for many functional programs. It uses an amortised analysis: assigning hypothetical amounts of free space (called potential) to data structures in proportion to their sizes using type annotations. Constraints on these annotations in the type system ensure that the total potential assigned to the input is an upper bound on the total memory required to satisfy all allocations.

We describe a related system for bounding the stack space requirements which uses the depth of data structures, by expressing potential in terms of maxima as well as sums. This is achieved by adding extra structure to typing contexts (inspired by O’Hearn’s bunched typing [2]) to describe the form of the bounds. We will also present the extra steps that must be taken to construct a typing during the analysis.
Original languageEnglish
Title of host publicationProgramming Languages and Systems
Subtitle of host publication18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings
EditorsGiuseppe Castagna
PublisherSpringer Berlin Heidelberg
Pages190-204
Number of pages15
ISBN (Electronic)978-3-642-00590-9
ISBN (Print)978-3-642-00589-3
DOIs
Publication statusPublished - 2009

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume5502
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint Dive into the research topics of 'Amortised Memory Analysis Using the Depth of Data Structures'. Together they form a unique fingerprint.

Cite this