# Asynchronous Sessions with Input Races

Ilaria Castellani111This research has been supported by the ANR17-CE25-0014-01
CISC project. INRIA, Université Côte d’Azur, France<EMAIL_ADDRESS>Dipartimento di Informatica, Università di Torino, ItalyDiSSTE, Università del
Piemonte Orientale, Italy Mariangiola Dezani-Ciancaglini Dipartimento di
Informatica, Università di Torino, Italy<EMAIL_ADDRESS>DiSSTE, Università
del Piemonte Orientale, Italy Paola Giannini222This original research has the
financial support of the Università del Piemonte Orientale. DiSSTE, Università
del Piemonte Orientale, Italy<EMAIL_ADDRESS>
###### Abstract

We propose a calculus for asynchronous multiparty sessions where input choices
with different senders are allowed in processes. We present a type system that
accepts such input races provided they do not hinder lock-freedom.

##  1 Introduction

The foundational work on multiparty sessions [12] introduced the notion of
_global type_ for specifying the overall behaviour of multiparty protocols.
The criterion for a session implementation to be correct with respect to its
specification was formalised via the notion of projection: each process
implementing the behaviour of a session participant was required to type-check
against the local type obtained by projecting the global type on that
participant.

However, the work [12] imposed strong restrictions on the syntax of global
types, requiring all initial communications in the branches of a choice to
have the same sender and the same receiver, and every third participant333We
call “third participant” any participant which is not involved in the first
communication of a branch. to have the same behaviour in all branches.
Although these were useful simplifying assumptions in order to achieve
multiparty session correctness, they limited the expressiveness of global
types, ruling out relevant protocols. For this reason, more permissive choice
constructors were investigated in subsequent work [2, 3, 10, 17, 14, 4, 6, 15,
11, 18]. A widely adopted relaxation of the choice operator, originally
proposed in [2], allows third participants to behave differently in different
branches, provided they are notified of which branch has been chosen. Later
proposals [10, 17, 14] accommodate processes with output choices among
different receivers, for instance a client choosing among different servers.
On the other hand _input races_ , namely input choices among different
senders, continued to be considered as problematic. As a consequence, common
protocols such as a server shared by different clients could not be specified
by means of global types.

Recent proposals introduce more flexibility in input choices for processes [4,
6, 15, 11, 18]. The work [11] defines the property of _race-freedom_ for
sessions as the absence, at any stage of computation, of a branching between
communications from different senders towards the same receiver leading to
distinct target states. A rather permissive type system is proposed, which is
shown to be both sound and complete for a range of liveness properties when
restricting attention to race-free sessions. The work [15] also addresses the
input race problem, referred to as the “+-problem” there. While the proposed
syntax for global and local types is completely free, two well-formedness
conditions are imposed on types, which are meant to prevent dangerous races.
Sessions are synchronous in [11, 15] and asynchronous in [18], which is the
work that is closest to ours. In that paper, input races are allowed under
sophisticated conditions on projections of global types. These conditions
track causalities between messages, and their soundness proof uses novel
graph-theoretic techniques from the theory of message-sequence charts.

Consider for example the following session, where two participants ${\sf p}$
and ${\sf q}$ send concurrently a message to a third participant ${\sf r}$,
which is ready to receive both messages in any order:

######  Example 1.1 (Confluent input race)

${\sf p}[\\![\,{\sf r}!\ell\,]\\!]\mathrel{\|}{\sf q}[\\![\,{\sf
r}!{\ell^{\prime}}\,]\\!]\mathrel{\|}{\sf r}[\\![\,{\sf p}?\ell;{\sf
q}?\ell^{\prime}+{\sf q}?\ell^{\prime};{\sf p}?\ell\,]\\!]$

No matter whether communication is synchronous or asynchronous, this session
incurs a race444 Either initially, if communication is synchronous, or after
performing both outputs, if communication is asynchronous.. However, this race
may be viewed as innocuous since after any branch is chosen, the input of the
other branch is still available, leading to the same target state. Indeed, the
race consists here of a choice between two different sequentialisations of
concurrent inputs555If we had a parallel construct $|$ for processes, this
situation would be represented as $({\sf p}?\ell\,|\,{\sf q}?\ell^{\prime})$..
This kind of input race will be called _confluent_. The above session is well
typed in [15], but not in [11, 18], where the syntax of global types forbids
different senders in a choice. In [11], this session is also ruled out by the
race-freedom condition.

By contrast, the following asynchronous session, where there is an apparent
input race in the process of participant ${\sf r}$, is actually race-free
according to [11] because it cannot evolve to a state in which both inputs of
${\sf r}$ are simultaneously enabled. This kind of uneffective input race,
which results from an agreement between the senders such that in every
computation only one of them sends a message to the receiver, will be called
_fake_.

######  Example 1.2 (Fake input race in asynchronous session)

${\sf p}[\\![\,{\sf q}!a;{\sf q}?a;({\sf q}!\ell;{\sf r}!b\oplus{\sf
q}!\ell^{\prime})\,]\\!]\mathrel{\|}{\sf q}[\\![\,{\sf p}!a;{\sf p}?a;({\sf
p}?\ell+{\sf p}?\ell^{\prime};{\sf r}!b)\,]\\!]\mathrel{\|}{\sf r}[\\![\,{\sf
p}?b+{\sf q}?b\,]\\!]$

This session implements the following protocol between Alice, Bob and Carol,
represented by participants ${\sf p}$, ${\sf q}$ and ${\sf r}$ respectively:
$\bullet$ Alice and Bob send each other the message “I arrived” and then they
read their messages;
$\bullet$ Alice sends Bob either the message “I will tell Carol”, after which
she sends Carol the message “We arrived”, or the message “Please tell Carol”;
$\bullet$ Bob reads either the message “I will tell Carol”, or the message
“Please tell Carol” after which he sends Carol the message “We arrived”;
$\bullet$ Carol reads the message “We arrived” with sender either Alice or
Bob.

The session of Example 1.2 cannot be typed in [15, 11, 18] because the syntax
of global types does not allow two participants to exchange messages by first
performing both outputs and then both inputs. If we omit the initial exchange
of messages between Alice and Bob, the resulting session can be typed in [11,
18] but not in [15].

Our goal is to devise a type system for asynchronous sessions that is
permissive enough to accept the sessions of Example 1.1 and Example 1.2, while
rejecting dangerous races that could lead to deadlock or starvation. In
particular, we will not be able to type the sessions discussed in the
introductions of [15, 18], since they both have a possibility of starvation.

For typing asynchronous sessions we use global types that split communications
into outputs and inputs, following the approach advocated in [5, 8]. For
instance, the session of Example 1.2 has the following global type: ${\sf
p}!{\sf q}.a;{\sf q}!{\sf p}.a;{\sf p}?{\sf q}.a;{\sf q}?{\sf p}.a;{\sf
p}!\\{{\sf q}.\ell;{\sf G}_{\\_}1\,,\,{\sf q}.\ell\textquoteright;{\sf
G}_{\\_}2\\}$ where ${\sf G}_{\\_}1={\sf p}!{\sf r}.b;{\sf q}?{\sf
p}.\ell;{\sf r}?\\{{\sf p}.b\,,\,{\sf q}.b\\}$ and ${\sf G}_{\\_}2={\sf
q}?{\sf p}.\ell\textquoteright;{\sf q}!{\sf r}.b;{\sf r}?\\{{\sf p}.b\,,\,{\sf
q}.b\\}$. Here ${\sf p}!{\sf q}.a$ denotes a send from ${\sf p}$ to ${\sf q}$
of label $a$, ${\sf p}?{\sf q}.a$ denotes a receive by ${\sf p}$ from ${\sf
q}$ of label $a$, ${\sf p}!\\{{\sf q}.\ell;{\sf G}_{\\_}1\,,\,{\sf
q}.\ell\textquoteright;{\sf G}_{\\_}2\\}$ is an output choice with sender
${\sf p}$ and receiver ${\sf q}$, and ${\sf r}?\\{{\sf p}.b\,,\,{\sf q}.b\\}$
is an input choice with receiver ${\sf r}$ and senders ${\sf p}$ and ${\sf
q}$.

The rest of the paper is organised as follows. In Section 2 we introduce our
calculus for asynchronous sessions. In Section 3 we define the syntax and
semantics of global types. In Section 4 we present our type system, illustrate
it with some examples, and establish the properties of Subject Reduction,
Session Fidelity and Lock-freedom. We conclude in Section 5 with a discussion
on future and related work.

##  2 Asynchronous Sessions

We assume the following base sets: _participants_ , ranged over by ${\sf
p},{\sf q},{\sf r}$ and forming the set ${\sf Part}$, and _labels_ , ranged
over by $\ell,\ell^{\prime},\dots$ and forming the set ${\sf Lab}$.

######  Definition 2.1 (Processes)

Processes are defined by:

$\begin{array}[]{rcl}P&::=_{\rho}&\mathbf{0}\mid\bigoplus_{i\in I}{\sf
p}_{i}!\ell_{i};P_{i}\mid\Sigma_{i\in I}{\sf p}_{i}?\ell_{i};P_{i}\end{array}$

where $I\neq\emptyset$ and ${\sf p}_{\\_}h!\ell_{\\_}h\neq{\sf
p}_{\\_}k!\ell_{\\_}k$ and ${\sf p}_{\\_}h?\ell_{\\_}h\neq{\sf
p}_{\\_}k?\ell_{\\_}k$ for $h,k\in I$ and $h\neq k$.

A process may be terminated, or it is an internal choice of outputs or an
external choice of inputs. The symbol $::=_{\rho}$, in Definition 2.1 and in
later definitions, indicates that the productions should be interpreted
_coinductively_ (they define possibly infinite processes) and that we focus on
_regular_ terms, namely, terms with finitely many distinct subterms. In this
way, we only obtain processes which are solutions of finite sets of equations,
see [7]. So, when writing processes, we shall use (mutually) recursive
equations.

In the following, we will omit trailing $\mathbf{0}$’s when writing processes.

In a full-fledged calculus, processes would exchange labels of the form
$\ell(v)$, where $v$ is a value. For simplicity, we consider only pure labels
here.

In our calculus, asynchronous communication is handled in the standard way, by
storing sent labels in a queue together with sender and receiver names.
Receivers may then fetch messages from the queue when required. We define
_messages_ to be triples $\langle{\sf p},\ell,{\sf q}\rangle$, where ${\sf p}$
is the sender and ${\sf q}$ is the receiver, and _message queues_ (or simply
_queues_) to be possibly empty sequences of messages:

$\mathcal{M}::=\emptyset\mid\langle{\sf p},\ell,{\sf
q}\rangle\cdot\mathcal{M}$

The order of messages in the queue is the order in which they will be read.
Since the only reading order that matters is that between messages with the
same sender and the same receiver, we consider message queues modulo the
structural equivalence given by:

$\mathcal{M}\cdot\langle{\sf p},\ell,{\sf q}\rangle\cdot\langle{\sf
r},\ell^{\prime},{\sf
s}\rangle\cdot\mathcal{M}^{\prime}\equiv\mathcal{M}\cdot\langle{\sf
r},\ell^{\prime},{\sf s}\rangle\cdot\langle{\sf p},\ell,{\sf
q}\rangle\cdot\mathcal{M}^{\prime}~{}~{}\text{if}~{}~{}{\sf p}\not={\sf
r}~{}~{}\text{or}~{}~{}{\sf q}\not={\sf s}$

Sessions are composed by a number of located processes of the form ${\sf
p}[\\![\,P\,]\\!]$, each enclosed within a different participant ${\sf p}$,
and by a message queue.

######  Definition 2.2 (Networks and Sessions)

Networks are defined by:

${\mathbb{N}}={\sf
p}_{\\_}1[\\![\,P_{\\_}1\,]\\!]\mathrel{\|}\cdots\mathrel{\|}{\sf
p}_{\\_}n[\\![\,P_{\\_}n\,]\\!]$ with ${\sf p}_{\\_}h\neq{\sf p}_{\\_}k$ for
any $h\neq k$

Sessions are defined by:

${\mathbb{N}}\parallel\mathcal{M}$

where ${\mathbb{N}}$ is a network, and $\mathcal{M}$ is a message queue.

We assume the standard structural congruence $\equiv$ on networks666 By abuse
of notation, we use the same symbol as for structural equivalence on queues.,
stating that parallel composition is associative and commutative and has
neutral element ${\sf p}[\\![\,\mathbf{0}\,]\\!]$ for any fresh ${\sf p}$.

If $P\neq\mathbf{0}$ we write ${\sf p}[\\![\,P\,]\\!]\in{\mathbb{N}}$ as short
for ${\mathbb{N}}\equiv{\sf
p}[\\![\,P\,]\\!]\mathrel{\|}{\mathbb{N}}^{\prime}$ for some
${\mathbb{N}}^{\prime}$. This abbreviation is justified by the associativity
and commutativity of parallel composition.

To define the operational semantics of sessions, we use an LTS whose
transitions are decorated by outputs or inputs. Therefore, we define the set
of input/output communications (communications for short), ranged over by
$\beta$, $\beta^{\prime}$, to be $\\{{\sf p}!{\sf q}.\ell,{\sf p}?{\sf
q}.\ell~{}|~{}{\sf p},{\sf q}\in{\sf Part},\ell\in{\sf Lab}\\}$, where ${\sf
p}!{\sf q}.\ell$ represents the output of the label $\ell$ from participant
${\sf p}$ to participant ${\sf q}$, and ${\sf p}?{\sf q}.\ell$ the input by
participant ${\sf p}$ of the label $\ell$ sent by participant ${\sf q}$.

The LTS semantics of networks, defined modulo $\equiv$, is specified by the
two Rules ${[\textsc{Send}]}$ and ${[\textsc{Rcv}]}$ given in Figure 1. Rule
${[\textsc{Send}]}$ allows a participant ${\sf p}$ with an internal choice (a
sender) to send to the participant ${\sf q}_{\\_}k$ the label $\ell_{\\_}k$ by
adding it to the queue. Symmetrically, Rule ${[\textsc{Rcv}]}$ allows a
participant ${\sf q}$ with an external choice (a receiver) to read the label
$\ell_{\\_}k$ sent by participant ${\sf p}_{\\_}k$, provided this label is
among the $\ell_{\\_}j$’s specified in the choice. Thanks to structural
equivalence, the first message from ${\sf p}_{\\_}k$ to ${\sf q}$ that appears
in the queue, if any, can always be moved to the top of the queue.

A key role in this paper is played by (possibly empty) sequences of
communications. As usual we define them as traces.

######  Definition 2.3 (Traces)

(Finite) traces are defined by:

$\tau::=\epsilon\mid\beta\,{\cdot}\,\tau$

We use $\\!\\!~{}|~{}\\!\tau\\!\\!~{}|~{}\\!$ to denote the length of the
trace $\tau$.

When $\tau=\beta_{\\_}1\,{\cdot}\,\ldots\,{\cdot}\,\beta_{\\_}n$ ($n\geq 1)$
we write
${\mathbb{N}}\mathrel{\|}\mathcal{M}\xrightarrow{\tau}{\mathbb{N}}^{\prime}\mathrel{\|}\mathcal{M}^{\prime}$
as short for

${\mathbb{N}}\mathrel{\|}\mathcal{M}\xrightarrow{\beta_{\\_}1}{\mathbb{N}}_{\\_}1\mathrel{\|}\mathcal{M}_{\\_}1\cdots\xrightarrow{\beta_{\\_}n}{\mathbb{N}}_{\\_}{n}\mathrel{\|}\mathcal{M}_{\\_}{n}={\mathbb{N}}^{\prime}\mathrel{\|}\mathcal{M}^{\prime}$

We now introduce the notion of player, which is characteristic of asynchronous
communication, where only one of the involved participants is active, namely
the sender for an output communication and the receiver for an input
communication. The player of a communication $\beta$ is the participant who is
active in $\beta$. The set of players of a trace is then obtained by
collecting the players of all its communications.

######  Definition 2.4 (Players of communications and traces)

We denote by ${\sf play}(\beta)$ the player of a communication $\beta$ defined
by

${\sf play}({\sf p}!{\sf q}.\ell)={\sf play}({\sf p}?{\sf q}.\ell)={\sf p}$

We denote by ${\sf Players}(\tau)$ the set of players of a trace $\tau$
defined by

${\sf Players}(\epsilon)=\emptyset\qquad{\sf
Players}(\beta\,{\cdot}\,\tau)=\\{{\sf play}(\beta)\\}\cup{\sf Players}(\tau)$

$\begin{array}[]{c}\\\\[5.0pt] {\sf p}[\\![\,\bigoplus_{i\in I}{\sf
q}_{i}!\ell_{i};P_{i}\,]\\!]\mathrel{\|}{\mathbb{N}}\mathrel{\|}\mathcal{M}\xrightarrow{{\sf
p}!{\sf q}_{\\_}k.\ell_{\\_}k}{\sf
p}[\\![\,P_{\\_}k\,]\\!]\mathrel{\|}{\mathbb{N}}\mathrel{\|}\mathcal{M}\cdot\langle{\sf
p},\ell_{\\_}k,{\sf q}_{\\_}k\rangle\quad\text{ where }\ k\in
I\quad{~{}~{}~{}~{}~{}~{}{[\textsc{Send}]}}\\\\[3.0pt] {\sf
q}[\\![\,\Sigma_{j\in J}{\sf
p}_{j}?\ell_{j};Q_{j}\,]\\!]\mathrel{\|}{\mathbb{N}}\mathrel{\|}\langle{\sf
p}_{\\_}k,\ell_{\\_}k,{\sf q}\rangle\cdot\mathcal{M}\xrightarrow{{\sf q}?{\sf
p}_{\\_}k.\ell_{\\_}k}{\sf
q}[\\![\,Q_{\\_}k\,]\\!]\mathrel{\|}{\mathbb{N}}\mathrel{\|}\mathcal{M}\quad\text{
where }\ k\in J\quad{~{}~{}~{}~{}~{}~{}{[\textsc{Rcv}]}}\\\\[3.0pt]
\end{array}$

Figure 1: LTS for sessions.

##  3 Global Types

As in [5, 8], our global types can be obtained from the standard ones [12, 13]
by splitting output and input communications. The novelty is that we allow
multiple receivers in output choices and multiple senders in input choices.

######  Definition 3.1 (Global types)

_Global types_ ${\sf G}$ are defined by the following grammar:

$\begin{array}[]{rcl}{\sf G}&::=_{\rho}&{\sf p}!\\{{\sf q}_{i}.\ell_{i};{\sf
G}_{i}\\}_{i\in I}\mid{\sf p}?\\{{\sf q}_{i}.\ell_{i};{\sf G}_{i}\\}_{i\in
I}\mid\sf{End}\end{array}$

where $I\neq\emptyset$, ${\sf p}\neq{\sf q}_{\\_}i$ for all $i\in I$ and ${\sf
q}_{\\_}h.\ell_{\\_}h\not={\sf q}_{\\_}k.\ell_{\\_}k\,$ for $h,k\in I$ and
$h\neq k$.

As for processes, $::=_{\rho}$ indicates that global types are coinductively
defined and _regular_.

The global type ${\sf p}!\\{{\sf q}_{i}.\ell_{i};{\sf G}_{i}\\}_{i\in I}$
specifies that player ${\sf p}$ sends the label $\ell_{\\_}k$ with $k\in I$ to
participant ${\sf q}_{\\_}k$ and then the interaction described by the global
type ${\sf G}_{\\_}k$ takes place. The global type ${\sf p}?\\{{\sf
q}_{i}.\ell_{i};{\sf G}_{i}\\}_{i\in I}$ specifies that player ${\sf p}$
receives the label $\ell_{\\_}k$ with $k\in I$ from participant ${\sf
q}_{\\_}k$ and then the interaction described by the global type ${\sf
G}_{\\_}k$ takes place.

We define ${\sf Players}({\sf G})$ as the smallest set satisfying the
following equations:

${\sf Players}(\sf{End})=\emptyset\quad{\sf Players}({\sf p}!\\{{\sf
q}_{i}.\ell_{i};{\sf G}_{i}\\}_{i\in I})={\sf Players}({\sf p}?\\{{\sf
q}_{i}.\ell_{i};{\sf G}_{i}\\}_{i\in I})=\\{{\sf p}\\}\cup\bigcup_{\\_}{i\in
I}{\sf Players}({\sf G}_{\\_}i)$

The regularity of global types ensures that the sets of players are finite. In
Section 2 we used the same notation for the players of traces. In all cases,
the context should make it easy to understand which function is in use.

To avoid starvation we require global types to satisfy a boundedness
condition. To formalise boundedness we use $\xi$ to denote a _path_ in global
type trees, i.e., a possibly infinite sequence of communications $\beta$. Note
that a finite path is a trace in the sense of Definition 2.3. We extend the
notation $\cdot$ to denote also the concatenation of a finite sequence with a
possibly infinite sequence. The function ${\sf Paths}$ gives the set of
_paths_ of a global type, which is the greatest set such that:

$\begin{array}[]{ll}{\sf Paths}(\sf{End})&=\\{\epsilon\\}\\\ {\sf Paths}({\sf
p}!\\{{\sf q}_{i}.\ell_{i};{\sf G}_{i}\\}_{i\in I})&=\bigcup_{\\_}{i\in
I}\\{{\sf p}!{\sf q}.\ell_{\\_}i\,{\cdot}\,\xi\mid\xi\in{\sf Paths}({\sf
G}_{\\_}i)\\}\\\ {\sf Paths}({\sf p}?\\{{\sf q}_{i}.\ell_{i};{\sf
G}_{i}\\}_{i\in I})&=\bigcup_{\\_}{i\in I}\\{{\sf p}?{\sf
q}.\ell_{\\_}i\,{\cdot}\,\xi\mid\xi\in{\sf Paths}({\sf
G}_{\\_}i)\\}\end{array}$

If $x\in\mathbf{N}\cup\\{\omega\\}$ is the length of $\xi$, we denote by
$\xi[n]$ the $n$-th communication in the path $\xi$, where $1\leq n<x$. It is
handy to define the _depth_ of a player ${\sf p}$ in a global type ${\sf G}$,
${\sf depth}({\sf G},{\sf p})$.

######  Definition 3.2 (Depth of a player)

Let ${\sf G}$ be a global type. For ${\xi\in{\sf Paths}({\sf G})}$ set

${\sf depth}(\xi,{\sf p})=\inf\\{n\mid{\sf play}(\xi[n])={\sf p}\\}$

and define ${\sf depth}({\sf G},{\sf p})$, the _depth_ of ${\sf p}$ in ${\sf
G}$, as follows:

${\sf depth}({\sf G},{\sf p})=\begin{cases}\sup\\{{\sf depth}(\xi,{\sf
p})\mid\xi\in{\sf Paths}({\sf G})\\}&{\sf p}\in{\sf Players}({\sf G})\\\
0&\text{otherwise}\end{cases}$

Note that ${\sf depth}({\sf G},{\sf p})=0$ iff ${\sf p}\not\in{\sf
Players}({\sf G})$. Moreover, if ${\sf p}\neq{\sf play}(\xi[n])$ for all
$n\in\mathbf{N}$, then ${\sf depth}(\xi,{\sf p})=\inf\,\emptyset=\infty$.
Hence, if ${\sf p}$ is a player of a global type ${\sf G}$ and there is some
path in ${\sf G}$ where ${\sf p}$ does not occur as a player, then ${\sf
depth}({\sf G},{\sf p})=\infty$.

######  Definition 3.3 (Boundedness)

A global type ${\sf G}$ is _bounded_ if ${\sf depth}({\sf G}^{\prime},{\sf
p})$ is finite for all participants ${\sf p}\in{\sf Players}({\sf G})$ and all
types ${\sf G}^{\prime}$ which occur in ${\sf G}$.

###### Example 3.4

The following example shows the necessity of considering all types occurring
in a global type for defining boundedness. Consider ${\sf G}={\sf r}!{\sf
q}.\ell;{\sf q}?{\sf r}.\ell;{\sf G}^{\prime}$, where

${\sf G}^{\prime}={\sf p}!\\{{\sf q}.\ell_{\\_}1;{\sf q}?{\sf
p}.\ell_{\\_}1;{\sf q}!{\sf r}.\ell_{\\_}3;{\sf r}?{\sf
q}.\ell_{\\_}3\,,\,{\sf q}.\ell_{\\_}2;{\sf q}?{\sf p}.\ell_{\\_}2;{\sf
G}^{\prime}\\}$

Then we have: ${\sf depth}({\sf G},{\sf p})=3,{\sf depth}({\sf G},{\sf
q})=2,{\sf depth}({\sf G},{\sf r})=1$, whereas ${\sf depth}({\sf
G}^{\prime},{\sf p})=1,{\sf depth}({\sf G}^{\prime},{\sf q})=2,{\sf
depth}({\sf G}^{\prime},{\sf r})=\infty$.

Since global types are regular the boundedness condition is decidable.

$\begin{array}[]{c}\hbox{\hbox{$\hbox{\small\small{{{{[{Top-
Out}]}}}}}\;$}${\hbox{$\displaystyle\displaystyle{\hbox{\hskip
0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hbox{$\displaystyle\displaystyle$}}}\vbox{}}}\over\hbox{\hskip
100.7604pt\vbox{\vbox{}\hbox{\hskip-100.7604pt\hbox{\hbox{$\displaystyle\displaystyle{\sf
p}!\\{{\sf q}_{i}.\ell_{i};{\sf G}_{i}\\}_{i\in
I}\mathrel{\|}\mathcal{M}\xrightarrow{{\sf p}!{\sf q}_{\\_}h.\ell_{\\_}h}{\sf
G}_{\\_}h\mathrel{\|}\mathcal{M}\cdot\langle{\sf p},\ell_{\\_}h,{\sf
q}_{\\_}h\rangle$}}}}}}$}}\hbox{\hbox{}\hbox{$\;\hbox{\small\small{$\begin{array}[]{l}{h\in
I}\end{array}$}}$}}$ }\\\\[17.22217pt]
\hbox{\hbox{$\hbox{\small\small{{{{[{Top-
In}]}}}}}\;$}${\hbox{$\displaystyle\displaystyle{\hbox{\hskip
0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hbox{$\displaystyle\displaystyle$}}}\vbox{}}}\over\hbox{\hskip
102.70485pt\vbox{\vbox{}\hbox{\hskip-102.70485pt\hbox{\hbox{$\displaystyle\displaystyle{\sf
p}?\\{{\sf q}_{i}.\ell_{i};{\sf G}_{i}\\}_{i\in I}\mathrel{\|}\langle{\sf
q}_{\\_}h,\ell_{\\_}h,{\sf p}\rangle\cdot\mathcal{M}\xrightarrow{{\sf
q}_{\\_}h?{\sf p}.\ell_{\\_}h}{\sf
G}_{\\_}h\mathrel{\|}\mathcal{M}$}}}}}}$}}\hbox{\hbox{}\hbox{$\;\hbox{\small\small{$\begin{array}[]{l}{h\in
I}\end{array}$}}$}}$ }\\\\[17.22217pt]
\hbox{\hbox{$\hbox{\small\small{{{{[{Inside-
Out}]}}}}}\;$}${\hbox{$\displaystyle\displaystyle{\hbox{\hskip
102.36359pt\vbox{\hbox{\hskip-102.36357pt\hbox{\hbox{$\displaystyle\displaystyle{\sf
G}_{\\_}i\mathrel{\|}\mathcal{M}\cdot\langle{\sf p},\ell_{\\_}i,{\sf
q}_{\\_}i\rangle\xrightarrow{\beta}{\sf
G}^{\prime}_{\\_}i\mathrel{\|}\mathcal{M}^{\prime}\cdot\langle{\sf
p},\ell_{\\_}i,{\sf q}_{\\_}i\rangle\quad\forall i\in
I$}}}\vbox{}}}\over\hbox{\hskip
77.26901pt\vbox{\vbox{}\hbox{\hskip-77.26901pt\hbox{\hbox{$\displaystyle\displaystyle{\sf
p}!\\{{\sf q}_{i}.\ell_{i};{\sf G}_{i}\\}_{i\in
I}\mathrel{\|}\mathcal{M}\xrightarrow{\beta}{\sf p}!\\{{\sf
q}_{i}.\ell_{i};{\sf G}^{\prime}_{i}\\}_{i\in
I}\mathrel{\|}\mathcal{M}^{\prime}$}}}}}}$}}\hbox{\hbox{}\hbox{$\;\hbox{\small\small{$\begin{array}[]{l}{{\sf
p}\neq{\sf play}(\beta)}\end{array}$}}$}}$ }\\\\[17.22217pt]
\hbox{\hbox{$\hbox{\small\small{{{{[{Inside-
In}]}}}}}\;$}${\hbox{$\displaystyle\displaystyle{\hbox{\hskip
56.70457pt\vbox{\hbox{\hskip-56.70456pt\hbox{\hbox{$\displaystyle\displaystyle{\sf
G}_{\\_}{j}\mathrel{\|}\mathcal{M}\xrightarrow{\beta}{\sf
G}_{\\_}{j}^{\prime}\mathrel{\|}\mathcal{M}^{\prime}\quad\forall{j}\in
J$}}}\vbox{}}}\over\hbox{\hskip
79.21346pt\vbox{\vbox{}\hbox{\hskip-79.21346pt\hbox{\hbox{$\displaystyle\displaystyle{\sf
p}?\\{{\sf q}_{i}.\ell_{i};{\sf G}_{i}\\}_{i\in
I}\mathrel{\|}\mathcal{M}\xrightarrow{\beta}{\sf p}?\\{{\sf
q}_{i}.\ell_{i};{\sf G}^{\prime}_{i}\\}_{i\in
I}\mathrel{\|}{\mathcal{M}^{\prime}}$}}}}}}$}}\hbox{\hbox{}\hbox{$\;\hbox{\small\small{$\begin{array}[]{l}{\begin{array}[]{c}J={\sf
rm}(\\{\langle{\sf q}_{\\_}i,\ell_{\\_}i,{\sf p}\rangle\\}_{\\_}{i\in
I},\mathcal{M})\neq\emptyset\\\ {\sf p}\neq{\sf play}(\beta)\quad\beta\neq{\sf
q}_{\\_}l!{\sf p}.{\ell_{\\_}l}\\\ {\sf G}^{\prime}_{\\_}l={\sf
G}_{\\_}k~{}~{}k\in J~{}~{}\forall l\in I\backslash
J\end{array}}\end{array}$}}$}}$ }\end{array}$

Figure 2: LTS for type configurations.

Global types in parallel with queues, dubbed _type configurations_ , are given
semantics by means of the LTS in Figure 2. The first two rules allow top level
outputs and inputs to be performed in the standard way. The remaining two
rules allow communications to be performed inside output and input choices.
These inside rules are needed to enable interleaving between independent
communications despite the sequential structure of global types. For example,
we want to allow ${\sf p}!{\sf q}.\ell;{\sf r}!{\sf
s}.\ell^{\prime}\mathrel{\|}\emptyset\xrightarrow{{\sf r}!{\sf
s}.\ell^{\prime}}{{\sf p}!{\sf q}.\ell}\mathrel{\|}\langle{\sf
r},\ell^{\prime},{\sf s}\rangle$ when ${\sf p}\neq{\sf r}$, because,
intuitively, outputs performed by different players should be independent.
This justifies the condition ${\sf p}\neq{\sf play}(\beta)$ in Rules [Inside-
Out] and [Inside-In]. In Rule [Inside-Out] we require all branches to be able
to perform the $\beta$ transition. This avoids for example:

$\begin{array}[]{c}{\sf p}!\\{{\sf q}.\ell;{\sf q}?{\sf p}.\ell;{\sf r}!{\sf
p}.\ell;{\sf p}?{\sf r}.\ell\,,\,{\sf q}.\ell^{\prime};{\sf q}?{\sf
p}.\ell^{\prime};{\sf r}!{\sf p}.\ell^{\prime};{\sf p}?{\sf
r}.\ell^{\prime}\\}\mathrel{\|}\emptyset\xrightarrow{{\sf r}!{\sf p}.\ell}\\\
{\sf p}!\\{{\sf q}.\ell;{\sf q}?{\sf p}.\ell;{\sf p}?{\sf r}.\ell\,,\,{\sf
q}.\ell^{\prime};{\sf q}?{\sf p}.\ell^{\prime};{\sf r}!{\sf
p}.\ell^{\prime};{\sf p}?{\sf r}.\ell^{\prime}\\}\mathrel{\|}\langle{\sf
r},\ell,{\sf p}\rangle\end{array}$

which, in case we choose the right branch, leads to the configuration ${\sf
p}?{\sf r}.\ell^{\prime}\mathrel{\|}\langle{\sf r},\ell,{\sf
p}\rangle\cdot\langle{\sf r},\ell^{\prime},{\sf p}\rangle$.

The shapes of the queues appearing in the premise of Rule [Inside-Out] ensure
that $\beta$ is not the matching input for any output in the choice. In Rule
[Inside-In], we consider only the branches with corresponding messages on top
of the queue (called live branches), using the index set of ready messages
${\sf rm}(\\{\langle{\sf q}_{\\_}i,\ell_{\\_}i,{\sf p}\rangle\\}_{\\_}{i\in
I},\mathcal{M})$ defined as follows, where ${\sf m}$ ranges over messages.

###### Definition 3.5

Given a set of messages $\\{{\sf m}_{\\_}i\\}_{\\_}{i\in I}$ and a queue
$\mathcal{M}$, the index set of the “ready messages” in this set is defined
by: ${\sf rm}(\\{{\sf m}_{\\_}i\\}_{\\_}{i\in I},\mathcal{M})=\\{i\in
I\mid\mathcal{M}\equiv{\sf m}_{\\_}i\cdot\mathcal{M}_{\\_}i\\}$.

The mapping ${\sf rm}$ plays a crucial role also in the typing rule for input
choices, as we will see in Section 4. The condition $J\neq\emptyset$ means
that there is at least one live branch. The condition $\beta\neq{\sf
q}_{\\_}l!{\sf p}.{\ell_{\\_}l}$ for all $l\in I\backslash J$ ensures that the
occurrence of $\beta$ does not generate a message that would “awaken” some
dead, i.e. not live, branch of the choice. In the resulting choice, the dead
branches become an arbitrary live branch (condition ${\sf
G}^{\prime}_{\\_}l={\sf G}_{\\_}k$ for some $k\in J$ and for all $l\in
I\backslash J$). In fact, such branches could also be omitted as they can
never be awaken.

It is easy to check that the LTS of type configurations preserves boundedness
of global types. Therefore, from now on we will assume all our global types to
be bounded.

##  4 Type System

$\begin{array}[]{c}\hbox{\hbox{$\hbox{\small\small{{{[{End}]}}}}\;$}${\hbox{\hbox{$\displaystyle\displaystyle{\hbox{\raise
1.83437pt\hbox{$\displaystyle\hbox{\hskip 0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hbox{$\displaystyle\displaystyle$}}}\vbox{}}}$}}\atop\hbox{\lower
2.78159pt\hbox{$\displaystyle\hbox{\hskip
27.8473pt\vbox{\vbox{}\hbox{\hskip-27.84729pt\hbox{\hbox{$\displaystyle\displaystyle\sf{End}\vdash{\sf
p}[\\![\,\mathbf{0}\,]\\!]\mathrel{\|}\emptyset$}}}}}$}}}$}\hskip-55.69461pt\hbox
to55.69461pt{$\displaystyle\mathrel{=}\joinrel\xleaders\hbox{\hbox{$\displaystyle\mkern-3.0mu=\mkern-3.0mu$}}\hfil\joinrel\mathrel{=}$}}}\hbox{\hbox{}\hbox{$\;\hbox{\small\small{$\begin{array}[]{l}\end{array}$}}$}}$
}\\\\[25.83325pt]
\hbox{\hbox{$\hbox{\small\small{{{[{Out}]}}}}\;$}${\hbox{\hbox{$\displaystyle\displaystyle{\hbox{\raise
1.83437pt\hbox{$\displaystyle\hbox{\hskip
163.03859pt\vbox{\hbox{\hskip-163.03859pt\hbox{\hbox{$\displaystyle\displaystyle{\sf
G}_{\\_}i\vdash{\sf
p}[\\![\,P_{\\_}i\,]\\!]\mathrel{\|}{\mathbb{N}}\mathrel{\|}\mathcal{M}\cdot\langle{\sf
p},\ell_{\\_}i,{\sf q}_{\\_}i\rangle$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\sf Players}({\sf
G}_{\\_}i)\setminus\\{{\sf p}\\}={\sf Players}({\mathbb{N}})\ \ \forall i\in
I$}}}}\vbox{}}}$}}\atop\hbox{\lower 2.78159pt\hbox{$\displaystyle\hbox{\hskip
77.31863pt\vbox{\vbox{}\hbox{\hskip-77.31862pt\hbox{\hbox{$\displaystyle\displaystyle{\sf
p}!\\{{\sf q}_{i}.\ell_{i};{\sf G}_{i}\\}_{i\in I}\vdash{\sf
p}[\\![\,\bigoplus_{i\in I}{\sf
q}_{i}!\ell_{i};P_{i}\,]\\!]\mathrel{\|}{\mathbb{N}}\mathrel{\|}\mathcal{M}$}}}}}$}}}$}\hskip-326.07718pt\hbox
to326.07718pt{$\displaystyle\mathrel{=}\joinrel\xleaders\hbox{\hbox{$\displaystyle\mkern-3.0mu=\mkern-3.0mu$}}\hfil\joinrel\mathrel{=}$}}}\hbox{\hbox{}\hbox{$\;\hbox{\small\small{$\begin{array}[]{l}\end{array}$}}$}}$
}\\\\[25.83325pt]
\hbox{\hbox{$\hbox{\small\small{{{[{In}]}}}}\;$}${\hbox{\hbox{$\displaystyle\displaystyle{\hbox{\raise
1.83437pt\hbox{$\displaystyle\hbox{\hskip
92.54091pt\vbox{\hbox{\hskip-92.5409pt\hbox{\hbox{$\displaystyle\displaystyle{\sf
G}_{\\_}{j}\vdash{\sf
p}[\\![\,P_{\\_}{j}\,]\\!]\mathrel{\|}{\mathbb{N}}\mathrel{\|}\mathcal{M}_{\\_}{j}\quad{\text{\Large{$\displaystyle\iota$}}({\sf
G}_{\\_}j,\mathbb{M})}\quad\forall j\in
J$}}}\vbox{\hbox{\hskip-87.42014pt\hbox{\hbox{$\displaystyle\displaystyle{\sf
Players}({\sf G}_{\\_}{i})\setminus\\{{\sf p}\\}={\sf
Players}({\mathbb{N}})\quad\forall i\in I$}}}\vbox{}}}}$}}\atop\hbox{\lower
2.78159pt\hbox{$\displaystyle\hbox{\hskip
81.98975pt\vbox{\vbox{}\hbox{\hskip-81.98973pt\hbox{\hbox{$\displaystyle\displaystyle{\sf
p}?\\{{\sf q}_{i}.\ell_{i};{\sf G}_{i}\\}_{i\in I}\vdash{\sf
p}[\\![\,\Sigma_{h\in H}{\sf
q}_{h}?\ell_{h};P_{h}\,]\\!]\mathrel{\|}{\mathbb{N}}\mathrel{\|}\mathcal{M}$}}}}}$}}}$}\hskip-185.08182pt\hbox
to185.08182pt{$\displaystyle\mathrel{=}\joinrel\xleaders\hbox{\hbox{$\displaystyle\mkern-3.0mu=\mkern-3.0mu$}}\hfil\joinrel\mathrel{=}$}}}\hbox{\hbox{}\hbox{$\;\hbox{\small\small{$\begin{array}[]{l}\begin{array}[]{l}J={\sf
rm}(\\{\langle{\sf q}_{\\_}i,\ell_{\\_}i,{\sf p}\rangle\\}_{\\_}{i\in
I},\mathcal{M})\\\ ~{}~{}={\sf rm}(\\{\langle{\sf q}_{\\_}h,\ell_{\\_}h,{\sf
p}\rangle\\}_{\\_}{h\in H},\mathcal{M})\neq\emptyset\\\
\mathcal{M}\equiv\langle{\sf q}_{\\_}{j},\ell_{\\_}{j},{\sf
p}\rangle\cdot\mathcal{M}_{\\_}{j}~{}\forall j\in J\\\
\mathbb{M}=\\{{\langle{\sf q}_{\\_}{l},\ell_{\\_}{l},{\sf p}\rangle}\mid
l\in(I\cup H)\setminus J\ \&\ {\sf q}_{\\_}l\neq{\sf q}_{\\_}j\ \forall j\in
J\\}\end{array}\end{array}$}}$}}$ }\end{array}$

Figure 3: Typing rules for sessions.

Global types are an abstraction of sessions. Usually, global types are
projected to participants, yielding local types which are assigned to
processes. The simplicity of our calculus and the flexibility of our global
types allow us to formulate a type system where global types are directly
derived for sessions, using judgements of the form ${\sf
G}\vdash{\mathbb{N}}\mathrel{\|}\mathcal{M}$. The typing rules are given in
Figure 3.

Rules [Out] and [In] just add simultaneously outputs and inputs to global
types and to the corresponding processes inside networks. The condition ${\sf
Players}({\sf G}_{\\_}i)\setminus\\{{\sf p}\\}={\sf Players}({\mathbb{N}})$
for all $i\in I$ ensures that all players in ${\mathbb{N}}$ are also players
in ${\sf G}$. For example, this condition prevents the derivation of ${\sf
G}\vdash{\sf p}[\\![\,P\,]\\!]\mathrel{\|}{\sf q}[\\![\,Q\,]\\!]$ with ${\sf
G}={\sf p}!{\sf q}.\ell;{\sf G}$ and $P={\sf q}!\ell;P$ and $Q$ arbitrary.

Rule [Out] considers all branches of the global type, since the choice of the
sent message is arbitrary. This rule requires that the session resulting from
the output of a branch be typed with the corresponding branch of the global
type.

Rule [In] requires that the global type and the process read the same messages
on the queue. To this end, it uses the index set of ready messages defined in
Definition 3.5, collecting the indices of the live branches of the global type
and of the input process777 As for global types, a branch of the input process
is live if it has a corresponding message on top of the queue, and dead
otherwise., and asking them to be equal (condition ${\sf rm}(\\{\langle{\sf
q}_{\\_}i,\ell_{\\_}i,{\sf p}\rangle\\}_{\\_}{i\in I},\mathcal{M})={\sf
rm}(\\{\langle{\sf q}_{\\_}h,\ell_{\\_}h,{\sf p}\rangle\\}_{\\_}{h\in
H},\mathcal{M})$. This set of indices must not be empty (condition
$J\neq\emptyset$). Only the branches of the global type and of the input
process thus selected are compared in the premises of Rule [In]. Note that in
this way we allow more freedom than in the synchronous subtyping for session
types [9]. In Rule [In], in order to ensure the condition $\beta\neq{\sf
q}_{\\_}l!{\sf p}.{\ell_{\\_}l}$ for all $l\in I\backslash J$ required by the
transition Rule [Inside-In], we want to prevent the enqueuing of messages that
would transform a dead branch of the process or of the global type into a live
branch. To this end, we introduce a predicate which forbids a global type to
generate such messages. Let $\mathbb{M}$ range over sets of messages.

###### Definition 4.1

The type ${\sf G}$ is inactive for the set of messages $\mathbb{M}$, if
${\text{\Large{$\iota$}}({\sf G},\mathbb{M})}$ holds, where:

$\begin{array}[]{c}{\text{\Large{$\iota$}}(\sf{End},\mathbb{M})}\quad\quad\quad{\text{\Large{$\iota$}}({\sf
p}?\\{{\sf q}_{i}.\ell_{i};{\sf G}_{i}\\}_{i\in I},\mathbb{M})}\quad\text{if}\
{\text{\Large{$\iota$}}({\sf G}_{\\_}i,\mathbb{M})}~{}~{}\forall i\in I\\\
{\text{\Large{$\iota$}}({\sf p}!\\{{\sf q}_{i}.\ell_{i};{\sf G}_{i}\\}_{i\in
I},\mathbb{M})}\quad\text{if}\ {\langle{\sf p},\ell_{\\_}i,{\sf
q}_{\\_}i\rangle\not\in\mathbb{M}}\ \text{and}\ {\text{\Large{$\iota$}}({\sf
G}_{\\_}i,\mathbb{M})}~{}~{}\forall i\in I\end{array}$

The predicate ${\text{\Large{$\iota$}}({\sf G},\mathbb{M})}$ looks for outputs
in ${\sf G}$ which produce messages in $\mathbb{M}$. The regularity of global
types guarantees the computability of this predicate. Notice that
${\text{\Large{$\iota$}}({\sf G},\mathbb{M})}$ also ensures that the network
cannot produce messages in $\mathbb{M}$. This is due to the typing Rule [Out]
prescribing that messages put on the queue by the global type be the same as
the ones of the network.

For example consider the following sequence of transitions

$\begin{array}[]{lll}{\sf q}[\\![\,{\sf
r}!\ell^{\prime}\,]\\!]\mathrel{\|}{\sf r}[\\![\,{\sf p}?\ell;{\sf
q}?\ell^{\prime}+{\sf q}?\ell^{\prime};{\sf
p}?\ell^{\prime}\,]\\!]\mathrel{\|}\langle{\sf p},\ell,{\sf
r}\rangle&\xrightarrow{{\sf q}!{\sf r}.\ell^{\prime}}&{\sf r}[\\![\,{\sf
p}?\ell;{\sf q}?\ell^{\prime}+{\sf q}?\ell^{\prime};{\sf
p}?\ell^{\prime}\,]\\!]\mathrel{\|}\langle{\sf p},\ell,{\sf
r}\rangle\cdot\langle{\sf q},\ell^{\prime},{\sf r}\rangle\\\
&\xrightarrow{{\sf r}?{\sf q}.\ell^{\prime}}&{\sf r}[\\![\,{\sf
p}?\ell^{\prime}\,]\\!]\mathrel{\|}\langle{\sf p},\ell,{\sf
r}\rangle\end{array}$

Since the input and the message in ${\sf r}[\\![\,{\sf
p}?\ell^{\prime}\,]\\!]\mathrel{\|}\langle{\sf p},\ell,{\sf r}\rangle$ do not
match, this session cannot be typed and therefore also the session ${\sf
q}[\\![\,{\sf r}!\ell^{\prime}\,]\\!]\mathrel{\|}{\sf r}[\\![\,{\sf
p}?\ell;{\sf q}?\ell^{\prime}+{\sf q}?\ell^{\prime};{\sf
p}?\ell^{\prime}\,]\\!]\mathrel{\|}\langle{\sf p},\ell,{\sf r}\rangle$ should
not be typable. Without checking the inactivity predicate we can type this
session by the global type

$(\ast)\quad{\sf r}?\\{{\sf p}.\ell;{\sf q}!{\sf r}.\ell^{\prime};{\sf r}?{\sf
q}.\ell^{\prime},{\sf q}.\ell^{\prime};{\sf q}!{\sf r}.\ell^{\prime};{\sf
r}?{\sf p}.\ell^{\prime}\\}$

as follows:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
77.13747pt\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
20.87943pt\hbox{$\displaystyle\penalty 1\sf{End}\vdash{\sf
r}[\\![\,\mathbf{0}\,]\\!]\mathrel{\|}\emptyset$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox
to95.81454pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{\sf r}?{\sf q}.\ell^{\prime}\vdash{\sf r}[\\![\,{\sf
q}?\ell^{\prime}\,]\\!]\mathrel{\|}\langle{\sf q},\ell^{\prime},{\sf
r}\rangle$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox
to130.03339pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{}}}\hbox{\kern
0.21437pt\hbox{$\displaystyle{\sf q}!{\sf r}.\ell^{\prime};{\sf r}?{\sf
q}.\ell^{\prime}\vdash{\sf q}[\\![\,{\sf
r}!\ell^{\prime}\,]\\!]\mathrel{\|}{\sf r}[\\![\,{\sf
q}?\ell^{\prime}\,]\\!]\mathrel{\|}\emptyset$}}}}\hskip 5.0pt plus
1.0fil\penalty 2$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox
to318.52715pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{\sf r}?\\{{\sf p}.\ell;{\sf q}!{\sf
r}.\ell^{\prime};{\sf r}?{\sf q}.\ell^{\prime},{\sf q}.\ell^{\prime};{\sf
q}!{\sf r}.\ell^{\prime};{\sf r}?{\sf p}.\ell^{\prime}\\}\vdash{\sf
q}[\\![\,{\sf r}!\ell^{\prime}\,]\\!]\mathrel{\|}{\sf r}[\\![\,{\sf
p}?\ell;{\sf q}?\ell^{\prime}+{\sf q}?\ell^{\prime};{\sf
p}?\ell^{\prime}\,]\\!]\mathrel{\|}\langle{\sf p},\ell,{\sf r}\rangle$}}}}$

The problem here is that Rule [In] does not check the dead branches of the
global type. The role of the inactivity predicate is just to ensure that the
transitions will not awake dead branches. This is done by checking the outputs
in the live branches. In this example the output ${\sf q}!{\sf
r}.\ell^{\prime}$ is in the branch starting with the input ${\sf r}?{\sf
p}.\ell$ and the queue contains $\langle{\sf p},\ell,{\sf r}\rangle$. So the
typing Rule [In] cannot be applied since ${\text{\Large{$\iota$}}({\sf q}!{\sf
r}.\ell^{\prime};{\sf r}?{\sf q}.\ell^{\prime},\\{\langle{\sf
q},\ell^{\prime},{\sf r}\rangle\\})}$ does not hold.

Notice that the session in Example 1.1 has the transition

$\begin{array}[]{lll}{\sf p}[\\![\,{\sf r}!\ell\,]\\!]\mathrel{\|}{\sf
q}[\\![\,{\sf r}!{\ell^{\prime}}\,]\\!]\mathrel{\|}{\sf r}[\\![\,{\sf
p}?\ell;{\sf q}?\ell^{\prime}+{\sf q}?\ell^{\prime};{\sf
p}?\ell\,]\\!]\mathrel{\|}\emptyset&\xrightarrow{{\sf p}!{\sf r}.\ell}&{\sf
q}[\\![\,{\sf r}!{\ell^{\prime}}\,]\\!]\mathrel{\|}{\sf r}[\\![\,{\sf
p}?\ell;{\sf q}?\ell^{\prime}+{\sf q}?\ell^{\prime};{\sf
p}?\ell\,]\\!]\mathrel{\|}\langle{\sf p},\ell,{\sf r}\rangle\end{array}$

and the resulting session differs from that of the previous example only for
the label of the last input. Correspondingly, the global types ${\sf
r}?\\{{\sf p}.\ell;{\sf q}!{\sf r}.\ell^{\prime};{\sf r}?{\sf
q}.\ell^{\prime}\,,\,{\sf q}.\ell^{\prime};\underline{{\sf r}?{\sf
p}.\ell}\\}$ and ${\sf r}?\\{{\sf p}.\ell;{\sf q}!{\sf r}.\ell^{\prime};{\sf
r}?{\sf q}.\ell^{\prime}\,,\,{\sf q}.\ell^{\prime};\underline{{\sf r}?{\sf
p}.\ell^{\prime}}\\}$ only differ for the labels of the underlined inputs.
Therefore ${\sf r}?\\{{\sf p}.\ell;{\sf q}!{\sf r}.\ell^{\prime};{\sf r}?{\sf
q}.\ell^{\prime}\,,\,{\sf q}.\ell^{\prime};{{\sf r}?{\sf p}.\ell}\\}$ cannot
be derived for the session ${\sf q}[\\![\,{\sf
r}!{\ell^{\prime}}\,]\\!]\mathrel{\|}{\sf r}[\\![\,{\sf p}?\ell;{\sf
q}?\ell^{\prime}+{\sf q}?\ell^{\prime};{\sf
p}?\ell\,]\\!]\mathrel{\|}\langle{\sf p},\ell,{\sf r}\rangle$, since as we
just saw the predicate ${\text{\Large{$\iota$}}({\sf q}!{\sf
r}.\ell^{\prime};{\sf r}?{\sf q}.\ell^{\prime},\\{\langle{\sf
q},\ell^{\prime},{\sf r}\rangle\\})}$ does not hold. In fact, this is expected
since the session can do a transition $\xrightarrow{{\sf q}!{\sf
r}.\ell^{\prime}}$ that the type configuration cannot mimic. On the other
hand, this session can be typed by the global type

${\sf q}!{\sf r}.\ell^{\prime};{\sf r}?\\{{\sf p}.\ell;{\sf r}?{\sf
q}.\ell^{\prime}\,,\,{\sf q}.\ell^{\prime};{\sf r}?{\sf p}.\ell\\}$

as follows:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
20.87943pt\hbox{$\displaystyle\penalty 1\sf{End}\vdash{\sf
r}[\\![\,\mathbf{0}\,]\\!]\mathrel{\|}\emptyset$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox
to95.81454pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{\sf r}?{\sf q}.\ell^{\prime}\vdash{\sf r}[\\![\,{\sf
q}?\ell^{\prime}\,]\\!]\mathrel{\|}\langle{\sf q},\ell^{\prime},{\sf
r}\rangle$}}}}\hskip 5.0pt plus 1.0fil\penalty 2\qquad\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
20.37497pt\hbox{$\displaystyle\penalty 1\sf{End}\vdash{\sf
r}[\\![\,\mathbf{0}\,]\\!]\mathrel{\|}\emptyset$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox
to94.80563pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{\sf r}?{\sf p}.\ell\vdash{\sf r}[\\![\,{\sf
p}?\ell\,]\\!]\mathrel{\|}\langle{\sf p},\ell,{\sf r}\rangle$}}}}\hskip 5.0pt
plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\hbox
to279.05789pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{}}}\hbox{\kern
4.76215pt\hbox{$\displaystyle{\sf r}?\\{{\sf p}.\ell;{\sf r}?{\sf
q}.\ell^{\prime}\,,\,{\sf q}.\ell^{\prime};{\sf r}?{\sf p}.\ell\\}\vdash{\sf
r}[\\![\,{\sf p}?\ell;{\sf q}?\ell^{\prime}+{\sf q}?\ell^{\prime};{\sf
p}?\ell\,]\\!]\mathrel{\|}\langle{\sf p},\ell,{\sf r}\rangle\cdot\langle{\sf
q},\ell^{\prime},{\sf r}\rangle$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox
to313.27672pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{}}}\hbox{\kern
8.8654pt\hbox{$\displaystyle{\sf q}!{\sf r}.\ell^{\prime};{\sf r}?\\{{\sf
p}.\ell;{\sf r}?{\sf q}.\ell^{\prime}\,,\,{\sf q}.\ell^{\prime};{\sf r}?{\sf
p}.\ell\\}\vdash{\sf q}[\\![\,{\sf r}!{\ell^{\prime}}\,]\\!]\mathrel{\|}{\sf
r}[\\![\,{\sf p}?\ell;{\sf q}?\ell^{\prime}+{\sf q}?\ell^{\prime};{\sf
p}?\ell\,]\\!]\mathrel{\|}\langle{\sf p},\ell,{\sf r}\rangle$}}}}$

In this derivation Rule [Out] is applied first, and thus Rule [In] is applied
only when the queue contains the matching messages for both branches.
Therefore Rule [In] checks the continuations of both branches, and the
inactivity predicate holds trivially for each of them.

Notice that bringing forward the output from ${\sf q}$ to ${\sf r}$ in the
global type $(\ast)$ does not enable us to type:

${\sf q}[\\![\,{\sf r}!\ell^{\prime}\,]\\!]\mathrel{\|}{\sf r}[\\![\,{\sf
p}?\ell;{\sf q}?\ell^{\prime}+{\sf q}?\ell^{\prime};{\sf
p}?\ell^{\prime}\,]\\!]\mathrel{\|}\langle{\sf p},\ell,{\sf r}\rangle$

In fact, we cannot complete the derivation:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
13.73613pt\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
20.87943pt\hbox{$\displaystyle\penalty 1\sf{End}\vdash{\sf
r}[\\![\,\mathbf{0}\,]\\!]\mathrel{\|}\emptyset$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox
to95.81454pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{\sf r}?{\sf q}.\ell^{\prime}\vdash{\sf r}[\\![\,{\sf
q}?\ell^{\prime}\,]\\!]\mathrel{\|}\langle{\sf q},\ell^{\prime},{\sf
r}\rangle$}}}}\hskip 5.0pt plus 1.0fil\penalty 2\qquad{\sf r}?{\sf
p}.\ell^{\prime}\vdash{\sf r}[\\![\,{\sf
p}?\ell^{\prime}\,]\\!]\mathrel{\|}\langle{\sf p},\ell,{\sf r}\rangle$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox
to272.6136pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{\sf r}?\\{{\sf p}.\ell;{\sf r}?{\sf
q}.\ell^{\prime}\,,\,{\sf q}.\ell^{\prime};{\sf r}?{\sf
p}.\ell^{\prime}\\}\vdash{\sf r}[\\![\,{\sf p}?\ell;{\sf q}?\ell^{\prime}+{\sf
q}?\ell^{\prime};{\sf p}?\ell^{\prime}\,]\\!]\mathrel{\|}\langle{\sf
p},\ell,{\sf r}\rangle\cdot\langle{\sf q},\ell^{\prime},{\sf
r}\rangle$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox
to306.83243pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{}}}\hbox{\kern
4.10327pt\hbox{$\displaystyle{\sf q}!{\sf r}.\ell^{\prime};{\sf r}?\\{{\sf
p}.\ell;{\sf r}?{\sf q}.\ell^{\prime}\,,\,{\sf q}.\ell^{\prime};{\sf r}?{\sf
p}.\ell^{\prime}\\}\vdash{\sf q}[\\![\,{\sf
r}!{\ell^{\prime}}\,]\\!]\mathrel{\|}{\sf r}[\\![\,{\sf p}?\ell;{\sf
q}?\ell^{\prime}+{\sf q}?\ell^{\prime};{\sf
p}?\ell^{\prime}\,]\\!]\mathrel{\|}\langle{\sf p},\ell,{\sf r}\rangle$}}}}$

Indeed, we cannot apply Rule [In] to derive the top right judgement ${\sf
r}?{\sf p}.\ell^{\prime}\vdash{\sf r}[\\![\,{\sf
p}?\ell^{\prime}\,]\\!]\mathrel{\|}\langle{\sf p},\ell,{\sf r}\rangle$, since
the only input does not match the message in the queue.

We can also type the following recursive version of Example 1.1:

${\sf p}[\\![\,P\,]\\!]\mathrel{\|}{\sf q}[\\![\,Q\,]\\!]\mathrel{\|}{\sf
r}[\\![\,R\,]\\!]$

where $P={\sf r}!\ell;P$, $Q={\sf r}!{\ell^{\prime}};Q$ and $R={\sf
p}?\ell;{\sf q}?\ell^{\prime};R+{\sf q}?\ell^{\prime};{\sf p}?\ell;R$. A
suitable global type is

${\sf G}={\sf p}!{\sf r}.\ell;{\sf q}!{\sf r}.\ell^{\prime};{\sf r}?\\{{\sf
p}.\ell;{\sf r}?{\sf q}.\ell^{\prime};{\sf G}\,,\,{\sf q}.\ell^{\prime};{\sf
r}?{\sf p}.\ell;{\sf G}\\}$

as shown by the following derivation:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
18.8395pt\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
48.9633pt\hbox{$\displaystyle\penalty 1\vdots$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox
to105.4266pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{\sf G}\vdash{\sf p}[\\![\,P\,]\\!]\mathrel{\|}{\sf
q}[\\![\,Q\,]\\!]\mathrel{\|}{\sf
r}[\\![\,R\,]\\!]\mathrel{\|}\emptyset$}}}}\hskip 5.0pt plus 1.0fil\penalty
2$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox
to177.32442pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{\sf r}?{\sf q}.\ell^{\prime};{\sf G}\vdash{\sf
p}[\\![\,P\,]\\!]\mathrel{\|}{\sf q}[\\![\,Q\,]\\!]\mathrel{\|}{\sf
r}[\\![\,{\sf q}?\ell^{\prime};R\,]\\!]\mathrel{\|}\langle{\sf
q},\ell^{\prime},{\sf r}\rangle$}}}}\hskip 5.0pt plus 1.0fil\penalty
2\qquad\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 16.94618pt\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
48.9633pt\hbox{$\displaystyle\penalty 1\vdots$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox
to105.4266pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{\sf G}\vdash{\sf p}[\\![\,P\,]\\!]\mathrel{\|}{\sf
q}[\\![\,Q\,]\\!]\mathrel{\|}{\sf
r}[\\![\,R\,]\\!]\mathrel{\|}\emptyset$}}}}\hskip 5.0pt plus 1.0fil\penalty
2$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox
to173.5378pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{\sf r}?{\sf p}.\ell;{\sf G}\vdash{\sf
p}[\\![\,P\,]\\!]\mathrel{\|}{\sf q}[\\![\,Q\,]\\!]\mathrel{\|}{\sf
r}[\\![\,{\sf p}?\ell;R\,]\\!]\mathrel{\|}\langle{\sf p},\ell,{\sf
r}\rangle$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox
to434.2999pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{}}}\hbox{\kern
75.35579pt\hbox{$\displaystyle{\sf r}?\\{{\sf p}.\ell;{\sf r}?{\sf
q}.\ell^{\prime};{\sf G}\,,\,{\sf q}.\ell^{\prime};{\sf r}?{\sf p}.\ell;{\sf
G}\\}\vdash{\sf p}[\\![\,P\,]\\!]\mathrel{\|}{\sf
q}[\\![\,Q\,]\\!]\mathrel{\|}{\sf r}[\\![\,R\,]\\!]\mathrel{\|}\langle{\sf
p},\ell,{\sf r}\rangle\cdot\langle{\sf q},\ell^{\prime},{\sf
r}\rangle$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox
to463.51872pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{}}}\hbox{\kern
93.8541pt\hbox{$\displaystyle{\sf q}!{\sf r}.\ell^{\prime};{\sf r}?\\{{\sf
p}.\ell;{\sf r}?{\sf q}.\ell^{\prime};{\sf G}\,,\,{\sf q}.\ell^{\prime};{\sf
r}?{\sf p}.\ell;{\sf G}\\}\vdash{\sf p}[\\![\,P\,]\\!]\mathrel{\|}{\sf
q}[\\![\,Q\,]\\!]\mathrel{\|}{\sf r}[\\![\,R\,]\\!]\mathrel{\|}\langle{\sf
p},\ell,{\sf r}\rangle$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox
to492.73755pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{}}}\hbox{\kern
193.65547pt\hbox{$\displaystyle{\sf G}\vdash{\sf
p}[\\![\,P\,]\\!]\mathrel{\|}{\sf q}[\\![\,Q\,]\\!]\mathrel{\|}{\sf
r}[\\![\,R\,]\\!]\mathrel{\|}\emptyset$}}}}$

Our type system enjoys the properties of Session Fidelity and Subject
Reduction. Moreover, it ensures the semantic property of Lock-freedom. Since
every participant can freely perform outputs, to prove this property we only
have to show that all inputs can be enabled. For lack of space we only give
the most interesting case in the proof of Subject Reduction.

######  Theorem 4.2 (Session Fidelity)

If ${\sf G}\vdash{\mathbb{N}}\mathrel{\|}\mathcal{M}$ and ${\sf
G}\mathrel{\|}\mathcal{M}\xrightarrow{\beta}{\sf
G}^{\prime}\mathrel{\|}\mathcal{M}^{\prime}$, then
${\mathbb{N}}\mathrel{\|}\mathcal{M}\xrightarrow{\beta}{\mathbb{N}}^{\prime}\mathrel{\|}\mathcal{M}^{\prime}$
and ${\sf
G}^{\prime}\vdash{\mathbb{N}}^{\prime}\mathrel{\|}\mathcal{M}^{\prime}$.

######  Theorem 4.3 (Subject Reduction)

If ${\sf G}\vdash{\mathbb{N}}\mathrel{\|}\mathcal{M}$ and
${\mathbb{N}}\mathrel{\|}\mathcal{M}\xrightarrow{\beta}{\mathbb{N}}^{\prime}\mathrel{\|}\mathcal{M}^{\prime}$,
then ${\sf G}\mathrel{\|}\mathcal{M}\xrightarrow{\beta}{\sf
G}^{\prime}\mathrel{\|}\mathcal{M}^{\prime}$ and ${\sf
G}^{\prime}\vdash{\mathbb{N}}^{\prime}\mathrel{\|}\mathcal{M}^{\prime}$.

######  Proof 4.4.

The proof is by induction on $d={\sf depth}({\sf G},{\sf p})$ where ${\sf
p}={\sf play}(\beta)$. Notice that
${\mathbb{N}}\mathrel{\|}\mathcal{M}\xrightarrow{\beta}{\mathbb{N}}^{\prime}\mathrel{\|}\mathcal{M}^{\prime}$
implies ${\sf p}\in{\sf Players}({\mathbb{N}})$, which together with ${\sf
G}\vdash{\mathbb{N}}\mathrel{\|}\mathcal{M}$ implies ${\sf p}\in{\sf
Players}({\sf G})$. Then $d>0$. Moreover $d$ is finite since ${\sf G}$ is
bounded.
Let $d>1$ and ${\sf G}={\sf r}?\\{{\sf q}_{i}.\ell_{i};{\sf G}_{i}\\}_{i\in
I}$ with ${\sf r}\neq{\sf p}$. Since ${\sf
G}\vdash{\mathbb{N}}\mathrel{\|}\mathcal{M}$ must be derived using Rule [In],
we get:

${\mathbb{N}}\equiv{\sf r}[\\![\,\Sigma_{h\in H}{\sf
q}_{h}?\ell_{h};R_{h}\,]\\!]\mathrel{\|}{\mathbb{N}}_{\\_}0$ ${\sf
G}_{\\_}{j}\vdash{\sf
r}[\\![\,R_{\\_}{j}\,]\\!]\mathrel{\|}{\mathbb{N}}_{\\_}0\mathrel{\|}\mathcal{M}_{\\_}{j}$
for all $j\in J$ ${\text{\Large{$\iota$}}({\sf G}_{\\_}j,\mathbb{M})}$ for all
$j\in J$

where $J={\sf rm}(\\{\langle{\sf q}_{\\_}i,\ell_{\\_}i,{\sf
p}\rangle\\}_{\\_}{i\in I},\mathcal{M})={\sf rm}(\\{\langle{\sf
q}_{\\_}h,\ell_{\\_}h,{\sf p}\rangle\\}_{\\_}{h\in H},\mathcal{M})$ and
$\mathcal{M}\equiv\langle{\sf q}_{\\_}{j},\ell_{\\_}{j},{\sf
r}\rangle\cdot\mathcal{M}_{\\_}{j}$ for all $j\in J$ and
$\mathbb{M}=\\{{\langle{\sf q}_{\\_}{l},\ell_{\\_}{l},{\sf r}\rangle}\mid
l\in(I\cup H)\setminus J\ \&\ {\sf q}_{\\_}l\neq{\sf q}_{\\_}j\ \forall j\in
J\\}$. The condition ${\sf r}\neq{\sf p}$ ensures that the transition
${\mathbb{N}}\mathrel{\|}\mathcal{M}\xrightarrow{\beta}{\mathbb{N}}^{\prime}\mathrel{\|}\mathcal{M}^{\prime}$
does not modify the process of participant ${\sf r}$ and does not dequeue any
message with receiver ${\sf r}$ from $\mathcal{M}$. Therefore we get
${\mathbb{N}}^{\prime}\equiv{\sf r}[\\![\,\Sigma_{h\in H}{\sf
q}_{h}?\ell_{h};R_{h}\,]\\!]\mathrel{\|}{\mathbb{N}}^{\prime}_{\\_}0$ and
$\mathcal{M}^{\prime}\equiv\langle{\sf q}_{\\_}{j},\ell_{\\_}{j},{\sf
r}\rangle\cdot\mathcal{M}^{\prime}_{\\_}{j}$ for all $j\in J$. Moreover the
transition can be done also if the process $\Sigma_{h\in H}{\sf
q}_{h}?\ell_{h};R_{h}$ is replaced by an arbitrary process and top messages
with receiver ${\sf r}$ are dequeued. Therefore

${\sf
r}[\\![\,R_{\\_}j\,]\\!]\mathrel{\|}{\mathbb{N}}_{\\_}0\mathrel{\|}\mathcal{M}_{\\_}j\xrightarrow{\beta}{\sf
r}[\\![\,R_{\\_}j\,]\\!]\mathrel{\|}{\mathbb{N}}_{\\_}0^{\prime}\mathrel{\|}\mathcal{M}^{\prime}_{\\_}j\text{
for all }j\in J$

It is easy to verify that ${\sf depth}({\sf G}_{\\_}j,{\sf p})<{\sf
depth}({\sf G},{\sf p})$. Then by induction we get ${\sf
G}_{\\_}j\mathrel{\|}\mathcal{M}_{\\_}j\xrightarrow{\beta}{\sf
G}_{\\_}j^{\prime}\mathrel{\|}\mathcal{M}_{\\_}j^{\prime}$ and ${\sf
G}^{\prime}_{\\_}j\vdash{\sf
r}[\\![\,R_{\\_}j\,]\\!]\mathrel{\|}{\mathbb{N}}^{\prime}_{\\_}0\mathrel{\|}\mathcal{M}_{\\_}j^{\prime}$
for all $j\in J$. Let ${\sf G}^{\prime}={\sf r}?\\{{\sf q}_{i}.\ell_{i};{\sf
G}^{\prime}_{i}\\}_{i\in I}$ where ${\sf G}^{\prime}_{\\_}l={\sf
G}_{\\_}{j_{\\_}0}$ for some $j_{\\_}0\in J$ and all $l\in I\backslash J$.
From ${\sf G}_{\\_}j\mathrel{\|}\mathcal{M}_{\\_}j\xrightarrow{\beta}{\sf
G}_{\\_}j^{\prime}\mathrel{\|}\mathcal{M}_{\\_}j^{\prime}$ we get ${\sf
G}_{\\_}j\mathrel{\|}\mathcal{M}\xrightarrow{\beta}{\sf
G}_{\\_}j^{\prime}\mathrel{\|}\mathcal{M}^{\prime}$ for all $j\in J$. Then we
derive ${\sf G}\mathrel{\|}\mathcal{M}\xrightarrow{\beta}{\sf
G}^{\prime}\mathrel{\|}\mathcal{M}^{\prime}$ by Rule [Inside-In]. The
condition ${\text{\Large{$\iota$}}({\sf G}_{\\_}j,\mathbb{M})}$ for all $j\in
J$ ensures that $\mathcal{M}^{\prime}$ cannot contain a message $\langle{\sf
q}_{\\_}k,\ell_{\\_}k,{\sf r}\rangle$ with $k\in(I\cup H)\setminus J$ and
${\sf q}_{\\_}k\neq{\sf q}_{\\_}j$ for all $j\in J$. The condition ${\sf
r}\neq{\sf p}$ ensures that the transition $\xrightarrow{\beta}$ cannot
dequeue a message with ${\sf r}$ as receiver. Hence ${\sf rm}(\\{\langle{\sf
q}_{\\_}h,\ell_{\\_}h,{\sf p}\rangle\\}_{\\_}{h\in
H},\mathcal{M}^{\prime})=J$. It is easy to verify that
${\text{\Large{$\iota$}}({\sf G}_{\\_}j,\mathbb{M})}$ implies
${\text{\Large{$\iota$}}({\sf G}^{\prime}_{\\_}j,\mathbb{M})}$ for all $j\in
J$. From ${\sf G}^{\prime}_{\\_}j\vdash{\sf
r}[\\![\,R_{\\_}j\,]\\!]\mathrel{\|}{\mathbb{N}}^{\prime}_{\\_}0\mathrel{\|}\mathcal{M}_{\\_}j^{\prime}$
for all $j\in J$ we get ${\sf Players}({\sf
G}^{\prime}_{\\_}{i})\setminus\\{{\sf r}\\}={\sf
Players}({\mathbb{N}}^{\prime}_{\\_}0)$ for all $i\in I$. Then all premises of
Rule [In] hold and we can derive ${\sf
G}^{\prime}\vdash{\mathbb{N}}^{\prime}\mathrel{\|}\mathcal{M}^{\prime}$.

######  Theorem 4.5 (Lock-freedom).

If ${\sf G}\vdash{\mathbb{N}}\mathrel{\|}\mathcal{M}$ and ${\sf
p}[\\![\,P\,]\\!]\in{\mathbb{N}}$, then
${\mathbb{N}}\mathrel{\|}\mathcal{M}\xrightarrow{\tau\cdot\beta}$ with ${\sf
play}(\beta)={\sf p}$ for some $\tau$, $\beta$.

As expected, since queues in type configurations can arbitrarily grow, our
type system is undecidable.

######  Theorem 4.6 (Undecidability).

Typing is undecidable.

In order to recover from this undecidability result, we can define an
inductive version of typing, thus obtaining a sound algorithm. This inductive
definition follows the standard pattern to deal with regular structures for
global types, and it requires the same queue at the beginning and at the end
of each cycle.

##  5 Related Work and Conclusion

We proposed flexible choice operators for an asynchronous multiparty session
calculus, in order to ensure the classical session correctness properties for
a larger class of protocols than is usually done. Several other proposals for
relaxing the constraints of the original choice operator of [12] were already
mentioned in Section 1. We now discuss some of them in more detail.

In [4], which builds on [14], we pushed this flexibility even further by
allowing input choices with different senders in processes, without
restrictions. The same approach was followed in [6]. However, this liberal
approach turned out to be incorrect, as pointed out in [11], as it allows the
following (synchronous) network to be typed, while it is not deadlock-free.
Indeed, this network can reach a deadlock if ${\sf p}$ chooses its second
branch, leading both ${\sf s}$ and ${\sf t}$ to choose their second branch
too. Then, if ${\sf r}$ chooses its first branch, it will be unable to
complete it.

$\begin{array}[]{c}{\sf p}[\\![\,({\sf s}!a;{\sf t}!a;{\sf r}!d)\oplus({\sf
s}!b;{\sf t}!b)\,]\\!]\mathrel{\|}{\sf r}[\\![\,({\sf s}?c;{\sf t}?e;{\sf
p}?d)+({\sf t}?e;{\sf s}?c)\,]\\!]\mathrel{\|}\\\ {\sf s}[\\![\,({\sf
p}?a;{\sf r}!c)+({\sf p}?b;{\sf r}!c)\,]\\!]\mathrel{\|}{\sf t}[\\![\,({\sf
p}?a;{\sf r}!e)+({\sf p}?b;{\sf r}!e)\,]\\!]\end{array}$

In fact, this session is not race-free according to the _race-freedom_
condition proposed in [11]. Note that the asynchronous session obtained by
composing this network with the empty queue is not typable in our type system.
Indeed, its typability would contradict Subject Reduction or Lock-freedom,
since it has the derivative ${\sf r}[\\![\,{\sf
p}?d\,]\\!]\mathrel{\|}\emptyset$ which is stuck. This session cannot be typed
in [15] either, since participant ${\sf r}$ does not satisfy the required
well-formedness conditions. Also the type system of [18] rejects this session,
the reason being that participant ${\sf r}$ can read the same message in more
than one branch. More precisely, participant ${\sf r}$ can read the message
$c$ from participant ${\sf s}$ and the message $e$ from participant ${\sf t}$
in both branches. This control is realised by annotating projections with the
set of available messages. We take advantage of queues in type configurations
for a similar but less refined control, which uses the predicate ensuring that
a global type is inactive for a given set of messages.

As future work, we plan to investigate three different variations of our
typing. The first one would be a weakening of condition
${\text{\Large{$\iota$}}({\sf G},\mathbb{M})}$ in Rule [In], taking into
account the order of sent messages and the expected inputs. The second one
would be a strengthening of our typing in order to forbid orphan messages. The
last one would be a weakening of our typing in order to allow optional
participants in the branches of choices, possibly using connecting
communications as in [14, 4].

Another direction that would be worth investigating is the relationship
between our approach and input races for sessions based on Classical Linear
Logic, see [16, 19].

To make our type system more efficient we will design two algorithms, taking
inspiration from [8], one for inferring global types for networks and the
other one for checking the correctness of global types for queues, allowing
also cycles in which queues increase.

Acknowledgments This paper came into being thanks to Ross Horne, who pointed
out to us the example reported in the Conclusion. We are indebted to him for
many interesting discussions on this subject and for suggestions on a previous
version of this paper. We also thank the anonymous referees for helpful
comments.

## References

  * [1]
  * [2] Marco Carbone, Nobuko Yoshida & Kohei Honda (2009): _Asynchronous Session Types: Exceptions and Multiparty Interactions_.  In Marco Bernardo, Luca Padovani & Gianluigi Zavattaro, editors: Formal Methods for Web Services, LNCS 5569, Springer, pp. 187–212, 10.1007/978-3-642-01918-0_5.
  * [3] Giuseppe Castagna, Mariangiola Dezani-Ciancaglini & Luca Padovani (2012): _On Global Types and Multi-Party Sessions_.  Logical Methods in Computer Science 8, pp. 1–45, 10.2168/LMCS-8(1:24)2012.
  * [4] Ilaria Castellani, Mariangiola Dezani-Ciancaglini & Paola Giannini (2019): _Reversible Sessions with Flexible Choices_.  Acta Informatica 56(7), pp. 553–583, 10.1007/s00236-019-00332-y.
  * [5] Ilaria Castellani, Mariangiola Dezani-Ciancaglini & Paola Giannini (2021): _Global types and event structure semantics for asynchronous multiparty sessions_.  CoRR abs/2102.00865, 10.48550/arXiv.2102.00865.
  * [6] Ilaria Castellani, Mariangiola Dezani-Ciancaglini, Paola Giannini & Ross Horne (2020): _Global Types with Internal Delegation_.  Theoretical Computer Science 807, pp. 128–153, 10.1016/j.tcs.2019.09.027.
  * [7] Bruno Courcelle (1983): _Fundamental Properties of Infinite Trees_.  Theoretical Computer Science 25, pp. 95–169, 10.1016/0304-3975(83)90059-2.
  * [8] Francesco Dagnino, Paola Giannini & Mariangiola Dezani-Ciancaglini (2021): _Deconfined Global Types for Asynchronous Sessions_.  CoRR abs/2111.11984, 10.48550/arXiv.2111.11984.
  * [9] Romain Demangeon & Kohei Honda (2012): _Nested Protocols in Session Types_.  In Maciej Koutny & Irek Ulidowski, editors: CONCUR, LNCS 7454, Springer, pp. 272–286, 10.1007/978-3-642-32940-1_20.
  * [10] Pierre-Malo Deniélou & Nobuko Yoshida (2012): _Multiparty Session Types Meet Communicating Automata_.  In Helmut Seidl, editor: ESOP, LNCS 7211, Springer, pp. 194–213, 10.1007/978-3-642-28869-2_10.
  * [11] Rob van Glabbeek, Peter Höfner & Ross Horne (2021): _Assuming Just Enough Fairness to make Session Types Complete for Lock-freedom_.  In Leonid Libkin, editor: LICS, ACM Press, pp. 1–13, 10.1109/LICS52264.2021.9470531.
  * [12] Kohei Honda, Nobuko Yoshida & Marco Carbone (2008): _Multiparty Asynchronous Session Types_.  In George C. Necula & Philip Wadler, editors: POPL, ACM Press, pp. 273–284, 10.1145/1328438.1328472.
  * [13] Kohei Honda, Nobuko Yoshida & Marco Carbone (2016): _Multiparty Asynchronous Session Types_.  Journal of ACM 63(1), pp. 9:1–9:67, 10.1145/2827695.
  * [14] Raymond Hu & Nobuko Yoshida (2017): _Explicit Connection Actions in Multiparty Session Types_.  In Marieke Huisman & Julia Rubin, editors: FASE, LNCS 10202, Springer, pp. 116–133, 10.1007/978-3-662-54494-5_7.
  * [15] Sung-Shik Jongmans & Nobuko Yoshida (2020): _Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types_.  In Peter Müller, editor: ESOP, LNCS 12075, Springer, pp. 251–279, 10.1007/978-3-030-44914-8_10.
  * [16] Wen Kokke, J. Garrett Morris & Philip Wadler (2020): _Towards Races in Linear Logic_.  Logical Methods in Computer Science 16(4), 10.23638/LMCS-16(4:15)2020.
  * [17] Julien Lange, Emilio Tuosto & Nobuko Yoshida (2015): _From Communicating Machines to Graphical Choreographies_.  In Sriram K. Rajamani & David Walker, editors: POPL, ACM Press, pp. 221–232, 10.1145/2676726.2676964.
  * [18] Rupak Majumdar, Madhavan Mukund, Felix Stutz & Damien Zufferey (2021): _Generalising Projection in Asynchronous Multiparty Session Types_.  In Serge Haddad & Daniele Varacca, editors: CONCUR, LIPIcs 203, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 35:1–35:24, 10.4230/LIPIcs.CONCUR.2021.35.
  * [19] Zesen Qian, G. A. Kavvos & Lars Birkedal (2021): _Client-server sessions in linear logic_.  Proc. ACM Program. Lang. 5(ICFP), pp. 1–31, 10.1145/3473567.