Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example

Decomposing the design (or documentation) of large systems is a practical necessity but finding compositional development methods for concurrent software is technically challenging. This paper includes the development of a difficult example in order to draw out lessons about such methods. The concurrent garbage collector development is interesting in several ways; in particular, the final step of its development appears to be just beyond what can be expressed by rely/guarantee relations. This prompts an exploration of the limitations of this well-known method. Although the rely/guarantee approach is used, most of the lessons are more general.