Verified Compilation of Linearizable Data Structures: Mechanizing Rely Guarantee for Semantic Refinement

Abstract : 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, 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. The present paper extends this work by considering the concrete implementation of some of these abstract concurrent data structures. We formalize, in the Coq proof assistant, a theorem establishing the semantic correctness of a compiling pass which translates abstract, atomic data structures into their concrete, fine-grained concurrent implementations. 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. Semantically, this instrumentation reflects the behavior of abstract data structures.
Document type :
Conference papers
Complete list of metadatas

Cited literature [30 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-01653620
Contributor : Yannick Zakowski <>
Submitted on : Friday, December 1, 2017 - 5:49:01 PM
Last modification on : Friday, September 13, 2019 - 9:48:42 AM

Identifiers

Citation

Yannick Zakowski, David Cachera, Delphine Demange, David Pichardie. Verified Compilation of Linearizable Data Structures: Mechanizing Rely Guarantee for Semantic Refinement. SAC 2018 - The 33rd ACM/SIGAPP Symposium On Applied Computing, Apr 2018, Pau, France. pp.1881-1890, ⟨10.1145/3167132.3167333⟩. ⟨hal-01653620⟩

Share

Metrics

Record views

829

Files downloads

209