Luca Padovani

Deadlock and lock freedom in the linear π-calculus

published or not. The documents may come

Deadlock and lock freedom in the linear π-calculus

I. INTRODUCTION

The linear π-calculus [START_REF] Kobayashi | Linearity and the picalculus[END_REF] is a resource-aware model of communicating processes that distinguishes between linear and unlimited channels. Unlimited channels can be used without restrictions, while linear channels are meant to be used for exactly one communication. This intrinsic limitation is rewarded by several benefits, including specialized behavioral equivalences for reasoning about communication optimizations, the efficient implementation of linear channels, and the fact that communications on linear channels enjoy desirable properties such as determinism and confluence. The value of these benefits is amplified given that a significant fraction of channels in several actual systems happen to be linear.

From an operational standpoint, the linear π-calculus only guarantees that well-typed processes never communicate twice on the same linear channel. In practice, one may be interested in stronger guarantees, such as deadlock freedom [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF] -the absence of stable states with pending communications on linear channels -or lock freedom [START_REF] Kobayashi | A type system for lock-free processes[END_REF], [START_REF] Kobayashi | A hybrid type system for lock-freedom of mobile processes[END_REF] -the possibility to complete pending communications on linear channels. A paradigmatic example of deadlock is illustrated by the process a?(x).b! x | b?(y).a! y [START_REF] Bettini | Global progress in dynamically interleaved multiparty sessions[END_REF] where the left subprocess forwards on b the message x received from a, and the right subprocess forwards on a the message y received from b. The process (1) is well typed when a and b are linear channels, but none of the pending communications on a and b can complete because of the mutual dependencies between corresponding inputs and outputs. An example of lock which is not a deadlock is illustrated by the process

c! a | * c?(x).c! x | a! 1984 (2)
where one occurrence of the linear channel a is repeatedly sent over the unlimited channel c but never used for receiving the 1984 message. Note that (2), unlike [START_REF] Bettini | Global progress in dynamically interleaved multiparty sessions[END_REF], reduces forever, but the communication pending on a cannot be completed.

In this work we propose two refinements of the linear π-calculus such that well-typed processes are (dead)lock free. The techniques we put forward have been inspired by previous ideas presented in [START_REF] Kobayashi | A type system for lock-free processes[END_REF]- [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF], [START_REF] Kobayashi | A hybrid type system for lock-freedom of mobile processes[END_REF], except that by narrowing the focus on the linear π-calculus we obtain type systems that are not just technically simpler but also more accurate in establishing (dead)lock freedom of relevant processes.

In a nutshell, we consider channel types of the form p ι [t] n m where the polarity p (either input ? or output !), the type of the message (t), and the multiplicity (unlimited ω or linear 1), are just like in the linear π-calculus. In addition, we annotate channel types with two numbers, a priority n and m tickets.

Priorities enforce an order on the use of channels: when a process owns two or more channels at the same time, channels with higher priority must be used before channels with lower priority (beware that we adopt the convention that "higher priority" means "smaller number"). In particular, an input u?(x).P is well typed if u has higher priority than all the channels occurring in P and an output u! v is well typed if u has higher priority than v. This mechanism makes (1) ill typed: it is not possible to assign two priorities h and k to a and b, for the structure of the process requires the simultaneous satisfiability of the two constraints h < k and k < h.

Tickets limit the number of travels that channels can do: u! v is well typed if v has at least one ticket; each time a channel is sent as a message, one ticket is removed from its type; a channel with no tickets cannot travel and must be used directly for performing a communication. This mechanism makes [START_REF] Bono | Typing Copyless Message Passing[END_REF] ill typed, because a is sent on c infinitely many times and so it would need infinitely many tickets.

The technique described thus far prevents deadlocks (if we just consider the constraints on priorities) and locks (if we also consider the constraints on tickets). Unfortunately, it fails to type most recursive processes. For example, the usual encoding of the factorial below where, for convenience, we have annotated linear names with their priority, is ill typed: * fact?(x, y h ).

if x = 0 then y h ! 1 else (νa k )(fact! x -1, a k | a k ?(z).y h ! x × z )

Since the newly created channel a is used in the same position as y in the recursive invocation of fact, we are led into thinking that a and y should have the same type hence the same priority h = k. This clashes with the input on a that blocks the output on y, requiring k < h. We see a symmetric phenomenon in * stream?(x, y h ).(νa k )(

y h ! x, a k | stream! x + 1, a k ) (4)
which generates a stream of integers. Here too a and y are used in the same position and should have the same priority h = k, but the output y! x, a also requires h < k.

We need some way to overcome these difficulties. Let us digress for a moment from fact and stream and consider

F 1 def = c?(x h ).y k ! x h and F 2 def = c?(x h , y k ).y k ! x h
both of which forward a linear channel x received from c to the linear channel y. In both cases it must be k < h, but there is a key difference between F 1 and F 2 : the priority of x in F 1 has a fixed lower bound k + 1 because y is free, while the priority of x in F 2 is arbitrary, provided that k < h, because y is bound. Rephrased in technical jargon, c is monomorphic in F 1 and polymorphic in F 2 with respect to priorities. The fact that a channel like c is monomorphic or polymorphic depends on the presence or absence of free linear channels in the continuation that follows the input on c. Normally this information is not inferrable solely from the type of c, but it turns out that we can easily approximate it in the linear π-calculus, where replicated processes cannot have free linear channels because it is not known how many times they will run. So, unlimited channels that are always used for replicated inputs (i.e., replicated channels [START_REF] Kobayashi | Linearity and the picalculus[END_REF]), are polymorphic. This is a very convenient circumstance, because replicated channels are the primary mechanism for implementing recursion. Indeed, going back to fact and stream, we see that they are replicated channels, that is they are polymorphic. This means that the mismatches between the priorities h of y and k of a in ( 3) and ( 4) can be compensated by this form of polymorphism and these processes can be declared well typed.

The interplay between recursion and polymorphism leads to a technical problem, though. Recall that in (4) there are two occurrences of a, one in stream! x + 1, a having the same type as y but lower priority and another in y! x, a with a similar type, but opposite (input) polarity. Overall we realize that the type t of y should satisfy the equations

t = ![int × t 1 ] 1 t 1 = ?[int × t 2 ] 2 t 2 = ?[int × t 3 ] 3 . . . ( 5
)
where t 1 would be the type of a in y! x, a (for the sake of readability we omit tickets). The problem is that t is not a regular type and therefore cannot be finitely represented by means of the well-known µ notation [START_REF] Courcelle | Fundamental properties of infinite trees[END_REF]. To recover a finite representation for t, we "relativize" priorities. In particular, we postulate that t should satisfy the equations

t = ![int × s] 1 s = ?[int × s] 1
and that messages sent on a channel of type t must have type int×s (as written in t) but with priorities shifted up by 1 (the priority of t). Below we illustrate such shifting, which turns relative priorities (within channel types) into absolute ones:

channel type t ![ int × s ] 1 message type int × ?[ int × s ] 1 + 1 shifted by int × ?[ int × s ] 1 + 2
Note that int is not affected by the shifting because it is not a linear type and that overall the channel types in this sequence are the same t 1 , t 2 , . . . that we initially guessed in [START_REF] Castagna | On Global Types and Multi-Party Sessions[END_REF], except that now t and s are regular hence finitely representable. Summary of contributions. We strengthen the notion of linearity in the linear π-calculus by defining two type systems ensuring the absence of deadlocks and locks involving linear channels, namely that linear channels are used exactly once as opposed to at most once. We exploit the features of the linear π-calculus to devise a form of channel polymorphism that allows us to deal with recursive processes that interleave actions on different linear channels also in cyclic network topologies. Such configurations are common in the implementation of parallel algorithms and session-based networks, and cannot be dealt with existing type systems for the generic π-calculus [START_REF] Kobayashi | A type system for lock-free processes[END_REF]- [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF]. Outline. In Section II we quickly review syntax and semantics of the π-calculus and give formal definitions of deadlock and lock freedom. The type systems are described in Section III and illustrated on several examples that highlight the features of our approach. Section IV contains a more detailed and technical comparison with related work and particularly with [START_REF] Kobayashi | A type system for lock-free processes[END_REF]- [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF]. Section V concludes and hints at ongoing and future developments. Additional technical material, extended examples, and proofs of the results can be found in the appendix, which is not formally part of the submission.

II. LANGUAGE

We use integer numbers h, k, . . . , m, n, . . . , a countable set of variables x, y, . . . , and a countable set of channels a, b, . . . ; names u, v, . . . are either channels or variables. Expressions e, . . . and processes P , Q, . . . are defined by: e ::= n u (e, e) inl e inr e P ::= 0 u?(x).P * u?(x).P u! e (P | Q) (νa)P let x, y = e in P case e {i x i ⇒ P i } i=inl,inr Expressions are integers, names, pairs of expressions, or expressions injected using either inl or inr. Values v, w, . . . are expressions without variables. Processes are the usual terms of the π-calculus enriched with pattern matching for pairs and injected values. In particular, let x, y = e in P deconstructs the value of e, which must be a pair, and continues as P where x and y have been respectively replaced by the first and second component of the pair. A process case e {i x i ⇒ P i } i=inl,inr evaluates e, which must result into a value (i v) where i ∈ {inl, inr}, and continues as P i where x i has been replaced by v. Binders are as expected, in particular let x, y = e in P , binds both x and y in P , and case e {i x i ⇒ P i } i=inl,inr binds x i in P i . The notions of free and bound names of a process P , respectively denoted by fn(P ) and bn(P ), are defined consequently. In the following we write (νã) for sequences of restrictions and we use polyadic inputs u?(x 1 , . . . , x n ) as an abbreviation for monadic input of (possibly nested) pairs followed by (possibly nested) pair deconstructions using let's. For example, u?(x, y).P abbreviates u?(z).let x, y = z in P for some fresh z.

The operational semantics is defined by a combination of structural congruence ≡ and a reduction relation →. The former is the same as in the π-calculus, except that we do not include the law * P ≡ P | * P because we treat replicated inputs in a special way. Reduction is defined by the rules below a! v | a?(x).P → P {v/x} a! v | * a?(x).P → P {v/x} | * a?(x).P let x, y = v, w in P → P {v, w/x, y} case k v {i x i ⇒ P i } i=inl,inr → P k {v/x k } and closed by reduction contexts C ::

= [ ] | (C | P ) | (νa)C
and structural congruence. The rules are unremarkable and P {v/x} is the usual capture-avoiding substitution of v in place of the free occurrences of x in P . We write → * for the reflexive, transitive closure of → and P → if there is no Q such that P → Q. We say that P is stable if P →.

To formulate deadlock and lock freedom, we need a few predicates that describe the pending communications of a process P with respect to some channel a: in(a, P )

def ⇐⇒ P ≡ C [a?(x).Q] ∧ a ∈ bn(C ) * in(a, P ) def ⇐⇒ P ≡ C [ * a?(x).Q] ∧ a ∈ bn(C ) out(a, P ) def ⇐⇒ P ≡ C [a! e ] ∧ a ∈ bn(C ) sync(a, P ) def ⇐⇒ (in(a, P ) ∨ * in(a, P )) ∧ out(a, P ) wait(a, P ) def ⇐⇒ (in(a, P ) ∨ out(a, P )) ∧ ¬sync(a, P )
In words, in(a, P ) holds if there is a sub-process Q within P that is waiting for a message from a (it is similar to the live predicate in [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF]). Note that, by definition of reduction context, the input is not guarded by other actions. The condition a ∈ bn(C ) means that a occurs free in P . The predicates out(a, P ) and * in(a, P ) are similar, but they regard outputs and replicated inputs, respectively. Whenever one of in(a, P ) or out(a, P ) holds, there is some pending input/output operation (we do not interpret * in(a, P ) as a pending communication, because we do not require that a replicated input process should run infinitely often). This discussion explains the sync(a, P ) and wait(a, P ) predicates: the first one denotes the fact that there are pending input/output operations on a, but a synchronization on a is immediately possible; the second one denotes the fact that there is a pending output or a pending non-replicated input on a, but no immediate synchronization on a is possible. Note that pending outputs trigger the wait predicate even when they regard unlimited channels. This is because such outputs may carry messages containing linear channels and in order to guarantee deadlock freedom we must be sure that all outputs, including those on unlimited channels, can be completed and the messages delivered. For this reason we treat unlimited channels as replicated channels and enforce input receptiveness for them. On the contrary, replicated inputs, which can be though of as persistently available servers, do not trigger the wait predicate because, by definition, they are not allowed to have free linear channels (the type system will enforce this property).

We define deadlock freedom as the absence of stable states with pending communications and lock freedom as the ability to eventually complete any pending communication. Formally: Definition II.1 (deadlock [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF] and lock freedom [START_REF] Kobayashi | A hybrid type system for lock-freedom of mobile processes[END_REF]).

1) We say that P is deadlock free if for every Q such that P → * (νã)Q → we have ¬wait(a, Q) for every a. 2) We say that P is lock free if for every Q such that P → * (νã)Q and wait(a, Q) there exists R such that Q → * R and sync(a, R).

For example, both (νa)a! 1984 and (νa)a?(x).P are deadlocks, whereas (νa) * a?(x).P is lock free. In principle, we should also require that let and case processes are always able to reduce and that expressions in top-level outputs are always evaluated. These properties are already guaranteed (for closed processes) by conventional type systems for the π-calculus, so we keep Definition II.1 focused on pending communications. Note that lock freedom implies deadlock freedom, but not viceversa (process (2) is deadlock free but not lock free).

Example II.2. Many parallel algorithms (Jacobi and Gauss-Seidel, leader election, vertex coloring, just to mention a few) use batteries of processes that iteratively communicate with their neighbors. To maximize parallelism, communication is full-duplex, that is processes simultaneously send messages to each other. For instance, the process

Node A def = * c A ?(x, y).(νa)(x! a | y?(z).c A ! a, z )
uses a channel x for sending messages to, and another channel y for receiving messages from, a neighbor process. Each message sent on x carries a payload (omitted) as well as a continuation channel a with which Node A communicates with its neighbor at the next iteration. Symmetrically, each message received from y contains the neighbor's payload (omitted) and continuation z. The use of fresh continuations at each iteration makes sure that messages are received in the desired order. An alternative modeling using half-duplex communication is

Node B def = * c B ?(x, y).y?(z).(νa)(x! a | c B ! a, z )
where the process first waits for the message from its neighbor, and only then sends its own information. It may then be relevant to understand whether a given configuration consisting of mixed nodes, some of type A and others of type B, is lock free. Below we represent three of them

L 1 (X) def = Node A | Node B | c X ! e, e L 2 (X, Y) def = Node A | Node B | c X ! e, f | c Y ! f, e L 3 (X, Y, Z) def = Node A | Node B | c X ! e, f | c Y ! g, e | c Z ! f, g
where each of X, Y, and Z can be either A and B to yield a different configuration. For example, we have

L 2 (B, B) → * Node A | Node B | f ?(z).(νa)(e! a | c B ! a, z ) | e?(z).(νb)(f ! a | c B ! b, z ) →
and the final configuration satisfies the in predicate but not out for both e and f , namely L 2 (B, B) is not lock free. We will see later that a given configuration L i is lock free if and only if at least one of its nodes is of type A.

III. TYPE SYSTEM

Notation. Polarities p, q, . . . are subsets of {?, !}. We abbreviate {?} with ?, {!} with !, and {?, !} with # and we say that ∅ and # are even polarities. Multiplicities ι, . . . are either 1 or ω. We also use a countable set of type variables α, . . . . Types t, s, . . . are defined by the grammar below:

t ::= int α t × s t ⊕ s p ι [t] n m µα.t
The types int, t × s, and t ⊕ s respectively denote integers, pairs inhabited by values (v, w) where v has type t and w has type s, and the disjoint sum of t and s inhabited by values (inl v) when v has type t or (inr w) when w has type s. The type p ι [t] n m denotes a channel to be used with polarity p and multiplicity ι for exchanging messages of type t. The polarity determines the operations allowed on the channel: ∅ means none, ? means input, ! means output, and # means both. The multiplicity determines how many times the channel can or must be used: 1 means that the channel must be used exactly once (for each element in p), while ω means that the channel can be used any number of times. The numbers n and m are respectively the priority and the tickets of the channel. As we have anticipated in Section I, priorities are used for imposing an order on the usage of channels, so that an action on a channel with low priority cannot block another action on a channel with higher priority. Recall that smaller numbers denote higher priorities, so for example an input on a channel with priority 4 can block an input on a channel with priority 5, but not viceversa. The tickets of a channel limit the number of times the channel can be sent in a message. For example, a channel with 3 tickets can be sent at most three times in a message, but it can be used at any time for an input/output operation according to its polarity. A channel with no tickets cannot be sent in a message. Tickets are always non-negative. We omit priority and tickets when ι = ω and the multiplicity when it is 1. Also, we often omit tickets when there is none. We use type variables and µ's for building recursive types. Notions of free and bound type variables are as expected. Contractiveness. For simplicity, we forbid non-contractive types in which recursion variables are not guarded by a channel type. For example, µα.α and µα.(α × α) are illegal while µα.p ι [α] n m is allowed. In this way, we will be able to define functions by induction on the structure of types, when such functions do not recur within channel types. Contractiveness can be weakened without compromising the results that follow, but some functions on types must be defined more carefully. The formal definition of contractiveness can be found in the appendix. We identify two types modulo renaming of bound type variables and if they have the same infinite unfolding, that is if they denote the same (regular) tree [START_REF] Courcelle | Fundamental properties of infinite trees[END_REF]. In particular, we have µα.t = t{µα.t/α}. Priorities and tickets. The priority of a channel gives a measure to the urgency with which the channel must be used: the higher the priority is, the sooner the channel must be used. This measure can be extended from channels to arbitrary types, the idea being that the priority of a type is the highest of the priorities of the channel types occurring therein. To compute the priority of a type, we define an auxiliary function | • | such that |t| is an element of Z ∪ {⊥, } where ⊥ < n < for every n ∈ Z. The function is defined inductively thus:

|t| def =        ⊥ if t = p ω [s] and ? ∈ p n if t = p[s] n m and p = ∅ min{|t 1 |, |t 2 |} if t = t 1 × t 2 or t = t 1 ⊕ t 2 otherwise (6)
Intuitively, unlimited channels with input polarity have the highest priority ⊥ (first equation) because their use cannot be postponed by any means to guarantee input receptiveness. Numbers, unlimited channels with only output polarity, and linear channels with empty polarity have the lowest priority (last equation) because they do not affect (dead)lock freedom in any way. Linear channels with pending operations must be used according to their priority (second equation). The priority of compound types is the highest (numerically speaking, the minimum) of the priorities of the component types (third equation). For instance, |!

[t] 3 1 × ?[s] 2 4 | = min{|![t] 3 1 |, |?[s] 2 4 |} = min{3, 2} = 2.
We say that a (value with

) type t is unlimited if |t| = , that it is linear if |t| ∈ Z, that it is relevant if |t| = ⊥.
We define another auxiliary function $ h k to shift priorities and tickets: $ h k t has the same structure of t, except that all priorities/tickets in the topmost linear channel types of t have been transposed by h and k respectively. Formally:

$ h k t def =        p[s] n+h m+k if t = p[s] n m and p = ∅ ($ h k t 1 ) × ($ h k t 2 ) if t = t 1 × t 2 ($ h k t 1 ) ⊕ ($ h k t 2 ) if t = t 1 ⊕ t 2 t otherwise (7)
As an example, we have

$ 1 1 (int × ?[int] 3 ) = ($ 1 1 int) × ($ 1 1 ?[int] 3 ) = int × ?[int] 4 1 .
Note that positive/negative shifting respectively corresponds to decreasing/increasing the priority. We write $ n for $ n 0 . A key property used in the proof of subject reduction is that shifting behaves like the identity on unlimited types: Lemma III.1. If t is unlimited, then $ h k t = t for any h, k. Monomorphic and polymorphic channels. A distinguishing feature of our type systems is that message types are "relative" to the priority of the channels on which they travel. We use shifting to compute the absolute type of messages that can be sent on a channel. For example, a channel whose type is ![s] h accepts messages of type $ h s, that is the type s (in the type t of the channel) where all top-level priorities have been shifted by h (the priority of the channel). As we have seen in Section I, this feature allows us to work with finite representations of recursive types having infinitely many different priorities. For example, a recursive type that satisfies the equation t = ![t] 1 denotes a linear channel on which it is possible to send a message of type ![t] 2 . In turn, on such a channel it is possible to send a message of type ![t] 3 , and so on and so forth.

Shifting is also used to implement polymorphism. For example, an unlimited (i.e., polymorphic) channel of type ! ω [s] accepts messages of type $ h s for any h. So, for linear (i.e., monomorphic) channels, the shifting is fixed and determined by the priority of the channel, while for unlimited (i.e., polymorphic) channels, the shifting is arbitrary.

We are aware that this way of realizing polymorphism, as opposed to e.g. using "priority variables", is sometimes more restrictive than necessary. For example, a channel of type

! ω [?[int] 1 × ![int] 0 ] accepts messages of type $ h (?[int] 1 × ![int] 0 ) = ?[int] h+1 × ![int] h for every h, but not messages of type ?[int] h+2 × ![int] h
where the first component of the pair has been shifted by h+1 and the second component of the pair only by h. A message of the latter type could be safely sent on the unlimited channel c appearing in the process F 2 of Section I. The type systems allow more flexible forms of polymorphism (see Section V). Type environments. We check that processes are well typed in type environments Γ , . . . , which are finite maps from names to types written u 1 : t 1 , . . . , u n : t n . We write dom(Γ ) for the domain of Γ , namely the set of names for which there is a binding in Γ , and Γ , Γ for the union of Γ and Γ when dom(Γ )∩ dom(Γ ) = ∅. In general we need a more flexible way of composing type environments, taking into account the linearity and relevance of types and the fact that we can split channel types by distributing different polarities to different processes. Following [START_REF] Kobayashi | Linearity and the picalculus[END_REF], we define a partial composition operator + between types, thus:

t + t = t if t is unlimited p ω [t] + q ω [t] = (p ∪ q) ω [t] p[s] n h + q[s] n k = (p ∪ q)[s] n h+k if p ∩ q = ∅ (8)
Informally, unlimited types compose with themselves without restrictions. The composition of two unlimited/relevant channel types has the union of their polarities. Two linear channel types can be composed only if they have the same priority and disjoint polarities, and the composition has the union of their polarities and the sum of their tickets. We extend the partial operator + to type environments, thus:

Γ + Γ def = Γ , Γ if dom(Γ ) ∩ dom(Γ ) = ∅ (Γ , u : t) + (Γ , u : s) def = (Γ + Γ ), u : t + s (9) Note that Γ + Γ is undefined if there is u ∈ dom(Γ ) ∩ dom(Γ ) such that Γ (u)+Γ (u) is undefined and that dom(Γ + Γ ) = dom(Γ ) ∪ dom(Γ ).
We write un(Γ ) if all the types in the range of Γ are unlimited. We let |Γ | denote the maximum priority of the types in the range of Γ , that is

|Γ | = min{|Γ (u)| | u ∈ dom(Γ )}.
Typing rules. The typing rules for expressions and processes are presented in Table 1. A judgment Γ e : t denotes that e is well typed and has type t in Γ and a judgment Γ k P denotes that P is well typed in Γ . The only difference between the type systems for deadlock and lock freedom is the "cost" k of travels for linear channels, which is 0 for deadlock freedom and 1 for lock freedom. This parameter affects only the rules for outputs, and is always propagated unchanged by all rules.

Rules for expressions as well as [T-IDLE], [T-PAR], [T-LET], and [T-CASE

] are standard for the linear π-calculus, with the usual splitting of environments and the requirement that unused environments in axioms must be unlimited.

Rule [T-IN] is used for typing linear inputs u?(x).P , where u must have type ?[t] n m . The continuation P is typed in an environment where the input polarity of u has been removed and the received message x has been added. Note that the type of x is not just t, but t shifted by n, consistently with the relative interpretation of priorities of message types. The tickets are irrelevant since u is used for an input operation, not as the content of a message. The condition n < |Γ | verifies that the input on u does not block operations on other channels with equal or higher priority. In particular, Γ cannot contain relevant channels. Below are some typical examples of illtyped processes that violate this condition:

• a : ?[int] 1 , b : ![int] 0
k a?(x).b! x is not derivable because 1 < 0: the input on a blocks the output on b, but b has higher priority than a;

• a : #[int] h k a?(x)
.a! x is a degenerate case of the previous example, where the input on a blocks the very output that should synchronize with it. Note that this process is well typed in the traditional linear π-calculus because #

[int] = ?[int] + ![int]; • a : ?[int] h , c : ? ω [int] k a?(x). * c?(y) is not derivable because |? ω [int]| = ⊥.
To guarantee input receptiveness, replicated inputs cannot be guarded by other operations. Rule [T-OUT] is used for typing linear outputs on channels of type ![t] n m . The type of the message e must be t (as specified in the type of the channel u) shifted by n again since t is relative to the priority of u. The tickets are shifted by 1, but only for lock freedom (k = 1). The meaning is that, by sending e as a message, one ticket from every linear channel type in the type of e is consumed. This prevents the degenerate phenomenon of infinite delegation that we have seen in [START_REF] Bono | Typing Copyless Message Passing[END_REF]. The condition 0 < |t| verifies that the priority of the message is lower (i.e., numerically greater) than that of the channel on which it travels. Below are three examples:

• The judgment a : ![?[int] 1 0 ] 2 0 , b : ?[int] 3 1 1 a! b is derivable because ?[int] 3 1 = $ 2 1 ?[int] 1 0 .
Note in particular that the channel to be sent on a must have no tickets, which is in fact what happens to b after 1 ticket is consumed from its type before it travels on a.

• The judgment a :

?[![int] 2 0 ] 0 0 , b : ![![int] 1 0 ] 1 0 1
a?(x).b! x is not derivable, because x received from a has no tickets so it cannot travel on b.

• Let t = µα.?[α] 0 and observe that #[t] 1 = ![t] 1 + ?[t] 1 .
The judgment a : #[t] 1 0 a! a is not derivable, despite the message a has the "right" type ?[t] 1 = $ 1 t, because the condition 0 < |t| = 0 is not satisfied. According to Definition II.1, a process like (νa)a! a is deadlock. (there are systems in which such process actually reduces, but in doing so it generates memory leaks [START_REF] Bono | Typing Copyless Message Passing[END_REF]).

Rule [T-IN*

] is used for typing replicated inputs * u?(x).P . This rules differs from [T-IN] in three important ways. First of all, u must be an unlimited channel with input polarity. Second, the residual environment Γ must be unlimited, because the continuation P can be spawned an arbitrary number of times. Third, it may be the case that u ∈ dom(Γ ), because [START_REF] Coppo | Global progress for dynamically interleaved multiparty sessions[END_REF] and ! ω [t] is unlimited. This means that replicated input processes may invoke themselves, as we have seen in many examples.

? ω [t] + ! ω [t] = # ω [t] according to
Rule [T-OUT*] is used for outputs on unlimited channels. There are two key differences with respect to [T-OUT]. First, the condition ⊥ < |t|, where t is the type of x, implies that only relevant names cannot be communicated, but a process like a! a is well typed when a is unlimited, for example by giving the inner a type µα.! ω [α]. Second, the type of the message need not match exactly the type t in the channel, but its priority can be shifted by an arbitrary amount n. This is the technical realization of polymorphism. In particular, each distinct output on u can shift the type of the message by a different amount, therefore allowing polymorphic recursion. We will see this feature at work Example III. [START_REF] Cécé | Verification of programs with half-duplex communication[END_REF].

Rule [T-NEW] is used for restricting new (linear and unlimited) channels. Only channels with an even polarity can be restricted: either the channel comes with full polarity #, or with no polarity ∅ (this is only useful for subject reduction).

We write DF P if ∅ 0 P and LF P if ∅ 1 P and all priorities in the derivation are non-negative. Intuitively, the type system for deadlock freedom ignores tickets because infinite delegations (like in (2)) are not deadlocks, while the type system for lock freedom requires a well-founded order on priorities (hence the restriction to natural numbers) and an upper bound on delegations (hence the importance of tickets).

Properties. The relative interpretation of priorities makes it possible to shift whole derivations and preserve typing. More precisely, let $ n Γ be the environment obtained by shifting all the types in the range of Γ by n, that is ($ n Γ )(u) = $ n Γ (u) for every u ∈ dom(Γ ). We have: Lemma III.2 (shifting). The following properties hold:

1) If Γ e : t, then $ n Γ e : $ n t.

2) If Γ 0 P , then $ n Γ 0 P .

3) If Γ 1 P and n ≥ 0, then $ n Γ 1 P .

Note that the converse of 3) does not hold. For example, the derivation for u : ![int] 1 0 1 (νa)(a! 1984 | a?(x).u! x ) relies on the fact that u has priority 1, for otherwise it would not be possible to prefix u! x with an input operation on a.

Typing is preserved by reductions and the type environment may change as a consequence of communications on linear channels, just like in the linear π-calculus [START_REF] Kobayashi | Linearity and the picalculus[END_REF]:

Lemma III.3 (subject reduction). If Γ k P and P → P , then Γ k P for some Γ .
The proof is essentially standard, except for the interesting case concerning the communication on unlimited (i.e., polymorphic) channels sketched below. Consider the derivation

Γ v : $ n t a : ! ω [t], Γ k a! v Γ , x : t k P un(Γ ) a : ? ω [t], Γ k * a?(x).P a : # ω [t], Γ + Γ k a! v | * a?(x).P
and observe that the actual type $ n t of the message v being sent does not match exactly the type t expected by the receiver, but is shifted by some arbitrary amount n. In order to type the reduct P {v/x}, we proceed like this. First of all we shift the derivation of Γ , x : t k P using Lemma III.2, and obtain:

$ n Γ , x : $ n t k P
Then, we observe that Γ is unlimited because it is the type environment used for typing a replicated process. This means that $ n Γ = Γ , since shifting is the identity on unlimited types (Lemma III.1). Therefore we deduce: Γ , x : $ n t k P Now, the actual and expected types of the message v coincide and we know from the initial derivation that Γ + Γ is defined, so we can apply the conventional substitution lemma for the linear π-calculus [START_REF] Kobayashi | Linearity and the picalculus[END_REF] and conclude:

Γ + Γ k P {v/x}
Since the type systems refine the one in [START_REF] Kobayashi | Linearity and the picalculus[END_REF], all the properties of the linear π-calculus (partial confluence, linear usage of channels, etc.) still hold. The added value is that the refined type systems guarantee deadlock/lock freedom.

Theorem III.4 (soundness). The following properties hold:

1) If DF P , then P is deadlock free.

2) If LF P , then P is lock free. x : t, a :

$ n 2 s 1 x! a z : $ m 1 s, a : $ m 1 t (a, z) : $ m 1 (t × s) [T-OUT*] c B : ! ω [t × s], z : $ m 1 s, a : $ m 1 t 1 c B ! a, z [T-PAR] c B : ! ω [t × s], x : t, z : $ m 1 s, a : #[$ 0 1 s] m+n 3 1 x! a | c B ! a, z [T-NEW] c B : ! ω [t × s], x : t, z : $ m 1 s 1 (νa)(x! a | c B ! a, z ) m < n [T-IN] c B : ! ω [t × s], x : t, y : s 1 y?(z).(νa)(x! a | c B ! a, z ) [T-IN*] c B : # ω [t × s] 1 * c B ?(x, y).y?(z).(νa)(x! a | c B ! a, z )
The proof of 1) is by contradiction, for the existence of a well-typed, stable process with pending input or output operations on linear channels would imply the existence of an infinite chain of channels with different priorities, contradicting the fact that there are only finitely many distinct channels in the process. The proof of 2) does an induction on a measure that includes, among other information, priority and tickets of the linear channel for which we are completing the communication (see Definition II.1(2)). The induction is well founded if so is the domain of priorities, whence the restriction to natural numbers for the priorities in the type system for lock freedom. The details can be found in the appendix.

We conclude this section with a few examples showcasing the key features of our type systems. In particular, the recursive processes in Examples III.5, III.7, and III.8 are representative of those configurations that are typeable thanks to our form of channel polymorphism, but not in similar type systems [START_REF] Kobayashi | A type system for lock-free processes[END_REF]- [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF] (see Section IV for a detailed discussion). 2 if and only if 0 < m < n. An analogous derivation is obtained for Node A if and only if 0 < n, m. We deduce that L 1 (A), L 2 (A, A), L 2 (A, B), and L 2 (B, A) are all well typed. Since these constraints on priorities are the most general ones, we also deduce that there are no derivations for L 1 (B) and L 2 (B, B), suggesting that these configurations are locked.

Example III.6. Below is the encoding of the function that computes the n-th number in the sequence of Fibonacci. Instead of showing the typing derivation, which is conventional for the linear π-calculus, we just annotate each linear name occurring in the term with its priority and leave it to the reader to verify that such annotations are consistent with the constraints expressed in the typing rules for deadlock freedom: * fibo?(x, y 0 ).

if x ≤ 1 then y 0 ! x else (νa -1 )(νb -2 ) fibo! x -1, a -1 | fibo! x -2, b -2 | b -2 ?(z 2 ).a -1 ?(z 1 ).y 0 ! z 1 + z 2
Note the use of negative priorities associated with the fresh continuation channels a and b, due to the fact that the inputs

| + + Alice → Bob : M0 | | Bob → Alice : A0 Alice → Bob : M1 | | Bob → Alice : A1
Fig. 1: Alternating Bit Protocol [START_REF] Deniélou | Multiparty session types meet communicating automata[END_REF].

on these channels block the output on the continuation y.

Observe also the role of polymorphic recursion in typing this process: the two recursive invocations of fibo are applied to continuation channels a and b with different priorities.

Example III.7. The following variation of the process Node A gives an example of dynamic lock-free system (beware that in this and the next example, subscripts in names denote tickets; we use colors to ease readability):

Ring def = * c?(x 0 0 , y 0 0 ). (νa 1 3 ) x 0 0 ?(z 1 1 ).(νb 1 2 )(c! z 1 1 , b 1 1 | c! b 1 1 , a 1 1 ) | y 0 0 ! a 1 2
Each message on c spawns two duplicates connected by a new channel b. As a consequence, the process (νe)(Ring | c! e, e ) grows as a ring of processes, each sending a message to its neighbor, and the ring doubles its diameter each time a round of communications is completed.

Example III.8. Figure 1 depicts a variant of the Alternating Bit Protocol [START_REF] Deniélou | Multiparty session types meet communicating automata[END_REF] in which Alice sends alternated messages M0 and M1 to Bob, and Bob answers with corresponding acknowledgments A0 and A1. The diagram describes communications (the rectangles) between the two parties and their dependencies (the arcs), combined with merging points (+ nodes), forks (| nodes with two outgoing arcs) and joins (| nodes with two incoming arcs). The particularity of this modeling of the protocol is that Alice concurrently waits for both A0 and A1 before sending the next corresponding Mi, but always alternating between M0 and M1 messages. We model Bob as the process below, which is parametric in two channels x and y from which Bob respectively receives messages M0 and M1 along with the continuations on which he sends the corresponding Ai (we omit the actual payloads and focus on channels and their continuations):

Bob def = * bob?(x 0 , y 2 ). (νa 3 3 b 5 3 ) x 0 ?(x 1 ).(x 1 ! a 3 2 | y 2 ?(ȳ 3 ).(ȳ 3 ! b 5 2 | bob! a 3 1 , b 5
1 )) We model Alice as two parallel threads Alice0 and Alice1, each handling messages and acknowledgments with matching number, so that Alice0 corresponds to the rightmost vertical flow in Figure 1, and Alice1 to the leftmost one. To respect the protocol and prevent that two messages with the same index are sent in a row, Alice uses a third channel z (unknown to Bob) with which she synchronizes the two threads:

Alice0 def = * alice0?(x 0 , z 1 ). (νa 1 1 c 2 1 ) x 0 ! a 1 1 | z 1 ! c 2 1 | a 1 ?(x 3 1 ).c 2 ?(z 4 1 ).alice0! x3 1 , z4 1 Alice1 def = * alice1?(y 2 , z 1 ). (νb 3 1 c 4 3 ) z 1 ?(z 2 ).(y 2 ! b 3 1 | z2 ! c 4 2 | b 3 ?(ȳ 5 1 ).alice1! ȳ5 1 , c 4 1 )
The whole protocol is modeled as the term (νab

)(Bob | Alice0 | Alice1 | bob! a, b | (νc)(alice0! a, c | alice1! b, c )).
Note the interleaving of possibly blocking actions on different channels in both Alice and Bob.

IV. RELATED WORK

The articles [START_REF] Kobayashi | A type system for lock-free processes[END_REF]- [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF], [START_REF] Kobayashi | A hybrid type system for lock-freedom of mobile processes[END_REF] have been a source of inspiration for our work so we devote most of this section to them. The discussion is quite technical and space constraints force us to assume some familiarity with these works. Deadlock freedom. [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF] defines a type system for ensuring deadlock freedom in the π-calculus. Channels types are pairs [t]/U where t is the type of messages and U -called usage -is a term of a process algebra that includes prefixing and parallel composition and that specifies how the channel is accessed. For example, a channel of type [int]/(! m n .? h k | ? n m .! k h ) can be used concurrently by two processes, one that first sends and then receives an integer and the other that does the opposite. Actions like ! m n are annotated with an obligation m and a capability n to prevent mutual dependencies between channels: inputs on a channel with capability n can only block operations on other channels whose obligation is larger than n. The special value ∞ is allowed for denoting various forms of unlimited channels. There is a significant overlapping between [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF] and our work: usages can describe linear channels as a particular case; linearized channels (those that can be accessed multiple times, but only sequentially) can be encoded using linear channels and continuation passing; priorities have been directly inspired by obligations and capabilities and are used similarly. Let us now analyze the main differences.

First we observe that having two quantities (obligation/capability) instead of a single one (priority) may improve the accuracy of the analysis in some cases. For example, * c?(x, y).x?(z).y?(z) | * c?(x, y).y?(z).x?(z) is ill typed in our type system but is typeable in [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF] by giving both x and y obligation 1 and capability 0. The null capability means that, assuming that outputs on x and y are available in the environment immediately (capability 0), then either of these processes guarantees that the both inputs will be performed after at most one reduction (obligation 1).

The main distinguishing features of our approach, however, are polymorphism and the fact that priorities have a relative interpretation in message types. To illustrate the effect of these features on the accuracy of our type systems, we revisit Example II.2 in the setting of [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF] assuming to extend usages with recursion (recursive usages are admitted in [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF], but only for type reconstruction purposes). The following modeling of L 2 (A, A) uses no explicit continuation passing and therefore is the most favorable to the type system in [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF]: * c?(x, y).

(x! 3 | y?(z).c! x, y ) | c! e, f | c! f, e (10)
The process is tentatively typed using the assignments

e : [int]/(µα.! m n .α | µα.? n m .α) f : [int]/(µα.? h k .α | µα.! k h .α)
where the fact that obligations and capabilities are swapped in complementary actions of the usages of e and f is necessary to satisfy the reliability condition [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF] which corresponds, in our setting, to the property that channel types with opposite polarities and same priority can be combined together (last equation of ( 8)). The structure of (10) requires the simultaneous satisfiability of k < m (there is an input on f with capability k that blocks e whose topmost obligation is m) and of m < k (there is an input on e with capability m that blocks f whose topmost obligation is k), therefore (10) cannot be proven deadlock free with the type discipline in [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF]. The problem is that obligations and capabilities, unlike priorities, are absolute values associated with actions: e and f always have the same obligation and capability regardless of the number of unfoldings of their usages. By contrast, in Example III.5 the channels e and f and their continuations are assigned a numerically increasing sequence of priorities. There are two features in [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF] that overcome partially the limitations due to absolute obligations and capabilities. The first one is that the behavioral nature of usages allows the typing of recursive processes involving one channel. For example, the following variant of is well typed in [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF]. The point is that in [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF] an input process u?(x).P is well typed if the capability of u is smaller than the obligation of all the channels in P except u itself. The second feature stems from the observation that the strict order < used for comparing the capability of a channel u and the obligation of another channel v can be safely weakened to ≤ if u has been created later than v. This property, denoted by the relation u ≺ v in [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF], can be inferred from the syntactic structure of processes and makes it possible to deal with processes like [START_REF] Brand | On communicating finite-state machines[END_REF], where the input on the newer channel a is allowed to block operations on the older channel y despite the fact that a and y have the same type (hence the same obligations and capabilities). As noted in [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF], the very same feature would also work using the opposite order , but one would have to choose between either ≺ or , since using their union would be unsound. The opposite order however arises naturally with continuation passing, as we have seen in ( 4) and in most of the examples throughout the paper.

In summary, the techniques based on absolute obligations/capabilities have difficulties handling systems where two or more recursive processes interleave actions on two or more channels. The use of the ≺ relation alleviates in part these limitations, when processes have a function-like behavior.

Usages provide more precise information on unlimited channels. For example, the lock-free modeling of the dining philosophers in [START_REF] Kobayashi | A type system for lock-free processes[END_REF] cannot be captured by our type system because it uses non-replicated unlimited channels for representing shared resources (the forks) accessed by competing processes (the philosophers). Lock freedom. Type systems for lock freedom have been presented in [START_REF] Kobayashi | A type system for lock-free processes[END_REF], [START_REF] Kobayashi | Type-based information flow analysis for the pi-calculus[END_REF]. These works rely on essentially the same types and usages already discussed for deadlock freedom, and so they are subject to the same problems that arise in [START_REF] Dardha | Session types revisited[END_REF]. In particular, all the processes discussed in Examples III.5, III.7, III.8, which are representative configurations mixing recursion and cyclic network topologies, are ill typed in [START_REF] Kobayashi | A type system for lock-free processes[END_REF]- [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF].

The partial order ≺ is unsound and cannot be used to improve the accuracy of lock-free analysis in [START_REF] Kobayashi | A type system for lock-free processes[END_REF], [START_REF] Kobayashi | Type-based information flow analysis for the pi-calculus[END_REF]. This is reflected also in our type system for lock freedom, where negative priorities are banned. Consequently, processes such as [START_REF] Brand | On communicating finite-state machines[END_REF] or the one in Example III.6 can be proved deadlock free but not lock free. Lock-free typability of (3) (restricted to natural numbers) and other recursive-like processes is recovered in [START_REF] Kobayashi | A hybrid type system for lock-freedom of mobile processes[END_REF], where it is observed that lock freedom can be characterized as the conjunction of deadlock freedom and termination. Such characterization turns out to be more accurate on recursive processes with function-like behaviors, partly because the type system for deadlock freedom imposes fewer constraints, partly thanks to the accuracy of the techniques for proving termination. In fact, the hybrid approach [START_REF] Kobayashi | A hybrid type system for lock-freedom of mobile processes[END_REF] is parametric on the specific techniques for verifying deadlock freedom or termination. This means that it suffers from the same shortcomings that we have discussed earlier for processes like [START_REF] Dardha | Session types revisited[END_REF] when instantiated with the deadlock free analysis of [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF], but also that it should be applicable in our setting, in which case it would benefit from the better accuracy of our type system for deadlock freedom. By the way, the limit we impose on the number of times a channel can be sent in a message is akin to ensuring a form of termination (in fact, the eventual use of the channel for performing a communication) so in a sense our type system for lock freedom can already be seen as an instance of the hybrid framework described in [START_REF] Kobayashi | A hybrid type system for lock-freedom of mobile processes[END_REF]. Session types. Session types [START_REF] Honda | Types for dyadic interaction[END_REF], [START_REF] Honda | Language primitives and type disciplines for structured communication-based programming[END_REF] are behavioral types akin to sequential usages in which each single input/output action is annotated with the type of a message. For example, the session type ![int].?[bool] denotes a channel on which it is possible to first sent an integer, and then receive a boolean. Duality relates session types associated with corresponding endpoints of a binary session and generalizes the composition operator between linear types [START_REF] Coppo | Global progress for dynamically interleaved multiparty sessions[END_REF]. For example, the session type above is dual of ?[int].! [bool]. Duality ensures communication safety and also lock freedom, but the latter property is guaranteed only within sessions, not when (blocking) actions from different sessions are interleaved with each other. In some works [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF], [START_REF] Wadler | Propositions as sessions[END_REF] a plain session type discipline ensures deadlock freedom also when sessions are interleaved, but only because the syntax of (well-typed) processes prevents the modeling of cyclic network topologies. Global types. A global type [START_REF] Castagna | On Global Types and Multi-Party Sessions[END_REF], [START_REF] Deniélou | Multiparty session types meet communicating automata[END_REF], [START_REF] Deniélou | Parameterised multiparty session types[END_REF], [START_REF] Honda | Multiparty asynchronous session types[END_REF] describes the interactions between participants of a session as opposed to the actions that participants perform on the channel of the session. For example, the interactions between the three processes that compose the system L 3 (A, B, B) in Example III.5 can be described by the recursive global type G 3 that satisfies the equation G 3 = A → B.B → C.C → A.G 3 which gives names A, B, and C to the three participants and specifies the order of their synchronizations. In general, global types also allow the specification of the type of the exchanged messages and include operators other than prefixing, such as choice and parallel composition. Global types that satisfy some wellformedness conditions are projectable into session types and processes that conform to these projections are guaranteed to be type safe, to implement the protocol described by the global type, and to be lock free. Therefore, global types are an effective way of extending the lock freedom property from binary to n-ary sessions.

One downside of global types is that they may make it harder to build and maintain systems compositionally (although some modularity and compositionality aspects have recently been addressed in [START_REF] Demangeon | Nested protocols in session types[END_REF] and [START_REF] Montesi | Compositional choreographies[END_REF]). For instance, L 2 (A, B) and L 3 (A, B, B) in Example II.2 are assembled in a modular way using the same constituents, but the global types G 2 = A → B.B → A.G 2 and G 3 above that describe the interactions in these systems are quite different. It may also be harder to describe "unstructured" interactions from a global perspective. For instance, it takes the most sophisticated global type language available to date [START_REF] Deniélou | Multiparty session types meet communicating automata[END_REF] to describe accurately the dependencies between Alice's threads in Example III.8. For these reasons, global types are ideal for describing delimited interactions within sessions, but they cannot dispense completely from the need of interleaving different sessions, in which case they are unable to prevent (dead)locks.

These observations have motivated the study of mixed approaches [START_REF] Bettini | Global progress in dynamically interleaved multiparty sessions[END_REF], [START_REF] Coppo | Inference of Global Progress Properties for Dynamically Interleaved Multiparty Sessions[END_REF], [START_REF] Coppo | Global progress for dynamically interleaved multiparty sessions[END_REF] that keep track of the order in which different sessions interleave with the purpose of detecting and flagging mutual dependencies between sessions that could lead to (dead)locks. These mixed approaches turn out to be quite restrictive (e.g., recursive processes can access one session only [START_REF] Coppo | Global progress for dynamically interleaved multiparty sessions[END_REF]) and require heavyweight and multi-layer type systems.

V. CONCLUSIONS

Type systems that enforce (dead)lock freedom of communicating processes inevitably rely on trade-offs, for such properties are undecidable [START_REF] Brand | On communicating finite-state machines[END_REF] even under severe restrictions of the communication model (e.g., for half-duplex communication with three or more processes [START_REF] Cécé | Verification of programs with half-duplex communication[END_REF]). These type systems essentially follow one of two approaches: some [START_REF] Kobayashi | A type system for lock-free processes[END_REF]- [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF] favor compositionality and apply to generic process algebras, but have difficulties in dealing with recursive processes and cyclic network topologies; others can handle such configurations, but only within the scope of (multiparty) sessions and assuming that the communication protocol is explicitly described in advance by a global type. In the context of the linear π-calculus, our type systems conjugate the advantages of both approaches and do so with minimal machinery. Indeed, all previous type systems for (dead)lock freedom rely on rich behavioral types (usages [START_REF] Kobayashi | A type system for lock-free processes[END_REF]- [START_REF] Kobayashi | Type systems for concurrent programs[END_REF], [START_REF] Kobayashi | A hybrid type system for lock-freedom of mobile processes[END_REF], session types [START_REF] Padovani | From Lock Freedom to Progress Using Session Types[END_REF], global types [START_REF] Bettini | Global progress in dynamically interleaved multiparty sessions[END_REF], [START_REF] Coppo | Inference of Global Progress Properties for Dynamically Interleaved Multiparty Sessions[END_REF], [START_REF] Coppo | Global progress for dynamically interleaved multiparty sessions[END_REF], [START_REF] Deniélou | Multiparty session types meet communicating automata[END_REF], [START_REF] Deniélou | Parameterised multiparty session types[END_REF], [START_REF] Honda | Multiparty asynchronous session types[END_REF], conversation types [START_REF] Vieira | Typing progress in communicationcentred systems[END_REF]), and when they are able to deal with recursive processes it is because they take advantage of such richness (see Section IV), almost implying the necessity of rich types to ensure properties as strong as (dead)lock freedom. We have shown that this is not the case, at least for the linear π-calculus.

The linear π-calculus is an adequate model for many concrete communicating systems. In particular, it is the "assembly language" that lies beneath binary sessions [START_REF] Dardha | Session types revisited[END_REF], [START_REF] Kobayashi | Type systems for concurrent programs[END_REF] and in the appendix we show that many multiparty sessions too can be compiled into the linear π-calculus. So, one can establish (dead)lock freedom of a session-based process (also in presence of session interleaving) by compiling it into the linear π-calculus and by typing the resulting process using our type systems. When this approach is unfeasible -not all multiparty sessions can be encoded using linear channelsor undesirable -the structure of sessions may serve other important purposes -the technique described in this paper can still be used for reasoning on inter-session (dead)lock freedom: just like we annotate channel types with priorities and tickets, it is possible to annotate the single actions within session and global types in the same way. This experiment was already attempted in [START_REF] Padovani | From Lock Freedom to Progress Using Session Types[END_REF], [START_REF] Vieira | Typing progress in communicationcentred systems[END_REF], but in these works the annotations are "absolute", much like obligations/capabilities, and so they suffer from issues analogous to those described in Section IV.

The form of channel polymorphism that lies at the core of our type systems allows the shifting of priorities with maps of the shape z → z + n. This prevents, for example, typing an output a! x 0 , y

1 if a has type ! ω [?[int] 1 × ![int] 3 ]
, because a expects x and y to have priorities at distance 2, while they are at distance 1. In fact, the type system for deadlock freedom can be generalized to rational numbers for priorities and positive affine maps for transforming them. In the example above, the map z → 1 2 z -1 2 turns the priorities 1 and 3 in the type of a into 0 and 1, namely the priorities of x and y. The type system for lock freedom is slightly less flexible, because its soundness proof requires priorities to be part of a well-founded set.

Finally, as witnessed by the examples in this paper, it is un-realistic to assume that the programmer is capable of guessing the correct values of priorities and tickets of linear channels in general. We are finalizing a complete type reconstruction algorithm for our type systems. Intuitively, the algorithm uses variables for representing unknown priorities and tickets and accumulates constraints between such variables according to the rules of the type systems (Table 1). These constraints can always be represented as an integer programming problem, which is solvable using known methods.

We will make extensive use of Lemma III.2 in the proofs that follow, to the point that it is convenient to extend the type system presented in Table 1 with the (admissible) rule

[T-SHIFT] Γ k P k = 1 ⇒ n ≥ 0 $ n Γ k P C. Subject reduction
In order to formulate and prove the subject reduction result, we need to determine a precise correspondence between the type environment before a reduction and the one after the reduction. We do so by defining a reduction relation for type environments using the same labels as those in the labeled reduction for processes. Let act -→ be the least relation defined by the rules

Γ , a : #[t] n m a -→ Γ , a : ∅[t] n m Γ , a : # ω [t] a -→ Γ , a : # ω [t] Γ , a : $ 0 1 t τ -→ Γ , a : t
The first rule consumes a linear channel a from the environment and is used when a synchronization on a occurs (recall that linear channels can be used for one synchronization only by definition). The middle rule leaves the environment unchanged when a synchronization on some unlimited channel a occurs. The last rule decreases consumes one ticket from the type of a and is used each time a is sent in a message. In the following we write Proof. By induction on the derivation of Γ v : $ 0 1 t. We only show two cases, correponding to the channel and pair expressions:

• (v = a) Then Γ = Γ , a : p ι [s] n
m and un(Γ ). We distinguish two subcases:

-(ι = 1) Then $ 0 1 t = p[s]
n m and m > 0 and t = p[s] n m-1 and we conclude by taking Γ = Γ , a : t and observing that Γ

τ -→ Γ . -(ι = ω) Then $ 0 1 t = t = p ω [s] and we conclude by taking Γ = Γ . • (v = (v 1 , v 2 )) Then Γ = Γ 1 + Γ 2 and $ 0 1 t = ($ 0 1 t 1 ) × ($ 0 1 t 2 ) and Γ i v i : $ 0 1 t i for i = 1, 2.
By induction hypothesis there exist Γ 1 and Γ 2 such that Γ i τ =⇒ Γ i and Γ i v i : t i for i = 1, 2. Observe that the τ -→ relation between type environments can only consume the tickets of values. This means that Γ 1 + Γ 2 is defined and moreover

Γ τ =⇒ Γ 1 + Γ 2 . We conclude by taking Γ = Γ 1 + Γ 2 .
The next result is standard and indicates that typing is preserved by structural congruence. Note that the result would not hold, had we included the law * P ≡ P | * P . Lemma B.4. If Γ k P and P ≡ Q, then Γ k Q.

Proof. By induction on the derivation of P ≡ Q.

The following result states that well-typing of processes is preserved by reductions. Note though that the type environment may change.

Lemma B.5 (Lemma III.3). If Γ k P and P act -→ P , then Γ k P for some Γ such that Γ act =⇒ Γ .

Proof. By induction on the derivation of P act -→ P and by cases on the last rule applied. We only show the most relevant cases. * P a = P a u! e a = u a ∨ e a P | Q a = P a ∨ Q a let x, y = e in P a = e a ∨ P a case e {i x i ⇒ P i } i=inl,inr a = e a ∨ P inl a ∨ P inr a (νa)P a = ⊥ (νb)P a = P a if a = b

[LR-COMM] Then P = a! v |a?(x).Q a -→ Q{v/x} = P and act = a. From [T-PAR] we deduce Γ = Γ 1 +Γ 2 where Γ 1 k a! v and Γ 2 k a?(x).Q. From [T-OUT] we deduce Γ 1 = Γ 1 + a : ![t] n m and Γ 1 v : $ n k t.
Given Γ 1 P where Γ is balanced and a ∈ dom(Γ ), the measure of a is a triple consisting of the priority |Γ (a)| of a, the tickets tickets(Γ (a)) of a, and the maximum "depth" of a in P , namely the maximum number of input prefixes that guard an occurrence of a in P . Observe that, when P is well typed, the depth P a is always finite. We write < for the usual lexicographic order on triples returned by measure(a, Γ , P ). Note that < is well founded, i.e. there are no infinite descending chains of triples related by <, because the type system for lock freedom restricts priorities to natural numbers. Lemma B.9. Let (1) Γ 1 P and (2) Γ balanced and (3) either in(a, P ) or out(a, P ). Then there exists Q such that P → * Q and sync(a, Q).

Proof. Without loss of generality we can make the following assumptions:

• that ¬sync(a, P ), otherwise we conclude immediately by taking Q = P ;

• that P has no restrictions at the top level. Indeed, if P ≡ (νb)P , from (1) and [T-NEW] we deduce Γ , b :

# ι [t] n m 1 P where Γ , b : # ι [t] n
m is balanced, so we could reason on P ; • that P has no let or case at the top level. If this is the case, then from (1) we can always reduce P to a well-typed process that contains no top level let's or case's. Note that, from (2), we know that the domain of Γ contains only channels (no variables). Therefore, any expression in any top-level output of P is evaluated.

We proceed by induction, showing that if the result holds for every triple (b, Γ , P ) such that measure(b, Γ , P ) < measure(a, Γ , P ), then it holds also for the triple (a, Γ , P ). We begin by analyzing a few cases that are impossible given the typing rules of processes:

• P ≡ C [a?(x).R] and a ∈ fn(R).

< n + |t| from 0 < |t| = |$ n 1 t| by definition of | • | ≤ n from a ∈ fn(e)
which is absurd, so this case is also impossible. Then we consider the cases in which there is a pending operation on a but no immediate synchronization is possible. In every case we are able to extend the reduction of P to a state where the measure of a is strictly smaller than measure(a, Γ , P ). This is enough for establishing the result, given that the order < on measures is well founded. =⇒ Γ and measure(a, Γ , P ) < measure(a, Γ , P ) because a is guarded by one less input prefix. We conclude by induction hypothesis.

Theorem B.10 (Theorem III.4). The following properties hold:

1) If DF P , then P is deadlock free.

2) If LF P , then P is lock free.

Proof. The two properties are straightforward consequences of Lemma B.7 and Lemma B.9, respectively.

APPENDIX C EXTENDED EXAMPLE: MULTIPARTY SESSIONS

In this section we show that a whole class of protocols whose lock freedom is guaranteed by design can be implemented by processes that are well-typed according to our type system for lock freedom. The challenging aspect of this exercise is that in general the processes will be recursive and interleaving possibly blocking actions pertaining several different linear channels configured in a cyclic network topology. We proceed as follows. First of all, we define a language for specifying protocols whose lock freedom is granted. We do so by means of a simple variant of global types [START_REF] Bettini | Global progress in dynamically interleaved multiparty sessions[END_REF], [START_REF] Deniélou | Multiparty session types meet communicating automata[END_REF], [START_REF] Deniélou | Parameterised multiparty session types[END_REF], [START_REF] Honda | Multiparty asynchronous session types[END_REF] describing sequences of interaction events between a fixed number of participants. Then, we extract from global types a characteristic implementation of the participants involved in the protocol, using the process language we have defined in Section II. Finally, we show how to construct a typing environment for the participants so that they are well typed according to the type discipline of Section III. Extensions. For technical convenience, we work with a slightly more general syntax of types:

t ::= • • • | µα k {α i := t i } i=1..n | $ n
m t Basically we generalize recursions so that the type µα k {α i := t i } i∈I simultaneously binds all the type variables α i for i ∈ I in each t i for i ∈ I. The elected type variable α k with k ∈ I stands for the whole term. It is known that this generalized recursion operator has the same expressive power as the one that binds exactly one variable [START_REF] Courcelle | Fundamental properties of infinite trees[END_REF], but it is more convenient to work with in this section. The notion of type contractiveness can be easily adjusted to this generalization. Equality between types works as before by considering the infinite unfolding of recursions, in particular, µα k {α i := t i } i∈I = t k {µα i {α i := t i } i∈I /α i } i∈I where t{s i /α i } i∈I denotes the simultaneous substitution of every free occurrence of α i in t with s i . We also consider $ n m as a type constructor rather than a function, because we must be able to denote the shifting of possibly open types, whereas the shifting function ( 7) is defined for closed types only. We extend equality between types with the laws of [START_REF] Coppo | Inference of Global Progress Properties for Dynamically Interleaved Multiparty Sessions[END_REF]. Because of contractiveness, every type can be rewritten into an equivalent one without $ n m constructors. Global types. We assume a finite, totally ordered set R of participant tags p, q, . . . , A, B, . . . that we use to uniquely identify the participants of a protocol. We also need a set of labels , . . . for identifying events occurring in protocols. Events ε, . . . and global types G, . . . are defined below:

ε ::= p → q@ G ::= α ε.G ε.{G, G} µα.G
An event p → q@ represents the communication of a message from participant p (the sender) to participant q (the receiver). We omit the type of the message, because it is irrelevant for our purposes, and we will think of events merely as synchronizations.

We decorate events with a label that uniquely identifies them, although we will see that the same label may occur several times in a given global type. The global type ε.G describes a protocol in which ε may occur before all the other events in G (the assurance that it will necessarily occur before them depends on other properties of the global type that are not captured by their syntactic structure). The global type ε.{G 1 , G 2 } describes a protocol in which the sender in ε communicates a binary decision to the receiver in ε. Depending on the outcome of the decision, the protocol evolves as either G 1 or G 2 . Global types α and µα.G are used for building recursive protocols. We do not impose any contractiveness conditions on global types, which we treat as purely syntactic objects. In fact, we abbreviate µα.α as end to denote the terminated protocol in which no event occurs. We write fv(G) for the set of free type variables in G, defined as expected.

Not every global type describes a sensible protocol. For example,

G a def = A → B.{C → D.end, D → C.end}
specifies that either C sends a message to D or D sends a message to C depending on the decision taken by A. The problem is that neither C nor D are aware of such decision, for A communicates it only to B, so there is no way C and D can behave differently in the two branches of the choice. We therefore need to identify a class of global types that describe sensible protocols, and that we call realizable. An edge p q is a set {p, q} with p = q representing a communication channel between two participants.

We let edge(p → q@ ) = p q. A sort is a set of edges and tells us which pairs of participants are supposed to communicate. Since we will analyze possibly open global types, we define the sort of a global type relative to a sort environment that maps type variables to sorts:

Definition C.1. A sort environment Σ is a finite map from type variables to sorts. We say that Σ is a sort environment for

G if fv(G) ⊆ dom(Σ). The sort of G relative to a sort environment Σ for G is Σ(G) def = {edge(ε) | ε occurs in G} ∪ α∈fv(G) Σ(α).
We write ∅ for the empty sort environment and upd(Σ, α, G) for the updated sort environment Σ, α : Σ(µα.G). We can now define the projection ↓(Σ, G, p q) of a global type G with respect to a sort environment Σ and an edge p q. Intuitively, ↓(Σ, G, p q) extracts from G the sub-protocol that concerns only participants p and q. Formally:

↓(Σ, α, p q) def = α ↓(Σ, ε.G, p q) def = ε.↓(Σ, G, p q) if p q = edge(ε) ↓(Σ, ε.G, p q) def = ↓(Σ, G, p q) if p q = edge(ε) ↓(Σ, ε.{G1, G2}, p q) def = ε. ↓(Σ, G1, p q) ↓(Σ, G2, p q) if p q = edge(ε) ↓(Σ, ε.{G1, G2}, p q) def = ↓(Σ, Gi, p q) if p q = edge(ε) ↓(Σ, µα.G, p q) def = µα.↓(upd(Σ, α, G), G, p q)
Note that projection is a partial function. It may be ill defined if the projections of two branches of a choice with respect to the same edge p q differ (fifth equation). For example, ↓(∅, G a , C D) is ill defined because it can be either C → D.end or D → C.end. Note the role played by labels in determining the existence of a projection. For example,

G b def = A → B@ 1 . B → A@ 2 .C → D@ 3 .end C → D@ 3 .B → A@ 4 .end
is projectable with respect to C D because the two occurrences of C → D@ 3 in the two branches have the same label. They must in fact represent the same event, since C and D are unaware of the choice taken by A. On the contrary, B → A@ 2 and B → A@ 4 may have different labels because both A and B are aware of the choice taken by A. Projectability alone is not a sufficient condition for realizability. We must also take into account the ordering of events induced by the structure of global types. For instance

G c def = A → B@ 1 . E → F@ 2 .C → D@ 3 .end C → D@ 3 .E → F@ 2 .
end is projectable but not realizable: the two occurrences of C → D and E → F must be tagged with the same label in order for ↓(∅, G c , C D) and ↓(∅, G c , E D) to be well defined, and yet G c specifies that the order of these events depends on the decision taken by A, which none of C, D, E, and F is aware of. To capture these inconsistencies we reason on the relation ≺ G induced by the structure of G such that ≺ G holds if and only if the event with label immediately precedes the event with label in G. We denote by ≺ + G the transitive closure of ≺ G and we require ≺ + G to be irreflexive for G to be realizable. Definition C.2 (realizable global type). We say that G is realizable if (1) ↓(∅, G, p q) is well defined for every p q and (2) the relation ≺ + G is irreflexive. According to this definition, G b is realizable but G c is not, because 2 ≺ + Gc 2 . Note that the relation ≺ G is solely determined by the syntactic structure of G regardless of recursions and type variables occurring in G. No non-trivial recursive global type would be realizable had we considered, for example, µα.A → B@ .α equivalent to its own unfolding A → B@ .µα.A → B@ .α. Characteristic participants. We now show how to build a set of processes that implement any realizable global type. Every participant p in a global type G will be modeled as a sequential process P(∅, G, p) that uses a tuple x [p] = x pq1 , . . . , x pqn of variables, where {q 1 , . . . , q n } = R \ {p} and the q i 's appear according to the total order on R (the total order serves only so that x [p] is a uniquely determined tuple). In particular, x pq is the channel that connects p to q. P(Σ, G, p) is defined inductively on G by the equations in the top half of Table 3. Despite the daunting look of the definition, the idea is simple: every event A → B to which p participates determines either an input or an output action on the channel x pq . When p is the receiver, a message is read from x pq and is given name x pq , because the message is actually the continuation channel on which the conversation between p and q continues. When p is the sender, it sends to q the continuation for the subsequent communications on the edge p q. This is done through the auxiliary function C(Σ, p, q, id , G) where id is the identity function: the continuation is an actual channel a if p q occurs in Σ(G), that is if p and q will communicate again in the future, or the dummy number 0 if no other interaction between p and q is expected. When the event implies a choice ε.{G 1 , G 2 }, we make the (arbitrary) decision that the sender always chooses the left branch G 1 . We use injection to encode the decision in the sender and case to decode the decision in the receiver and we use the same auxiliary function C for sending the decision, to which we pass the injector inl to wrap the continuation. Recursions µα.G are implemented by associating the type variable α with $ -n ?[T(Σ, G, p, q, )] $ -n T(Σ, G, p, q, ) p, q = A, B p, q = B, A otherwise T(Σ, A → B@ .{G 1 , G 2 }, p, q, n) def =    $ -n ![T(Σ, G 1 , q, p, ) ⊕ T(Σ, G 2 , q, p, )] $ -n ?[T(Σ, G 1 , p, q, ) ⊕ T(Σ, G 2 , p, q, )] $ -n T(Σ, G i , p, q, ) p, q = A, B p, q = B, A otherwise T(Σ, µα.G, p, q, n) def = $ 0 1 µαpq αpq = T(upd(Σ, α, G), G, p, q, n) αqp = T(upd(Σ, α, G), G, q, p, n)

an unlimited channel c α : the replicated input on c α corresponds to defining a recursive process; the output on c α corresponds to invoking the recursive process. The whole tuple x [p] is transmitted at each invocation. Typing participants. We now arrive at the main point of this section, namely the definition of a suitable type environment Γ p def = {x pq : t pq } q∈R\{p} such that the process P(∅, G, p) is well typed in Γ p . Determining the input/output behavior of P(∅, G, p) with respect to a channel x pq is easy: this information is written in the global type. But for P(∅, G, p) to be well typed, we must also make sure that blocking actions respect the priority of channels (see rule [T-IN]) and that delegations are allowed by the tickets of channels (see [T-OUT] and [T-OUT*]). We determine priorities using the event order ≺ G and tickets looking at the structure of P(∅, G, p). We know that every realizable global type G has an irreflexive event order ≺ + G , meaning that the events in G form a DAG. Therefore, there exists a topological ordering ord from labels in G to positive natural numbers such that ≺ G implies 0 < ord( ) < ord( ). In a sense, ord( ) is the abstract time at which the event labeled occurs. The idea is to use ord( ) as the priority for the channel types when projecting the action labeled by . In what follows, we simplify the notation writing just in place of ord( ). Now, the bottom half of Table 3 defines T(Σ, G, p, q, n) as the type of x pq in the global type G relative to an arbitrary offset n that is smaller than any label occurring in G. Given how P(Σ, G, p) uses the channel x pq , the definition of T(Σ, G, p, q, n) is hopefully self-explanatory except for a few twists that we comment on here: The type T(Σ, α, p, q, n) is the type variable α pq only if the edge p q is used in the recursion marked by the type variable α; otherwise, it is int to denote a dummy natural number. Priorities are determined as the difference between the label of the topmost action in G and the current offset n; after the action, the offset becomes . We have T(Σ, A → B@ .G, A, B, n) = $ -n ![T(Σ, G, B, A, )] where A and B are swapped within ![•]. The swapping is motivated by the fact that A sends to B a channel whose type determines how the channel is used by B. The same phenomenon occurs in determining the type of a choice. Then, because of the definition of T(Σ, α, p, q, n), it may happen that the type T(Σ, G, p, q, n) contains both the α pq and the α qp type variables. For this reason, T(Σ, µα.G, p, q, n) binds both α pq and α qp , taking advantage of the generalized recursion for channel types. We apply $ 0 1 in the two places where a channel is delegated, in accordance with the definition of P(Σ, G, p). Finally, note that T(Σ, G, p, q, n) is well defined whenever G is realizable.

Example III. 5 .=

 5 Regarding the processes in Example II.2µα.?[α] m 1 and observe that s = $ 0 1 s = ?[$ 0 1 s] m 1 . For Node B we obtain the typing derivation shown in Table

  L 2 (A, B) * c?(y).(y! | c! y ) | * d?(y).y?(z).d! y | c! e | d! e

τ 3 .

 3 =⇒ for the reflexive, transitive closure of τ Let Γ v : $ 0 1 t. Then there exists Γ such that Γ τ =⇒ Γ and Γ v : t.

[

  LR-COMM*] Then P = a! v | * a?(x).Q a -→ Q{v/x} | * a?(x).Q = P and act = a. From [T-PAR] we deduce Γ = Γ 1 + Γ 2 where Γ 1 k a! v and Γ 2 k * a?(x).Q. From [T-OUT*] we deduce Γ 1 = Γ 1 + a : ! ω [t] and Γ 1 e : $ nDefinition B.8 (measure). Let Γ 1 P where Γ is balanced and a : t ∈ Γ . Then measure(a, Γ , P ) def = (|t|, tickets(t), P a ) where P a is inductively defined below, where we assume ⊥ + 1 = ⊥:a a = 0 u a = ⊥ if a = u e 1 ,e 2 a = e 1 a ∨ e 2 a inl e a = inr e a = e a 0 a = ⊥ u?(x).P a = u a ∨ ( P a + 1)

  Then a : #[t] n m ∈ Γ . According to [T-IN] we have Γ , x : $ n t 1 R and n < |Γ |. Then a ∈ dom(Γ ), hence this case is impossible. • P ≡ C [a! e ] and a ∈ fn(e) and a : # ω [t] ∈ Γ and ¬ * in(a, P ). Then from [T-OUT*] we deduce Γ e : $ n 1 t and 0 ≤ |t|. From ¬ * in(a, P ) we know that e must contain the endpoint a with input capability, for otherwise it would occur at the top level of P . Hence |t| = ⊥, which contradicts 0 ≤ |t|. Hence this case is impossible. • P ≡ C [a! e ] and a ∈ fn(e) and a : #[t] n m ∈ Γ . Then from [T-OUT] we deduce Γ e : $ n 1 t and 0 < |t|. We deduce n

  • P ≡ C [b! v | * b?(x).R] and a ∈ fn(v). Then P → C [R{v/x} | * b?(x).R] = P . By Lemma III.3 we deduce that Γ 1 P for some Γ such that tickets(Γ (a)) < tickets(Γ (a)), therefore measure(a, Γ , P ) < measure(a, Γ , P ). We conclude by induction hypothesis.• P ≡ C [b! v ]where a ∈ fn(v) and b is a linear channel. From [T-OUT] we deduce |Γ (b)| < |Γ (a)|. By induction hypothesis we derive P → * C [b! v | b?(x).R] → C [R{v/x}] = P . By Lemma III.3 there exists Γ such that Γ 1 P and tickets(Γ (a)) < tickets(Γ (a)). We conclude by induction hypothesis. • P ≡ C [b?(x).R] where a ∈ fn(R) \ {b}. From [T-IN] we deduce |Γ (b)| < |Γ (a)|. By induction hypothesis we derive P τ =⇒ C [b! v | b?(x).R] b -→ C [R{v/x}] = P for some v. By Lemma III.3 we deduce Γ 1 P for some Γ such that Γ b

TABLE 3 :$

 3 Global type projections.P(Σ, α, p) def = cα! x [p] P(Σ, A → B.G, A) def = C(Σ, A, B, id, G) P(Σ, A → B.G, B) def = xBA?(xBA).P(Σ, G, B) P(Σ, A → B.G, p) def = P(Σ, G, p) p ∈ A B P(Σ, A → B.{G 1 , G 2 }, A) def = C(Σ, A, B, inl, G 1 ) P(Σ, A → B.{G 1 , G 2 }, B) def = xBA?(y).case y {inl xBA ⇒ P(Σ, G 1 , B), inr xBA ⇒ P(Σ, G 2 , B)} P(Σ, A → B.{G 1 , G 2 }, p) def = P(Σ, G i , p) p ∈ A B P(Σ, µα.G, p) def = (νcα)(cα! x [p] | * cα?(x [p] ).P(upd(Σ, α, G), G, p)) C(Σ, p, q, f, G) def = (νa)(xpq! f a | let xpq = a in P(Σ, G, p)) p q ∈ Σ(G) C(Σ, p, q, f, G) def = xpq! f 0 | let xpq = 0 in P(Σ, G, p) p q ∈ Σ(G)T(Σ, α, p, q, n) , A → B@ .G, p, q, n) -n ![T(Σ, G, q, p, )]

For instance, given G d def =

 def µα.A → B.B → C.C → A.α and assuming R = {A, B, C}, we haveP(∅, G d , A) = (νc α )(c α ! x AB , x AC | * c α ?(x AB , x AC ).(νa)(x AB ! a | let x AB = a in x AC ?(x AC ).c α ! x AB , x AC ))

TABLE 1 :

 1 Typing rules for expressions and processes.

Expressions [T-CONST]

TABLE 2 :

 2 Typing derivation for Node B .

	a : $ n 2 s a : $ n 2 s	0 < m

[T-OUT]

  From [T-IN] we deduceΓ 2 = Γ 2 + a : ?[t] n h and Γ 2 , x : $ n t k Q.The fact that the types associated with the two a's are complementary follows from the definition of Γ 1 + Γ 2 . By Lemma B.3 we deduce that there existsΓ 1 such that Γ 1 v : $ n t and Γ 1 τ =⇒ Γ 1 . Note that Γ 1 + Γ 2 is defined. Then by Lemma B.2(2) we obtain Γ 1 + Γ 2 k Q{v/x}. Let Γ = Γ 1 + Γ 2 + a : ∅[t] n m+h . From [T-PAR]we deduce Γ k P . We conclude by observing that Γ

act

=⇒ Γ .

un(Γ ) Γ n : int [T-NAME] un(Γ ) Γ , u : t u : t [T-PAIR] Γ e : t Γ e : s Γ + Γ (e, e ) : t × s [T-INL] Γ e : t Γ inl e : t ⊕ s [T-INR] Γ e : s Γ inr e : t ⊕ s Processes[T-IDLE] un(Γ ) Γ k 0 [T-IN] Γ , x : $ n t k P n < |Γ | Γ + u : ?[t] n m k u?(x).P [T-OUT] Γ e : $ n k t 0 < |t| Γ + u : ![t] n m k u! e [T-IN*] Γ , x : t k P un(Γ ) Γ + u : ? ω [t] k * u?(x).P [T-OUT*] Γ e : $ n k t ⊥ < |t| Γ + u : ! ω [t] k u! e [T-NEW] Γ , a : p ι [t] n m k P p even Γ k (νa)P [T-LET] Γ e : t × s Γ , x : t, y : s k P Γ + Γ k let x, y = e in P [T-PAR] Γ i k P i (i=1,2) Γ 1 + Γ 2 k P 1 | P 2 [T-CASE]Γ e : t ⊕ s Γ , x : t k P Γ , y : s k Q Γ + Γ k case e {inl x ⇒ P, inr y ⇒ Q}

k t. From [T-IN*] we deduce Γ 2 = Γ 2 + a : ? ω [t] and Γ 2 , x : t k Q and un(Γ 2 ). By Lemma B.3 we deduce that there exists Γ 1 such that Γ 1 v : $ n t and Γ 1 τ =⇒ Γ 1 . By Lemma III.2 we deduce $ n Γ 2 , x : $ n t k Q. From un(Γ 2 ) and Lemma III.1 we deduce Γ 2 = $ n Γ 2 , therefore Γ 1 + $ n Γ 2 is defined. By Lemma B.2(2) we deduce Γ 1 + Γ 2 k Q{v/x}. From [T-IN*] and [T-PAR] we obtain Γ 1 + Γ 2 k Q{v/x} | * a?(x).Q. We conclude by taking Γ = Γ 1 + Γ 2 and observing that Γ act =⇒ Γ .

APPENDIX A

Although the reduction relation defined in Section II is adequate to explain the operational semantics of the language and the deadlock and lock freedom properties, it lacks some important information that is instrumental for the proof of subject reduction. In particular, it is necessary to keep track of the channel on which a synchronization occurs, so that we can suitably update the type of that channel in case it is linear (recall that, by definition, only one synchronization is supposed to occur on a linear channel). To this aim, we define a labeled variant of the reduction relation which keeps track of this information. Labels act, . . . are either channels or the special symbol τ indicating an unobservable reduction. The labeled reduction relation is inductively defined by the rules below:

The two reduction semantics are perfectly equivalent:

Theorem A.1. The predicates P → Q and ∃act :

Proof. A straightforward induction on the derivation of the reduction.

APPENDIX B

A. Definitions

Below is the formal definition of contractive types: we say that a type is contractive if ∅ con(t) is inductively derivable by the rules

where A is a set of type variables. Note that µα.p ι [α] m n is contractive but neither µα.(α × α) nor µα.(α ⊕ α) are. The last one, in particular, seems preventing the definition of any recursive algebraic type. The definition of contractiveness we adopt is convenient for the rest of the technical development but it can be relaxed to allow α be guarded by any constructor, at the cost of definiting the function | • | coinductively (see ( 6)).

B. Basic properties

Below are two auxiliary results regarding the type systems, namely the shifting property and the substitution lemma for expressions and processes. Both results can be easily proved with an induction on the derivation of the judgment in the premise.

Lemma B.1 (Lemma III.2). The following properties hold: i∈I * a i ?(x i ).P i . Proof. From the hypothesis that P is well typed and does not reduce we know that P ≡ (νã)Q where

we deduce Γ 0 Q for some Γ that is balanced. We proceed showing that J = K = ∅ by contradiction. In particular, we show that if J ∪ K = ∅, then it is possible to find an infinite chain of channels with strictly decreasing priorities. This is absurd since Q is finite, so there is a finite number of distinct channels in it.

We begin doing a few generic considerations about the channels occurring in these processes:

• all the a i 's are unlimited channels, because they are used for replicated inputs;

• all the b j are linear channels, because they are used for linear inputs;

• all the c k 's are linear channels, because P → whereas if they were unlimited they would be able to synchronize with one of the replicated inputs (recall that the type system guarantees input receptiveness);

we know that none of the P i 's has free linear channels. Now suppose j ∈ J and Γ (b j ) = ?[t] n m . Since b j is a linear channel, there must be another occurrence of b j with output polarity. We observe that:

• b j is not any of the b l for l ∈ J \ {j}, for the occurrence of b j we are looking for must have output polarity; • b j is not any of the c k 's, because P → and all the e k must be closed and therefore evaluated. We analyze the remaining possibilities:

Since c k is a linear channel, there must be another occurrence of c k with input polarity. We observe that:

• c k is not any of the b j 's, because P →. • c k is not any of the c l for l ∈ K \ {j}, for the occurrence of c k we are looking for must have input polarity. We analyze the remaining possibilities:

where n < n. In conclusion, for every possibility that is not ruled out by simple considerations, from any channel in {b j | j ∈ J} ∪ {c k | k ∈ K} we have been able to find another channel in the same set with a strictly smaller priority. This contradicts the fact that the very same set must be finite.

In order to prove that the type system for lock freedom is sound we need to define the measure of a channel. Intuitively, the measure of a represents an upper bound to the (finite) number of reduction steps that must occur before a synchronization on a occurs. The measure of a channel depends on both its type and the positions in which it occurs in a process. We only consider processes that are well typed in a balanced environment.

We let tickets(t) denote the tickets of a type, which is computed similarly to the priority of a type, except that we consider m in the second equation of [START_REF] Cécé | Verification of programs with half-duplex communication[END_REF].

For example, considering again G d above, we have

assuming that 1 , 2 , and 3 label the three events in G d .

The main result of this section states that the P(∅, G, p)'s are well typed and so is their parallel composition:

Theorem C.3. Let G be realizable. Then for every p ∈ R we have {x pq : T(∅, G, p, q, 0) | q ∈ R \ {p}} 1 P(∅, G, p).

Note that a global type with two participants is always realizable. This corresponds to a binary session.

APPENDIX D PROOFS FOR APPENDIX C

We write p for {?, !} \ p. We write n < G if n < ord( ) for every occurring in G.

Lemma D.1. Let n < G and T(Σ, G, p, q, n) = t. Then:

h k for some p and h > 0. Proof. By induction on G.

• (G = α) We have:

1) (p q ∈ Σ(G)) Then t = int by definition of T.

2) (p q ∈ Σ(α)) Then t = $ 0 1 α pq by definition of T and we conclude by taking h = 0 and k = 1. 3) (p q ∈ G) This case is impossible.

• (G = A → B@ .G ) We have:

1) (p q ∈ Σ(G)) Then p q = A B and p q ∈ Σ(G ) and t = $ -n T(Σ, G , p, q, ) = $ -n int = int by definition of T, by induction hypothesis, and by equality on types. 2) (p q ∈ G and α ∈ fv(G) and p q ∈ Σ(G)) Then p q = A B and p q ∈ G and α ∈ fv(G ). We have

α pq by definition of T and by induction hypothesis. We conclude by taking h = -n + m.

3) (p q ∈ G) Then either p q = A B or p q ∈ G . If p, q = A, B, then t = ![s] h k where h = -n and k = 0 and s = T(Σ, G , q, p, ) and we conclude by observing that h > 0 from the hypothesis n < G. If p, q = B, A we conclude similarly. If p q = A B, then by induction hypothesis we have T(Σ, G , p, q, ) = p[s] m k for some m > 0 and we conclude t = p[s] h k by taking h = -n + m. • (G = A → B@ .{G 1 , G 2 }) This case is similar to the previous one, the only interesting sub-case is when p q ∈ G and α ∈ fv(G) and p q ∈ Σ(G). By definition of global type projection we have t = T(Σ, G i , p, q, ) for every i = 1, 2, therefore we deduce α ∈ fv(G 1 ) ∩ fv(G 2 ). We conclude by induction hypothesis as in the previous case.

and observe that Σ is a sort environment for G and t = $ 0 1 t pq = $ 0 1 T(Σ , G , p, q, n)σ and T(Σ, G, q, p, n) = $ 0 1 t qp = $ 0 1 T(Σ , G , q, p, n)σ. We distinguish three sub-cases: 1) (p q ∈ Σ(G)) Then p q ∈ Σ (G ) and we conclude t = int.

2) (p q ∈ G and p q ∈ Σ(β) and β ∈ fv(G)) Then p q ∈ G and β = α and β ∈ fv(G ). By induction hypothesis we deduce T(Σ , G , p, q, n) = $ h m β pq . We conclude by taking k = m + 1 and observing that t = $ h k β pq . 3) (p q ∈ G) Then p q ∈ G and by induction hypothesis we deduce T(Σ , G , p, q, n) = p[s] h m and T(Σ , G , q, p, n) = p[s] h m for some h > 0. We conclude by taking k = m + 1 and observing that t

m n and m > 0 for every p q ∈ Σ(α).

Proof. We have

property of set union

Lemma D.4. Let

• σ be a Σ-substitution;

• n < G;

• Σ = Σ, α : Σ(µα.G);

• s pq = µα pq .{α pq := T(Σ , G, p, q, n), α qp := T(Σ , G, q, p, n)};

• σ = σ, {s pq σ/α pq } p q⊆R . Then σ is a Σ -substitution.

Proof. We must prove the three conditions of Definition D.2. The first condition is satisfied because dom(σ ) = dom(σ) ∪ {α pq | p q ⊆ R}, so let us consider conditions 2 and 3. For every type variable β = α these conditions are trivially satisfied from the hypothesis that σ is a Σ-substitution, therefore we focus on α. Observe that, by Lemma D.3, we have

Regarding condition 2 of Definition D.2, assume p q ∈ Σ (α) = Σ (G). We conclude σ (α pq ) = s pq σ by definition of σ = T(Σ , G, p, q, n){s pq , s qp /α pq , α qp }σ by unfolding of s pq = int{s pq , s qp /α pq , α qp }σ by Lemma D.1 = int by definition of type substitution Regarding condition 3 of Definition D.2, assume p q ∈ Σ (α) = Σ (G). We distinguish two sub-cases:

• (p q ∈ G and p q ∈ Σ (β) and β ∈ fv(G)) From p q ∈ G we deduce β = α, so σ (α pq ) = T(Σ , G, p, q, n){s pq , s qp /α pq , α qp }σ by definition of σ = $ h k β pq {s pq , s qp /α pq , α qp }σ by Lemma D.

and similarly we obtain σ (α qp ) = p[t] h k . Lemma D.5. Let n < G and σ be a Σ-substitution. Then:

h k and h > 0. Proof. If p q ∈ Σ(G), then by Lemma D.1 we deduce T(Σ, G, p, q, n) = int and we conclude immediately. If p q ∈ Σ(G), then we distinguish two sub-cases:

h k and h > 0. We conclude by taking t = sσ.

• (p q ∈ G and α ∈ fv(G) and p q ∈ Σ(α)) By Lemma D.1 we have T(Σ, G, p, q, n) = $ h k α pq and T(Σ, G, q, p, n) = $ h k α qp . By definition of Σ-substitution we deduce σ(α pq ) = p[s] h k and σ(α qp ) = p[s] h k and h > 0. We conclude by taking h = h + h and k = k + k .

We introduce the following abbreviations for referring to the environments used in the typing derivations of the following lemma:

Lemma D.6. Let σ be a Σ-substitution and n < G. Then Θ [Σ,p] σ, Γ [Σ,G,p,n] σ 1 P(Σ, G, p).

Proof. By induction on G. We omit the cases for choices, since they are analogous to the ones for interactions. G = α Let s pq def = σ(α pq ). We have:

We derive:

where we use the fact that 0 ≤ |(|s pq ) which follows from the hypothesis that σ is a Σ-substitution.

and observe that σ is a Σ -substitution by Lemma D.4. We have:

We derive:

.G and p = A We consider the case A B ∈ Σ(G ), the other being analogous. Then, from Lemma D.5, we know that

for some h, k ∈ N, p ∈ {?, !} such that h > 0, and s. We have:

as well as B:

. . .

IND.HYP.

Θ

Θ [Σ,p] σ, {x pq : $ -n T(Σ, G, p, q, )σ} q =B , x AB : p[s] -n+h k 1 P(Σ, G , p)

[T-LET] Θ [Σ,p] σ, {x pq : $ -n T(Σ, G, p, q, σ)} q =B , a : p[s] -n+h k 1 let x AB = a in P(Σ, G , p) From these we obtain:

A B Θ [Σ,p] σ, {x pq : T(Σ, G , p, q, )σ} q =A , x BA : ?[T(Σ, G , B, A, )σ] 0 0 1 x BA ?(x BA ).P(Σ, G , p) Let G be realizable. Then {x pq : T(∅, G, p, q, 0) | q ∈ R \ {p}} 1 P(∅, G, p) for every p ∈ R.

Proof. Consequence of Lemma D.6 by taking σ = ∅.