Dimitris Mostrous

Vasco Thudichum Vasconcelos

Affine Sessions

Session types describe the structure of protocols from the point of view of each participating channel. In particular, the types describe the type of communicated values, and also the dynamic alternation of input and output actions on the same channel, by which a protocol can be statically verified. Crucial to any term language with session types is the notion of linearity, which guarantees that channels exhibit exactly the behaviour prescribed by their type. We relax the condition of linearity to that of affinity, by which channels exhibit at most the behaviour prescribed by their types. This more liberal setting allows us to incorporate an elegant error handling mechanism which simplifies and improves related works on exceptions. Moreover, our treatment does not affect the progress properties of the language: sessions never get stuck.

Introduction

A session is "a semantically atomic chain of communication actions which can interleave with other such chains freely, for high-level abstraction of interactionbased computing" [START_REF] Takeuchi | An interaction-based language and its typing system[END_REF]. Session types capture this intuition as a description of the structure of a protocol, in the simplest case between two programs (binary sessions). This description consists of types that indicate whether a communication channel will next perform an output or input action, the type of the value to send or receive, and what to do next, inductively. For example, !nat.!string.?bool.end is the type of a channel that will first send a value of type nat, then one of type string, then wait for a value of type bool, and nothing more. This type can be materialised by the π-calculus [START_REF] Milner | A calculus of mobile processes, parts I and II[END_REF] process a5.a "hello".a(x).0. To compose two processes that communicate over a channel, we require that each has a complementary (or dual) type, so that an input will match an output, and vice versa. The dual of the previous type is ?nat.?string.!bool.end, and can be implemented by a(x).a(y).a(x + 1 < 2).0. To ensure that the actions take place in the prescribed order, session typing relies crucially on the notion of linearity [START_REF] Girard | Linear logic[END_REF], which means that a causal chain can be assumed. To see why, imagine that we write the first process as a5.0 | a "hello".a(x).0. Now we cannot determine which output can react first, and the second process can receive a "hello" first, which would clearly be unsound and would most likely raise an error.

Beyond the basic input/output types, sessions typically provide constructors for alternative sub-protocols, which are very useful for structured interaction. For example, & {go : T 1 , cancel : T 2 } can be assigned to an (external) choice a {go.P 1 cancel.P 2 }. The dual type, where T denotes T with an alternation of all constructors, is ⊕ go : T 1 , cancel : T 2 , and corresponds to a process that will make a (internal) choice, either a go.Q 1 or a cancel.Q 2 . In the first case the two processes will continue as P 1 and Q 1 , respectively.

As can be seen, sessions are very suitable as a static verification mechanism for interacting programs. However, they are also quite rigid, since everything in the description of a session type must be implemented by a program with that type. Indeed, in many real world situations, interactions are structured but can be aborted at any time, for example an online store should be prepared for clients that get disconnected, that close their web browsers, or for general errors that abruptly severe the expected pattern of interaction.

In this work, we address the above issues. In technical terms, we relax the condition of linearity to that of affinity, inspired by Affine Logic (which is the variation of Linear Logic with unrestricted weakening; see [START_REF] Asperti | Intuitionistic light affine logic[END_REF] for an introduction), and this allows processes to terminate their sessions prematurely. However, a naive introduction of affinity can leave programs in a stuck state: let us re-write the first process into a5.a "hello".0, i.e., without the final input; then, after two communications the dual process will be stuck trying to perform a(5 + 1 < 2).0. One of the basic tenets of sessions, progress, is now lost. Actually, the study of Proof Nets for Affine Logic [START_REF] Asperti | Intuitionistic light affine logic[END_REF] reveals that weakening is not, and should not be, invisible. In particular, there exists a device that will perform the weakening step by step, progressing through the dependencies of a proof, and removing all that must be removed. This is exactly what we need in order to handle an abrupt termination of an interaction in an explicit way, and we denote it by a , which reads cancel a. Now we can write a5.a "hello".a , and after two steps against the dual process we obtain a(5 + 1 < 2).0 | a , which results in the cancellation of the output (and in general, of any subsequent actions on a). We take this idea a step further: if cancellation of a session is explicit, we can treat it as an exception, and for this we introduce a do-catch construct that can provide an alternative behaviour activated when a cancellation is encountered. For example, we can write do a(5 + 1 < 2).0 catch P , and a composition with a will replace a(5 + 1 < 2).0 with the exception handler P . A do-catch is not the same as the try-catch commonly found in sequential languages: it does not define a persistent scope that captures exceptions from the inside, but rather it applies to the first communication and is activated by exceptions from the outside (as in the previous example). Thus, do a(5 + 1 < 2).0 catch P in parallel to a(x).0 becomes 0, because the communication was successful.

Affine Sessions by Example

We describe a simple interaction that implements a book purchase taking place between three processes, Buyer, Seller, and Bank. The buyer sends the title of a book, receives the price, and makes a choice to either buy it or cancel. If the buyer chooses to buy the book, the credit card is sent over the session, and the buyer is informed whether or not the transaction was successful. The diagram in Figure 1 shows the interactions of a specific purchase. We now show how this scenario can be implemented using sessions, and how our treatment of affinity can be used to enable a more concise and natural handling of exceptional outcomes. Our language is an almost standard π-calculus where replication is written acc a(x).P and plays the role of "accept" in sessions terminology [START_REF] Honda | Language primitives and type disciplines for structured communication-based programming[END_REF]. Dually, an output that activates a replication is written req ab.P , and is called a "request". We will use some standard contructs that are encodable in π-calculus, like ae for an expression e. Also, we use if t then P else Q that can be implemented by a new session, specifically a {true.P false.Q} against some process representing the test t that communicates the result by a selection of one of the labels, a true or a false.

An implementation of the protocol we described in Figure 1 is shown below: First we note how sessions are established. For example, in Buyer the fresh name b is sent to Seller via the request req seller b, where it will substitute s in a copy of the replication, and it appears also locally. These are the two endpoints of the session, and it is easy to check that the interactions match perfectly. Another point is the "borrowing" of the session b (which becomes identified with s) from Seller to Bank, with cs.c(r) and k(r).r(card).kr (again, c and k are identified), respectively, so that the credit card is received directly by Bank; see also Figure 1.

Buyer . = (
A more robust variation of Seller could utilise the do-catch mechanism to account for the possibility of the Bank not being available (or being crashed), by providing an alternative payment provider. This can be achieved if we substitute req bank c with do req bank c catch req paymate c, so that a failure to use the bank service (bank ) will activate req paymate c (which must have the same type) and the protocol has a chance to complete successfully.

The Buyer might also benefit from our notion of exception handling. For example, we show an adaptation that catches a cancellation at the last communication of the buy branch and prints an informative message:

BuyerMsg . = (νb)       req seller b | b "
     
As mentioned in the Introduction, a do-catch on some communication does not catch subsequent cancellations. For instance, if in the above example the do-catch was placed on b "Proofs and Types", then any b generated after this output was performed would be uncaught, since reqprint "Error 42" would have been already discarded. However, a do-catch does catch cancellations emitted before the point of definition, so placing it near the end of a protocol is very useful if we just want a single exception handler that catches everything.

Indeed, exception handlers that persist for the lifetime of the whole session are definable. Specifically, we can write try P catch (b : Q) to mean that one endpoint of b is implemented in P and that Q should be activated if b is canceled at any point from the outside of P . This try-catch notation translates to a do-catch on the last prefix on b in P , in multiple branches as required, assuming that b is not delegated (i.e., sent over another channel), as is the case in BuyerMsg. 1 Then we have, for example, that try b5.P catch (b : Q) | b(x).0 becomes try P catch (b : Q) and try b5.P catch (b : Q) | b becomes P | Q where P is P with b and all its dependencies canceled. In general, however, our mechanism is very finegrained, and a single session can have multiple, nested do-catch on crucial points of communication.

Note also that a can be very useful in itself, even without the do-catch mechanism. Here are two ways to implement a process that starts a protocol with Seller only to check the price of a book: Both the above processes can be typed. However, the first requires a knowledge of the protocol, which in that case includes an exit point (branch cancel), while the second is completely transparent. For example, imagine a buyer that selects buy by accident and then wishes to cancel the purchase: without cancellation it is impossible because it is not predicted by the session type; with cancellation it is extremely simple, as shown below.

CheckPriceA . = (
BuyerCancel . = (νb) req seller b | b "Gödel, Escher, Bach".b(price).b buy.b
We now make a small digression to discuss how our affine sessions can be encoded in standard sessions. The purpose is to shed light on the complexity that is required, which motivates even more our development. First of all, it is possible that both endpoints of a session emit a cancellation, possibly at different moments. Therefore, if we are to encode this behaviour in a standard session system, we must allow a protocol to end at any point and by the request of either of the participants. This can be achieved by an exchange of a decision, to go or to cancel, by both endpoints, before all communications. We show the translation for output and input; the rest is similar.

!T 1 .T 2 . = ⊕ go : & {go : !T 1 . T 2 , cancel : end} , cancel : & {go : end, cancel : end} ?T 1 .T 2 . = !T 1 .T 2 end . = end
The notable point is that by an alternation of constructors we obtain a translation that preserves duality, and it is easy to check that it preserves soundness. Moreover, the only way to proceed is if both ends agree to go. The term-level translation follows the structure of the types, and a becomes a cancel. All free sessions in the term must be canceled in the branches that do not result in normal execution so as to obtain the same typing environment, but this is always possible. The above translation only handles cancellation. Our do-catch mechanism can also be encoded within the branches of the previous translation, but it becomes quite complicated due to the typing contraints that must be respected. In any case, we think it is obvious that the burden is heavy if one wishes to obtain a functionality as general as the one available in the affine system, and types would become completely illegible from the multiplication of constructors.

The Process Calculus of Affine Sessions

Syntax Our language is a small extension of standard π-calculus [START_REF] Milner | A calculus of mobile processes, parts I and II[END_REF]. With respect to standard sessions systems [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF][START_REF] Vasco | Fundamentals of session types[END_REF], we avoid the need for polarities and double binders by carefully introducing a logically-founded typing principle, detailed later. For technical convenience we shall consider all indexing sets I to be totally ordered, so that we can speak, e.g., of the maximum element. Also for technical convenience, we separate the prefixes denoted by ρ, i.e., all communication actions except for accept (replication). We only added two nonstandard constructs: the cancellation a and the do-catch construct that captures a cancellation, denoted by do ρ catch P . Notice that we restricted the action to a prefix in ρ, but this is not so limiting. In the case of replication, it does not make sense to catch an event that never occurs, since as we shall see we never explicitly cancel a persistent service. For parallel composition, it would be ambiguous to allow do (P | Q) catch R since more than one action can be active in (P | Q), and moreover we do not think it would really add any benefit since we can add a separate do-catch for each session. Similarly, do a catch P would be strange: it would allow to trigger some behaviour when the other end is canceled, but while at the same time the protected session is canceled too. It can be added if a good use is discovered, but we preferred to keep the semantics simpler.

ρ ::= a(x : T ).P (input)

| ab.P (output) | a {l i .P i } i∈I (branching) | a l k .P (selection)
| req ab.P (request)

P ::= ρ (prefix)
| acc a(x : T ).P (replicated accept)

| 0 (nil)

| P | Q (parallel) | (νa : T )P (restriction) | a (cancel) | do ρ catch P (catch)
Structural Congruence With ≡ we denote the least congruence on processes that is an equivalence relation, equates processes up to α-conversion, satisfies the abelian monoid laws for parallel composition, the usual laws for scope extrusion, and satisfies the axiom:

(νa : T )(a | • • • | a ) ≡ 0
We added this axiom mainly for the left-to-right direction which allows "leftover" cancellations to disappear; this is convenient for technical reasons.

Reduction We use two kinds of contexts, C[ ] which are standard, and H[ ] for (possible) exception handling, defined below.

Standard Contexts : C[ • ] ::= • | ( C[ • ] | P ) | (νa : T ) C[ • ] Do-Catch Contexts : H[ • ] ::= • | do • catch P
Reduction is defined in two parts, first the standard rules, and then the cancellation rules. The standard reductions are defined below:

H 1 [ ab.P ] | H 2 [ a(x : T ).Q ] -→ P | Q{ b /x} (R-Com) H 1 [ a l k .P ] | H 2 [ a {l i .Q i } i∈I ] -→ P | Q k (k ∈ I) (R-Bra) H[ req ab.P ] | acc a(x : T ).Q -→ P | Q{ b /x} | acc a(x : T ).Q (R-Ses) P ≡ P -→ Q ≡ Q ⇒ P -→ Q (R-Str) P -→ Q ⇒ C[ P ] -→ C[ Q ] (R-Ctx)
The only notable point is that we discard any do-catch handlers, since there is no cancellation, which explains why the H-contexts disappear.

The cancellation reductions follow:

req ab.P | a -→ a | b | P (C-Req) ab.P | a -→ a | b | P (C-Out) a(x : T ).P | a -→ (νx : T )(a | x | P ) (C-Inp) a l k .P | a -→ P | a (C-Sel) a {l i .P i } i∈I | a -→ P k | a max(I) = k (C-Bra) do ρ catch P | a -→ P | a subject(ρ) = a (C-Cat)
We discuss some notable points.

Only what is strictly needed will be deleted, in particular one might have expected a(x : T ).P | a to result in the annihilation of P , which can be done by generating b for each b in the free names of P . However, this has several drawbacks: first, it is too absolute, since some interactions in P may not depend on a or x, and we prefer to preserve them; second, it is technically simpler, since in this setting we can use typing restrictions to avoid the creation of any b for a replication acc b(x).Q inside P , which follows our decision to never delete services; finally, it is what happens in Proof Nets for Affine Logic (see [START_REF] Asperti | Intuitionistic light affine logic[END_REF]).

In the cancellation of branching, (C-Bra), we choose the maximum index k which exists by our assumption that index sets are totally ordered. This is a simple way to avoid non-determinism solely by cancellation. 2 Notice that it follows the pattern of activating a continuation, motivated above.

In the rule (C-Cat), we use a function subject(ρ) which returns the subject in the prefix of ρ. This is defined in the obvious way, e.g., subject(ab.P ) = subject(req ab.P ) = a, and similarly for the other cases. The typing system will ensure that a does not appear in P , so it is ok to leave a in the result; this is needed for canceled requests, where the a should remain until it reacts with all of them.

We clarify some of the main points:

i) Consider a(x).( Q | acc b(z).R ) | a .
The replication provided on b may or may not depend on x. A cancellation of a does not necessarily mean that b will be affected, but if x appears in R it is possible that subsequent sessions will be canceled. ii) Consider a(x).( acc x(z).Q | bx.R ) | a . As can be seen, the replicated channel x is delegated on b, and it should not be deleted just because a is canceled. Indeed, this situation is not allowed by the restrictions in our type system. In other words, some sessions cannot be canceled. iii) Consider a(x).( Q | be.R ) | a . The session output be.R will not be canceled, but since it is possible that e = x and in general e could appear in R, other cancellations may eventually be generated. iv) A communication discards any handlers: do ab.P catch Q | a(x : T ).R -→ P | R{ b /x}. The type system ensures that it is sound to discard Q, since it contains the same sessions as ab.P , except for a. v) A cancellation activates a handler, which may provide some default values to a session, completing it or eventually re-throwing a cancellation, as in:

do ab.P catch (b5.b ) | a -→ b5.b | a .

Typing Affine Sessions

Types The session types we use are standard [START_REF] Honda | Language primitives and type disciplines for structured communication-based programming[END_REF] with two exceptions. First, following [START_REF] Vasco | Fundamentals of session types[END_REF] we allow a session type to evolve into a shared type. Second, we decompose shared types into accept types acc T and request types req T , following the logical principles of Affine Logic. Technically, acc T corresponds to !T ("of course T ") and req T to ?T ("why not T ") [START_REF] Girard | Linear logic[END_REF]. This has several technical advantages that simplify our development, for example acc T retains information on the persistence of a term with that type, since it must be replicated, which is useful for typing. Moreover, req T is the only type allowed in the context of a resource that can be used zero or more times.

T ::= end (nothing)

| !T.T (output) | ?T.T (input) | ⊕ {l i : T i } i∈I (selection) | & {l i : T i } i∈I (branching) | req T (request) | acc T (accept)
Duality The two ends of a session are composed when their types are dual, which is defined as an involution over the type constructors, similarly to Linear Logic's negation except that end is self-dual.

3 !T 1 .T 2 . = ?T 1 .T 2 ?T 1 .T 2 . = !T 1 .T 2 ⊕ {l i : T i } i∈I . = & l i : T i i∈I & {l i : T i } i∈I . = ⊕ l i : T i i∈I req T . = acc T acc T . = req T end . = end
Typing Rules Typing judgements take the form: P Γ where Γ ::= ∅ | Γ, a : T meaning that term P has interface Γ . We shall also use Γ , ∆, Θ for interfaces.

We restrict replications to be unique, but allow multiple requests to take place against them. This means that processes can have multiple uses of a : req T , which corresponds to the logical principle of contraction. For this, we make use of the splitting relation from [START_REF] Vasco | Fundamentals of session types[END_REF]:

∅ = ∅ • ∅ Γ = Γ 1 • Γ 2 Γ, a : req T = (Γ 1 , a : req T ) • (Γ 2 , a : req T ) Γ = Γ 1 • Γ 2 Γ, a : T = (Γ 1 , a : T ) • Γ 2 Γ = Γ 1 • Γ 2 Γ, a : T = Γ 1 • (Γ 2 , a : T )
In the typing rules, req Γ stands for an interface of the shape a 1 : req T 1 , . . . , a n : req T n . Similarly, end Γ stands for an interface a 1 : end, . . . , a n : end.

We also define a predicate no-requests(T ), used to forbid any request type from appearing in the type of a , since this maps by duality to the deletion of a persistent accept on the other side, which we do not allow. 4no-requests(req T ) = false no-requests(acc T ) = no-requests(T ) no-requests(end) = true no-requests(!T 1 .T 2 ) = no-requests(T 1 ) ∧ no-requests(T 2 )

no-requests(?T 1 .T 2 ) = no-requests(T 1 ) ∧ no-requests(T 2 )

no-requests(⊕ {l i :

S i } i∈I ) = no-requests(& {l i : S i } i∈I ) = ∧ i∈I no-requests(S i )
The typing rules are presented in Figure 2. We focus on some key points. First, we type modulo structural equivalence, a possibility suggested by [START_REF] Milner | Functions as processes[END_REF] and used in [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF]. This is because associativity of " | " does not preserve typability, i.e., a composition between P and (Q | R) may be untypable as (P | Q) | R; see

P Γ1 Q Γ2 P | Q Γ1 • Γ2 (ParSes) P Γ1, a : acc T Q Γ2, a : req T P | Q (Γ1 • Γ2), a : acc T (Res) P Γ1, a : T Q Γ2, a : T (νa : T )(P | Q) Γ1 • Γ2 (Str) Q Γ Q ≡ P P Γ (Nil) 0 req Γ, end ∆ (Catch) ρ Γ, a : T P Γ subject(ρ) = a do ρ catch P Γ, a : T (Cancel) no-requests(T )
a a : T Fig. 2. Affine Session Typing (ParSes), (Res). This applies also to (νa) that causes similar problems. In fact, the splitting of the terms in (Res) is inspired by the work [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF] which interprets sessions as propositions in a form of Intuitionistic Linear Logic. It is because of this separation of terms, which applies also to (ParSes), that we can avoid channel polarities: the two ends of a session can never become causally dependent or intermixed. The purpose of (ParSes) is to type multiple requests against a persistent accept, which explains why a : acc T remains in the conclusion. An output ab.P records a conclusion b : T 1 , so in fact it will compose against b : T 1 . Therefore !T 1 .T 2 really means "send T 1 ," which matches with the dual input.

A cancellation a can be given any type that does not contain a request, as explained previously.

A do-catch is typed as follows: if ρ is an action on a and has an interface Γ, a : T , then the handler P will implement Γ , i.e., all sessions of ρ except for a : T which has been canceled. Of course, inside P these other sessions can be canceled anyway, which corresponds to "re-throwing" the cancellation, but they can also be implemented in whole or in part. The rule is sound, since no session is damaged, irrespectively of which term we execute, ρ or P .

Motivating the "no requests" restriction on the type of a There are pragmatic motivations behind our decision to not allow cancellation of replicated terms, namely that we do not wish a request to cancel a service possibly shared by many processes. However, there are also technical challenges, stemming from the fact that multiple actions of type a : req T can appear in a well-typed term, which as we explain below can create ambiguity in cancellation reductions.

Let us assume that the no-requests(T ) restriction was lifted. Now, as an example consider the composition req ab.P | a | ca.Q | c(x).acc x(y).R. First, let us look at the underlined term: it is impossible to know what is the type of a , as it could be either acc T or req T . If the type is acc T , which means that the (dual) accept is canceled, we should apply cancellation to req ab.P ; if the type is req T , i.e., if a is in fact the cancellation of another request, then we should not touch reqab.P . In our example, it is easy to check that the replication will appear after a communication on c so the type of a must be req T , but in general it is not possible to determine this information (again, consider just the underlined term). Our restriction on the type of a ensures that, in a case like the underlined term above, we can be sure that the type cannot be req T , so it must be acc T and we can proceed to cancel req ab.P using (C-Req). Indeed, the full composition is not typable since in that case the type of a must be req T , and no-requests(req T ) is not true. In fact, without our restriction, (C-Req) does not work any more, since it assumes a to be of type acc T , so we would need to replace it with:

(νa : T )( i∈I req ab i .P i | a ) -→ (νa : T )( i∈I (b i | P i ) | a ) (C-Req')
This is the special case in which we know the type of a must be acc T , since it is bound and all other elements are requests. This variation is more complex, and we would also have to forego the ability to use do-catch on req ab.P , so we chose not to introduce it. Even if we did use this seemingly more liberal system, we would anyway not want replications to be deleted, so it would be of limited value. The only advantage of this alternative solution is that it does not put restrictions on the shape of types assigned to a , and therefore it works also with polymorphism (i.e., a second-order setting).

Typing the Book Purchase Example

It is easy to verify that the examples from Section 2 are well-typed. For the Buyer we obtain the following (for some req Γ 1 and end ∆ 1 ):

Buyer req Γ 1 , end ∆ 1 , seller : req T 1
with T 1 = !string.?double.⊕ buy : !string.& {accepted : end, rejected : end} , cancel : end .

The type T 1 is the behaviour of b inside Buyer.

For the Seller we obtain:

Seller req Γ 2 , bank : req T 2 , seller : acc T 1 with T 2 = ?double.?(?string.T 3 ).!T 3 .T 3 ) and T 3 = ⊕ {accepted : end, rejected : end} .

For the Bank we obtain:

Bank req Γ 3 , bank : acc T 2
Interestingly, no type structure is needed for the affine adaptations: cancellation is completely transparent. The variation of Seller with an added do-catch, do req bank c catch req paymate c, will simply need paymate : req T 2 in its interface, i.e., with a type matching that of bank, but the original Seller can also be typed in the same way by weakening. Similarly, BuyerMsg has the same interface as Buyer, except that it must include print : req string, and again the two processes can be assigned the same interface by weakening, if needed. The processes Check-PriceA, CheckPriceB, and BuyerCancel can be assigned the same type for seller, namely req T 1 , exactly like Buyer.

Finally, as we shall see next affinity does not destroy any of the good properties we expect to obtain with session typing.

Properties

Typed terms enjoy the expected soundness properties. In particular we have:

Lemma 1 (Substitution). If P Γ and a ∈ dom(Γ ) then Q{ a /b} Γ { a /b}. Theorem 1 (Subject Reduction). If P Γ and P -→ Q then Q Γ .
Proof. The proof relies on several results including Lemma 1. The non-standard case is for cancellations and in particular for do ρ catch P | Q. However, it can be easily checked that the substitution of ρ by P is sound, because both terms offer the same interface except for the canceled session (and dually P can be thrown away in standard communication).

Theorem 2 (Diamond property). If P Γ and

Q 1 ←-P -→ Q 2 then either Q 1 ≡ Q 2 or Q 1 -→ R ←-Q 2 .
Proof. The result is actually easy to establish, since the only critical pairs arise from multiple requests to the same replication or to the same cancellation. However, even in that case the theorem holds because: a) replications are immediately available and functional (uniform availability); b) cancellations are persistent. The fact that a can never be assigned req T simplifies the proof.

The above strong confluence property indicates that our sessions are completely deterministic, even considering the possible orderings of requests.

Progress

Our contribution to the theory of session types is well-behaved affinity, in the sense that we can guarantee that any session that ends prematurely will not affect the quality of a program. Indeed, if we simply allowed unrestricted weakening, for example by a type rule Γ 0 as done in [START_REF] Giunti | Algorithmic type checking for a pi-calculus with name matching and session types[END_REF], but without any apparatus at the language level, it would be easy to type a process such as (νa)ab.P | b(x).Q and clearly not only a but also b would be stuck for ever. In this section we prove that this never happens to a well-typed term.

Let us write λ for a prefix ρ that is not a request, i.e., such that ρ = req ab.P . This is proved very easily by induction on typing derivations.

We now define a notion of permanently blocked process, which intuitively is a process that cannot proceed in any context, either because of deadlock or because of (restricted) sessions without a dual. We will use the fact that linear communications are always under the corresponding bound name, from Proposition 1. As usual P -→ means that P cannot reduce.

Definition 1 (Blocked process). A process P is blocked if P -→ and:

P ≡ (ν a : T ) (H1[ ρ1 ] | • • • | Hn[ ρn ]) n ≥ 1 ∀i ∈ {1, . . . , n} . subject(ρi) ∈ { a}
We give some examples to clarify the definition: i) req ax.req by.P | req br.req ak.Q is not considered blocked since it can reduce properly if we add the appropriate replications. ii) (νa)(req ax.req by.P | req br.req ak.Q) is not considered blocked because we can add a replication acc b(x).R and it will perform one step (before becoming blocked). iii) both (νa)(req ax.req by.P | req ak.req br.Q) and (νa, b)(req ax.req by.P | req br.req ak.Q) are blocked, and indeed they have no chance of reducing. iv) a(x).by.P | b(z).ar.Q is not considered blocked, even if it can never reduce, but from Proposition 1 we don't need to consider this case. v) (νa, b, c)(a(x).by.P | b(z).cr.Q | c(s).ae.R) is blocked; there is a cycle spanning all three sub-processes. vi) (νa)ab.P and (νa, b)(ab.P | b(x).Q) are blocked; this is "bad" affinity. vii) The above examples can be extended with do-catch, which explains the H-contexts in the definition.

We can now present the main result:

Theorem 3 (Progress). If P Γ then: a) for all Q, C[ ] such that P ≡ C[ Q ], Q is not blocked. b) if P -→, then either P ≡ 0 or there exists Q, a, ∆, Θ with Q ∆ and Q -→, such that (ν a)(P | Q) Θ and (ν a)(P | Q) -→.
Part a) is shown by Theorem 1 and with the help of a lemma: if P Γ then P is not blocked. Part b), which is similar to the formulation in [START_REF] Dezani-Ciancaglini | On progress for structured communications[END_REF], is shown by induction on the type derivation.

The theorem is actually very strong, since it holds also for requests, contrary to related works such as [START_REF] Dezani-Ciancaglini | On progress for structured communications[END_REF] where terms enjoy progress only for the linear part of sessions, i.e., where a request (that may never be activated) can permanently disable any sessions that depend on it.

Moreover, notice that b) in itself is not enough: we could have a blocked subterm in parallel to a request req a 1 b.P , then we could iterate compositions with forwarders acc a i (x).req a i+1 x and there would always be a reduction. In general, the existence of a "good" Q does not exclude a "bad" one that leads to deadlock. However, from a) we know that there is no subterm that is blocked. Also, we have not considered circular dependencies for replications; it is easy to check that they cannot lead to deadlock, and actually they cannot be typed.

Finally, we have checked that typed processes are strongly normalising, which is not so surprising since we followed closely the logical principles of Affine Logic. We leave the complete proof of this result, which uses the technique of Reducibility Candidates [START_REF] Girard | Linear logic[END_REF] in conjunction with Theorem 2, to a longer version. Note that Progress (Theorem 3) is in a sense more important, for two reasons: first, a system without progress can still be strongly normalising, since blocked terms are by definition irreducible; second, practical systems typically allow divergence, and in that case the progress property (which we believe can be transferred without surprises to this setting) becomes much more relevant.

Related work and future plans

We divide our discussion on the related work in three parts: relaxing linearity in session types, dealing with exceptional behaviour, and logical foundations.

The study of language constructs for exceptional behavior (including exceptional handling and compensation handling) has received significant attention; we refer the reader to a recent overview [START_REF] Ferreira | Results of the SENSORIA Project[END_REF], while concentrating on those works more closely related to ours. Carbone at al. are probably the first to introduce exceptional behaviour in session types [START_REF] Carbone | Structured interactional exceptions in session types[END_REF]. They do so by extending the programming language (the π-calculus) to include a throw primitive and a try-catch process. The language of types is also extended with an abstraction for a try-catch block: essentially a pair of types describing the normal and the exceptional behaviour. The extensions allow communication peers to escape, in a coordinated manner, from a dialogue and reach another point from where the protocol may progress. Carbone [START_REF] Carbone | Session-based choreography with exceptions[END_REF] and Capecchi et al. [START_REF] Capecchi | Global escape in multiparty sessions[END_REF] port these ideas to the multi-party setting. Hu et al. present an extension of multi-party session types that allow to specify conversations that may be interrupted [START_REF] Hu | Practical interruptible conversations: Distributed dynamic verification with session types and Python[END_REF]. Towards this end, an interruptible type constructor is added to the type language, requiring types that govern conversations to be designed with the possible interrupt points in mind. In contrast, we propose a model where programs with and without exceptional behaviour are governed by the same (conventional) types, as it is the norm in functional and object-oriented programming languages.

Caires et al. proposed the conversation calculus [START_REF] Hugo | The conversation calculus: A model of service-oriented computation[END_REF]. The model introduces the idea of conversation context, providing for a simple mechanism to locally handle exceptional conditions. The language supports error recovery via throw and try-catch primitives. No type abstraction is proposed.

Contracts take a different approach by using process-algebra languages [START_REF] Castagna | A theory of contracts for web services[END_REF] or labeled transition systems [START_REF] Bravetti | Contract-based discovery and composition of web services[END_REF] for describing the communication behaviour of processes. In contrast to session types, where client-service compliance is given by a symmetric duality relation, contracts come equipped with an asymmetric notion of compliance usually requiring that a client and a service reach a successful state. In these works it is possible to end a session (usually on the client side only) prematurely, but there is no mechanism equivalent to our cancellation, no relationship with exception handling, and no clear logical foundations.

Caires and Pfenning gave a Curry-Howard correspondence relating Intuitionistic Linear Logic and session types in a synchronous π-calculus [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF]. Although we do not use their types, there is a clear correspondence between !T 1 .T 2 and T 1 ⊗ T 2 , and similarly for input. The splitting of the term when composing session endpoints, in our case with (Res), which is standard from [START_REF] Abramsky | Computational interpretations of linear logic[END_REF], was never used in sessions before the work [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF]. For output (and request) we followed a different but equivalent approach in which b in ab.P is free, when in [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF] it would be restricted to appear strictly under P . In fact, we did not change anything compared to the usual output rule [START_REF] Honda | Language primitives and type disciplines for structured communication-based programming[END_REF], which shows that a logical system can be obtained from a standard session system simply by an adaptation of (Res) so that it plays the role of a logical "cut." Indeed, the system we presented can be mildly adapted to obtain an embedding of typed processes to proofs of Affine Logic. In any case, our formulation allows to type more processes than Linear Logic interpretations, and to our knowledge it is the first logical account of exceptions in sessions, based on an original interpretation of weakening. Moreover, Propositional Affine Logic is decidable, a result by Kopylov [START_REF] Kopylov | Decidability of linear affine logic[END_REF], so there are better prospects for type inference.

As part of future work, we would like to develop an algorithmic typing system, along the lines of [START_REF] Vasco | Fundamentals of session types[END_REF]. We also believe it would be interesting to apply our technique to multiparty sessions [START_REF] Honda | Multiparty asynchronous session types[END_REF] based on Proof Nets [START_REF] Mostrous | Multiparty sessions based on proof nets[END_REF].

b : e 178 b : select buy c : e 178 cFig. 1 .

 1781781 Fig. 1. Sequence Diagram for Succesful Book Purchase

  νb) req seller b | b "The Prince".b(price).(b cancel | R) CheckPriceB . = (νb) req seller b | b "Beyond Good and Evil".b(price).(b | R)

  : ⊕ {li : Ti} i∈I (Bra) ∀i ∈ I . Pi Γ, a : Ti I = ∅ a {li.Pi} i∈I Γ, a : & {li : Ti} i∈I (Req) P Γ req ab.P Γ • a : req T • b : T (Acc) P req Γ, x : T acc a(x : T ).P req Γ, a : acc T (Par)

Proposition 1 .

 1 If P Γ and P ≡ (ν a)(H[ λ ] | Q) and subject(λ) = b and b ∈ fn(Q) then b ∈ a.

We assume that in BuyerMsg P and Q do not use b. The restriction to non-delegated sessions is for simplicity: if the last action on b was to send it over some channel k, e.g., using kb, the encoding would be more complicated, because we would not have access to the end of the session and anything after that output would not be caught.

The expert might notice that logical negation suggests a dualisation of all components, e.g., !T.T . = ?T .T In fact the output type !T.T and the request req T hide a duality on T , effected by the type system, so everything is compatible.

[START_REF] Caires | Session types as intuitionistic linear propositions[END_REF] This method works fine until one adds a second-order fragment: then type substitutions must be carefully controlled, or some results will become slightly weaker.

Acknowledgments This work was supported by FCT through funding of MUL-TICORE project, ref. PTDC/EIA-CCO/122547/2010, and LaSIGE Strategic Project, ref. PEst-OE/EEI/UI0408/2014. We would like to thank the anonymous reviewers and also Nobuko Yoshida, Hugo Torres Vieira, Francisco Martins, and the members of the Gloss group in the University of Lisbon, for their detailed and insightful comments.


Rumyana Neykova

Nobuko Yoshida

Multiparty Session Actors

Actor coordination armoured with a suitable protocol description language has been a pressing problem in the actors community. We study the applicability of multiparty session type (MPST) protocols for verification of actor programs. We incorporate sessions to actors by introducing minimum additions to the model such as the notion of actor roles and protocol mailboxes. The framework uses Scribble, which is a protocol description language based on multiparty session types. Our programming model supports actor-like syntax and runtime verification mechanism guaranteeing communication safety of the participating entities. An actor can implement multiple roles in a similar way as an object can implement multiple interfaces. Multiple roles allow for cooperative interconcurrency in a single actor. We demonstrate our framework by designing and implementing a session actor library in Python and its runtime verification mechanism. Benchmark results demonstrate that the runtime checks induce negligible overhead.

Introduction

The actor model [START_REF] Agha | Actors: a model of concurrent computation in distributed systems[END_REF][START_REF] Agha | A foundation for actor computation[END_REF] is (re)gaining attention in the research community and in the mainstream programming languages as a promising concurrency paradigm. Unfortunately, the programming model itself does not ensure correct sequencing of interactions between different computational processes. A study in [START_REF] Tasharofi | Why do Scala developers mix the actor model with other concurrency models?[END_REF] points out that "the property of no shared space and asynchronous communication can make implementing coordination protocols harder and providing a language for coordinating protocols is needed". This reveals that the coordination of actors is a challenging problem when implementing, and especially when scaling up an actor system.

To overcome this problem, we need to solve several shortcomings existing in the actor programming models. First, although actors often have multiple states and complex policies for changing states, no general-purpose specification language is currently in use for describing actor protocols. Second, a clear guidance on actor discovery and coordination of distributed actors is missing. This leads to adhoc implementations and mixing the model with other paradigms which weaken its benefits [START_REF] Tasharofi | Why do Scala developers mix the actor model with other concurrency models?[END_REF]. Third, no verification mechanism (neither static nor dynamic) is proposed to ensure correct sequencing of actor interactions. Most actor implementations provide static typing within a single actor, but the communication between actors -the complex communication patterns that are most likely to deadlock -are not checked.

We tackle the aforementioned challenges by studying applicability of multyparty session types (MPST) [START_REF] Honda | Multiparty asynchronous session types[END_REF], a type theory for communicating processes, to actor systems. The tenet of MPST safety assurance methodology is the use of a high-level, global specification (also called protocol) for describing the interactions of communication entities. From the global protocol each entity is given a local session type defining the order and the payload type of the interactions. Programs are then written as a collection of possibly interleaved conversations, verified against prescribed protocols and constraints at runtime. The practical incarnation of the theoretical MPST is the protocol specification language Scribble [START_REF]Scribble project home page[END_REF]. Scribble is equipped with a verification mechanism, which makes protocol creation easier and protocol verification sound. Declarative protocol specifications in Scribble can readily avoid typical errors in communications programming, including type errors, disrespect of call orders, circular service dependencies and deadlocks. We call these safety properties ensured by MPST communication safety.

Recent works from [START_REF] Neykova | SPY: Local Verification of Global Protocols[END_REF][START_REF] Hu | Practical Interruptible Conversations: Distributed Dynamic Verification with Session Types and Python[END_REF] prove the suitability of Scribble and its tools for the dynamic verification of real world complex protocols [START_REF]Ocean Observatories Initiative[END_REF] and present a runtime verification framework that guarantees safety and session fidelity of the underlying communications. The verification mechanism is applied to a large cyberinfrastructure. The MPST dynamic verification framework is built on a runtime layer for protocol management and developers use MPST primitives for communication, which limits the verification methodology to a specific infrastructure. In this paper, we take the MPST one step further. We adapt and distil the model to present a MPST verification of actors systems. A main departure from our previous work is that [START_REF] Neykova | SPY: Local Verification of Global Protocols[END_REF][START_REF] Hu | Practical Interruptible Conversations: Distributed Dynamic Verification with Session Types and Python[END_REF] required special conversation runtime, built into the application, which restrict the programming style and the model applicability. In this paper, we prove the generality of MPST framework by showing Scribble protocols offer a wider usage, in particular, for actor programming.

Our programming model is grounded on three new design ideas: (1) use Scribble protocols and their relation to finite state machines for specification and runtime verification of actor interactions; (2) augment actor messages and their mailboxes dynamically with protocol (role) information; and (3) propose an algorithm based on virtual routers (protocol mailboxes) for the dynamic discovery of actor mailboxes within a protocol. We implement a session actor library in Python to demonstrate the applicability of the approach. To the best of our knowledge, this is the first design and implementation of session types and their dynamic verification toolchain in an actor library.

The paper is organised as follows: § 2 gives a brief overview of the the key features of our model and presents the running example. § 3 describes the constructs of Session Actors and highlights the main design decisions. § 4 presents the implementation of the model on concrete middleware. § 5 evaluates the framework overheads, compares it with a popular Scala actor library [START_REF]Akka -scala actor library[END_REF] and shows applications. Finally, § 6 discusses related work and concludes. The code for the runtime and the monitor tool, example applications and omitted details are available at [25].

Session Actors Programming Model

Actor Models and Design Choices

Actor Model Overview We assume the following actor features to determine our design choices. Actors are concurrent autonomous entities that exchange messages asynchronously. An actor is an entity (a class in our framework) that has a mailbox and a behaviour. Actors communicate between each other only by exchanging messages. Upon receiving a message, the behaviour of the actor is executed, upon which the actor can send a number of messages to other actors, create a number of actors or change its internal state. Each actor is equipped with a mailbox where messages are buffered. Actors have states and behaviours. Behaviours of an actor can only be changed by that actor itself, while processing a message. Active threads within actors continuously process messages whenever their mailboxes are not empty. There are only three primitive operations each actor can perform: (1) create new actors; (2) send messages to other actors whose address the sender knows; and (3) become an actor with a new state and behaviour. All these operations are atomic. The only order inherent is a causal order, and the only guarantee provided is that messages sent by actors will eventually be processed by their receivers. Other synchronisation and coordination constraints need to be externally enforced, by the unit called roles. The notion of roles is crucial in our framework and is explained below.

Session Actors To verify actor interactions, we introduce multiparty roles that enable multiple local control flows inside an actor. Each actor is annotated with supported protocols and roles it implements. As a result, session actors are containers for roles. Each actor also holds a reference to the other participating roles in the protocols. These references are bound to their physical actor containers through the actor discovery mechanism (during the protocol creation, explained in § 4.3), Without session annotations a session actor behaves identically to a plain actor. In a nutshell, an actor can be transformed to a session actor by applying the following design methodology:

1. the global protocol the actor is part of is written in Scribble and projected to local specifications; 2. the actor class is annotated with a @protocol decorator, which links to the local protocol specification; 3. each method is annotated with @role decorator that exposes a role instance (acting as a container for all protocol roles); and 4. interactions with other actors are performed via the exposed role instance.

The changes and additions that the MPST annotations bring to the original actor model are as follows (we link to the subsections where they are explained): (a) different passive objects (called roles) that run inside an actor are given a session type ( § 4.2); (b) an actor engages in structured protocol communications via a protocol mailbox ( § 4.3) and dynamically learns the roles it is communicating with; and (c) an actor message execution is bound to a protocol structure ( § 4.4). This structure is checked via the internal FSM-based monitor. This design choice (incorporating roles inside actors) enables to apply the MPST verification framework to actors, as explained in this and the next two sections.

Scribble overview Scribble [START_REF]Scribble project home page[END_REF][START_REF] Honda | Scribbling interactions with a formal foundation[END_REF] is a practical and human-readable language for protocol specification that is designed from the multiparty session types theory [START_REF] Honda | Multiparty asynchronous session types[END_REF][START_REF] Bettini | Global progress in dynamically interleaved multiparty sessions[END_REF]. It is a language to describe application-level protocols among communicating systems and aims to prevent communication mismatches and type errors during communications. A Scribble protocol represents an agreement on how participating systems interact with each other by describing an abstract structure of message exchanges between roles. Roles abstract from the actual identity of the endpoints that may participate in a runtime conversation instantiating the protocol. The core structures supported in Scribble are asynchronous message passing, choice, parallel and recursion constructs. The Scribble toolkit comes with libraries for parsing, well-formedness checking algorithms and several language bindings. An implementation of Python-based Scribble tools for projection and validation [START_REF]Scribble project home page[END_REF], as well as static verification for various languages, e.g. [START_REF] Ng | Multiparty session C: Safe parallel programming with message optimisation[END_REF] are explained in the literature [START_REF] Honda | Structuring Communication with Session Types[END_REF].

Session Actor

MPST verification framework The top-down development methodology for MPST verification is shown in the left part of Fig. 1 and the additions for session actors is illustrated on the right.

A distributed protocol is specified as a global Scribble protocol, which collectively defines the admissible communication behaviours between the participating entities, called roles inside the protocol. Then, the Scribble toolchain is used to algorithmically project the global protocol to local specifications.

For each role a finite state machine (FSM), which prescribes the allowed actions and communicating parties, is generated from the local specification and stored in a distributed storage to be retrieved whenever a role is instantiated. When a party requests to start or join a session, the initial message specifies which role it intends to play as. Its monitor retrieves the local specification based on the protocol name and the role. A runtime monitor ensures that each endpoint program conforms to the core protocol structure.

To guarantee session fidelity we perform two main checks. First, we verify that the type (operation and payload) of each message matches its specification (operations can be mapped directly to message headers, or to method calls, class names or other relevant artefacts in the program). Second, we verify that the overall order of interactions is correct, i.e. interaction sequences, branches and recursions proceed as expected, respecting the explicit dependencies (for example, m1() from A to B; m2() from B to C; where A, B and C denote roles and m1() and m2() denote methods imposes an inputoutput causality). These measures rule out errors, e.g. communication mismatches, that violate the permitted protocol.

Verification of Session Actors

We explain how we apply the above methodology. As observed in [START_REF] Scholliers | Parallel actor monitors: Disentangling task-level parallelism from data partitioning in the actor model[END_REF] in many actor systems an actor encapsulates a number of passive objects, accessed from the other actors through asynchronous method calls. Similarly session actors are a collection of interleaving control flows of actor roles. An actor role is associated with a FSM, generated from a global protocol. This verification structure is depicted in the right hand side of Fig. 1.

The association is done through annotating the actor type (class) and receive messages (methods) with protocol information. Annotating the actor type with protocol information results in registering the type for a particular role. When a session is started, a join message is sent (in a round-robin style) to all registered actors. When this join message is received, the generated FSM is loaded into the actor role and all subsequent messages on that protocol (role) are tracked and checked via the verification mechanism explained above. Message receive is delegated to the appropriate FSM via pattern matching on the protocol id, contained in the message. If all actors messages comply to their assigned FSMs, the whole communication is guaranteed to be safe. If participants do not comply, violations (such as deadlocks, communication mismatch or breakage of a protocol) are detected and delegated to a Policy actor. Further implementation details are explained in § 4.

Warehouse Management Use Case

To illustrate and motivate central design decisions of our model, we present the buyerseller protocol from [START_REF] Honda | Multiparty asynchronous session types[END_REF] and extend it to a full warehouse management scenario. A warehouse consists of multiple customers communicating to a warehouse provider. It can be involved in a Purchase protocol (with customers), but can also be involved in a StoreLoad protocol with dealers to update its storage.

Scribble Protocol. The interactions between the entities in the system are presented as two Scribble protocols, shown in Fig. 2(a) and 2(b). The protocols are called Purchase and StoreLoad and involve three (a Buyer (B), a Seller (S) and an Authenticator (A)) and two (a Store (S), a Dealer (D)) parties, respectively. At the start of a purchase session, B sends login details to S, which delegates the request to an Authentication server. After the authentication is completed, B sends a request quote for a product to S and S replies with the product price. Then B has a choice to ask for another product, to proceed with buying the product, or to quit. By buying a product the warehouse decreases the product amount it has in the store. Products in stock are increased as prescribed by the StoreLoad protocol, Fig. 2(b). The protocol starts with a recursion where the warehouse (in the role of S) has a choice to send a product request to a dealer (D) to load the store with n numbers of a product. After receiving the request, D delivers the product (operation put on Line 8). These interactions are repeated in a loop until S decides to quit the protocol (Line 11). The reader can refer to [START_REF]Scribble project home page[END_REF] for the full specification of the Scribble syntax.

Challenges. There are several challenging points to implement the above scenario. First, a warehouse implementation should be involved in both protocols, therefore it can play more than one role. Second, initially the user does not know the exact warehouse it is buying from, therefore the customer learns dynamically the address of the warehouse. Third, there can be a specific restriction on the protocol that cannot be expressed as system constants (such as specific timeout depending on the customer). The next section explains the implementation of this example in Session Actors.

Session Actor Language

This section explains the main operations in the session actor language and its usecase implementation in Python.

Session Actor language operations Fig. 3 presents the main session actor operations and annotations. The central concept of the session actor is the role. A role can be considered as a passive object inside an actor and it contains meta information used for MPST-verification. A session actor is registered for a role via the @protocol annotation. The annotation specifies the name of the protocol and role the session actor is registered for and the rest of the participants in the protocol. The aforementioned meta information is stored in a role instance created in the actor. To be used for communication, the method should be annotated with the role using the @role decorator and passing the role instance name. The instance serves as a container for references to all protocol roles, which allows sending a message to a role in the session actor without knowing the actor location. A message is sent via c.role.method, where c is the self role instance and role is the role the message is intended for.

Sending to a role without explicitly knowing the actor location is possible by the actor discovery mechanism (the details will be explained in § 4). When a session is started via the create method, actors receive an invitation for joining the protocol. The Fig. 4: Session Actor implementation for the Warehouse role operation join is a default handler for invitation messages. If a session actor changes the join behaviour and applies additional security policies to the joiners, the method should be overloaded. Introducing actor roles via protocol executions is a novelty of our work: without roles and the actor discovery mechanism, actors need additional configurations to introduce their addresses, and this would grow the complexity of configurations.

Warehouse service implementation We explain the main constructs by an implementation of a session actor accountable for the Warehouse service. Fig. 4 presents the implementation of a warehouse service as a single session actor that keeps the inventory as a state (self.purchaseDB). Lines 1-2 annotate the session actor class with two protocol decoratorsc and c1 (for seller and store roles respectively). c and c1 are accessible within the warehouse actor and are holders for mailboxes of the other actors, involved in the two protocols.

All message handlers are annotated with a role and for convenience are implemented as methods. For example, the login method (Line 5) is invoked when a login message (Line 4, Fig. 2 (a)) is sent. The role annotation for c (Line 4) specifies the sender to be buyer.

The handler body continues following Line 5, Fig. 2 (a) -sending a login message via the send primitive to the session actor, registered as a role auth in the protocol of c. Value c.auth is initialised with the auth actor mailbox as a result of the actor discovery mechanism (explained in the next section). The handling of authenticate (Line 6, Fig. 2 (a)) and request (Line 6, Fig. 2 (b)) messages is similar, so we omit it and focus on the buy handler (Line 9-12), where after sending the delivery details (Line 11), the warehouse actor sends a message to itself (Line 12) using the primitive become with value update. Value update is annotated with another role c1, but has as a sender self. This is the mechanism used for switching between roles within an actor. Update method (Line 19-20) implements the request branch (Line 6-9, Fig. 2 (b)) of the StoreLoad protocol -sending a request to the dealer and handling the reply via method put.

The correct order of messages is verified by the FSM attached to c and c1. As a result, errors such as calling put before update or executing two consecutive updates, will be detected as invalid.

This section explains our implementation of Session Actors. The key design choices follow the actor framework explained in § 2.1. We have implemented the multiparty session actors on top of Celery [8] (a Python framework for distributed task processing) with support for distributed actors [START_REF]Cell -actors for celery[END_REF]. Celery uses advanced message queue protocol (AMQP 0-9-1 [START_REF]Advanced Message Queuing Protocol homepage[END_REF]) as a transport. The reason for choosing AMQP network as base for our framework is that AMQP middleware shares a similar abstraction with the actor programming model, which makes the implementation of distributed actors more natural.

AMQP Background

We first summarise the key features of the AMQP model. In AMQP, messages are published by producers to entities, called exchanges (or mailboxes). Exchanges then distribute message copies to queues using binding rules. Then AMQP brokers (virtual routers) deliver messages to consumers subscribed to queues. Exchanges can be of different types, depending on the binding rules and the routing strategies they implement. We explain the three exchange types used in our implementation: round-robin exchange (deliver messages, alternating to all subscribers), direct exchange (subscribers subscribe with a binding key and messages are delivered when a key stored in the message meta information matches the binding key of the subscription) and broadcast exchange (deliver a message to all subscribers).

Distributed actors are naturally represented in this AMQP context using the abstractions of exchanges. Each actor type is represented in the network as an exchange and is realised as a consumer subscribed to a queue based on a pattern matching on the actor id. Message handlers are implemented as methods on the actor class.

Our distributed actor discovery mechanism draws on the AMPQ abstractions of exchanges, queues and binding, and our extensions to the actor programming model are built using Python advanced abstraction capabilities: two main capabilities are greenlets (for realising the actors inter-concurrency) and decorators (for annotating actor types and methods).

A greenlet (or micro/green thread) is a light-weight cooperatively-scheduled execution unit in Python. A Python decorator is any callable Python object that is used to modify the function, method or class definition it annotates using the @ symbol. A decorator is passed the original object being defined and returns a modified object, which is then bound to the name in the definition. These decorators in Python are partly inspired by Java annotations.

Actor Roles

A key idea of actor roles is each role to run as a micro-thread in an actor (using Python greenlet library). Actors are assigned to session roles by adding the @protocol decorator to the actor class declaration. Methods that implement a part of a protocol are annotated with the @role decorator. A role is activated when a message is received and ready to be processed. Switching between roles is done via the become primitive (as demonstrated in Fig. 4), which is realised as sending a message to the internal queue of the actor. Roles are scheduled cooperatively. This means that at most one role can be active in a session actor at a time.

Actors Discovery

Fig. 5: Organising Session Actors into protocols Fig. 6: Session Actors Monitoring Fig. 5 presents the network setting (in terms of AMQP objects) for realising the actor discovery for buyer and seller of the protocol Purchase. We use the three types from AMQP explained in § 4.1. For simplicity, we create some of the objects on starting of the actor system -round-robin exchange per actor type (warehouse and customer in Fig. 5) and broadcast exchange per protocol type (purchase in Fig. 5). All spawned actors alternate to receive messages addressed to their type exchange. Session actors are registered for roles via the protocol decorator and as a result their type exchange is bound to the protocol exchange (Line 1 in Fig. 4 binds warehouse to purchase in Fig. 5).

We now explain the workflow for actor discovery. When a protocol is started, a fresh protocol id and an exchange with that id are created. The type of the exchange uses AMPQ type, direct explained in § 4.1. A direct type is used so that messages with a routing key are delivered to actors linked to the exchange with binding to that key (it corresponds to protocol id in Fig. 5). Then join message is sent to the protocol exchange and delivered to one actor per registered role (join is broadcasted to warehouse and customer in Fig. 5). On join, an actor binds itself to the protocol id exchange with subscription key equal to its role (bindings seller and buyer in Fig. 5). When an actor sends a message to another actor within the same session (for example c.buyer.send in Fig. 4), the message is sent to the protocol id exchange (stored in c) and from there delivered to the buyer actor.

Preservation through FSM checking

Before a message is dispatched to its message handler, the message goes through a monitor. Fig. 6 illustrates the monitoring process. Each message contains meta information (a routing key) with the role name the message is intended for and the id of the protocol the message is in the part of. When an actor joins a protocol, the FSM, generated from the Scribble compiler (as shown in Fig. 1) is loaded from a distributed storage to the actor memory.

Then the checking goes through the following steps. First, depending on the role and the protocol id the matching FSM is retrieved from the actor memory. Next the FSM checks the message labels/operators (already in the part of the actor payload) and sender and receiver roles (in the part of the message binding key implemented as our extension) are valid.

The check assertions step verifies that if any constraints on the size/value of the payload are specified in Scribble, they are also fulfilled. If a message is detected as wrong the session actor throws a distributed exception and sends an error message back to the sending role and does not pass the message to its handler for processing. This behaviour can change by implementing the wrong message method of the session actor.

Evaluations of Session Actors

This section reports on the performance of our framework. The goal of our evaluation is two fold. First, we compare our host distributed actor framework [8] with a mainstream actor library (AKKA [START_REF]Akka -scala actor library[END_REF]) to show our host framework is a suitable choice. Second, we show that our main contribution, verification of MPST protocols, can be realised with reasonable cost. The full source code of the benchmark protocols and applications and the raw data are available from the project page [25].

Session Actors Performance

We test the overhead in message delivery implementation using the pingpong benchmark [START_REF] Imam | Integrating task parallelism with actors[END_REF] in which two processes send each other messages back and forth. The original version of the code was obtained from Scala pingpong.scala from http:// scala-lang.org/old/node/54 and adapted to use distributed AKKA actors (instead of local). We distinguish two protocols. Each pingpong can be a separate session (protocol FlatPingPong) or the whole iteration can be part of one recursive protocol (RecPingPong). The protocols are given in Fig. 7(b). This distinction is important only to session actors, because the protocol shape has implications on checking. For AKKA actors the notion of session does not exist and therefore the two protocols have the same implementation.

Set Up We prepared each scenario 50 times and measured the overall execution time (the difference between successive runs was found to be negligible). The creation and population of the network was not measured as part of the execution time. The client and server actor nodes and the AMQP broker were each run on separate machines (Intel Core2 Duo 2.80 GHz, 4 GB memory, 64-bit Ubuntu 11.04, kernel 2.6.38). All hosts are interconnected through Gigabit Ethernet and Latency between each node was measured to be 0.24 ms on average (ping 64 bytes). The version of Python used was 2.7, of Scala -2.10.2 and of the AKKA-actors -2.2.1.

Results Fig. 7(a) compares three separate benchmark measurements for session actors. The base case for comparison. "Celery" is a pure actor implementation without the addition of roles. "With Role" measures the overhead of roles annotations without having the monitor capabilities enabled. The two main cases, "Rec Monitor" and "Monitor", measure the full overhead of session actors. This separation aims to clearly illustrate the overhead introduced by each of the additions, presented in the paper: roles annotations, MPST verification and actor discovery. Note that the FSMs for the recursive and for the flat protocol have the same number of states. Therefore, the observed difference in the performance is a result of the cost of the actor discovery.

The goal of the benchmarks is two fold. First, to compare the actor framework that we use with one of the most widely used frameworks for distributed actors. Second, to evaluate the performance implications of our extensions. A difference between the performance of AKKA and Celery is not surprising and can be explained with a distinct nature of the frameworks. AKKA runs on top of JVM and the remote actors in these benchmarks use direct TCP connections. On the other hand, Celery is Python-based framework which uses a message middleware as a transport, which adds additional layer of indirection. Given these differences, Celery actors have reasonable performance and are a viable alternative.

Regarding our additions we can draw several positive conclusions from the benchmarks: (1) the cost of the FSM checking is negligible and largely overshadowed by the cost of the communication (such as latency and routing); and (2) the cost of the actor discovery is reasonable, given the protocol load.

MPST Verification Overhead

In this subsection, we discuss the row overhead of monitor checking, which is a main factor that can affect the performance and scalability of our implementation. Knowing the complexity of checking protocols of different length is useful to reason on the applicability of the model.

We have applied two optimisations to the monitor, presented in [START_REF] Neykova | SPY: Local Verification of Global Protocols[END_REF][START_REF] Hu | Practical Interruptible Conversations: Distributed Dynamic Verification with Session Types and Python[END_REF], which significantly reduce the runtime overhead. First, we pre-generate the FSM based on the global protocol. Second, we cache the FSM protocols the first time when a role is loaded. Therefore, the slight runtime overhead, observed in the previous section is a result of the time required to choose the correct FSM among all in-memory FSMs inside the actor and the time required to check the FSM transition table that the message is expected. Both have the linear complexity on the number of roles running inside the actor and the number of states inside the FSM respectively. Table 1 shows the approximate execution time for checking a protocols of increasing length. The small numbers are omitted since the time taken is negligible.

Applications of Session Actors

As a practical evaluation of our framework, we have implemented two popular actor applications and adapted them to session actors.

The first application is a distributed chat with multiple chat rooms, where a number of clients connect to a reactive server and execute operations based on their privileges. Depending on privileges some clients might have extended number of allowed messages. We impose this restriction dynamically by annotating the restricted operations with different roles. An operation is allowed only if its actor has already joined a session in the annotated role.

The second usecase is a general MapReduce for counting words in a document. It is an adaptation from an example presented in the official website for celery actors: http: //cell.readthedocs.org/en/latest/getting-started/index.html. The session actor usage removes the requirement for the manual actor spawning of Reducers actors inside the Mapper actor, which reduces the code size and the complexity of the implementation.

We give in Fig. 8 the implementation of the latter example. For sake of space and clarity, the implementation reported here abstracts from technical details that are not important for the scope of this paper-interested readers can find the full sources in [25]. The protocol is started on Line 26 specifying the type of the actors for each role and passing the arguments for the initial executionn (the number of reducers) and file (the name of the source file to be counted). The Mapper implements the join method, which is invoked when the actor joins a protocol. Since the Mapper is the starting role, Note that spawning and linking of the actors are not specified in the code because the actor discovery mechanism accounts for it. The protocol proceeds by Mapper sending one message for each line of the document. The receiver of each message is one of the Reducers. Each Reducer counts the words in its line and sends the result to the Aggregator (c.A, Line 48), which stores all words in a dictionary and aggregates them. When a threshold for the result is reached, the Aggregator prints the result and stops the session explicitly.

Our experiences with session actors are promising. Although they introduce new notions, i.e. a protocol and a role, we found that their addition to a class-based actor framework is natural to integrate without requiring a radical new way of thinking. The protocol and role annotations are matched well with typical actor applications, and even they result in simplifying the code by removing the boilerplate for actor discovery and coordination. The protocol-oriented approach to actor programming accounts for the early error detection in the application design and the coordination of actors. The runtime verification guarantees and enforces the correct order of interactions, which is normally ensured only by hours of testing.

Related Work

Behavioural and session types for actors and objects There are several theoretical works that have studied the behavioural types for verifying actors [START_REF] Mostrous | Session Typing for a Featherweight Erlang[END_REF][START_REF] Crafa | Behavioural types for actor systems[END_REF]. The work [START_REF] Crafa | Behavioural types for actor systems[END_REF] proposes a behavioural typing system for an actor calculus where a type describes a sequence of inputs and outputs performed by the actor body. In [START_REF] Mostrous | Session Typing for a Featherweight Erlang[END_REF], a concurrent fragment of Erlang is enriched with sessions and session types. Messages are linked to a session via correlation sets (explicit identifiers, contained in the message), and clients create the required references and send them in the service invocation message. The developed typing system guarantees that all within-session messages have a chance of being received. The formalism is based on only binary sessions.

Several recent papers have combined session types, as specification of protocols on communicating channels, with object-oriented paradigm. A work close to ours is [START_REF] Gay | Modular session types for distributed object-oriented programming[END_REF], where a session channel is stored as a field of an object, therefore channels can be accessed from different methods. They explicitly specify the (partial) type for each method bound to a channel. Our implementation also allows modularised sessions based on channel-based communication. Their work [START_REF] Gay | Modular session types for distributed object-oriented programming[END_REF] is mainly theoretical and gives a static typing system based on binary session types. Our work aims to provide a design and implementation of runtime verification based on multiparty session types, and is integrated with existing development frameworks based on Celery [8] and AMQP [START_REF]Advanced Message Queuing Protocol homepage[END_REF].

The work in [START_REF] Caires | Spatial-behavioral types for concurrency and resource control in distributed systems[END_REF] formalises behaviours of non-uniform active objects where the set of available methods may change dynamically. It uses the approach based on spatial logic for a fine grained access control of resources. Method availability in [START_REF] Caires | Spatial-behavioral types for concurrency and resource control in distributed systems[END_REF] depends on the state of the object in a similar way as ours.

See [START_REF]BETTY WG3 -Languages Survey[END_REF] for more general comparisons between session types and other frameworks in object-oriented paradigms.

Other Actor frameworks The most popular actor's library (the AKKA framework [START_REF]Akka -scala actor library[END_REF] in Scala studied in [START_REF] Tasharofi | Why do Scala developers mix the actor model with other concurrency models?[END_REF]) supports FSM verification mechanism (through inheritance) and typed channels. Their channel typing is simple so that it cannot capture structures of communications such as sequencing, branching or recursions. These structures ensured by session types are the key element for guaranteeing deadlock freedom between multiple actors. In addition, in [START_REF]Akka -scala actor library[END_REF], channels and FSMs are unrelated and cannot be intermixed; on the other hand, in our approach, we rely on external specifications based on the choreography (MPST) and the FSMs usage is internalised (i.e. FSMs are automatically generated from a global type), therefore it does not affect program structures.

Several works study an extension of actors in multicore control flows. Multithreaded active objects [START_REF] Henrio | Multi-threaded active objects[END_REF] allow several threads to co-exist inside an active object and provide an annotation system to control their concurrent executions. Parallel Actor Monitors (PAM) [START_REF] Scholliers | Parallel actor monitors: Disentangling task-level parallelism from data partitioning in the actor model[END_REF] is another framework for intra actor parallelism. PAMs are monitors attached to each actor that schedule the execution of the messages based on synchronisation constraints. Our framework also enables multiple control flows inside an actor as [START_REF] Henrio | Multi-threaded active objects[END_REF][START_REF] Scholliers | Parallel actor monitors: Disentangling task-level parallelism from data partitioning in the actor model[END_REF]. In addition, we embed monitors inside actors in a similar way as [START_REF] Scholliers | Parallel actor monitors: Disentangling task-level parallelism from data partitioning in the actor model[END_REF][START_REF] Henrio | Multi-threaded active objects[END_REF] embed schedulers. The main focus of the monitors in [START_REF] Henrio | Multi-threaded active objects[END_REF][START_REF] Scholliers | Parallel actor monitors: Disentangling task-level parallelism from data partitioning in the actor model[END_REF] is scheduling the order of the method executions in order to optimise the actor performance on multi-core machines, while our approach aims to provide explicit protocol specifications and verification among interactions between distributed actors in multi-node environments.

The work [START_REF] Schäfer | Jcobox: Generalizing active objects to concurrent components[END_REF] proposes a solution to have multiple cooperatively scheduled tasks within a single active object similar to our notion of cooperative roles within an actor. The approach is implemented as a Java extension with an actor-like concurrency where communication is based on asynchronous method calls with objects as targets.

They resort to RMI for writing distributed implementations and do not allow specifying sequencing of messages (protocols) like ours.

The work [START_REF] Ren | Actors, roles and coordinators -a coordination model for open distributed and embedded systems[END_REF] proposes a framework of three layers for actor roles and coordinators, which resembles roles and protocol mailboxes in our setting. Their specifications focus on QoS requirements, while our aim is to describe and ensure correct patterns of interactions (message passing).

Comparing with the above works, our aim is to provide effective framework for multi-node environments where actors can be distributed transparently to different machines and/or cores.

Conclusion

We propose an actor specification and verification framework based on multiparty session types, providing a Python library with actor communication primitives. Cooperative multitasking within sessions allows for combining active and reactive behaviours in a simple and type-safe way. The framework is naturally integrated with Celery [8] which uses advanced message queue protocol (AMQP [START_REF]Advanced Message Queuing Protocol homepage[END_REF]), and uses effectively its types for realising the key mechanisms such as the actor discovery. We demonstrate the overhead of our implementation is very small. We then show that programming in session actors is straightforward by implementing and rewriting usecases from [START_REF]Akka -scala actor library[END_REF]. To our best knowledge, no other work is linking FSMs, actors and choreographies in a single framework. As a future work, we plan to extend to other main stream actor-based languages such as Scala and Erlang to test the generality of our framework. As actor languages and frameworks are getting more and more attractions, we believe that our work would offer an important step for writing correct large-scale actor-based communication programs.

Fig. 1 :

 1 Fig. 1: MPST-development methodology (left) and session actors (right)

Fig. 2 :

 2 Fig. 2: Global protocols in Scribble for (a) Purchase protocol and (b) StoreLoad protocol

Fig. 7 :

 7 Fig. 7: (a) The PingPong benchmark (the overhead of message delivery) and (b) The PingPong protocol

Fig. 8 :

 8 Fig. 8: WordCount in Session Actors

Table 1 :

 1 Execution Time for checking protocol with increasing length

	States	100	1000	10000
	Time (ms)	0.0479	0.0501	0.0569

Acknowledgement We thank Ask Solem for his support and guidance. This work has been partially sponsored by VMWare, Pivotal and EPSRC EP/K011715/1 and EP/K034413/1.