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

Peter Gammie 🌐, Tony Hosking 🌐 and Kai Engelhardt

April 13, 2015

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session ConcurrentGC

Depends on