Introduction of Pastry
The Pastry we are talking about here is not the delicious food, but a network protocol. The Pastry protocol is a structured Peer-to-Peer algorithm realizing a Distributed Hash Table (DHT) over an underlying virtual ring of nodes. Hash keys are assigned to the numerically closest node, according to their Ids that both keys and nodes share from the same Id space. Nodes join and leave the ring dynamically and it is desired that a lookup request from arbitrary node for a key is routed to the responsible node for that key which then delivers the message as answer.
Motivation
Several implementations of Pastry are available and have been applied in practice, but no attempt has so far been made to formally describe the algorithm or to verify its properties. Since Pastry combines rather complex data structures, asynchronous communication, concurrency, resilience to churn, i.e., spontaneous join and departure of nodes, it makes an interesting target for verification.
Research Focus
This thesis models Pastry's core algorithms, which provide the correct lookup service in the presence of churn and maintain a local data structures to adapt the dynamic updates of neighborhood.
This thesis focuses on Join protocol of Pastry and formally defines different statuses (from "dead" to "ready") of a node according to its stage during join. Only "ready" nodes are suppose to have consistent key mapping among each other and are allowed to deliver the answer message. The correctness property is identified by this thesis to be CorrectDelivery, stating 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 "ready" node to that key. This property is non-trivial to preserve in the presence of churn.
Methodology
The specification language TLA+ is used to model different versions (collected on the Web Page Formal Models) of Pastry algorithm starting with CastroPastry, followed by HaeberlenPastry, IdealPastry and finally LuPastry. In order to validate the models and to search for bugs, the TLA+ model checker TLC is employed to analyze several qualitative properties. Models are simplified for more efficient checking with TLC and to mitigate the state explosion problem.
Results
Through this thesis, unexpected violations of CorrectDelivery in CastroPastry and HaeberlenPastry are discovered and analyzed. Based on the analysis and improvements of HaeberlenPastry, the Pastry protocol IdealPastry is designed and first verified using the interactive theorem prover TLAPS for TLA+. IdealPastry is designed such that a "ready" node handles one joining node at a time and it assumes that (1) no departure of nodes (2) no concurrent join between two "ready" nodes closed to each other. The last assumption of IdealPastry is removed by its improved version LuPastry. In LuPastry, a "ready" node adds the joining node directly when it receives the join request and does not accepts any further join request until it gets the confirmation from the current joining node that it is "ready". LuPastry is proved to be correct w.r.t. CorrectDelivery under the assumption that no nodes leave the network, which cannot be further relaxed due to possible network separation when particular nodes simultaneously leave the network.