Formal Derivation of Concurrent Garbage Collectors
Distributed, Parallel, and Cluster Computing
2010-06-23 v1 Logic in Computer Science
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.
Cite
@article{arxiv.1006.4342,
title = {Formal Derivation of Concurrent Garbage Collectors},
author = {Dusko Pavlovic and Peter Pepper and Douglas R. Smith},
journal= {arXiv preprint arXiv:1006.4342},
year = {2010}
}
Comments
38 pages, 21 figures. The short version of this paper appeared in the Proceedings of MPC 2010