Formal Derivation of Concurrent Garbage Collectors

TL;DR

This paper presents a formal derivation method for concurrent garbage collectors, using refinement from specifications and extending lattice-theoretic fixpoint theorems to handle concurrent mutation and collection dynamics.

Contribution

It introduces a formal derivation approach for concurrent garbage collectors based on domain-independent theories and extends classical fixpoint theorems for concurrency.

Findings

Derived a family of concurrent garbage collectors from formal specifications

Extended lattice-theoretic fixpoint theorems to model concurrency dynamics

Demonstrated correctness through formal refinement processes

Abstract

Concurrent garbage collectors are notoriously difficult to implement correctly. Previous approaches to the issue of producing correct collectors have mainly been based on posit-and-prove verification or on the application of domain-specific templates and transformations. We show how to derive the upper reaches of a family of concurrent garbage collectors by refinement from a formal specification, emphasizing the application of domain-independent design theories and transformations. A key contribution is an extension to the classical lattice-theoretic fixpoint theorems to account for the dynamics of concurrent mutation and collection.