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

Peter Gammie; Antony L. Hosking; Kai Engelhardt

doi:10.1145/2737924.2738006

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

Peter Gammie, Antony L. Hosking, Kai Engelhardt

Research output: Contribution to journal › Article › peer-review

11 Citations (Scopus)

Abstract

We report on a machine-checked verification of safety for a stateof-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.

Original language	English
Pages (from-to)	99-109
Number of pages	11
Journal	ACM SIGPLAN Notices
Volume	50
Issue number	6
DOIs	https://doi.org/10.1145/2737924.2738006
Publication status	Published - Jun 2015
Externally published	Yes

Access to Document

10.1145/2737924.2738006

Cite this

@article{34dd405547194e64bb787d69cab74996,

title = "Relaxing safely: Verified on-the-fly garbage collection for x86-TSO",

abstract = "We report on a machine-checked verification of safety for a stateof-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.",

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.",

year = "2015",

month = jun,

doi = "10.1145/2737924.2738006",

language = "English",

volume = "50",

pages = "99--109",

journal = "ACM SIGPLAN Notices",

issn = "1523-2867",

publisher = "Association for Computing Machinery (ACM)",

number = "6",

}

TY - JOUR

T1 - Relaxing safely

T2 - Verified on-the-fly garbage collection for x86-TSO

AU - Gammie, Peter

AU - Hosking, Antony L.

AU - Engelhardt, Kai

PY - 2015/6

Y1 - 2015/6

N2 - We report on a machine-checked verification of safety for a stateof-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.

AB - We report on a machine-checked verification of safety for a stateof-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.

KW - Formal verification

KW - Machine-checked proof

KW - Relaxed memory

KW - TSO

UR - http://www.scopus.com/inward/record.url?scp=84951111581&partnerID=8YFLogxK

U2 - 10.1145/2737924.2738006

DO - 10.1145/2737924.2738006

M3 - Article

AN - SCOPUS:84951111581

SN - 1523-2867

VL - 50

SP - 99

EP - 109

JO - ACM SIGPLAN Notices

JF - ACM SIGPLAN Notices

IS - 6

ER -

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

Abstract

Access to Document

Other files and links

Fingerprint

Cite this