Verifying a Concurrent Garbage Collector using a Rely-Guarantee Methodology

Abstract : Concurrent garbage collection algorithms are an emblematic challenge in the area of concurrent program verification. In this paper, we address this problem by proposing a mechanized proof methodology based on the popular Rely-Guarantee (RG) proof technique. We design a specific compiler intermediate representation (IR) with strong type guarantees, dedicated support for abstract concurrent data structures, and high-level iterators on runtime internals. In addition, we define an RG program logic supporting an incremental proof methodology where annotations and invariants can be progressively enriched. We formalize the IR, the proof system, and prove the soundness of the methodology in the Coq proof assistant. Equipped with this IR, we prove a fully concurrent garbage collector where mutators never have to wait for the collector.
Type de document :
Communication dans un congrès
ITP 2017 - 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasília, Brazil. Springer, 10499, pp.496-513, 2017, Lecture Notes in Computer Science. 〈10.1007/978-3-319-66107-0_31〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01613389
Contributeur : Delphine Demange <>
Soumis le : mercredi 11 octobre 2017 - 15:10:27
Dernière modification le : mercredi 16 mai 2018 - 11:24:13
Document(s) archivé(s) le : vendredi 12 janvier 2018 - 15:08:43

Fichier

itp17.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, et al.. Verifying a Concurrent Garbage Collector using a Rely-Guarantee Methodology. ITP 2017 - 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasília, Brazil. Springer, 10499, pp.496-513, 2017, Lecture Notes in Computer Science. 〈10.1007/978-3-319-66107-0_31〉. 〈hal-01613389〉

Partager

Métriques

Consultations de la notice

709

Téléchargements de fichiers

43