Article

A general framework for certifying garbage collectors and their mutators

Authors:

Andrew McCreight,

Long LiAuthors Info & Claims

PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 468 - 479

https://doi.org/10.1145/1250734.1250788

Published: 10 June 2007 Publication History

Abstract

Garbage-collected languages such as Java and C# are becoming more and more widely used in both high-end software and real-time embedded applications. The correctness of the GC implementation is essential to the reliability and security of a large portion of the world's mission-critical software. Unfortunately, garbage collectors--especially incremental and concurrent ones--are extremely hard to implement correctly. In this paper, we present a new uniform approach to verifying the safety of both a mutator and its garbage collector in Hoare-style logic. We define a formal garbage collector interface general enough to reason about a variety of algorithms while allowing the mutator to ignore implementation-specific details of the collector. Our approach supports collectors that require read and write barriers. We have used our approach to mechanically verify assembly implementations of mark-sweep, copying and incremental copying GCs in Coq, as well as sample mutator programs that can be linked with any of the GCs to produce a fully-verified garbage-collected program. Our work provides a foundation for reasoning about complex mutator-collector interaction and makes an important advance toward building fully certified production-quality GCs.

References

[1]

A.W. Appel. Foundational proof-carrying code. In Symp. on Logic in Comp. Sci. (LICS'01), pages 247--258. IEEE Comp. Soc., June 2001.

Digital Library

[2]

H.G. Baker, Jr. List processing in real time on a serial computer. Commun. ACM, 21(4):280--294, 1978.

Digital Library

[3]

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

Digital Library

[4]

L. Birkedal, N. Torp-Smith, and J.C. Reynolds. Local reasoning about a copying garbage collector. In POPL '04: Proc. of the 31st ACM SIGPLAN-SIGACT symp. on Principles of prog. lang., pages 220--231, New York, NY, USA, 2004. ACM Press.

Digital Library

[5]

H.-J. Boehm and M. Weiser. Garbage collection in an uncooperative environment. Software Practice and Exp., 18(9):807--820, 1988.

Digital Library

[6]

R.A. Brooks. Trading data space for reduced time and code space in real-time garbage collection on stock hardware. In LFP '84: Proc. of the 1984 ACM Symp. on LISP and functional prog., pages 256--262, New York, NY, USA, 1984. ACM Press.

Digital Library

[7]

L. Burdy. B vs. Coq to prove a garbage collector. In RJ. Boulton and PB. Jackson, editors, 14th Int'l Conference on Theorem Proving in Higher Order Logics: Supplemental Proc., pages 85--97, Sept. 2001. Report EDI-INF-RR-0046, Division of Informatics, University of Edinburgh.

[8]

C. Calcagno, P. O'Hearn, and R. Bornat. Program logic and equivalence in the presence of garbage collection. Theoretical Comp. Sci., 298(3):557--581, 2003.

Digital Library

[9]

J. Chen and D. Tarditi. A simple typed intermediate language for object-oriented languages. In POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 38--49, New York, NY, USA, 2005. ACM Press.

Digital Library

[10]

Coq Development Team. The Coq proof assistant reference manual. Coq release v8.0, Oct. 2005.

[11]

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. Commun. ACM, 21(11):966--975, 1978.

Digital Library

[12]

X. Feng, Z. Ni, Z. Shao, and Y. Guo. An open framework for foundational proof-carrying code. In The third ACM SIGPLAN Workshop on Types in Language Design and Implementation, pages 67--78, Nice, France, Jan. 2007. ACM Press.

Digital Library

[13]

X. Feng, Z. Shao, A. Vaynberg, S. Xiang, and Z. Ni. Modular verif. of assembly code with stack-based control abstractions. In Proc. 2006 ACM Conf. on Prog. Lang. Design and Impl., June 2006.

Digital Library

[14]

G. Gonthier. Verifying the safety of a practical concurrent garbage collector. In RAlur and THenzinger, editors, Computer Aided Verification CAV'96, Lecture Notes in Computer Science, New Brunswick, NJ, 1996. Springer-Verlag.

Digital Library

[15]

J. Gosling, B. Joy, G. Steele, and G. Bracha. The Java Language Specification Second Edition. Addison-Wesley, Boston, Mass., 2000.

Digital Library

[16]

D. Gries. An exercise in proving parallel programs correct. Commun. ACM, 20(12):921--930, 1977.

Digital Library

[17]

D. Gries. Corrigendum. Commun. ACM, 21(12):1048, 1978.

Digital Library

[18]

J. Guy, L. Steele. Multiprocessing compactifying garbage collection. Commun. ACM, 18(9):495--508, 1975.

Digital Library

[19]

K. Havelund. Mechanical verification of a garbage collector. In FMPPTA'99, 1999.

Digital Library

[20]

C. Hawblitzel, H. Huang, L. Wittie, and J. Chen. A garbage-collecting typed assembly language. In The Third ACM SIGPLAN Workshop on Types in Lang. Design and Impl. ACM Press, Jan. 2007.

Digital Library

[21]

A. Hejlsberg, S. Wiltamuth, and P. Golde. The C# Programming Language. Addison-Wesley, Boston, Mass., 2004.

[22]

G. Hunt, J. Larus, M. Abadi, M. Aiken, P. Barham, M. Fahndrich, C. Hawblitzel, O. Hodson, S. Levi, N. Murphy, B. Steensgaard, D. Tarditi, T. Wobber, and B. Zill. An overview of the Singularity project. Technical Report MSR-TR-2005-135, Microsoft Research, Redmond, WA, 2005.

[23]

R. Hunter and S. Krishnamurthi. A model of garbage collection for oo languages. In Tenth Int'l Workshop on Foundations of Object-Oriented Lang. (FOOL10), 2003.

[24]

P. Jackson. Verifying a garbage collection algorithm. In Proc. of 11th Int'l Conference on Theorem Proving in Higher Order Logics TPHOLs'98, volume 1479 of Lecture Notes in Computer Science, pages 225--244, Canberra, Sept. 1998. Springer-Verlag.

Digital Library

[25]

C.B. Jones. Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst., 5(4):596--619, 1983.

Digital Library

[26]

R.E. Jones. Garbage Collection: Algorithms for Automatic Dynamic Memory Management. Wiley, Chichester, July 1996. With a chapter on Distributed Garbage Collection by R. Lins.

Digital Library

[27]

C. Lin, A. McCreight, Z. Shao, Y. Chen, and Y. Guo. Foundational typed assembly language with certified garbage collection. In 1st IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE 2007), June 2007.

Digital Library

[28]

A. McCreight, Z. Shao, C. Lin, and L. Li. A general framework for certifying garbage collectors and their mutators (extended version). Technical Report YALEU/DCS/TR-1378, Yale University, New Haven, CT, Mar. 2007.

[29]

A. McCreight, Z. Shao, C. Lin, and L. Li. A general framework for certifying garbage collectors and their mutators (implementation). http://flint.cs.yale.edu/flint/publications/hgc.html, Jan. 2007.

Digital Library

[30]

S. Monnier, B. Saha, and Z. Shao. Principled scavenging. In Proc. 2001 ACM Conf. on Prog. Lang. Design and Impl., pages 81--91, New York, 2001. ACM Press.

Digital Library

[31]

S. Monnier and Z. Shao. Typed regions. Technical Report YALEU/DCS/TR-1242, Dept. of Comp. Sci., Yale University, New Haven, CT, Oct. 2002.

[32]

G. Morrisett, M. Felleisen, and R. Harper. Abstract models of memory management. In FPCA '95: Proc. of the 7th Int'l conference on Functional prog. lang. and comp. architecture, pages 66--77, New York, NY, USA, 1995. ACM Press.

Digital Library

[33]

G. Morrisett, D. Walker, K. Crary, and N. Glew. From system F to typed assembly language. ACM Transactions on Programming Languages and Systems, 21(3):527--568, 1999.

Digital Library

[34]

Mozilla. Mozilla foundation security advisory 2006-01. http://www.mozilla.org/security/announce/2006/mfsa2006-01.html.

[35]

L.P. Nieto and J. Esparza. Verifying single and multi-mutator garbage collectors with owicki-gries in isabelle/hol. In MFCS '00: Proc. of the 25th Int'l Symp. on Mathematical Foundations of Comp. Sci., pages 619--628, London, UK, 2000. Springer-Verlag.

Digital Library

[36]

NIST. Vulnerability summary cve-2006-3451. http://nvd.nist.gov/nvd.cfm?cvename=CVE-2006-3451.

[37]

P.W. O'Hearn, H. Yang, and J.C. Reynolds. Separation and information hiding. In POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 268--280, New York, NY, USA, 2004. ACM Press.

Digital Library

[38]

W. Paul, M. Broy, and T. In der Rieden. The verisoft project. http://www.verisoft.de, 2007.

[39]

C. Paulin-Mohring. Inductive definitions in the system Coq-rules and properties. In Proc. TLCA, volume 664 of Lecture Notes in Computer Science, 1993.

Digital Library

[40]

J.C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS '02: Proc. of the 17th Annual IEEE Symp. on Logic in Comp. Sci., pages 55--74, Washington, DC, USA, 2002. IEEE Computer Society.

Digital Library

[41]

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

[42]

J.C. Vanderwaart and K. Crary. A typed interface for garbage collection. In TLDI '03: Proc. of the 2003 ACM SIGPLAN Int'l Workshop on Types in Lang. Design and Impl., pages 109--122, New York, NY, USA, 2003. ACM Press.

Digital Library

[43]

M.T. Vechev, E. Yahav, and D.F. Bacon. Correctness-preserving derivation of concurrent garbage collection algorithms. In PLDI '06: Proc. of the 2006 ACM SIGPLAN conference on Prog. Lang. Design and Impl., pages 341--353, New York, NY, USA, 2006. ACM Press.

Digital Library

[44]

D.C. Wang and A.W. Appel. Type-preserving garbage collectors. In Proc. of the 28th ACM Symp. on Principles of prog. lang., pages 166--178, New York, NY, USA, 2001. ACM Press.

Digital Library

[45]

D. Yu and Z. Shao. Verification of safety properties for concurrent assembly code. In Proc. 9th ACM SIGPLAN International Conference on Functional Programming, September 2004.

Digital Library

[46]

T. Yuasa. Real-time garbage collection on general-purpose machines. J. Syst. Softw., 11(3):181--198, 1990.

Digital Library

Cited By

Madiot JPottier F(2022)A separation logic for heap space under garbage collectionProceedings of the ACM on Programming Languages10.1145/34986726:POPL(1-28)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498672
Charguéraud A(2020)Separation logic for sequential programs (functional pearl)Proceedings of the ACM on Programming Languages10.1145/34089984:ICFP(1-34)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408998
Appel ANaumann DDing CMaas M(2020)Verified sequential Malloc/FreeProceedings of the 2020 ACM SIGPLAN International Symposium on Memory Management10.1145/3381898.3397211(48-59)Online publication date: 16-Jun-2020
https://dl.acm.org/doi/10.1145/3381898.3397211
Show More Cited By

Index Terms

A general framework for certifying garbage collectors and their mutators
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Correctness
      2. Formal methods
2. Theory of computation
  1. Logic
    1. Proof theory
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

Automated verification of practical garbage collectors
POPL '09

Garbage collectors are notoriously hard to verify, due to their low-level interaction with the underlying system and the general difficulty in reasoning about reachability in graphs. Several papers have presented verified collectors, but either the ...
A study of the scalability of stop-the-world garbage collectors on multicores
ASPLOS '13

Large-scale multicore architectures create new challenges for garbage collectors (GCs). In particular, throughput-oriented stop-the-world algorithms demonstrate good performance with a small number of cores, but have been shown to degrade badly beyond ...
A general framework for certifying garbage collectors and their mutators
Proceedings of the 2007 PLDI conference

Garbage-collected languages such as Java and C# are becoming more and more widely used in both high-end software and real-time embedded applications. The correctness of the GC implementation is essential to the reliability and security of a large ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2007

508 pages

ISBN:9781595936332

DOI:10.1145/1250734

General Chair:
Jeanne Ferrante
University of California, San Diego, USA
,
Program Chair:
Kathryn S. McKinley
University of Texas at Austin, USA

ACM SIGPLAN Notices Volume 42, Issue 6
Proceedings of the 2007 PLDI conference
June 2007
491 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1273442
Issue’s Table of Contents

Copyright © 2007 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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 10 June 2007

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

PLDI '07

Sponsor:

PLDI '07: ACM SIGPLAN Conference on Programming Language Design and Implementation

June 10 - 13, 2007

California, San Diego, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

67
Total Citations
View Citations
538
Total Downloads

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

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Madiot JPottier F(2022)A separation logic for heap space under garbage collectionProceedings of the ACM on Programming Languages10.1145/34986726:POPL(1-28)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498672
Charguéraud A(2020)Separation logic for sequential programs (functional pearl)Proceedings of the ACM on Programming Languages10.1145/34089984:ICFP(1-34)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408998
Appel ANaumann DDing CMaas M(2020)Verified sequential Malloc/FreeProceedings of the 2020 ACM SIGPLAN International Symposium on Memory Management10.1145/3381898.3397211(48-59)Online publication date: 16-Jun-2020
https://dl.acm.org/doi/10.1145/3381898.3397211
Kokologiannakis MRaad AVafeiadis V(2019)Effective lock handling in stateless model checkingProceedings of the ACM on Programming Languages10.1145/33605993:OOPSLA(1-26)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360599
Near JDarais DAbuah CStevens TGaddamadugu PWang LSomani NZhang MSharma NShan ASong D(2019)Duet: an expressive higher-order language and linear type system for statically enforcing differential privacyProceedings of the ACM on Programming Languages10.1145/33605983:OOPSLA(1-30)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360598
Wang SCao QMohan AHobor A(2019)Certifying graph-manipulating C programs via localizations within data structuresProceedings of the ACM on Programming Languages10.1145/33605973:OOPSLA(1-30)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360597
Wang YHu XZou ZTan WTan G(2019)IVT: an efficient method for sharing subtype polymorphic objectsProceedings of the ACM on Programming Languages10.1145/33605563:OOPSLA(1-22)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360556
Huang MFu HChatterjee KGoharshady A(2019)Modular verification for almost-sure termination of probabilistic programsProceedings of the ACM on Programming Languages10.1145/33605553:OOPSLA(1-29)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360555
Zuriel YFriedman MSheffi GCohen NPetrank E(2019)Efficient lock-free durable setsProceedings of the ACM on Programming Languages10.1145/33605543:OOPSLA(1-26)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360554
Henriksen IBilardi GPingali K(2019)Derivative grammars: a symbolic approach to parsing with derivativesProceedings of the ACM on Programming Languages10.1145/33605533:OOPSLA(1-28)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360553
Show More Cited By

View Options

Get Access

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 Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents