On-the-fly garbage collectors provide an interesting class of concurrent algorithms for study, as they are quintessentially concurrent, rather than sequential algorithms which manage to work despite the concurrency. Dijstra et al. [1] present an algorithm with an extremely complex and difficult proof. Other proofs of the same algorithm have been produced, but all are hard to grasp.

In this paper, a new algorithm is presented. It is slightly simpler than [1], involving the use of only two “colors” for marking the data structure (rather than three), but its real objective and strength is its amenability to a very straightforward proof. This is presented for a program fragment in ADA, in the form of invariants which involve the program coutner explicitly. The algorithm is shown to be robust in the face of the apparently trivial programming changes which have invalidated other proofs; it also appears to be compatible with the hardware used to implement the mutator part of [1] on the Intel iAPX-432 machine.

The straightforward nature of the algorithm makes it possible to develop provable variants with little effort. A more efficient version and an incremental garbage collector are shown. This is an extremely lucid and approachable paper in an area not often found rewarding by nonspecialists. It is strongly recommended.