Synthesis of Concurrent Garbage Collectors

Presented as part of the 2012 HCSS conference.

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. Dijkstra’s on-the-fly concurrent garbage collector algorithm falls out from a straightforward application of fixpoint-iteration algorithm design and a finite differencing transformation. Other transformations include refinement of high-level types to more complicated, but efficient low-level types, globalization to transform from functional to shared-memory programs, and so on. Most of the transformations work by performing equational calculations using theorems from the application domain, and current efforts are augmenting the transformations to generate checkable proofs at the same time as they refine the source specification – in effect to generate proof-carrying code.

Biography:

Dr. Douglas R. Smith is a Principal Scientist at Kestrel Institute and serves as President of Kestrel Technology LLC (both in Palo Alto). He is a Fellow of the American Association of Artificial Intelligence (AAAI) and an ASE Fellow (Automated Software Engineering). During 1986-2000, he periodically taught an advanced graduate course on knowledge-based software development at Stanford University. Dr. Smith served as Chairman of IFIP Working Group 2.1 on Algorithmic Languages and Calculi during 1994-2000. Dr. Smith’s research interests have centered around formal specifications, automated inference, and program synthesis. He has led the development of a series of software synthesis systems, including KIDS (Kestrel Interactive Development Systems), Specware, Designware, and Planware. Applications have included a variety of complex high-performance schedulers for the US Air Force. Dr. Smith has over 30 years of experience in the field of automated program synthesis and has published over 100 papers. He has one patent. He received the Ph.D. in Computer Science from Duke University in 1979.