A refinement proof for a garbage collector

Abstract

We describe how the PVS theorem prover has been used to verify a safety property of a widely studied garbage collection algorithm. The safety property asserts that “nothing but garbage is ever collected”. The garbage collection algorithm and its composition with the user program can be regarded as a concurrent system with two processes working on a shared memory. Such concurrent systems can be encoded in PVS as state transition systems using a model similar to TLA [16]. The safety criterion is formulated as a refinement and proved using refinement mappings. Russinoff [19] originally verified the algorithm in the Boyer-Moore prover, but his proof was not based on refinement. Furthermore, the safety property formulation required a glass box view of the algorithm. Using refinement, however, the safety criterion makes sense independent of the garbage collection algorithm. As a by-product, we encode a version of the theory of refinement mappings in PVS. The paper reflects substantial work that was done over two decades ago, but which is still relevant.