WG211/M14Pepper

Title: Derivation of program families and its application to concurrent garbage collectors.

Abstract: A powerful methodology for developing whole families of programs consists in providing an abstract collection of specifications together with abstract implementations, all organized in a refinement hierarchy. Then concrete problem specifications can be seen as instances of the abstract specifications, which leads to the (semi)automatic derivation of concrete solutions. (Formally this can be seen as a pushout construction in categories.) This work is done jointly with Doug Smith from Kestrel Institute, Palo Alto, where the derivations are carried out within the framework of Kestrel's program derivation system, based on a combination of algebraic and co-algebraic techniques. These semi-automatic derivations actually lead from high-level abstract specifications all the way down to concrete C implementations.

We apply these concepts to the problem class of concurrent garbage collectors and demonstrate that indeed all kinds of garbage collectors can be formally and systematically derived from a few and simple requirements and design ideas.