Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Types for Proofs and Programs

TYPES 1999: Types for Proofs and Programs pp 148–161Cite as

Memory Management: An Abstract Formulation of Incremental Tracing

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1956))

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.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Ben-Ari. Algorithms for on-the-fly garbage collection. ACM Transactions on Programming Languages and Systems, 6(3):333–344, July 1984.

    Article  MATH  Google Scholar 

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

    Article  MATH  Google Scholar 

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

    Google Scholar 

  4. G. Gonthier. Verifying the safety of a practical concurrent garbage collector. volume 1102 of Lecture Notes in Computer Science. Springer, July 1996.

    Google Scholar 

  5. P. Jackson. Verifying a garbage collection algorithm. In Proceedings of TPHOLs, 1998.

    Google Scholar 

  6. R. Jones and R. Lins. Garbage Collection: Algorithms for Automatic Dynamic memory Management. John Wiley & Sons, 1996.

    Google Scholar 

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

    Google Scholar 

  8. D. M. Russinoff. A mechanically verified garbage collector. Formal Aspects of Computing, 6:359–390, 1994.

    Article  MATH  Google Scholar 

  9. P. R. Wilson. Uniprocessor garbage collection techniques. ACM Computing Surveys. Accepted, in revision.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. AT&T Labs, 180 Park Ave., Florham Park, NJ, 07932, USA

    Healfdene Goguen, Richard Brooksby & Rod Burstall

  2. Ravenbrook Limited, 51 St. Andrew’s Rd., Cambridge, CB4 1DH, UK

    Healfdene Goguen, Richard Brooksby & Rod Burstall

  3. LFCS, The King’s Buildings, University of Edinburgh, EH9 3JZ, UK

    Healfdene Goguen, Richard Brooksby & Rod Burstall

Authors
  1. Healfdene Goguen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Richard Brooksby
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Rod Burstall
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing Science, Chalmers University of Technology and University of Göteborg, 41296, Göteborg, Sweden

    Thierry Coquand , Peter Dybjer , Bengt Nordström  & Jan Smith , ,  & 

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation