We report on a machine-checked verification of safety for a state-of-the-art, on-the-fly, concurrent, mark-sweep garbage collector that is designed for multi-core architectures with weak memory consistency. The proof explicitly incorporates the relaxed memory semantics of x86 multiprocessors. To our knowledge, this is the first fully machine-checked proof of safety for 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 abstract model is detailed enough for its correspondence with an assembly language implementation to be straightforward.
@inproceedings{Gammie+2015PLDI,
author = {Gammie, Peter and Hosking, Antony L. and Engelhardt, Kai},
title = {Relaxing Safely: Verified On-the-Fly Garbage Collection for
x86-TSO},
booktitle = {ACM SIGPLAN International Conference on Programming Language
Design and Implementation},
series = {PLDI},
year = {2015},
month = {June},
address = {Portland, Oregon},
doi = {10.1145/2737924.2738006},
pages = {99-109},
acm = {http://dl.acm.org/authorize?N93651},
gscholar = {2}
}