Amortised Memory Analysis Using the Depth of Data Structures

Brian Campbell

doi:10.1007/978-3-642-00590-9_14

Amortised Memory Analysis Using the Depth of Data Structures

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract / Description of output

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 language	English
Title of host publication	Programming Languages and Systems
Subtitle of host publication	18th 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
Editors	Giuseppe Castagna
Publisher	Springer
Pages	190-204
Number of pages	15
ISBN (Electronic)	978-3-642-00590-9
ISBN (Print)	978-3-642-00589-3
DOIs	https://doi.org/10.1007/978-3-642-00590-9_14
Publication status	Published - 2009

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin Heidelberg
Volume	5502
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

10.1007/978-3-642-00590-9_14

depthAccepted author manuscript, 256 KB

http://dx.doi.org/10.1007/978-3-642-00590-9_14

ReQueST: ReQueST:Resource Quantification in e-science Technologies.
Sannella, D., Aspinall, D., Gilmore, S. & Stark, I.
EPSRC
1/05/05 → 31/01/09
Project: Research

Cite this

Campbell, B. (2009). Amortised Memory Analysis Using the Depth of Data Structures. In G. Castagna (Ed.), Programming Languages and Systems: 18th 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 (pp. 190-204). (Lecture Notes in Computer Science; Vol. 5502). Springer. https://doi.org/10.1007/978-3-642-00590-9_14

Campbell, Brian. / Amortised Memory Analysis Using the Depth of Data Structures. Programming Languages and Systems: 18th 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. editor / Giuseppe Castagna. Springer, 2009. pp. 190-204 (Lecture Notes in Computer Science).

@inproceedings{b1eb4c62ef214c92bc6ee2defe274f47,

title = "Amortised Memory Analysis Using the Depth of Data Structures",

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{\textquoteright}Hearn{\textquoteright}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.",

author = "Brian Campbell",

year = "2009",

doi = "10.1007/978-3-642-00590-9_14",

language = "English",

isbn = "978-3-642-00589-3",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "190--204",

editor = "Giuseppe Castagna",

booktitle = "Programming Languages and Systems",

address = "United Kingdom",

}

Campbell, B 2009, Amortised Memory Analysis Using the Depth of Data Structures. in G Castagna (ed.), Programming Languages and Systems: 18th 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. Lecture Notes in Computer Science, vol. 5502, Springer, pp. 190-204. https://doi.org/10.1007/978-3-642-00590-9_14

Amortised Memory Analysis Using the Depth of Data Structures. / Campbell, Brian.
Programming Languages and Systems: 18th 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. ed. / Giuseppe Castagna. Springer, 2009. p. 190-204 (Lecture Notes in Computer Science; Vol. 5502).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Amortised Memory Analysis Using the Depth of Data Structures

AU - Campbell, Brian

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-642-00590-9_14

DO - 10.1007/978-3-642-00590-9_14

M3 - Conference contribution

SN - 978-3-642-00589-3

T3 - Lecture Notes in Computer Science

SP - 190

EP - 204

BT - Programming Languages and Systems

A2 - Castagna, Giuseppe

PB - Springer

ER -

Campbell B. Amortised Memory Analysis Using the Depth of Data Structures. In Castagna G, editor, Programming Languages and Systems: 18th 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. Springer. 2009. p. 190-204. (Lecture Notes in Computer Science). doi: 10.1007/978-3-642-00590-9_14

Amortised Memory Analysis Using the Depth of Data Structures

Abstract / Description of output

Publication series

Access to Document

Fingerprint

Projects

ReQueST: ReQueST:Resource Quantification in e-science Technologies.

Cite this