Chris Hawblitzel
Erez Petrank
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.
- 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. Google Scholar
Digital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Sam Borman. Sensible sanitation -- understanding the IBM Java garbage collector, part 1: Object allocation. IBM developer Works, August 2002.Google Scholar
- 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. Google ScholarDigital Library
- C. J. Cheney. A non-recursive list compacting algorithm. Communications of the ACM, 13(11):677--8, November 1970. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google ScholarDigital Library
- Damien Doligez and Georges Gonthier. Portable, unobtrusive garbage collection for multiprocessor systems. In POPL, Portland, OR, January 1994. ACM Press. Google ScholarDigital Library
- Tamar Domani, Elliot Kolodner, and Erez Petrank. A generational on-the-fly garbage collector for Java. In PLDI, Vancouver, June 2000. Google ScholarDigital Library
- Healfdene Goguen, Richard Brooksby, and Rod Burstall. An abstract formulation of memory management, December 1998. draft.Google Scholar
- 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. Google ScholarDigital Library
- Klaus Havelund and N. Shankar. A mechanized refinement proof for a garbage collector. Technical report, Aalborg University, 1997. Submitted to Formal Aspects of Computing.Google Scholar
- 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. Google ScholarDigital Library
- Haim Kermany and Erez Petrank. The Compressor: Concurrent, incremental and parallel compaction. In PLDI, pages 354--363, Ottawa, June 2006. ACM Press. Google ScholarDigital Library
- Yossi Levanoni and Erez Petrank. An on-the-fly reference counting garbage collector for Java. In PLDI, 28(1), January 2006. Google ScholarDigital Library
- John McCarthy. Recursive functions of symbolic expressions and their computation by machine. Communications of the ACM, 3:184--195, 1960. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Marvin L. Minsky. A Lisp garbage collector algorithm using serial secondary storage. Technical Report Memo 58 (rev.), Project MAC, MIT, Cambridge, MA, December 1963. Google ScholarDigital Library
- Stefan Monnier, Bratin Saha, and Zhong Shao. Principled scavenging. In PLDI, Snowbird, Utah, June 2001. Google ScholarDigital Library
- Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. In POPL, pages 85--97, January 1998. Google ScholarDigital Library
- George Necula. Proof-Carrying Code. In POPL, pages 106--119. ACM Press, 1997. Google ScholarDigital Library
- Filip Pizlo, Erez Petrank, and Bjarne Steensgaard. A study of concurrent real-time garbage collectors. In PLDI, pages 33--44, Tucson, AZ, June 2008. Google ScholarDigital Library
- David M. Russinoff. A mechanically verified incremental garbage collector. Formal Aspects of Computing, 6:359--390, 1994.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- Daniel C. Wang and Andrew W. Appel. Type-preserving garbage collectors. In POPL, January 2001. Google ScholarDigital Library
Index Terms
- Automated verification of practical garbage collectors
Recommendations
Automated verification of practical garbage collectors
POPL '09Garbage 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 general framework for certifying garbage collectors and their mutators
PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and ImplementationGarbage-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 ...
A general framework for certifying garbage collectors and their mutators
Proceedings of the 2007 PLDI conferenceGarbage-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