Compilation of Linearizable Data Structures: A Mechanised RG Logic for Semantic RefinementReport as inadecuate

Compilation of Linearizable Data Structures: A Mechanised RG Logic for Semantic Refinement - Download this document for free, or read online. Document in PDF available to download.

1 CELTIQUE - Software certification with semantic analysis Inria Rennes – Bretagne Atlantique , IRISA D4 - LANGAGE ET GÉNIE LOGICIEL 2 ENS Rennes - École normale supérieure - Rennes

Abstract : 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.

Keywords : Coq Verified Compilation Linearizability Rely Guarantee

Author: Yannick Zakowski - David Cachera - Delphine Demange - David Pichardie -



Related documents