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.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: ConcurrentIMP