Verification of a Generational Garbage Collector

RESUMO

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).