TODO list

Assumptions

Initially, we are "commenting out" the while-loop inside of the collect() function of the garbage collector. It is natural to do that, because the last atomic block (addOrigins();mark();) is enough to achieve the safety condition of the garbage collector (i.e. that no reachable from the roots node is left unmarked).

In terms of atomicity we initially assume that the whole collect function:

collect() {
atomic
   marked ← {root1, . . . , rootR}
   pending ← ∪(x∈marked fields(x))
   log ← ε
   mark()
   sweep()
}

The current plan is to gradually relax the atomicity scope and then prove the correctness of the algorithm with in the presence of the currently omitted while loop.

TO DO:

1. State the invariant for the while loop in the mark() function.
2. Write down the mark function in Coq.
3. Prove collect.

collect() {
atomic
   marked ← {root1, . . . , rootR}
   pending ← ∪(x∈marked fields(x))
   log ← ε

atomic
   addOrigins()
   mark()
   sweep()
]

4. Prove the new collect.