Abstract 1 Introduction 2 Session Processes and Their Type Systems 3 The Role of Delayed Actions and Self-Synchronizations in DF 4 The Case of Asynchronous Processes 5 Closing Remarks References

Contrasting Deadlock-Free Session Processes

Juan C. Jaramillo ORCID Unversity of Groningen, The Netherlands Jorge A. Pérez ORCID Unversity of Groningen, The Netherlands
Abstract

Deadlock freedom is a crucial property for message-passing programs. Over the years, several different type systems for concurrent processes that ensure deadlock freedom have been proposed; this diversity raises the question of how they compare. We address this question, considering two type systems not covered in prior work: Kokke et al.’s 𝖧𝖢𝖯, a type system based on a linear logic with hypersequents, and Padovani’s priority-based type system for asynchronous processes, dubbed 𝖯. Their distinctive features make formal comparisons relevant and challenging. Our findings are two-fold: (1) the hypersequent setting does not drastically change the class of deadlock-free processes induced by linear logic, and (2) we relate the classes of deadlock-free processes induced by 𝖧𝖢𝖯 and 𝖯. We prove that our results hold under both synchronous and asynchronous communication. Our results provide new insights into the essential mechanisms involved in statically avoiding deadlocks in concurrency.

Keywords and phrases:
session types, process calculi, deadlock freedom
Funding:
Juan C. Jaramillo: Ministry of Science of Colombia (Minciencias).
Copyright and License:
[Uncaptioned image] © Juan C. Jaramillo and Jorge A. Pérez; licensed under Creative Commons License CC-BY 4.0
2012 ACM Subject Classification:
Theory of computation Type structures
; Theory of computation Program analysis ; Theory of computation Process calculi
Related Version:
Full Version: https://arxiv.org/abs/2504.15845 [19]
Acknowledgements:
We are grateful to Channa Dias Perera for initial discussions on the topics of this paper. We also thank Andreia Mordido and the anonymous reviewers for their helpful suggestions.
Editors:
Jonathan Aldrich and Alexandra Silva

1 Introduction

The deadlock freedom property (DF, in the following) is a crucial guarantee for message-passing programs. Informally, DF ensures that processes “never get stuck” – an essential requirement in concurrent and distributed software systems, where even a single component that becomes permanently blocked while waiting for a message can compromise reliability. As illustration, consider a toy concurrent program in the language of Gay and Vasconcelos [14]:

𝗅𝖾𝗍(x1,z)=𝗋𝖾𝖼𝖾𝗂𝗏𝖾x1𝗂𝗇𝗌𝖾𝗇𝖽  42y1𝗅𝖾𝗍(y2,k)=𝗋𝖾𝖼𝖾𝗂𝗏𝖾y2𝗂𝗇𝗌𝖾𝗇𝖽𝚑𝚎𝚕𝚕𝚘x2

We have two concurrent threads, each running an expression with two actions in sequence. This program is evaluated under a context that binds together x1 and x2 and declares them as endpoints of the same linear channel (same for y1 and y2); we omit it for readability. Given a linear channel x, “𝗌𝖾𝗇𝖽𝚟x” sends value 𝚟 along x and returns the continuation of x, whereas “𝗋𝖾𝖼𝖾𝗂𝗏𝖾x” returns a pair with the continuation of x and a received value. The threads are thus engaged in separate but intertwined protocols (one along xi, the other along yi). Each thread should receive on a channel and then send a value on the other. However, the output matching the input in one thread is blocked in the other – the program is stuck. The key challenge in enforcing DF is thus performing the non-local analysis needed to avoid circular dependencies between threads, which are often less apparent than in this program.

An expressive model for concurrent processes, the π-calculus offers a convenient basis for developing analysis techniques for message-passing programs in different paradigms [32]. Several type systems that enforce (forms of) DF have been proposed over the years (see, e.g., [21, 11, 5, 27, 7, 34, 1]). They avoid circular dependencies in processes using different insights, which raises the question of how they compare. In this paper, we rigorously compare some representative type systems for DF to better understand their underlying mechanisms.

A key motivation for studying type systems for concurrent processes is their suitability for developing advanced analysis techniques at an appropriate level of abstraction – these typed frameworks have been directly incorporated into languages such as Scala [33], OCaml [28, 17], and Rust [24]. Also, concurrent processes offer an adequate representation level for verifying liveness properties in real Go programs [25, 26]. Moreover, type systems for the π-calculus are the basis for static analyzers (such as Kobayashi’s TyPiCal [20]) and can be ported to enforce DF for higher-order concurrent programs [29]. Type systems based on the Curry-Howard correspondence between session types and linear logic (“propositions-as-sessions” [3, 37]) enforce DF; they entail topological invariants on processes, key to ensure deadlock and memory leak freedom in concurrent programs [18]. Further understanding the essential mechanisms that enforce DF in logic-based session types is a central topic in our work.

Prior work by Dardha and Pérez [9] contrasts type systems for DF by relating the classes of processes they induce. They compare a priority-based type system by Kobayashi [21] and a type system derived from “propositions-as-sessions”. Writing 𝕂 and 𝕃 to denote the respective classes of processes, a result in [9] is that 𝕃𝕂: there exist deadlock-free processes that cannot be typed by logic-based type systems. The class 𝕂𝕃 includes, for instance, process networks organized in circular topologies (e.g., the dinning philosophers). It also includes process P0 below, in which two processes interact along independent protocols (sessions):

P0(νx1x2)(νy1y2)(x1(z).y1¯𝟺𝟸.0|x2¯𝚑𝚎𝚕𝚕𝚘.y2(k).0)

Above, “(νx1x2)” declares a new session with linear endpoints x1 and x2, and “x(y).Q” (resp. “x¯v.Q”) denotes an input (resp. output of value v) along x with continuation Q. P0 is the deadlock-free variant of the program given above, now neatly specified as a process. In 𝕃, processes can share at most one session in parallel, whereas processes in P0 share two: the session “x1x2” for exchanging “𝚑𝚎𝚕𝚕𝚘” and the session “y1y2” for exchanging “𝟺𝟸”. In [9], both compared classes rely on a reduction semantics; accordingly, DF concerns the absence of stable states with pending reduction steps on linear names/channels.

Here we extend the work in [9] by considering type systems not studied there: (i) Kokke et al.’s 𝖧𝖢𝖯 [23] and (ii) Padovani’s priority-based type system [27], here dubbed 𝖯. Their distinctive features make formal comparisons relevant and challenging, as we discuss next.

Derived from “propositions-as-sessions”, 𝖧𝖢𝖯 is based on a presentation of classical linear logic (CLL) with hypersequents. 𝖧𝖢𝖯 has been studied in several works, which have deepened into its theory and applications [22, 12, 31]. In 𝖧𝖢𝖯, the semantics of processes is given by a Labeled Transition System (LTS), rather than by a reduction semantics. This unlocks the use of well-established analysis techniques, notably observational equivalences, to reason about typed processes. The (typed) LTS for 𝖧𝖢𝖯 includes the usual rules for observing actions and synchronizations, here dubbed regular transitions, but also rules that allow for delayed actions (i.e., observable actions due to prefixes not at top-level) and self-synchronizations (i.e., internal actions that do not require the interaction of two parallel processes). Remarkably, the bisimilarity induced by the LTS coincides, in a fully-abstract way, with a denotational equivalence over processes – this gives a strong justification for the design of the LTS. Typing ensures progress: well-typed processes not equivalent to 𝟎 always have a transition step.

An intriguing observation is that there are 𝖧𝖢𝖯 processes that are stuck in a reduction-based setting but have synchronizations under 𝖧𝖢𝖯’s LTS. We discuss two interesting examples, using “x().Q” and “x¯.Q” to denote empty inputs and outputs, respectively:

  • Process P1(νxx)x¯.x().0 is self-synchronizing: it does not have any reductions, whereas P1𝜏𝟎, as in 𝖧𝖢𝖯 synchronizations do not need a parallel context to be enabled.

  • Process P2(νxx)(νyy)(y¯.x().0|x¯.y().0) is arguably the paradigmatic example of a deadlock, with two independent sessions unable to reduce. In 𝖧𝖢𝖯, thanks to delayed actions, we have both P2𝜏(νyy)(y¯.0|y().0) and P2𝜏(νxx)(x¯.0|x().0).

This observation shows that comparisons such as [9] should accommodate other semantics for processes, beyond reductions, which entail other definitions of DF and induce new deadlock-free processes (such as P1 and P2). This begs a first question:

(Q1)

What is the status of delayed actions and self-synchronizations, as typable in 𝖧𝖢𝖯, with respect to DF? Do they induce a distinct class of deadlock-free processes?

Considering Padovani’s 𝖯 means addressing the case of processes with asynchronous communication, widely used in real programs. In the π-calculus, asynchronous communication is obtained by defining outputs as non-blocking actions; only inputs can block the execution of a process [2, 16]. Asynchrony and DF are then closely related: because an asynchronous setting involves the least amount of blocking operations, it offers the most elementary scenario for investigating DF [35]. Now, the comparisons in [9] are limited to synchronous processes; we then observe that they should be extended to address asynchronous communication, too. Let us write and to denote the class of processes induced by 𝖧𝖢𝖯 and 𝖯, respectively, and to denote the class of processes induced by 𝖢𝖯 (a fragment of 𝖧𝖢𝖯 without hypersequents and with a restricted form of parallel composition). We consider the second question:

(Q2)

What is the status of and with respect to asynchronous processes in ?

Interestingly, our two questions are intertwined: 𝖧𝖢𝖯 and 𝖯 are related due to asynchrony. Our insight is that delayed actions in 𝖧𝖢𝖯 already implement an asynchronous semantics. To see this, consider the process P3(νxx)(νyy)(y¯.x¯.0|x().y().0), which is not stuck: the output on y is not really blocking, as delayed actions allow to anticipate the output (and synchronization) on x. In other words, P3 is morally the same as (νxx)(νyy)(y¯.0|x¯.0|x().y().0). We thus conclude that the (typed) operational semantics for 𝖧𝖢𝖯 admits many synchronous-looking processes (such as P3) that actually behave in an asynchronous way; this naturally invites the question of how relates to .

Contributions and Outline.

This paper offers conceptual and technical contributions. From a conceptual view, we reflect upon the significance of formally comparing different type systems for concurrency, while uniformly presenting various notions in the literature. On the technical side, we address (Q1) and (Q2), thus extending and complementing [9]. A key discovery is identifying commuting conversions and disentanglement as key notions for characterizing deadlock-free processes in 𝖧𝖢𝖯 – as we will see, these notions define sound process optimizations that respect causality and increase parallelism. As our results hold also in an asynchronous setting, not treated in prior work, our findings are most related to abstractions and mechanisms used in practical concurrent programming. More in detail:

§ 2

We introduce 𝖲𝖯, a session π-calculus that we use as baseline for comparisons, as well as 𝖢𝖯 and 𝖧𝖢𝖯, the type systems resulting from the Curry-Howard correspondence with CLL and CLL with hypersequents, respectively.

§ 3

We define  and : the classes of deadlock-free 𝖲𝖯 processes induced by 𝖢𝖯 and 𝖧𝖢𝖯, respectively. We identify two relevant sub-classes of :

𝖥:

Processes that use the 𝖥ull LTS.

𝖱:

Processes that only use 𝖱egular transitions (no delayed actions/self-synchronizations).

In our main result (Corollary 53), we prove that for every process P𝖥, there exists an observationally equivalent process P𝖱. Enabled by process optimizations induced via commuting conversions and disentanglement, this result shows that delayed actions and self-synchronizations are inessential when it comes to DF, addressing (Q1).

§ 4

To address (Q2), we define : the class of deadlock free 𝖲𝖯 processes induced by 𝖯, and its sub-class μ (“micro ”), which is inspired by 𝖢𝖯. We prove that =μ (Corollary 74), thus casting Dardha and Pérez’s key finding into the asynchronous setting. Our main results are: Theorem 76, which precisely relates the classes , 𝖥, 𝖱, and ; and Corollary 77, which strengthens Corollary 53 by considering DF in . Moreover, we introduce 𝖲𝖯𝔞, an asynchronous variant of 𝖲𝖯, and its corresponding classes of processes. We show how to transfer Theorems 76 and 77 from 𝖲𝖯 to 𝖲𝖯𝔞 (Corollary 88).

Figure 1 offers a graphical description of the classes of processes and some of our main results (Corollaries 53, 74, and 76). For simplicity, the figure does not depict several encodings needed to bridge syntactic differences between the various classes of processes / type systems under consideration; Figure 12 (Page 12) presents a detailed version. In § 5 we collect some closing remarks. The extended version of the paper [19] contains omitted proofs.

Figure 1: Overview of main results. Above, 𝖥, 𝖱, , , and μ stand for classes of deadlock-free 𝖲𝖯 processes. The red arrow represents optimizations (commuting conversions and disentanglement) that relate 𝖥 and 𝖱. The green lines denote the correspondence =μ. The dotted line means that P and P′′ are the representatives of P in 𝖱 and , up to an encoding.

2 Session Processes and Their Type Systems

We present 𝖲𝖯, our reference language of session processes. As observed by Dardha and Pérez [9], this is a convenient framework for formal comparisons, because typing in 𝖲𝖯 ensures communication safety but not DF. We also present 𝖢𝖯 and 𝖧𝖢𝖯, the two typed languages based on “propositions-as-sessions”, and recall useful associated results.

2.1 Session Processes (𝗦𝗣)

𝖲𝖯 is a core session-typed π-calculus, based on the language defined by Vasconcelos [36]. We assume a base set of variables, ranged over by x,y,, which denote channels (or names): they can be seen as endpoints on which interaction takes place. Processes interact to exchange values v,v,; for simplicity, values correspond to variables, i.e., v::=x. We write x~ to denote a finite sequence of variables. The syntax of processes is as follows:

P ::= 0|x¯v.P|x(y).P|P1|P2|(νxy)P|x¯.P|x().P

Process 𝟎 denotes inaction. Process x¯v.P sends v along x and continues as P. Process x(y).P receives v along x and continues as P{v/y}, i.e., the process resulting from the capture-avoiding substitution of y by v in P. Process P1|P2 denotes the parallel execution of P1 and P2. Process (νxy)P declares x and y as co-variables, restricting their scope to P. That is, restriction declares co-variables as dual ends of a channel. Finally, x¯.P and x().P denote empty output and input (close and wait), which represent the closing of session x.

As usual, x(y).P binds y in P and (νxy)P binds x,y in P. The sets of free and bound variables of P, denoted 𝚏𝚟(P) and 𝚋𝚟(P), are defined accordingly. The semantics of processes is given using a reduction relation, defined next.

Definition 1 (𝖲𝖯: Reduction).

Reduction for 𝖲𝖯, denoted , is defined by the rules in Figure 2 (top). It relies on structural congruence, denoted , the smallest congruence on processes that satisfies the axioms in Figure 2 (bottom).

We now define session types, which express protocols associated to channels:

Definition 2 (𝖲𝖯: Session Types and Typing Environments).

The syntax of session types and typing environments is inductively defined as follows:

T,S::=?S.T|!S.T|𝖾𝗇𝖽?|𝖾𝗇𝖽!Γ::=|Γ,x:T

The type !S.T (resp. ?S.T) is assigned to a channel able to send (resp. receive) a value of type S and to continue as T. For convenience, we have two different types for channels with terminated protocols, denoted 𝖾𝗇𝖽? and 𝖾𝗇𝖽!. Duality on types ensures that the endpoints of a channel agree on the protocol they describe:

Definition 3 (𝖲𝖯: Duality).

The dual of S, denoted S¯, is defined as follows:

?S.T¯!S.T¯!S.T¯?S.T¯𝖾𝗇𝖽?¯𝖾𝗇𝖽!𝖾𝗇𝖽!¯𝖾𝗇𝖽?
Figure 2: 𝖲𝖯: Reduction semantics (top) and structural congruence (bottom).
Figure 3: 𝖲𝖯: Typing Rules for Processes.
Definition 4 (𝖲𝖯: Typing Judgment and Typing Rules).

The judgment Γ𝚂P describes a well-typed process under the typing environment Γ. The typing rules for 𝖲𝖯 are shown in Figure 3. We shall write P𝖲𝖯 if Γ𝚂P, for some Γ.

We now state the properties of well-typed 𝖲𝖯 processes, whose proofs follow [36]:

Theorem 5 (𝖲𝖯: Preservation [36]).

Suppose Γ𝚂P. If PQ then Γ𝚂Q. Also, if PQ then Γ𝚂Q.

We will be interested in well-formed processes, defined using two auxiliary notions. First, we say that P is prefixed at x, written 𝙿𝚛(P)=x, if P has one of the following forms: x().P, x¯.P, x(z).P, or x¯v.P. Second, we say a process (νxy)(P|Q) is a redex if: (1) P=x().P and Q=y¯.Q, or (2) P=x(z).P and Q=y¯v.Q. We may now define:

Definition 6 (𝖲𝖯: Well-formedness).

A process is well-formed if for each of its structural congruent processes of the form (νx1y1)(νxnyn)(P1||Pm) where 𝙿𝚛(Pi)=xk and 𝙿𝚛(Pj)=yk, then (νxkyk)(Pi|Pj) is a redex.

Theorem 7 (Safety [36]).

Typable processes are well-formed.

As a consequence of Theorems 5 and 7 we obtain the main guarantee of 𝖲𝖯: typable processes only reduce to well-formed processes.

Corollary 8 ([36]).

If Γ𝚂P and PQ, then Q is well-formed.

Even though typability ensures well-formedness, which excludes error processes such as (νxy)(x¯v.P|y().Q) and (νxy)(x().P|y().Q), typability in 𝖲𝖯 also admits well-typed process that exhibit unwanted behaviors, in particular deadlocks. Before illustrating this fact, we give the first definition of deadlock freedom that we will encounter, which follows [9]. We write (νxy~)Q to stand for (νx1y1)(νxnyn)Q, for some n0.

Definition 9 (𝖲𝖯: Deadlock Freedom).

A process P𝖲𝖯 is deadlock free, written 𝒟𝐒(P), if the following condition holds: whenever PP and one of the following holds: (1) P(νxy~)(xi¯v.Q1|Q2), (2) P(νxy~)(xi(z).Q1|Q2), (3) P(νxy~)(xi().Q1|Q2), or (4) P(νxy~)(xi¯.Q1|Q2) (with xix~ in all cases), then PR, for some R.

Hence, 𝒟𝐒(P) is read as “P is deadlock-free in 𝖲𝖯”. Later on, we will encounter analogous notations for 𝖧𝖢𝖯 and 𝖯; they will be denoted 𝒟𝐇(P) and 𝒟𝐏(P), respectively.

Example 10 (𝖲𝖯: A Typable but Deadlocked Process).

Consider the process P10 defined as

P10(νx1y1)(νx2y2)(νv1k1)(νv2k2)(x1(z1).x2(z2).C1|y2¯v2.y1¯v1.C2)

where C1x1().x2().z1().z2().0 and C2y1¯.y2¯.k1¯.k2¯.0. Similar to P2 (§ 1), the structure of actions in process P10 induces a circular dependency that prevents synchronizations: we have that ¬𝒟𝐒(P10) and yet P10 is well-typed with the empty environment.

2.2 𝗖𝗣 and 𝗛𝗖𝗣

The languages 𝖢𝖯 and 𝖧𝖢𝖯 use the same syntax. Here we consider 𝖧𝖢𝖯 as presented by Kokke et al. [23] (other variants have been studied in, e.g., [13]). Assuming an infinite set of names (x,y,z,), the set of processes (P,Q,) in 𝖢𝖯 and 𝖧𝖢𝖯 is defined as follows:

P,Q::=𝟎 |(νxy)P|P|Q|[xy]|x[y].P|x(y).P|x[].P|x().P

Most constructs are similar to those in 𝖲𝖯; differences are the forwarder process [xy], which equates x and y, and process x[y].P, which denotes the output of the private name y along x, with continuation P. Also, the empty output is now denoted x[].P. In x[y].P and x(y).P, the name y is bound in P. We write P{x/y} to denote the capture-avoiding substitution of y for x in P. We write 𝖿𝗇(P) to denote the free names of P. We use π to range over prefixes: x[y],x(y),x(), x[].

The types assigned to names correspond to formulas of classical linear logic (CLL):

A,B::=𝟏||AB|A&B

The assignment x:A says that x follows the input/output interactions described by A. Assignments x:AB and x:A&B are read as sending and receiving an object of type A along x, with continuation B, respectively. There is a duality in the interpretation of the following pairs: and &; 𝟏 and . Formally, the dual type of A, denoted A, is defined as

𝟏𝟏(AB)A&B(A&B)AB

Let Γ,Δ range over environments, unordered collections of assignments. Given an environment Δ=x1:A1,,xn:An, its domain, written dom(Δ), is the set {x1,,xn}.

Definition 11 (𝖢𝖯).

Typing judgements for 𝖢𝖯 are of the form P𝙲Γ, with typing rules as given in Figure 4. We shall write P𝖢𝖯 if P𝙲Γ, for some Γ.

Figure 4: 𝖢𝖯: Typing rules for processes.

Observe how typing in 𝖢𝖯 induces a specific shape for output processes: x[y].(P|Q). This is not the case in 𝖧𝖢𝖯, where processes are described by hyperenvironments, unordered collections of environments: ,𝒢::=Γ1Γn.

Definition 12 (𝖧𝖢𝖯).

Typing judgements for 𝖧𝖢𝖯 are of the form P𝙷𝒢, with typing rules as given in Figure 5. We shall write P𝖧𝖢𝖯 if P𝙷𝒢, for some 𝒢.

Figure 5: 𝖧𝖢𝖯: Typing rules for processes.

𝖢𝖯 and 𝖧𝖢𝖯 differ in process composition, which is key to exclude the circular dependencies that lead to deadlocks: it is realized by Rule C-Cut in 𝖢𝖯 and Rule H-Cut in 𝖧𝖢𝖯. The former requires two premises describing processes that share exactly one session; typing involves both composition and restriction and induces tree-like process topologies. The latter involves one premise only, which describes a process in which the separation between x and y is made explicit by “” at the level of hyperenvironments; typing involves restriction only.

Every P typable in 𝖢𝖯 is also typable in 𝖧𝖢𝖯, but the converse does not hold. We have:

Lemma 13 (Relation Between 𝖢𝖯 and 𝖧𝖢𝖯 [23]).

If P𝙲Γ then P𝙷Γ.

Example 14 (The converse of Lemma 13 does not hold).

To illustrate a process typable in 𝖧𝖢𝖯 but not in 𝖢𝖯, consider P14(νx1y1)(νx2y2)(νv1k1)(νv2k2)(P14|P14′′), where:

P14 x1(z1).x2(z2).x1().x2().z1().z2().0
P14′′ y1[v1].([v1v1]|y2[v2].([v2v2]|C)) C y1[].0|y2[].0|k1[].0|k2[].0

We have P14𝙷. First, P14𝙷x1:&,x2:& follows from several applications of Rules H- and H-&. To type P14′′, we first obtain C𝙷y1:𝟏y2:𝟏k1:𝟏k2:𝟏, crucially using Rule H-Mix2 several times to compose the four independent processes. Because [v2v2]𝙷v2:𝟏,v2:, by Rules H-Mix2 and H- we have: y2[v2].([v2v2]|C)𝙷y1:𝟏y2:𝟏𝟏,v2:k1:𝟏k2:𝟏. We proceed similarly to type the output on y1 and complete the typing of P14′′. Finally, to compose P14 and P14′′ we apply H-Mix2 and H-Cut.

Now, C cannot be typed in 𝖢𝖯: there is no rule similar to Rule H-Mix2, which can compose independent processes. Hence, P14 is not typable in 𝖢𝖯.

In general, the composition of two processes that share more than one session cannot be typed in 𝖢𝖯. Now consider Q14:

Q14(νv2k2)((νv1k1)((νx2y2)((νx1y1)( P14|y1[v1].([v1v1]|y1[].0)
| y2[v2].([v2v2]|y2[].0))|k1[].0)|k2[].0)

Observe how Q14 modifies P14 by keeping P14 unchanged and dividing the two outputs in P14′′ into threads that can be composed separately using Rule C-Cut. We have Q14𝙲.

Given a P𝙷𝒢, with 𝒢=Γ1Γn, we are interested in partitioning the free names in P according to the environments Γ1,,Γn. These name partitions describe which names are used by each parallel component of P; they are defined considering all the different hyperenvironments under which P is typable.

Definition 15 (𝖧𝖢𝖯: Name Partitions).

Given 𝒢=Γ1Γn, we define 𝖯𝖺𝗋𝗍(𝒢)={dom(Γ1),,dom(Γn)}. Given P, its name partitions are 𝗇𝗉(P)={𝖯𝖺𝗋𝗍(𝒢)|P𝙷𝒢}.

xPy holds whenever there is a G𝗇𝗉(P) such that x and y belong to different proper subsets of G. Also, xPy holds whenever x and y belong to the same proper subset of G.

Example 16.

Consider the process P16x().(z[].0|y[].0): it can be typed under the hyperenvironments 𝒢x:,z:𝟏y:𝟏 and z:𝟏x:,y:𝟏. Given this, 𝗇𝗉(P16)={{{x,z},{y}},{{z},{x,y}}}, and we have, e.g., yP16z and xP16y.

The semantics of 𝖧𝖢𝖯 is given in terms of a Labeled Transition System (LTS):

Definition 17 (𝖧𝖢𝖯: LTS).

The binary relation on 𝖧𝖢𝖯 processes 𝑙 is defined by the rules in Figure 6, with action labels defined as follows:

l,l::=[xy]|x[y]|x(y)|x()|x[]|l|l|τ

In the following, 𝖿𝗇(l), 𝖻𝗇(l), and 𝖼𝗇(l) denote the free, bound, and channel names of l, respectively. They are defined as follows: 𝖿𝗇([xy]){x,y}, 𝖿𝗇(τ)=𝖻𝗇(τ), 𝖿𝗇(x[y])=𝖿𝗇(x(y))=𝖿𝗇(x())=𝖿𝗇(x())x, and 𝖻𝗇(x[y])=𝖻𝗇(x(y)){y}. Also, 𝖿𝗇(l1|l2)𝖿𝗇(l1)𝖿𝗇(l2), and 𝖻𝗇(l1|l2)𝖻𝗇(l1)𝖻𝗇(l2). Moreover, 𝖼𝗇(l)𝖿𝗇(l)𝖻𝗇(l).

The rules in Figure 6 are inspired by proof-theoretical transformations on 𝖧𝖢𝖯’s proof derivations [23]; they can be divided into two classes. The rules above the line are usual formulations for actions, structural rules, and communication. Actions can appear in parallel in a label, and compatible actions in parallel induce a τ-transition. The five rules below the line formalize delayed actions and self-synchronizations. Intuitively, the first four rules allow to observe an action l in a delayed style; such an action must be independent from the prefix at the top-level (on x). The last rule, |π, implements self-synchronization for a process π.P: the (top-level) prefix π is considered in parallel with a (delayed) action l emanating from P.

Figure 6: The LTS for 𝖧𝖢𝖯 (Definition 17) includes rules for actions and communication (top) and for delayed actions and self-synchronizations (bottom).
Example 18.

To illustrate the LTS of 𝖧𝖢𝖯, recall the processes P1 and P2 from § 1. In 𝖧𝖢𝖯, they are denoted as: P18(νxx)(x[].x().0) and Q18(νxx)(νyy)(y[].x().0|x[].y().0). Consider the following type derivation, parametric on w,z:

Thus, P18 is typed as Πx,x followed by an application of Rule H-Cut. Also, Q18 is typed by Πx,y and Πy,x followed by an application of Rules H-Mix2 and H-Cut. Because Rule C-𝟏 only types empty outputs followed by 𝟎, neither P18 nor Q18 are typable in 𝖢𝖯.

By Rules |π and 𝟏 in Figure 6, P18𝜏𝟎. Similarly, y[].x().0|x[].y().0x()|x[]y[].0|y().0 by Rules π,π1 and syn. Finally, by Rule 𝟏, Q18𝜏(νyy)(y[].0|y().0).

We now recall some useful notions and results from [23].

Definition 19 (𝖧𝖢𝖯: Weak LTS and Bisimilarity [23]).

𝑙 is the smallest relation such that: (1) P𝜏P for all P; (2) and if P𝜏P, P𝑙Q, and Q𝜏Q, then P𝑙Q.
A symmetric relation is a bisimulation if PQ implies that if P𝑙P then Q𝑙Q for some Q such that PQ. Bisimilarity is the largest relation 𝙷 that is a bisimulation.

Well-typed processes satisfy readiness, defined as follows:

Theorem 20 (𝖧𝖢𝖯: Readiness [23]).

Let P𝙷Γ1Γn. For every i[1,n], there exist xdom(Γi), lx, and P such that PlxP.

In 𝖧𝖢𝖯, transitions associated to sessions in different partitions can be fired in parallel:

Lemma 21 ([23]).

If P𝙷𝒢Γ,x:AΔ,y:B, PlxP, and PlyP′′, then there exists Q s.t. Plx|lyQ (up to α-renaming).

Definition 22 (𝖧𝖢𝖯: Structural Congruence).

Let 𝙷 be the smallest congruence relation generated by the axioms:

P|Q 𝙷Q|P P| 0 𝙷P
P|(Q|R) 𝙷(P|Q)|R (νxy)P 𝙷(νyx)P
(νxy)P|Q 𝙷(νxy)(P|Q)if x,y𝖿𝗇(Q) (νxy)(νwz)P 𝙷(νwz)(νxy)P

Because of Readiness (Theorem 20), 𝖧𝖢𝖯 also satisfies progress:

Corollary 23 (𝖧𝖢𝖯: Progress [23]).

If P𝖧𝖢𝖯 and P𝙷𝟎, then P𝑙P for some l, P.

In order to relate with reduction-based semantics (in 𝖲𝖯), we define the following:

Definition 24 (𝖧𝖢𝖯: Reduction).

We write for the reflexive, transitive closure of 𝜏.

Lemma 25.

Let P 𝖧𝖢𝖯 s.t. P𝙷, then exists P s.t. PP𝙷𝟎.

Proof sketch.

We prove it in two steps: (1) We prove that if P𝙷𝟎, then there exists P s.t. P𝜏P, and P𝙷. This ensures the existence of a τ-transition in every step. (2) We then prove that 𝟎 can be reached in finitely many steps. See [19] for details.

Inspired by Lemma 25 we have the following definition of deadlock freedom for 𝖧𝖢𝖯.

Definition 26 (𝖧𝖢𝖯: Deadlock Freedom).

Let P𝖧𝖢𝖯. We say that P is deadlock free, written 𝒟𝐇(P), iff there exists P s.t. PP𝙷𝟎.

𝖧𝖢𝖯 has a denotational semantics that interprets well-typed processes as sets of possible interactions on their free names. Given a process P, its set of denotations is written P. Denotational equivalence, noted , is the typed relation defined as: PQ iff P=Q. We shall rely on denotational equivalence; its exact formulation, given in [19], is interesting but not crucial for following our results. We notice that 𝙷 is sound wrt and that our results are reflected by bisimilarity, as ensured by the following result:

Theorem 27 (𝖧𝖢𝖯: Full Abstraction [23]).

For well-typed processes: 𝙷=.

3 The Role of Delayed Actions and Self-Synchronizations in DF

We have seen that 𝖲𝖯 defines a flexible typing discipline that admits deadlocked and deadlock-free processes. Also, we saw the way in which 𝖢𝖯 and 𝖧𝖢𝖯 enforce DF by typing, and that the latter’s LTS allows for delayed actions and self-synchronizations. By defining two classes of 𝖲𝖯 processes, and , which capture typability as in 𝖢𝖯 and 𝖧𝖢𝖯, respectively (Definition 34), we study whether delayed actions and self-synchronizations influence DF.

We proceed as follows. As we have seen, 𝒟𝐇(P) means that P is deadlock free by considering all sources of behavior, including delayed actions and self-synchronizations; we shall also define 𝒟𝐇𝖱(P) to mean that P is deadlock free by considering regular transitions only. Our main result is Corollary 53, which ensures: (1) delayed actions and self-synchronizations are inessential when it comes to DF, and (2) given an encoding :𝖲𝖯𝖧𝖢𝖯, for a process P𝖲𝖯 such that 𝒟𝐇(P), there is a P that simulates P, and 𝒟𝐇𝖱(P).

3.1 From 𝗦𝗣 to 𝗛𝗖𝗣

We start by translating processes in 𝖲𝖯 into processes in 𝖧𝖢𝖯:

Definition 28.

Let P𝖲𝖯. The encoding :𝖲𝖯𝖧𝖢𝖯 is a homomorphism except for the case of free output, defined as x¯v.Px[y].([yv]|P). For types, we define:

𝖾𝗇𝖽?𝖾𝗇𝖽!𝟏?T.ST&S!T.STS

For typing environments, we define: and Γ,x:TΓ,x:T.

Regular Transitions do not depend on self-synchronizations or delayed actions:

Definition 29 (𝖧𝖢𝖯: Regular Transitions).

A derivation T for P𝑙Q is denoted T:P𝑙Q. We define 𝖱𝖳(T) iff T is derived only using rules above the horizontal line in Figure 6.

Example 30.

Recall the processes P18 and Q18 from Example 18, which use self-synchronizations and delayed actions, respectively: we have that T1:P18𝜏𝟎, and T2:Q18𝜏(νyy)(y[].0|y().0). Therefore, ¬𝖱𝖳(T1) and ¬𝖱𝖳(T2).

The encoding of free output induces transitions involving the forwarder process, not present in the source 𝖲𝖯 process. We handle the substitutions induced by forwarders in Rule AxCut (Figure 6) as follows:

Definition 31 (𝖧𝖢𝖯: Ready-for-Substitution).

Let P 𝖧𝖢𝖯. We say that P=(νxy)P is ready for substitution of z for x, written 𝖱𝖲z,x(P), if there exists z𝖿𝗇(P) and P s.t. P[yz]P, and (νxy)P𝜏P{x/z}. Otherwise, we write ¬𝖱𝖲(P).

We may now define transitions for processes that are ready for a substitution.

Definition 32 (𝖧𝖢𝖯: Eager-to-Rename).

The relation 𝙴𝚁𝑙 on 𝖧𝖢𝖯 processes is defined as:

(P𝑙Q)𝖱𝖲x,z(Q) P𝙴𝚁𝑙Q{x/z}and(P𝑙Q)¬𝖱𝖲(Q)P𝙴𝚁𝑙Q

Intuitively, 𝙴𝚁𝑙 executes outputs and forwarders in one single step. When P only relies on regular transitions we have the following operational correspondence result.

Theorem 33 (: Operational Correspondence).

Let P.

  1. 1.

    If T:P𝙴𝚁𝜏R and 𝖱𝖳(T), then PQ s.t. Q𝙷R.

  2. 2.

    If PQ, then P𝙴𝚁𝜏R s.t. R𝙷Q.

Proof sketch.

Part (1) is proven by case analysis in 𝜏, and (2) is proven by induction in the derivation of . See [19] for details.

Following Dardha and Pérez [9], we now define and as the classes of 𝖲𝖯 processes that are also typable in 𝖢𝖯 and 𝖧𝖢𝖯, respectively:

Definition 34 (Classes and ).

The classes and of 𝖲𝖯 processes are defined as:

{P𝖲𝖯|Γ𝚂PP𝙲Γ}
{P𝖲𝖯|Γ𝚂PΓ=Γ1,,ΓnP𝙷Γ1Γn}

Hence, in writing “P” we are not referring to an 𝖧𝖢𝖯 process directly, but rather to a 𝖲𝖯 process P (in the sense of § 2.1) that is related (up to ) to some (typable) 𝖧𝖢𝖯 process. This is how 𝖲𝖯 offers a unifying framework for comparing different type systems. As a direct consequence of Lemma 13 and Example 14 we have that .

3.2 A Refined Account of , Based on Deadlock Freedom

As explained in the previous section, 𝖧𝖢𝖯 enjoys liveness properties corresponding to the LTS. If we focus only on τ-transitions (cf. Definition 24) we obtain the following results.

We extend Definition 29 (regular transitions) to sequences of transitions, as follows:

Definition 35 (𝖧𝖢𝖯: Regular Sequence of Transitions).

Assume P1,,Pn in 𝖧𝖢𝖯 and transitions Ti:PiliPi+1. We say that a transition sequence ρ:Pl1lnPn transitions regularly iff 𝖱𝖳(Ti) for all i=1,,n. We write 𝖱𝖳(ρ).

We are interested in processes whose transitions are regular, thus we refine deadlock freedom in 𝖧𝖢𝖯 (Definition 26) as follows:

Definition 36 (𝖧𝖢𝖯: Deadlock Freedom based on Regular Transitions).

Let P𝖧𝖢𝖯. We say that P is deadlock free without delayed actions and self-synchronizations, written 𝒟𝐇𝖱(P), iff 𝒟𝐇(P), ρ:PP𝙷𝟎, and 𝖱𝖳(ρ).

In turn, Definitions 26 and 36 allow us to refine the definition of (Definition 34):

Definition 37 (𝖧𝖢𝖯: Sub-classes of ).

We define the following classes of DF processes:

𝖥 {P|𝒟𝐇(P)}𝖱{P|𝒟𝐇𝖱(P)}

By Definitions 34 and 37 we have 𝖱𝖥.

Example 38.

Consider the 𝖲𝖯 processes:

P38(νwz)(w¯.(νxy)(x¯.0|y().z().0))Q38(νwz)(w¯.0|(νxy)(x¯.0|z().y().0))

We have P38𝖥𝖱 and Q38𝖱. Although ¬𝒟𝐒(P38), the 𝖧𝖢𝖯 process P38 has a τ-transition due to a delayed action, and therefore 𝒟𝐇(P38).

Theorem 39.

If P𝖱, then 𝒟𝐒(P).

Proof.

It follows from Theorem 33 and Definitions 37 and 9.

From 𝗙 to 𝗥 via process optimizations.

We now embark to show how to transform processes in 𝖥 (where self-synchronizations and delayed actions are used) into processes in 𝖱 (where they are not). Intuitively, we would like to transform, e.g.,

(νwz)(w¯.(νxy)(x¯.0|y().z().0))into(νwz)(w¯.0|(νxy)(x¯.0|z().y().0))

The transformation from 𝖥 to 𝖱 is formalized by Theorem 47. To achieve it, we leverage two existing ingredients. The first ingredient is the notion of commuting conversions: sound transformations on processes that involve actions from independent sessions (cf. [10, 30]).

Definition 40 (𝖧𝖢𝖯: Commuting Conversions).

We define 𝑐𝑐 as the smallest congruence on 𝖧𝖢𝖯 processes induced by the equalities in Figure 7.

Figure 7: 𝖧𝖢𝖯: Commuting Conversions (Definition 40).

The transformations induced by 𝑐𝑐 have a proof-theoretical origin, and so they are type-preserving, which ensures that they do not alter the causality relations on processes. We can show that that 𝑐𝑐 is sound wrt 𝙷, i.e., if P𝑐𝑐Q then P𝙷Q.

Example 41.

Recall processes P14, P14′′, and P14 from Example 14. We illustrate the optimizations on processes induced by commuting conversions by combining P14′′ and the process Q41x2(z2).x1(z1).x1().x2().z1().z2().0, as follows:

P41(νx1y1)(νx2y2)(νv1k1)(νv2k2)(Q41|P14′′)

Note that a τ-transition along the sessions x1y1 or x2y2 in P41 would depend on a delayed action. Now, we can use a commuting conversion to swap the order of the inputs, effectively anticipating the input on x1: Q41𝑐𝑐x1(z1).x2(z2).x1().x2().z1().z2().0=P14; therefore, P41𝑐𝑐P14. Clearly, there is a transition sequence ρ:P14𝙷𝟎 s.t. 𝖱𝖳(ρ).

The second ingredient is disentanglement, which also induces optimizations on processes:

Figure 8: 𝖧𝖢𝖯: Disentanglement (Definition 42). See [19] for details.
Definition 42 (𝖧𝖢𝖯: Disentanglement [22]).

Disentanglement is described by the smallest relation on (typed) processes closed under the rules in Figure 8. We write for the reflexive and transitive closure of .

Each of the process transformations in Figure 8 is justified by an operation on derivations; this way, e.g., for the second rule we have:

This way, disentanglement proceeds by the repeated application of the rules from Figure 8 to the derivation of P𝙷Γ1Γn, which aims at moving downwards the instances of Rule H-Mix2 (cf. Figure 5). If H-Mix2 gets stuck in either H-Cut or H-, then it becomes an instance of C-Cut or C-, respectively (cf. Figure 4).

Disentanglement increases the parallelism in processes. This way, e.g., for P14 and Q14 (Example 14) we have: P14Q14. Also, note that Rule H-𝟏 types x[].P𝙷Γx:𝟏, induces a discrepancy: at the process level, the rule places the empty output in sequential composition with P, whereas at the level of typing x:𝟏 is placed in its own partition, enforcing independence from all names in 𝖿𝗇(P). Disentanglement solves this discrepancy. Consider, e.g., process P18=(νxx)(x[].x().0): we have P18(νxx)(x[].0|x().0).

Lemma 43 (Disentanglement [23]).

If there exists a derivation d of P𝙷Γ1Γn, then there exist derivations d1,,dn of P1𝙲Γ1,,Pn𝙲Γn in 𝖢𝖯, and


where we use the double line to indicate multiple uses of the same rule.

The following result ensures that process observations are invariant under disentanglement. Moreover, since instances of H-Cut are turned into instances of C-Cut, disentangled processes do not feature occurrences of restriction between sessions in sequential composition.

Lemma 44.

Suppose P𝖧𝖢𝖯. If PP then P𝙷P.

Proof.

We prove that if PP then PP by induction on the length k of . For the base case (k=1) we proceed by a case analysis in the last rule applied in the type derivation of P𝙷𝒢. The fact that P𝙷P follows from Theorem 27.

Given a process P, the rules for disentanglement can be applied in any order; we therefore define a set of disentangled processes:

Definition 45 (𝖧𝖢𝖯: Disentangled Processes).

Given P𝖧𝖢𝖯, the set Dist(P) is defined as follows:

Dist(P){P𝖧𝖢𝖯|PP,P=P1||Pn𝙷Γ1Γn,P1𝙲Γ1,,Pn𝙲Γn}

From Lemma 44 we have that all disentangled processes are observationally equivalent:

Lemma 46.

Let P𝖧𝖢𝖯. If Q,RDist(P), then Q𝙷R.

Proof.

From Lemma 44, P𝙷P for all PDist(P). By Definition 19, 𝙷 is transitive. Hence, for all Q,RDist(P), Q𝙷R. We use disentanglement to prove that if 𝒟𝐇(P) then there is a P s.t. 𝒟𝐇𝖱(P), with P𝙷P.

The following main result establishes that the notions of 𝒟𝐇() (Definition 26) and 𝒟𝐇𝖱() (Definition 36) are equivalent, up to commuting conversions and disentanglement.

Theorem 47.

For all processes P𝖧𝖢𝖯 s.t. 𝒟𝐇(P), then there exist P,Q𝖧𝖢𝖯 s.t.: (1) PDist(P), (2) P𝑐𝑐Q, (3) P𝙷Q, (4) 𝒟𝐇𝖱(Q).

Proof sketch.

Parts (1)-(3) follow from Definitions 45, 40, and 44. For part (4) we show that self-synchronizations and delayed actions are eliminated by means of disentanglement and commuting conversions, respectively. See [19] for details.

Theorem 47 concerns 𝖧𝖢𝖯 processes. To lift this result to 𝖲𝖯, we need some results.

Lemma 48.

Let P. There exists P s.t.: (1) PP. (2) P𝑐𝑐P.

Proof.

The items follow by induction on the length of and 𝑐𝑐, respectively. For (1) in the base cases we proceed by a case analysis in the last rule applied in the type derivation of P𝙷Γ; it shows the structure of P and by Definition 28 we obtain the structure of P. The proof finishes by applying a single step of to the type derivation of P𝙷Γ and replicating it to the derivation of Γ𝚂P. The proof of (2) proceeds similarly.

Lemma 48 ensures that the following definition is sound:

Definition 49 (Lifting Commuting Conversions and Disentanglement to 𝖲𝖯).

Let P,P. We write PP and P𝑐𝑐P, whenever PP and P𝑐𝑐P hold, respectively.

Having disentanglement in 𝖲𝖯, we aim to prove that the resulting disentangled process simulates the original process. To define simulation in 𝖲𝖯, we need the following notion:

Definition 50 (𝖲𝖯: Labelled Reduction Semantics).

Let P𝖲𝖯, then Pτ:xyQ whenever:

(1) P(νxy)(x¯v.P|y(z).Q|R)(νxy)(P|Q{v/z}|R)Q, or (2) P(νxy)(x().P|y¯.Q|R)(νxy)(P|Q|R)Q.

Definition 51 (𝖲𝖯: Simulation).

A binary relation 𝕊 in 𝖲𝖯 is a (typed) simulation if whenever (P,Q)𝕊 then Γ𝚂P, Γ𝚂Q and Pτ:xyP implies Qτ:xyQ for some Q s.t. (P,Q)𝕊. We write PQ whenever (P,Q)𝕊 for a (typed) simulation 𝕊.

In the LTS semantics of 𝖧𝖢𝖯, the processes P and Q from Theorem 47 are bisimilar; however, in a reduction semantics, any transitions of P that use delayed actions or self-synchronization would be considered as deadlocks, and then Q would only simulate P. Formally:

Theorem 52.

The relation 𝕊={(P,R)P,and PR} is a simulation.

Proof sketch.

By induction in the structure of P, with a case analysis in . See [19] for details.

Finally, Corollary 53, given below, brings Theorem 47 to 𝖲𝖯: it shows that even though in 𝖧𝖢𝖯 both 𝒟𝐇() and 𝒟𝐇𝖱() are equivalent, in 𝖲𝖯 those notions are related via a simulation.

Corollary 53.

Given P𝖥, then there exist Q and P𝖱 s.t.: (1) QDist(P), (2) Q𝑐𝑐P, (3) PP, (4) P𝙷P.

Proof.

It follows by Lemmata 48, 47, and 52.

Example 54 (Corollary 53, At Work).

Consider the process P54 and its encoding into 𝖧𝖢𝖯:

P54 (νwz)(w¯.(νxy)(x¯.0|(νku)(k().0|y().z().u¯.0)))
P54 (νwz)(w[].(νxy)(x[].0|(νku)(k().0|y().z().u[].0)))

Note that ¬𝒟𝐒(P54) but P54 has two τ-transitions:

P54 𝜏(νxy)(x[].0|(νku)(k().0|y().u[].0))𝙷𝟎 (1)
P54 𝜏(νwz)(w[].(νku)(k().0|z().u[].0))𝙷𝟎 (2)

where the transition in (1) is due to a delayed action on z and a self-synchronization along the session wz, and the transition in (2) is due to a delayed τ-transition along the session xy. Hence, 𝒟𝐇(P54). Via disentanglement we obtain:

P54(νwz)(w[].0|(νxy)(x[].0|(νku)(k().0|y().z().u[].0)))R

In R, neither a delayed action nor a self-synchronization are needed, thus 𝒟𝐇𝖱(R). We could also give priority to the τ-transition along wz; however, because the input on z is not at the top-level, a synchronization on wz still requires a delayed action. This shows the need for commuting conversions. Indeed, by using 𝑐𝑐 we obtain:

R𝑐𝑐(νwz)(w[].0|(νxy)(x[].0|(νku)(k().0|z().y().u[].0)))R

We have that 𝒟𝐇𝖱(R). Moreover, there is a process P in 𝖲𝖯 s.t. P=R:

P(νwz)(w¯.0|(νxy)(x¯.0|(νku)(k().0|z().y().u¯.0)))

Notice that P54P follows trivially since 𝒟𝐒(P).

4 The Case of Asynchronous Processes

Table 1: Inventory of type systems, classes of processes, and encodings considered in the paper. Shaded cells concern elements used in the case of asynchronous processes (§ 4).

Up to here we have addressed (Q1) by considering the relation between 𝖥 and 𝖱 in 𝖧𝖢𝖯. We now turn our attention to (Q2) and consider the interplay of DF and asynchronous processes as typable by Padovani’s type system for asynchronous processes, here dubbed 𝖯 [27].

We proceed as follows. In § 4.1 we recall Padovani’s type system and introduce , the class of 𝖲𝖯 processes induced by 𝖯, and its sub-class μ, derived from the type system μ𝖯. In § 4.2, we show that μ= (Corollary 74). In § 4.3, we establish a key result: the precise relations between , 𝖥, 𝖱, and (Theorem 76). Also, we revisit Corollary 53 from the standpoint of 𝖯: we prove that the process P𝖱 (obtained via commuting conversions and disentanglement) is also in (Corollary 77). In § 4.4 we present 𝖲𝖯𝔞, an asynchronous version of 𝖲𝖯, and show how to extend our results for 𝖲𝖯 to 𝖲𝖯𝔞 (Corollary 88).

Table 1 summarizes all technical ingredients, including those introduced in this section.

4.1 The Type System 𝗣

We summarize the linear fragment of the type system 𝖯 by Padovani [27], which streamlines Kobayashi’s type system for deadlock freedom [21]. We assume sets of channels a,b, and variables x,y,; then, names u,v, are either channels or variables. We find it convenient to use processes with polyadic communication:

P::=u!x1,,xn|u?(x1,,xn).P|P|Q|(νa)P|𝟎

Two salient features are the output u!x1,,xn, which does not have a continuation, and “(νa)P”, the standard restriction construct of the π-calculus. Notions of free and bound names are as usual: in the process u?(x1,,xn).P, x1,,xn are bound in P; in (νa)P, a is bound in P. We write 𝖿𝗇(P) and 𝖻𝗇(P) for the free and bound names of P, respectively.

The reduction semantics is closed under a structural congruence, denoted 𝙿, which is standardly defined by the following axioms: (i) P|Q𝙿Q|P, (ii) P| 0𝙿P, (iii) P|(Q|R)𝙿(P|Q)|R, (iv) (νx)P|Q𝙿(νx)(P|Q) (if x𝖿𝗇(Q)), and (v) (νx)(νy)𝙿(νy)(νx)P.

Reduction is then defined as

a!v1,,vn|a?(x1,,xn).P𝙿P{v1,,vn/x1,,xn}
Example 55.

Differently from 𝖲𝖯, channels in Padovani’s framework are used exactly once. Structured communications can of course be still expressed, using continuations. Consider the process P55(νx)(Q55|R55) with

Q55 (νa)(νc)(x!a,c|c!a) R55 x?(z1,w).w?(z2).((νr)z1!r|z2?(w).0)

Q55 sends the two endpoints of a channel: the first is sent along x (together with a continuation channel c), and the other is sent along c. Channel a occurs in both outputs, but these occurrences actually denote different endpoints; this difference will be justified by typing (cf. Example 59). R55 receives these endpoints to implement a local exchange of name r along a.

Padovani’s type system ensures the absence of pending communications in a process with respect to a channel. To formalize this notion, we rely on reduction contexts, defined as 𝒞::=[]|(𝒞|P)|(νx)𝒞. We may now define the following auxiliary predicates:

𝗈𝗎𝗍(a,P) P𝙿𝒞[a!e]a𝖻𝗇(C) 𝗂𝗇(a,P) P𝙿𝒞[a?(x).Q]a𝖻𝗇(C)
𝗌𝗒𝗇𝖼(a,P) (𝗂𝗇(a,P)𝗈𝗎𝗍(a,P))

Intuitively, predicate 𝗂𝗇(a,P) holds if a is free in P and there is a subprocess of P that can perform a linear input on a. Predicate 𝗈𝗎𝗍(a,P) holds if a is free in P and a subprocess of P is waiting to send a value v. Predicate 𝗌𝗒𝗇𝖼(a,P) denotes a pending input/output on a for which a synchronization on a is immediately available. This way, to formalize a pending input/output for which a synchronization on a is not immediately possible, we define:

𝗐𝖺𝗂𝗍(a,P)(𝗂𝗇(a,P)𝗈𝗎𝗍(a,P))¬𝗌𝗒𝗇𝖼(a,P)

Thus, ensuring no pending communications in P means ensuring ¬𝗐𝖺𝗂𝗍(a,P) for every a.

Example 56 (Predicates at work).

Consider the process P56a?(x).b!v1|b?(y).a!v2, which has a circular dependency. We have: (1) 𝗈𝗎𝗍(a,P56) and 𝗈𝗎𝗍(b,P56). (2) 𝗂𝗇(a,P56) and 𝗂𝗇(b,P56). (3) ¬𝗌𝗒𝗇𝖼(a,P56) and ¬𝗌𝗒𝗇𝖼(b,P56). (4) 𝗐𝖺𝗂𝗍(a,P56) and 𝗐𝖺𝗂𝗍(b,P56).

Type System.

To ensure absence of pending communications, 𝖯 relies on priorities. Let p,q, denote subsets of {?,!} (polarities). Types for channels are defined as follows:

t::=p[t1,,tm]n

where n is the priority of a channel, which indicates urgency for its use: the lower the number, the higher the urgency. We write # for {?,!}. This way, # and are even polarities.

Example 57 (Priorities).

To illustrate types and priorities, recall again the process P56=a?(x).b!v1|b?(y).a!v2. As we have seen, we have 𝗐𝖺𝗂𝗍(a,P56) and 𝗐𝖺𝗂𝗍(b,P56).

Let us assume that x,y,v1,v2 are all typed with some type t. By inspecting the left thread of P56, we infer that a and b must be typed as ?[t]m and ![t]n, respectively, for some m,n. Then, by inspecting the right thread, we infer that a and b must then be typed with ![t]m and ?[t]n, respectively. This way, their types in the composed process are #[t]m (for a) and #[t]n (for b). Looking again at the left thread, as the input along a is blocking the output along b, we must have m<n; in the right thread we have the exact opposite situation, thus n<m. These unsolvable inequalities reveal the circular dependency between a and b, which will make P56 not typable in the type system 𝖯.

We now summarize how typing excludes pending communications. Type environments Γ,Γ, are finite maps from channels to types. We write dom(Γ) for the domain of Γ. We write Γ,Γ for the union of Γ and Γ when dom(Γ)dom(Γ)=. We write + to denote a partial composition operator on types defined as: p[s1,,sm]n+q[s1,,sm]n=(pq)[s1,,sm]n if pq=, and undefined otherwise. For type environments we have: Γ+ΓΓ,Γ if dom(Γ)dom(Γ)=, and (Γ,u:t)+(Γ,u:s)(Γ+Γ),u:t+s. Let ={}, where n< for every n. The functions , from types to , and $h from types to types are defined as follows:

t{nif t=p[s]nand potherwise$ht{p[s]n+hif t=p[s]nand ptotherwise

Intuitively, the function $h allows us to shift priorities. We say that a type t is unlimited, written 𝗎𝗇(t), iff t=. We write 𝗎𝗇(Γ) iff all the types in the range of Γ are unlimited. We are now ready to give the typing rules, considering only processes with biadic communication, for simplicity. The rules for monadic communication are as expected.

Definition 58 (𝖯).

The typing rules for processes use judgements of the form Γ𝙿P and Γ𝙿e~:t~ and are presented in Figure 9. We shall write P𝖯 if Γ𝙿P, for some Γ.

Rule T-In is used to type inputs u?(x1,x2).P, where u has type ?[t1,t2]n. The condition n<Γ ensures that u has been assigned the highest urgency; accordingly, the types of x and y are shifted by n. Rule T-Out, used to type outputs on channels of type ![t1,t2]n, follows a similar principle: the types of x and y are shifted by n, since they must have lower urgency than u. Rule T-New is used for restricting new channels with full (#) or empty () polarity.

Example 59.

Recall processes Q55 and R55 from Example 55. Consider types s=$1![[]4]2 and s=$2?[[]4]1. Note that s+s=#[[]4]3. Process Q55 is typed as follows:

Similarly we can check that x:?[s,$1?[s]1]1𝙿R55. Note that x is typed with opposite polarities in Q55 and R55; thus by applying Rules T-Par and T-New we obtain 𝙿P55.

Figure 9: 𝖯: Typing rules for asynchronous processes.

We may now characterize deadlock freedom. Let us write 𝙿 to denote the reflexive, transitive closure of 𝙿. Also, write P/𝙿 if there is no Q such that P𝙿Q. We have:

Definition 60 (𝖯: Deadlock Freedom [27]).

We say that P𝖯 is deadlock free, written 𝒟𝐏(P), if for every Q such that P𝙿(νa~)Q/𝙿 we have ¬𝗐𝖺𝗂𝗍(a,Q) for every a.

We have that processes typed in the empty environment are deadlock free:

Theorem 61 (𝖯: Deadlock Freedom [27]).

If 𝙿P, then 𝒟𝐏(P).

4.2 Relating and

We now consider μ𝖯 (“micro 𝖯”), which is a fragment of 𝖯 that is similar to 𝖢𝖯. We also define the encoding {[]}f:𝖲𝖯𝖯, and and μ the classes of 𝖲𝖯 processes that are captured by 𝖯 and μ𝖯, respectively. These are all ingredients for our results in § 4.3.

Definition 62 (μ𝖯).

The typing rules for processes are presented in Figure 10. A judgement Γ𝙿μP denotes that P is well typed in Γ. We shall write Pμ𝖯 if Γ𝙿μP, for some Γ.

Figure 10: μ𝖯: Modified typing rules for asynchronous processes.

μ𝖯 results from 𝖯 by replacing Rules T-Par and T-New in Figure 9 with Rule M-New-Par, which combines restriction and parallel just as Rule C-Cut in Figure 4.

Lemma 63.

If Γ𝙿μP then Γ𝙿P.

Proof sketch.

By induction on the type derivation, with a case analysis in the last rule applied. See [19] for details.

Corollary 64.

If 𝙿μP, then 𝒟𝐏(P).

Proof.

It follows by Lemmata 63 and 61. We now define an encoding from 𝖲𝖯 to 𝖯, following a continuation-passing style (cf. [8]). Let f be a function from names to names. We use the following conventions: fx stands for f(x), and f,{xc} stands for the function f s.t. f(x)=c and f(y)=f(y) if xy.

Definition 65.

The (partial) encoding {[]}f:𝖲𝖯𝖯 is parameterized by a function, ranging over f,g, from names to names, and is defined for processes as follows:

{[x¯v.P]}f (νm)(fx!fv,m|m?(k).(νc)(k!c|{[P]}f,{xc}))
{[x(z).P]}f fx?(z,m).(νa)(m!a|a?(c).{[P]}f,{xc})
{[x¯.0]}f (νr)fx!r
{[x().P]}f fx?(r).{[P]}f(with r𝚏𝚟(P)𝚋𝚟(P))
{[(νxy)P]}f (νd){[P]}f,{x,yd}

and as a homomorphism for P|Q and 𝟎. The encoding of session types is as follows:

{[𝖾𝗇𝖽?]} ?[[]]n {[!S.T]} ?[{[T]},![![{[S]}]i]j]n
{[𝖾𝗇𝖽!]} ![[]]n {[?S.T]} ![{[T]},![![{[S¯]}]i]j]n

Typing environments are encoded inductively as {[]}f and {[Γ,x:T]}f{[Γ]}f,fx:{[T]}. The values of i,j and n are calculated when checking in μ𝖯 the typablity of {[Γ]}f𝙿μ{[P]}f.

Intuitively, the encoding of processes in Definition 65 collapses the two endpoints of a session into a single name in 𝖯. The encoding of x¯v.P mimics both the sequential structure of a session and synchronous communication. {[x¯v.P]}f sends the (renamed) value fv and a new channel m along which an input m?(k). blocks the continuation {[P]}f,{xc}, and receives the channel along which the the continuation c of the session x will be sent. Dually, {[x(z).P]}f receives the intended value and the channel m, which sends the channel a, along which the continuation of the session x will be received. Finally, the encoding is partial because {[x¯.P]}f is only defined when P=𝟎: this allows us to characterize the session processes captured in 𝖢𝖯, where the empty output has no continuation (see Definition 11).

Example 66.

Consider the process P66(νxy)(x¯v.R|y(z).Q) in 𝖲𝖯. We show {[P66]}f and illustrate its reductions. Let us assume P66 is well-typed. Because of linearity of x and y, they only appear in the left and right subprocess, respectively. Let f={x,yd} and g1={xc},g2={yc}, then we have:

{[P66]} =(νd)({[x¯v.R]}f|{[y(z).Q]}f)
=(νd)((νm)(d!v,m|m?(k).(νc)(k!c|{[R]}g1))
|d?(z,m).(νa)(m!a|a?(c).{[Q]}g2))
𝙿(νm)(m?(k).(νc)(k!c|{[R]}g1)|(νa)(m!a|a?(c).{[Q]}g2{v/z}))
𝙿(νa)((νc)(a!c|{[R]}g1)|a?(c).{[Q]}g2{v/z})
𝙿(νc)({[R]}g1|{[Q]}g2{v/z,c/c})

Our main result concerns the classes of processes associated to 𝖯 and μ𝖯, which we define by mirroring the definition of and (Definition 34):

Definition 67 ( and μ).

The classes of processes and μ are defined as follows:

{P𝖲𝖯|Γ𝚂P{[Γ]}f𝙿{[P]}f}μ{P𝖲𝖯|Γ𝚂P{[Γ]}f𝙿μ{[P]}f}

The following result establishes an operational correspondence between a process and its encoding, what will allows us to capture deadlock free session processes via the encoding.

Theorem 68 (Operational Correspondence for {[]}f).

Let Pμ. We have:

  1. 1.
    1. (a)

      If P(νxy~)(x¯.Q1|y().Q2|S), then Q𝖯 such that {[P]}f𝙿Q and Q𝙿{[(νxy~)(Q1|Q2|S)]}f.

    2. (b)

      If P(νxy~)(x¯v.Q1|y(z).Q2|S), then Q𝖯 such that {[P]}f𝙿3Q and Q𝙿{[(νxy~)(Q1|Q2{v/z}|S)]}f.

  2. 2.

    If {[P]}f𝙿R, then either:

    1. (a)

      P𝖲𝖯 such that PP and R𝙿{[P]}f, or

    2. (b)

      Q𝖯, and P𝖲𝖯 such that R𝙿2Q, PP and Q𝙿{[P]}f.

Proof.

By assumption, Pμ and so we have that Γ𝚂P, for some Γ, and {[Γ]}f𝙿μ{[P]}f is defined. Moreover, by Corollary 8 P is well-formed. We consider each item separately. Item 1(b) follows by Definition 65 and the rest of the analysis proceeds as in Example 66; Item 1(a) is similar. Item (2): If {[P]}f𝙿R, then {[P]}f𝙿(νa~)(d!v~|d?(x~).K|S). By typability of P and Definition 65 one of the two possibilities apply:

  1. i

    P(νxy~)(x¯.0|y().K|S), {[S]}f=S, {[K]}f=K and f=f,{x,yd},

  2. ii

    P(νxy~)(x¯v.S1|y(z).K|S2) and f=f,{x,yd}

In case (i) {[P]}f𝙿(νa~)((νr)d!r|d?(r).K|S)𝙿(νa~)(K|S) and P(νxy~)(x¯.0|y().K|S)(νxy~)(K|S′′), which verifies case (2a). In case (ii) we proceed as in Example 66, which verifies case (2b).

As a consequence of Theorem 68 we have the following result, which shows the relation between deadlock-free processes in μ.

Corollary 69.

Let Pμ. 𝒟𝐒(P) iff 𝒟𝐏({[P]}f).

Proof.

For each direction we prove its contrapositive. We discuss only the right-to-left direction; the analysis for the left-to-right direction is similar. By Definition 60, there exist R and a s.t. {[P]}f𝙿(νa~)R/𝙿 and 𝗐𝖺𝗂𝗍(a,R). If 𝗐𝖺𝗂𝗍(a,R) holds because 𝗂𝗇(a,R) then R𝙿(νa~)(a?(x).Q|S). By Theorems 68 and 65 there exists P(νxy~)(z(w).Q|S) s.t. PP and R𝙿{[P]}f. Note that P/, since otherwise by Theorem 68(1), (νa~)R𝙿R′′ for some process R′′, contradicting our assumption, thus ¬𝒟𝐒(P). The case when 𝗐𝖺𝗂𝗍(a,R) holds because 𝗈𝗎𝗍(a,R) proceeds similarly.

Corollary 69 allows us to detect DF session processes via the encoding.

4.3 Comparing and

From § 3 we infer that a process P, typed as P𝙷Γ1Γn, can be decomposed into processes P1𝙲Γ1, , Pn𝙲Γn. Moreover, by Lemma 48 (disentanglement in 𝖲𝖯) we infer that processes P1,,Pn have a pre-image in 𝖲𝖯, therefore i[1,n].Pi.

As an important preliminary step, we first prove that =μ (Corollary 74). We split the proof in two separate inclusions. The following lemma is useful to prove that μ.

Lemma 70.

Let Γ and P be an environment and a process in 𝖯, resp. The following hold:

  1. 1.

    If Γ𝙿P, then $nΓ𝙿P.

  2. 2.

    If Γ𝙿μP, then $nΓ𝙿μP.

  3. 3.

    Let P𝖯. If Γ𝙿μP and 𝗎𝗇(T), then Γ,x:T𝙿μP, with x fresh wrt P.

  4. 4.

    Let Γ1,,Γn be typing environments in 𝖲𝖯, then {[Γ1,,Γn]}f={[Γ1]}f++{[Γn]}f, for some renaming function f.

  5. 5.

    Let T be a session type. Then {[T]}f+$m{[T¯]}f=p[T]n, for some m0, n, T a type in 𝖯, and p even.

Proof.

(1) Proven in [27]. (2) Follows from Lemma 63 and item 1. (3) Follows by induction on the type derivation. (Figure 10). (4)  Follows immediately by linearity of names in Γi, for i[1,n]. (5) Follows by induction on the structure of T.

Theorem 71.

μ.

Proof sketch.

By induction on the type derivation Γ𝚂P with a case analysis in the last rule applied. See [19] for details.

To prove the other direction we need the following result.

Lemma 72.

Let S and T be session types. We have: (1) {[S]}f+{[T]}f is defined iff T=S¯. (2) S¯=(S).

Proof.

Item (1) follows by Definition 65 and def. of +. Item (2) follows immediately by induction in the structure of S and Definition 28.

Theorem 73.

μ.

Proof sketch.

By induction on the type derivation Γ𝚂P with a case analysis in the last rule applied. See [19] for details.

Corollary 74.

=μ.

Proof.

It follows by Theorems 71 and 73.

Main Results.

We may now return to considering . Note that : to see this, consider, e.g., the self-synchronizing process P1𝖥 from Example 18. Using Corollary 74 and disentanglement (Definition 42) we show that given a process P𝖥, we can find a deadlock-free process P. Formally, we have:

Theorem 75.

Given P𝖥, P𝖱 s.t. P, P𝙷P, and 𝒟𝐏({[P]}f).

Proof.

By Corollary 53, P𝑐𝑐P=P1||Pn, and by Lemma 48 i[1,n], there exists Pi s.t. Pi=Pi. From Corollaries 74 and 63 we infer {[Pi]}f, i[1,n]. Moreover, by repeatedly applying Rule T-Par we have that P. Finally, 𝒟𝐏({[P]}f) follows from Theorems 39 and 69.

The following result relates , its subclasses 𝖥 and 𝖱, and .

Theorem 76.

The following hold: (1) . (2) 𝖥. (3) 𝖱.

Proof sketch.

We give witnesses for each statement; see [19] for details.

Finally, from Theorem 75 we have the following result, which complements Corollary 53: given P𝖥, there exists a bisimilar process P𝖱 via disentanglement. Note that this result applies in particular to processes in 𝖥.

Corollary 77.

Given P𝖥, there exists P𝖱 s.t. (1) PP, (2) P𝙷P, and (2) 𝒟𝐏({[P]}f).

4.4 Asynchronous Session Processes

Figure 11: 𝖲𝖯𝔞: Typing Rules for Processes.

Up to here, we have considered asynchronous communication somewhat indirectly: we have examined the type system for asynchronous processes 𝖯, defined its associated classes and μ, and related them to and 𝖥. To treat asynchronous communication directly, here we consider 𝖲𝖯𝔞, an asynchronous variant of 𝖲𝖯, and discuss how to transfer our results from §§ 3 and 4.3 from 𝖲𝖯 to 𝖲𝖯𝔞 by leveraging an encoding :𝖲𝖯𝔞𝖲𝖯.

𝗦𝗣𝖆: Asynchronous 𝗦𝗣.

We define 𝖲𝖯𝔞 as a variant of 𝖲𝖯 with asynchronous communication. Considerations about variables, endpoints, and values are as for 𝖲𝖯 (cf. § 2.1). The syntax of processes is largely as before; only constructs for output and input are modified:

P ::= 0|x().P|x¯|x¯v,c|x(y,w).P|P1|P2|(νxy)P

Process x¯v,c sends names v and c along x: the former is a message and the latter is a continuation. Because it has no continuation, this process may be seen as an “output particle” that carries a message. Accordingly, process x(y,w).P receives two values v and c along x and continues as P{v/y,c/w}, i.e., the process resulting from the capture-avoiding substitution of y by v, and w by c in P. The construct for empty output is also modified. In both z(x,y).P and (νxy)P x,y are bound in P.

Definition 78 (𝖲𝖯𝔞).

The typing rules for processes are presented in Figure 11. A judgement Γ𝚂𝔞P denotes that P is well typed in Γ. We shall write P𝖲𝖯𝔞 if Γ𝚂𝔞P, for some Γ.

Most typing rules are self-explanatory. Rule A-Eoutput types an empty output without continuation. Rule A-Out types the output particle x¯v,c where x:!T.S. Since the output has no continuation, the session name c typed as S serves a a continuation name for x. Dually, Rule A-In types x as ?T.S provided that y and w are typed as T and S in P, respectively, thus, w serves as a continuation for x in P.

The reduction semantics for 𝖲𝖯𝔞 is defined as follows:

(νxy)(x¯v,c|y(z,w).Q|S) (Q{v/z,c/w}|S) A-Com
(νxy)(x¯|y().Q|S) Q|S A-EmptyCom

Structural rules and the congruence are defined as in Figure 2. A labeled reduction semantics Pτ:xyQ for 𝖲𝖯𝔞 follows easily from Definition 50.

Example 79.

Consider the process P10 from Example 10, which is typable and deadlocked in 𝖲𝖯. The following process can be seen as the analogue of P10 but in the asynchronous setting of 𝖲𝖯𝔞. We define P79 as (νx1y1)(νx2y2)(νv1k1)(νv2k2)P, where

P x1(z1,w1).x2(z2,w2).w1().w2().z1().z2().0
|(νc2c2)(y2¯v2,c2|c2¯)|(νc1c1)(y1¯v1,c1|c1¯)|k1¯|k2¯

Note how c1 and c2 serve as a continuation for y1 and y2, respectively. There exist processes Q1,Q2 such that P79τ:x1y1Q1τ:x2y2Q2 0.

We define DF for 𝖲𝖯𝔞 by adapting Definition 9:

Definition 80 (𝖲𝖯𝔞: Deadlock Freedom).

A process P𝖲𝖯𝔞 is deadlock free, written 𝒟𝐀(P), if the following holds: whenever PP and one of the following holds: (1) P(νxy~)(xi¯v,c|Q2), (2) P(νxy~)(xi(y).Q1|Q2), (3) P(νxy~)(xi().Q1|Q2), or (4) P(νxy~)(xi¯|Q2) (with xix~ in all cases) then there exists R such that PR.

Example 81 (Comparing DF in 𝖲𝖯 and 𝖲𝖯𝔞).

As just illustrated by means of processes P10 (from Example 10) and P79, moving to an asynchronous setting may solve certain deadlocks: we have ¬𝒟𝐒(P10) and 𝒟𝐀(P79).

On the other hand, moving to an asynchronous setting alone does not resolve the problem. Consider the process Q81(νx2y2)(y2().0|(νx1y1)(y1().(x2¯|x1¯))). Clearly, Q81 is typable in 𝖲𝖯𝔞. Also, let Q81 be the 𝖲𝖯 variant of Q81 with 𝟎 as continuation for outputs, i.e., Q81(νx2y2)(y2().0|(νx1y1)(y1().(x2¯.0|x1¯.0))). We have that Q81 is typable in 𝖲𝖯 and that ¬𝒟𝐒(Q81) and ¬𝒟𝐀(Q81).

Our goal is to transfer our technical results for 𝖲𝖯 to the asynchronous setting of 𝖲𝖯𝔞. To this end, we define the following encoding:

Definition 82.

We define the encoding from 𝖲𝖯𝔞 to 𝖲𝖯 as follows:

x¯v,c x¯v.x¯c.x¯.0 𝖾𝗇𝖽? 𝖾𝗇𝖽?
x(y,w).P x(y).x(w).x().P 𝖾𝗇𝖽! 𝖾𝗇𝖽!
x().P x().P !T.S !T.!S.𝖾𝗇𝖽!
x¯ x¯.0 ?T.S ?T.?S.𝖾𝗇𝖽?

and as an homomorphism for 𝟎, P|Q, and (νxy)P.

Example 83 (, At Work).

Consider again the process P79. We have seen that 𝒟𝐀(P79). We now check that does not add deadlocks by verifying that 𝒟𝐒(P79):

P79 (νx1y1)(νx2y2)(νv1k1)(νv2k2)P
P x1(z1).x1(w1).x1().x2(z2).x2(w2).x2().w1().w2().z1().z2().0
|(νc2c2)(y2¯v2.y2¯c2.y2¯.0|c2¯.0)
|(νc1c1)(y1¯v1.y1¯c1.y1¯.0|c1¯.0)|k1¯.0|k2¯.0

One can show that there exist Q1,Q2 such that P79τ:x1y13Q1τ:x2y23Q2𝟎.

By a similar analysis to the one for Theorem 68, we have the following result:

Theorem 84 (: Operational Correspondence).

Let P𝖲𝖯𝔞. The following holds:

  1. 1.

    if P(νxy)(x(w,z).P|y¯v1,v2|R), then Q𝖲𝖯 s.t. P3Q and Q=P{v1/w,v2/z}|R.

  2. 2.

    If P(νxy)(x().P|y¯.0|R), then Q𝖲𝖯 s.t. PQ and Q=P|R.

  3. 3.

    If PQ, then either: (i) there exists Q𝖲𝖯 s.t. Q2Q, PP and P=Q, or (ii) PP and P=Q.

Using Theorems 84, 9, and 80 we formalize our claim from Example 83: does not add deadlocks.

Theorem 85 (Correspondence DF).

For all P𝖲𝖯𝔞, 𝒟𝐀(P) iff 𝒟𝐒(P).

Proof sketch.

For each direction we prove its contrapositive and proceed by contradiction. See [19] for details.

Using the encoding , and inspired by Theorems 84 and 85, we can define the following classes of asynchronous processes by relying on their synchronous counterparts:

Definition 86.

The classes of asynchronous processes are defined as follows:

𝔞 {P𝖲𝖯𝔞|P} 𝔞 {P𝖲𝖯𝔞|P} μ𝔞 {P𝖲𝖯𝔞|Pμ}
𝔞 {P𝖲𝖯𝔞|P} 𝖥𝔞 {P𝖲𝖯𝔞|P𝖥} 𝖱𝔞 {P𝖲𝖯𝔞|P𝖱}

Each asynchronous class is contained (up to ) in its corresponding synchronous class:

Lemma 87.

Let P𝖲𝖯𝔞. The following hold: (1) If P𝔞, then P. (2) If P𝔞, then P. (3) If P𝔞, then P. (4) If Pμ𝔞, then Pμ. (5) If P𝖥𝔞, then P𝖥. (6) If P𝖱𝔞, then P𝖱.

Proof.

It follows straightforwardly from Definition 86. Thus, we can transfer our main results (Corollaries 53, 77, and 74) to 𝖲𝖯𝔞 via . For instance, Corollary 53 is transferred to 𝖲𝖯𝔞 as follows, using Lemma 87, and Theorem 84:

Corollary 88.

Given P𝖥𝔞, there exist Q and P𝖱𝔞 s.t.: (1) QDist(P), (2) Q𝑐𝑐P, (3) PP, (4) P𝙷P.

5 Closing Remarks

Figure 12: Overview of main results (detailed version). The inclusions between the classes of processes follow from Theorem 76. The red arrow stands for the relation 𝑐𝑐 (disentanglement and commuting conversions) from Corollary 53, where P1,,Pn. This arrow, together with {[P]}f, represent Corollary 77. The green lines represent Corollary 74 (=μ).

Enforcing DF is a relevant issue for message-passing programs, and type systems for concurrent processes offer a convenient setting to develop analysis techniques that detect insidious circular dependencies in programs. Because there exist different type systems that enforce DF, it is natural to wonder how they compare.

We have studied this question in the general and expressive setting of the π-calculus. Our approach aims at establishing the key strengths and limitations of three representative type systems: 𝖲𝖯, the reference language for session-typed processes; 𝖧𝖢𝖯, the session-typed language based on “propositions-as-sessions” and hypersequents; and 𝖯, the priority-based type system for asynchronous processes. Figure 12 gives an overview of our main technical results, refining Figure 1. We briefly discuss their broader significance. Our work can be seen as covering three dimensions of comparison: type systems (𝖲𝖯, 𝖧𝖢𝖯, 𝖯), process semantics (reduction semantics and LTS), and several definitions of DF (cf. Definitions 9, 26, 36, 60, and 80). Clearly, each type system connects these dimensions in its own way via meta-theoretical results (e.g., type preservation). From this perspective, considering a type system such as 𝖧𝖢𝖯, which comes with an LTS for typed processes with very distinctive features (delayed actions and self-synchronizations), brings significant value to our results. In contrast, the work of Dardha and Pérez [9] (the most closely related work) considers different type systems for synchronous processes but only under a reduction semantics, which influences the definition(s) of DF to be considered.

Our key discovery is identifying the role that commuting conversions and disentanglement have in the class of deadlock-free processes induced by 𝖧𝖢𝖯 (Corollary 53). Although studying the practical ramifications of our results goes beyond the scope of this paper, two observations are relevant. First, our results pave the way for developing extensions of the static analyzer TyPiCal [20] that support the mechanized analysis of (session) processes with asynchronous communication. Second, commuting conversions are already important in practical developments, such as execution strategies in abstract machines for session-typed programs [4] and definitions of session subtyping [6, 15] that enable flexible programming interfaces. An in-depth exploration of these latent connections between our results and tools for the analysis of message-passing programs is left for future work.

It is worth stressing that 𝖧𝖢𝖯’s LTS enjoys strong logical and denotational justifications; by identifying disentanglement and commuting conversions as key notions for DF, we provide new insights into 𝖧𝖢𝖯 and its LTS. This way, our work sheds new light into the foundations of 𝖧𝖢𝖯, its positioning within the line of work on “propositions-as-sessions”, and its expressive power. For instance, it is surprising that processes that share more than one session are typable in 𝖧𝖢𝖯, in the sense of Example 14. While Kokke et al. [23, 22] have studied disentanglement as a tool to relate 𝖧𝖢𝖯 and 𝖢𝖯, here we uncover its connection with DF. Also, their work on 𝖧𝖢𝖯 (𝖧𝖢𝖯 with a reduction semantics but without delayed actions and self-synchronizations) is complementary to our findings. In this sense, our work also offers good motivations for the use of LTSs with regular transitions as the semantics for logic-based session processes (which usually rely on reduction semantics).

It is remarkable that 𝖧𝖢𝖯 and 𝖯 are not just two type systems relevant for a formal comparison, but that they are actually connected thanks to asynchrony (an important aspect not covered in Dardha and Pérez’s work); the connection is made precise by Theorem 76 and Corollary 77. Here again delayed actions in 𝖧𝖢𝖯 result to be insightful for an enhanced understanding of logic-based session types. In this line, we observe that De Young et al. [10] study asynchrony under “propositions-as-sessions”, and in particular explain the role of commuting conversions, which in an asynchronous setting act as as structural congruences (cf. Definition 40). In the synchronous case, they correspond to behavioral equivalences [30].

An interesting point concerns the exact relation between our class (Definition 34) and the class 𝕃 in Dardha and Pérez’s work. There is a key difference between the two: while they consider 𝖢𝖯 with a typing rule for independent parallel composition (cf. Rule H-Mix2 in Figure 5), we only have Rule C-Mix0 in Figure 4. The reason is technical: it is known that having both Mix0 and Mix2 induces the conflation of the units 𝟏 and , which conflicts with the distinction made by 𝖧𝖢𝖯’s denotational semantics (see [19] for details). (In [9], the conflated type is denoted “”, and there are no process constructs for session closing.) For the sake of consistency with the denotational semantics, we opted to not include this rule. Therefore, there are processes that are not in our class but are in Dardha and Pérez’s 𝕃.

Having discovered the relation between DF and commuting conversions and disentanglement, an interesting item for future work is revisiting the process transformations proposed by Dardha and Pérez [9] using disentanglement. To focus on the fundamental issues of DF enforcement, we have not covered processes with recursion/sharing; we also plan to consider typed languages with constructs for shared servers and clients.

References

  • [1] Stephanie Balzer, Bernardo Toninho, and Frank Pfenning. Manifest deadlock-freedom for shared session types. In Luís Caires, editor, Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11423 of Lecture Notes in Computer Science, pages 611–639. Springer, 2019. doi:10.1007/978-3-030-17184-1_22.
  • [2] Gérard Boudol. Asynchrony and the π-calculus (note). Technical report, Rapport de Recherche 1702, INRIA, Sophia-Antipolis, 1992.
  • [3] Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In Paul Gastin and François Laroussinie, editors, CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings, volume 6269 of Lecture Notes in Computer Science, pages 222–236. Springer, 2010. doi:10.1007/978-3-642-15375-4_16.
  • [4] Luís Caires and Bernardo Toninho. The session abstract machine. In Stephanie Weirich, editor, Programming Languages and Systems - 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, volume 14576 of Lecture Notes in Computer Science, pages 206–235. Springer, 2024. doi:10.1007/978-3-031-57262-3_9.
  • [5] Marco Carbone and Søren Debois. A graphical approach to progress for structured communication in web services. In Simon Bliudze, Roberto Bruni, Davide Grohmann, and Alexandra Silva, editors, Proceedings Third Interaction and Concurrency Experience: Guaranteed Interaction, ICE 2010, Amsterdam, The Netherlands, 10th of June 2010, volume 38 of EPTCS, pages 13–27, 2010. doi:10.4204/EPTCS.38.4.
  • [6] Tzu-Chun Chen, Mariangiola Dezani-Ciancaglini, and Nobuko Yoshida. On the preciseness of subtyping in session types. In Olaf Chitil, Andy King, and Olivier Danvy, editors, Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, Kent, Canterbury, United Kingdom, September 8-10, 2014, pages 135–146. ACM, 2014. doi:10.1145/2643135.2643138.
  • [7] Ornela Dardha and Simon J. Gay. A new linear logic for deadlock-free session-typed processes. In Christel Baier and Ugo Dal Lago, editors, Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, volume 10803 of Lecture Notes in Computer Science, pages 91–109. Springer, 2018. doi:10.1007/978-3-319-89366-2_5.
  • [8] Ornela Dardha, Elena Giachino, and Davide Sangiorgi. Session types revisited. In Proc. of PPDP’12, pages 139–150. ACM, 2012. doi:10.1145/2370776.2370794.
  • [9] Ornela Dardha and Jorge A. Pérez. Comparing type systems for deadlock freedom. Journal of Logical and Algebraic Methods in Programming, 124:100717, 2022. (Preliminary version in the Proceedings of EXPRESS/SOS 2015). doi:10.1016/j.jlamp.2021.100717.
  • [10] Henry DeYoung, Luís Caires, Frank Pfenning, and Bernardo Toninho. Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication. In Patrick Cégielski and Arnaud Durand, editors, CSL, volume 16 of LIPIcs, pages 228–242. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2012. doi:10.4230/LIPICS.CSL.2012.228.
  • [11] Mariangiola Dezani-Ciancaglini, Ugo de’Liguoro, and Nobuko Yoshida. On progress for structured communications. In Gilles Barthe and Cédric Fournet, editors, Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers, volume 4912 of Lecture Notes in Computer Science, pages 257–275. Springer, 2007. doi:10.1007/978-3-540-78663-4_18.
  • [12] Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, and J. Garrett Morris. Separating sessions smoothly. In Serge Haddad and Daniele Varacca, editors, 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, volume 203 of LIPIcs, pages 36:1–36:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPICS.CONCUR.2021.36.
  • [13] Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, and J. Garrett Morris. Separating sessions smoothly. Logical Methods in Computer Science, Volume 19, Issue 3, July 2023. doi:10.46298/lmcs-19(3:3)2023.
  • [14] Simon J. Gay and Vasco Thudichum Vasconcelos. Linear type theory for asynchronous session types. J. Funct. Program., 20(1):19–50, 2010. doi:10.1017/S0956796809990268.
  • [15] Silvia Ghilezan, Jovanka Pantović, Ivan Prokić, Alceste Scalas, and Nobuko Yoshida. Precise subtyping for asynchronous multiparty sessions. Proc. ACM Program. Lang., 5(POPL), January 2021. doi:10.1145/3434297.
  • [16] Kohei Honda and Mario Tokoro. On asynchronous communication semantics. In Object-Based Concurrent Computing, number 612, in LNCS, 1992.
  • [17] Keigo Imai, Rumyana Neykova, Nobuko Yoshida, and Shoji Yuen. Multiparty Session Programming With Global Protocol Combinators. In Robert Hirschfeld and Tobias Pape, editors, 34th European Conference on Object-Oriented Programming (ECOOP 2020), volume 166 of Leibniz International Proceedings in Informatics (LIPIcs), pages 9:1–9:30, Dagstuhl, Germany, 2020. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.ECOOP.2020.9.
  • [18] Jules Jacobs and Stephanie Balzer. Higher-order leak and deadlock free locks. Proc. ACM Program. Lang., 7(POPL):1027–1057, 2023. doi:10.1145/3571229.
  • [19] Juan C. Jaramillo and Jorge A. Pérez. Contrasting deadlock-free session processes (extended version), 2025. arXiv:2504.15845.
  • [20] Naoki Kobayashi. TyPiCal: Type-based Static Analyzer for the Pi-Calculus. https://www-kb.is.s.u-tokyo.ac.jp/˜koba/typical/. Accessed: 2025-03-13.
  • [21] Naoki Kobayashi. A new type system for deadlock-free processes. In CONCUR’06, volume 4137 of LNCS, pages 233–247, 2006. doi:10.1007/11817949_16.
  • [22] Wen Kokke, Fabrizio Montesi, and Marco Peressotti. Taking linear logic apart. In Thomas Ehrhard, Maribel Fernández, Valeria de Paiva, and Lorenzo Tortora de Falco, editors, Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity-TLLA@FLoC 2018, Oxford, UK, 7-8 July 2018, volume 292 of EPTCS, pages 90–103, 2018. doi:10.4204/EPTCS.292.5.
  • [23] Wen Kokke, Fabrizio Montesi, and Marco Peressotti. Better late than never: A fully-abstract semantics for classical processes. Proceedings of the ACM on Programming Languages, 3(POPL), 2019. doi:10.1145/3290337.
  • [24] Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types. In Karim Ali and Jan Vitek, editors, 36th European Conference on Object-Oriented Programming (ECOOP 2022), volume 222 of Leibniz International Proceedings in Informatics (LIPIcs), pages 4:1–4:29, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.ECOOP.2022.4.
  • [25] Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. Fencing off go: liveness and safety for channel-based programming. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 748–761. ACM, 2017. doi:10.1145/3009837.3009847.
  • [26] Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. A static verification framework for message passing in go using behavioural types. In Michel Chaudron, Ivica Crnkovic, Marsha Chechik, and Mark Harman, editors, Proceedings of the 40th International Conference on Software Engineering, ICSE 2018, Gothenburg, Sweden, May 27 - June 03, 2018, pages 1137–1148. ACM, 2018. doi:10.1145/3180155.3180157.
  • [27] Luca Padovani. Deadlock and lock freedom in the linear π-calculus. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, New York, NY, USA, 2014. Association for Computing Machinery. doi:10.1145/2603088.2603116.
  • [28] Luca Padovani. A simple library implementation of binary sessions. J. Funct. Program., 27:e4, 2017. doi:10.1017/S0956796816000289.
  • [29] Luca Padovani and Luca Novara. Types for deadlock-free higher-order programs. In Susanne Graf and Mahesh Viswanathan, editors, Formal Techniques for Distributed Objects, Components, and Systems - 35th IFIP WG 6.1 International Conference, FORTE 2015, Held as Part of the 10th International Federated Conference on Distributed Computing Techniques, DisCoTec 2015, Grenoble, France, June 2-4, 2015, Proceedings, volume 9039 of Lecture Notes in Computer Science, pages 3–18. Springer, 2015. doi:10.1007/978-3-319-19195-9_1.
  • [30] Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logical relations and observational equivalences for session-based concurrency. Information and Computation, 239:254–302, 2014. doi:10.1016/j.ic.2014.08.001.
  • [31] Zesen Qian, G. A. Kavvos, and Lars Birkedal. Client-server sessions in linear logic. Proc. ACM Program. Lang., 5(ICFP), August 2021. doi:10.1145/3473567.
  • [32] Davide Sangiorgi and David Walker. PI-Calculus: A Theory of Mobile Processes. Cambridge University Press, USA, 2001.
  • [33] Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming. In Peter Müller, editor, 31st European Conference on Object-Oriented Programming (ECOOP 2017), volume 74 of Leibniz International Proceedings in Informatics (LIPIcs), pages 24:1–24:31, Dagstuhl, Germany, 2017. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.ECOOP.2017.24.
  • [34] Bernardo Toninho and Nobuko Yoshida. Interconnectability of session-based logical processes. ACM Trans. Program. Lang. Syst., 40(4):17:1–17:42, 2018. doi:10.1145/3242173.
  • [35] Bas van den Heuvel and Jorge A. Pérez. A gentle overview of asynchronous session-based concurrency: Deadlock freedom by typing. In Clément Aubert, Cinzia Di Giusto, Simon Fowler, and Violet Ka I Pun, editors, Proceedings 17th Interaction and Concurrency Experience, ICE 2024, Groningen, The Netherlands, 21st June 2024, volume 414 of EPTCS, pages 1–20, 2024. doi:10.4204/EPTCS.414.1.
  • [36] Vasco T. Vasconcelos. Fundamentals of session types. Inf. Comput., 217:52–70, 2012. doi:10.1016/j.ic.2012.05.002.
  • [37] Philip Wadler. Propositions as sessions. J. Funct. Program., 24(2-3):384–418, 2014. doi:10.1017/S095679681400001X.