Skip to main content

Verified Concurrent Garbage Collection

x86-TSO memory model The GC and mutators collaborate in marking the heap
  • Modern programming languages rely on sophisticated run-time systems to provide valuable services to applications that enhance their reliability and maintainability. Mission-critical applications rely on these services to be trustworthy and bug-free. Among these services, automatic memory management (garbage collection) is key. Concurrent garbage collection is a long-standing target for formalization and proof because it captures complex concurrent behaviours and interactions between programs and their run-time environment. This project explores how to formalize and verify realistic concurrent, real-time, garbage collection algorithms, with a focus on the issues that arise when considering execution on modern relaxed consistency memory hierarchies. These pose new problems for formalization and proof, that require reasoning about non-sequentially-consistent programs that manipulate shared state via low-level non-blocking synchronization primitives. The objective is to provide a proof of a realistic garbage collector on real hardware, as a step towards verification of run-time systems as a trusted base for mission-critical applications.

  • Approach:

  • Contact:

    Tony Hosking, Tony.Hosking<at>



  • Kai Engelhardt
  • Peter Gammie
  • Tony Hosking
  • Yutaka Nagashima


Abstract PDF Adam Sandberg Ericsson, Magnus Myreen and Johannes ├ůman Pohjola
A verified generational garbage collector for CakeML
Journal of Automated Reasoning, Volume 63, Issue 2, pp. 463–488, August, 2019
Abstract PDF Ahmed Hussein, Mathias Payer, Tony Hosking and Chris Vick
One process to reap them all: Garbage collection as-a-service
International Conference on Virtual Execution Environments, pp. 171–186, Xi'an, China, April, 2017
Abstract to be published Stephen Blackburn, Amer Diwan, Matthias Hauswirth, Peter Sweeney, José Nelson Amaral, Tim Brecht, Lubom\'\ir Bulej, Cliff Click, Lieven Eeckhout, Sebastian Fischmeister, Daniel Frampton, Laurie Hendren, Michael Hind, Tony Hosking, Richard Jones, Tomas Kalibera, Nathan Keynes, Nathaniel Nystrom and Andreas Zeller
The truth, the whole truth, and nothing but the truth: A pragmatic guide to assessing empirical evaluations
ACM Transactions on Programming Languages and Systems, Volume 38, Issue 4, pp. 15:1-20, October, 2016
Abstract PDF Yi Lin, Steve Blackburn, Tony Hosking and Michael Norrish
Rust as a language for high performance GC implementation
International Symposium on Memory Management, pp. 89–98, Santa Barbara, California, USA, June, 2016
Abstract PDF Peter Gammie, Tony Hosking and Kai Engelhardt
Relaxing safely: verified on-the-fly garbage collection for x86-TSO
Proceedings of the 2015 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 11, Portland, Oregon, United States, June, 2015
Abstract PDF Yi Lin, Stephen M. Blackburn, Kunshan Wang, Tony Hosking and Michael Norrish
Stop and go: Understanding yieldpoint behavior
International Symposium on Memory Management, pp. 70–80, Portland, OR, USA, June, 2015
Abstract to be published Richard Jones, Tony Hosking and Eliot Moss
The garbage collection handbook: The art of automatic memory management
Chapman and Hall/CRC Press, 2011