A Machine-Checked Correctness Proof for Pastry

Noran Azmy 1, 2 Stephan Merz 1 Christoph Weidenbach 1, 2
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
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 metadatas

Cited literature [24 references]  Display  Hide  Download

https://hal.inria.fr/hal-01768758
Contributor : Stephan Merz <>
Submitted on : Tuesday, April 17, 2018 - 2:19:31 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:04 PM

File

paper.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

174

Files downloads

137