Verified Concurrent Garbage Collection

• 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:

  • We use Peter Sewell et al's model of x86-TSOl.
  • The model is encoded using synchronous message passing ala CCS / CSP, and a single global invariant is shown to hold.

• Contact:

  Tony Hosking, Tony.Hosking<at>data61.csiro.au

People

Publications

		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
		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
		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
		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
		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
		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
		Richard Jones, Tony Hosking and Eliot Moss The garbage collection handbook: The art of automatic memory management Chapman and Hall/CRC Press, 2011