Computer Science > Programming Languages
Title:Verification of a Generational Garbage Collector
View PDF HTML (experimental)Abstract:We have formally verified in Rocq+VST a multi-generation collector with support for mutable references, written in C and compatible with OCaml data types. Its carefully specified API supports C programs or CertiRocq (a verified compiler from Rocq to C) is similar to that of OCaml's collector. We have demonstrated the adequacy of our API specification for the mutator (client of the garbage collector) by verifying client programs. Our program and our verification are modular so that (1) the API spec is independent of the implementation (e.g., the choice of copying vs. mark-and-sweep, generational-vs-nongenerational) and (2) the specification and verification of components of the implementation (such as the forwarding function) are independent of other components (e.g., design decisions regarding older generations, multiple threads, or "remembered sets" of mutable references).
Bibliographic and Citation Tools
Code, Data and Media Associated with this Article
Demos
Recommenders and Search Tools
arXivLabs: experimental projects with community collaborators
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.