Noran Azmy

Stephan Merz

Christoph Weidenbach

A Rigorous Correctness Proof for Pastry

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

In a peer-to-peer network, individual nodes -called peers -communicate directly with each other and act as both suppliers and users of a given service. One such service that can be implemented by a peer-to-peer protocol is a distributed hash table (DHT): a decentralized distributed system that provides a lookup service similar to a hash table, but where the responsibility for storing key-value pairs is divided among the different nodes on the network. Nodes can efficiently retrieve the value associated with a given key by sending a lookup message for that key. Correct routing guarantees that lookup messages arrive at the node responsible for storing the key-value pair. Pastry [START_REF] Rowstron | Pastry: Scalable, Decentralized Object Location and Routing for Large-Scale Peer-to-Peer Systems[END_REF] and Chord [START_REF] Stoica | Chord: A Scalable Peer-to-peer Lookup Service for Internet Applications[END_REF] are well-known examples of protocols implementing DHTs.

Using Alloy to formally model and verify Chord, Zave [START_REF] Zave | Using Lightweight Modeling to Understand Chord[END_REF] showed that the join protocol is correct provided that no node leaves the network, but that the full version of the protocol may not maintain the claimed invariants. In [START_REF] Zave | How to Make Chord Correct (Using a Stable Base)[END_REF], she presented a version of Chord with a partially-automated proof of correctness. Lu discovered similar correctness problems for Pastry using the TLA + proof assistant [START_REF] Lu | Formal Verification of the Pastry Protocol Using TLA +[END_REF]. Some other work has been done in this area that does not rely on mechanized verification, i.e., model checking or theorem proving. Borgström et al. [START_REF] Borgström | Verifying a Structured Peer-to-Peer Overlay Network: The Static Case[END_REF] used CCS to verify correctness of the DKS look-up protocol, assuming that the network remains stable (i.e., nodes neither join nor leave). Bakhshi et al. [START_REF] Bakhshi | Verification of Peer-to-Peer Algorithms: A Case Study[END_REF] used process algebra to formally verify the stabilization process of Chord.

Like Lu, we are interested in the formal verification of Pastry using the TLA + proof system, w.r.t. the safety property correct delivery [START_REF] Lu | Formal Verification of the Pastry Protocol Using TLA +[END_REF]: At any point in time, there is at most one node that answers a lookup request for a key, and this node must be the closest live node to that key.

TLA + [START_REF] Lamport | Specifying Systems: The TLA + Language and Tools for Hardware and Software Engineers[END_REF] is a formal specification language that mainly targets concurrent and distributed systems. It is based on untyped Zermelo-Fraenkel set theory for specifying data structures, and the Temporal Logic of Actions, a variant of linear temporal logic, for describing system behavior. Systems are specified as state machines over a tuple of state variables by defining a state predicate Init and a transition predicate Next that constrain the possible initial states and the next-state relation. Transition predicates (also called actions) are first-order formulas that contain unprimed and primed state variables for denoting the values of the variables in the state before and after the transition. Validation of TLA + specifications is mechanized by TLC [START_REF] Yu | Model checking TLA + Specifications[END_REF], an explicit-state model checker for finite instances of TLA + specifications, and formal verification by TLAPS, the TLA + Proof System [START_REF] Cousineau | TLA + Proofs[END_REF]. TLAPS is based on a hierarchical proof language; the user writes a TLA + proof in the form of a hierarchy of proof steps, each of which is interpreted by the proof manager, which generates corresponding proof obligations and passes them to automatic back-end provers, including Zenon, Isabelle/TLA + , and SMT solvers. Larger steps that cannot be proven directly by any of the back-end provers can be broken further into sub-steps. Because the language is untyped, part of the proof effort consists in proving a typing invariant that expresses the shapes of functions and operators.

Using model checking and theorem proving, Lu discovered several problems in the original Pastry protocol and presented a variant of the protocol, called LuPastry, for which he verified correct delivery under the strong assumption that nodes never fail (i.e., leave the network). Notably, his Pastry variant enforces that a live node may only facilitate the joining of one new node at a time. Lu's proof reduces correct delivery to a set of around 50 claimed invariants, which are proven with the help of TLAPS. As such, LuPastry represents a major effort in the area of computer-aided formal verification of distributed algorithms. Still, the proof relies on many unproven assumptions relating to arithmetic and to protocol-specific data structures. Upon examining these assumptions, we discovered counter-examples to several of them. While we were able to prove stronger variants of many assumptions, this was not possible for others. In fact, we were able to find a counter-example to one of Lu's claimed main invariants, for which the TLA + proof was only possible because of incorrect assumptions. Fixing these problems led to a redesign of the overall proof.

Our contribution in this paper is LuPastry + : a revised specification and complete proof of correct delivery for LuPastry. While the essentials of the actual protocol are not changed, we improve on the LuPastry specification by fixing some unhandled border cases and introducing abstractions in some operator definitions that make the specification more modular and confine the reasoning complexity to a small part of the proof. The new abstractions typically lead to a significant reduction of the size of higher-level proofs. Moreover, our proof does not rely on unproven assumptions, because all low-level lemmas have been proved using TLAPS.

The paper is organized as follows. Section 2 describes the main aspects of the original LuPastry model, which are also in LuPastry + . We explain our contribution and the structure of the LuPastry + proof in Section 3. A sketch of the machine-checked proof is given in Section 4. Section 5 summarizes our results and our experience in using TLAPS.

The (Lu)Pastry Model

The Pastry network can be visualized as a ring of keys I ∆ = 0 . . 2 M -1 for some positive integer M (see Figure 1). Each live node is assigned a unique key k ∈ I as an identifier and needs to determine its coverage: a contiguous range of keys, including the node's own ID, that the node is responsible for, or covers. If a node i covers key k , then i considers itself (1) the proper recipient of all look-up messages addressed to k , and (2) the node responsible for facilitating the joining of any new node with ID k . In the absence of a central server and shared memory, live nodes need to rely on message passing and local information to agree on a proper division of coverage.

Let ready nodes be the live nodes that are not in the process of joining the network (they are fully-joined). Ready nodes are of particular interest since only ready nodes may accept look-up messages or facilitate the joining of new nodes. Ideally, the coverage ranges computed by all ready nodes (1) do not overlap, (2) cover the whole range of keys, and (3) are computed based on the smallest absolute distance to the node: if a ready node i covers key k , then k is closer to i in terms of absolute ring distance than it is to any other ready node j = i , with a rule for breaking ties. These conditions all hold for the ring illustrated in Figure 1. Condition (2) may be temporarily violated when a new node joins but is not yet ready, thus the safety property that we are interested in verifying requires only (1) and (3).

For two nodes x and y, we may be interested in the clockwise distance from x to y, or the absolute (shortest) distance between x and y.

ClockwiseDistance(x , y)

∆ = if y ≥ x then y -x else RingSize -x + y AbsoluteDistance(x , y) ∆ = let d 1 ∆ = ClockwiseDistance(x , y) d 2 ∆ = ClockwiseDistance(y, x ) in if d 1 ≤ d 2 then d 1 else d 2
A node i computes its coverage by maintaining a leaf set: a set containing what i believes to be its L live neighbor nodes on both the left and right sides, where the positive integer L is a parameter of the specification. LeftNeighbor is defined analogously. choose denotes Hilbert's choice operator and will be discussed further in Section 3. Node i considers its coverage range as the interval [LeftCoverage(ls), RightCoverage(ls)], where the key LeftCoverage(ls) is the midpoint between LeftNeighbor (ls) and i , and similarly, RightCoverage(ls) is the midpoint between i and RightNeighbor (ls). In Figure 1, assuming up-to-date leaf sets, node 0's left and right neighbors are 11 and 7, respectively. Therefore, its coverage is the interval [14, 3] (i.e., the set of keys {14, 15, 0, 1, 2, 3}).

LeftCoverage(ls)

The Pastry model presented here is called LuPastry [START_REF] Lu | Formal Verification of the Pastry Protocol Using TLA +[END_REF], in which two main restrictions are introduced to the dynamic behavior of the protocol: (1) nodes are assumed to never fail (leave the network), and (2) a ready node may facilitate the joining of at most one new node at a time.

The main dynamic aspect of the protocol is the join process, explained as follows (see also Figure 2). In LuPastry, each node is either Dead (not shown), Waiting (white), OK (gray) or Ready (black). Only Ready nodes facilitate the joining of new nodes into the network. A Dead node i that decides to join the network turns to Waiting and sends a join request to a Ready node j that it knows about. The request is forwarded to the Ready node k that covers key i . Node k responds to i 's request when it is free for handling a new join request, and communicates to i its own leaf set. Node i receives k 's reply and, in order to construct its proper leaf set, sends probe messages to the nodes in the leaf set received from k . All non-Dead nodes that receive the probe add i to their leaf set if appropriate (i.e., if node i is among the L closest live neighbor nodes), and send a probe reply to i with their own leaf set information. This process continues until i has probed all nodes it has heard about and that are close enough to i to be in i 's leaf set, then i becomes OK. In order for i to become Ready and eventually serve the IDs closest to i , node i has to exchange leases with both its left and right neighbors (one of which must be k ). Node i sends out lease request messages to both its neighbors. If i 's neighbor is Ready or OK, and also considers i to be its neighbor, it grants i the lease in a lease reply message. When i has received lease replies from both its neighbors, it switches to Ready, and grants its neighbors leases in turn. When k receives i 's lease, it may help other new nodes join the ring.

k i j r (
The global state of the LuPastry network is represented as the tuple vars of state variables. 5vars ∆ = Messages, Status, LeafSets, Probing, Leases, Grants, ToJoin Messages represents the set of messages currently in transmission. Variables Status and LeafSets are arrays whose i -th entries are the current status and leaf set of node i . Similarly, Probing[i ] is the set of nodes that node i has probed but has not heard back from yet, Leases[i ] and Grants[i ] are the set of nodes i has acquired leases from, and granted leases to, respectively. Lastly, ToJoin[i ] designates the node that is currently joining through i , if any, otherwise ToJoin[i ] = i .

The TLA + specifications of the initial state and of the next-state relation are defined by the operators Init and Next shown in Fig. 3; they use auxiliary operators that represent elementary operations on leaf sets and routing tables, and that define the individual transitions of the Pastry protocol. The constant A is a parameter of the specification designating the nodes that are live (and Ready) initially. Note that, because LuPastry is a distributed system, each action may modify the local variables of at most one node i , the node executing it, besides the set Messages. The TLA + specification of LuPastry is defined as the formula Spec

∆ = Init ∧ 2[Next] vars .
EmptyLS (i ) is a leaf set owned by i with no nodes in the right and left sides. AddToLS (a, ls) is the leaf set obtained by adding the set of nodes a to ls. In case of an overflow, the new right (resp., left) leaf set consists of the L closest nodes to i from the right (resp., left); nodes that are farther away are discarded.

Init ∆ = ∧ Messages = {} ∧ Status = [i ∈ I → if i ∈ A then "Ready" else "Dead"] ∧ ToJoin = [i ∈ I → i] ∧ Probing = [i ∈ I → {}] ∧ Leases = [i ∈ I → if i ∈ A then A else {i}] ∧ Grants = [i ∈ I → if i ∈ A then A else {i}] ∧ LeafSets = [i ∈ I → if i ∈ A then AddToLS (A, EmptyLS (i)) else EmptyLS (i)] Next ∆ = ∃i, j ∈ I : ∨ Lookup(i, j ) ∨ RouteLookup(i, j ) ∨ DeliverLookup(i, j ) ∨ Join(i, j ) ∨ RouteJoinRequest(i, j ) ∨ ReceiveJoinRequest(i) ∨ ReceiveJoinReply(i) ∨ ReceiveProbe(i) ∨ ReceiveProbeReply(i) ∨ RequestLease(i) ∨ ReceiveLeaseRequest(i) ∨ ReceiveLeaseReply(i)

The LuPastry + Model and Proof

Our contribution is illustrated in Figure 4, and can be divided into two parts: (1) changes to the TLA + specification of LuPastry, and (2) the first complete proof of correctness. The Refined LuPastry Specification

Changes to the LuPastry Specification

At the bottom layer, we refine LuPastry [START_REF] Lu | Formal Verification of the Pastry Protocol Using TLA +[END_REF] as follows. In order for the proof to gain in modularity, readability, and simplicity, we introduce additional operators that abstract away from arithmetic calculations and reduce the use of TLA + 's choose operator, which is difficult for back-end provers to reason about and hence restrains automation. This also makes the specification more concise.

Arithmetic calculations, which mainly involve comparisons between distances between nodes on the ring, appeared so extensively in LuPastry that arithmetic reasoning was frequently needed at the top level of the original proof. For example, typical subformulas ClockwiseDistance(i , j ) ≤ ClockwiseDistance(i , k ) require that the definition of ClockwiseDistance be unfolded. Instead, in LuPastry + we define a predicate ClockwiseArc(i , j , k ), which holds if j lies on the clockwise path from i to k .

ClockwiseArc(i , j , k ) ∆ = ClockwiseDistance(i , j ) ≤ ClockwiseDistance(i , k )
We then prove once and for all the necessary properties of this relation in TLAPS, using the SMT backend for arithmetical reasoning, so that unfolding of the definition is no longer needed in the top-level proof. The following are some examples of these properties.

theorem ArcAntiSymmetry ∆ = ∀ x , y, z ∈ I : ∧ ClockwiseArc(x , y, z ) ∧ ClockwiseArc(x , z , y) ⇒ y = z ∧ ClockwiseArc(x , y, z ) ∧ ClockwiseArc(y, x , z ) ⇒ x = y theorem ArcRotation ∆ = ∀ x , y, z ∈ I : ∧ x = y ∧ ClockwiseArc(x , y, z ) ⇒ ClockwiseArc(y, z , x ) ∧ y = z ∧ ClockwiseArc(x , y, z ) ⇒ ClockwiseArc(z , x , y)
This abstraction helps automate the proof process since now automatic backends like Zenon or Spass without native support for integer arithmetic are able to solve larger steps.

A related issue is the extensive use of Hilbert's ε-operator for definite choice. The TLA + expression choose x ∈ S : P (x ) denotes some fixed but arbitrary element x in set S for which the property P holds, if some such x exists. If P holds for no x ∈ S , as in choose x ∈ Nat : x * 0 = 1, the result of the choose expression is not specified.

The LuPastry definition of the operator RightNeighbor , shown in the previous section, uses choose. It is unwieldy to reason about operator RightNeighbor by unfolding its definition because we would invariably have to show the existence of a node contained in ls.right and whose distance to ls.node is minimal among all these nodes. Formally, we need the following lemma:

lemma ∀x ∈ I , S ∈ (subset I ) \ {{}} : ∃y ∈ S : ∀z ∈ S : ClockwiseDistance(x , y) ≤ ClockwiseDistance(x , z )
In LuPastry + , we perform three changes. First, we redefine RightNeighbor to abstract away from the choose expression. The new term ClosestFromTheRight is itself defined in terms of choose, but generalizes the previous operator and reuses the operator ClockwiseArc introduced above. Second, since ClosestFromTheRight is defined using a choose expression, we add a lemma that guarantees the existence of a value satisfying the characteristic predicate.

lemma choose ClosestFromTheRight ∆ = ∀ x ∈ I , a ∈ subset I : a = {} ⇒ ∃ y ∈ a : ∀ z ∈ a : ClockwiseArc(x , y, z )
Third, we add type and expansion lemmas that respectively provide type information and the relevant properties of ClosestFromTheRight. We introduce similar lemmas for operator RightNeighbor .

lemma type ClosestFromTheRight ∆ = ∀ x ∈ I , a ∈ subset I : ClosestFromTheRight(x , a) ∈ I lemma def ClosestFromTheRight ∆ = ∀ x ∈ I , a ∈ subset I : ∧ a = {} ⇒ ClosestFromTheRight(x , a) = x ∧ a = {} ⇒ ClosestFromTheRight(x , a) ∈ a ∧ ∀ y ∈ a : ClockwiseArc(x , ClosestFromTheRight(x , a), y)
We illustrate the effect of these abstractions using a simple lemma about adding new nodes to the leaf set data structure, that we prove once with and once without the use of the new operators. lemma ∀ ls ∈ LeafSet, a ∈ subset I : IsProper (AddToLS (a, ls))

Basically, the lemma says that the leaf set obtained by adding some new nodes to a leaf set is "proper", where "proper" is defined as follows.

IsProper (ls) ∆ = ∧ ∀ x ∈ ls.left \ ls.right, y ∈ ls.right : ClockwiseArc(y, x , ls.node) ∧ ∀ x ∈ ls.right \ ls.left, y ∈ ls.left : ClockwiseArc(ls.node, x , y)

The proof P 1 of this lemma according to the original definition of IsProper consists of 23 interactive proof steps that generate 64 proof obligations. With our new abstractions, the new proof P 2 consists of only 12 interactive proof steps (40 proof obligations). This significant difference comes from the fact that the new operators allow back-end provers to succeed directly on some steps in P 2 , which have to be broken down into further substeps in the original proof P 1 . Already for this simple example we observe a 50% reduction in the number of steps, i.e., user interactions. 6Additionally, we fix some corner cases in the original specification. We modify the probing process so that the node does not probe itself. This is clearly unnecessary, and removing it simplifies some parts of the proof. We also add a missing border case to the TLA + formula FindNext(i , j ) that computes the next hop on the route from node i to node j .

New Proof of Correctness

The upper layers of Figure 4 compare our new proof to Lu's original proof. The original LuPastry proof relied on a large number of unproven assumptions. In attempting to prove these assumptions, we found counter-examples to many of them, such as arithmetic assumptions ignoring border cases. Moreover, several assumptions were not actually used in the proof. For example, Lu's proof relied on 112 unproven assumptions about the leaf set data structure. Upon examining these assumptions, we could prove only 21 directly. We discovered that more than 30 were unused in Lu's proof. The rest of the assumptions were incorrect. Our analysis of Lu's assumptions led us to reformulate those that were needed for the top-level proof. This was possible for all but 6 of the incorrect assumptions. The following assumption, used by Lu as an unproven TLA + lemma, states that after adding some set of nodes a to a leaf set ls1, the right neighbor of the resulting leaf set ls2 can only be closer to the leaf set owner i than the original right neighbor of ls1.

lemma ∀ ls1, ls2 ∈ LeafSet, i ∈ I , a ∈ subset I : i = ls1.node ∧ ls2 = AddToLS (a, ls1) ⇒ ClockwiseDistance(i , RightNeighbor (ls2)) ≤ ClockwiseDistance(i , RightNeighbor (ls1))
This lemma does not hold if the right-hand part of the leaf set is empty (i.e., ls1.right = {}), because in this case RightNeighbor (ls1) = i and i is closer to itself than to any other node. The lemma was therefore reformulated as follows.

lemma ∀ ls1, ls2 ∈ LeafSet, i ∈ I , a ∈ subset I : i = ls1.node ∧ ls1.right = {} ∧ ls2 = AddToLS (a, ls1) ⇒ ClockwiseDistance(i , RightNeighbor (ls2)) ≤ ClockwiseDistance(i , RightNeighbor (ls1))
Other assumptions had to be eliminated entirely. For example,

lemma ∀ ls ∈ LeafSet, k ∈ I : LeafSetContent(AddToLS ({k }, ls)) \ {k } = LeafSetContent(ls)
states that the leaf set obtained by adding a node k to some leaf set ls, contains the same nodes in ls, and possibly also k . This is not true: if ls is full, adding a new node k to it will generally result in some other node being removed from the leaf set, invalidating the claimed equality. 7 Aside from reformulating and proving some assumptions from the original proof, we also added and proved many new facts that were helpful for the proof, resulting in more lemmas in the "Leaf Set Properties" layer.

In the top level of the proof, Lu proves correct delivery by reducing the property to 50 other properties and proves that these properties are invariants of LuPastry, based on the (partly wrong) assumptions made in the lower levels of the proof. Since some assumptions were discovered to fail, the following property SemJoinLeafSet is, in fact, not an invariant.

SemJoinLeafSet ∆ = ∀m ∈ Messages : m.content.type = "JoinReply" ⇒ let n ∆ = m.content.ls.node in ∧ ClockwiseDistance(LeftNeighbor (LeafSets[n]), n) ≤ ClockwiseDistance(LeftNeighbor (m.content.ls), n) ∧ ClockwiseDistance(n, RightNeighbor (LeafSets[n]))
≤ ClockwiseDistance(n, RightNeighbor (m.content.ls))

The predicate asserts that if some node n sends a JoinReply message then n's current neighbors are closer to it than its neighbors were at the time when the message was sent. This is not true, however, if n's leaf set was empty at the time the message was sent. As mentioned earlier, in case of an empty leaf set, the left and right neighbors of node n are n itself. Any new neighbors of n will be farther away from n than n itself.

We have written a new, complete correctness proof for correct delivery of the revised protocol specification that does not rely on any unproven assumptions (see Figure 4(b)). At the lowest level of the proof we have 82 lemmas about arithmetic. The abstraction layer provides some 80 lemmas relating to our new operators. The leaf set layer consists of 155 lemmas about the leaf set data structure. On top of this basis are 80 correctness invariants. All lemmas have fully machine-checked proofs.

Because our proof is rigorous, there was a need for a larger number of invariants than in Lu's proof. Also, some of the more involved invariants were split into several invariants in order to facilitate their proof. While our new proof LuPastry + shares some invariants with the original proof of LuPastry, there is no one-to-one correspondence between the two sets of invariants. In particular, while Lu's original proof depends more on the lease exchange phase of the protocol, our own correctness invariants focus more on probing.

A Proof of Correctness for LuPastry +

Our main TLA + theorem LuPastryCorrectness proves correct delivery, as expressed by the following predicate [START_REF] Lu | Formal Verification of the Pastry Protocol Using TLA +[END_REF], as an invariant of LuPastry + . The full TLA + specification and proof are available online [START_REF]LuPastry + : Specification and Proof Files[END_REF]. 8

CorrectDelivery

∆ = ∀ i , k ∈ I : enabled DeliverLookup(i , k ) ⇒ ∧ ∀ n ∈ I : n = i ∧ Status[n] = "Ready" ⇒ AbsoluteDistance(i , k ) ≤ AbsoluteDistance(n, k ) ∧ ∀ j ∈ I \ {i } : ¬enabled DeliverLookup(j , k ) theorem LuPastryCorrectness ∆ = Spec ⇒ 2CorrectDelivery
Action DeliverLookup is defined as follows.

DeliverLookup(i , j ) ∆ = ∧ Status[i ] = "Ready" ∧ Covers(LeafSets[i ], j ) ∧ ∃ m ∈ Messages : ∧ m.content.type = "Lookup" ∧ m.destination = i ∧ m.content.node = j ∧ Messages = (Messages \ {m}) ∧ unchanged Status, LeafSets, Probing, Leases, Grants, ToJoin
In what follows, we use shorthand notation instead of the full names of TLA + functions/operators for compactness. RN (i ) = RightNeighbor (LeafSets[i ]), and CR(i ) = ClosestFromTheRight(i , ReadyNodes \ {i }) is the closest Ready/OK node to node i from the right. LN (i ) and CL(i ) are defined analogously. We use i 1 . . . i n to denote a clockwise path on the ring; this is similar to the TLA + operator ClockwiseArc, but extended to an arbitrary number of nodes. The shortest "absolute" path between two nodes i and j may be i j or j i ; we denote this shortest path by i j . In a ring of 16 nodes, for example, (3 5) = (3 5), but (3 15) = (15 3). We write |p| for the length of the path p.

The idea of our proof is intuitive. As pointed out in Section 2, we basically need to prove non-overlapping coverage, i.e., that the coverage of any ready node r 2 starts strictly after the coverage of any other ready node r 1 ends.

NonOverlappingCoverage ∆ = ∀ r 1, r 2 ∈ ReadyNodes : r 1 = r 2 ⇒ ClockwiseDistance(r 1, RightCoverage(LeafSets[r 1])) < ClockwiseDistance(r 1, LeftCoverage(LeafSets[r 2]))
It is easy to prove non-overlapping coverage if we prove the following property, which (adapting notation) was already pointed out by Lu [START_REF] Lu | Formal Verification of the Pastry Protocol Using TLA +[END_REF] as a main invariant.

CloseNeighbors ∆ = ∀ r 1, r 2 ∈ ReadyNodes : r 1 = r 2 ⇒ ∧ ClockwiseArc(r 1, RightNeighbor (LeafSets[r 1]), r 2) ∧ ClockwiseArc(r 2, LeftNeighbor (LeafSets[r 1]), r 1)
We prove CloseNeighbors by proving a stronger property which we call stable network. A node i is stable if CR(i ) and CL(i ) are in i 's leaf set (Figure 5a). A Pastry ring is stable if all Ready or OK nodes are stable. It is clear that in a stable ring, the properties CloseNeighbors, and consequently NonOverlappingCoverage hold. For a minimum leaf set size L = 3, stable network is an invariant of LuPastry + . Let a participating node be a node that is either Ready or OK, or is the to-join node of a Ready node. Essentially, a participating node is any node that is known to some Ready or OK node. Let i and j be two consecutive Ready or OK nodes on the ring (see Figure 5b). There can be at most two participating nodes k 1 , k 2 between i and j : the to-join nodes of i and j . Any other non-Dead node between i and j must be a Waiting node whose join request has not been picked up by i or j (since they are busy facilitating the joins of k 1 and k 2 ), and so it can not be in the leaf sets of i or j . For a minimum leaf set size L = 3, we can ensure that stable i and j remain stable even if new nodes are added to their leaf sets.

We observe that the ring has the following properties, which we have proven in TLA + . P1 The coverage of a node is computed based on half the distance to its neighbors. A key k covered by a node i lies in either the right or left coverage regions of i (see Fig. 1). If i and j are leaf set neighbors, i.e., i = LN (j ) and j = RN (i ), their coverage regions cannot overlap.

P2 If k is in i 's right (left) coverage region, i k RN (i ) (LN (i ) k i ))
. P3 If i is a stable node and r = i is some Ready or OK node, then i RN (i ) r and r LN (i ) i . P4 Because we exclude node failure, all protocol actions that modify a node's leaf set do so through the operation AddToLS . Therefore, nodes are not purposely removed from a leaf set, but a node j may only be evicted from the leaf set for node i through an AddToLS operation that results in an overflow; i.e., if the leaf set of i becomes full and j is replaced by another node that is closer to i . P5 A new node k joins the network through a Ready node i that initially covers it, and so k will remain closest to i on one side (right or left) until it finishes its join process. i . P6 If the leaf set size L ≥ 3, no action can cause CR(i ) or CL(i ) to be removed from i 's leaf set due to an overflow (see Figure 5b). P7 At any point in time, a participating node i is either probing CR(i ) (resp., CL(i )), or CR(i ) (resp., CL(i )) is in i 's leaf set. P8 At any point in time, a participating node i is either probing CR(i ) (resp., CL(i )), or i is in the leaf set of CR(i ) (resp., CL(i )).

Using these properties, our proof can be outlined in two theorems. right coverage region and j 's left coverage region. Therefore, i k RN (i ) j and i LN (j ) k j , by P2, P3. In order for both to hold, it must be that i = LN (j ) and j = RN (i ). Therefore, the coverage regions of i and j cannot overlap (contradiction, by P1). Therefore, in a stable LuPastry + network, two Ready nodes i and j cannot both think they cover the same key k , and so at most one of DeliverLookup(i , k ) and DeliverLookup(j , k ) is enabled.

It remains to show that if DeliverLookup(i , k ) is enabled then i is closer to k than any other Ready node r is in terms of absolute distance on the ring. Assume again that k is in i 's right coverage region, and so i k RN (i ) r (by P3). Because k lies within half the distance from i to RN (i ) (by P1), k must lie within half the distance from i to r . Therefore, |i

k | = |i k | ≤ |k r |. If |r k | = |k r |,
(i ) = CL(i )).
Therefore, e = ReceiveProbeReply(j ) and CR e (i ) = j . Now, i = CL (j ). By P8 and since j 's probing set is empty, j is in i 's leaf set. Therefore, i remains stable.

The total TLA + proof consists of more than 30,000 lines. The time taken to run the proof manager on the entire proof is 8 hours and 57 minutes on a single Intel Xeon(R) CPU E5-2680 core running at 2.7GHz with 256GB RAM.

Conclusion

This paper presents LuPastry + : the first completely machine-checked proof of correct delivery for the variant of Pastry introduced by Lu [START_REF] Lu | Formal Verification of the Pastry Protocol Using TLA +[END_REF]. Like Lu's proof, our proof has been mechanized in the TLA + proof system. Compared to Lu's specification, we introduce some new TLA + operators that abstract away from arithmetic reasoning and other troublesome TLA + constructs, and this helps avoid low-level arithmetic reasoning at higher levels of the proof. Most importantly, our proof no longer relies on any unproven assumptions. Because we filled all the holes, our overall proof is longer (more than 30,000 lines overall) than Lu's original proof. Nevertheless, our new operators helped significantly reduce the number of steps in the main proof.

Lu [START_REF] Lu | Formal Verification of the Pastry Protocol Using TLA +[END_REF] shows that correct delivery does not hold for the original published specification of Pastry, in particular in the case of node failure. Like Lu's original proof, our proof assumes that nodes never fail and focuses only on the join protocol. An interesting future work would be to identify assumptions on node failures that maintain the correctness of the protocol, or of a suitable variant, in the presence of nodes joining and leaving the ring.

Our experience shows that TLA + is well-suited for modeling concurrent and distributed algorithms such as Pastry. In particular, the set-theoretic nature of the specification language encourages the user to model the algorithm at a suitably high level of abstraction. Moreover, TLA + 's hierarchical proof language lets a user focus on parts of the proof without having to remember details about unrelated parts of the proof. Like Lu, we rely on a large invariant for proving the main safety property of the protocol "in one shot", rather than proceeding by refinement from a high-level model where nodes join atomically, down to a detailed model of the real protocol. TLA + has a notion of refinement based on trace inclusion, and it would be interesting to develop a refinement-based proof and compare its complexity to that of our proof. The difficulty is that parts of the state, such as contents of leaf sets under construction, become visible when some node completes its join protocol, revealing information about other nodes joining concurrently that would have to be anticipated in a refinement-based development.

On a technical level, TLAPS includes facilities for checking the status of a proof that can identify which steps are affected by a change in the specification or the proof. While TLAPS can manage a proof of the size reported here, it is barely able to do so. For example, the Java heap size allotted to Eclipse has to be increased to several gigabytes, and status checking currently takes almost as much time as rerunning the proof. We are in contact with the TLAPS developers who are investigating solutions to these bottlenecks. Although users of a mechanical theorem prover always dream of better automation, the main difficulty in the formal verification of algorithms is in fact finding sufficiently strong inductive invariants that underpin the correctness argument, and any assistance in this task would be most welcome.

Fig. 1 :

 1 Fig. 1: A Pastry ring of size 16 with three live nodes 0, 7 and 11. The nodes should divide key coverage among them, as indicated by the separators.

Fig. 2 :

 2 Fig. 2: The Pastry Join Protocol

Fig. 3 :

 3 Fig. 3: Initial condition and next-state relation specified in TLA + .

Fig. 4 :

 4 Fig. 4: Structure of the original LuPastry proof versus the rigorous version.

RightNeighbor (ls ) ∆=

 ) ClosestFromTheRight(ls.node, ls.right) ClosestFromTheRight(x , a) ∆ = if a = {} then x else choose y ∈ a : ∀z ∈ a : ClockwiseArc(x , y, z )

Fig. 5 :

 5 Fig. 5: Network Stability

  The neighbors of i are the closest nodes to i in its leaf set ls.

			4
	LeafSet	∆ = { ls ∈ [node : I , left : subset I , right : subset I ] :
	∧ ls.node / ∈ ls.left	∧ Cardinality(ls.left) ≤ L
	∧ ls.node / ∈ ls.right ∧ Cardinality(ls.right) ≤ L }
	RightNeighbor (ls)	∆ =
	if ls.right = {} then ls.node
	else choose n ∈ ls.right : ∀ p ∈ ls.right :
	ClockwiseDistance(ls.node, p) ≥ ClockwiseDistance(ls.node, n)

  Only after k has finished joining and turned Ready can other nodes join the network between k and i . Therefore, any participating node between i and CR(i ) is either ToJoin[i ] or ToJoin[CR(i )]. That is, there can never be three different participating nodes k 1 , k 2 , k 3 such that

	i	k 1	k 2	k 3	CR(i ), or dually, CL(i )	k 1	k 2	k 3

  Theorem 1. In any stable LuPastry + network, correct delivery holds.Proof (Outline). The action DeliverLookup(i , k ) is enabled only if i is a Ready node that thinks it covers key k . Assume for the sake of contradiction that DeliverLookup(i , k ) and DeliverLookup(j , k ) are enabled where j = i . Nodes i and j are Ready, and both think they cover k . W.l.o.g.

	11	14	i	k1
		0		k2
	8
	7	2		j
	(a) This ring is stable if nodes	(b) For L ≥ 3, i's leaf set can
	0, 2, 7, 11 are stable. Node 0 is	always accommodate
	stable if its left leaf set contains	k1 = ToJoin[i], k2 = ToJoin[j ],
	11 and its right leaf set contains 2.	and i's Ready/OK neighbor j .
				, i	k	j ; k is in i 's

  The definition of Init implies that the LuPastry + ring is stable in the initial state: nodes in A are Ready and all other nodes are Dead. The leaf set of each A-node i is composed by adding all other A-nodes to i 's empty leaf set. Consequently, the leaf set of i will contain its closest right and left Aneighbors. All A-nodes are stable, and so the network is stable. Now consider a stable Pastry network N . For the induction step, we need to show that N remains stable after executing any sub-action e of Next. We use N e to refer to the new state of N after the execution of e, and CR e (i ) and CL e (i ) the next values of CR(i ) (resp., CL(i )) for a node i . Note that for a node i that is not Ready or OK, the only action that can change i into a Ready or OK node is ReceiveProbeReply(i ): i receives the last probe reply message it was waiting for, its probing set becomes empty, and i becomes OK. We need to show that (1) if e results in some unstable node i in N to become Ready or OK, then i is stable in N e , and (2) all stable nodes in N remain stable in N e . (1) Let i be an unstable N -node. Since N is stable, i is not Ready or OK. It must be that e = ReceiveProbeReply(i ). Since e can only change the local variables of i , the status of all other nodes remains unchanged; CR e (i ) = CR(i ) and CL e (i ) = CL(i ). By P7 and since i 's probing set is empty, CR(i ) and CL(i ) are in i 's leaf set, hence i is stable in N e . (2) Let i be a stable node in N . If CR e (i ) = CR(i ) and CL e (i ) = CL(i ), then i remains stable in N e by P6. Now suppose CR e (i ) = CR(i ) (the proof is similar for CL e

				we are done. Alternatively, assume |r	k | = |r	k |.
	Because of the ordering of the nodes on the ring r	i	k , we have that
	|r	k | = |r	i | + |i	k |. Since path lengths are non-negative, (i	k ) ≤
	(r	k ).

Theorem 2. For L ≥ 3, the network is always stable. Proof (Outline).

Nodes also maintain routing tables for the purpose of efficient message routing, but these are irrelevant to our discussion.

For compactness, we omit parts of the specification irrelevant to the discussion. TLA + functions and operators have been given new names for better readability.

Both examples can be found in our proof files in module ProofCorrectness.

Currently, TLAPS requires that enabled be unfolded manually in the machinechecked proof.