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 :
Theses
Complete list of metadatas

Cited literature [83 references]  Display  Hide  Download

https://hal.univ-lorraine.fr/tel-01750356
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 12:43:46 PM
Last modification on : Tuesday, April 24, 2018 - 1:30:05 PM

File

DDOC_T_2013_0179_LU.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-01750356, version 1

Collections

Citation

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

Share

Metrics

Record views

62

Files downloads

45