Verifying a Concurrent Garbage Collector
using a Rely-Guarantee Methodology

Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri,
David Pichardie, Suresh Jagannathan, Jan Vitek


Concurrent garbage collection algorithms are an emblematic challenge in the area of concurrent program verification. In this paper, we address this problem by proposing a mechanized proof methodology based on the popular Rely-Guarantee (RG) proof technique. We design a specific compiler intermediate representation (IR) with strong type guarantees, dedicated support for abstract concurrent data structures, and high-level iterators on runtime internals. In addition, we define an RG program logic supporting an incremental proof methodology where annotations and invariants can be progressively enriched.
We formalize the IR, the proof system, and prove the soundness of the methodology in the Coq proof assistant. Equipped with this IR, we prove a fully concurrent garbage collector where mutators never have to wait for the collector.


Coq Development

The accompanying Coq development is available here. It requires Coq 8.4pl6 (January 2016) in order to be compiled.