Formal proof of Pastry

Pastry is an algorithm for implementing a distributed hash table over a peer-to-peer overlay network. It was presented in the seminal paper
A. Rowstron, P. Druschel. Pastry: scalable, decentralized object location and routing for large-scale peer-to-peer systems. Proc. IFIP/ACM Intl. Conf. Distributed System Platforms (Middleware'01), LNCS 2218, pp. 329-350 (2001). Springer link.
As part of his PhD thesis, Tianxiang Lu modeled published versions of Pastry in TLA+ and verified his specifications using TLC, the TLA+ model checker. He discovered that the Pastry ring could become permanently disconnected when new nodes joined the ring, even in the absence of node failures. He then designed a version of Pastry that avoided this problem. The main idea was to allow any Ready node (i.e., a node that is fully integrated into the Pastry ring) to help only one new node at a time join the ring. He reduced the correctness property to key invariants and developed a proof using TLAPS, the TLA+ Proof System.

The low-level theory underlying the Pastry ring involves reasoning about (modulus) arithmetic, and arithmetic reasoning was poorly supported at the time of Tianxiang Lu's work. His TLA+ proof therefore assumed many facts about arithmetic, as well as other data structures, notably Pastry's leaf sets representing the neighborhood of a node. During her PhD thesis, Noran Azmy revisited the Pastry proof and discovered that many of these assumptions were actually wrong, essentially because they overlooked certain corner cases. Worse, at least one of Lu's invariants did not hold, and its proof had succeeded only because of unjustified assumptions. This was a harsh reminder that you should avoid using axioms in interactive proofs.

Subsequently, Noran Azmy rewrote the entire proof. She not only corrected (and proved!) the necessary low-level facts, but also introduced certain higher-level abstractions that simplified reasoning about the operations used in Pastry, and she rewrote the higher-level invariants. This led to a completely formal and machine-checked of Lu's variant of Pastry, still in a pure-join model, i.e. without nodes leaving the ring or failing.

Analyzing the proof, we realized that the final lease exchange phase of the join protocol was actually not needed for correctness. This phase was not present in the original Pastry protocol, but had been introduced in a subsequent technical report, presumably for ensuring more accurate information about the neighborhood of nodes. Lu had already shown that this additional step did not prevent the ring from disintegrating in the presence of node departures. Azmy ported her existing proof to a simplified version of the protocol, where lease exchange is replaced by a simple notification from the newly joined node to its helper node about the end of the join protocol.

The formal proofs are not for the faint of heart, consisting of some 30,000 lines of proof (for a few hundred lines of specification). They are made available here in order to document this effort. If you use them as a starting point for your own project, I'd love to hear from you.

Formal models and proofs

The main author of both proofs was Noran Azmy, based on work by Tianxiang Lu. Hernán Vanzetto, Stephan Merz, and Christoph Weidenbach also contributed ideas and proofs.
LuPastryPlus
TLA+ specifications and proofs of Lu's version of Pastry, in a pure-join model.
Simplified LuPastryPlus
TLA+ specifications and proofs of simplified version without lease exchanges, still in a pure-join model.

References

  1. Tianxiang Lu, Stephan Merz, Christoph Weidenbach. Towards Verification of the Pastry Protocol Using TLA+. 13th IFIP WG 6.1 Intl. Conf. Formal Techniques for Distributed Systems (FORTE 2011). © Springer, LNCS 6722, pp. 244-258 (2011). [PDF | Springer Link]
  2. Tianxiang Lu. Formal Verification of the Pastry Protocol. PhD thesis, Universität des Saarlandes and Université de Lorraine, 2013.
  3. Noran Azmy, Stephan Merz, Christoph Weidenbach. A Rigorous Correctness Proof for Pastry. 5th Intl. Conf. Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2016). © Springer, LNCS 9675, pp. 86-101 (2016). [PDF | Springer Link]
  4. Noran Azmy. A Machine-Checked Proof of Correctness of Pastry. PhD thesis, Universität des Saarlandes and Université de Lorraine, 2016.

Stephan Merz