Dimitrios Kouzapas

Nobuko Yoshida

Kohei Honda

On Asynchronous Session Semantics

This paper studies a behavioural theory of the π-calculus with session types under the fundamental principles of the practice of distributed computing -asynchronous communication which is order-preserving inside each connection (session), augmented with asynchronous inspection of events (message arrivals). A new theory of bisimulations is introduced, distinct from either standard asynchronous or synchronous bisimilarity, accurately capturing the semantic nature of session-based asynchronously communicating processes augmented with event primitives. The bisimilarity coincides with the reduction-closed barbed congruence. We examine its properties and compare them with existing semantics. Using the behavioural theory, we verify that the program transformation of multithreaded into event-driven session based processes, using Lauer-Needham duality, is type and semantic preserving.

Introduction

Modern transports such as TCP in distributed networks provide reliable, ordered delivery of messages from a program on one computer to another, once a connection is established. In practical communications programming, two parties start a conversation by establishing a connection over such a transport and exchange semantically meaningful, formatted messages through this connection. The distinction between possibly non order-preserving communications outside of connection and order-preserving ones inside each connection is a key feature of this practice: order preservation allows proper handling of a sequence of messages following an agreed-upon conversation structure, while unordered deliveries across connections enhance asynchronous, efficient bandwidth usage. Further, asynchronous event processing [START_REF] Inc | New IO APIs[END_REF] using locally buffered messages enables the receiver to asynchronously inspect and consume events/messages. This paper investigates semantic foundations of asynchronously communicating processes, capturing these key elements of modern communications programmingdistinction between non order-preserving communications outside connections and the order-preserving ones inside each connection, as well as the incorporation of asynchronous inspection of message arrivals. We use the π-calculus augmented with session primitives, buffers and a simple event inspection primitive. Typed sessions capture structured conversations in connections with type safety; while a buffer represents an intermediary between a process and its environment, capturing non-blocking nature of communications, and enabling asynchronous event processing. The formalism is intended to be an idealised but expressive core communications programming language, offering a basis for a tractable semantic study. Our study shows that the combination of these basic elements for modern communications programming leads to a rich behavioural theory which differs from both the standard synchronous communications semantics and the fully asynchronous one [START_REF] Honda | An object calculus for asynchronous communication[END_REF], captured through novel equational laws for asynchrony. These laws can then be used as a semantic justification of a well-known program transformation based on Lauer and Needham's duality principle [START_REF] Lauer | On the duality of operating system structures[END_REF], which translates multithreaded programs to their equivalent single-threaded, asynchronous, event-based programs. This transformation is regularly used in practice, albeit in an ad-hoc manner, playing a key role in e.g. high-performance servers. Our translation is given formally, is type-preserving and is backed up by a rigorous semantic justification. While we do not detail in the main sections, the transform is implemented in the session-extension of Java [START_REF] Hu | Type-safe eventful sessions in Java[END_REF][START_REF] Hu | Session-Based Distributed Programming in Java[END_REF], resulting in competitive performance in comparison with more ad-hoc transformations.

Let us outline some of the key technical ideas of the present work informally. In the present theory, the asynchronous order-preserving communications over a connection are modelled as asynchronous session communication, extending the synchronous session calculus [START_REF] Honda | Language primitives and type disciplines for structured communication-based programming[END_REF][START_REF] Takeuchi | An Interaction-based Language and its Typing System[END_REF] with message queues [START_REF] Coppo | Asynchronous Session Types and Progress for Object-Oriented Languages[END_REF][START_REF] Gay | Linear type theory for asynchronous session types[END_REF][START_REF] Honda | Multiparty Asynchronous Session Types[END_REF]. A message queue, written s [i: h, o: h ], encapsulates input buffer (i) with elements h and output buffer (o) with h . Figure below represents the two end points of a session. A message v is first enqueued by a sender s! v ; P at its output queue at s, which intuitively represents a communication pipe extending from the sender's locality to the receiver's. The message will eventually reach the receiver's locality, formalised as its transfer from the sender's output buffer (at s) to the receiver's input buffer (at s). For a receiver, only when this transfer takes place, a visible (and asynchronous) message reception takes place, since only then the receiver can inspect and consume the message (as shown in Remote below).Note that dequeuing and enqueing actions inside a location are local to each process and is therefore invisible (τ-actions) (Local below).

Local (the dashed arrows)

s! v ; Q | s [o : h] τ -→ Q | s [o : h•v] s?(x).P | s [i : w• h] τ -→ P{w/ x } | s [i : h] Remote (the solid arrows) s [i : h] s? v -→ s [i : h•v] s [o : v• h] s! v -→ s [o : h]
The induced semantics captures the nature of asynchronous observables not studied before. For example, in weak asynchronous bisimilarity in the asynchronous π-calculus (≈ a in [START_REF] Honda | An object calculus for asynchronous communication[END_REF][START_REF] Honda | On reduction-based process semantics[END_REF]), the message order is not observable

(s! v 1 | s! v 2 ≈ a s! v 2 | s! v 1 )
but in our semantics, messages for the same destination do not commute (s! v 1 ; s! v 2 ≈ s! v 2 ; s! v 1 ) as in the synchronous semantics [START_REF] Milner | A Calculus of Mobile Processes[END_REF] (≈ s in [START_REF] Honda | An object calculus for asynchronous communication[END_REF][START_REF] Honda | On reduction-based process semantics[END_REF]); whereas two inputs for different targets commute (s 1 ?(x); s 2 ?(y); P ≈ s 2 ?(x); s 1 ?(y); P) since the dequeue action is not observable, differing from the synchronous semantics, s 1 ?(x); s 2 ?(y); P ≈ s s 2 ?(x); s 1 ?(y); P.

Asynchronous event-handling [START_REF] Hu | Type-safe eventful sessions in Java[END_REF] introduces further subtleties in observational laws. Asynchronous event-based programming is characterised by reactive flows driven by the detection of events, that is message arrivals at local buffers. In our formalism, this facility is distilled as an arrived predicate: e.g., Q = if arrived s then P 1 else P 2 reduces to P 1 if the s input buffer contains one or more message; otherwise Q reduces to P 2 . By arrived, we can observe the movement of messages between two locations.

For example, Q | s[i : / 0] | s[o : v] is not equivalent with Q | s[i : v] | s[o : / 0]
because the former can reduce to P 2 (since v has not arrived at the local buffer at s yet) while the latter cannot.

Online appendix [23] lists the full definition of Lauer-Needham transformation, the detailed definitions, full proofs and the benchmark results in Session-based Java which demonstrate the potential of the session-type based translation as semantically transparent optimisation techniques.

Asynchronous Network Communications in Sessions 2.1 Syntax and Operational Semantics

We use a sub-calculus of the eventful session π-calculus [START_REF] Hu | Type-safe eventful sessions in Java[END_REF], defined below.

P i } i∈I | if e then P else Q | (ν a) P | P | Q | 0 | µX.P | X | a [ s] | a s | (ν s) P | s [i : h, o : h ] (Message) h ::= v | l
Values v, v , ... include constants (tt, ff), shared channels a, b, c and session channels s, s . A session channel denotes one endpoint of a session: s and s denote two ends of a single session, with s = s. Labels for branching and selection range over l, l , ..., variables over x, y, z, and process variables over X,Y, Z. Shared channel identifiers u, u denote shared channels/variables; session identifiers k, k are session endpoints and variables. n denotes either a or s. Expressions e are values, variables and the message arrival predicates (arrived u, arrived k and arrived k h: the last one checks for the arrival of the specific message h at k). s and h stand for vectors of session channels and messages respectively. ε denotes the empty vector. We distinguish two kinds of asynchronous communications, asynchronous session initiation and asynchronous session communication (over an established session). The former involves the unordered delivery of a session request message a s , where a s represents an asynchronous message in transit towards an acceptor at a, carrying a fresh session channel s. As in actual network, a request message will first move through the network and eventually get buffered at a receiver's end. Only then a message arrival can be detected. This aspect is formalised by the introduction of a shared channel input queue a [ s], often called shared input queue for brevity, which denotes an acceptor's local buffer at a with pending session requests for s. The intuitive meaning of the endpoint configuration s [i : h, o : h ] is explained in Introduction.

Requester u(x); P requests a session initiation, while acceptor u(x).P accepts one. Through an established session, output k! e ; P sends e through channel k asynchronously, input k?(x).P receives through k, selection k l; P chooses the branch with label l, and branching k {l i : P i } i∈I offers branches. The (ν a) P binds a channel a, while (ν s) P binds the two endpoints, s and s, making them private within P. The conditional, parallel composition, recursions and inaction are standard. 0 is often omitted. For brevity, one or more components may be omitted from a configuration when they are irrelevant, writing e.g. s [i : h] which denotes the input part of s [i : h, o : h ]. The notions of free variables and channels are standard [START_REF] Mostrous | Session-based communication optimisation for higher-order mobile processes[END_REF]; fn(P) denotes the set of free channels in P. a s , (ν s) P and s [i : h, o : h ] only appear at runtime. A process without free variables is called closed and a closed process without runtime syntax is called program.

[Request1] [Request2] [Accept] [Send,Recv] [Sel,Bra] [Comm] [Areq] [Ases] [Amsg] a(x); P -→ (ν s) (P{s/ x } | s [i : ε, o : ε] | a s ) (s / ∈ fn(P)) a [ s] | a s -→ a [ s•s] a(x).P | a [s• s] -→ P{s/ x } | s [i : ε, o : ε] | a [ s] s! v ; P | s [o : h] -→ P | s [o : h•v] s?(x).P | s [i : v• h] -→ P{v/ x } | s [i : h] s l i ; P | s [o : h] -→ P | s [o : h•l i ] s {l j : P j } j∈J | s [i : l i • h] -→ P i | s [i : h] (i ∈ J) s [o : v• h] | s [i : h ] -→ s [o : h] | s [i : h •v] E[arrived a] | a [ s] -→ E[b] | a [ s] (| s| ≥ 1) b E[arrived s] | s [i : h] -→ E[b] | s [i : h] (| h| ≥ 1) b E[arrived s h] | s [i : h] -→ E[b] | s [i : h] ( h = h• h ) b
The above table defines the reduction relation over closed terms. The key rules are given in Figure above. We use the standard evaluation contexts E[ ] defined as E ::= -| s! E ; P | if E then P else Q. The structural congruence ≡ and the rest of the reduction rules are standard. We set → → = (-→ ∪ ≡) * .

The first three rules define the initialisation. In [Request1], a client requests a server for a fresh session via shared channel a. A fresh session channel, with two ends s (server-side) and s (client-side) as well as the empty configuration at the client side, are generated and the session request message a s is dispatched. Rule [Request2] enqueues the request in the shared input queue at a. A server accepts a session request from the queue using [Accept], instantiating its variable with s in the request message; the new session is now established. Asynchronous order-preserving session communications are modelled by the next four rules. Rule [Send] enqueues a value in the o-buffer at the local configuration; rule [Receive] dequeues the first value from the i-buffer at the local configuration; rules [Sel] and [Bra] similarly enqueue and dequeue a label. The arrival of a message at a remote site is embodied by [Comm], which removes the first message from the o-buffer of the sender configuration and enqueues it in the i-buffer at the receiving configuration.

Output actions are always non-blocking. An input action can block if no message is available at the corresponding local input buffer. The use of the message arrivals can avoid this blocking: [Areq] evaluates arrived a to tt iff the queue is non-empty (e b means e evaluates to the boolean b); similarly for arrived k in [Areq]. [Amsg] evaluates arrived s h to tt iff the buffer is nonempty and its next message matches h.

Types and Typing

The type syntax follows the standard session types from [START_REF] Honda | Language primitives and type disciplines for structured communication-based programming[END_REF].

(Shared) U ::= bool | i S | o S | X | µ X.U (Value) T ::= U | S (Session) S ::= !(T ); S | ?(T ); S | ⊕{l i : S i } i∈I | &{l i : S i } i∈I | µ X.S | X | end
The shared types U include booleans bool (and, in examples, naturals nat); shared channel types i S (input) and o S (output) for shared channels through which a session of type S is established; type variables (X, Y, Z, ..); and recursive types. The IO-types (often called server/client types) ensure a unique server and many clients [START_REF] Honda | A uniform type structure for secure information flow[END_REF]. In the present work they are used for controlling locality (queues are placed only at the server sides) and associated typed transitions, playing a central role in our behavioural theory. In session types, output type !(T ); S represents outputting values of type T , then performing as S. Dually for input type ?(T ); S. Selection type ⊕{l i : S i } i∈I describes a selection of one of the labels say l i then behaves as T i . Branching type &{l i : S i } i∈I waits with I options, and behaves as type T i if i-th label is chosen. End type end represents the session completion and is often omitted. In recursive type µ X.S, type variables are guarded in the standard sense.

The judgements of processes and expressions are Γ P ∆ and Γ , ∆ e : T , with

Γ ::= / 0 | Γ •u:U | Γ •X :∆ and ∆ ::= / 0 | ∆ •a | ∆ •k :T | ∆ •s where session type is extended to T ::= M; S | M with M ::= / 0 | ⊕ l | &l | !(T ) | ?(T ) | M;
M which represents types for values stored in queues (note / 0; S = S). Γ is called shared environment, which maps shared channels and process variables to, respectively, constant types and value types; ∆ is called linear environment maps session channels to session types and recording shared channels for acceptor's input queues and session channels for end-point queues. The judgement is read: program P is typed under shared environment Γ , uses channels as linear environment ∆ . In the expression judgement, expression e has type T under Γ , and uses channels as linear environment ∆ . We often omit ∆ if it is clear from the context. The typing system is similar with [START_REF] Bettini | Global progress in dynamically interleaved multiparty sessions[END_REF][START_REF] Hu | Type-safe eventful sessions in Java[END_REF], and can be found in online Appendix [23]. We say that ∆ well configured if s : S ∈ ∆ , then s : S ∈ ∆ . We define: {s :!(T ); S • s : ?(T ); S } -→ {s : S • s : S }, {s :

⊕{l i : S i } i∈I • s : &{l i : S i } i∈I } -→ {s : S k • s : S k } (k ∈ I), and ∆ ∪ ∆ -→ ∆ ∪ ∆ if ∆ -→ ∆ . 1
Proposition 2.1 (Subject Reduction). if Γ P ∆ and P → → Q and ∆ is well-configured, then we have Γ Q ∆ such that ∆ -→ * ∆ and ∆ is well-configured.

Asynchronous Session Bisimulations and its Properties

Labelled Transitions and Bisimilarity

Untyped and Typed LTS. This section studies the basic properties of behavioural equivalences. We use the following labels ( , , ...):

::= a s | a s | a(s) | s? v | s! v | s!(a) | s&l | s ⊕ l | τ
where the labels denote the session accept, request, bound request, input, output, bound output, branching, selection and the τ-action. sbj( ) denotes the set of free subjects in ; and fn( ) (resp. bn( )) denotes the set of free (resp. bound) names in . The symmetric operator on labels that denotes that is a dual of , is defined as: a s a s , a s a(s), s? v s! v , s? a s!(a), and s&l s ⊕ l.

Acc a[ s] a s -→ a[ s•s] Req a s a s -→ 0 In s [i : h] s? v -→ s [i : h•v] Out s [o : v• h] s! v -→ s [o : h] Bra s [i : h] s&l -→ s [i : h•l] Sel s [o : l• h] s⊕l -→ s [o : h] Local P -→ Q P τ -→ Q Par P -→ P bn( ) ∩ fn(Q) = / 0 P|Q -→ P |Q Tau P -→ P Q -→ Q P|Q τ -→ (ν bn( , ))(P |Q ) Res P -→ P n ∈ fn( ) (ν n)P -→ (ν n)P OpS P a s -→ P (ν s)P a(s) -→ P OpN P s! a -→ P (ν a)P s!(a)
-→ P

Alpha P ≡ α P P -→ Q P -→ Q
Rule Local is defined from the reductions by [Request1, Accept, Send, Recv, Bra, Sel, Areq, Ases, Amsg] as well as [Comm] when the communication object is a session (delegation).

In the untyped labelled transition system (LTS) defined above, Acc / Req are for the session initialisation. The next four rules In / Out / Bra / Sel say the action is observable when it moves from its local queue to its remote queue. When the process accesses its local queue, the action is invisible from the outside, as formalised by Local . In contrast, Com expresses an interaction between two local configutations. This distinction is useful in our later proofs. Other compositional rules are standard. Based on the LTS, we use the standard notations [START_REF] Milner | Communication and Concurrency[END_REF] such as P =⇒ Q, P =⇒ Q and P ˆ =⇒ Q. We define the typed LTS on the basis of the untyped one, using the type information to control the enabling of actions. This is realised by introducing the environment transition, defined below. A transition (Γ , ∆ ) -→ (Γ , ∆ ) means that an environment (Γ , ∆ ) allows an action to take place, and the resulting environment is (Γ , ∆ ), constraining process transitions through the linear and shared environments. This constraint is at the heart of our typed LTS, accurately capturing interactions in the presence of sessions and local buffers. We write

Γ 1 P 1 ∆ 1 -→ Γ 2 P 2 ∆ 2 if P 1 -→ P 2 and (Γ 1 , ∆ 1 ) -→ (Γ 2 , ∆ 2 )
with Γ i P i ∆ i . Similarly for other transition relations.

Γ (a) = i S , a ∈ ∆ , s fresh ⇒ (Γ , ∆ ) a s -→ (Γ , ∆ • s : S) Γ (a) = o S , a ∈ ∆ ⇒ (Γ , ∆ ) a s -→ (Γ , ∆ ) Γ (a) = o S , a ∈ ∆ , s fresh ⇒ (Γ , ∆ ) a(s) -→ (Γ , ∆ • s : S) Γ v :U and U = i S and s / ∈ dom(∆ ) ⇒ (Γ , ∆ • s :!(U); S) s! v -→ (Γ , ∆ • s : S) s / ∈ dom(∆ ) ⇒ (Γ , ∆ • s :!(o S ); S) s!(a) -→ (Γ • a : o S , ∆ • s : S) Γ v :U and U = i S and s / ∈ dom(∆ ) ⇒ (Γ , ∆ • s :?(U); S) s? v -→ (Γ , ∆ • s : S) s / ∈ dom(∆ ) ⇒ (Γ , ∆ • s : ⊕ {l i : S i } i∈I ) s⊕l k -→ (Γ , ∆ • s : S k ) s / ∈ dom(∆ ) ⇒ (Γ , ∆ • s : & {l i : S i } i∈I ) s&l k -→ (Γ , ∆ • s : S k ) ∆ -→ ∆ ⇒ (Γ , ∆ ) τ -→ (Γ , ∆ )
The first rule says that reception of a message via a is possible only when a is inputtyped (i-mode) and its queue is present (a ∈ ∆ ). The second is dual, saying that an output at a is possible only when a has o-mode and no queue exists. Similarly for a bound output action. The two session output rules ( = s! v and s!(a)) are the standard value output and a scope opening rule. The next is for value input. Label input and output are defined similarly. Note that we send and receive only a shared channel which has o-mode. This is because a new accept should not be created without its queue in the same location. The final rule ( = τ) follows the reduction rules defined before Proposition 2.1. The LTS omits delegations since it is not necessary in the bisimulation we consider (due to the notion of localisation, see the next paragraph). Write for the symmetric and transitive closure of -→ over linear environments. We say a relation on typed processes is a typed relation if, whenever it relates two typed processes, we have Γ P 1 ∆ 1 and Γ P 2 ∆ 2 such that ∆ 1 ∆ 2 . We write

Γ P 1 ∆ 1 RP 2 ∆ 2 if (Γ P 1 ∆ 1 ,Γ P 2 ∆ 2 )
are in a typed relation R. Further we often leave the environments implicit, writing simply P 1 RP 2 . Localisation and Bisimulation. Our bisimulation is a typed relation over those processes which are localised, in the sense that they are equipped with all necessary local queues. We say an environment ∆ is delegation-free if it contains types which are generated by deleting S from value type T in the syntax of types defined in § 2.2 (i.e. either !(S); S or ?(S); S does not appear in ∆ ). Similarly for Γ . Now let P be closed and Γ P ∆ where Γ and ∆ are delegation-free (note that P can perform delegations at hidden channels by Local ). Then we say P is localised w.r.t. Γ , ∆ if (1) For each s : S ∈ dom(∆ ), s ∈ ∆ ; and (2) if Γ (a) = i S , then a ∈ ∆ . We say P is localised if it is so for a suitable pair of environments. For example, s?(x); s! x + 1 ; 0 is not localised, but s?(x); s! x+1

; 0 | s [i: h 1 , o: h 2 ] is. Similarly, a(x).P is not localised, but a(x).P | a [ s] is.
By composing buffers at appropriate channels, any typable closed process can become localised. If P is localised w.r.t. (Γ , ∆ ) then Γ P ∆ l -→ Γ P ∆ implies P is localised w.r.t. (Γ , ∆ ) (in the case of τ-transition, note queues always stay). We can now introduce the reduction congruence and the asynchronous bisimilarity. 1. P 1 ⇓ n iff P 2 ⇓ n. 2. Whenever Γ P 1 ∆ 1 RP 2 ∆ 2 holds, P 1 → → P 1 implies P 2 → → P 2 such that Γ P 1 ∆ 1 RP 2 ∆ 2 holds with ∆ 1 ∆ 2 and the symmetric case.

The maximum reduction congruence which is not a universal relation exists [START_REF] Honda | On reduction-based process semantics[END_REF] which we call reduction congruency, denoted by ∼ =.

Definition 3.2 (Asynchronous Session Bisimulation).

A typed relation R over localised processes is a weak asynchronous session bisimulation or often a bisimulation for brevity, if, whenever Γ P 1 ∆ 1 RP 2 ∆ 2 , the following two conditions holds:

(1)

Γ P 1 ∆ 1 -→ Γ P 1 ∆ 1 implies Γ P 2 ∆ 2 ˆ =⇒ Γ P 2 ∆ 2 such that Γ P 1 ∆ 1 RP 2 ∆ 2 with ∆ 1 ∆ 2 holds
and (2) the symmetric case of (1). The maximum bisimulation exists which we call bisimilarity, denoted by ≈. We sometimes leave environments implicit, writing e.g. P ≈ Q.

We extend ≈ to possibly non-localised closed terms by relating them when their minimal localisations are related by ≈ (given Γ P ∆ , its minimal localisation adds empty queues to P for the input shared channels in Γ and session channels in ∆ that are missing their queues). Further ≈ is extended to open terms in the standard way [START_REF] Honda | On reduction-based process semantics[END_REF].

Properties of Asynchronous Session Bisimilarity

Characterisation of Reduction Congruence. This subsection studies central properties of asynchronous session semantics. We first show that the bisimilarity coincides with the naturally defined reduction-closed congruence [START_REF] Honda | On reduction-based process semantics[END_REF], given below. The soundness (≈⊂ ∼ =) is by showing ≈ is congruent. The most difficult case is a closure under parallel composition, which requires to check the side condition ∆ 1 ∆ 2 for each case. The completeness ( ∼ =⊂≈) follows [7, § 2.6] where we prove that every external action is definable by a testing process, see [23]. Asynchrony and Session Determinacy. Let us call an output action if is one of a s , a(s), s! v , s!(a), s ⊕ l; and an input action if is one of a s , s? v , s&l. In the following, the first property says that we can delay an output arbitrarily, while the second says that we can always immediately perform a (well-typed) input. The asynchronous interaction on the session buffers enables inputs to happen before multi-internal steps and outputs to happen after multi-internal steps.

Following [START_REF] Philippou | On confluence in the pi-calculus[END_REF], we define determinacy and confluence. Below and henceforth we often omit the environments in typed transitions.

Definition 3.5 (Determinacy). We say

Γ Q ∆ is derivative of Γ P ∆ if there exists such that Γ P ∆ =⇒ Γ Q ∆ . We say Γ P ∆ is determinate if for each derivative Q of P and action , if Q -→ Q and Q ˆ =⇒ Q then Q ≈ Q .
We then extend the above notions to session communications.

Definition 3.6 (Session Determinacy). Let us write

P -→ s Q if P -→ Q where if = τ then it is generated without using [Request1], [Request2], [Accept],
[Areq] nor [Amsg] from reduction rules (i.e. a communication is performed without arrival predicates or accept actions). We extend the definition to =⇒ s and ˆ =⇒ s etc. We say P is session determinate

if P is typable, is localised and if Γ P ∆ =⇒ Q ∆ then Γ P ∆ =⇒ s Q ∆ . We call such Q a session derivative of P.
We define 1 2 ("residual of 1 after 2 ") as (1) a s if 1 = a(s ) and s ∈ bn( 2 ); (2) s! s if 1 = s!(s ) and s ∈ bn( 2 ); (3) s! a if 1 = s!(a) and a ∈ bn( 2 ); and otherwise Definition 3.7 (Confluence). Γ P ∆ is confluent if for each derivative Q of P and

1 , 2 such that 1 2 , (i) if Q -→ Q 1 and Q =⇒ Q 2 , then Q 1 =⇒ Q 1 and Q 2 =⇒ Q 2 ≈ Q 1 ; and (ii) if Q 1 -→ Q 1 and Q 2 =⇒ Q 2 , then Q 1 2 1 =⇒ Q 1 and Q 2 1 2 =⇒ Q 2 ≈ Q 1 .
Lemma 3.8. Let P be session determinate and Γ P =⇒ Q ∆ . Then P ≈ Q.

Theorem 3.9 (Session Determinacy). Let P be session determinate. Then P is determinate and confluent.

The following relation is used to prove the event-based optimisation. The proof of the following lemma is by showing =⇒ R ⇐= with =⇒ determinate is a bisimulation.

Definition 3.10 (Determinate Upto-expansion Relation). Let R be a symmetric, typed

relation such that if Γ P ∆ R Q ∆ and (1) P, Q are determinate; (2) If Γ P ∆ l -→ Γ P ∆ then Γ Q ∆ l =⇒ Γ Q ∆ and Γ P ∆ =⇒ Γ P ∆ with Γ P ∆ R Q ∆ ;

Lauer-Needham Transform

In an early work [START_REF] Lauer | On the duality of operating system structures[END_REF], Lauer and Needham observed that a concurrent program may be written equivalently either in a thread-based programming style (with shared memory primitives) or in an event-based style (with a single-threaded event loop processing messages sequentially with non-blocking handlers). Following this framework and using high-level asynchronous event primitives such as selectors [START_REF] Inc | New IO APIs[END_REF] for the event-based style, many studies compare these two programming styles, often focusing on performance of server architectures (see [13, § 6] for recent studies on event programming). These implementations implicitly or explicitly assume a transformation from a program written in the thread-based style, especially those which generate a new thread for each service request (as in thread-based web servers), to its equivalent event-based program, which treats concurrent services using a single threaded event-loop (as in event-based web servers). However the precise semantic effects of such a transformation nor the exact meaning of the associated "equivalence" has not been clarified.

We study the semantic effects of such a transformation using the asynchronous session bisimulation. We first specify both event and thread based programming models and introduce a formal mapping from a thread-based process to their event-based one, following [START_REF] Lauer | On the duality of operating system structures[END_REF]. As a threaded system we assume a server process whose code creates fresh threads at each service invocation. The key idea is to decompose this whole code into distinct smaller code segments, each handling the part of the original code starting from a blocking action. Such a blocking action is represented as reception of a message (input or branching). Then a single global event-loop can treat each message arrival by processing the corresponding code segment combined with an environment, returning to inspect the content of event/message buffers. We first stipulate a class of processes which we consider for our translation. Below * a(x); P denotes an input replication abbreviating µX.a(x).(P|X).

Definition 4.1 (Server).

A simple server at a is a closed process * a(x). P with a typing of form a : i S , b 1 : o S 1 , .., b n : o S n where P is sequential (i.e. contains no parallel composition | ) and is determinate and under any localisation. A simple server is often considered with its localisation with an empty queue a[ε].

A server spawns an unbounded number of threads as it receives session requests repeatedly. Each thread may initiate other sessions with outside, and its interactions may involve delegations and name passing. Definition 4.1 assumes two conditions: (1) determinacy and (2) sequential processing of each event. A practical example of (1) is a web server which only serves static web pages. As will be discussed later, determinacy plays an essential role in our proofs while sequentiality is for simplicity of the mapping. Given a server * a(w : S); P | a[ε], its translation, which we call Lauer-Needham transform or LN-transform for short, is written LN [[ * a(w : S); P | a[ε]]](the full mapping is non-trivial and given in [23]). The key elements of LN [[ * a(w : S); P]] follow:

1. A selector handles events on message arrival. Its function includes a selector queue q ε that stores sessions whose arrival is continuously inspected. Its initial element is a, c 0 . This data says: "if a message comes at a, jump to the code block (CPS procedure) whose subject is c 0 ". 2. A collection of code blocks CodeBlocks a, o, q, c , CPS procedures handling incoming messages. A code block originates from a threaded server blocking subterm, i.e. a subterm starting from an input or a branching. 3. Loop o, q implements the event-loop. It passes execution from the selector to a code block in CPS style, after a successful arrive inspection from the selector.

We use the standard "select" primitive represented as a process, called selector [START_REF] Hu | Type-safe eventful sessions in Java[END_REF]. It stores a collection of session channels, with each channel associated with an environment, binding variables to values. It then picks up one of them at which a message arrives, receives that message via that channel and has it be processed by the corresponding code block. Finally it stores the session and the associated environment back in the collection, and moves to the next iteration. Since a selector should handle channels of different types, it uses the typecase construct from [START_REF] Hu | Type-safe eventful sessions in Java[END_REF]. typecase k of {(x i :T i ) P i } i∈I takes a session endpoint k and a list of cases (x i :T i ), each binding the free variable x i of type pattern T i in P i . Its reduction is defined as:

typecase s of {(x i : T i ) P i } i∈I | s [S, i : h, o : h ] -→ P j {s/ x j } | s [S, i : h, o : h ]
where j ∈ I such that (∀i < j.T i ≤ S ∧T j ≤ S) where ≤ denotes a subtyping relation. The typecase construct finds a match of the session type of the tested channel among the session types in its list, and proceeds with the corresponding process. For the matching to take place, session endpoint configuration syntax is extended with the runtime session typing [START_REF] Hu | Type-safe eventful sessions in Java[END_REF]. The selectors are defined by the following reduction relations:

new selector r in P -→ (ν r)(P | sel r, ε ) register s , r ; P | sel r, s -→ P | sel r, s • s let x = select(r) in typecase x of {(x i : T i ) : P i } i∈I | sel r, s • s | s [S, i : h] -→ P i {s / x i } | sel r, s | s [S, i : h] ( h = ε) let x = select(r) in typecase x of {(x i : T i ) : P i } i∈I | sel r, s • s | s [i : ε] -→ let x = select(r) in typecase x of {(x i : T i ) : P i } i∈I | sel r, s • s | s [i : ε]
where in the third line S and T i satisfy the condition for typecase in the reduction rule.

The last two rules integrate reductions for typecase to highlight their combined usage (which is in effect the only way the selection is meaningfully performed). Operator new selector r in P (binding r in P) creates a new selector sel r, ε , named r and with the empty queue ε. Operator register s , r ; P registers a session channel s to r, adding s to the original queue s. The next let retrieves a registered session and checks the availability to test if an event has been triggered. If so, find the match of the type of s among {T i } and select P i ; if not, the next session is tested. As proved in [START_REF] Hu | Type-safe eventful sessions in Java[END_REF], these primitives are encodable in the original calculus augmented with typecase. The bisimulations and their properties (such as congruency of ≈) remain unchanged.

Example 4.1 (Lauer-Needham Transform). As an example of a server, consider:

P = * a(x); x?(y).x! y + 1 ; x?(z).x! y + z ; 0 | a[ε]
This process has the session type ?(nat); !(nat)?(nat); !(nat) at a, and can be read: a process should first expect to receive (?) a message of type nat and send (!) it, then to receive (? again) a nat, and finish by sending (!) a result. We extract the blocking subterms from this process as follows.

Blocking Process Type at Blocking Prefix a(x). x?(y).x! y + 1 x?(z).x! y + z ; 0 i ?(nat); !(nat); ?(nat); !(nat) x?(y).x! y + 1 x?(z).x! y + z ; 0 ?(nat); !(nat); ?(nat); !(nat) x?(z).x! y + z ; 0 ?(nat); !(nat)

These blocking processes are translated into code blocks (CodeBlocks) given as: * c 0 (y); a(x). update(y, x, x); register sel, x, y, c which processes each message, using environments to record threads' states. The operation update(y, x, x); updates an environment, while register stores the blocking session channel, the associated continuation c i and the current environment y in the selector queue sel. Finally, using these code blocks, the main event-loop denoted Loop, is given as:

Loop = * o.let (x, y, z) = select from
, i : ε, o : ε] means [s 1 , i : ε, o : ε] | [s 2 , i : ε, o : ε]).
Non-Blocking Input Non-Blocking Output (1) s 1 ?(x); s 2 ?(y); P ≈ a s 2 ?(y); s 1 ?(x); P s 1 v | s 2 w | P ≈ a s 1 w | s 2 v | P (2) s 1 ?(x); s 2 ?(y); P ≈ s s 2 ?(y); s 1 ?(x); P s 1 ! v ; s 2 ! w ; P ≈ s s 2 ! w ; s 1 ! v ; P (3) s 1 ?(x); s 2 ?(y);

P | s 1 [ε] | s 2 [ε] ≈ 2 s 1 ! v ; s 2 ! w ; P | s 1 [ε] | s 2 [ε] ≈ 2 s 2 ?(y); s 1 ?(x); P | s 1 [ε] | s 2 [ε] s 2 ! w ; s 1 ! v ; P | s 1 [ε] | s 2 [ε] (4) s 1 ?(x); s 2 ?(y); P | Π 1,2 [s i , i : ε, o : ε] ≈ s 1 ! v ; s 2 ! w ; P | Π 1,2 [s i , i : ε, o : ε] ≈ s 2 ?(y); s 1 ?(x); P | Π 1,2 [s i , i : ε, o : ε] s 2 ! w ; s 1 ! v ; P | Π 1,2 [s i , i : ε, o : ε] Input Order-
P | s [ε] s! v ; s! w ; P | s [ε] ≈ 2 s! w ; s! v ; P | s [ε] (4) s?(x); s?(y); P | Π 1,2 [s i , i : ε, o : ε] ≈ s! v ; s! w ; P | Π 1,2 [s i , i : ε, o : ε] ≈ s?(x); s?(y); P | Π 1,2 [s i , i : ε, o : ε] s! w ; s! v ; P | Π 1,2 [s i , i : ε, o : ε] Lemma 3.4 (1) Lemma 3.4 (2) (1) yes yes (2) (ν s)(s! v ; s ?(x); 0 | s?(x); 0) (ν s)(s! v ; s ! v ; 0 | s ?(x); 0) (3) yes s! v ; s ?(x); 0 | s [v ] (4) yes yes
Another technical interest is the effects of the arrived predicate on these combinations. We define the synchronous and asynchronous π-calculi augmented with the arrived predicate and local buffers. For the asynchronous π-calculus, we add a[ h] and arrived a in the syntax, and define the following rules for input and outputs.

a v a v -→ 0 a[ h] a h -→ a[ h • h] if arrived a then P else Q|a[ε] τ -→ Q | a[ε] a?(x). P | a[ h 1 • h i • h 2 ] -→ P{h i /x} | a[ h 1 • h 2 ] if arrived a then P else Q|a[ h] τ -→ P | a[ h]
where, in the last rule, | h| ≥ 1. The above definition precludes the order preservation as the property of transport, but still keeps the non-blocking property as in the asynchronous π-calculus. The synchronous version is similarly defined by setting the buffer size to be one. The non-local version is defined just by adding arrived predicate. Let Q = if e then P 1 else P 2 with P 1 ≈ P 2 . If the syntax does not include arrival predicates, we have

Q | s[i : / 0] | s[o : v] ≈ Q | s[i : v] | s[o : / 0]. In the presence of the arrival predicate, we have Q | s[i : / 0] | s[o : v] ≈ Q | s[i : v] | s[o : / 0
] with e = arrived s. Interestingly in all of the calculi (1-4), the same example as the above, which separate semantics with/without the arrived, are effective.

The IO queues provide non-blocking inputs and outputs, while preserving the input/output ordering, which distinguishes the present framework from other known semantics. As a whole, we observe that the present semantic framework is closer to the asynchronous bisimulation (1) ≈ a , augmented with order-preserving nature per session. Its key properties arise from local, buffered session semantics and typing. We have also seen the semantic significance of the arrived predicates, which enables processes to observe the effects of fine-grained synchronisations.

Related Work. Some of the key proof methods of our work draw their ideas from [START_REF] Philippou | On confluence in the pi-calculus[END_REF], which study an extension of the confluence theory on the π-calculus. Our work differs in that we investigate the effect of asynchronous IO queues and its relationship to confluence. The work [START_REF] Beauxis | On the asynchronous nature of the asynchronous pi-calculus[END_REF] examines expressiveness of various messaging mediums by adding message bags (no ordering), stacks (LIFO policy) and message queues (FIFO policy) in the asynchronous π-calculus [START_REF] Honda | An object calculus for asynchronous communication[END_REF]. They show that the calculus with the message bags is encodable into the asynchronous π-calculus, but it is impossible to encode the message queues and stacks. Neither the effects of locality, queues, typed transitions, and event-based programming are studied.

Programming constructs that can test the presence of actions or events are studied in the context of the Linda language [START_REF] Busi | Comparing three semantics for Linda-like languages[END_REF] and CSP [START_REF] Lowe | Extending csp with tests for availability[END_REF][START_REF] Lowe | Models for csp with availability information[END_REF]. The work [START_REF] Busi | Comparing three semantics for Linda-like languages[END_REF] measures expressive powers between three variants of asynchronous Linda-like calculi, with a construct for inspecting the output in the tuple space, which is reminiscent of the inp predicate of Linda. The first calculus (called instantaneous) corresponds to (1) [START_REF] Honda | An object calculus for asynchronous communication[END_REF], the second one (called ordered) formalises emissions of messages to the tuple spaces, and the third one (called unordered) models unordered outputs in the tuple space by decomposing one messaging into two stages -emission from an output process and rendering from the tuple space. It shows that the instantaneous and ordered calculi are Turing powerful, while the unordered is not. The work [START_REF] Lowe | Extending csp with tests for availability[END_REF] studies CSP with a construct that checks if a parallel process is able to perform an output action on a given channel and a subsequent work [START_REF] Lowe | Models for csp with availability information[END_REF] investigates the expressiveness of its variants focusing on the full abstraction theorem of the trace equivalence. Our calculi [START_REF] Beauxis | On the asynchronous nature of the asynchronous pi-calculus[END_REF][START_REF] Bettini | Global progress in dynamically interleaved multiparty sessions[END_REF][START_REF] Busi | Comparing three semantics for Linda-like languages[END_REF][START_REF] Caires | Session types as intuitionistic linear propositions[END_REF] are Turing powerful and we aim to examine properties and applications of the typed bisimilarity characterised by buffered sessions: on the other hand, the focus of [START_REF] Busi | Comparing three semantics for Linda-like languages[END_REF] is a tuple space where our input/output order preserving examples (which treat different objects with the same session channel) cannot be naturally (and efficiently) defined. The same point applies to [START_REF] Lowe | Extending csp with tests for availability[END_REF][START_REF] Lowe | Models for csp with availability information[END_REF]. As another difference, the nature of localities has not been considered either in [START_REF] Busi | Comparing three semantics for Linda-like languages[END_REF][START_REF] Lowe | Extending csp with tests for availability[END_REF][START_REF] Lowe | Models for csp with availability information[END_REF] since no notion of a local or remote tuple or environment is defined. Further, none of the above work [START_REF] Beauxis | On the asynchronous nature of the asynchronous pi-calculus[END_REF][START_REF] Busi | Comparing three semantics for Linda-like languages[END_REF][START_REF] Lowe | Extending csp with tests for availability[END_REF][START_REF] Lowe | Models for csp with availability information[END_REF][START_REF] Philippou | On confluence in the pi-calculus[END_REF] treats large applications which include these constructs ( § 4) or the performance analysis of the proposed primitives.

Using eventful session types, we have demonstrated that our bisimulation theory is applicable, through the verification of the correctness of the Lauer-Needham transform. The asynchronous nature realised through IO message queues provides a precise analysis of local and eventful behaviours, found in major distributed transports such as TCP. The benchmark results from high-performance clusters in [23] show that the throughput for the thread-eliminated Server implementations in Session Java [START_REF] Hu | Type-safe eventful sessions in Java[END_REF] exhibits higher throughput than the multithreaded Server implementations, justifying the effect of the type and semantic preserving LN-transformation.

As the future work, we plan to investigate bisimulation theories under multiparty session types [START_REF] Honda | Multiparty Asynchronous Session Types[END_REF] and a relationship with a linear logic interpretation of sessions, which connects a behavioural theory and permutation laws under locality assumption [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF].

(

  Identifier) u ::= a, b | x, y k ::= s, s | x, y n ::= a, b | s, s (Value) v ::= tt, ff | a, b | s, s (Expression) e ::= v | x, y, z | arrived u | arrived k | arrived k h (Process) P, Q ::= u(x).P | u(x); P | k! e ; P | k?(x).P | k l; P | k {l i :

Definition 3 . 1 (

 31 Reduction Congruence). We write P ↓ a if P ≡ (ν n)(a s | R) with a ∈ n. Similarly we write P ↓s if P ≡ (ν n)(s [o : h• h] | R) with s ∈ n. P ⇓ n means ∃P .P → → P ↓ n. A typed relation R is reduction congruence if itis a congruence and satisfies the following conditions for each P 1 RP 2 whenever they are localised w.r.t. their given environments.

Theorem 3 . 3 (

 33 Soundness and Completeness). ≈ = ∼ =.

Lemma 3 . 4 (

 34 Input and Output Asynchrony). Suppose Γ P ∆ =⇒ P ∆ .-(output delay) If is an output action, then Γ P ∆ =⇒ -→ P ∆ .-(input advance) If is an input action, then Γ P ∆ -→=⇒ P ∆ .

  and (3) the symmetric case. Then we call R a determinate uptoexpansion relation, or often simply upto-expansion relation. Lemma 3.11. Let R be an upto-expansion relation. Then R ⊂≈.

  Above select from sel in selects a message from the selector queue sel, and treats it in P. The new construct creates a new environment y. The typecase construct then branches into different processes depending on the session of the received message, and dispatch the task to each code block.

	(input advance) or (2) (output delay) is satisfied or not. If not, we place a counterexam-
	ple (in (4), Π 1,2 [s i
	sel in typecase x of {
	i ?(nat); !(nat); ?(nat); !(nat) : new y : env in z(y)
	?(nat); !(nat); ?(nat); !(nat) : z(x, y)
	?(nat); !(nat)	: z(x, y)}
	The determinate property allows us to conclude that:
	Lemma 4.2. * a(w : S); R | a [ε] is confluent.

In the following sections, we study semantic properties of typed processes: however these developments can be understood without knowing the details of the typing rules. This is because the properties of the typing system are captured by the typed LTS defined in section 3.1 later.

. We write l 1 l

when l 1 = l 2 and if l 1 , l 2 are input actions, sbj(l 1 ) = sbj(l 2 ).

Acknowledgements. We thank Raymond Hu for collaborations and the reviewers for their useful comments. The work is partially supported by EP/F003757/1, EP/G015635/1, EP/G015481/1 and EP/F002114/1.

We can now establish the correctness of the transform. The proofs of the following results are found in [23], which use a determinate upto-expansion relation (Definition 3.10) through Lemmas 3.11. First we give a basic equation for the standard event loop, handling events by non-blocking handlers. We use recursive equations of agents for legibility, which can be easily encoded into recursions. P 1 = if arrived s 1 then (s 1 ?(x).R 1 ); P 2 elseif arrived s 2 then (s 2 ?(x).R 2 ); P 1 else P 1 P 2 = if arrived s 2 then (s 2 ?(x).R 2 ); P 1 elseif arrived s 1 then (s 1 ?(x).R 1 ); P 2 else P 2 where we assume well-typedness and each of R 1,2 , under any closing substitution and localisation, is determinate and reaches 0 after a series of outputs and τ-actions. The sequencing (s 1 ?(x).R 1 ); P 2 denotes the process obtained by replacing each 0 in R 1 with P 2 . We can then show P 1 ≈ P 2 by using the up-to-expansion relation. The following lemma proves its generalisation, elucidating the selectors behaviour in the stateless environment. It says that we can permute the session channels in a selector queue while keeping the same behaviour because of the determinacy of the server's code.

where each R i is determinate and reaches 0 after a sequence of non-blocking actions (outputs and τ-actions as well as a single input/branching action at x i ). The sequencing R i ; X is defined as above. Then, assuming typability, we have

Thus the selector's behaviour can be matched with the original threaded behaviour step by step in the sense that there is no difference between which event (resp. thread) is selected to be executed first. We conclude:

Discussions

Comparisons with Asynchronous/Synchronous Calculi. We give comprehensive comparisons with other calculi, clarifying the relationship between (1) the sessiontyped asynchronous π-calculus [START_REF] Honda | An object calculus for asynchronous communication[END_REF] without queues (≈ a , the asynchronous version of the labelled transition relation for the asynchronous π-calculus), (2) the session-typed synchronous π-calculus [START_REF] Honda | Language primitives and type disciplines for structured communication-based programming[END_REF][START_REF] Takeuchi | An Interaction-based Language and its Typing System[END_REF] without queues (≈ s ), (3) the asynchronous session πcalculus with two end-point queues without IO queues [START_REF] Coppo | Asynchronous Session Types and Progress for Object-Oriented Languages[END_REF][START_REF] Gay | Linear type theory for asynchronous session types[END_REF][START_REF] Mostrous | Session-based communication optimisation for higher-order mobile processes[END_REF] (≈ 2 ), and (4) the asynchronous session π-calculus with two end-point IO-queues (≈), i.e. the one developed in this paper. The semantics of ( 2) is called non-local since the output process directly puts the value into the input queue. The transition relation for non-local semantics (2) is defined by replacing the output and selection rules in the LTS relation to:


Tianxiang Lu

Stephan Merz
email: stephan.merz@loria.fr

Christoph Weidenbach
email: weidenbach@mpi-inf.mpg.de

Towards Verification of the Pastry Protocol using TLA +

Keywords: formal specification, model checking, verification methods, network protocols

Pastry is an algorithm that provides a scalable distributed hash table over an underlying P2P network. 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 and fault tolerance, it makes an interesting target for verification. We have modeled Pastry's core routing algorithms and communication protocol in the specification language TLA + . In order to validate the model and to search for bugs we employed the TLA + model checker tlc to analyze several qualitative properties. We obtained non-trivial insights in the behavior of Pastry through the model checking analysis. Furthermore, we started to verify Pastry using the very same model and the interactive theorem prover tlaps for TLA + . A first result is the reduction of global Pastry correctness properties to invariants of the underlying data structures.

Introduction

Pastry [START_REF] Rowstron | Pastry: Scalable, distributed object location and routing for large-scale peer-to-peer systems[END_REF][START_REF] Castro | Performance and dependability of structured peer-to-peer overlays[END_REF][START_REF] Haeberlen | Consistent key mapping in structured overlays[END_REF] is an overlay network protocol that implements a distributed hash table. The network nodes are assigned logical identifiers from an Id space of naturals in the interval [0, 2 M -1] for some M . The Id space is considered as a ring, i.e., 2 M -1 is the neighbor of 0. The Ids serve two purposes. First, they are the logical network addresses of nodes. Second, they are the keys of the hash table. An active node is in particular responsible for keys that are numerically close to its network Id, i.e., it provides the primary storage for the hash table entries associated with these keys. Key responsibility is divided equally according to the distance between two neighbor nodes. If a node is responsible for a key we say it covers the key.

The most important sub-protocols of Pastry are join and lookup. The join protocol eventually adds a new node with an unused network Id to the ring.

The lookup protocol delivers the hash table entry for a given key. An important correctness property of Pastry is Correct Key Delivery, requiring that there is always at most one node responsible for a given key. This property is non-trivial to obtain in the presence of spontaneous arrival and departure of nodes. Nodes may simply drop off, and Pastry is meant to be robust against such changes, i.e., churn. For this reason, every node holds two leaf sets of size l containing its closest neighbors to either side (l nodes to the left and l to the right). A node also holds the hash table content of its leaf set neighbors. If a node detects, e.g. by a ping, that one of its direct neighbor nodes dropped off, the node takes actions to recover from this state. So the value of l is relevant for the amount of "drop off" and fault tolerance of the protocol.

A lookup request must be routed to the node responsible for the key. Routing using the leaf sets of nodes is possible in principle, but results in a linear number of steps before the responsible node receives the message. Therefore, on top of the leaf sets of a node a routing table is implemented that enables routing in a logarithmic number of steps in the size of the ring. Pastry routes a message by forwarding it to nodes that match progressively longer prefixes with the destination key. In the example of Fig. 1, node 18 received a lookup message for key 95. The key is outside node 18's coverage and furthermore, it doesn't lie between the leftmost node and the rightmost node of its leaf sets. Querying its routing table, node 18 finds node 58, whose identifier matches the longest prefix with the destination key and then forwards the message to that node. Node 58 repeats the process and finally, the lookup message is answered by node 65, which is the closest node to the key 95, i.e., it covers key 95. In this case, we say that node 65 delivers the lookup request for key 95 (see also Fig. 4).

The first challenge in modeling Pastry was to determine an appropriate level of abstraction. As a guiding principle, we focused the model towards supporting detailed proofs of the correctness properties. We abstracted from an explicit notion of time because it does not contribute to the verification of correctness properties. For example, time-triggered periodic maintenance messages exchanged between neighbors are modelled by non-deterministic sending of such messages. In contrast, we developed a detailed model for the address ring, the routing tables, the leaf sets, as well as the messages and actions of the protocol because these parts are central to the correctness of Pastry.

The second challenge was to fill in needed details for the formal model that are not contained in the published descriptions of Pastry. Model checking was very helpful for justifying our decisions. For instance, it was not explicitly stated what it means for a leaf set to be "complete", i.e., when a node starts taking over coverage and becoming an active member on the ring. It was not stated whether an overlap between the right and left leaf set is permitted or whether the sets should always be disjoint. We made explicit assumptions on how such corner cases should be handled, sometimes based on an exploration of the source code of the FreePastry implementation [START_REF]Pastry: A substrate for peer-to-peer applications[END_REF]. Thus, we implemented an overlap in our model only if there are at most 2l nodes present on the entire network, where l is the size of each leaf set. A complete leaf set only contains less than l nodes, if there are less than l nodes on the overall ring.

A further challenge was to formulate the correctness property; in fact, it is not stated explicitly in the literature [START_REF] Rowstron | Pastry: Scalable, distributed object location and routing for large-scale peer-to-peer systems[END_REF][START_REF] Castro | Performance and dependability of structured peer-to-peer overlays[END_REF][START_REF] Haeberlen | Consistent key mapping in structured overlays[END_REF]. The main property that we are interested in is that the lookup message for a particular key is answered by at most one "ready" node covering the key. We introduced a more finegrained status notion for nodes, where only "ready" nodes answer lookup and join requests. The additional status of a node being "ok" was added in the refined model described in Section 4 to support several nodes joining simultaneously between two consecutive "ready" nodes.

The paper is organized as follows. In Section 2 we explain the basic mechanisms behind the join protocol of Pastry. This protocol is the most important part of Pastry for correctness. Key aspects of our formal model are introduced in Section 3. To the best of our knowledge, we present the first formal model covering the full Pastry algorithm. A number of important properties are model checked, subsections 3.3-3.4 and subsections 4.2-4.3, and the results are used to refine our model in case the model checker found undesired behavior. In addition to model checking our model, we have also been able to prove an important reduction property of Pastry. Basically, the correctness of the protocol can be reduced to the consistency of leaf sets, as we show in Section 5, Theorem 6. The paper ends with a summary of our results, related work, and future directions of research in Section 6. Further details and all proofs can be found in a technical report [START_REF] Lu | Towards verification of the pastry protocol using TLA+[END_REF].

The Join Protocol

The most sophisticated part of Pastry is the protocol for a node to join the ring. In its simplest form, a single node joins between two "ready" nodes on the ring. The new node receives its leaf sets from the "ready" nodes, negotiates with both the new leaf sets and then goes to status "ready".

The join protocol is complicated because any node may drop off at any time, in particular while it handles a join request. Moreover, several nodes may join the ring concurrently between two adjacent "ready" nodes. Still, all "ready" nodes must agree on key coverage.

Figure 2 presents a first version of the join protocol in more detail, according to our understanding from [START_REF] Rowstron | Pastry: Scalable, distributed object location and routing for large-scale peer-to-peer systems[END_REF] and [START_REF] Castro | Performance and dependability of structured peer-to-peer overlays[END_REF]. We will refine this protocol in Sect. 4 according to the description in [START_REF] Haeberlen | Consistent key mapping in structured overlays[END_REF]. Node j announces its interest in joining the ring by performing a Join action. At this point, its status is "wait". Its join request will be routed to the closest "ready" node i just like routing a lookup message, treating j as the key. Node i replies to j by performing a join reply, JReply action, transmitting its current leaf sets to enable node j to construct its own leaf sets. Then the node j probes all nodes in its leaf sets in order to confirm their presence on the ring. A probe reply, action PReply, signals j that the respective leaf set node received the probe message from j and updated its local leaf set with j . The reply contains the updated leaf set. Each time the node j receives a probe reply message, it updates the local information based on the received message and checks if there are outstanding probes. If no outstanding probe exists anymore or a timeout occurs, it checks whether its leaf set is complete. If it is, it finishes the join phase and goes to status "ready". Otherwise, any fault case is summarized in Fig. 2 by Repair. For example, if a probe eventually fails, the probed node needs to be removed from the leaf set. Then the node j probes the most distant nodes (leftmost and rightmost) in its leaf sets to get more nodes, retrying to complete its leaf set.

A First Formal Model of Pastry

We modeled Pastry as a (potentially infinite-state) transition system in TLA + [START_REF] Lamport | Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers[END_REF].

Although there are of course alternative logics and respective theorem provers for modelling Pastry, TLA + fits protocol verification quite nicely, because its concept of actions matches the rule/message based definition of protocols. Our model is available on the Web3 . We explain those parts of the model that are used later on for model checking and for proving the reduction theorem.

Static Model

Several parameters define the size of the ring and of the fundamental data structures. In particular, M ∈ N defines the space I = [0, 2 M -1] of node and key identifiers, and l ∈ N indicates the size of each leaf set. The following definition introduces different notions of distances between nodes or keys that will be used in the model. Definition 1 (Distances). Given x, y ∈ I :

Dist(x , y) ∆ =      x -y + 2 M -1 if x -y < -2 M -1 x -y -2 M -1 if x -y > 2 M -1 x -y, else AbsDist(x , y) ∆ = |Dist(x , y)| CwDist(x , y) ∆ = AbsDist(x , y) if Dist(x , y) < 0 2 M -AbsDist(x , y) else
The sign of Dist(x , y) is positive if there are fewer identifiers on the counterclockwise path from x to y than on the clockwise path; it is negative otherwise. The absolute value AbsDist(x , y) gives the length of the shortest path along the ring from x to y. Finally, the clockwise distance CwDist(x , y) returns the length of the clockwise path from x to y.

The leaf set data structure ls of a node is modeled as a record with three components ls.node, ls.left and ls.right. The first component contains the identifier of the node maintaining the leaf set, the other two components are the two leaf sets to either side of the node. The following operations access leaf sets.

Definition 2 (Operations on Leaf Sets).

GetLSetContent(ls)

∆ = ls.left ∪ ls.right ∪ {ls.node} LeftNeighbor (ls) ∆ =                ls.
)) ÷ 2 + 1)%2 M Covers(ls, k ) ∆ = CwDist(LeftCover (ls), k ) ≤ CwDist(LeftCover (ls), RightCover (ls))
In these definitions, ÷ and % stand for division and modulo on the natural numbers, respectively. Note that they are in fact only applied in the above definitions to natural numbers. We also define the operation AddToLSet(A, ls) that updates the leaf set data structure with a set A of nodes. More precisely, both leaf sets in the resulting data structure ls contain the l nodes closest to ls.node among those contained in ls and the nodes in A, according to the clockwise or counter-clockwise distance.

Dynamic Model

Fig. 3 shows the high-level outline of the transition model specification in TLA + . The overall system specification Spec is defined as Init ∧ [Next] vars , which is the standard form of TLA + system specifications. It requires that all runs start with a state that satisfies the initial condition Init, and that every transition either does not change vars (defined as the tuple of all state variables) or corresponds to a system transition as defined by formula Next. This form of system specification is sufficient for proving safety properties. If we were interested in proving liveness properties of our model, we should add fairness hypotheses asserting that certain actions eventually occur. The variable receivedMsgs holds the set of messages in transit. Our model assumes that messages are never modified. However, message loss is implicitly covered because no action is ever required to execute. The other variables hold vars ∆ = receivedMsgs, status, lset, probing, failed , rtable Init arrays that assign to every node i ∈ I its status, leaf set, the set of nodes it is currently probing, the set of nodes it has determined to have dropped off the ring, and its routing table. The predicate Init is defined as a conjunction that initializes all variables; in particular, the model takes a parameter A indicating the set of nodes that are initially "ready".

∆ = ∧ receivedMsgs = {} ∧ status = [i ∈ I → if i ∈ A then "ready" else "dead"] ∧ lset = [i ∈ I → if i ∈ A then AddToLSet(A, [node → i, left → {}, right → {}]) else [node → i, left → {}, right → {}]] ∧ probing = [i ∈ I → {}] ∧ failed = [i ∈ I → {}] ∧ rtable = . . . Next ∆ = ∃i, j ∈ I : ∨ Deliver (i, j ) ∨ Join(i, j ) ∨ JReply(i, j ) ∨ Probe(i, j ) ∨ PReply(i, j ) ∨ . . . Spec ∆ = Init ∧ [Next]vars
The next-state relation Next is a disjunction of all possible system actions, for all pairs of identifiers i , j ∈ I . Each action is defined as a TLA + action formula, which is a first-order formula containing unprimed as well as primed occurrences of the state variables, which refer respectively to the values of these variables at the states before and after the action. As an example, Fig. 4 shows the definition of action Deliver (i , k ) in TLA + . The action is executable if the node i is "ready", if there exists an unhandled message of type "lookup" addressed to i , and if k , the ID of the requested key, falls within the coverage of node i (cf. Definition 2). Its effect is here simply defined as removing the message m from the network, because we are only interested in the execution of the action, not in the answer message that it generates. The other variables are unchanged (in TLA + , unchanged e is a shorthand for the formula e = e).

Deliver (i, k ) ∆ = ∧ status[i] = "ready" ∧ ∃m ∈ receivedMsgs : ∧ m.mreq.type = "lookup" ∧ m.destination = i ∧ m.mreq.node = k ∧ Covers(lset[i], k ) ∧ receivedMsgs = receivedMsgs \ {m} ∧ unchanged status, rtable, lset, probing, failed , lease

Validation By Model Checking

We used tlc [START_REF] Yu | Model checking TLA+ specifications[END_REF], the TLA + model checker, to validate and debug our model. It is all too easy to introduce errors into a model that prevent the system from ever performing any useful transition, so we want to make sure that nodes can successfully perform Deliver actions or execute the join protocol described in Section 2. We used the model checker by asserting their impossibility, using the following formulas.

Property 3 (NeverDeliver and NeverJoin)

NeverDeliver ∆ = ∀i , j ∈ I : [¬Deliver (i , j )] vars NeverJoin ∆ = ∀j ∈ I \ A : (status[j ] = "ready")
The first formula asserts that the Deliver action can never be executed, for any i , j ∈ I . Similarly, the second formula asserts that the only nodes that may ever become "ready" are those in the set A of nodes initialized to be "ready". Running the model checker on our model, it quickly produced counter-examples to these claims, which we examined to ensure that the runs look as expected. (Section 4.3 summarizes the results for the model checking runs that we performed.)

We validated the model by checking several similar properties. For example, we defined formulas ConcurrentJoin and CcJoinDeliver whose violation yielded counter-examples that show how two nodes may join concurrently in close proximity to the same existing node, and how they may subsequently execute Deliver actions for keys for which they acquired responsibility.

Correct Key Delivery

As the main correctness property of Pastry, we want to show that at any time there can be only one node responsible for any key. This is formally expressed as follows.

Property 4 (Correct Key Delivery)

CorrectDeliver ∆ = ∀i , k ∈ I : enabled Deliver (i , k ) ⇒ ∧ ∀n ∈ I : status[n] = "ready" ⇒ AbsDist(i , k ) ≤ AbsDist(n, k ) ∧ ∀j ∈ I \ {i } : ¬enabled Deliver (j , k )
For an action formula A, the state formula enabled A is obtained by existential quantification over all primed state variables occurring in A; it is true at a state s whenever there exists some successor state t such that A is true for the pair (s, t), that is, when A can execute at state s. Thus, CorrectDeliver asserts that whenever node i can execute the Deliver action for key k then (a) node i has minimal absolute distance from k among all the "ready" nodes and (b) i is the only node that may execute Deliver for key k . When we attempted to verify Property 4, the model checker produced a counter-example, which we illustrate in Fig. 5. The run starts in a state with just two "ready" nodes c and d that contain each other in their respective leaf sets (the actual size of the leaf sets being 1). Two nodes a and b concurrently join between nodes c and d . According to their location on the ring, a's join request is handled by node c, and b's request by d . Both nodes learn about the presence of c and d , and add them to their leaf sets, then send probe requests to both c and d in order to update the leaf sets. Now, suppose that node d is the first to handle a's probe message, and that node c first handles b's probe. Learning that a new node has joined, which is closer than the previous entry in the respective leaf set, c and d update their leaf sets with b and a, respectively (cf. Fig. 5), and send these updated leaf sets to b and a. Based on the reply from d , node a will not update its leaf set because its closest left-hand neighbor is still found to be c, while it learns no new information about the neighborhood to the right. Similarly, node b maintains its leaf sets containing c and d . Now, the other probe messages are handled. Consider node c receiving a's probe: it learns of the existence of a new node to its right closer to the one currently in its leaf set (b) and updates its leaf set accordingly, then replies to a. However, node a still does not learn about node b from this reply and maintains its leaf sets containing c and d . Symmetrically, node d updates its leaf set to contain b instead of a, but b does not learn about the presence of a. At the end, the leaf sets of the old nodes c and d are correct, but a and b do not know about each other and have incorrect leaf set entries.

Finally, a lookup message arrives for key k , which lies between a and b, but closer to a. This lookup message may be routed to node b, which incorrectly believes that it covers key k (since k is closer to b than to c, which b believes to be its left-hand neighbor), and delivers the key.

The counter-example shows that our model of the join protocol may lead to inconsistent views of "ready" nodes about their neighborhoods on the ring, and is therefore insufficient. Indeed, after the initial publication of Pastry, Haeberlen et al. [START_REF] Haeberlen | Consistent key mapping in structured overlays[END_REF] presented a refined description of Pastry's join protocol, without providing an explicit motivation. We believe that the above counter example explains the refinement of [START_REF] Haeberlen | Consistent key mapping in structured overlays[END_REF], which we model and analyze in the sequel.

Refining the Join Protocol

In contrast to the join protocol described in Section 2, the refined join protocol requires an explicit transfer of coverage from the "ready" neighbor nodes before a joining node can become "ready" and answer lookup requests. In the case of the counter-example shown in Fig. 5, node a would request grants from the nodes c and d , which it believes to be its neighbors. Node d would refuse this request and instead inform node a of the presence of node b, enabling it to rebuild its leaf sets. Similarly, node b would learn about the presence of node a. Finally, the two nodes grant each other a lease for the nodes they cover. We now describe the extended protocol as we have understood and modelled it, and our further verification efforts. In fact, our formal model is also inspired by the implementation in FreePastry [START_REF]Pastry: A substrate for peer-to-peer applications[END_REF], where nodes periodically exchange their leaf sets to spread information about nodes dropping off and arriving.

Lease Granting Protocol

Figure 6 depicts the extension to the join protocol as described in Section 2 (cf. Fig. 2). After node i has built complete leaf sets, it reaches status "ok". It sends messages to its neighbors ln and rn (the two closest nodes in its current leaf sets), requesting a lease for the keys it covers. A node receiving a lease request from a node that it considers to be its neighbor grants the lease, otherwise it returns its own leaf sets to the requesting node. The receiving node will update its own leaf sets accordingly and request a lease from the new neighbor(s). Only when both neighbors grant the lease will node i become "ready". Moreover, any node that is "ok" or "ready" may non-deterministically rerun the lease granting protocol at any time. In the actual implementation, this happens periodically, as well as when a node suspects its neighbor to have left the ring.

We amended our TLA + model to reflect this extended join protocol and reran tlc on the extended model. Whereas the results for the properties used to validate the model (cf. Section 3.3) were unchanged, the model checker no longer produced a counter-example to Property 4. However, we were unable to complete the model checking run and killed tlc after it had been running for more than a month.

Symmetry of Leaf Sets

Based on the counter-example shown in Section 3.4, one may be tempted to assert that leaf set membership of nodes should be symmetrical in the sense that for any two "ready" nodes i , j it holds that i appears in the leaf sets of j if and only if j appears in the leaf sets of i .

Property 5 (Symmetry of leaf set membership)

Symmetry ∆ = ∀i , j ∈ I : status[i ] = "ready" ∧ status[j ] = "ready" ⇒ (i ∈ GetLSetContent(lset[j ]) ⇔ j ∈ GetLSetContent(lset[i ]))
However, the above property is violated during the execution of the join protocol and tlc yields the following counter-example: a node k joins between 1. tlc result with four nodes, leaf set length l = 1 i and j . It finishes its communication with i getting its coverage set from i , but its communication with j is not yet finished. Hence, i and j are "ready" whereas k is not. Furthermore, i may have removed j from its leaf set, so the symmetry is broken.

Validation

Table 1 summarizes the model checking experiments we have described so far, over the extended model. tlc was run with two worker threads (on two CPUs) on a 32 Bit Linux machine with Xeon(R) X5460 CPUs running at 3.16GHz with about 4 GB of memory per CPU. For each run, we report the running time, the number of states generated until tlc found a counter-example (or, in the case of Property 4, until we killed the process), and the largest depth of these states. Since the verification of Property 4 did not produce a counter-example, we ran the model checker in breadth-first search mode. We can therefore assert that if the model contains a counter-example to this property, it must be of depth at least 21.

All properties except Neighbor and NeighborProp were introduced in previous sections. The property Neighbor is inspired by the counter-example described in Section 3.4. It is actually the NeighborClosest property relaxed to "ok" and "ready" nodes. It asserts that whenever i , j are nodes that are "ok" or "ready", then the left and right neighbors of node i according to its leaf set contents must be at least as close to i than is node j . This property does not hold, as the counter-example of Section 3.4 shows, but it does if node i is in fact "ready", which corresponds the NeighborClosest property. The NeighborProp property is the conjunction HalfNeighbor ∧ NeighborClosest, see the next section.

Theorem Proving

Having gained confidence in our model, we now turn to formally proving the main correctness Property 4, using the interactive TLA + proof system (tlaps) [START_REF] Chaudhuri | Verifying safety properties with the TLA+ proof system[END_REF].

Our full proofs are available on the Web5 . The intuition gained from the counterexample of Section 3.4 tells us that the key to establishing Property 4 is that the leaf sets of all nodes participating in the protocol contain the expected elements. We start by defining a number of auxiliary formulas.

Ready ∆ = {i ∈ I : status[i ] = "ready"} ReadyOK ∆ = {i ∈ I : status[i ] ∈ {"ready", "ok"}} HalfNeighbor ∆ = ∨ ∀i ∈ ReadyOK : RightNeighbor (lset[i ]) = i ∧ LeftNeighbor (lset[i ]) = i ∨ ∧ Cardinality(ReadyOK ) ≤ 1 ∧ ∀i ∈ ReadyOK : LeftNeighbor (lset[i ]) = i ∧ RightNeighbor (lset[i ]) = i NeighborClosest ∆ = ∀i , j ∈ Ready : i = j ⇒ ∧ CwDist(LeftNeighbor (lset[i ]), i ) ≤ CwDist(j , i ) ∧ CwDist(i , RightNeighbor (lset[i ])) ≤ CwDist(i , j )
Sets Ready and ReadyOK contain the nodes that are "ready", resp. "ready" or "ok". Formula HalfNeighbor asserts that whenever there is more than one "ready" or "ok" node i , then the left and right neighbors of every such node i are different from i . In particular, it follows by Definition 2 that no leaf set of i can be empty. The formula NeighborClosest states that the left and right neighbors of any "ready" node i lie closer to i than any "ready" node j different from i . We used tlc to verify NeighborProp ∆ = HalfNeighbor ∧ NeighborClosest. Running tlc for more than a month did not yield a counter-example. Using tlaps, we have mechanically proved that NeighborProp implies Property 4, as asserted by the following theorem.

Theorem 6 (Reduction). HalfNeighbor ∧ NeighborClosest ⇒ CorrectDeliver .

We sketch our mechanically verified tlaps proof of Theorem 6 by two lemmas. The first lemma shows that, assuming the hypotheses of Theorem 6, then for any two "ready" nodes i , n, with i = n and key k , if node i covers k then i must be at least as close to k as is n.

Lemma 7 (Coverage Lemma).

HalfNeighbor

∧ NeighborClosest ⇒ ∀i , n ∈ Ready : ∀k ∈ I : i = n ∧ Covers(lset[i ], k ) ⇒ AbsDist(i , k ) ≤ AbsDist(n, k )
The second lemma shows, under the same hypotheses, that if i covers k then n cannot cover k . Taking together Lemma 7 and Lemma 8, Theorem 6 follows easily by the definitions of the property CorrectDeliver (Property 4) and the action Deliver (see Fig. 4).

Lemma 8 (Disjoint Covers).

HalfNeighbor ∧ NeighborClosest ⇒ ∀i , n ∈ Ready : ∀k ∈ I

: i = n ∧ Covers(lset[i ], k ) ⇒ ¬Covers(lset[n], k )
In order to complete the proof that our model of Pastry satisfies Property 4, it is enough by Theorem 6 to show that every reachable state satisfies properties HalfNeighbor and NeighborClosest. We have embarked on an invariant proof and have defined a predicate that strengthens these properties. We are currently in the process of showing that it is indeed preserved by all actions of our model.

Conclusion and Future Work

In this paper we have presented a formal model of the Pastry routing protocol, a fundamental building block of P2P overlay networks. To the best of our knowledge, this is the first formal model of Pastry, although the application of formal modeling and verification techniques to P2P protocols is not entirely new. For example, Velipalasar et al. [START_REF] Velipasalar | Design and verification of communication protocols for peer-to-peer multimedia systems[END_REF] report on experiments of applying the Spin model checker to a model of a communication protocol used in a P2P multimedia system. More closely related to our topic, Borgström et al. [START_REF] Borgström | Verifying a structured peer-to-peer overlay network: The static case[END_REF] present initial work towards the verification of a distributed hash table in a P2P overlay network in a process calculus setting, but only considered fixed configurations with perfect routing information. As we have seen, the main challenge in verifying Pastry lies in the correct handling of nodes joining the system on the fly. Bakhshi and Gurov [START_REF] Bakhshi | Verification of peer-to-peer algorithms: A case study[END_REF] model the Pure Join protocol of Chord in the π-calculus and show that the routing information along the ring eventually stabilizes in the presence of potentially concurrent joins. Numerous technical differences aside, they do not consider possible interferences between the join and lookup sub-protocols, as we do in our model.

Pastry is a reasonably complex algorithm that mixes complex data structures, dynamic network protocols, and timed behavior for periodic node updates. We decided to abstract from timing aspects, which are mainly important for performance, but otherwise model the algorithm as faithfully as possible. Our main difficulties were to fill in details that are not obvious from the published descriptions of the algorithm, and to formally state the correctness properties expected from Pastry. In this respect, the model checker helped us understand the need for the extension of the join protocol by lease granting, as described in [START_REF] Haeberlen | Consistent key mapping in structured overlays[END_REF]. It was also invaluable to improve our understanding of the protocol because it allowed us to state "what-if" questions and refute conjectures such as the symmetry of leaf set membership (Property 5). The building of the first overall model of Pastry in TLA + took us about 3 months. Almost two third of it was devoted to the formal development of the underlying data structures, such as the address ring, leaf sets or routing tables.

After having built up confidence in the correctness of our model, we started full formal verification using theorem proving. In particular, we have reduced the correctness Property 4 to a predicate about leaf sets that the algorithm should maintain, and have defined a candidate for an inductive invariant. Future work will include full verification of the correctness properties. Afterwards, we will extend the model by considering liveness properties, which obviously require assumptions about the ring being sufficiently stable. We also intend to study which parts of the proof are amenable to automated theorem proving techniques, as the effort currently required by interactive proofs is too high to scale to more complete P2P protocols.

Fig. 1 .

 1 Fig. 1. Pastry Routing Example

Fig. 2 .

 2 Fig. 2. Overview of the join protocol.

Fig. 3 .

 3 Fig. 3. Overall Structure of the TLA + Specification of Pastry.

Fig. 4 .

 4 Fig. 4. TLA + specification of action Deliver .

4

 4

Fig. 5 .

 5 Fig. 5. Counter-example leading to a violation of CorrectDeliver .

Fig. 6 .

 6 Fig. 6. Extending the Join Protocol by Lease Granting.

http://www.mpi-inf.mpg.de/ ~tianlu/software/PastryModelChecking.zip

Observe that there can be two nodes with minimal distance from k , to either side of the key. The asymmetry in the definition of LeftCover and RightCover is designed to break the tie and ensure that only one node is allowed to deliver.

http://www.mpi-inf.mpg.de/ ~tianlu/software/PastryTheoremProving.zip

Acknowledgements: We would like to thank the reviewers for their valuable comments.