Trustworthy Systems

Relaxing safely: verified on-the-fly garbage collection for x86-TSO

Authors

Peter Gammie, Tony Hosking and Kai Engelhardt

NICTA

Purdue University

UNSW

Abstract

We report the machine-checked verification of safety for an on-the-fly, concurrent, mark-sweep garbage collector in Isabelle/HOL. The collector is state-of-the-art in that it is designed for multi-core architectures with weak memory consistency. The proof explicitly accounts for both of these features, incorporating the x86-TSO model for relaxed memory semantics on x86 multiprocessors. To our knowledge, this is the first fully machine-checked proof of such a garbage collector. We couch the proof in a framework that system implementers will find appealing, with the fundamental components of the system specified in a simple and intuitive programming language. The framework is sufficiently detailed that correspondence between abstract model and assembly coded implementation is straightforward so as to allow formal refinement from model to implementation.

BibTeX Entry

  @inproceedings{Gammie_HE_15,
    address          = {Portland, Oregon, United States},
    author           = {Gammie, Peter and Hosking, Tony (Antony) and Engelhardt, Kai},
    booktitle        = {ACM SIGPLAN Conference on Programming Language Design and Implementation},
    doi              = {10.1145/2737924.2738006},
    editor           = {{Steve Blackburn}},
    keywords         = {formal verification, machine-checked proof, relaxed memory, tso},
    month            = jun,
    pages            = {11},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8488.pdf},
    publisher        = {ACM},
    title            = {Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-{TSO}},
    year             = {2015}
  }

Download