Skip to Main content Skip to Navigation
Journal articles

A Machine-Checked Correctness Proof for Pastry

Noran Azmy 1, 2 Stephan Merz 1, 3 Christoph Weidenbach 1, 2
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
3 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
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.
Document type :
Journal articles
Complete list of metadata

Cited literature [24 references]  Display  Hide  Download
Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Tuesday, April 17, 2018 - 2:19:31 PM
Last modification on : Wednesday, November 3, 2021 - 7:09:25 AM


Files produced by the author(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⟩



Record views


Files downloads