Compilation of Linearizable Data Structures

Yannick Zakowski (1, 2) , David Cachera (1) , Delphine Demange (1) , David Pichardie (1)

1 CELTIQUE - Software certification with semantic analysis
2 ENS Rennes - École normale supérieure - Rennes

Modern programming languages provide libraries for concurrent data structures. For better performance, these are implemented with fine-grained concurrency. Still, such implementations are linearizable: the programmer can safely assume that they behave atomically. We formalize this insight in Coq as an end-to-end theorem establishing the semantic preservation of a compiler translating abstract, atomic data structures into their concrete, fine-grained concurrent implementation. This embeds the notion of linearizable data structures in a formally verified compiler. At the crux of the proof lies a generic result establishing, once and for all, a simulation relation, starting from a carefully crafted rely-guarantee specification. Inspired by the work of Vafeiadis, implementations are annotated with linearization points, which instrument programs semantics to reflect the behavior of abstract data structures. We successfully applied our generic theorem to concurrent buffers, a data structure used in the implementation of concurrent garbage collectors.

Mots clés: Coq; Verified Compilation; Linearizability; Rely Guarantee

Domaines: Langage de programmation [cs.PL]

Yannick Zakowski, David Cachera, Delphine Demange, David Pichardie. Compilation of Linearizable Data Structures: A Mechanised RG Logic for Semantic Refinement. [Research Report] ENS Rennes; IRISA, Inria Rennes; Université Rennes 1. 2017. ⟨hal-01538128⟩