Søren Debois

Thomas Hildebrandt

Tijs Slaats
email: tslaats@itu.dk

Nobuko Yoshida
email: yoshida@doc.ic.ac.uk

Type Checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion

We present the first session typing system guaranteeing response liveness properties for possibly non-terminating communicating processes. The types augment the branch and select types of the standard binary session types with a set of required responses, indicating that whenever a particular label is selected, a set of other labels, its responses, must eventually also be selected. We prove that these extended types are strictly more expressive than standard session types. We provide a type system for a process calculus similar to a subset of collaborative BPMN processes with internal (data-based) and external (event-based) branching, message passing, bounded and unbounded looping. We prove that this type system is sound, i.e., it guarantees request-response liveness for dead-lock free processes. We exemplify the use of the calculus and type system on a concrete example of an infinite state system.

Introduction

Session types were originally introduced as typing systems for particular πcalculi, modelling the interleaved execution of two-party protocols. A well-typed process is guaranteed freedom from race-conditions as well as communication compatibility, usually referred to as session fidelity [START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF][START_REF] Yoshida | Language primitives and type discipline for structured communication-based programming revisited: Two systems for higherorder session communication[END_REF][START_REF] Vasconcelos | Fundamentals of session types[END_REF]. Session types have subsequently been studied intensely, with much work on applications, typically to programming languages, e.g., [START_REF] Dezani-Ciancaglini | Objects and session types[END_REF][START_REF] Hu | Session-based distributed programming in Java[END_REF][START_REF] Honda | Scribbling interactions with a formal foundation[END_REF][START_REF] Mostrous | Session typing for a featherweight Erlang[END_REF]. A number of generalisations of the theory has been proposed, notably to multi-party session types [START_REF] Honda | Multiparty asynchronous session types[END_REF]. Multi-party session types have a close resemblance to choreographies as found in standards for business process modelling languages such as BPMN [START_REF]Object Management Group BPMN Technical Committee, Business Process Model and Notation[END_REF] and WS-CDL, and has been argued in theory to be able to provide typed BPMN processes [START_REF] Deniélou | Multiparty session types meet communicating automata[END_REF].

Behavioral types usually furnish safety guarantees, notably progress and lock-freedom [START_REF] Carbone | A graphical approach to progress for structured communication in web services[END_REF][START_REF] Bettini | Global progress in dynamically interleaved multiparty sessions[END_REF][START_REF] Coppo | Inference of global progress properties for dynamically interleaved multiparty sessions[END_REF][START_REF] Dezani-Ciancaglini | On progress for structured communications[END_REF][START_REF] Vieira | Typing progress in communication-centred systems[END_REF]. In contrast, in this paper we extend binary session types to allow specification of liveness-the property of a process eventually "doing something good". Liveness properties are usually verified by model-checking techniques [START_REF] Damm | Lscs: Breathing life into message sequence charts[END_REF][START_REF] Brill | Live sequence charts: An introduction to lines, arrows, and strange boxes in the context of formal verification[END_REF][START_REF] Cheung | Verification of liveness properties using compositional reachability analysis[END_REF], requiring a state-space exploration. In the present paper we show that a fundamental class of liveness properties, so-called request-response properties, can be dealt with by type rules, that is, without resorting to statespace exploration. As a consequence, we can deal statically with infinite state systems as exemplified below. Also, liveness properties specified in types can be understood and used as interface specifications and for compositional reasoning. As an example, the above diagram contains two pools: The Buyer and the ShoppingCart. Only the latter specifies a process, which has two parts: Ordering and Delivery. Ordering is a loop starting with an event-based gateway, branching on the message received by the customer. If it is AddItem or RemoveItem, the appropriate item is added or removed from the order, whereafter the loop repeats. If it is Checkout, the loop is exited, and the Delivery phase commences. This phase is again a loop, delivering the ordered items and then sending the invoice to the buyer.

A buyer who wants to communicate safely with the Shopping Cart, must follow the protocol described above, and in particular must be able to receive an unbounded number of items before receiving the invoice. Writing AI, RI, CO, DI, and SI for the actions "Add Items", "Remove Items", "Checkout", "Deliver Items" and "Send Invoice"; we can describe this protocol with a session type: µt.&{AI.?.t, RI.?.t, CO.?.µt . ⊕ {DI.!.t , SI.!.end}} . This session type can be regarded as a behavioral interface, specifying that the process first expects to receive either an AI (AddItem), RI (RemoveItem) or a CO (CheckOut) event. The two first events must be followed by a message (indicated by "?"), which in the implementation provides the item to be added or removed, after which the protocol returns to the initial state. The checkout event is followed by a message (again indicated by a "?") after which the protocol enters a new loop, either sending a DI (DeliverItem) event followed by a message (indicated by a "!") and repeating, or sending an SI (SendInvoice) event followed by a message (the invoice) and ending.

However, standard session types can not specify the very relevant liveness property, that a CheckOut event is eventually followed by an invoice event. This is an example of a so-called response property: an action (the request) must be followed by a particular response. In this paper we conservatively extend binary session types to specify such response properties, and we show that this extension is strictly more expressive than standard session types. We do so by annotating the checkout selection in the type with the required response: Intuitively: "if CO is selected, then subsequently also SI must be selected." Determining from the flow graph alone if this response property is guaranteed is in general not possible: Data values dictate whether the second loop terminates. However, we can remove this data-dependency by replacing the loop with a bounded iteration. In BPMN this can be realised by a Sequential Multiple Instance Subprocess, which sequentially executes a (run-time determined) number of instances of a sub-process. With this, we may re-define Delivery as in Fig. B, yielding a re-defined Shopping Cart process which has the response property.

In general, we need also be able to check processes where responses are requested within (potentially) infinite loops. The type system we present gives such guarantees, essentially by collecting all requested responses in a forward analysis, exploiting that potentially infinite loops can guarantee a particular response only if every path through the loop can; and that order (request-response vs responserequest) is in this case irrelevant. We prove that, if the system is lock free, then the typing system indeed guarantees that all requested responses are eventually fulfilled. Lock-freedom is needed because, as is well known, collaborative processes with interleaved sessions may introduce dependency locks. Lock-freedom is well-studied for both π-calculus, e.g., [START_REF] Kobayashi | A type system for lock-free processes[END_REF], and binary session types [START_REF] Carbone | A graphical approach to progress for structured communication in web services[END_REF][START_REF] Bettini | Global progress in dynamically interleaved multiparty sessions[END_REF][START_REF] Coppo | Inference of global progress properties for dynamically interleaved multiparty sessions[END_REF][START_REF] Dezani-Ciancaglini | On progress for structured communications[END_REF][START_REF] Vieira | Typing progress in communication-centred systems[END_REF], or may alternatively be achieved by resorting to global types [START_REF] Honda | Multiparty asynchronous session types[END_REF].

In summary, our contributions are as follows.

-We extend binary session types with a notion of required response.

-We prove that this extension induces a strictly more expressive language class than standard session types. -We give a typing system conservatively extending standard binary session types which gives the further guarantee that a lock-free well-typed process will, in any execution, provide all its required responses.

-We exemplify the use of these extended types to guarantee both safety and liveness properties for a non-trivial, infinite state collaborative process, which exhibits both possibly infinite looping and bounded iteration.

Related work. There is a vast amount of work on verification of collaborative processes. Most of the work take a model-checking approach, where the system under verification is represented as a kind of automaton or Petri Nets. An example that explicitly addresses collaborative business processes is [START_REF] Roa | A verification method for collaborative business processes[END_REF], which however does not cover liveness properties. Live Sequence Charts (LSCs) [START_REF] Damm | Lscs: Breathing life into message sequence charts[END_REF] is a conservative extension of Message Sequence Charts allowing to distinguish possible (may) from required (must) behaviour, and thus the specification of liveness properties. LSCs can be mapped to symbolic timed automata [START_REF] Brill | Live sequence charts: An introduction to lines, arrows, and strange boxes in the context of formal verification[END_REF] but relies as all model-checking approaches on abstraction techniques for reducing a large or even infinite state space to a tractable size. Here the work in [START_REF] Cheung | Verification of liveness properties using compositional reachability analysis[END_REF] is interesting for the fact that the model-checking can be split on components. The work in [START_REF] Kobayashi | A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes[END_REF] allows for model-checking of ML programs by a translation to higherorder recursion schemes. Interestingly, the model-checking problem is reduced to a type-checking problem, but rely on a technique for generation of a specific type system for the property of interest. In contrast, our approach is based on a single type system directly applicable for the process language at hand, where the (less general) liveness and safety properties of interest are specified as the type to be checked and can also be used as interface descriptions of processes.

The fair subtyping of [START_REF] Padovani | Fair subtyping for open session types[END_REF], the only work on session types addressing liveness we are aware of, details a liveness-preserving subtyping-relation for a session types-like CCS calculus. Here liveness is taken to mean the ability to always eventually output a special name, whereas in the present work, we consider the specification of fine-grained request-response liveness properties-"if something happens, something else must happen".

Overview of this paper. In Sec. 2 we define our calculus and its LTS-semantics.

In Sec. 3 we extend binary session types with specification of response liveness properties, give transition semantics for types, and sketch a proof that the extended types induce a strictly larger class of languages than does standard types.

In Sec. 4 we define exactly how types induce a notion of liveness on processes. In Sec. 5 we give our extended typing rules for sessions with responses and state its subject reduction result. In Sec. 6 we prove that the extended typing rules guarantees liveness for lock-free processes. Finally, in Sec. 7 we conclude. For want of space, this paper omits details and proofs; for these, refer to [START_REF] Debois | Type checking liveness for collaborative processes with bounded and unbounded recursion[END_REF].

Process Terms and Semantics

Processes communicate only via named communication (session) channels by synchronizing send and receive actions or synchronizing select and branch events (as in standard session typed π-calculus). The session typing rules presented in the next section guarantees that there is always at most one active send and receive action for a given channel. To distinguish dual ends of communication channels, we employ polarised names [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF][START_REF] Yoshida | Language primitives and type discipline for structured communication-based programming revisited: Two systems for higherorder session communication[END_REF]: If c is a channel name, c + and c -are the dual ends of the channel c. We call these polarised channel names, with "+" and "-" polarities. If k is a polarised channel name, we write k for its dual, e.g., c + = c -. In general c ranges over channel names; p over polarities +, -; k, h over polarised channel names; x over data variables; i over recursion variables (explained below); v over data values including numbers, strings and booleans; e over data expressions; and finally X, Y over process variables.

P ::= k! e .P | k?(x).P | k!l.P | k?{l i .P i } i∈I | 0 | P | Q | rec X.P | (rec e X(i).P ; Q) | X[ k] | if e then P else Q
The first four process constructors are for taking part in a communication. These are standard for session typed π-calculi, except that for simplicity of presentation, we only allow data to be sent (see Section 7). The process k! e .P sends data v over channel k when e ⇓ v, and proceeds as P . Dually, k?(x).P receives a data value over channel k and substitutes it for the x binding in P . A branch process k?{l i .P i } i∈I offers a choice between labels l i , proceeding to P i if the i'th label is chosen. The process 0 is the standard inactive process (termination), and P | Q is the parallel composition of processes P and Q.

Recursion comes in two forms: a general, potentially non-terminating recursion rec X.P , where X binds in P ; and a primitive recursion, guaranteed to terminate, with syntax (rec e X(i).P ; Q). The latter process, when e ⇓ n + 1, executes P {n/i} and repeats, and when e ⇓ 0, evolves to Q. By convention in (rec e X(i).P ; Q) neither of 0, rec Y.P , (rec e Y (i).P ; P ) and P | P occurs as subterms of P . These conventions ensure that the process (rec e X(i).P ; Q) will eventually terminate the loop and execute Q. Process variables X[ k] mention the channel names k active at unfolding time for technical reasons.

We define the free polarised names fn(P ) of P as usual, with fn(X[ k]) = k; substitution of process variables from X[ k]{P/X} = P ; and finally value substitution P {v/x} in the obvious way, e.g., k! e .P {v/x} = k! e{v/x} .(P {v/x}). Variable substitution can never affect channels.

Example 2.1. We now show how to model the example BPMN process given in the introduction. To illustrate the possibility of type checking infinite state systems, we use a persistent data object represented by a process DATA(o) communicating on a session channel o.

DATA(o) = rec X. o + ?(x). rec Y. o + ?      read. o + ! x . Y [o + ] write. X[o + ] quit. 0
After having received its initial value, this process repeatedly accepts commands read and write on the session channel o for respectively reading and writing its value, or the command quit for discarding the data object.

To make examples more readable, we employ the following shorthands. We write init(o, v).P for o -! v .P , which initializes the data object; we write free o.P for o -!quit.P , the process which terminates the data object session; we write read o(x).P for o -!read. o -?(x).P , the process which loads the value of the data object o into the process-local variable x; and finally, we write o := e.P for o -!write.o -! e .P , the process which sets the value of the data-object o.

The shopping cart process can then be modelled as

P (Q) = DATA(o) | init(o, ). rec X.k      AI. k?(x). read o(y). o := add(y, x). X[ko -] RI. k?(x). read o(y). o := rem(y, x). X[ko -] CO. k?(x). read o(y). o := add(y, x). Q
Here k is the session channel shared with the customer and o is the session channel for communicating with the data object modelling order data. We assume our expression language has suitable operators "add" and "rem", adding and removing items from the order. Finally, the process Q is a stand-in for either the (non live) delivery part of the BPMN process in

D 0 = rec Y. read o(y). if n(y) > 0 then k!DI. k! next(y) . o := update(y). Y [ko -] else k!SI. k! inv(y) . free o.0
where n(y) is the integer expression computing from the order y the number of items to send, next(y), update(y) and inv(y) are, respectively, the next item(s) to be sent; an update of the order to mark that these items have indeed been sent; and the invoice for the order. Whether this process terminates depends on the data operations. Using instead bounded iteration, live delivery becomes: (2) in prefix rules, the co-name of the subject cannot appear in the continuation. We impose (1) because if the co-channel of the subject of λ is in P , then P | P does not offer synchronisation on λ to its environment; the synchronisation is offered only to P . E.g., the process

D = read o(y). (rec n(y) Y (i).
P = c + ! v .Q | c -?(x).R does not have a transition c + ! v .Q | c -?(x).R c + !v ---→ Q | c -?(x).R.
If it had such a transition, no environment U able to receive on c -could be put in parallel with P and form a --→ P , and P contains k, again no well-typed environment for that process can contain k.

[C-Out] e ⇓ v k! e .P k!v --→ P k ∈ fn(P ) [C-In] k?(x).P k?v --→ P {v/x} k ∈ fn(P ) [C-Sel] k!l.P k⊕l --→ P k ∈ fn(P ) [C-Bra] k?{li.Pi}i∈I k&l i ---→ Pi k ∈ fn(P ) [C-ParL] P λ -→ Q P | P λ -→ Q | P subj(λ) ∈ fn(P ) [C-Com1] P k!v --→ P Q k?v --→ Q P | Q τ -→ P | Q [C-Com2] P k⊕l --→ P Q k&l --→ Q P | Q τ :l --→ P | Q [C-Rec] P {rec X.P/X} λ -→ Q rec X.P λ -→ Q [C-Prec0] e ⇓ 0 Q λ -→ R (rec e X(i).P ; Q) λ -→ R [C-PrecN] e ⇓ n + 1 P {n/i}{(rec n X(i).P ; Q)/X} λ -→ R (rec e X(i).P ; Q) λ -→ R [C-CondT] e ⇓ true P λ -→ P if e then P else Q λ -→ P [C-CondF] e ⇓ false Q λ -→ Q if e then P else Q λ -→ Q

Session Types with Responses

In this section, we generalise binary session types to session types with responses. In addition to providing the standard communication safety properties, these also allow us to specify response liveness properties.

Compared to standard session types, we do not consider delegation (name passing). Firstly, as illustrated by our example calculus, the types are already expressive enough to cover a non-trivial subset of collaborative processes. Secondly, as we show in the end of the section, session types with responses are already strictly more expressive than standard session types with respect to the languages they can express. Thus, as we also address in Sec. 7, admitting delegation and answering the open question about how response obligations can be safely exchanged with the environment, is an interesting direction for future work which is beyond the scope of the present paper.

We first define request/response liveness in the abstract. In general, we shall take it to be the property that "a request is eventually followed by a response". Definition 3.1. A request/response structure is a tuple (A, R, req, res) where A is a set of actions, R is a set of responses, and req : A → R and res : A → R are maps defining the set of responses requested respectively performed by an action.

Notation. We write for the empty string, we let φ, ψ range over finite strings, and we let α, β, γ range over finite or infinite sequences. We write sequence concatenation by juxtaposition, i.e., φα. Definition 3.2. Suppose (A, R, req, res) is a request/response structure and α a sequence over A. Then the responses res(α) of α is defined by res(α) = ∪{res(a) | ∃ϕ, β. α = ϕaβ}. Moreover, α is live iff α = φaβ =⇒ req(a) ⊆ res(β). Definition 3.3 (LTS with requests/responses). Let (S, L, -→) be an LTS. When the set of labels L is the set of actions of a request/response structure, we say that (S, L, -→) is an LTS with requests/responses, and that a transition sequence of this LTS is live when its underlying sequence of labels is.

Next, syntax of types. Let l range over labels and L sets of labels.

S, T

::= &{l i [L i ].T i } i∈I | ⊕{l i [L i ].T i } i∈I | !.T | ?.T | µt.T | t | end By convention, the l i in each &{l i [L i ].T i } i∈I resp. ⊕{l i [L i ].T i } i∈I are distinct.
A session type is a (possibly infinite) tree of actions permitted for one partner of a two-party communication. The type &{l i [L i ].T i } i∈I , called branch, is the type of offering a choice between different continuations. If the partner chooses the label l i , the session proceeds as T i . Compared to standard session types, making the choice l i also requests a subsequent response on every label mentioned in the set of labels L i ; we formalise this in the notion of responsive trace below. Dual to branch is select ⊕{l i [L i ].T i } i∈I : the type of making a choice between different continuations. Like branch, making a choice l i requests every label in L i as future responses. The type !.T and ?.T are the types of sending and receiving data values. As mentioned above, channels cannot be communicated. Also, we have deliberately omitted types of values (e.g. integers, strings, booleans) being sent, since this can be trivially added and we want to focus on the behavioural aspects of the types. Finally, session types with responses include recursive types. We take the equi-recursive view, identifying a type T and its unfolding into a potentially infinite tree. We define the central notion of duality between types as the symmetric relation induced coinductively by the following rules.

end end T T !.T ?.T T i T i J ⊆ I &{l i [L i ].T i } i∈I ⊕{l j [L j ].T j } j∈J (1)
The first rule says that dual processes agree on when communication ends; the second that if a process sends a message, its dual must receive; and the third says that if one process offers a branch, its dual must choose among the offered choices. However, required responses do not need to match: the two participants in a session need not agree on the notion of liveness for the collaborative session. Having defined the syntax of session types with responses, we proceed to give their semantics. The meaning of a session type is the possible sequences of communication actions it allows, requiring that pending responses eventually be done. Formally, we equip session types with a labeled transition semantics in Fig. D. We emphasise that under the equi-recursive view of session types, the Type transition labels: transition system of a recursive type T may in general be infinite.

ρ ::= ! | ? | &l[L] | ⊕l[L] Type transition label duality: ! ? and &l[L] ⊕l[L ] [D-Out] !.T ! -→ T ?.T ? -→ T [D-In] [D-Bra] i ∈ I &{li[Li].Ti}i∈I &l i [L i ] ----→ Ti i ∈ I ⊕{li[Li].Ti}i∈I ⊕l i [L i ] ----→ Ti [D-Sel]
Taking actions A to be the set of labels ranged over by ρ, and recalling that L is our universe of labels for branch/select, we obtain a request/response structure (A, P(L), req, res) with the latter two operators defined as follows.

res(!) = res(?) = ∅ res(&l[L]) = res(⊕l[L]) = {l} req(!) = req(?) = ∅ req(&l[L]) = req(⊕l[L]) = L
Selecting a label l performs the response l; pending responses L associated with that label are conversely requested. The LTS of Fig. D is thus one with responses, and we may speak of its transition sequences being live or not. Definition 3.5. Let T be a type. We define:

1. The traces tr(T ) = {(ρ i ) i∈I | (T i , ρ i ) i∈I transition sequence of T } 2. The responsive traces tr R (T ) = {α ∈ tr(T ) | α live }.
That is, in responsive traces any request is followed by a response. That is, we compare standard session types and session types of responses by considering the sequences of branch/select labels they admit. This follows recent work on multi-party session types and automata [START_REF] Deniélou | Multiparty session types meet communicating automata[END_REF][START_REF] Deniélou | Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types[END_REF]. Of these, only t is responsive; u is not, since it never selects SI as required by its CO action. That is, t, u ∈ str(T P ) and t ∈ str R (T P ), but u ∈ str R (T P ).

Theorem 3.8. The language of session types with responses R is strictly more expressive than that of standard session types T ; that is, T ⊂ R.

Proof (sketch). The non-strict inclusion is immediate by definition; it remains to prove it strict. For this consider the session type with responses

T = µt. ⊕ {a[b].t; b[a]
.t}, which has as responsive traces all strings with both infinitely many as and bs. We can find every sequence a n as a prefix of such a trace. But, (by regularity) any standard session type that has all a n as finite traces must also have the trace a ω , which is not a responsive trace of T , and thus the responsive traces of T can not be expressed as the traces of a standard session type.

Session Typing

Recall that the standard typing system [START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF][START_REF] Yoshida | Language primitives and type discipline for structured communication-based programming revisited: Two systems for higherorder session communication[END_REF] for session types has judgements Θ std P ∆. We use this typing system without restating it; refer to either [START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF][START_REF] Yoshida | Language primitives and type discipline for structured communication-based programming revisited: Two systems for higherorder session communication[END_REF] or the full version of this paper [START_REF] Debois | Type checking liveness for collaborative processes with bounded and unbounded recursion[END_REF]. In this judgement, Θ takes process variables to session type environments; in turn, a session typing environment ∆ is a finite partial map from channels to types. We write ∆, ∆ for the union of ∆ and ∆ , defined when their domains are disjoint. We say ∆ is completed if ∆(T ) = end when defined; it is balanced if k : T, k : U ∈ ∆ implies T U . We generalise transitions of types (Fig. D) to session typing environments in Fig. E, with transitions δ ::= τ | τ : l, L | k : ρ. We define subj(k : ρ) = k and subj(τ : l, L) = subj(τ ) = τ . We lift sel(-), req(-), and res(-) to actions δ in

[E-Lift] T ρ -→ T k : T k:ρ --→ k : T [E-Par] ∆ δ -→ ∆ ∆, ∆ δ -→ ∆ , ∆ [E-Com1] ∆1 k:! -→ ∆ 1 ∆2 k:? --→ ∆ 2 ∆1, ∆2 τ -→ ∆ 1 , ∆ 2 [E-Com2] ∆1 k:⊕l[L] ----→ ∆ 1 ∆2 k:&l[L ] -----→ ∆ 2 ∆1, ∆2 τ :l,L∪L -----→ ∆ 1 , ∆ 2 Fig. E. Transitions of types (2)
the obvious way, e.g., req(τ : l, L) = L. The type environment transition is thus an LTS with responses, and we may speak of its transition sequences being live. We can now say what it means for a process to be live (relying on the definition of maximal transition sequences given in Def. 6.2 below).

Definition 4.4 (Live process).

A well-typed process Θ std P ∆ is live wrt. Θ, ∆ iff for any maximal transition sequence (P i , λ i ) i of P there exists a live type transition sequence (∆ i , δ i ) i of ∆ s.t. ((P i , ∆ i ), (λ i , δ i )) i is a typed transition sequence of Θ std P ∆.

Example 4.5. Wrt. the standard session typing system, both of the processes P (D 0 ) and P (D) of Example 2.1 are typable wrt. the types we postulated for them in Example 3.4. Specifically, we have • std P (D 0 ) k : T P , o + : T D , o -: T D and similarly for P (D). The judgement means that the process P (D) treats k according to T P and the (two ends of) the data object according to T D and its syntactic dual T D . The standard session typing system of course does not act on our liveness annotations, and so does not care that P (D 0 ) is not live.

Typing System for Liveness

We now give our extended typing system for session types with responses. The central judgement will be Γ ; L P ∆, with the intended meaning that "with process variables Γ and pending responses L, the process P conforms to ∆." We shall see in the next section that a well-typed lock-free P is live and will eventually perform every response in L. We need: At each state but the initial one either b or a is pending. Yet the process is live: any response requested in the body of the recursion is also discharged in the body, although not in order. Since infinite behaviour arises as of unfolding of recursion, responses are ensured if the body of every recursion discharges the requests of that body, even if out of order.

[F-Par] Γ ; L1 P1 ∆1 Γ ; L2 P2 ∆2 Γ ; L1 ∪ L2 P1 | P2 ∆1, ∆2 [F-Inact] ∆ completed Γ ; ∅ 0 ∆ [F-Var] L ⊆ I ⊆ A dom(∆) = k Γ, X : (A, I, ∆); L X[ k] ∆ [F-VarP] L ⊆ L dom(∆) = k Γ, X : (L , ∆); L X[ k] ∆ [F-RecP] Γ, X : (L , ∆); L P ∆ Γ ; L Q ∆ L ⊆ L Γ ; L (rec e X(i).P ; Q) ∆ [F-Rec]
For general recursion, [F-Rec] and [F-Var], we thus find for each recursion a set of responses, such that at most that set is requested in its body and that it reponds with at least that set. In the process variable environment Γ we record this response invariant for each variable, along with a tally of the responses performed since the start of the recursion. The tally is updated by the rules [F-Sel]/[F-Bra] for select and branch. The rule for process variable [F-Var] typing then checks that the tally includes the invariant, and that the invariant includes every currently pending response. Definition 5.1. We define std(Γ ), the standard process variable environment of Γ by std(Γ )(X) = ∆ when Γ (X) = (A, I, ∆) or Γ (X) = ∆. Theorem 5.2. If Γ ; L P ∆ then also std(Γ ) std P ∆.

Liveness

We now prove that a lock-free process well-typed under our liveness typing system is indeed live as defined in Def. 4.4. To define lock-freedom and fairness, we must track occurrences of prefixes across transitions. This is straightforward in the absence of a structural congruence; refer to [START_REF] Fossati | Intensional and extensional characterisation of global progress in the π-calculus[END_REF] for a formal treatment. Our notion of lock-freedom is derived from [START_REF] Kobayashi | A type system for lock-free processes[END_REF]. Definition 6.1. A prefix M is a process on one of the forms k! e .P , k?(x).P , k?{l i .P i }, or k!l.P . An occurence of a prefix M in a process P is a path in the abstract syntax tree of P to a subterm on the form M (see [START_REF] Fossati | Intensional and extensional characterisation of global progress in the π-calculus[END_REF] for details). An occurrence of a prefix P in M where P λ -→ Q is preserved by the latter if M has the same occurrence in Q; executed otherwise. It is enabled if it is executed by some transition, and top-level if it is not nested in another prefix. Definition 6.2. An infinite transition sequence s = (P i , λ i ) i∈N is fair iff whenever a prefix M occurs enabled in P n then some m ≥ n has P m λm --→ P m+1 executing that occurence. A transition sequence s is terminated iff it has length n and P n -→. It is maximal iff it is finite and terminated or infinite and fair. A maximal transition sequence (P i , λ i ) is lock-free iff whenever there is a toplevel occurence of a prefix M in P i , then there exists some j ≥ i s.t. P j λj -→ P j+1 executes that occurrence. A process is lock-free iff all its transition sequences are. Definition 6.3. For a process transition label λ, define sel(λ) by sel(k!v) = sel(k?v) = sel(τ ) = ∅ and sel(k&l) = sel(k ⊕ l) = sel(τ : l) = l. Given a trace α we lift sel(-) pointwise, that is, sel(α) = {sel(λ) | α = φλα }. Proposition 6.4. Suppose • ; L P ∆ with P lock-free, and let s = (P i , α i ) i be a maximal transition sequence of P . Then L ⊆ sel(α). Theorem 6.6. Suppose • ; L P ∆ with P lock-free. Then P is live for • , ∆. Example 6.7. We saw in Example 5.4 that P (D) is typable as •; ∅ P (D) k : T P , o + : T D , o -: T D . Noting P (D) lock-free, by the above Theorem it is live, and so will uphold the liveness guarantee in T P : if CO is selected, then eventually also SI is selected. Or in the intuition of the example: If the buyer performs "Checkout", he is guaranteed to subsequently receive an invoice.

Conclusion and Future Work

We introduced a conservative generalization of binary session types to session types with responses, which allows to specify response liveness properties. We showed that session types with responses are strictly more expressive (wrt. the classes of behaviours they can express) than standard binary session types. We provided a typing system for a process calculus similar to a non-trivial subset of collaborative BPMN processes with possibly infinite loops and bounded iteration and proved that lock-free, well typed processes are live.

We have identified several interesting directions for future work: Firstly, the present techniques could be lifted to multi-party session types, which guarantees lock-freedom. Secondly, investigate more general liveness properties. Thirdly, channel passing is presently omitted for simplicity of presentation and not needed for our expressiveness result (Theorem 3.8). Introducing it, raises the question of wether one can delegate the responsibility for doing responses or not? If not, then channel passing does not affect the liveness properties of a lock-free process, and so is not really interesting for the present paper. If one could, it must be ensured that responses are not forever delegated without ever being fulfilled, which is an interesting challenge for future work. We hope to leverage existing techniques for the π-calculus, e.g., [START_REF] Kobayashi | A type system for lock-free processes[END_REF]. Finally, and more speculatively, we plan to investigate relations to fair subtyping [START_REF] Padovani | Fair subtyping for open session types[END_REF] and Live Sequence Charts [START_REF] Damm | Lscs: Breathing life into message sequence charts[END_REF].

Fig

  Fig. A. A Potentially Non-live Shopping Cart BPMN Process

Fig. B .

 B Fig. B. Live delivery with MI Sub-Process

  Fig. A or the live delivery part shown in Fig. B. The non-live delivery loop can be represented by the process

  k!DI.read o(y). k! pickitem(y, i) .Y [ko -]; k!SI. read o(y). k! inv(y) . free o.0) (The second line is the body of the loop; the third line is the continuation.) Here pickitem(y, i) is the expression extracting the ith item from the order y. Transition Semantics. We give a labelled transition semantics in Fig C. We assume a total evaluation relation e ⇓ v; note the absence of a structural congruence. We assume τ is neither a channel nor a polarised channel. Define subj(k!v) = subj(k?v) = subj(k&l) = subj(k⊕l) = k and subj(τ ) = subj(τ : l) = τ , and τ = τ . We use these rules along with symmetric rules for [C-ParL] and [C-Com1/2]. Compared to standard CCS or π semantics, there are two significant changes: (1) In the [C-ParL], a transition λ of P is not preserved by parallel if the co-channel of the subject of λ is in P ; and

Fig. C .

 C Fig. C. Transition semantics for terms

Fig. D .

 D Fig. D. Transitions of types (1)

Definition 3 . 6 .

 36 A type T is a standard session type if it requests no responses, that is, every occurrence of L in it is has L = ∅. Define sel(ρ) = l when ρ = &l[L] or ρ = ⊕l[L], otherwise ; lift sel(-) to sequences by union. We then define: 1. The selection traces str(T ) = {sel(α) | α ∈ tr(T )} 2. The responsive selection traces str R (T ) = {sel(α) | α ∈ tr R (T )}. 3. The language of standard session types T = {α | α ∈ str(T ), T is a standard session type}. 4. The language of responsive session types R = {α | α ∈ str R (T ), T is a session type with responses}.

Example 3 . 7 .

 37 The type T P of Example 3.4 has (amongst others) the two selection traces: t = AI CO DI DI SI and u = AI CO DI DI DI • • • .

Definition 4 . 1 .Theorem 4 . 2 .Definition 4 . 3 .

 414243 We define a binary relation on type transition labels δ and transition labels λ, written δ λ, as follows. τ τ , k : &l[L] k&l, k : ! k!v, τ : l, L τ : l, k : ⊕l[L] k ⊕ l, k : ? k?x. If Γ std P ∆ and P λ -→ Q, then there exists δ λ s.t. ∆ δ -→ ∆ and Γ std Q ∆ . The typed transition system is the transition system which has states Γ std P ∆ and transitions Γ std P ∆ λ,δ --→ Γ std P ∆ whenever there exist transitions P λ -→ P and ∆ δ -→ ∆ with δ λ.

[

  F-Out] Γ ; L P ∆, k : T Γ ; L k! e .P ∆, k : !.T [F-In] Γ ; L P ∆, k : T Γ ; L k?(x).P ∆, k : ?.T [F-Bra] ∀i ∈ I : Γ + li; (L \ li) ∪ Li Pi ∆, k : Ti Γ ; L k?{li.Pi} i∈I ∆, k : &{li[Li].Ti}i∈I [F-Sel] Γ + lj; (L \ lj) ∪ Lj P ∆, k : Tj Γ ; L k!lj.P ∆, k : ⊕{li[Li].Ti}i∈I (j ∈ I)

  Γ, X : (∅, I, ∆); I P ∆ L ⊆ I Γ ; L rec X.P ∆ [F-Cond] Γ ; L P ∆ Γ ; L Q ∆ Γ ; L if e then P else Q ∆ Fig. F. Typing System Our typing system is in Fig. F. The rules [F-Bra]/[F-Sel] types branch/select.To type k!l.P wrt. k : ⊕l[L ].T , P must do every response in L . For this we maintain an environment L of pending responses. In the hypothesis, when typing P , we add to this the new pending responses L . But selecting l performs the response l, so altogether, to support pending responses L in the conclusion, we must have pending responses L \ {l} ∪ L in the hypothesis. Branching is similar.For finite processes, liveness is ensured if the inactive process can be typed with the empty request environment. For infinite processes there is no point at which we can insist on having no pending responses. Consider rec X. k!a. k!b. X[k], typeable under k : µt. ⊕ {a[b].t; b[a].t}. This process has the single transition sequence P k⊕a ---→ k!b.P k⊕b --→ P k⊕a ---→ • • •.

Theorem 5 . 3 (

 53 Subject reduction). Suppose that •; L P ∆ with and P λ -→ Q. Then there exists a type transition ∆ δ -→ ∆ with δ λ, such that •; (L \ res(δ)) ∪ req(δ) Q ∆ . Moreover, if ∆ balanced then also ∆ balanced. Example 5.4. With the system of Figure F, the process P (D) is typable wrt. the types given Example 3.4. The process P (D 0 ) on the other hand is not: We have •; ∅ P (D) k : T P , o + : T D , o -: T D , but the same does not hold for P (D 0 ). We also exemplify a typing judgment with non-trivial guaranteed responses. The process D, the order-fulfillment part of P (D), can in fact be typed •; {SI} D k : µt . ⊕{DI.!.t , SI.!.end}, o -: T D Note the left-most {SI}, indicating intuitively that this process will eventually select SI in any execution. The process D has this property essentially because it is implemented by bounded recursion.

Example 6 . 5 .

 65 We saw in Example 5.4 that the process D of Example 2.1 is typable •; {SI} D • • • . By Proposition 6.4 above, noting that D is clearly lock-free, every maximal transition sequence of D must eventually select SI.

  µt.&{AI.?.t, RI.?.t, CO[{SI}].?.µt . ⊕ {DI.!.t , SI.!.end}} .

  Example 3.4. Recall from Ex. 2.1 the processes DATA(o) encoding data-object and P (D) encoding the (live) shopping-cart process. The former treats the channel o as T D = µt.?.µs.&{read.!.s, write.t, quit.end }. The latter treats its channel k to the buyer as T P = µt.&{AI.?.t, RI.?.t, CO[{SI}].?.µt . ⊕ {DI.!.t , SI.!.end}}. To illustrate both responses in unbounded recursion and duality of disparate responses, note that the P (D) actually treats its data object channel o -according to the type T E = µt.!.µs. ⊕ {read.?.s, write[{read}].t, quit.end }, i.e., every write is eventually followed by a read. However, T D T E : the types T E and T D are nonetheless dual.

Session typing environments ∆ defined at the start of Section 4.

Response environments L are simply sets of branch/select labels.

Process variable environments Γ are finite partial maps from process variables X to tuples (L, L, ∆) or (L, ∆). We write these (A, I, ∆) for (A)ccumulated selections and request (I)nvariant. We define (Γ +L)(X) = (A∪L, I, ∆) when Γ (X) = (A, I, ∆) and Γ (X) otherwise, writing Γ +l instead of Γ +{l}.

( ) Work supported in part by the Computational Artifacts project (VELUX 33295, 2014-2017), by the Danish Agency for Science, Technology and Innovation, and by EPSRC EP/K034413/1, EP/K011715/1 and EP/L00058X/1.


Peter Zeller
email: pzeller@cs.uni-kl.de

Annette Bieniusa
email: bieniusa@cs.uni-kl.de

Arnd Poetzsch-Heffter

Formal Specification and Verification of CRDTs

Keywords: CRDT, formal verification, eventual consistency

Convergent Replicated Data Types (CRDTs) can be used as basic building blocks for storing and managing replicated data in a distributed system. They provide high availability and performance, and they guarantee eventual consistency. In this paper, we develop a formal framework for the analysis and verification of CRDTs. We investigate and compare the three currently used specification techniques for CRDTs and formalize them based on an abstract model for managing replicated data in distributed systems. We show how CRDT implementations can be expressed in our framework and present a general strategy for verifying CRDTs. Finally, we report on our experiences in using the framework for the verification of important existing CRDT implementations. The framework and the proofs were developed within the interactive theorem prover Isabelle/HOL.

Introduction

Global computing systems and worldwide applications often require data replication, that is, the data is not only stored at one computing node, but at several nodes. There are a number of reasons for replication. To realize reliable services, high availability and fault-tolerance might be important. A centralized storage system might not provide enough throughput for allowing millions of users to access the data. Furthermore, systems often serve clients from different regions in the world; Geo-replication helps to keep the latency low. Last but not least, mobile clients might not be connected all the time, but should provide certain offline functionality using a local store that is synchronized with the global state when the connection is reestablished.

The CAP theorem [START_REF] Gilbert | Brewer's conjecture and the feasibility of consistent, available, partition-tolerant web services[END_REF] tells us that distributed systems cannot guarantee high availability, partition tolerance, and strong consistency at the same time. In this paper, we investigate techniques that aim at high availability and partition tolerance by providing a weaker form of consistency, called eventual consistency [START_REF] Terry | Managing update conflicts in bayou, a weakly connected replicated storage system[END_REF][START_REF] Vogels | Eventually consistent[END_REF][START_REF] Saito | Optimistic replication[END_REF][START_REF] Burckhardt | Replicated data types: specification, verification, optimality[END_REF].

In an eventually consistent system, the different replicas do not have to provide the same view of the data at all times. Operations manipulating the data are first applied to a subset of the replicas. At some suitable later point in time, the updates are communicated to the other replicas. Only after all updates are delivered to all replicas the data has to be consistent again. This means in particular that the replicas have to be able to merge concurrent updates into a consistent view. It usually depends on the application how a merge operation should behave. The idea of replicated data types is to package a behavior given by operations and a way to handle concurrent updates, so that they can be reused in many situations.

Convergent replicated data types (CRDTs) [START_REF] Shapiro | A comprehensive study of Convergent and Commutative Replicated Data Types[END_REF] are a special class of replicated data types where concurrent updates are handled by merging the resulting states. The basic setting is that there is a number of replicas of the data type. Operations are executed on a single replica and the different replicas conceptually exchange their whole states with each other according to some protocol. The state of a replica is also called the payload. To guarantee convergence, there needs to be a partial order on the payloads and a merge operation computing the least upper bound, such that the payloads form a semilattice. All operations which change the payload have to increase the payload with respect to the partial order. This setup ensures that replicas which have seen the same set of updates also have the same state and thus return the same value. This property is called Strong Eventual Consistency (SEC) [START_REF] Shapiro | Conflictfree replicated data types[END_REF].

A simple example of a CRDT is a counter. A counter provides update operations to increment or decrement the value and a query function to read the value. It is usually implemented by keeping the number of increments and the number of decrements for each replica in a map from replica-IDs to positive integers. Each replica only increments its own increment-and decrement-counts and states are merged by taking the component-wise maximum. It is easy to prove that this computes a least upper bound. The value of the counter can be determined by summing up all increment counts in the map and subtracting the sum of the decrement counts. Separating increment-and decrement-counts ensures, that the updates are increasing operations. Having a count for every replica instead of a single counter ensures that no updates are lost due to concurrent writes.

Contributions.

In general, CRDT implementations can be quite sophisticated and complex, in particular in the way they handle concurrent updates. Therefore it is important to provide high-level behavioral specifications for the users and techniques to verify CRDT implementations w.r.t. their specifications. Towards this challenge, the paper makes the following contributions:

-A framework in Isabelle/HOL [START_REF] Nipkow | Isabelle/HOL -A Proof Assistant for Higher-Order Logic[END_REF] that supports the formal verification of CRDTs. The framework in particular provides a system model that is parametric w.r.t. the CRDT to be analyzed and support for verification. -We analyzed, clarified, and formalized different specification and abstract implementation techniques for CRDTs (Sections 3, 4 and 6). -We successfully verified a number of CRDTs described in the literature with our framework.

We present the system model in Section 2; describe our specification technique in Section 3, the implementation technique in Section 4 and the verification as-

-→ s s as -→ s s a -→ s s as;a --→ s (update) v = vs(r)(r+=1) pl = update crdt (a, r, pls(r))
(pls,vs,ph)

Update(r,a)

-------→ (pls(r := pl ), vs(r

:= v ), ph ∪ {(v , pl )}) (merge) (v, pl) ∈ ph v = vs(r) v pl = merge crdt (pls(r), pl) (pls,vs,ph) Merge(r,v,pl)
--------→ (pls(r := pl ), vs(r

:= v ), ph ∪ {(v , pl )})
Table 1. System Model pects in Section 5. In Section 6 we discuss an alternative specification technique. Finally, we consider related work, summarize the results, and give an outlook on future work in Sections 7 and 8

System model

We developed a formal system model that supports an arbitrary but fixed number of replicas and is parametric in the CRDT to be analyzed, i.e., it can be instantiated with different CRDTs. A CRDT is parameterized by four type parameters and described by four components:

-pl, the type of the payload (i.e. the state at each replica) -ua, the type for the update arguments (a sum type of all update operations) -qa, the type for the query arguments (a sum type of all query operations) -r, the sum type for the possible return values of the queries -init :: pl , the initial payload for all replicas -update :: ua ⇒ replicaId ⇒ pl ⇒ pl , the function expressing how an update operation modifies the payload at a given replica, where replicaId denotes the node on which the update is performed first -merge :: pl ⇒ pl ⇒ pl , the function merging payloads -query :: qa ⇒ pl ⇒ r , the function expressing the results of querying a payload Given a CRDT (init crdt , update crdt , merge crdt , query crdt ), the system model describes the labeled transition relation s tr -→ s expressing that executing trace tr in state s leads to state s (cf. Table 1) where a trace is a sequence of operations and an operation is either the application of an update or a merge (queries need not be considered, as they do not modify the state). The state of the system consists of three components:

-For each replica r, its current payload.

-For each replica r, its current version vector [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF]. The version vector or short version is a mapping from replica-IDs to natural numbers. If the version of r has m as entry for key k, the payload of r has merged the first m operations applied to replica k into its payload. -The set of all version-payload pairs that have been seen during execution so far. This set is called the payload history and is used to make sure that a merge operation can only be applied to version-payload pairs that appeared earlier in the execution.

Initially, the payload of each replica is init crdt , the version vector of each replica is the all-zero vector, and the payload history is the empty set. There are two kind of transition steps:

-An update operation Update(r , a) applies an update function of the CRDT (determined by the arguments a) to the current payload of r and modifies the state accordingly; in particular, the rth component of the version vector of r is incremented by one. -A merge operation Merge(r, v, pl) is executed as follows: The new version v is calculated by taking the least upper bound of the old version vector vs(r) and the merged version vector v. Similarly, the new payload pl is the least upper bound operation on payloads, which is specific to the respective CRDT, and implemented by the merge crdt function.

Discussion. The system model focuses on simple operational behavior. Other aspects, such as timestamps, were intentionally left out because they would make the system model more complicated than needed for most CRDTs. Only a few CRDTs like the Last-Writer-Wins-Register depend on timestamps. Also, often timestamps are only used to provide some total order on operations, and lexicographic ordering of the version vectors also suffices to provide such an order.

Specification

In this section we present and formalize a technique for specifying the behavior of CRDTs based on the system model presented in the previous section.

A specification should tell users the result value of any query operation, when a trace of operations performed in the system is given. A trace gives a total order on the operations performed in the system, but for operations performed independently on different replicas this order does not influence the result. Therefore, we would like to abstract from this total order. Furthermore, the traces include explicit merge operations, but from a user's perspective this merge operations are implicit. Thus, it should not be important, how updates were delivered to a replica. The result of an operation should only depend on those operations that are visible when the operation is about to be performed. Hence, the trace can be actually deconstructed into a partially ordered set of update operations, where the partial order is the visibility relation, which we denote by ≺ in the following.

The specification technique that we formalize here supports the sketched abstractions and explains the result of an operation only depending on the visible update history. It follows the ideas from Bouajjani et al. [START_REF] Bouajjani | Verifying eventual consistency of optimistic replication systems[END_REF], and Burckhardt et al. [START_REF] Burckhardt | Replicated data types: specification, verification, optimality[END_REF], but is specifically tailored to CRDTs, allowing for some simplifications. In the case of CRDTs, the visibility relation is a partial order. All operations at one replica are ordered by time and a merge makes all operations, which are visible to the source of the merge, visible at the destination of the merge.

Formalization. In our formalization we represent the visibility relation using version vectors. The advantage of this is that they are easy to handle in the operational semantics and also when working with Isabelle/HOL. The properties of a partial order like transitivity and antisymmetry are already given by the structure and do not have to be specified additionally. The version vector at each replica can be directly derived from a given trace. It also uniquely identifies every operation, and we can encode the whole history of updates with the visibility relation as a set of update operations, represented by (version, replicaId , args) triples. We call this structure the update history and denote it by H in the following. The visibility relation ≺ on update operations is simply derived from the order on the version vectors.

A specification is formalized as a function spec, which takes the update history visible at a given replica and the arguments of a query and returns the result of the query. A specification is valid if for every reachable state and all queries a, the specification yields the same result as the application of the query to the current state: ∀ tr,pls,vs,a,r. s init tr -→ (pls, vs, ) ⇒ spec(H(tr, vs(r)), a) = query crdt (a, pls(r))

Here, the term H(tr, vs(r)) calculates the update history from the trace tr while only taking the operations before the version vs(r) into account.

Examples. Table 2 shows specifications for several CRDTs from the literature [START_REF] Shapiro | A comprehensive study of Convergent and Commutative Replicated Data Types[END_REF]. The Counter is a data type providing an update-operation to increment or decrement the value of the Counter and a query-operation Get() which returns the current value of the counter. The argument to the update is a single integer value. We specify the return value of a Get() operation on a counter by Two-Phase-Set (guarded remove):

spec(H, Contains(x)) = ∃e∈H.args(e) = Add(x) ∧ ¬(∃e∈H.args(e) = Remove(x) ∧ (∃ f ∈H. args(f ) = Add(x) ∧ f ≺ e))
Observed-Remove-Set:

spec(H, Contains(x)) = ∃a∈H.args(a) = Add(x) ∧ ¬(∃r∈H.a ≺ r ∧ args(r) = Remove(x))
Multi-Value-Register:

spec(H, Get()) = {x | ∃e∈H.args(e) = Set(x) ∧ ¬(∃ f ∈H. e ≺ f )}
Table 2. Specifications of CRDTs taking all update operations e from the update history H and then summing up their update arguments. The Grow-Set is a set which only allows adding elements. An element is in the set, when there exists an operation adding the element. The Two-Phase-Set also allows to remove elements from the set, with the limitation that an element cannot be added again once it was removed. An element is in the set, if there is an operation adding the element and no operation removing it. This specification allows removing an element before it was added to the set, which might not be desired. The Two-Phase-Set with the guarded remove operation, ignores remove operations, when the respective element is not yet in the set. For this data type, an element is in the set, when there exists an operation adding the element, and there is no operation which removes the element and which happened after an add operation of the same element. The Observed-Remove-Set is a set, where an element can be added and removed arbitrarily often. A remove operation only affects the add operations which have been observed, i.e. which happened before the remove operation. We specify that the query Contains(x) returns true, if and only if there exists an update operation a adding x to the set and there exists no update operation r which happened after a and removes x from the set. The final example is the Multi-Value-Register. It has a Set(x) operation to set the register to a single value. The Get() query returns a set containing the values of the last concurrent Set operations. More precisely, it returns all values x so that there exists an operation Set(x), for which no later update operation exists.

Properties and Discussion. It is not possible to describe non-converging data types with this technique. Since the specified return value of a query only depends on the visible update history and the arguments, two replicas which have seen the same set of updates will also return the same result. One problem with this specification technique is that in general a specification can reference all operations from the past. The state of a replica is basically determined by the complete update history, which can be quite large and not very abstract. Therefore it is hard to reason about the effects of operations when programming with the data types or when verifying properties about systems using them, where one usually wants to reason about the effect of a single method in a modular way.

Also, the example of the Two-Phase-Set with a guarded remove operation shows that small changes to the behavior of one update operation can make the whole specification more complex. We would like such a change to only affect the specification of the remove operation. Thus, the question is whether we can specify CRDTs avoiding these problems. We present and discuss an alternative specification technique in Section 6. It is also possible to use abstract implementations as a form of specification, as detailed in the next section.

Implementations

To implement a CRDT in our framework one has to define the type of the payload and the four fields of the CRDT record (init crdt , update crdt , merge crdt , query crdt ) as defined in the system model. Technically, the implementation can be any Isabelle function with a matching type.

To keep the examples short, we introduced a uid-function, which generates a new unique identifier. This can easily be implemented in our system model by adding a counter to the payload of the data type. A unique identifier can then be obtained by taking a pair (replicaId, counter) and incrementing the counter. It is also possible to use the version vector as a unique identifier for an update operation, which can make the verification easier, as the payload is then directly related to the update history. 3 shows two implementations of the Counter CRDT. The first implementation is an abstract one, in which the payload is a set of all update arguments tagged with a unique identifier. The query can then be answered by summing up all the update arguments in the set. This implementation is very inefficient, but easy to understand. The second implementation is closer to Counter implementations found in real systems. Here, the payload consists of two mappings from replicaIds to integers. The first map (p) sums up all the positive update operations per replica and the second map (n) sums up all the negative ones. While this is still one of the easier CRDTs, it is not trivial to see, that the optimized implementation is valid with respect to its specification. We will come back to this example in Section 5 and show how the correctness can be proven using our framework. Table 4 shows abstract implementations of the other CRDTs introduced in Section 3. The Grow-Set can be implemented using a normal set where the merge is simply the union of two sets. The payload of the Two-Phase-Set can be described by assigning one out of three possible states to each element. In a new, empty set all elements are in the init state. Once an element is added, it goes to the in state, and when it is removed it goes to the out state. The merge simply takes the maximum state for each element with respect to the order init < in < out. The last two CRDTs in Table 4 have a very similar implementation. This is not very surprising, as the Set operation of the register is basically an operation, that first removes all elements from the set and then adds a single new element. In both cases the payload consists of a set of elements tagged with an unique identifier and a set of tombstones, that contains all unique identifiers of the removed elements. The unique identifier makes sure, that the remove operation only affects previous add-operations, as it is demanded by the specification.

Relation to Specifications. All CRDT implementations can be specified by the specification technique described in Section 3, when the merge operation computes a least upper bound with respect to a semilattice and the update operations are increasing with respect to the order on the semilattice. This is possible, as the state can be reconstructed from a given update history, when the implementation is known. Because the merge operation of a CRDT computes a least upper bound, it is straight-forward to extend it to a merge function, which merges a set of payloads. Then a function to calculate the state can be defined recursively in terms of previous versions: If there is an update at the top of the history, apply the update operation to the merge of all previous versions. If there is no update operation at the top, just take the merge of all previous versions. This terminates, when the set of all previous versions only consists of the initial state.

The converse is also true: each specification given in this form describes a CRDT. A specification can be turned into an inefficient implementation by storing the visible update history in the payload of the data type. The update history is just a growing set which can be merged using the union of sets, thus forming a semilattice.

Verification

In our work on verification of CRDTs we considered two properties. The first property is the convergence of a CRDT, meaning that two replicas, which have received the same set of updates, should return the same results for any given query. This property is common to all CRDTs and does not require any further specification. The second property is the behavior of a CRDT, i.e. we want to prove, that a specification as presented in Section 3 is valid for a given implementation. As we discussed earlier, this is a strictly stronger property, but it requires a specification for each data type.

Section 5.1 covers the verification of the convergence property, in Section 5.2 we present a technique for verifying the behavior, and in Section 5.3 we evaluate our experience in using Isabelle/HOL for the verification of CRDTs with the presented techniques.

Verification of Convergence

The convergence property can be verified by proving that the payload of the CRDT forms a semilattice, such that the merge-operation computes a least upper bound and the update-operations increase the payload with respect to the order on the semilattice. [START_REF] Shapiro | A comprehensive study of Convergent and Commutative Replicated Data Types[END_REF] (refl)

Inv(H, pl) ⇒ pl ≤ crdt pl (trans) Inv(H1, pl1) ∧ Inv(H2, pl2) ∧ Inv(H3, pl3)∧ pl1 ≤ crdt pl2 ∧ pl2 ≤ crdt pl3 ⇒ pl1 ≤ crdt pl3 (antisym) Inv(H1, pl1) ∧ Inv(H2, pl2) ∧ pl1 ≤ crdt pl2 ≤ crdt pl1 ⇒ pl1 = pl2 (commute) Inv(H1, pl1) ∧ Inv(H2, pl2) ⇒ merge crdt (pl1, pl2) = merge crdt (pl2, pl1) (upper bound) Inv(H1, pl1) ∧ Inv(H2, pl2) ⇒ pl1 ≤ crdt merge crdt (pl1, pl2) (least upper bound) Inv(H1, pl1) ∧ Inv(H2, pl2) ∧ Inv(H3, pl3)∧ pl1 ≤ crdt pl3 ∧ pl2 ≤ crdt pl3 ⇒ merge crdt (pl1, pl2) ≤ pl3
(monotonic updates) Inv(H, pl) ⇒ pl ≤ crdt update crdt (args, r, pl)

Table 5. Verifying convergence of CRDTs

However, only very simple data types form a semilattice in the classical mathematical sense. Often the semilattice properties only hold for a subset of the payloads. For some states which are theoretically representable by the payload type, but are never reached in an actual execution, the semilattice properties sometimes do not hold. In theory it could even be the case that there are two reachable states for which the merge operation does not yield the correct result, but where the two states can never be reached in the same execution. However, for the examples we considered it was always sufficient to restrict the payload to exclude some of the unreachable states. Technically, this was done by giving an invariant Inv over the update history H and the payload pl. The same type of invariant will also be used for the verification of behavioral properties in the next section. In the examples we considered, it was not necessary to use the update history H in the invariant. An overview of the sufficient conditions for convergence, which we used, is given in Table 5. The order on the payloads is denoted by ≤ crdt .

In order to verify these conditions for the Counter CRDT, we have to define the order on the payloads. Here we can simply compare the mappings for each replicaId: (p, n) ≤ (p , n ) ↔ ∀ r p(r) ≤ p (r) ∧ n(r) ≤ n (r). An invariant is not required for this example and the proof of the semilattice conditions can be done mainly automatically by Isabelle/HOL. In fact, for all the easier examples, it was possible to do the majority of the proofs with the automated methods provided by Isabelle/HOL (sledgehammer, auto, . . . ).

Verification of Behavior

For the verification of behavioral properties we have developed a small framework, which simplifies the verification and provides two general strategies for verifying a CRDT. The first strategy basically is an induction over the traces. The idea of the second strategy is to show that a CRDT behaves equivalently to

The invariant must hold initially:

Inv({}, initial crdt )
Merges must preserve the invariant:

∀ H 1 ,H 2 ,pl 1 ,pl 2 valid(H1) ∧ valid(H2) ∧ Inv(H1, pl1) ∧ Inv(H2, pl2)
∧ consistent(H1, H2) ⇒ Inv(H1 ∪ H2, merge crdt (pl1, pl2))

Updates must preserve the invariant:

∀ H,pl,r,v,args valid(H) ∧ Inv(H, pl) ∧ v = sup v (H) ⇒ Inv(H ∪ {(v(r := v(r) + 1), r, args)}, update crdt (args, r, pl))
The invariant must imply the specification:

∀ H,pl,qa valid(H) ∧ Inv(H, pl) ⇒ query crdt (qa, pl) = spec(H, qa)
Table 6. Verifying behavior of CRDTs another CRDT which has already been verified. In this paper we only present the first strategy. When using this strategy, one has to provide an invariant between the payloads and the visible update history. It then has to be shown that the invariant implies the specification, that the invariant holds for the initial payload with the empty update history, and that the invariant is maintained by update-and merge-operations. Table 6 shows the four subgoals.

For both operations our framework provides basic properties about valid update histories (predicate valid), which hold for all CRDTs. Because we used version vectors for representing the visibility relation, it is not necessary to specify the partial order properties of the relation, but instead it is necessary to specify constraints for the version vectors. The most important property is that the updates on one replica form a total order where the local component of the version vector is always increased by one and the other components increase monotonically. Other properties describe the causality between version vectors in more detail and can be found in [START_REF] Zeller | Specification and Verification of Convergent Replicated Data Types[END_REF].

In the case of an update operation one has to show that the invariant is maintained when adding a new update to the top of the update history, meaning that all other updates are visible to the new update. In a real execution this is usually not the case, but the framework can still do this abstraction step, because updates which are not visible do not influence the new update.

In the case of a merge operation one can assume that the invariant holds for two compatible update histories with two corresponding payloads, and then has to show that the invariant also holds for the union of the two update histories with the merged payload. Two update histories are compatible, when for each replica, the sequence of updates on that replica in one update history is a prefix of the sequence of updates in the other update history.

To verify the counter example we used the following invariant:

Inv(H, (p, n)) ↔ ∀ r p(r) = {x|∃ v (v, r, x) ∈ H ∧x ≥ 0}∧n(r) = {-x|∃ v (v, r, x) ∈ H ∧x < 0}.
For proving, that a merge-operation preserves the invariant, we have to use the property of compatible histories. From this property we get, that for any replica r, we either have

{x|∃ v (v, r, x) ∈ H ∧ x ≥ 0} ⊆ {x|∃ v (v, r, x) ∈ H ∧ x ≥ 0}
or the other way around. This combined with the fact, that all elements are positive, ensures that calculating the maximum yields the correct result. The other parts of the verification, namely update-operations, the initial state and the connection between the invariant and the specification, are rather trivial on paper, whereas in Isabelle the latter requires some work in transforming the sums.

Evaluation

We used the interactive theorem prover Isabelle/HOL [START_REF] Nipkow | Isabelle/HOL -A Proof Assistant for Higher-Order Logic[END_REF] for the verification of several important CRDTs. To this end, we manually translated the pseudocode implementations from the literature [START_REF] Shapiro | A comprehensive study of Convergent and Commutative Replicated Data Types[END_REF][START_REF] Bieniusa | An optimized conflict-free replicated set[END_REF] into Isabelle functions, and then verified those implementations. The verified CRDTs are the Increment-Only-Counter, PN-Counter, Grow-Set, Two-Phase-Set, a simple and an optimized OR-Set implementation, and a Multi-Value-Register. The theory files are available on GitHub 1 .

For the simple data types, the semilattice properties were mostly automatically proved by Isabelle/HOL. For the more complicated data types, like the optimized OR-Set or the similarly implemented MV-register, a suitable invariant had to be found and verified first, which required more manual work in the proofs.

Verifying the behavior of the data types was a more difficult task. Finding a suitable invariant has to be done manually, and the invariant has to be chosen such that it is easy to work with it in Isabelle/HOL. Proving that the invariant is maintained also requires many manual steps, as it usually requires some data transformations which can not be handled automatically by Isabelle/HOL.

We found two small problems, while verifying the CRDTs mentioned above:

-When trying to verify an implementation of the OR-set based on figure 2 in [START_REF] Bieniusa | An optimized conflict-free replicated set[END_REF], we found a small problem in our translation of this implementation to Isabelle. In the original description the remove-operation computes the set R of entries to be removed with the formula R = {(e, n)|∃n : (e, n) ∈ E}. When this expression is translated to Isabelle code in a direct way, one obtains an equation like R = {(e, n). ∃n.(e, n) ∈ E}. Then R will always contain all possible entries, because in Isabelle e and n are new variables, and e does not reference the parameter of the function as intended. This problem can be easily fixed, and was not a real issue in the original description, but rather a mistake made in the translation to Isabelle, which happened because of the different semantics of the pseudo-code used in the original description and Isabelle.

1 https://github.com/SyncFree/isabelle_crdt_verification -We discovered another small problem with the MV-Register presented in specification 10 from [START_REF] Shapiro | A comprehensive study of Convergent and Commutative Replicated Data Types[END_REF]. This MV-register is slightly different from the one described in the previous sections, as its assign operation allows to assign multiple values to the register in one step. The problem is in the assign function. When the assigned list of elements is empty, the payload will also be empty after the operation. This is a problem, because all information about the current version is lost. It thus violates the requirement that updates monotonically increase the payload and it can lead to inconsistent replicas. As an example consider the following sequence of operations executed on replica 1:

{(⊥, [0, 0])} Assign({a}) --------→ {(a, [1, 0])} Assign({b}) -------→ {(b, [2, 0])} Assign({}) -------→ {} Assign({c})
-------→ {(c, [1, 0])}. Furthermore assume that replica 2 first merges the payload {(b, [2, 0])} and then the payload {(c, [1, 0])}. Then all updates have been delivered to both replicas, but the payload of replica 1 is {(c, [START_REF] Bieniusa | Brief announcement: Semantics of eventually consistent replicated sets[END_REF]0])} and the payload of replica 2 is {(b, [START_REF] Bieniusa | An optimized conflict-free replicated set[END_REF]0])}. This problem can be easily fixed by disallowing the assignment of an empty set or by storing the current version in an extra field of the payload.

Alternative Specifications

We have already seen two specification techniques: specifications based on the complete update history, and abstract implementations, which are a kind of state-based specifications. Another specification technique was sketched in [START_REF] Bieniusa | Brief announcement: Semantics of eventually consistent replicated sets[END_REF]. In this section we discuss and formalize the technique.

The technique is a state-based one, and uses the notation of pre-and postconditions to specify the effect of operations on the state. Using the technique of pre-and post-conditions, a sequential specification can be given as a set of Hoaretriples. The Hoare-triple {P }op{Q} requires that Q should hold after operation op whenever P was true before executing the operation.

For example, the increment operation of a counter can be specified by the triple {val() = i} inc(x) {val() = i + x} and similarly a set is specified using triples like {true} add(e) {contains(e)}. Such a sequential specification is applicable to replicated data types if there is no interaction with other replicas between the pre-and post-condition.

In such cases, the replicated counter and the Observed-Remove-Set behave exactly as their corresponding sequential data type. For the Two-Phase-Set this is not true, since an add-operation does not guarantee that the element is in the set afterwards. There are examples like the Multi-Value-Register, where no corresponding and meaningful sequential data type exists, but for replicated data types which try to mimic sequential data types, it is a desirable property to maintain the sequential semantics in time spans where there are no concurrent operations, i.e. where the visibility relation describes a sequence.

In [START_REF] Bieniusa | Brief announcement: Semantics of eventually consistent replicated sets[END_REF] those sequential specifications are combined with concurrent specifications, that describe the effect of executing operations concurrently. The concurrent specification is written in a similar style as the sequential specification.

Instead of only a single operation it considers several operations of the following form executed in parallel: {P }op 1 op 2 • • • op n {Q}. The informal meaning is that if P holds in a state s, then executing all operations on s independently and then merging the resulting states should yield a state where Q holds.

Formally, we define a triple {P }op 1 op 2 ---------------------→ (pls , vs , ph ) ∧ ∀ i∈{1,...,n} pls(r i ) = pls(r 1 ) ∧ P (pls(r 1 )) ⇒ Q(merge crdt (pls (r 1 ), . . . , pls (r n )))

If we reach a state (pls, vs, ph) where the payload on the replicas r 1 to r n are equal and satisfy the pre-condition P , then executing each operation op i on replica r i yields a state (pls , vs , ph ) where the post-condition Q holds for the merged payload of replicas r 1 to r n .

Obviously, one can only specify a subset of all possible executions using this specification techniques. The advantages of this technique is that it is more modular and thus better composable than the technique introduced in Section 3, and that it is easier to see the sequential semantics of the data type. Also, there is the principle of permutation equivalence [START_REF] Bieniusa | Brief announcement: Semantics of eventually consistent replicated sets[END_REF], which can be applied to this technique very easily, and is a good design guideline for designing new CRDTs.

Related Work

Burckhardt et al. [START_REF] Burckhardt | Replicated data types: specification, verification, optimality[END_REF] worked on verifying the behavioral properties of CRDTs. Their techniques are very similar to ours, but they have not used a tool to check their proofs. Their formal system model is more general than ours, as it supports timestamps and visibility relations which are not partial orders.

Bouajjani et al. [START_REF] Bouajjani | Verifying eventual consistency of optimistic replication systems[END_REF] present a specification technique which is based on the history of updates with the visibility relation. They obtain a more flexible system model by allowing the partial order to be completely different for different operations. This allows them to cover a wide selection of optimistic replication systems, in particular ones that use speculative execution. In contrast to our work, they use an algorithmic approach to reduce the verification problem to model-checking and reachability.

The only other work we are aware of which uses a theorem prover to verify CRDTs is by Christopher Meiklejohn. Using the interactive theorem prover Coq, the semilattice properties of the increase-only-counter and the PN-counter CRDTs [START_REF] Meiklejohn | Distributed data structures with Coq[END_REF] are verified. Unlike our work, the behavioral properties of CRDTs are not considered and the verification is not based on a formal system model.

Conclusion and Future work

In this paper, we have presented a formal framework for the analysis and verification of CRDTs. As the case studies have shown, it is feasible to verify CRDTs with Isabelle/HOL. The problem found in the MV-register during verification shows that it is easy to miss some corner case when designing a CRDT. The verified CRDTs were given in pseudo-code and then translated to Isabelle, which is a very high level language. Real implementations of the same CRDTs will probably be more complex, and thus the chance of introducing bugs might be even higher. But also the amount of work required for verifying a real implementation is higher.

It is an open question if more research into the automated verification and testing of CRDTs is required. This depends on how applications will use CRDTs in the future. For sequential data types, it is often sufficient to have lists, sets, and maps for managing data, as can be seen in commonly used data formats like XML or JSON. In the case of CRDTs, more data types are required, because different applications require different conflict resolution behavior. This could be very application specific. For example, an application could require a set where add-operations win over remove-operations, but when a remove-operation is performed by an administrator of the system, then that operation should win. If every application needs its own CRDTs, then automatic tools to auto-generate correct code might be a good idea.

In future work, we want to extend the specification techniques presented in this paper for reasoning about applications using CRDTs. Such large-scale distributed applications are usually long-running and should be stable, but are difficult to maintain. It is therefore of special interest to have a stable and correct code base.

  Counter: spec(H, Get()) = e∈H. args(e) Grow-Set: spec(H, Contains(x)) = ∃e∈H.args(e) = Add(x) Two-Phase-Set: spec(H, Contains(x)) = ∃e∈H.args(e) = Add(x) ∧ ¬(∃e ∈ H. args(e) = Remove(x))

  (id × int)set = {} update(x, r, s) = s ∪ {(uid(), x)} merge(s, s ) = s ∪ s query(Get(), s) = (id,x)∈s x Optimized Counter:s :: (replicaId → int) × (replicaId → int) = (λr. 0, λr. 0) update(x, r, (p, n)) = if x ≥ 0 then (p(r := p(r) + x), n)else (p, n(r := n(r) -x)) merge((p, n), (p , n )) = (λr. max(p(r), p (r)), λr. max(n(r), n (r))) query(Get(), (p, n)) = r p(r)r n(r)

  Grow-Set:s :: a set = {} update(Add(x), r, s) = s ∪ {x} merge(s, s ) = s ∪ s query(Contains(x), s) = x ∈ s Two-Phase-Set:s :: a ⇒ {init = 0, in = 1, out = 2} = (λx. init) update(Add(x), r, s) = (if s(x) = init then s(x := in) else s) update(Rem(x), r, s) = s(x := out) merge(s, s ) = (λx. max(s(x), s (x))) query(Contains(x), s) = (s(x) = in) Two-Phase-Set (guardedremove): Same as above, but with different remove operation: update(Rem(x), r, s) = (if s(x) = in then s(x := out) else s) Observed-Remove-Set: s.e :: (id × a)set = {}, s.t :: id set = {} update(Add(x), r, s) = s(e := s.e ∪ {(uid(), x)}) update(Rem(x), r, s) = s(t := s.t ∪ {id|∃x.(id, x) ∈ s.e}) merge(s, s ) = (e = s.e ∪ s .e, t = s.t ∪ s .t) query(Contains(x), s) = ∃ id .(x, id) ∈ s.e ∧ id / ∈ s.t Multi-Value-Register: s.e :: (id × a)set = {}, s.t :: id set = {} update(Set(x), r, s) = s(e := {(uid(), x)}, t := s.t ∪ {id|∃x.(id, x) ∈ s.e}) merge(s, s ) = (e = s.e ∪ s .e, t = s.t ∪ s .t) query(Get(), s) = {x|∃ id .(x, id) ∈ s.e ∧ id / ∈ s.t}Table 4. State-based specifications of CRDTs

Table 3 .

 3 Abstract and optimized implementation of a Counter CRDT

Table

  • • • op n {Q} to be valid, if the following condition is met: ∀ tr,pls,vs,ph,pls ,vs ,ph ,r1,...,rn,op1,opn : s init

		tr -→ (pls, vs, ph)
	∧ (pls, vs, ph)	Update(r1,op1);...;Update(rn,opn)

Acknowledgement. This research is supported in part by European FP7 project 609 551 SyncFree