Relaxing safely: Verified on-the-fly garbage collection for x86-TSO

Peter Gammie, Antony L. Hosking, Kai Engelhardt

Research output: Contribution to journalArticlepeer-review

10 Citations (Scopus)


We report on a machine-checked verification of safety for a stateof-the-art, on-the-fly, concurrent, mark-sweep garbage collector that is designed for multi-core architectures with weak memory consistency. The proof explicitly incorporates the relaxed memory semantics of x86 multiprocessors. To our knowledge, this is the first fully machine-checked proof of safety for such a garbage collector. We couch the proof in a framework that system implementers will find appealing, with the fundamental components of the system specified in a simple and intuitive programming language. The abstract model is detailed enough for its correspondence with an assembly language implementation to be straightforward.

Original languageEnglish
Pages (from-to)99-109
Number of pages11
JournalACM SIGPLAN Notices
Issue number6
Publication statusPublished - Jun 2015
Externally publishedYes


Dive into the research topics of 'Relaxing safely: Verified on-the-fly garbage collection for x86-TSO'. Together they form a unique fingerprint.

Cite this