Tel-Aviv University - Computer Science Colloquium

Sunday, March 12, 2006, 11:15-12:15

Room 309
Schreiber Building


Eran Yahav

IBM Research


Systematic Derivation of Concurrent Garbage Collectors



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 garbage

collected 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

new algorithms can be synthesized from the abstract algorithm by

a series of our transformations. We relate the algorithms formally

using a new definition of precision, and informally with respect to

overhead and concurrency.

This provides many insights about the nature of concurrent

collection, allows the direct synthesis of new and useful algorithms,

reduces the burden of proof to a single simple algorithm, and lays

the groundwork for the automated synthesis of correct concurrent



This is joint work with Martin Vechev and David F. Bacon