Partial Verification of a Simple Mark and Sweep Garbage Collector

This directory contains a shape analysis to meet the challenge of verifying partial correctness of a mark and sweep garbage collector. The challenge was raised during the 2001 University of Washington and Microsoft Research Summer Institute .

Modeling the problem

We assume that the heap concists of objects with left and right reference fields, as shown below. 

class Node {
  Node left;
  Node right;
  ...
}
We also assume that a root reference variable provides a single access point to the heap.

List of examples and their descriptions

(see additional comments below)
Example Example description Properties checked Command line
mark The mark phase of the garbage collector
  1. Absence of null dereferences
  2. All objects reachable from root are marked
  3. All objects not reachable from root are not marked
tvla mark store
sweep The sweep phase of the garbage collector
  1. Absence of null dereferences
  2. All marked objects are not collected
  3. All objects not marked are collected
tvla sweep storeAfterMark
markAndSweep Mark phase followed by a sweep phase
  1. Absence of null dereferences
  2. All objects reachable from root are not collected
  3. All objects not reachable from root are collected
tvla markAndSweep store

Comments on the way method bodies are modelled by first-order transition systems

The original C functions were pre-processed in the following ways in order to simplify the analysis:
  1. Statements that assign to fields are preceded by statements that assign the value NULL to the fields.
    For example, x->n = y; is replaced with x->n = NULL; x->n = y;
  2. Statements that copy a value from one field to another are simplified by using temporary variables.
    For example, x->n = y->n; is replaced with the sequence of assignments
    t = y->n; x->n = NULL; x->n = t; t = NULL;
Program conditions are modelled by two actions---one for the true branch and one for the false branch.