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
Topics
Session ConcurrentGC
- Model
- Proofs_Basis
- Global_Invariants
- Local_Invariants
- Tactics
- Global_Invariants_Lemmas
- Local_Invariants_Lemmas
- Initial_Conditions
- Noninterference
- Global_Noninterference
- MarkObject
- Phases
- StrongTricolour
- TSO
- Valid_Refs
- Worklists
- Proofs
- Concrete_heap
- Concrete