research-article

Open access

Local reasoning about a copying garbage collector

Authors:

Noah Torp-Smith,

John C. ReynoldsAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 30, Issue 4

Article No.: 24, Pages 1 - 58

https://doi.org/10.1145/1377492.1377499

Published: 01 August 2008 Publication History

Abstract

We present a programming language, model, and logic appropriate for implementing and reasoning about a memory management system. We state semantically what is meant by correctness of a copying garbage collector, and employ a variant of the novel separation logics to formally specify partial correctness of Cheney's copying garbage collector in our program logic. Finally, we prove that our implementation of Cheney's algorithm meets its specification using the logic we have given and auxiliary variables.

References

[1]

Aditya, S. and Caro, A. 1993. Compiler-directed type reconstruction for polymorphic languages. In Proceedings of the Conference on Functional Programming Languages and Computer Architecture (FPCA'93). Copenhagen, Denmark. ACM Press, 74--82.]]

Digital Library

[2]

Aditya, S., Flood, C. H., and Hicks, J. E. 1994. Garbage collection for strongly-typed languages using run-time type reconstruction. In Proceedings of the ACM Conference on LISP and Functional Programming (LFP'94). Orlando, FL, ACM Press, 12--23.]]

Digital Library

[3]

Ahmed, A., Jia, L., and Walker, D. 2003. Reasoning about hierarchical storage. In Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science (LICS'03). Ottawa, Canada. IEEE Press.]]

Digital Library

[4]

Appel, A. W. 2001. Foundational proof carrying code. In Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS'01). Boston, MA. IEEE Press.]]

Digital Library

[5]

Appel, A. W. and Gonçalves, M. J. R. 1993. Hash-consing garbage collection. Tech. rep. CS-TR-412-93, Princeton University.]]

[6]

Ben-Ari, M. 1984. Algorithms for on-the-fly garbage collection. ACM Trans. Program. Lang. Syst. 6, 3, 333--344.]]

Digital Library

[7]

Berdine, J., Calcagno, C., and O'Hearn, P. W. 2005. Symbolic execution with separation logic. In Proceedings of the 3rd Asian Symposium on Programming Languages and Systems (APLAS'05), Tsukuba, Japan. Springer Verlag, 52--68.]]

Digital Library

[8]

Biering, B., Birkedal, L., and Torp-Smith, N. 2005. BI-hyperdoctrines and higher order separation logic. In Proceedings of the European Symposium on Programming (ESoP'05). Edinburgh, Scotland, 233--247.]]

Digital Library

[9]

Birkedal, L., Torp-Smith, N., and Reynolds, J. 2004. Local reasoning about a copying garbage collector. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'04). Venice, Italy, 220--231.]]

Digital Library

[10]

Birkedal, L., Torp-Smith, N., and Yang, H. 2005. Semantics of separation-logic typing and higher-order frame rules. In Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS'05), Chicago, IL. IEEE Press, 260--269.]]

Digital Library

[11]

Bornat, R. 2000. Proving pointer programs in Hoare logic. In Proceedings of the 5th International Conference on Mathematics of Program Construction. Vol. 1837. Lecture Notes In Computer Science, Springer Verlag, 102--126.]]

Digital Library

[12]

Bornat, R. 2003. Correctness of copydag via local reasoning. Private Communication.]]

[13]

Bornat, R., Calcagno, C., and O'Hearn, P. 2004. Local reasoning, separation and aliasing. In Proceedings of the Conference on Semantics, Program Analysis, and Computing Environments (SPACE'04). Venice, Italy.]]

[14]

Burdy, L. 2001. B vs Coq to prove a garbage collector. In Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'01). Lecture Notes in Computer Science, Vol. 2152. Springer Verlag.]]

[15]

Calcagno, C., Ishtiaq, S., and O'Hearn, P. W. 2000. Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic. In Proceedings of the 2nd International Conference on Principles and Practice of Declarative Programming (PPDP'00). Montreal, Canada.]]

Digital Library

[16]

Calcagno, C., O'Hearn, P. W., and Bornat, R. 2003. Program logic and equivalence in the presence of garbage collection. Theor. Comput. Sci. 298, 3, 557--587.]]

Digital Library

[17]

Cheney, C. J. 1970. A nonrecursive list compacting algorithm. Comm. ACM 13, 11, 677--678.]]

Digital Library

[18]

Coupet-Grimal, S. 2003. C. nouvet. J. Logic Comput. 13, 6, 815--833.]]

[19]

Crary, K., Walker, D., and Morrisett, G. 1999. Typed memory management in a calculus of capabilities. In Proceedings of the 26th ACM SIGPLAN-SIGACT on Principles of Programming Languages (POPL'99). San Antonio, TX. 262--275.]]

Digital Library

[20]

Dijkstra, E. W., Lamport, L., Martin, A. J., Scholten, G. S., and Steffens, E. M. F. 1978. On-the-fly garbage collection: an exercise in cooperation. Comm. ACM 21, 11, 965--975.]]

Digital Library

[21]

Fluet, M. and Wang, D. 2004. Implementation and performance evaluation of a safe runtime system in Cyclone. In Informal Proceedings of the 2nd Workshop on Semantics, Program Analysis and Computing Environments for Memory Management (SPACE'04). Venice, Italy. ACM/SIGPLAN.]]

[22]

Goto, E. 1974. Monocopy and associative algorithms in extended lisp. Tech. rep. TR 74-03, University of Tokyo.]]

[23]

Gries, D. and Levin, G. 1980. Assignment and procedure call proof rules. ACM Trans. Program. Lang. Syst. 2, 4, 564--579.]]

Digital Library

[24]

Guttmann, J., Ramsdell, J., and Wand, M. 1994. VLISP: A verified implementation of scheme. Lisp Symb. Comput. 8, 1--2, 5--32.]]

Digital Library

[25]

Guttmann, J. D., Monk, L. G., Ramsdell, J. D., Farmer, W. M., and Swarup, V. 1992. A guide to VLISP, a verified programming language implementation. Tech. rep. M92B091, The MITRE Corporation.]]

[26]

Hallenberg, N., Elsman, M., and Tofte, M. 2002. Combining region inference and garbage collection. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'02). Berlin, Germany. ACM Press.]]

Digital Library

[27]

Havelund, K. 1999. Mechanical verification of a garbage collector. In Proceedings of the 4th International Workshop on Formal Methods for Parallel Programming: Theory and Applications (FMPPTA'99). San Juan, Puerto Rico.]]

Digital Library

[28]

Hawblitzel, C., Wei, E., Huang, H., Krupski, E., and Wittie, L. 2004. Low-level linear memory management. In Proceedings of the Conference on Semantics, Program Analysis, and Computing Environments (SPACE'04). Venice, Italy.]]

[29]

Hoare, C. A. R. 1969. An axiomatic approach to computer programming. Comm. ACM 12, 583, 576--580.]]

Digital Library

[30]

Jackson, P. B. 1998. Verifying a garbage collection algorithm. In Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'98), Lecture Notes in Computer Science, vol. 1479, Springer Verlag, 225--244.]]

Digital Library

[31]

Jim, T., Morrisett, G., Grossman, D., Hicks, M., Cheney, J., and Wang, Y. 2002. Cyclone: A safe dialect of C. In Proceedings of the USENIX Annual Technical Conference. Monterey, CA. 275--288.]]

Digital Library

[32]

Mehta, F. and Nipkow, T. 2003. Proving pointer programs in higher-order logic. In Proceedings of the Conference on Automated Deduction (CADE-19).]]

[33]

Monnier, S. and Shao, Z. 2002. Typed regions. Tech. rep. YALEU/DCS/TR-1242, Department of Computer Science, Yale University, New Haven, CT.]]

[34]

Morrisett, G., Felleisen, M., and Harper, R. 1995. Abstract models of memory management. In Proceedings of the 7th International Conference on Functional Programming Languages and Computer Architecture (FPCA'95), La Jolla, CA. ACM Press, 66--77.]]

Digital Library

[35]

Morrisett, G., Walker, D., Crary, K., and Glew, N. 1999. From system F to typed assembly language. ACM Trans. Program. Lang. Syst. 21, 3, 527--568.]]

Digital Library

[36]

Necula, G. C. 1997. Proof-carrying code. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'97). Paris, France, 106--119.]]

Digital Library

[37]

Necula, G. C. and Lee, P. 1996. Safe kernel extensions without run-time checking. In Proceedings of the 2nd USENIX Symposium on Operating Systems Design and Implementation (OSDI'96). Berkeley, CA. 229--243.]]

Digital Library

[38]

O'Hearn, P. W. 2004. Resources, concurrency and local reasoning. In Proceedings of the 15th International Conference on Concurrency Theory (CONCUR'04), Lecture Notes in Computer Science, vol. 3170, 49--67.]]

[39]

O'Hearn, P. W., Reynolds, J. C., and Yang, H. 2001. Local reasoning about programs that alter data structures. In Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL'01). Berlin, Germany.]]

Digital Library

[40]

Owicki, S. and Gries, D. 1976. An axiomatic proof technique for parallel programs. Acta Informatica 6, 4, 319--340.]]

Digital Library

[41]

Petersen, L., Harper, R., Crary, K., and Pfenning, F. 2003. A type theory for memory allocation and data layout. In Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'03). New Orleans, LA. 172--184.]]

Digital Library

[42]

Pixley, C. 1988. An incremental garbage collection algorithm for multimutator systems. Distrib. Comput. 3, 1, 41--50.]]

Digital Library

[43]

Pym, D. 2002. The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logics Series. vol. 26, Kluwer.]]

[44]

Reynolds, J. C. 1981. The Craft of Programming. Prentice-Hall International Series in Computer Science. Prentice-Hall.]]

Digital Library

[45]

Reynolds, J. C. 2002. Separation logic: A logic for shared mutable data structures. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02). Copenhagen, Denmark. IEEE Press, 55--74.]]

Digital Library

[46]

Russinoff, D. M. 1994. A mechanically verified incremental garbage collector. Formal Aspects Comput. 6, 359--390.]]

Digital Library

[47]

Smith, F., Walker, D., and Morrisett, G. 2000. Alias types. In Proceedings of the 9th European Symposium on Programming Languages and Systems (ESOP'00). Berlin, Germany. 366--381.]]

Digital Library

[48]

Stoyle, G., Hicks, M., Bierman, G., Sewell, P., and Neamtiu, I. 2005. Mutatis mutandis: Safe and predictable dynamic software updating. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'05). Long Beach, CA. ACM Press, 183--194.]]

Digital Library

[49]

Swarup, V., Farmer, W. M., Guttmann, J. D., Monk, L. G., and Ramsdell, J. D. 1992. The VLISP byte-code interpreter. Tech. rep. M 92B096, The MITRE Corporation.]]

[50]

Tofte, M. and Birkedal, L. 1998. A region inference algorithm. ACM Trans. Program. Lang. Syst. 20, 4, 734--767.]]

Digital Library

[51]

Tofte, M., Birkedal, L., Elsman, M., and Hallenberg, N. 2004. A retrospective on region-based memory management. Higher-Order Symb. Comput. 17, 3, 245--265.]]

Digital Library

[52]

Tofte, M. and Talpin, J.-P. 1994. Implementation of the call-by-value lambda-calculus using a stack of regions. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'94), Portland, OR. 188--201.]]

Digital Library

[53]

Wadler, P. L. 1976. Analysis of an algorithm for real time garbage collection. Comm. ACM 19, 9, 491--500.]]

Digital Library

[54]

Wang, D. and Appel, A. W. 2001. Type preserving garbage collectors. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'01). London, UK. 166--178.]]

Digital Library

[55]

Weber, T. 2004. Towards mechanized program verification with separation logic. In Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL'04). Karpacz, Poland.]]

[56]

Yang, H. 2001. Local reasoning for stateful programs. Ph. D. thesis, University of Illinois, Urbana-Champaign.]]

Digital Library

Cited By

Zakowski YCachera DDemange DPetri GPichardie DJagannathan SVitek J(2019)Verifying a Concurrent Garbage Collector with a Rely-Guarantee MethodologyJournal of Automated Reasoning10.1007/s10817-018-9489-x63:2(489-515)Online publication date: 1-Aug-2019
https://dl.acm.org/doi/10.1007/s10817-018-9489-x
Jones CYatapanage N(2019)Investigating the limits of rely/guarantee relations based on a concurrent garbage collector exampleFormal Aspects of Computing10.1007/s00165-019-00482-331:3(353-374)Online publication date: 1-Jun-2019
https://dl.acm.org/doi/10.1007/s00165-019-00482-3
Jones CVelykis AYatapanage N(2017)General Lessons from a Rely/Guarantee DevelopmentDependable Software Engineering. Theories, Tools, and Applications10.1007/978-3-319-69483-2_1(3-22)Online publication date: 17-Oct-2017
https://doi.org/10.1007/978-3-319-69483-2_1
Show More Cited By

Index Terms

Local reasoning about a copying garbage collector
1. Software and its engineering
  1. Software creation and management
    1. Software post-development issues
      1. Documentation
2. Theory of computation
  1. Logic
    1. Programming logic
  2. Semantics and reasoning
    1. Program reasoning
      1. Assertions
      2. Program specifications

Recommendations

Local reasoning about a copying garbage collector
POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We present a programming language, model, and logic appropriate for implementing and reasoning about a memory management system. We then state what is meant by correctness of a copying garbage collector, and employ a variant of the novel separation ...
Local reasoning about a copying garbage collector
POPL '04

We present a programming language, model, and logic appropriate for implementing and reasoning about a memory management system. We then state what is meant by correctness of a copying garbage collector, and employ a variant of the novel separation ...
Jade: A High-throughput Concurrent Copying Garbage Collector
EuroSys '24: Proceedings of the Nineteenth European Conference on Computer Systems

Garbage collection (GC) pauses are a notorious issue threatening the latency of applications. To mitigate this problem, state-of-the-art concurrent copying collectors allow GC threads to run simultaneously with application threads (mutators) in nearly ...

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 30, Issue 4

July 2008

358 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/1377492

Issue’s Table of Contents

Copyright © 2008 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 August 2008

Accepted: 01 August 2006

Revised: 01 November 2005

Received: 01 July 2004

Published in TOPLAS Volume 30, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Danish Natural Science Research Council
Danish Technical Research Council
National Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

21
Total Citations
View Citations
562
Total Downloads

Downloads (Last 12 months)59
Downloads (Last 6 weeks)11

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Zakowski YCachera DDemange DPetri GPichardie DJagannathan SVitek J(2019)Verifying a Concurrent Garbage Collector with a Rely-Guarantee MethodologyJournal of Automated Reasoning10.1007/s10817-018-9489-x63:2(489-515)Online publication date: 1-Aug-2019
https://dl.acm.org/doi/10.1007/s10817-018-9489-x
Jones CYatapanage N(2019)Investigating the limits of rely/guarantee relations based on a concurrent garbage collector exampleFormal Aspects of Computing10.1007/s00165-019-00482-331:3(353-374)Online publication date: 1-Jun-2019
https://dl.acm.org/doi/10.1007/s00165-019-00482-3
Jones CVelykis AYatapanage N(2017)General Lessons from a Rely/Guarantee DevelopmentDependable Software Engineering. Theories, Tools, and Applications10.1007/978-3-319-69483-2_1(3-22)Online publication date: 17-Oct-2017
https://doi.org/10.1007/978-3-319-69483-2_1
Gammie PHosking AEngelhardt K(2015)Relaxing safely: verified on-the-fly garbage collection for x86-TSOACM SIGPLAN Notices10.1145/2813885.273800650:6(99-109)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1145/2813885.2738006
Gammie PHosking AEngelhardt KGrove DBlackburn S(2015)Relaxing safely: verified on-the-fly garbage collection for x86-TSOProceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2737924.2738006(99-109)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1145/2737924.2738006
Hobor AVillard J(2013)The ramifications of sharing in data structuresACM SIGPLAN Notices10.1145/2480359.242913148:1(523-536)Online publication date: 23-Jan-2013
https://dl.acm.org/doi/10.1145/2480359.2429131
Hobor AVillard JGiacobazzi RCousot R(2013)The ramifications of sharing in data structuresProceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/2429069.2429131(523-536)Online publication date: 23-Jan-2013
https://dl.acm.org/doi/10.1145/2429069.2429131
Loulergue FGava FKosmatov NLemerre M(2012)Towards verified cloud computing environments2012 International Conference on High Performance Computing & Simulation (HPCS)10.1109/HPCSim.2012.6266896(91-97)Online publication date: Jul-2012
https://doi.org/10.1109/HPCSim.2012.6266896
Gast H(2011)Developer-oriented correctness proofs a case study of Cheney's algorithmProceedings of the 13th international conference on Formal methods and software engineering10.5555/2075089.2075131(489-504)Online publication date: 26-Oct-2011
https://dl.acm.org/doi/10.5555/2075089.2075131
Hur CDreyer DBall TSagiv M(2011)A kripke logical relation between ML and assemblyProceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/1926385.1926402(133-146)Online publication date: 26-Jan-2011
https://dl.acm.org/doi/10.1145/1926385.1926402
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Figures

Tables

Media

View Issue’s Table of Contents