Gammie, PeterHosking, Antony L.Engelhardt, Kai2025-12-312025-12-311523-2867ORCID:/0000-0002-4487-6923/work/164436681https://hdl.handle.net/1885/733797501We 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.11enPublisher Copyright: © 2015 ACM.Formal verificationMachine-checked proofRelaxed memoryTSO201510.1145/2737924.273800684951111581