A Rigorous Correctness Proof for Pastry

Abstract : Peer-to-peer protocols for maintaining distributed hash tables, such as Pastry or Chord, have become popular for a class of Internet applications. While such protocols promise certain properties concerning correctness and performance, verification attempts using formal methods invariably discover border cases that violate some of those guarantees. Tianxiang Lu reported correctness problems in published versions of Pastry and also developed a model, which he called LuPastry, for which he provided a partial proof of correct delivery assuming no node departures, mechanized in the TLA+ Proof System. Lu's proof is based on certain assumptions that were left unproven. We found counterexamples to several of these assumptions. In this paper, we present a revised model and rigorous proof of correct delivery, which we call LuPastry+. Aside from being the first complete proof, LuPastry+ also improves upon Lu's work by reformulating parts of the specification in such a way that the reasoning complexity is confined to a small part of the proof.
Type de document :
Communication dans un congrès
Michael J. Butler; Klaus-Dieter Schewe; Atif Mashkoor; Miklós Biró. Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, 2016, Linz, Austria. Springer, 9675, pp.86-101, 2016, 〈10.1007/978-3-319-33600-8_5〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01322342
Contributeur : Stephan Merz <>
Soumis le : vendredi 27 mai 2016 - 09:28:34
Dernière modification le : lundi 20 novembre 2017 - 15:14:02

Fichier

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

Identifiants

Collections

Citation

Noran Azmy, Stephan Merz, Christoph Weidenbach. A Rigorous Correctness Proof for Pastry. Michael J. Butler; Klaus-Dieter Schewe; Atif Mashkoor; Miklós Biró. Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, 2016, Linz, Austria. Springer, 9675, pp.86-101, 2016, 〈10.1007/978-3-319-33600-8_5〉. 〈hal-01322342〉

Partager

Métriques

Consultations de la notice

161

Téléchargements de fichiers

65