What Is a Garbage Collector? An Exercise in Compositional Refinement

Specifications define the expected behavior of software components and systems. They are critical to software correctness yet writing good specifications can be quite challenging. We examine the case of the specification for a concurrent garbage collector that operates in conjunction with a cooperative mutator. We argue that many previous attempts to specify the behavior of such a garbage collector are flawed. The typical problem is that correctness is specified in terms of assertions that hold at specific program points leaving a step of interpretation to be convinced that the intended behavior has been properly formalized. We introduce a notion of compositional refinement that serves as an acceptable specification for properties of components like a garbage collector that are refined in the context of an assumed environment like a mutator.