Garbage collection greatly simplifies the life of the programmer, removing the need for manually deallocating memory. However, heap space usage of garbage-collected programs can be tricky to understand: to argue that the garbage collector can reclaim the space associated with a heap object, one has to prove that this object is unreachable.
In this talk, I will present my PhD thesis work: a Separation Logic with space credits, allowing for the verification of heap space bounds in the presence of garbage collection. Crucially, this logic tracks the reachability of heap objects in a modular way, and allows for recovering space credits when the user proves an object unreachable.
I will focus on the challenges of concurrency. In particular, I will motivate the need for two novel language constructs — protected sections and polling points — and explain how they account for the subtleties of OCaml5’s stop-the-world garbage collection strategy. I will unveil how these constructs allow for safely writing standard lock-free data structures, and how we verify their intuitive heap space bounds using a form of “ahead-of-time deallocation”.
