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