A Machine-Checked Correctness Proof for Pastry

Abstract : Protocols implemented on overlay networks in a peer-to-peer (P2P) setting promise flexibility, performance, and scalability due to the possibility for nodes to join and leave the network while the protocol is running. These protocols must ensure that all nodes maintain a consistent view of the network, in the absence of centralized control, so that requests can be routed to the intended destination. This aspect represents an interesting target for formal verification. In previous work, Lu studied the Pastry algorithm for implementing a distributed hash table (DHT) over a P2P network and identified problems in published versions of the algorithm. He suggested a variant of the algorithm, together with a machine-checked proof in the TLA+ Proof System (TLAPS), assuming the absence of node failures. We identify and correct problems in Lu's proof that are due to unchecked assumptions concerning modulus arithmetic and underlying data structures. We introduce higher-level abstractions into the specifications and proofs that are intended for improving the degree of automation achieved by the proof backends. These abstractions are instrumental for presenting the first complete formal proof. Finally, we formally prove that an even simpler version of Lu's algorithm, in which the final phase of the join protocol is omitted, is still correct, again assuming that nodes do not fail.
Type de document :
Article dans une revue
Science of Computer Programming, Elsevier, 2018, 158, pp.64-80. 〈10.1016/j.scico.2017.08.003〉
Liste complète des métadonnées

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

Contributeur : Stephan Merz <>
Soumis le : mardi 17 avril 2018 - 14:19:31
Dernière modification le : mercredi 18 avril 2018 - 01:24:19


Fichiers produits par l'(les) auteur(s)




Noran Azmy, Stephan Merz, Christoph Weidenbach. A Machine-Checked Correctness Proof for Pastry. Science of Computer Programming, Elsevier, 2018, 158, pp.64-80. 〈10.1016/j.scico.2017.08.003〉. 〈hal-01768758〉



Consultations de la notice


Téléchargements de fichiers