Abstract:

Concurrent garbage collectors are notoriously hard to design,
implement, and verify. We present a framework for the automatic
exploration of a space of concurrent mark-and-sweep collectors. In
our framework, the designer specifies a set of “building blocks”
from which algorithms can be constructed. These blocks reflect the
designer’s insights about the coordination between the collector and
the mutator. Given a set of building blocks, our framework
automatically explores a space of algorithms, using model checking
with abstraction to verify algorithms in the space. We capture the
intuition behind some common mark-and-sweep algorithms using a set
of building blocks.We utilize our framework to automatically explore
a space of more than 1,600,000 algorithms built from these blocks,
and derive 6 (correct) algorithms with various space, synchronization,
and precision tradeoffs.

In our previous work (PLDI'06), we presented a framework for
unifying and relating concurrent collectors. In this work, we
automatically synthesize provably correct concurrent collectors.
This work will appear in PLDI'07.

Joint work with Martin Vechev (Cambridge University), David Bacon
(IBM Research), and Noam Rinetzky (Tel Aviv University).