Next: The correctness proof Up: Example Previous: Example

### The marker phase of a garbage collection algorithm

The work documented in this section has been contributed by Rod Burstall and Adriana Compagnoni. The starting point in the development of the present example was the garbage collection algorithm presented in [Ben-Ari, 1984]. The garbage collector consists of two phases. In the first phase, the collector marks all nodes accessible from the root, and in the second phase, all unmarked nodes are appended to a list of free nodes. In Ben-Ari's algorithm the memory is scanned to count the number of marked nodes to detect whether all accesible nodes have been marked. In our algorithm we use a flag changed which is set to be true whenever a node is marked. Another difference is that instead of having in each memory cell an array with the nodes immediately accesible from it, we have a function `is_linked` which given two cell indexes i and j gives true if and only if there is a link from i to j. We follow the convention that marked nodes are black and unmarked nodes are white. We assume that in an initial state all nodes are white. The algorithm mark then consists in

1. blackening the root,
2. propagating the colouring,
3. collecting white nodes.

The collecting phase will also set all nodes white.

We represent the memory as an array a of colours (black and white) of size n with indexes from 0 to n-1,

``` ** Module mark Imports lib_ipl
changed = ... : location
i = ... : location
j = ... : location
a = ... : location
sort = ... : location->Type
black = ... : bool
white = ... : bool
isBlack = ... : bool->bool
isWhite = ... : bool->bool
n : nat