Mario Bravetti

Gianluigi Zavattaro

Foundations of Coordination and Contracts and their Contribution to Session Type Theory

We briefly recall results obtained in twenty years of research, spanning across the old and the new millennium, on the expressiveness of coordination languages and on behavioural contracts for Service-Oriented Computing. Then, we show how the techniques developed in those contexts are currently contributing to the clarification of aspects that were unclear about session types, in particular, asynchronous session subtyping that was considered decidable since 2009, while it was proved to be undecidable in 2017.

Introduction

Shared dataspaces and the so-called generative communication paradigm [START_REF] Gelernter | Generative communication in linda[END_REF] attracted a lot of attention since the initial years of research about foundations of coordination models and languages. Linda [START_REF] Carriero | The s/net's linda kernel (extended abstract)[END_REF], probably the most popular language based on this coordination model, is based on the idea that concurrent processes interact via a shared dataspace, the so-called Tuple Space (TS for short), where the information needed to coordinate the activities are introduced and retrieved. After its insertion in the TS, a datum becomes equally accessible to all processes, but it is bound to none. In this way, the interaction among concurrent processes is decoupled in space and time, principles useful in the development of modular and scalable concurrent and distributed systems.

Concerning foundational studies on Linda-like coordination languages, it appeared immediately clear that techniques borrowed from the tradition of concurrency theory could be naturally applied. At the first two editions of the Coordination conference, two process calculi based on Linda were proposed by De Nicola and Pugliese [START_REF] De Nicola | A process algebra based on LINDA[END_REF] and by Busi, Gorrieri and Zavattaro [START_REF] Busi | Three semantics of the output operation for generative communication[END_REF]. In particular, the latter started a line of research on the expressiveness of Linda-like coordination primitives that exploited, besides process calculi, also Petri nets. For instance, Petri nets were used in [START_REF] Busi | On the Turing equivalence of Linda coordination primitives[END_REF], to prove that a Linda process calculus with input, output and test-for-absence is not Turing complete if the semantics for output is unordered, i.e., there is an unpredictable delay between the execution of an output and the actual availability of the emitted datum in the TS. It is interesting to recall that, on the other hand, the same calculus is Turing complete if an ordered semantics is considered, i.e. an emitted datum is immediately available in the TS after the corresponding output is executed. Turing completeness was proved by showing an encoding of a Turing powerful formalism, namely Random Access Machines (RAMs), which is a computational model based on registers that can be incremented, decremented and tested for emptiness.

The success of the Linda coordination model was witnessed by the development, at the end of the 90s, of Linda-based middlewares from main ICT vendors like IBM and Sun Microsystem, which proposed T-Spaces and JavaSpaces, respectively. The basic Linda coordination model was extended with primitives for event notification, time-out based data expiration, and transactions. The techniques for evaluating the expressive power of Linda languages had to become more sophisticated to cope with these additional primitives. In particular, Petri nets with transfer and reset arcs [START_REF] Dufourd | Reset nets between decidability and undecidability[END_REF] were adopted to cope also with the new coordination mechanisms for event notification [START_REF] Busi | On the expressiveness of event notification in datadriven coordination languages[END_REF] and for temporary data [START_REF] Busi | Temporary data in shared dataspace coordination languages[END_REF].

During the initial years of the new millennium, Service-Oriented Computing (SOC) emerged as an alternative model for developing communication-based distributed systems. In particular, the large diffusion of Web Services called for the development of new languages and techniques for service composition. The idea, at the basis of SOC, is to conceive an ecosystem of services that expose operations that can be combined to realize new applications. To support this idea, it is necessary for the services to be equipped with an interface that, besides describing the offered operations and the format of the exchanged messages, defines the conversation protocols, i.e., the expected flow of invocations of the operations. These interfaces, in particular the specification of the conversation protocol, are also called behavioural contracts.

Process calculi contributed to the development of theories for behavioural contracts. This line of research was initiated by Carpineti, Castagna, Laneve and Padovani [START_REF] Carpineti | A formal account of contracts for web services[END_REF], for the case of client-server composition, and by Bravetti and Zavattaro [START_REF] Bravetti | Contract based multi-party service composition[END_REF], for multiparty service compositions. The latter is particularly significant for the so-called service choreographies, i.e., systems in which there exists no central orchestrator, responsible for invoking all the other services in the system, because services reciprocally interact. Behavioural contract theories focused mainly on the investigation of appropriate notions of correctness for service compositions (i.e., define when a system based on services is free from communication errors) and on the characterization of notions of compatibility between services and behavioural contracts (i.e., define when a service conforms to a given behavioural contract).

For multiparty composition, a fairness based notion of correctness, called compliance, was proposed for the first time in [START_REF] Bravetti | Contract based multi-party service composition[END_REF]: a system is correct if, whatever state can be reached, there exists a continuation of the computation that yields a final state in which all services have successfully completed. Given the notion of compliance, it is possible to define also a natural notion of refinement for behavioural contracts: a refinement is a relation among contracts such that, given a set of compliant contracts C 1 , • • • , C n , each contract C i can be independently replaced by any of its possible refinements C i , and the overall system obtained by composition of C 1 , • • • , C n is still compliant. Contract refinement can then be used to check whether a service conforms with a behavioural contract: it is sufficient to verify if the communication behaviour of the service refines the behavioural contract. This, in fact, implies that such service can be safely used wherever a service is expected with the behaviour specified by the contract.

A negative result in the theory of behavioural contracts is that, in general, the union of two refinement relations is not guaranteed to be itself a refinement. This implies the impossibility to define a maximal notion of refinement. For this reason, most of the effort in the line of research on behavioural contracts initiated in [START_REF] Bravetti | Contract based multi-party service composition[END_REF] has been dedicated to the identification of interesting subclasses of contracts for which the maximal refinement exists. Such classes are: contracts with output persistence [START_REF] Bravetti | Contract based multi-party service composition[END_REF] (i.e. output actions cannot be avoided when a state is entered in which they are ready to be executed), contract refinement preserving strong compliance [START_REF] Bravetti | A theory for strong service compliance[END_REF] (i.e. as soon as an output is ready to be executed, a receiver is guaranteed to be ready to receive it), and asynchronously communicating contracts [START_REF] Bravetti | Contract compliance and choreography conformance in the presence of message queues[END_REF] (i.e. communication is mediated by fifo buffers). In the first two of these three cases, it has been also possible to provide a sound algorithmic characterization of the corresponding maximal refinements.

To the best of our knowledge, characterizing algorithmically the maximal contract refinement in case of asynchronous communication is still an open problem. The main source of difficulty derives from the fact that, due to the presence of unbounded communication buffers, systems of asynchronously communicating contracts are infinite-state, even if contracts are finite-state. In the light of this difficulty, we tried to take inspiration from work on session types, where asynchronous communication has been investigated since the seminal work by Honda, Yoshida and Carbone [START_REF] Honda | Multiparty asynchronous session types[END_REF] (recipient of the most influential POPL'08 paper award). Session types can be seen as a simplification of contracts obtained by imposing some limitations: there are only two possible choices, internal choice among distinct outputs and external choice among distinct inputs.

The counterpart of contract refinement in the context of session types is subtyping [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF]. If we consider asynchronous communication, both contract refinement and session subtyping can admit a refinement/subtype to perform the communication actions in a different order. For instance, given a contract/type that performs an input followed by an output, a refinement/subtype can anticipate the output before the input, because such output can be buffered and actually received afterwards. Asynchronous session subtyping was already studied by Mostrous, Yoshida, and Honda in [START_REF] Mostrous | Global principal typing in partially commutative asynchronous sessions[END_REF], where also an algorithm for checking subtyping was presented. Upon studying this algorithm we noticed an error in its proof of termination: if, while checking subtyping, the buffer grows unboundedly, the proposed procedure does not terminate. Subsequently, Bravetti, Carbone and Zavattaro [START_REF] Bravetti | Undecidability of asynchronous session subtyping[END_REF] and Lange and Yoshida [START_REF] Lange | On the undecidability of asynchronous session subtyping[END_REF] independently proved that asynchronous session subtyping is actually undecidable. Our experience in the modeling of Turing complete formalism (see the above discussion about encoding RAMs in the Linda process calculus) helped in finding an appropriate Turing powerful model to be encoded in terms of asynchronous session subtyping. In particular, we were able to present a translation from a Queue Machine M (a computational model similar to pushdown automata, but with a queue instead of a stack) to a pair of session types that are in asynchronous subtyping relation if and only if M does not terminate. Then, undecidability of asynchronous session subtyping directly follows from the undecidability of the halting problem for Queue Machines.

These negative results opened the problem of identifying significant classes of session types for which asynchronous subtyping can be decided. Currently, the most interesting fragments have been identified in [START_REF] Bravetti | Undecidability of asynchronous session subtyping[END_REF][START_REF] Lange | On the undecidability of asynchronous session subtyping[END_REF] and [START_REF] Bravetti | On the boundary between decidability and undecidability of asynchronous session subtyping[END_REF]. In the former, an algorithm is presented for the case in which one of the two types is completely deterministic, i.e. all choices -both internal and external-have one branch only. In the latter, we have considered single-out (and single-in) session types, meaning that in both types to be checked all internal choices (resp. external choices) have one branch only. In the design of our algorithm we have been inspired by our expertise in the analysis of the expressiveness of Linda process calculi. In particular, the analysis techniques in Petri nets with transfer and reset arcs (our tools to prove decidability results) are based on the notion of well quasi ordering (wqo): while generating an infinite sequence of elements, it is guaranteed to eventually generate an element that is greater -with respect to the wqo-of an already generated element. Similarly to the procedure in [START_REF] Mostrous | Global principal typing in partially commutative asynchronous sessions[END_REF], our algorithm checks a sequence of judgements, but differently from [START_REF] Mostrous | Global principal typing in partially commutative asynchronous sessions[END_REF], termination is guaranteed because there exists a wqo on judgements, and the algorithm can terminate when a judgement greater than an already checked one is considered.

Outline of the paper. The remainder of this paper is divided in three main parts: in Section 2 we discuss the techniques used to investigate the expressive power of the Linda coordination model; in Section 3 we recall the main results concerning behavioural contracts; and in Section 4 we present recent results on session types for asynchronous communication. The additional Section 5 reports some concluding remarks.

Process Calculi to Study the Expressiveness of Linda

Several Linda process calculi have been proposed in the literature, like PAL [START_REF] De Nicola | A process algebra based on LINDA[END_REF], LLinda [START_REF] De Nicola | Coordinating mobile agents via blackboards and access rights[END_REF], and the Linda calculi in [START_REF] Busi | Three semantics of the output operation for generative communication[END_REF] and [START_REF] Brogi | Modeling coordination via asynchronous communication[END_REF], just to mention some of them (published in the proceedings of the first two editions of the Coordination conference). Those calculi have been defined for several purposes: investigate from a foundational viewpoint coordination models and languages, develop novel formal analysis techniques for coordinated systems, or drive the implementation of fullyfledged coordination languages. In this section, we focus on process calculi used to prove results about the expressive power of primitives for Tuple Spaces. Different techniques have been adopted, spanning from Turing completeness (used, e.g., in [START_REF] Busi | On the Turing equivalence of Linda coordination primitives[END_REF]) to modular embeddings (used, e.g., in [START_REF] Brogi | Modeling coordination via asynchronous communication[END_REF]). To give the reader a more precise idea of such techniques, in particular the former, we report some results taken from [START_REF] Busi | On the Turing equivalence of Linda coordination primitives[END_REF][START_REF] Busi | On the expressiveness of event notification in datadriven coordination languages[END_REF].

We start by introducing a Linda calculus with four basic primitives: (i) out to introduce a new datum into a shared repository called dataspace, (ii) in to consume one datum available in the repository, (iii) notify to register the interest PRE : Table 1. The transition system for processes (symmetric rule of PAR omitted).

j ∈ I i∈I αi.Pi
in future emissions of a specific datum (when such datum will be emitted a new instance of a given process will be spawned), and (iv) tfa to test for the absence of a specific datum. This calculus is Turing complete (result taken from [START_REF] Busi | On the Turing equivalence of Linda coordination primitives[END_REF]) while the fragment without tfa is not (result taken from [START_REF] Busi | On the expressiveness of event notification in datadriven coordination languages[END_REF]). The proof of Turing completeness is by reduction from Random Access Machines, while the non Turing completeness of the considered fragment was proved in [START_REF] Busi | On the expressiveness of event notification in datadriven coordination languages[END_REF] by resorting to a (non Turing complete) variant of Petri net, namely Petri nets with transfer arcs (see, e.g., [START_REF] Dufourd | Reset nets between decidability and undecidability[END_REF]); here, we present an alternative proof technique based on well quasi orderings (which are actually used to prove decidability results for Petri nets with transfer arcs).

We now formally report the definition of a Linda-based process calculus, starting from the syntax of processes.

Definition 1 (Linda Processes). Let Name, ranged over by a, b, . . ., be a denumerable set of names. Processes are defined by the following grammar: The basic process actions are in(a) and out(a) denoting the consumption or emission, respectively, of one instance of datum a from/into the shared dataspace. Two additional primitives are considered: notify(a, P ) to register a listener interested in future emissions of the datum a (the reaction to such event will be the spawning of process P ) and tfa(a) to test for the absence of the datum a. The term i∈I α i .P i denotes a process ready to perform any of the action α i , and then proceed by executing the corresponding continuation P i . We use 0 to denote such process in case I = ∅, and we will usually omit trailing 0.

The replicated process !α.P performs an initial action α and then spawns the continuation P by keeping !α.P in parallel. Two parallel processes P and Q are denoted with P |Q. In the following we will use the notation i∈I P i to denote the parallel composition of processes indexed on the set of indexes I.

We now formalize the operational semantics for Linda processes in terms of a transition system with four kinds of labels: in(a), out(a), notify(a, P ), and tfa(a). The transition system is the least one satisfying the axioms and rules reported in Table 1. The PRE rule simply allows a sum process to execute one of its initial actions and then continue with the corresponding continuation. REPL allows !α.P to execute α, spawn an instance of the continuation P , and keep !α.P in parallel. Finally, PAR allows a parallel process to execute an action. We now move to the syntax and semantics of systems, in which processes are equipped with a dataspace and a multiset of registered listeners.

Definition 2 (Linda Systems). A system S is a tuple P, S, L where P is a process, S is the dataspace (i.e. a multiset over Name), and L are the registered listeners (i.e. a multiset of pairs (a, P )).

The semantics of systems is defined by the minimal transition system satisfying the rules in Table 2. The transitions for systems allow processes to (i) consume data from the shared dataspace, (ii) register a new listener, (iii) introduce a new datum in the shared dataspace with the corresponding spawning of the processes in the interested listeners, and (iv) test for the absence of one datum in the dataspace. We use to denote multiset union.

In the following, we will consider termination and divergence of systems.

Definition 3 (Termination and Divergence). Given a system S, we say that S terminates, denoted S ↓, if there exists at least an ending computation, i.e., there exist

S 1 , • • • , S n such that S → S 1 → S 2 • • • → S n →
, where S n → means that there exists no system S s.t. S n → S . We say that S diverges, denoted S ↑, if there exists at least one infinite computation, i.e., there exist one infinite sequence of systems

S 1 , • • • , S n , • • • such that S → S 1 → S 2 • • • → S n → • • • .

Turing Completeness

The Turing completeness of the Linda calculus was proved in [START_REF] Busi | On the Turing equivalence of Linda coordination primitives[END_REF]. Actually, the calculus in that paper considered a variant of the tfa primitive called inp, which is a non-blocking version of in: inp has two possible continuations P and Q, the first one activated in case the consumption succeeds, and a second one activated if the message of interest is absent. This primitive coincides with the process in(a).P + tfa(a).Q. The proof of Turing completeness was based on an encoding of Random Access Machines (RAMs) [START_REF] Shepherdson | Computability of recursive functions[END_REF], a well known register-based Turing powerful formalism. Here, we rephrase that encoding by exploiting in, out and tfa, without using notify. For this reason, in this subsection, we do not consider listeners and denote systems simply with pairs P, S of processes and dataspace.

A RAM, denoted in the following with R, is a computational model composed of a finite set of registers r 1 , . . . , r n , that can hold arbitrarily large natural numbers, and of a program composed by indexed instructions (1 : I 1 ), . . . , (m : I m ), that is a sequence of numbered instructions, like arithmetic operations (on the contents of registers) or conditional jumps. An internal state of a RAM is given by (i, c 1 , . . . , c n ) where i is the program counter indicating the next instruction to be executed, and c 1 , . . . , c n are the current contents of the registers r 1 , . . . , r n , respectively.

The computation starts from the first instruction (1 : I 1 ) and terminates when the program counter points to an undefined instruction. In other terms, the initial configuration is (1, 0, . . . , 0) and the computation continues by executing the other instructions in sequence, unless a jump instruction is encountered. The execution stops when an instruction outside the valid range 1, . . . , m is reached.

Formally, we indicate by (i, c 1 , . . . , c n ) → R (i , c 1 , . . . , c n ) the fact that the configuration of the RAM R changes from (i, c 1 , . . . , c n ) to (i , c 1 , . . . , c n ) after the execution of the i-th instruction.

In [START_REF] Minsky | Computation: finite and infinite machines[END_REF] it is shown that the following two instructions are sufficient to model every recursive function: (i : Succ(r j )) to add 1 to the content of register r j ; (i : DecJump(r j , s)) that, if the content of register r j is not zero, decreases it by 1 and goes to the next instruction, otherwise jumps to instruction s.

We start presenting how to encode RAM instructions into Linda processes:

[[(i : Succ(r j ))]] = !in(p i ).out(r j ).out(p i+1 ) [[(i : DecJump(r j , s))]] = !in(p i ). in(r j ).out(p i+1 ) + tfa(r j ).out(p s )
The idea is to represent the content of the register r j with a corresponding number of instances of the datum r j in the dataspace. The program counter is modeled by a datum p i indicating that the i-th instruction is the next one to be executed. The modeling of the i-th instruction always starts with the consumption of the p i datum. An increment instruction on r j simply produces one datum r j , while a DecJump instruction either consumes one datum r j or tests for the absence of such datum. After these operations, the subsequent program counter datum is emitted.

We now present the full definition of our encoding. Let R be a RAM with m instructions, and let (i, c 1 , . . . , c n ) be one of its configurations. With

[[(i, c 1 , . . . , c n )]] R = 1≤i≤m [[(i : I i )]], {p i , r 1 , • • • , r 1 c1 times , • • • , r n , • • • , r n cn times
} we denote the system representing the configuration (i, c 1 , . . . , c n ).

We now formally recall the correctness of the encoding (proved in [START_REF] Busi | On the Turing equivalence of Linda coordination primitives[END_REF]) from which we conclude the Turing completeness of the Linda calculus.

Theorem 1. Let R be a RAM. Given → 3 as a notation for three successive reductions of systems, we have that:

-Soundness: if [[(i, c 1 , . . . , c n )]] R → 3 Q then there exists a unique configura- tion (j, c 1 , . . . , c n ) such that Q = [[(j, c 1 , . . . , c n )]] R and (i, c 1 , . . . , c n ) → R (j, c 1 , . . . , c n ) -Completeness: if (i, c 1 , . . . , c n ) → R (j, c 1 , . . . , c n ) then [[(i, c 1 , . . . , c n )]] → 3 [[(j, c 1 , . . . , c n )]]
As a consequence of the Turing completeness of the Linda calculus, we have that both termination and divergence are undecidable, namely, given a system S, it is in general undecidable whether S ↓ or S ↑. Notice that Turing completeness does not depend on notify, as this primitive is not used in the modeling of RAMs reported in the previous subsection.

Decidability of Divergence in the Calculus without tfa

We now focus on the expressive power of tfa, by investigating whether the calculus continues to be Turing complete even if we remove such primitive. Hence, we consider the fragment of the Linda calculus without the tfa primitive. We will observe that this fragment is no longer Turing powerful, as divergence turns out to be decidable, namely, given a system S, it is always possible to decide whether S ↑. This result was proved in [START_REF] Busi | On the expressiveness of event notification in datadriven coordination languages[END_REF] by presenting an encoding of a Linda calculus with in, out, and notify into Petri nets with transfer arcs: an extension of place/transition Petri nets for which properties like coverability, or the existence of an infinite firing sequence, are still decidable. In this section we present a novel alternative proof (at least for this considered Linda calculus) inspired by the theory of well structured transition systems (WSTS) [START_REF] Finkel | Well-structured transition systems everywhere![END_REF]: we first define an ordering on systems configurations which is proved to be a well quasi ordering, and then we show that the operational semantics is compatible with such ordering.

We start by recalling the notion of well quasi ordering (see, e.g., [START_REF] Finkel | Well-structured transition systems everywhere![END_REF]).

Definition 4. A reflexive and transitive relation on a set X is called quasi ordering. A well quasi ordering (wqo) is a quasi ordering (X, ≤) such that, for every infinite sequence x 1 , x 2 , • • • , there exist i < j with x i ≤ x j .

In the following we will use the following well known results for wqo:

-Consider a finite set S and the set of its multisets M(S). We have that multiset inclusion is a well quasi ordering for the latter, namely (M(S), ⊆) is a wqo, where ⊆ denotes multiset inclusion.

-Consider k well quasi orderings (X 1 , ≤ 1 ), • • • , (X k , ≤ k ). Let Π be the carte- sian product X 1 × • • • × X k and ≤ k be the natural extension of the or- derings ≤ 1 , • • • , ≤ k to Π, i.e., (x 1 , • • • , x k ) ≤ k (y 1 , • • • , y k ) if and only if x 1 ≤ 1 y 1 , • • • , x k ≤ k y k . We have that (Π, ≤ k ) is a wqo.
We now recall, taking it from [START_REF] Finkel | Well-structured transition systems everywhere![END_REF], the notion of compatibility1 of a transition system w.r.t. an ordering. Definition 5. A transition system (X, →) is compatible with respect to an ordering (X, <) if, given two states s, t ∈ X of the transition system such that s < t and s → s for some s , then there exists t such that s < t and t → t .

A known result from the theory of WSTS (Theorem 4.6 in [START_REF] Finkel | Well-structured transition systems everywhere![END_REF]) is that it is decidable to establish the existence of an infinite computation in a transition system compatible with a wqo. To exploit this result, we now define a wqo on systems P, S, L . To do this we will make use of the above result stating that multiset inclusion over multisets with a finite domain is a wqo. This result can be directly applied to dataspaces S and registered listeners L as they are multisets, while this is not possible on processes P that are terms with a given syntax. Hence, it is necessary to give an interpretation of such terms P as multisets: this can be obtained by extracting from a term P the multiset of sequential or replicated processes constituting P . Formally, given the process P we define inductively, on its syntactic structure, the multiset m(P ) as follows:

m( i∈I α i .P i ) = { i∈I α i .P i } m(!α.P ) = {!α.P } m(P |Q) = m(P ) m(Q)
We are now ready to define the following ordering on systems:

P, S, L ≤ S P , S , L ⇔ m(P ) ⊆ m(P ) ∧ S ⊆ S ∧ L ⊆ L
We now prove that this ordering ≤ S on systems is a wqo for the set of systems that are reachable from a given initial system. Proposition 1. Let S 0 = P 0 , S 0 , L 0 be an initial system and let Sys be the set of systems that are reachable from S 0 according to the reduction relation defined in Table 2. We have that (Sys, ≤ S ) is a wqo. Proof. Let S = P, S, L be a system reachable from the initial system S 0 = P 0 , S 0 , L 0 . It is easy to see that the data in S and the listeners in L are taken from finite domains given, respectively, by the parameters of the primitives out and notify occurring in the initial process P 0 (plus data or listeners already available in S 0 or L 0 ). We now observe that also the sequential or replicated processes in m(P ) are taken from a finite domain. In fact, P is the parallel composition of terms that already occur in the initial process P or in the listeners in L 0 . This is because the reduction relation defined in Table 2 does not generate new processes, but simply consumes initial actions in front of already available sequential or replicated processes or spawns processes already present in listeners.

Hence (for the first of the two well known results recalled for wqo) we can conclude that multiset inclusion is a wqo for the multisets m(P ) associated to the reachable processes P , as well as for the reachable dataspaces S and listeners L. The ordering ≤ S is the natural ordering for the cartesian product of these last three wqo, hence it is also a wqo (for the second of the recalled results).

We now observe that the reduction relation for systems defined in Table 2 is compatible with the ordering ≤ S . Proposition 2. Let S, S and T be three systems, in which the tfa primitive does not occur, such that S → S and S ≤ S T . We have that there exists a system T such that T → T and S ≤ S T .

Proof. We first observe that, for every pair of processes P and P such that m(P ) ⊆ m(P ), if P α -→ Q then there exists also Q such that P α -→ Q and m(Q) ⊆ m(Q ). This can be proved by induction on the structure of P . If P = i∈I α i .R i (resp. P = !α.R) then P is the parallel composition of terms including also P . Let Q be the process in the r.h.s. of the transition inferred on P by the rule PRE (resp. REPL) in Table 1. Such transition can be inferred (by the same rule plus possible successive applications of PAR) also on P : let Q be the process in the r.h.s. of such transition. As the same PRE (resp. REPL) rule is initially applied, we have that Q is the parallel composition of processes including also Q, hence m(Q) ⊆ m(Q ). In the inductive case, we have that the last rule applied in the transition P α -→ Q is PAR, and the thesis directly follows from the inductive hypothesis on the transition used in the premise of the application of PAR.

Consider now three systems S, S and T , in which the tfa primitive does not occur, such that S ≤ S T and S → S . The latter implies that, given S = P, S S , L S and S = P , S S , L S , there exists α such that P α -→ P . Consider now T = Q, S T , L T . Having S ≤ S T , we also have m(P ) ⊆ m(Q). For the above observation, then also

Q α -→ Q for a process Q such that m(P ) ⊆ m(Q ). Given this transition Q α -→ Q , by the rules in Table 1, we also have that T → T = Q , S T , L T with S ≤ S T . The latter is a consequence of m(P ) ⊆ m(Q ), S S ⊆ S T and L S ⊆ L T .
The last two statements follow from the fact that S T (resp. L T ) is obtained from S T (resp. L T ) by applying the same modification applied to S S (resp. L S ) to obtain S S (resp. L S ); hence multiset inclusion S S ⊆ S T (resp. L S ⊆ L T ) is preserved.

We can finally conclude with our decidability result.

Theorem 2. Let S = P, S, L be a system in which the tfa primitive does not occur. It is decidable whether S ↑.

Proof. Direct consequence of Proposition 1, Proposition 2 and the result taken from the theory of WSTS (Theorem 4.6 in [START_REF] Finkel | Well-structured transition systems everywhere![END_REF]) recalled above.

We conclude by recalling other related results about the un/decidability of S ↓, i.e. the existence of a terminating computation. In [START_REF] Busi | On the expressiveness of event notification in datadriven coordination languages[END_REF] it is proved that S ↓ is undecidable in the fragment of the Linda calculus, without tfa, considered in this subsection: hence we conclude that the Linda calculus with in, out and notify is in between decidability and undecidability, namely, S ↑ is decidable while S↓ is not. The undecidability proof consists of an encoding of RAMs which is nondeterministic: the Linda system corresponding to a RAM could have several alternative computations, but all the computations that are not faithful w.r.t. the modeled RAM are guaranteed to be divergent. Hence, the Linda system has a terminating computation if and only if the corresponding RAM terminates.

In the same paper [START_REF] Busi | On the expressiveness of event notification in datadriven coordination languages[END_REF], it is also discussed that if we remove also the primitive notify from the calculus, also S ↓ becomes decidable. This follows from the possibility to faithfully encode the fragment of the calculus with only in and out into classical place/transition Petri nets, for which it is possible to decide the reachability of any marking from which no other transitions can be fired. This additional result allows us to conclude that adding the primitive notify strictly increases the expressive power of the Linda calculus with only in and out.

Behavioural Contracts

Behavioural contracts are used to describe the message-passing behaviour of processes. The adoption of process calculi to the specification and analysis of behavioural contracts was initiated by Fournet et al. [START_REF] Fournet | Stuck-free conformance[END_REF], who proposed to specify contracts as CCS-like processes. They also defined a notion of conformance between processes and contracts following a substitution principle: a process conforms to a contract if it can replace it in any context without adding additional stuck behaviour. Contract have been subsequently studied in the context of service oriented computing: contracts for client-service interaction have been proposed by Carpineti et al. [START_REF] Carpineti | A formal account of contracts for web services[END_REF] and then independently extended along different directions by, e.g., Bravetti and Zavattaro (see e.g. [START_REF] Bravetti | Contract based multi-party service composition[END_REF][START_REF] Bravetti | A theory for strong service compliance[END_REF][START_REF] Bravetti | Towards a unifying theory for choreography conformance and contract compliance[END_REF]) by Laneve and Padovani [START_REF] Laneve | The Must preorder revisited[END_REF], by Castagna et al. [START_REF] Castagna | A theory of contracts for web services[END_REF], and Barbanera and de'Liguoro [START_REF] Barbanera | Two notions of sub-behaviour for session-based client/server systems[END_REF].

All such theories of contracts introduce, under different assumptions, notions of contract refinements that can be seen as generalizations of the notion of conformance initially studied in [START_REF] Fournet | Stuck-free conformance[END_REF]: a contract refines another one if it can safely replace it in any possible context. To give to the reader an idea of such techniques, here we report a contract theory discussed in [START_REF] Bravetti | Towards a unifying theory for choreography conformance and contract compliance[END_REF][START_REF] Bravetti | A Foundational Theory of Contracts for Multi-party Service Composition[END_REF], for synchronous communication, and [START_REF] Bravetti | Contract compliance and choreography conformance in the presence of message queues[END_REF], for the asynchronous case. In particular, the latter represents the unique contract theory, to the best of our knowledge, specifically tailored to asynchronous communication.

More precisely, the contract theory that we present is based on the following ingredients: the notion of correct contract composition, the definition of contract refinement, and its algorithmic characterization. Both synchronous and asynchronous communication, excluding the algorithmic characterization which is available only for the synchronous case.

We start by presenting the formal definition of behavioural contracts as it appears in [START_REF] Boreale | Rigorous Software Engineering for Service-Oriented Systems -Results of the SENSORIA Project on Software Engineering for Service-Oriented Computing[END_REF]. Contracts can be seen as a representation of the communication actions that can be performed at a certain location over the network. We assume a denumerable set of action names N , ranged over by a, b, c, . . . and a denumerable set Loc of location names, ranged over by l, l , l 1 , • • • . We use τ / ∈ N to denote an internal (unsynchronizable) action. Contracts are denoted adopting a basic process algebra with prefixes over {τ, a, a l | a ∈ N , l ∈ Loc}, denoting internal, input, and output action, respectively. Notice that a destination location is specified for outputs. Such a process algebra is a simple extension of basic CCS [START_REF] Milner | Communication and concurrency[END_REF] with successful termination denoted by "1" (whereas the traditional null process "0" denotes a failure or a deadlock).

Definition 6 (Behavioural Contracts). We consider a denumerable set of contract variables Var ranged over by X, Y , • • • . The syntax of contracts is

1 √ -→ 0 α.C α -→ C C λ -→ C C +D λ -→ C C{recX.C/X} λ -→ C recX.C λ -→ C
Table 3. Semantic rules for contracts (symmetric rules omitted).

defined by the following grammar

C ::= 0 | 1 | α.C | C +C | X | recX.C α ::= τ | a | a l
where recX. is a binder for the process variable X denoting recursive definition of processes. We assume that in a contract C all process variables are bound. In the following we will omit trailing " 1" when writing contracts.

The operational semantics of contracts is defined in terms of a transition system labeled over L = {a, a l , τ, √ | a ∈ N , l ∈ Loc}, ranged over by λ, λ , . . . , obtained by the rules in Table 3 (plus a symmetric rule for choice). We use the notation C{ / } to denote syntactic replacement. Semantic rules are the standard ones, apart from that of term 1, which performs a √ transition denoting successful termination. The semantics of a contract C yields a finite-state labeled transition system,2 whose states are the contracts reachable from C.

We now present a simple example of a contract describing an authentication service that repeatedly performs two kinds of task: (i) the authentication of clients by receiving their username and password, and (ii) the request to an external account service for update of the list of the registered users.

recX.( username.password.(accepted client .X + f ailed client .X) + updateAccounts accountServer .newAccounts.X )

The contract indicates a repeated choice between the two possible tasks. The first task is activated by the reception of an invocation on username. In this case, a password should subsequently be received and then two possible answers are sent back to the client: either accepted or failed . The second task is activated by sending a request for update to the accountServer. In this case, the newAccounts are subsequently received.

In the following we will study independent contract refinement. As already anticipated in the Introduction under synchronous communication a maximal independent contract refinement that preserves compliance does not exist. In [START_REF] Bravetti | Contract based multi-party service composition[END_REF] we showed that this is a consequence of the symmetry between input and output actions and that a possible solution, for synchronous communication, is to resort to output persistent contracts; thus breaking such a symmetry.

λ 1 λ 2 • • • λ n-1 λ n , we use C w -→ C to denote the sequence of transitions C λ1 -→ C 1 λ2 -→ • • • λn-1 -→ C n-1 λn -→ C . A contract C is output persistent if, for any C such that C w -→ C and C a l -→, the following holds: C √ -→ / and, if C α -→ C with α = a l , then also C a l -→.
The output persistence property states that once a contract decides to execute an output, its actual execution is mandatory in order to successfully complete the execution of the contract. This property typically holds in languages for the description of service orchestrations (see e.g. WS-BPEL [START_REF]Web Services Business Process Execution Language Version 2.0 OASIS Standard[END_REF]) in which output actions cannot be used as guards in external choices (see e.g. the pick operator of WS-BPEL which is an external choice guarded on input actions).

The previous example of the authentication server (which is not output persistent) can be rephrased as follows to be used in a synchronous setting: recX.( username.password.(τ.accepted client .X + τ.f ailed client .X) + τ.updateAccounts accountServer .newAccounts.X )

Notice that, in this new version of the example, we have simply added an internal action τ in front of outputs occurring in choices. This guarantees that, at the moment the choice is to be resolved, the output action is not yet ready to be executed: it becomes available only after the τ and, then, its eventual execution is mandatory.

In the remainder, when we consider synchronous communication, we will restrict to output persistent contracts.

Synchronous Contract Composition

Synchronous systems are formed by the parallel composition of contracts.

Definition 8 (Synchronous Systems). The syntax of synchronous systems is defined by the following grammar

P ::= [C] l | P ||P
We assume systems to be such that: (i) every contract subterm [C] l occurs in P at a different location l and (ii) no output action with destination l is syntactically included inside a contract subterm occurring in P at the same location l, i.e. actions a l cannot occur inside a subterm [C] l of P .

A contract located at location l is denoted with [C] l . Located contracts can be combined in parallel with the operator P ||P .

System operational semantics is defined by the rules in Table 4 plus symmetric rules. Transition system labels, still ranged over by λ, λ , • • • , are now taken from the extended set {a sr , a sr , τ, √ | a ∈ N ; s, r ∈ Loc}, where: a sr (a sr , resp.) denotes a potential output (input, resp.) with the sender being at location s and the receiver at location r; τ denotes a synchronization or a move performed internally by one contract in the system and √ denotes successful termination.

C ar -→ C [C]s asr -→ [C ]s C a -→ C [C]r asr -→ [C ]r C √ -→ C [C] l √ -→ [C ] l P λ -→ P P ||Q λ -→ P ||Q λ = √ P asr -→ P Q asr -→ Q P ||Q τ -→ P ||Q P √ -→ P Q √ -→ Q P ||Q √ -→ P ||Q Table 4.
Synchronous system semantics (symmetric rules omitted).

C ar -→ C [C, Q]s asr -→ [C , Q]s [C, Q]r asr -→ [C, Q :: a s ]r C √ -→ C [C, ] l √ -→ [C , ] l C a -→ C b l ∈ Q ⇒ b = a [C, Q :: a s :: Q ]r τ -→ [C , Q :: Q ]r
Table 5. Asynchronous system semantics (rules for parallel omitted).

Asynchronous Contract Composition

In asynchronous systems contracts are equipped with an input message queue.

Definition 9 (Asynchronous Systems). The syntax of asynchronous systems is defined by the following grammar

P ::= [C, Q] l | P ||P Q ::= | a l :: Q
We assume asynchronous systems to be such that: (i) and (ii) of Definition 8 (with

[C, Q] l replacing [C] l ) hold true.
Terms Q denote message queues. They are sequences of messages, each one denoted with a l where a is the action name and l is the location of the sender. We use " " to denote the empty message queue. Trailing are usually left implicit, and we use "::" also as an operator over the syntax: if Q and Q are -terminated queues, according to the syntax above, then Q :: Q means appending the two queues into a single -terminated list. Therefore, if Q is a queue, then :: Q, Q :: , and Q are syntactically equal. In the following, when we talk about asynchronous contract systems, we will use the shorthand [C] l to stand for [C, ] l . Asynchronous system operational semantics is defined by the rules in Table 5 plus the rules for the parallel operator of Table 4. In Table 5 we assume that b l ∈ Q holds true if and only if b l syntactically occurs inside Q. This notation is used in the premise of the novel τ synchronization rule that represents the consumption of an a message from the queue by removal of the oldest a one.

As an example consider the system: [a s .b s ] r || [b.a] s . After executing the two outputs, the system evolves to [START_REF] Barbanera | Two notions of sub-behaviour for session-based client/server systems[END_REF] r || [b.a, a r :: b r ] s . The receiver is now ready to consume the two messages stored in the queue, thus reaching [START_REF] Barbanera | Two notions of sub-behaviour for session-based client/server systems[END_REF] r || [START_REF] Barbanera | Two notions of sub-behaviour for session-based client/server systems[END_REF] s . Notice that the two messages are consumed in the opposite order of reception.

Notice that the information about the sender attached to queue messages is actually not used by the operational semantic rules in Table 5: even if omitted we would have obtained the same transitions. Nevertheless, we decided to use the same queue syntax as in [START_REF] Bravetti | Contract compliance and choreography conformance in the presence of message queues[END_REF] to be more adherent to reality, where messages can be distinguished e.g. depending on the sender. As a matter of fact, in [START_REF] Bravetti | Contract compliance and choreography conformance in the presence of message queues[END_REF], this information is used to produce, instead of τ actions, more informative labels that include denotation of the sender-receiver (this makes it possible to establish conformance w.r.t. a given choreographical specification).

Contract Refinement

We now recall the formal definition of independent contract refinement that preserves correct composition of contracts in both the synchronous and asynchronous cases. With P τ -→ * P we denote the existence of a (possibly empty) sequence of τ -labeled transitions starting from the system P and leading to P .

Definition 10 (Correct Contract Composition -Compliance).

A system P is a correct contract composition, denoted P ↓, if for every P such that P Intuitively, a system composed of contracts is correct if any possible computation may guarantee completion, i.e. it can be extended to reach a successfully terminated computation (in the asynchronous case this means that all queues are empty). In this case, such contracts are called compliant. An example of contract composition that is correct (both in the synchronous and asynchronous

case) is [a l3 ] l1 || [b l3 ] l2 || [a.b] l3 . Another example is [a s .b s ] r || [b.a] s
considered above, which is correct only in the asychronous case.

We are now ready to define the notion of contract refinement. Given a contract C, we use oloc(C) to denote the set of locations used as destinations in all the output actions occurring inside C.

Definition 11 (Independent Refinement).

A pre-order ≤ over contracts is an independent refinement if, for any n ≥ 1, contracts C 1 , . . . , C n and C 1 , . . . , C n such that ∀i. C i ≤ C i , and distinguished location names l 1 , . . . , l n ∈ Loc such that ∀i. oloc(C i ) ∪ oloc(C i ) ⊆ {l j | 1 ≤ j ≤ n ∧ j = i}, we have:

([C 1 ] l1 || . . . || [C n ] ln ) ↓ ⇒ ([C 1 ] l1 || . . . || [C n ] ln ) ↓
An independent refinement pre-order formalizes the possibility to replace in a correct contract composition every contract with one of its refinements, with the guarantee that the new system is still correct. In [START_REF] Bravetti | Contract based multi-party service composition[END_REF] it is shown that in the synchronous case, in the absence of the output persistence assumption, it could happen that given two independent refinement pre-orders, their union is no longer an independent refinement pre-order. In other words, there exists no maximal independent refinement pre-order.

On the contrary, if we restrict to output persistent contracts or we consider asynchronous communication, we have that the maximal independent refinement pre-order exists: it can be achieved by considering a coarser form of refinement in which, given any system composed of a set of contracts, refinement is applied to one contract only (thus leaving the others unchanged). This form of refinement, that we call compliance testing [START_REF] Bravetti | Choreographies and behavioural contracts on the way to dynamic updates[END_REF], is a form of testing where both the test and the system under test must reach success. Given a system P , we use loc(P ) to denote the subset of Loc of the locations of contracts syntactically occurring inside P .

Definition 12 (Refinement Relation

). A contract C is a refinement of a contract C denoted C
C, if and only if for all l ∈ Loc and system P such that l / ∈ loc(P ) and l / ∈ oloc(C) ∪ oloc(C ) ⊆ loc(P ), we have:

([C] l ||P ) ↓ ⇒ ([C ] l ||P ) ↓
Theorem 3 (Maximal Independent Refinement). There exists a maximal independent refinement ≤ pre-order and it corresponds to the (compliance testing based) refinement relation " ".

Properties of Contract Refinement

We now discuss some properties of contract refinement and also show a sound characterization that is decidable for the synchronous case. We use I(C) (O(C), resp.) to stand for the subset of N of the names a of input (output, resp.) actions a (a, resp.) syntactically occurring in C. Given O ⊆ N we assume O to stand for {a | a ∈ O}.

We first observe that the refinement relation allows input on new names (and unreachable outputs on new names) to be added in refined contracts.

Theorem 4 (Refinements with Extended Inputs and Outputs). Let C, C be contracts. Both of the following hold

C {0/α.C | α ∈ I(C ) -I(C)} ≺ C ⇔ C ≺ C C {T /α.C | α ∈ O(C ) -O(C)} ≺ C ⇔ C ≺ C
where T is: 0 in the synchronous case, τ.0 in the asynchronous case.

This theorem is a direct consequence of queue based communication (in the asynchronous case) and output persistence (in the synchronous case): a subcontract C cannot perform reachable outputs that were not included in the potential outputs of the supercontract C; and, similarly, a compliant test P of a contract [C] l cannot perform reachable outputs directed to l that C cannot receive (e.g. in the asynchronous case [a] l ||[a l + b l ] l is not a correct contract composition).

From this theorem we can derive two fundamental properties of the maximal independent refinement pre-order: external choices on inputs can be extended, e.g. a + b a; while internal choices on outputs can be reduced, e.g. a l a l + b l in the asynchronous case and τ.a l τ.a l + τ.b l in the synchronous one, because the lefthand term is more deterministic (typical property in testing).

We now focus on determining an algorithmic sound characterization of the synchronous contract refinement relation. This is achieved by resorting to the theory of fair testing, called should-testing [START_REF] Rensink | Fair testing[END_REF]. As a side result we also have that the refinement relation is coarser than fair testing preorder. We denote with test the should-testing pre-order defined in [START_REF] Rensink | Fair testing[END_REF] where we consider √ to be included in the set of actions of terms under testing as any other action ( √ is treated as a normal action and not as the special action representing success of tests in [START_REF] Rensink | Fair testing[END_REF]). In order to resort to the theory should-testing, we define a normal form for contracts C, denoted with N F(C), that corresponds to terms of the language in [START_REF] Rensink | Fair testing[END_REF] (mainly a matter of replacing 1 with a √ action, see [START_REF] Bravetti | Towards a unifying theory for choreography conformance and contract compliance[END_REF] for details).

Theorem 5 (Resorting to Fair Testing). Let C, C be contracts. We have

N F(C {0/α.C | α ∈ I(C ) -I(C)}) test N F(C) ⇒ C C
The opposite implication does not hold in general. This can be easily seen by considering uncontrollable contracts, i.e. contracts for which there is no compliant test. For instance the contract 0, any other contract a.b.0 or c.d.0 or more complex examples like a + a.b. These contracts are all equivalent according to our refinement relation, but of course not according to fair testing. Notice that such uncontrollable contracts have completely different traces: this means that trace pre-order is not coarser than our refinement relation.

Session Types

In this section we move to session types, in particular we report about our study of asynchronous session subtyping. Session types [START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF][START_REF] Honda | Multiparty asynchronous session types[END_REF] are types for controlling the communication behaviour of processes over channels. In a very simple but effective way, they express the pattern of sends and receives that a process must perform. They are, therefore, similar to behavioural contracts, but more constrained in the kind of behaviours they can express. Since they can guarantee freedom from some basic programming errors, session types are becoming popular with many main stream language implementations, e.g., Haskell [START_REF] Lindley | Embedding session types in haskell[END_REF], Go [START_REF] Ng | Static deadlock detection for concurrent go by global session graph synthesis[END_REF] or Rust [START_REF] Jespersen | Session types for Rust[END_REF]. In [START_REF] Mostrous | Global principal typing in partially commutative asynchronous sessions[END_REF] session subtyping is introduced for asynchronous communication and it is also stated that it is decidable. Recently it has been proven that, on the contrary, it is undecidable. Here we present such an undecidability result [START_REF] Bravetti | Undecidability of asynchronous session subtyping[END_REF] and the decidability result in [START_REF] Bravetti | On the boundary between decidability and undecidability of asynchronous session subtyping[END_REF], where the largest known decidable fragment is introduced. In particular, we recall the basic definitions of session types and synchronous and asynchronous session subtyping. We then report the undecidability proof in [START_REF] Bravetti | Undecidability of asynchronous session subtyping[END_REF]. Finally, we present the fragment of singleout (and single-in) session types, for which we show asynchronous subtyping to be decidable [START_REF] Bravetti | On the boundary between decidability and undecidability of asynchronous session subtyping[END_REF]. The techniques for these (un)decidability results can be seen as improvements of those developed for Linda process calculi: reduction from Turing complete computational models and exploitation of well quasi orderings.

Session Subtyping

Session subtyping, which is the counterpart for session types of refinement for behavioural contracts, was first introduced by Gay and Hole [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF] for a sessionbased π-calculus where communication is synchronous. Session subtyping of [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF] is endowed with covariant/contravariant properties that correspond to those we observed on behavioural contract refinement: internal choices on outputs can be reduced, while external choices on inputs can be extended. To the best of our knowledge, Mostrous et al. [START_REF] Mostrous | Global principal typing in partially commutative asynchronous sessions[END_REF] were the first to adapt the notion of session subtyping to an asynchronous setting. Their computation model is a session π-calculus with asynchronous communication that makes use of session queues for maintaining the order in which messages are sent. Based on such a model they introduce the idea of output anticipation, which is also a main feature of our theory in [START_REF] Bravetti | Undecidability of asynchronous session subtyping[END_REF][START_REF] Bravetti | On the boundary between decidability and undecidability of asynchronous session subtyping[END_REF] that we present here. Mostrous and Yoshida [START_REF] Mostrous | Session typing and asynchronous subtyping for the higher-order π-calculus[END_REF] extended the notion of asynchronous subtyping to session types for the higher-order πcalculus. They also observed that their definition of asynchronous subtyping allows for orphan messages, i.e. sent messages which are never consumed from the session queue. Orphan messages are, instead, prohibited with the definition of subtyping given by Chen et al. [START_REF] Chen | On the preciseness of subtyping in session types[END_REF]: they show that such a definition is both sound and complete w.r.t. type safety and orphan message freedom. We start with the formal syntax of binary session types, adopting a simplified notation (used, e.g., in [START_REF] Bravetti | Undecidability of asynchronous session subtyping[END_REF][START_REF] Bravetti | On the boundary between decidability and undecidability of asynchronous session subtyping[END_REF]) without dedicated constructs for sending an output/receiving an input. We instead represent outputs and inputs directly inside choices. More precisely, we consider output selection ⊕{l i : T i } i∈I , expressing an internal choice among outputs, and input branching &{l i : T i } i∈I , expressing an external choice among inputs. Each possible choice is labeled by a label l i , taken from a global set of labels L, followed by a session continuation T i . Labels in a branching/selection are assumed to be pairwise distinct.

Definition 13 (Session Types). Given a set of labels L, ranged over by l, the syntax of binary session types is given by the following grammar:

T ::= ⊕{l i : T i } i∈I | &{l i : T i } i∈I | µt.T | t | end A session type is single-out if, for all of its subterms ⊕{l i : T i } i∈I , |I| = 1; it is single-in if, for all of its subterms &{l i : T i } i∈I , |I| = 1.
In the sequel, we leave implicit the index set i ∈ I in input branchings and output selections when it is already clear from the denotation of the types. Note also that we abstract from the type of the message that could be sent over the channel, since this is orthogonal to our theory. Types µt.T and t denote standard tail recursion for recursive types. We assume recursion to be guarded: in µt.T , the recursion variable t occurs within the scope of an output or an input type.

In the following, we will consider closed terms only, i.e., types with all recursion variables t occurring under the scope of a corresponding definition µt.T . Type end denotes the type of a channel that can no longer be used.

For session types, we define the usual notion of duality: given a session type T , its dual T is defined as: ⊕{l i : T i } i∈I = &{l i : T i } i∈I , &{l i : T i } i∈I = ⊕{l i : T i } i∈I , end = end, t = t, and µt.T = µt.T . In the sequel, we say that a relation R on session types is dual closed if (S, T ) ∈ R implies (T , S) ∈ R.

We start by considering a synchronous subtyping relation, similar to that of Gay and Hole [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF] but, to be more consistent with contracts, following a process-oriented instead of a channel-based approach. 3 Moreover, following [START_REF] Mostrous | Global principal typing in partially commutative asynchronous sessions[END_REF], we consider a generalized version of unfolding that allows us to unfold recursions µt.T as many times as needed.

Definition 14 (n-unfolding).

unfold 0 (T ) = T unfold 1 (⊕{l i : T i } i∈I ) = ⊕{l i : unfold 1 (T i )} i∈I unfold 1 (µt.T ) = T {µt.T /t} unfold 1 (&{l i : T i } i∈I ) = &{l i : unfold 1 (T i )} i∈I unfold 1 (end) = end unfold n (T ) = unfold 1 (unfold n-1 (T ))
Definition 15 (Synchronous Subtyping, ≤ s ). R is a synchronous subtyping relation whenever (T, S) ∈ R implies that:

1. if T = end then ∃n ≥ 0 such that unfold n (S) = end; 2. if T = ⊕{l i : T i } i∈I then ∃n ≥ 0 such that unfold n (S) = ⊕{l j : S j } j∈J , I ⊆ J and ∀i ∈ I. (T i , S i ) ∈ R; 3. if T = &{l i : T i } i∈I then ∃n ≥ 0 such that unfold n (S) = &{l j : S j } j∈J , J ⊆ I and ∀j ∈ J. (T j , S j ) ∈ R; 4. if T = µt.T then (T {T /t}, S) ∈ R.

T is a synchronous subtype of S, written T ≤ s S, if there is a synchronous subtyping relation R such that (T, S) ∈ R.

Two types T and S are related by ≤ s , whenever S is able to simulate T with output and input types enjoying covariance and contravariance properties, respectively. Notice the asymmetric use of unfolding between the left-and righthand terms T and S: in T recursion is always unfolded once, while in S many unfoldings can be needed in order to expose the starting operator of T .

As already discussed, subtyping is the counterpart of contract refinement in the context of session types. Consider, for instance, &{a : end, b : end} ≤ s &{a : end} ⊕ {a : end} ≤ s ⊕ {a : end, b : end} that hold for input contravariance and output covariance. These examples of subtypings precisely correspond to those of contract refinements commented in Section 3.4. Note that, while in the case of contracts they were obtained as a consequence of considering the maximal independent refinement, in the theory of session types they are taken by definition. We now consider the standard notion of asynchronous subtyping ≤ introduced by Chen et al. [START_REF] Chen | On the preciseness of subtyping in session types[END_REF], which enjoys orphan message freedom; we consider the simple rephrasing based on dual closeness we introduced in [START_REF] Bravetti | On the boundary between decidability and undecidability of asynchronous session subtyping[END_REF]. In the definition of ≤ we use the following notion of input context.

Definition 16 (Input Context

). An input context A is a session type with multiple holes defined by the syntax:

A ::= [ ] n | &{l i : A i } i∈I .
The holes [ ] n , with n ∈ N + , of an input context A are assumed to be consistently enumerated, i.e. there exists m ≥ 1 such that A includes one and only one [ ] n for each n ≤ m. Given types T 1 ,. . . , T m , we use A[T k ] k∈{1,...,m} to denote the type obtained by filling each hole k in A with the corresponding term T k .

Definition 17 (Asynchronous Subtyping, ≤). R is an asynchronous subtyping relation whenever it is dual closed and (T, S) ∈ R implies 1., 3., and 4. of Definition 15, plus the following modified version of 2.:

2. if T = ⊕{l i : T i } i∈I then ∃n ≥ 0, A such that -unfold n (S) = A[⊕{l j : S kj } j∈J k ] k∈{1,...,m} , -∀k ∈ {1, . . . , m}. I ⊆ J k and -∀i ∈ I, (T i , A[S ki ] k∈{1,...,m} ) ∈ R
T is an asynchronous subtype of S, written T ≤ S, if there is an asynchronous subtyping relation R such that (T, S) ∈ R.

We now explain the modified version of Rule 2. and its impact on the obtained subtyping relation. Concerning the adopted notation, for each hole k of the input context A (which is at the beginnig of the righthand term S after any needed unfolding), we take l j , with j ∈ J k , to be the labels of the output selection in the hole. Moreover, we use S kj to denote the type reached after output l j in the hole k. An important characteristic of asynchronous subtyping (formalized by Rule 2. above) is the following one. In a subtype output selections can be anticipated so to bring them before the input branchings that in the supertype occur in front of them. For example

⊕ l : &{l 1 : T 1 , l 2 : T 2 } ≤ & l 1 : ⊕{l : T 1 }, l 2 : ⊕{l : T 2 }
where the output selection with label l (occurring in the supertype) is anticipated w.r.t. the input branching with labels l 1 and l 2 (such an output selection is present in all its input branches). As already discussed in the Introduction, output anticipation reflects the fact that we are considering asynchronous communication protocols in which messages are stored in queues. In this setting, it is safe to replace a peer that follows a given protocol with another one following a modified protocol where outputs are anticipated: in fact, the difference is simply that such outputs will be stored earlier in the communication queue.

As a further example, consider the types T = µt.&{l : ⊕{l : t}} and S = µt.&{l : &{l : ⊕{l : t}}}. We have T ≤ S by considering an infinite subtyping relation including pairs (T , S ), with S being &{l : S}, &{l : &{l : S}}, &{l : &{l : &{l : S}}}, . . . ; that is, the effect of each output anticipation is that a new input &{l : } is accumulated in the initial part of the r.h.s. It is worth to observe that every accumulated input &{l : } is eventually consumed in the simulation game (orphan message freedom), but the accumulated inputs grows unboundedly.

Undecidability of Asynchronous Subtyping

The proof of undecidability of the asynchronous subtyping relation, taken from [START_REF] Bravetti | Undecidability of asynchronous session subtyping[END_REF], is by reduction from the acceptance problem for queue machines.

Definition 18 (Queue machine). A queue machine M is defined by a sixtuple (Q, Σ, Γ, $, s, δ) where: Q is a finite set of states; Σ ⊂ Γ is a finite set denoting the input alphabet; Γ is a finite set denoting the queue alphabet (ranged over by A, B, C, X); $ ∈ Γ -Σ is the initial queue symbol; s ∈ Q is the start state; δ : Q × Γ → Q × Γ * is the transition function.

We now formally define queue machine computations.

Definition 19 (Queue machine computation). A configuration of a queue machine is an ordered pair (q, γ) where q ∈ Q is its current state and γ ∈ Γ * is the queue (Γ * is the Kleene closure of Γ ). The starting configuration on an input string x is (s, x$). The transition relation → M over configurations Q × Γ * , leading from a configuration to the next one, is defined as follows. For any p, q ∈ Q, A ∈ Γ and α, γ ∈ Γ * we have (p, Aα) → M (q, αγ) whenever δ(p, A) = (q, γ). A machine M accepts an input x if it eventually terminates on input x, i.e. it reaches a blocking configuration with the empty queue (notice that, as the transition relation is total, the unique way to terminate is by emptying the queue). Formally, x is accepted by M if (s, x$) → * M (q, ) where is the empty string and → * M is the reflexive and transitive closure of → M .

Queue machines are Turing complete, see [START_REF] Kozen | Automata and computability[END_REF] (page 354) and [START_REF] Bravetti | Undecidability of asynchronous session subtyping[END_REF].

Our goal is to construct a pair of types, say T and S, from a given queue machine M and a given input x, such that: T ≤ S if and only if x is not accepted by M . Intuitively, type T encodes the finite control of M , i.e., its transition function δ, starting from its initial state s. And type S encodes the machine queue that initially contains x$, where x is the input string x = X 1 • • • X n of length n ≥ 0. The set of labels L for such types T and S is M 's queue alphabet Γ .

Formally, the queue of a machine is encoded into a session type as follows:

Definition 20 (Queue Encoding). Let M = (Q, Σ, Γ, $, s, δ) be a queue machine and let

C 1 • • • C m ∈ Γ * , with m ≥ 0. We define: [[C 1 • • •C m ]] = &{C 1 : . . . &{C m : µt. ⊕ {A : &{A : t}} A∈Γ }} Given a configuration (q, γ) of M , the encoding of the queue γ = C 1 • • • C m is thus defined as [[C 1 • • • C m ]]. A 1 ? A k ! ..... $? X 1 ? X n ? ..... A 1 ! A k ? Fig. 1. Session type encoding the initial queue X 1 • • • X n $
Note that whenever m = 0, we have [[ ]] = µt. ⊕ {A : &{A : t}} A∈Γ . Observe that we are using a slight abuse of notation: in both output selections and input branchings, labels l A , with A ∈ Γ , are simply denoted by A.

Figure 1 contains a graphical representation of the queue encoding with its initial content X 1 • • • X n $. In order to better clarify our development, we graphically represent session types as labeled transition systems (in the form of communicating automata [START_REF] Brand | On communicating finite-state machines[END_REF]), where an output selection ⊕{l i : T i } i∈I is represented as a choice among alternative output transitions labeled with "l i !", and an input branching &{l i : T i } i∈I is represented as a choice among alternative input transitions labeled with "l i ?". Intuitively, we encode a queue containing symbols C 1 • • • C m with a session type that starts with m inputs with labels C 1 , . . . , C m , respectively. Thus, in Figure 1

, we have C 1 • • • C m = X 1 • • • X n $.
After such sequence of inputs, representing the current queue content, there is a recursive type representing the capability to enqueue new symbols. Such a type repeatedly performs an output selection with one choice for each symbol A i in the queue alphabet Γ (with k being the cardinality of Γ ), followed by an input labeled with the same symbol A i .

We now give the definition of the type modelling the finite control of a queue machine, i.e., the encoding of the transition function δ.

Definition 21 (Finite Control Encoding). Let M = (Q, Σ, Γ, $, s, δ) be a queue machine and let q ∈ Q and S ⊆ Q. We define:

[[q]] S =    µq.&{A : ⊕{B A 1 : • • • ⊕ {B A n A : [[q ]] S∪q }}} A∈Γ if q ∈ S and δ(q, A) = (q , B A 1 • • • B A n A ) q if q ∈ S
The encoding of the transition function of M is then defined as

[[s]] ∅ .
The encoding of the finite control is a recursively defined term with one recursion variable q for each state q ∈ Q of the machine. Above, [[q]] S is a function that, given a state q and a set of states S, returns a type representing the possible behaviour of the queue machine starting from state q. Such behaviour consists of first reading from the queue (input branching on A ∈ Γ ) and then writing on the queue a sequence of symbols B A 1 , . . . , B A n A . The parameter S is necessary for

A 1 ? A k ? B 1 ! ..... B 1 ! B k ! ..... B k ! ..... q [[ ] ] q 1 [[ ] ] q k [[ ] ] 1 1 n k n 1 (for Γ = {Ai|i ≤ k} and δ(q, Ai) = (qi, B i 1 • • • B i n i ) for every i)
Fig. 2. Session type encoding a finite control.

managing the recursive definition of this type. In fact, as the definition of the encoding function is itself recursive, this parameter keeps track of the states that have been already encoded (see example below). In Figure 2, we report a graphical representation of the Labelled Transition System corresponding to the session type that encodes the queue machine finite control, i.e. the transition function δ. Each state q ∈ Q is mapped onto a state [[q]] of a session type, which performs an input branching with a choice for each symbol in the queue alphabet Γ (with k being the cardinality of Γ ). Each of these choices represents a possible symbol that can be read from the queue. After this initial input branching, each choice continues with a sequence of outputs labeled with the symbols that are to be inserted in the queue (after the symbol labeling that choice has been consumed). This is done according to function δ, assuming that δ(q

, A i ) = (q i , B i 1 • • • B i ni )
, with n i ≥ 0, for all i in {1, . . . , k}. After the insertion phase, state [[q i ]] of the session type corresponding to state q i of the queue machine is reached.

Notice that, queue insertion actually happens in the encoding because, when the encoding of the finite control performs an output of a B symbol, the encoding of the queue must mimic such an output, possibly by anticipating it. This has the effect of adding an input on B at the end of the sequence of initial inputs of the queue machine encoding. Theorem 6. Given a queue machine M = (Q, Σ, Γ, $, s, δ), an input string x, and the two types T = [[s]] ∅ and S = [[x$]], we have that M accepts x iff T ≤ S.

Decidability of Single-Out/Single-In Asynchronous Subtyping

We now show decidability of asynchronous session subtyping over single-out/ single-in session types. The full technical machinery can be found in [START_REF] Bravetti | On the boundary between decidability and undecidability of asynchronous session subtyping[END_REF].

We start by giving a procedure (an algorithm that does not necessarily terminate) for the general subtyping relation, which we showed to be undecidable. Such a procedure is inspired by the one proposed by Mostrous et al. [START_REF] Mostrous | Global principal typing in partially commutative asynchronous sessions[END_REF] for asynchronous subtyping in multiparty session types. In order to do so, we introduce two functions on the syntax of types. The function outDepth calculates how many unfolding are necessary for bringing an output outside a recursion. If that is not possible, the function is undefined (denoted by ⊥). As an example consider, for any T 1 and T 2 , outDepth(⊕{l 1 : T 1 , l 2 : T 2 }) = 0. On the other hand, consider the type T ex = & l 1 : µt. ⊕ l 2 : T 1 , l 3 : µt.& l 4 : µt . ⊕{l 5 : T 2 } : we have, outDepth T ex = 2. We then define outUnf(), a variant of the unfolding function given in Definition 14, which unfolds only where it is necessary, in order to reach an output. The function above differs from unfold n : for example, unfold 2 T ex would unfold twice both subterms µt. ⊕{l 2 : T 1 } and µt.& l 4 : µt . ⊕{l 5 : T 2 } . On the other hand, applying outDepth to the same term would unfold once the term reached with l 1 and twice the one reached with l 3 . In the subtyping procedure defined below we make use of outUnf() in order to have that recursive definitions under the scope of an output are never unfolded. This guarantees that during the execution of the procedure, even if the set of reached terms could be unbounded, all the subterms starting with an output are taken from a bounded set of terms. This is important to guarantee termination of the algorithm that we are going to define as an extension of the procedure described below.

Subtyping Procedure. An environment Σ is a set containing pairs (T, S), where T and S are types. Judgements are triples of the form Σ T ≤ a S which intuitively read as "in order to succeed, the procedure must check whether T is a subtype of S, provided that pairs in Σ have already been visited". Our subtyping procedure, applied to the types T and S, consists of deriving the state space of our judgments using the rules in Figure 3 bottom-up starting from the initial judgement ∅ T ≤ a S. More precisely, we use the transition relation Σ T ≤ a S → Σ T ≤ a S to indicate that if Σ T ≤ a S matches the conclusions of one of the rules in Figure 3, then Σ T ≤ a S is produced by the corresponding premises. The procedure explores the reachable judgements according to this transition relation. We give highest priority to rule Asmp, thus ensuring that at most one rule is applicable. 4 The idea behind Σ is to avoid cycles when dealing with recursive types. Rules RecR 1 and RecR 2 deal with the case in which the type on the right-hand side is a recursion and must be unfolded. If the type on the left-hand side is not an output then the procedure simply adds the current pair to Σ and continues. On the other hand, if an output must be found, we apply RecR 1 which checks whether such output is available. Rule Out allows nested outputs to be anticipated (when not under recursion) and condition A = [ ] 1 ⇒ ∀i ∈ I.& ∈ T i (inspired by [START_REF] Chen | On the preciseness of subtyping in session types[END_REF]) makes sure there are no orphan messages. In fact, this condition implies that if there is some output which is anticipated in the subtype w.r.t. some inputs, in every continuation of the subtype there are input actions that will eventually reproduce also the input behaviour of the supertype. The remaining rules are self-explanatory. Σ T ≤ a S → * Σ T ≤ a S is the reflexive and transitive closure of the transition relation among judgements. We write Σ T ≤ a S → ok if the judgement Σ T ≤ a S matches the conclusion of one of the axioms Asmp or End, and Σ T ≤ a S → err to mean that no rule can be applied to Σ T ≤ a S. Due to input branching and output selection, the rules In and Out could generate branching also in the state space Figure 3, where ≤ a is replaced by ≤ t , plus the following additional rule: S ∈ reach(Z) antOutInf(S) |γ| < |β| leafSet(antOut(S, γ)) = leafSet(antOut(S, β)) Σ, (T, antOut(S, γ)) T ≤ t antOut(S, β) Asmp2

Intuitively, we have that this additional termination rule guarantees to catch all those cases where the term on the right grows indefinitely, by anticipating outputs and accumulating inputs. These infinitely many distinct types are anyway obtainable starting from the finite set reach(Z), by means of output anticipations. Hence there exists S ∈ reach(Z) that can generate infinitely many of these types: this guarantees antOutInf(S) to be true. As observed above, the leaves of such infinitely many terms are themselves taken from the finite set reach(Z).

In Section 2 we have commented that multiset inclusion is a wqo over multisets defined on a finite domain; here we use a similar result according to which set equality is a wqo over the subsets of a finite given set. In fact, the possible subsets in this case are finite thus in an infinite sequence of such subsets at least one is repeated. The termination of our algorithm follows this wqo: Asmp2, besides checking conditions that are guaranteed to hold if the procedure ≤ a continues indefinitely, checks also for the equality between the set of leaves of the r.h.s. term in the current judgement and in a previously checked one.

Theorem 7 (Decidability for Single-out Types). Asynchronous subtyping ≤ over single-out session types is decidable.

Exploiting dual closeness of ≤ we can use the algorithm presented for single-out types also for single-in types (it is sufficient to check subtyping on the duals, observing that the dual of a single-in type is single-out).

Corollary 1 (Decidability for Single-in Types). Asynchronous subtyping ≤ over single-in session types is decidable.

Conclusion

In this survey paper we have recalled the main results related with two lines of research on the expressiveness of Linda-like coordination models and on the theory of behavioural contracts. In the third part of the paper, we have discussed how the techniques developed for Linda-like coordination have recently contributed to the advancement of the research in the context of session types for asynchronous communication. Session types, which can be seen as a simplification of contracts, already had a wide application on concurrent programming languages, as, e.g., Haskell [START_REF] Lindley | Embedding session types in haskell[END_REF], Go [START_REF] Ng | Static deadlock detection for concurrent go by global session graph synthesis[END_REF] and Rust [START_REF] Jespersen | Session types for Rust[END_REF].

We expect two possible lines for future work: on the one hand, analyse the impact on the theory of contracts of our results for session types (in fact, very few results are present in the literature about contracts for asynchronous communication) and, on the other hand, continue in the context of session types by investigating novel techniques for sound algorithmic characterizations of asynchronous session subtyping.

α

  ::= in(a) | out(a) | notify(a, P ) | tfa(a) P ::= i∈I α i .P i | !α.P | P |P

  , L → P , S, L (a, Q) P out(a) -→ P L = {(a, Pi)|i ∈ I} {(bj, Qj) | ∀j.bj = a} P, S, L → P | i∈I Pi, S a, L P tfa(a) -→ P a ∈ S P, S, L → P , S, L

Definition 7 (

 7 Output Persistence). Consider the following notation: C λ -→ means ∃C : C λ -→ C and, given a (possibly empty) sequence of labels w =

Table 2 .

 2 The reduction relation for systems (brackets in singletons are omitted).

The compatibility notion used in this paper is named strict compatibility in[START_REF] Finkel | Well-structured transition systems everywhere![END_REF].

As for basic CCS[START_REF] Milner | Communication and concurrency[END_REF] finite-stateness is an obvious consequence of the fact that the process algebra does not include static operators, like parallel or restriction.

Differently from our definitions, in the channel-based approach of Gay and Hole[START_REF] Gay | Subtyping for session types in the pi calculus[END_REF] subtyping is covariant on branchings and contra-variant on selections.

The priority of Asmp is sufficient because all the other rules are alternative, i.e., given a judgement Σ T ≤a S there are no two rules different from Asmp that can be both applied.

Fig. 3. A Procedure for Checking Subtyping to be explored by the procedure. Namely, given a judgement Σ T ≤ a S, there are several subsequent judgements Σ T ≤ a S such that Σ T ≤ a S → Σ T ≤ a S . The procedure could (i) successfully terminate because all the explored branches reach a successful judgement Σ T ≤ a S → ok , (ii) terminate with an error in case at least one judgement Σ T ≤ a S → err is reached, or (iii) diverge because no branch terminates with an error and at least one branch never reaches a succesful judgement. As we prove in [START_REF] Bravetti | On the boundary between decidability and undecidability of asynchronous session subtyping[END_REF] the procedure is sound with respect to asynchronous subtyping ≤ and it can diverge only if the checked types are in the ≤ relation.

If we consider types T and S of the example considered after Definition 17 the subtyping procedure in Figure 3 applied to ∅ T ≤ a S does not terminate. The problem is that the termination rule Asmp cannot be applied because the term on the r.h.s. (i.e. the supertype) generates always new terms in the form &{l : &{l : . . . &{l : S} . . . }}. Notice that, in this particular example, these infinitely many distinct terms are obtained by adding single inputs (i.e. singlechoice input branchings) in front of the term in the r.h.s.: we call this linear input accumulation. In general, however, input accumulation takes the form of a tree (thus accounting for all possible alternative accumulated input behaviors at the same time).

We now show how to decide asynchronous subtyping over single-out types, i.e. when input accumulation can indeed be in the general form of a tree, but, due to the absence of output selections with multiple choices, it gets accumulated in a deterministic (i.e. unique) way. This will also allow us to deal with single-in types by exploiting duality. As anticipated, it deals with general input accumulation by representing it as a tree. We need to be able to extract the leaves from these trees: this is done by the leaf set function. The leaf set of a session type T is the set of subterms reachable from its root through a path of inputs. For example, the leaf set of the term &{l 1 : µt. ⊕ {l 2 : t}, l 3 : &{l 4 : ⊕{l 2 : µt. ⊕ {l 2 : t}}}} is {µt. ⊕ {l 2 : t}, ⊕{l 2 : µt. ⊕ {l 2 : t}}.

During the check of subtyping, according to Figure 3 (rule Out), when a term in the r.h.s. having input accumulation has to mimic an output in front of the l.h.s., such output must be present in front of all the leaves of the tree. In this case, the checking continues by anticipating the output from all the leaves. We make use of an auxiliary output anticipation function, called antOut, that indicates the way a term changes after having anticipated a sequence of outputs. antOut(T, l) yields the term obtained from T by anticipating all outputs occurring in the sequence l. For example, the function applied to the type T = µt. ⊕ l 1 : &{l : ⊕{l 2 : t}, l : ⊕{l 2 : t} and the sequence (l 1 , l 2 ) returns &{l : T, l : T }, while it is undefined with the sequence (l 1 , l 1 ). Moreover, we say that T can infinitely anticipate outputs, written antOutInf(T ), if there exists an infinite sequence of labels

The definition of antOutInf(T ) is not algorithmic in that it quantifies on every possible natural number n. Nevertheless, it can be decided by checking whether, for every session type obtained from T by means of output anticipations, all the terms populating its leaf set can anticipate the same output label. Although the types that can be obtained from T by means of output anticipations may be infinite, the terms populating the leaf sets are finite and are over-approximated by the function reach(T ) which is defined as the minimal set of (single-out) session types such that:

1. T ∈ reach(T ); 2. &{l i : T i } i∈I ∈ reach(T ) implies T i ∈ reach(T ) for every i ∈ I; 3. µt.T ∈ reach(T ) implies T {µt.T /t} ∈ reach(T ); 4. ⊕{l : T } ∈ reach(T ) implies T ∈ reach(T ).

Notice that reach(T ) contains the session types obtained by consuming initial inputs and outputs, and by unfolding recursion when it is at the top level. Proposition 3. Given a single-out session type T , reach(T ) is finite and it is decidable whether antOutInf(T ).

Subtyping algorithm for single-out types. We are now ready to present an additional termination condition that, once included into the subtyping procedure in Figure 3, makes it a valid algorithm for checking subtyping for single-out types. The termination condition is defined as an additional rule, named Asmp2, that complements the already defined Asmp rule by detecting those cases in which the subtyping procedure in Figure 3 does not terminate (Asmp2, presented below, is assumed to have the same priority as rule Asmp: both rules have highest priority). The new rule is defined parametrically on the session type Z, which is the type on the right-hand side of the initial pair of types to be checked (i.e. the algorithm is intended to check V ≤Z, for some type Z). We start from the initial judgement ∅ V ≤ t Z and then apply from bottom to top the rules in