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.
- 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.
Tony Hosking, Tony.Hosking<at>data61.csiro.au
|Ahmed Hussein, Mathias Payer, Tony Hosking and Chris Vick|
One process to reap them all: Garbage collection as-a-service
ACM SIGPLAN/SIGOPS 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ír 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, Volume 38, 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
PLDI 2015: the 36th annual 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