Kestrel Institute

file

Visible to the public Synthesis of Concurrent Garbage Collectors

Abstract:

Garbage collection is an attractive target for exploring the issues in synthesizing concurrent algorithms. The basic algorithms are tricky to get correct, and become even trickier when implemented on modern multi-core architectures. We are using Kestrel's Specware system to synthesize garbage collectors, starting from a formal specification of collection requirements. Novel features include a mixed algebraic/coalgebraic style of specification, and coalgebraically-oriented transformations that generate correct-by-construction refinements.

file

Visible to the public High Assurance Java Virtual Machine