founded in 1614  -  top 100 university

Research database

Publication

Lock-free parallel and concurrent garbage collection by mark&sweep

Gao, H., Groote, J. F. & Hesselink, W. H. 1-Feb-2007 In : Science of computer programming. 64, 3, p. 341-374 34 p.

Research output: Scientific - peer-reviewArticle

Documents

DOI

This paper presents a lock-free algorithm for mark&sweep garbage collection (GC) in a realistic model using synchronization primitives load-linked/store-conditional (LL/SC) or compare-and-swap (CAS) offered by machine arch i lectures. The algorithm is concurrent in the sense that garbage collection can run concurrently with the application (the mutator threads). It is parallel in that garbage collection itself may employ several concurrent collector threads.

We first design and prove an algorithm with a coarse grain of atomicity and subsequently apply the reduction method developed and verified in [H. Gao, W.H. Hesselink, A formal reduction for lock-free parallel algorithms, in: Proceedings of the 16th Conference on Computer Aided Verification, CAV, July 2004] to implement the high-level atomic steps by means of the low-level primitives. Even the correctness of the coarse grain algorithm is very delicate due to the presence of concurrent mutator and collector threads. We have verified it therefore by means of the interactive theorem prover PVS. (c) 2006 Elsevier B.V. All rights reserved.

Original languageEnglish
Pages (from-to)341-374
Number of pages34
JournalScience of computer programming
Volume64
Issue number3
StatePublished - 1-Feb-2007

Keywords

  • garbage collection, lock-free, shared-memory, correctness, theorem proving, ALGORITHM, PROGRAMS

View graph of relations

Download statistics

No data available

ID: 2794845