F* PoP Up Seminar: Mechanised Verification of an OCaml-style Garbage Collector
Nikhil Swamy
Mechanised Verification of an OCaml-style Garbage Collector
Sheera Shamsu, IIT Madras
Programming languages with managed runtimes often provide memory safety with the help of a garbage collector (GC). GCs are often implemented in an unsafe language like C and utilise low-level memory operations. Bugs in the GC implementation affects the memory safety guarantees of the managed language.
In this work, we present a specification and verification framework for GCs operating over OCaml-style objects. Unlike prior work, our correctness conditions are based on graph reachability, which permits evolution of the GC without having to rewrite the core safety specifications. Our framework is developed in F*, a proof-oriented solver-aided programming language, and its subset Low*, which facilitates extraction of verified C code. Using this framework, we have verified a stop-the-world mark and sweep GC which is compatible with OCaml. Our experimental results illustrates that the extracted verified code performs on par with a handwritten GC implementation.