Verifying the safety of a practical concurrent garbage collector

Abstract

We describe our experience in the mechanical verification of the safety invariants of an asynchronous garbage-collection algorithm [1], using the TLP system [2]. We only give a cursory overview of the algorithm and its formalisation. Our main focus is on the lessons learned from carrying a sizeable (22,000+ lines) formal proof through an off-the-shelf prover. In particular, we found the TLP style of structured proofs to be particularly effective for organising, writing, and managing proof scripts.