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
  is_linked : nat->nat->bool
  E = ... : Type
  mark = ... : prog|sort