Verified compilation of linearizable data structures
Yannick Zakowski, David Cachera, Delphine Demange, David Pichardie · 2018
Compiling concurrent and managed languages involves implementing sophisticated interactions between client code and the runtime system. An emblematic runtime service, whose implementation is particularly error-prone, is concurrent garbage collection. In a recent work [31], we implement an on-the-fly concurrent garbage collector, and formally prove its functional correctness in the Coq proof assistant. The garbage collector is implemented in a compiler intermediate representation featuring abstract concurrent data structures.