A. Rowstron, P. Druschel.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 anyPastry: 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.

Readynode (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.

- 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.

- 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]
- Tianxiang Lu. Formal Verification of the Pastry Protocol. PhD thesis, Universität des Saarlandes and Université de Lorraine, 2013.
- 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]
- Noran Azmy. A Machine-Checked Proof of Correctness of Pastry. PhD thesis, Universität des Saarlandes and Université de Lorraine, 2016.

Stephan Merz