Sunday, March 12, 2006, 11:15-12:15
Room 309
--------------------------------------------------------------------------------
Eran Yahav
IBM Research
Title:
Systematic Derivation of Concurrent Garbage Collectors
Abstract:
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
collectors.
This is joint work with Martin Vechev and David F. Bacon