A Correct and Useful Incremental Copying Garbage Collector
Martin Kero, Johan Nordlander and Per Lindgren
The 2007 International
Symposium on Memory Management (ISMM 2007) Montreal, Canada, 21-22
October, 2007
Abstract
As safety-critical systems become more complex, higher-level
programming language features such as automatic memory management become
desirable. Designing a a garbage collector with real-time properties is a
particularly difficult task, involving the construction of both an incremental
run-time algorithm as well as methods enabling a priori reasoning about
schedulability in two dimensions (time and memory usage in conjunction). In
order to comply with such ambitious goals with any amount of formal rigor, a
comprehensive understanding of the actual algorithm used is of course a
fundamental requirement. In this paper we present a formal model of an
incremental copying garbage collector, where each atomic increment is modeled as
a transition between states of a heap process. Soundness of the algorithm is
shown by proving that the garbage collecting heap process is weakly bisimilar to
a non-collecting heap with infinite storage space. In addition, we show that our
collector is both terminating and useful, in the sense that it actually recovers
the unreachable parts of any given heap in a finite number of steps.