Sciweavers

PLDI
2006
ACM

Correctness-preserving derivation of concurrent garbage collection algorithms

14 years 4 months ago
Correctness-preserving derivation of concurrent garbage collection algorithms
Constructing correct concurrent garbage collection algorithms is notoriously hard. Numerous such algorithms have been proposed, implemented, and deployed – and yet the relationship among them in terms of speed and precision is poorly understood, and the validation of one algorithm does not carry over to others. As programs with low latency requirements written in garbagecollected languages become part of society’s mission-critical infrastructure, it is imperative that we raise the level of confidence in the correctness of the underlying system, and that we understand the trade-offs inherent in our algorithmic choice. In this paper we present correctness-preserving transformations that can be applied to an initial abstract concurrent garbage collection algorithm which is simpler, more precise, and easier to prove correct than algorithms used in practice — but also more expensive and with less concurrency. We then show how both pre-existing and rithms can be synthesized from the ...
Martin T. Vechev, Eran Yahav, David F. Bacon
Added 14 Jun 2010
Updated 14 Jun 2010
Type Conference
Year 2006
Where PLDI
Authors Martin T. Vechev, Eran Yahav, David F. Bacon
Comments (0)