A correct and useful incremental copying garbage collector
2007 (English)In: Proceedings of the the 2007 International Symposium on Memory Management: Québec, Canada, October 21 - 22, 2007, New York: ACM Digital Library, 2007, 129-140 p.Conference paper (Refereed)
Designing 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.
Place, publisher, year, edition, pages
New York: ACM Digital Library, 2007. 129-140 p.
Research subject Dependable Communication and Computation Systems; Embedded System
IdentifiersURN: urn:nbn:se:ltu:diva-39218DOI: 10.1145/1296907.1296924Local ID: dddc6810-546d-11dc-8e15-000ea68e967bISBN: 978-1-59593-893-0OAI: oai:DiVA.org:ltu-39218DiVA: diva2:1012727
International Symposium on Memory Management : 21/10/2007 - 22/10/2007
Godkänd; 2007; 20070827 (keero)2016-10-032016-10-03Bibliographically approved