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.shtml},
Formal proof development},
ISSN = {2150-914x},
}
|