Automated verification of practical garbage collectors

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 , Erez Petrank, An on-the-fly mark and sweep garbage collector based on sliding views, Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, October 26-30, 2003, Anaheim, California, USA
• 2: Katherine Barabash , Ori Ben-Yitzhak , Irit Goft , Elliot K. Kolodner , Victor Leikehman , Yoav Ossia , Avi Owshanko , Erez Petrank, A parallel, incremental, mostly concurrent garbage collector for servers, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.6, p.1097-1146, November 2005 [doi>10.1145/1108970.1108972]
• 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.
• 4: Lars Birkedal , Noah Torp-Smith , John C. Reynolds, Local reasoning about a copying garbage collector, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.220-231, January 14-16, 2004, Venice, Italy
• 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 , Polyvios Pratikaki, Type-preserving compilation for large-scale optimizing object-oriented compilers, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA
• 7: C. J. Cheney, A nonrecursive list compacting algorithm, Communications of the ACM, v.13 n.11, p.677-678, Nov 1970 [doi>10.1145/362790.362798]
• 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.
• 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.
• 10: Damien Doligez , Georges Gonthier, Portable, unobtrusive garbage collection for multiprocessor systems, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.70-83, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.174673]
• 11: Tamar Domani , Elliot K. Kolodner , Erez Petrank, A generational on-the-fly garbage collector for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.274-284, June 18-21, 2000, Vancouver, British Columbia, Canada
• 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, Proceedings of the 8th International Conference on Computer Aided Verification, p.462-465, August 03, 1996
• 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, Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, p.225-244, September 27-October 01, 1998
• 16: Haim Kermany , Erez Petrank, The Compressor: concurrent, incremental, and parallel compaction, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 17: Yossi Levanoni , Erez Petrank, An on-the-fly reference-counting garbage collector for java, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.1, p.1-69, January 2006 [doi>10.1145/1111596.1111597]
• 18: John McCarthy, Recursive functions of symbolic expressions and their computation by machine, Part I, Communications of the ACM, v.3 n.4, p.184-195, April 1960 [doi>10.1145/367177.367199]
• 19: Andrew McCreight , Zhong Shao , Chunxiao Lin , Long Li, A general framework for certifying garbage collectors and their mutators, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 20: Marvin Minsky, A LISP Garbage Collector Algorithm Using Serial Secondary Storage, Massachusetts Institute of Technology, Cambridge, MA, 1963
• 21: Stefan Monnier , Bratin Saha , Zhong Shao, Principled scavenging, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.81-91, June 2001, Snowbird, Utah, United States
• 22: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.85-97, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268954]
• 23: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 24: Filip Pizlo , Erez Petrank , Bjarne Steensgaard, A study of concurrent real-time garbage collectors, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA
• 25: David M. Russinoff. A mechanically verified incremental garbage collector. Formal Aspects of Computing, 6:359--390, 1994.
• 26: Martin T. Vechev , Eran Yahav , David F. Bacon , Noam Rinetzky, CGCExplorer: a semi-automated search procedure for provably correct concurrent collectors, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 27: Daniel C. Wang , Andrew W. Appel, Type-preserving garbage collectors, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.166-178, January 2001, London, United Kingdom

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

General Terms:
Verification

Keywords:
garbage collection, verification