Lock-free Parallel Garbage Collection by Mark&Sweep

This is joint work with Gao Hui (Groningen University) and Jan Friso Groote (Eindhoven University of Technology). It concerns our papers:

• H. Gao, J. F. Groote, W. H. Hesselink: Lock-free parallel and concurrent garbage collection by mark&sweep. Science of Computer Programming 64 (2007) 341-374.
• Gao H., Groote J.F., Hesselink W.H.: Lock-free parallel garbage collection. In Pan, Y.; Chen, D.; Guo, M.; Cao, J.; Dongarra, J. (Eds.) : Proceedings of Third International Symposium on Parallel and Distributed Processing and Applications (ISPA'05), Nanjing, China, LNCS 3758, pp. 263-274, 2005.

This paper presents a lock-free parallel algorithm for mark&sweep garbage collection (GC) in a realistic model using synchronization primitives compare-and-swap (CAS) and load-linked/store-conditional (LL/SC) offered by machine architectures. Mutators and collectors can simultaneously operate on the data structure. In particular no strict alternation between usage and cleaning up is necessary contrary to what is common in most other GC algorithms.

We first design and prove an algorithm with a coarse grain of atomicity and subsequently apply the reduction theorem to implement the higher-level atomic steps by means of the low-level primitives CAS or LL/SC. Even so, the structure of our algorithm and its correctness properties, as well as the complexity of reasoning about them, makes neither automatic nor manual verification feasible. We have therefore chosen the higher-order interactive theorem prover PVS for mechanical support. All theories and associated proof scripts can be downloaded here.

Comments and questions are welcome.
Last modified: Fri Apr 24 09:47:01 CEST 2009
Back to my home page.
Wim H. Hesselink, e-mail: w.h.hesselink@rug.nl