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
Technical Supplement (6 pages)
Coq implementation [320k]