Verifying Garbage Collection Algorithms using the PVS Theorem Prover
by Paul B. Jackson
This talk covers ongoing work that is part of a collaboration between myself, Healf Goguen, and Rod Burstall at Edinburgh LFCS, and members of the memory management (MM) group at the Harlequin software house.
The aim of the collaboration is to explore ways in which formal
methods can help the MM group. Our primary interest at LFCS is in
checking correctness of algorithms that the MM group uses, but we are
also interested in how the process of setting up models and proving
formal properties can have impact on the MM group's design procedures.
To date, we have agreed on a set of abstract designs for basic,
incremental, and generational garbage collection algorithms, and are
now exploring ways of verifying them.
Our predominant approach has been to use the PVS theorem proving
system to model the algorithms using state transition systems, and prove
safety and liveness properties about traces of states of these
systems. Similar approaches have been used in the past for the
mechanical verification of a Ben-Ari garbage collection algorithm by
Russinoff[Russ], and of a concurrent algorithm for CAML-light by
We are currently also looking at the appropriateness of labelled
transition system models, and carrying out the verification by showing
a model of garbage collected heap memory to be weakly bisimular to a
model of an ideal infinite heap without collection.
[Russ] David Russinoff. "A Mechanically Verified Incremental Garbage Collector". Formal Aspects of Computing (1994) 6:359-390.
[Gonth] Georges Gonthier. "Verifying the Safety of a Practical Concurrent Garbage Collector". Procs of CAV '96. LNCS 1102, Springer Verlag.