More Web Proxy on the site http://driver.im/

research-article

Automated verification of practical garbage collectors

Authors:

Chris Hawblitzel,

Erez PetrankAuthors Info & Claims

ACM SIGPLAN Notices, Volume 44, Issue 1

Pages 441 - 453

https://doi.org/10.1145/1594834.1480935

Published: 21 January 2009 Publication History

Abstract

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 proofs were hand-written or the collectors were too simplistic to use on practical applications. In this work, we present two mechanically verified garbage collectors, both practical enough to use for real-world C# benchmarks. The collectors and their associated allocators consist of x86 assembly language instructions and macro instructions, annotated with preconditions, postconditions, invariants, and assertions. We used the Boogie verification generator and the Z3 automated theorem prover to verify this assembly language code mechanically. We provide measurements comparing the performance of the verified collector with that of the standard Bartok collectors on off-the-shelf C# benchmarks, demonstrating their competitiveness.

References

[1]

Hezi Azatchi, Yossi Levanoni, Harel Paz, and Erez Petrank. An onthe-fly mark and sweep garbage collector based on sliding view. In OOPSLA'03 ACM Conference on Object-Oriented Systems, Languages and Applications, ACM SIGPLAN Notices, Anaheim, CA, November 2003. ACM Press.

Digital Library

[2]

Katherine Barabash, Ori Ben-Yitzhak, Irit Goft, Elliot K. Kolodner, Victor Leikehman, Yoav Ossia, Avi Owshanko, and Erez Petrank. A parallel, incremental, mostly concurrent garbage collector for servers. ACM Transactions on Programming Languages and Systems, 27(6):1097--1146, November 2005.

Digital Library

[3]

Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In Formal Methods for Components and Objects: 4th International Symposium, FMCO 2005.

Digital Library

[4]

Lars Birkedal, Noah Torpe-Smith, and John C. Reynolds. Local reasoning about a copying garbage collector. In POPL, pages 220--231, Venice, January 2004. ACM Press.

Digital Library

[5]

Sam Borman. Sensible sanitation -- understanding the IBM Java garbage collector, part 1: Object allocation. IBM developer Works, August 2002.

[6]

Juan Chen, Chris Hawblitzel, Frances Perry, Mike Emmi, Jeremy Condit, Derrick Coetzee, and Polyvios Pratikakis. Type-preserving compilation for large-scale optimizing object-oriented compilers. In PLDI, pages 183--192, Tucson, AZ, June 2008.

Digital Library

[7]

C. J. Cheney. A non-recursive list compacting algorithm. Communications of the ACM, 13(11):677--8, November 1970.

Digital Library

[8]

Leonardo de Moura and Nikolaj Bjorner. Z3: An Efficient SMT Solver. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008.

Digital Library

[9]

Edsgar W. Dijkstra, Leslie Lamport, A. J. Martin, C. S. Scholten, and E. F. M. Steffens. On-the-fly garbage collection: An exercise in cooperation. In Lecture Notes in Computer Science, No. 46. Springer-Verlag, New York, 1976.

Digital Library

[10]

Damien Doligez and Georges Gonthier. Portable, unobtrusive garbage collection for multiprocessor systems. In POPL, Portland, OR, January 1994. ACM Press.

Digital Library

[11]

Tamar Domani, Elliot Kolodner, and Erez Petrank. A generational on-the-fly garbage collector for Java. In PLDI, Vancouver, June 2000.

Digital Library

[12]

Healfdene Goguen, Richard Brooksby, and Rod Burstall. An abstract formulation of memory management, December 1998. draft.

[13]

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

Digital Library

[14]

Klaus Havelund and N. Shankar. A mechanized refinement proof for a garbage collector. Technical report, Aalborg University, 1997. Submitted to Formal Aspects of Computing.

[15]

Paul B. Jackson. Verifying a garbage collection algorithm. In Proceedings of 11th International Conference on Theorem Proving in Higher Order Logics TPHOLs'98, volume 1479 of Lecture Notes in Computer Science, pages 225---244, Canberra, September 1998. Springer-Verlag.

Digital Library

[16]

Haim Kermany and Erez Petrank. The Compressor: Concurrent, incremental and parallel compaction. In PLDI, pages 354--363, Ottawa, June 2006. ACM Press.

Digital Library

[17]

Yossi Levanoni and Erez Petrank. An on-the-fly reference counting garbage collector for Java. In PLDI, 28(1), January 2006.

Digital Library

[18]

John McCarthy. Recursive functions of symbolic expressions and their computation by machine. Communications of the ACM, 3:184--195, 1960.

Digital Library

[19]

Andrew McCreight, Zhong Shao, Chunxiao Lin, and Long Li. A general framework for certifying garbage collectors and their mutators. In PLDI, San Diego, CA, June 2007.

Digital Library

[20]

Marvin L. Minsky. A Lisp garbage collector algorithm using serial secondary storage. Technical Report Memo 58 (rev.), Project MAC, MIT, Cambridge, MA, December 1963.

Digital Library

[21]

Stefan Monnier, Bratin Saha, and Zhong Shao. Principled scavenging. In PLDI, Snowbird, Utah, June 2001.

Digital Library

[22]

Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. In POPL, pages 85--97, January 1998.

Digital Library

[23]

George Necula. Proof-Carrying Code. In POPL, pages 106--119. ACM Press, 1997.

Digital Library

[24]

Filip Pizlo, Erez Petrank, and Bjarne Steensgaard. A study of concurrent real-time garbage collectors. In PLDI, pages 33--44, Tucson, AZ, June 2008.

Digital Library

[25]

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

[26]

Martin Vechev, Eran Yahav, David Bacon, and Noam Rinetzky. CGCExplorer: A semi-automated search procedure for provably correct concurrent collectors. In PLDI, San Diego, CA, June 2007.

Digital Library

[27]

Daniel C. Wang and Andrew W. Appel. Type-preserving garbage collectors. In POPL, January 2001.

Digital Library

Cited By

Österlund ELöwe W(2018)Self-adaptive concurrent componentsAutomated Software Engineering10.1007/s10515-017-0219-025:1(47-99)Online publication date: 1-Mar-2018
https://dl.acm.org/doi/10.1007/s10515-017-0219-0
Fang BSighireanu M(2017)A refinement hierarchy for free list memory allocatorsACM SIGPLAN Notices10.1145/3156685.309227552:9(104-114)Online publication date: 18-Jun-2017
https://dl.acm.org/doi/10.1145/3156685.3092275
Ugawa TAbe TMaeda T(2017)Model checking copy phases of concurrent copying garbage collection with various memory modelsProceedings of the ACM on Programming Languages10.1145/31338771:OOPSLA(1-26)Online publication date: 12-Oct-2017
https://dl.acm.org/doi/10.1145/3133877
Show More Cited By

Index Terms

Automated verification of practical garbage collectors
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Correctness
2. Theory of computation
  1. Logic
    1. Proof theory

Recommendations

A general framework for certifying garbage collectors and their mutators
PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation

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 ...
A study of concurrent real-time garbage collectors
PLDI '08

Concurrent garbage collection is highly attractive for real-time systems, because offloading the collection effort from the executing threads allows faster response, allowing for extremely short deadlines at the microseconds level. Concurrent collectors ...
Automated verification of practical garbage collectors
POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

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

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 44, Issue 1

POPL '09

January 2009

453 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1594834

Issue’s Table of Contents

POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2009
464 pages
ISBN:9781605583792
DOI:10.1145/1480881
General Chair:
Zhong Shao
Yale University, USA
,
Program Chair:
Benjamin C. Pierce
University of Pennsylvania, USA

Copyright © 2009 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: 21 January 2009

Published in SIGPLAN Volume 44, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

58
Total Citations
View Citations
552
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)3

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Österlund ELöwe W(2018)Self-adaptive concurrent componentsAutomated Software Engineering10.1007/s10515-017-0219-025:1(47-99)Online publication date: 1-Mar-2018
https://dl.acm.org/doi/10.1007/s10515-017-0219-0
Fang BSighireanu M(2017)A refinement hierarchy for free list memory allocatorsACM SIGPLAN Notices10.1145/3156685.309227552:9(104-114)Online publication date: 18-Jun-2017
https://dl.acm.org/doi/10.1145/3156685.3092275
Ugawa TAbe TMaeda T(2017)Model checking copy phases of concurrent copying garbage collection with various memory modelsProceedings of the ACM on Programming Languages10.1145/31338771:OOPSLA(1-26)Online publication date: 12-Oct-2017
https://dl.acm.org/doi/10.1145/3133877
Fang BSighireanu MKirsch CTitzer B(2017)A refinement hierarchy for free list memory allocatorsProceedings of the 2017 ACM SIGPLAN International Symposium on Memory Management10.1145/3092255.3092275(104-114)Online publication date: 18-Jun-2017
https://dl.acm.org/doi/10.1145/3092255.3092275
Zakowski YCachera DDemange DPetri GPichardie DJagannathan SVitek J(2017)Verifying a Concurrent Garbage Collector Using a Rely-Guarantee MethodologyInteractive Theorem Proving10.1007/978-3-319-66107-0_31(496-513)Online publication date: 2017
https://doi.org/10.1007/978-3-319-66107-0_31
Sandberg Ericsson AMyreen MÅman Pohjola J(2017)A Verified Generational Garbage Collector for CakeMLInteractive Theorem Proving10.1007/978-3-319-66107-0_28(444-461)Online publication date: 2017
https://doi.org/10.1007/978-3-319-66107-0_28
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
Jensen JBenton NKennedy A(2013)High-level separation logic for low-level codeACM SIGPLAN Notices10.1145/2480359.242910548:1(301-314)Online publication date: 23-Jan-2013
https://dl.acm.org/doi/10.1145/2480359.2429105
Show More Cited By

View Options

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 Issue’s Table of Contents