Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology

Abstract : Concurrent garbage collection algorithms are a challenge for program verification. In this paper, we address this problem by proposing a mechanized proof methodology based on the Rely-Guarantee proof technique. We design a compiler intermediate representation with strong type guarantees, dedicated support for abstract concurrent data structures, and high-level iterators on runtime internals. In addition, we define an Rely-Guarantee program logic supporting an incremental proof methodology where annotations and invariants can be progressively enriched. We formalize the intermediate representation, the proof system, and prove the soundness of the methodology in the Coq proof assistant. Equipped with this, we prove a fully concurrent garbage collector where mutators never have to wait for the collector.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, In press
Liste complète des métadonnées

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

https://hal.archives-ouvertes.fr/hal-01897251
Contributeur : Yannick Zakowski <>
Soumis le : mercredi 17 octobre 2018 - 02:45:51
Dernière modification le : mercredi 24 octobre 2018 - 01:09:57

Fichier

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

Identifiants

  • HAL Id : hal-01897251, version 1

Citation

Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, et al.. Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology. Journal of Automated Reasoning, Springer Verlag, In press. 〈hal-01897251〉

Partager

Métriques

Consultations de la notice

65

Téléchargements de fichiers

7