Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO

Title:	Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO
Authors:	Peter Gammie, Tony Hosking and Kai Engelhardt
Submission date:	2015-04-13
Abstract:	We use ConcurrentIMP to model Schism, a state-of-the-art real-time garbage collection scheme for weak memory, and show that it is safe on x86-TSO. This development accompanies the PLDI 2015 paper of the same name.
BibTeX:	@article{ConcurrentGC-AFP, author = {Peter Gammie and Tony Hosking and Kai Engelhardt}, title = {Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO}, journal = {Archive of Formal Proofs}, month = apr, year = 2015, note = {\url{http://isa-afp.org/entries/ConcurrentGC.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	ConcurrentIMP
Status: [skipped]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.