KnowledgeBase » SEMINAR » ID = 439

Verifying Garbage Collection Algorithms using the PVS Theorem Prover

by Paul B. Jackson
1996-1997

Abstract

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 Gonthier[Gonth].

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.