Skip to Main content Skip to Navigation

Formal verification of the Pastry protocol

Abstract : Pastry is a structured P2P algorithm realizing a Distributed Hash Table over an underlying virtual ring of nodes. Several implementations of Pastry are available, but no attempt has so far been made to formally describe the algorithm or to verify its properties. Since Pastry combines complex data structures, asynchronous communication, and concurrency in the presence of spontaneous join and departure of nodes, it makes an interesting target for verification. This thesis focuses on the Join protocol of Pastry that integrates new nodes into the ring. All member nodes must have a consistent key mapping among each other. The main correctness property, named CorrectDelivery, states that there is always at most one node that can deliver an answer to a lookup request for a key and this node is the numerically closest member node to that key. This property is non-trivial to preserve in the presence of churn. In this thesis, unexpected violations of CorrectDelivery in the published versions of Pastry are discovered and analyzed using the TLA+ model checker TLC. Based on the analysis, the protocol IdealPastry is designed and verified using the interactive theorem prover TLAPS for TLA+. By relaxing certain hypotheses, IdealPastry is further improved to LuPastry, which is again formally proved correct under the assumption that no nodes leave the network. This hypothesis cannot be relaxed in general due to possible network separation when particular nodes simultaneously leave the network
Document type :
Complete list of metadata

Cited literature [83 references]  Display  Hide  Download
Contributor : Thèses UL Connect in order to contact the contributor
Submitted on : Thursday, March 29, 2018 - 12:43:46 PM
Last modification on : Saturday, October 16, 2021 - 11:26:08 AM


Files produced by the author(s)


  • HAL Id : tel-01750356, version 1



Tianxiang Lu. Formal verification of the Pastry protocol. Other [cs.OH]. Université de Lorraine, 2013. English. ⟨NNT : 2013LORR0179⟩. ⟨tel-01750356⟩



Record views


Files downloads