Abstract
We present an abstract model of computer memory, in the form of directed, labeled graphs with simple transitions corresponding to valid memory operations. We also introduce a refinement of this basic model of memory that incorporates features of memory management. After giving some examples of how this refined model captures various incremental tracing algorithms, we investigate properties of the two representations and show that they are behaviorally equivalent. The proofs have been formally verified in the proof assistant Coq.
Most of this author’s work was carried out at the LFCS, The King’s Buildings, University of Edinburgh, EH9 3JZ, UK.
This author was at Harlequin Ltd. at the time of the collaboration.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Ben-Ari. Algorithms for on-the-fly garbage collection. ACM Transactions on Programming Languages and Systems, 6(3):333–344, July 1984.
E. W. Dijkstra, L. Lamport, A. J. Martin, C. S. Scholten, and E. F. M. Steffens. On-the-fly garbage collection: An exercise in cooperation. Communications of the Association for Computing Machinery, 21(11):966–975, November 1978.
Dowek, Felty, Herbelin, Huet, Murthy, Parent, Paulin-Mohring, and Werner. The Coq proof assistant user’s guide, version 5.8. Technical report, INRIA-Rocquencourt, Feb. 1993.
G. Gonthier. Verifying the safety of a practical concurrent garbage collector. volume 1102 of Lecture Notes in Computer Science. Springer, July 1996.
P. Jackson. Verifying a garbage collection algorithm. In Proceedings of TPHOLs, 1998.
R. Jones and R. Lins. Garbage Collection: Algorithms for Automatic Dynamic memory Management. John Wiley & Sons, 1996.
G. Morrisett, M. Felleisen, and R. Harper. Abstract models of memory management. In Functional Programming and Computer Architecture, pages 66–77, La Jolla, CA, June 1995. ACM.
D. M. Russinoff. A mechanically verified garbage collector. Formal Aspects of Computing, 6:359–390, 1994.
P. R. Wilson. Uniprocessor garbage collection techniques. ACM Computing Surveys. Accepted, in revision.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Goguen, H., Brooksby, R., Burstall, R. (2000). Memory Management: An Abstract Formulation of Incremental Tracing. In: Coquand, T., Dybjer, P., Nordström, B., Smith, J. (eds) Types for Proofs and Programs. TYPES 1999. Lecture Notes in Computer Science, vol 1956. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44557-9_9
Download citation
DOI: https://doi.org/10.1007/3-540-44557-9_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41517-6
Online ISBN: 978-3-540-44557-9
eBook Packages: Springer Book Archive