A Machine-Checked Correctness Proof for Pastry - Archive ouverte HAL Access content directly
Journal Articles Science of Computer Programming Year : 2018

A Machine-Checked Correctness Proof for Pastry

(1, 2) , (1, 3) , (1, 2)


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.
Fichier principal
Vignette du fichier
paper.pdf (367.58 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-01768758 , version 1 (17-04-2018)



Noran Azmy, Stephan Merz, Christoph Weidenbach. A Machine-Checked Correctness Proof for Pastry. Science of Computer Programming, 2018, 158, pp.64-80. ⟨10.1016/j.scico.2017.08.003⟩. ⟨hal-01768758⟩
227 View
180 Download



Gmail Facebook Twitter LinkedIn More