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
Past
|
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 |