@inproceedings{6d8d8fb2cd714c0db5214b1f26fddb11,
title = "Relaxing safely: Verified on-the-fly garbage collection for x86-TSO",
abstract = "We report on a machine-checked verification of safety for a stateofthe-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.",
keywords = "Formal verification, Machine-checked proof, Relaxed memory, TSO",
author = "Peter Gammie and Hosking, {Antony L.} and Kai Engelhardt",
note = "Publisher Copyright: {\textcopyright} 2015 ACM.; 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015 ; Conference date: 13-06-2015 Through 17-06-2015",
year = "2015",
month = jun,
day = "3",
doi = "10.1145/2737924.2738006",
language = "English",
series = "Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)",
publisher = "Association for Computing Machinery (ACM)",
pages = "99--109",
editor = "Steve Blackburn and David Grove",
booktitle = "PLDI 2015 - Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation",
address = "United States",
}