ISMM 2007 START Conference Manager    

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


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.

START Conference Manager (V2.54.5)