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

Peter Gammie 🌐, Tony Hosking 🌐 and Kai Engelhardt

April 13, 2015

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.

License

BSD License

Topics

Session ConcurrentGC

Depends on

Cite

× 
@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   = {April},
  year    = {2015},
  note    = {\url{https://isa-afp.org/entries/ConcurrentGC.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: