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.
Type de document :
Communication dans un congrès
SAC 2018 - The 33rd ACM/SIGAPP Symposium On Applied Computing, Apr 2018, Pau, France. ACM, pp.1881-1890, 2018, 〈10.1145/3167132.3167333〉
Liste complète des métadonnées

Littérature citée [30 références]  Voir  Masquer  Télécharger

https://hal.archives-ouvertes.fr/hal-01653620
Contributeur : Yannick Zakowski <>
Soumis le : vendredi 1 décembre 2017 - 17:49:01
Dernière modification le : mercredi 3 octobre 2018 - 11:20:40

Fichier

Identifiants

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. ACM, pp.1881-1890, 2018, 〈10.1145/3167132.3167333〉. 〈hal-01653620〉

Partager

Métriques

Consultations de la notice

548

Téléchargements de fichiers

144