Designing a garbage collector with real-time properties is particularly difficult task, involving the construction of an incremental run-time algorithm as well as methods for a priori reasoning about schedulability in two dimensions (time and memory usage). Fundamental to the success of any such undertaking must of course be the formalism in which the actual garbage-collection algorithm is defined and understood.
In this talk I will 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 process is weakly bisimilar to a non-collecting process with infinite storage space. In addition, the formalized collector is shown to be both terminating and useful, in the sense that it actually recovers the unreachable parts of any given heap in a finite number of steps.
Johan Nordlander is universitetslektor in Computer Science at Luleå University of Technology in Sweden. Previously he was a postdoc in PacSoft at the Oregon Graduate Institute of Science and Technology, a PhD student at the Department of Computing Science, Chalmers University of Technology, Göteborg, Sweden, and a software consultant at Data Ductus AB, Skellefteå, Sweden.
Prof Nordlander's research interests lie in the field of programming language design, especially in the intersection of the functional, object-oriented and concurrent paradigms. He is one of the main designers of Timber, a language deeply rooted in all three paradigms, and based on the notion of reactive objects. He is also responsible for an older language in a similar vein called O'Haskell.
Mark Jones