Rely-Guarantee Specification of a Concurrent Garbage Collector

Roger C. Su 📧 and Nisansala P. Yatapanage 📧

October 15, 2026

Abstract

We specify a model of the Ben-Ari concurrent garbage collector in the rely-guarantee paradigm, and verify its correctness. The aim is to show that the algorithm can be verified with rely-guarantee without the use of shared auxiliary variables. The approach is to reason that a certain property is maintained by one component for all instances of a variable, and then instantiate it to the particular instance required by the rely of the other component.

License

BSD License

Note

Some of the proofs were initially generated by Claude, and then extensively revised by hand.

Topics

Related publications

  • N. P. Yatapanage. "The complexity of interference: When rely/guarantee does not work." To appear in the 12th International Symposium on Dependable Software Engineering: Theories, Tools and Applications (SETTA 2026). Preprint available at arXiv:2609.27392.

Session RG_VDM_Garbage_Collector

Cite

× 
@article{RG_VDM_Garbage_Collector-AFP,
  author  = {Roger C. Su and Nisansala P. Yatapanage},
  title   = {Rely-Guarantee Specification of a Concurrent Garbage Collector},
  journal = {Archive of Formal Proofs},
  month   = {October},
  year    = {2026},
  note    = {\url{https://isa-afp.org/entries/RG_VDM_Garbage_Collector.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download