The FLINT Project

Research

People

Publications

Software

Support

Links

Internal

A General Framework for Certifying Garbage Collectors and Their Mutators

Last modified: Thu Jun 14 07:34:28 2007 GMT.

Authors

Andrew McCreight
Zhong Shao
Chunxiao Lin
Long Li

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.

Published

  • In Proc. ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation (PLDI'07), San Diego, CA, pages 468-479, June 2007. © ACM.
  • Technical Supplement (6 pages)
  • Coq implementation [320k]

  • Copyright © 1996-2017 The FLINT Group <flint at cs dot yale dot edu>
    Yale University Department of Computer Science
    Validate this page
    colophon