Verifying a Concurrent Garbage Collector
using a Rely-Guarantee Methodology
Abstract
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.
Papers
- In Interactive Theorem Proving (ITP'17), LNCS 10499, Springer 2017.
[preprint,slides]
- Extended version submitted to the special issue of ITP 2017 to be edited in the Journal of Automated Reasoning (JAR'18).
[preprint]
- Yannick Zakowski's Ph.D. dissertation, 2017.
[manuscript]
Coq Development
The accompanying Coq development is available here. It requires Coq 8.4pl6 (January 2016) in order to be compiled.