Skip to main content

Verified Concurrent Garbage Collection

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>





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
PLDI 2015: the 36th annual 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