A Typed Interface for Garbage Collection
Presenter: Mehmet
Preview
Dear denizens and fellows of PL Lab,
I will present “A Typed Interface for Garbage Collection” this Thursday for the first reading group of this quarter. I attached the paper to save you from the burden of searching it. I hope it will spark some interesting discussion as it is on the intersection of types, GC, and certified code (don’t be scared of the terms, we usually get to important notions and gist of definitions to make sure that everyone can enjoy the reading group).
Cheers, Mehmet
Summary
The paper focuses on statically verifying that a program’s stack will always conform to a shape parseable by a garbage collector (GC) while scanning the root set. The main motivation behind this is to have it as part of a certified programming system with a nontrivial high-performance GC with a subtle interface. The paper specifically focuses on making programs suitable for such a GC. It starts with a first-order functional programming language that manipulates the stack explicitly and has only continuation passing style (CPS) calls rather than normal function calls in many other languages. This The paper reformulates classical rules for function application as rules about shape of the stack vs. the shape that a function expects. Then, it focuses on the constructs in the language that can allocate memory and designs a type system that guarantees that each frame will point to the next one and each frame will have a structure parseable by a GC. To do so, they use LX type system to write of type-level functions to reason about: (1) the types and representations of objects on the stack, (2) correctness of shape of each stack frame w.r.t. the function that owns it, and (3) validity of the shape of the stack calls to other functions. Then they use these functions to impose restrictions on the shape of the stack and ask programmer for evidence values for certain cases. Finally, they show that the language is usable by compiling an ML-like language to the intermediate language they proposed.
Due to the presentation style and the density of the paper, it was difficult to follow. We commented on it saying that slowly building up the solution from smaller blocks could’ve been a better way of transmitting the ideas in the paper. Miroslav commented on the formal framework for reasoning about the stack, saying that it can be useful for static analysis of concatenative languages.
After the presentation, Kyle and I discussed whether such a formal system for interfacing a GC can be used as a starting point for fuzzing a GC, which is a difficult problem because interface for a GC is quite subtle and relies on the shape of the memory during program execution a lot.