Ugo de’Liguoro and Luca Padovani John Q. Open and Joan R. Acces 2 42nd
Conference on Very Important Topics (CVIT 2016) CVIT 2016 CVIT 2016 December
24–27, 2016 Little Whinging, United Kingdom 42 23

# Mailbox Types for Unordered Interactions

Ugo de’Liguoro  Università di Torino, Dipartimento di Informatica, Torino,
Italy  Luca Padovani  Università di Torino, Dipartimento di Informatica,
Torino, Italy

###### Abstract.

We propose a type system for reasoning on protocol conformance and deadlock
freedom in networks of processes that communicate through unordered mailboxes.
We model these networks in the mailbox calculus, a mild extension of the
asynchronous $\pi$-calculus with first-class mailboxes and selective input.
The calculus subsumes the actor model and allows us to analyze networks with
dynamic topologies and varying number of processes possibly mixing different
concurrency abstractions. Well-typed processes are deadlock free and never
fail because of unexpected messages. For a non-trivial class of them, junk
freedom is also guaranteed. We illustrate the expressiveness of the calculus
and of the type system by encoding instances of non-uniform, concurrent
objects, binary sessions extended with joins and forks, and some known actor
benchmarks.

###### Key words and phrases:

actors, concurrent objects, first-class mailboxes, unordered communication
protocols, behavioral types, protocol conformance, deadlock freedom, junk
freedom

###### 1991 Mathematics Subject Classification:

D.1.3 Concurrent Programming; D.3.3 Language Constructs and Features
(_Concurrent programming structures, Input/output_); F.1.2 Modes of
Computation (_Parallelism and concurrency_); F.3.3 Studies of Program
Constructs (_Type structure_).

##  1\. Introduction

Message passing is a key mechanism used to coordinate concurrent processes.
The order in which a process consumes messages may coincide with the order in
which they arrive at destination (_ordered processing_) or may depend on some
intrinsic property of the messages themselves, such as their priority, their
tag, or the shape of their content (_out-of-order or selective processing_).
Ordered message processing is common in networks of processes connected by
point-to-point _channels_. Out-of-order message processing is common in
networks of processes using _mailboxes_ , into which processes concurrently
store messages and from which one process selectively receives messages. This
communication model is typically found in the various implementations of
actors [22, 1] such as Erlang [3], Scala and Akka actors [21], CAF [8] and
Kilim [45]. Non-uniform, concurrent objects [43, 41, 14] are also examples of
out-of-order message processors. For example, a busy lock postpones the
processing of any $\mathtt{\color[rgb]{0.3,0,0}acquire}$ message until it is
released by its current owner. Out-of-order message processing adds further
complexity to the challenging task of concurrent and parallel application
development: storing a message into the wrong mailbox or at the wrong time,
forgetting a message in a mailbox, or relying on the presence of a particular
message that is not guaranteed to be found in a mailbox are programming
mistakes that are easy to do and hard to detect without adequate support from
the language and its development tools.

⬇

1class Account(var balance: Double) extends ScalaActor[AnyRef] {

2 private val self = this

3 override def process(msg: AnyRef) {

4 msg match {

5 case dm: DebitMessage => \label{begin.account.debit}

6 balance += dm.amount

7 val sender = dm.sender.asInstanceOf[Account]

8 sender.send(ReplyMessage.ONLY) \label{end.account.debit}

9 case cm: CreditMessage => \label{begin.account.credit}

10 balance -= cm.amount

11 val sender = cm.sender.asInstanceOf[ScalaActor[AnyRef]]

12 val recipient = cm.recipient.asInstanceOf[Account]

13 recipient.send(new DebitMessage(self, cm.amount))
\label{account.credit.send}

14 receive { \label{account.credit.wait}

15 case rm: ReplyMessage =>

16 sender.send(ReplyMessage.ONLY)

17 } \label{end.account.credit}

18 case _: StopMessage => exit() \label{account.stop}

19 case message => \label{begin.account.unknown}

20 val ex = new IllegalArgumentException("Unsupported␣message")

21 ex.printStackTrace(System.err) \label{end.account.unknown}

22 }

23 }

24}

Listing 1: An example of Scala actor taken from the Savina benchmark suite
[27].

The Scala actor in Listing 1, taken from the Savina benchmark suite [27],
allows us to illustrate some of the subtle pitfalls that programmers must
carefully avoid when dealing with out-of-order message processing. The process
method matches messages found in the actor’s mailbox according to their type.
If a message of type DebitMessage is found, then balance is incremented by the
deposited amount and the actor requesting the operation is notified with a
ReplyMessage (lines LABEL:begin.account.debit–LABEL:end.account.debit). If a
message of type CreditMessage is found, balance is decremented by the amount
that is transferred to recipient (lines
LABEL:begin.account.credit–LABEL:account.credit.send). Since the operation is
meant to be atomic, the actor temporarily changes its behavior and waits for a
ReplyMessage from recipient signalling that the transfer is complete, before
notifying sender in turn (lines
LABEL:account.credit.wait–LABEL:end.account.credit). A message of type
StopMessage terminates the actor (line LABEL:account.stop).

Note how the correct execution of this code depends on some key assumptions:

  * •

ReplyMessage should be stored in the actor’s mailbox only when the actor is
involved in a transaction, or else the message would trigger the “catch all”
clause that throws a “unsupported message” exception (lines
LABEL:begin.account.unknown–LABEL:end.account.unknown).

  * •

No debit or credit message should be in the actor’s mailbox by the time it
receives StopMessage, or else some critical operations affecting the balance
would not be performed.

  * •

Two distinct accounts should not try to simultaneously initiate a transaction
with each other. If this were allowed, each account could consume the credit
message found in its own mailbox and then deadlock waiting for a reply from
the other account (lines LABEL:account.credit.wait–LABEL:end.account.credit).

Static analysis techniques that certify the validity of assumptions like these
can be valuable for developers. For example, session types [25] have proved to
be an effective formalism for the enforcement of communication protocols and
have been applied to a variety of programming paradigms and languages [2],
including those based on mailbox communications [35, 7, 16, 37]. However,
session types are specifically designed to address point-to-point, ordered
interactions over channels [23]. Retrofitting them to a substantially
different communication model calls for some inevitable compromises on the
network topologies that can be addressed and forces programmers to give up
some of the flexibility offered by unordered message processing.

Another aspect that complicates the analysis of actor systems is that the pure
actor model as it has been originally conceived [22, 1] does not accurately
reflect the actual practice of actor programming. In the pure actor model,
each actor owns a single mailbox and the only synchronization mechanism is
message reception from such mailbox. However, it is a known fact that the
implementation of complex coordination protocols in the pure actor model is
challenging [47, 46, 28, 9]. These difficulties have led programmers to mix
the actor model with different concurrency abstractions [26, 46], to extend
actors with controlled forms of synchronization [47] and to consider actors
with multiple/first-class mailboxes [20, 28, 9]. In fact, popular
implementations of the actor model feature disguised instances of
multiple/first-class mailbox usage, even if they are not explicitly presented
as such: in Akka, the messages that an actor is unable to process immediately
can be temporarily stashed into a different mailbox [20]; in Erlang, hot code
swapping implies transferring at runtime the input capability on a mailbox
from a piece of code to a different one [3].

In summary, there is still a considerable gap between the scope of available
approaches used to analyze mailbox-based communicating systems and the array
of features used in programming these systems. To help narrowing this gap, we
make the following contributions:

  * •

We introduce _mailbox types_ , a new kind of behavioral types with a simple
and intuitive semantics embodying the unordered nature of mailboxes. Mailbox
types allow us to describe mailboxes subject to selective message processing
as well as mailboxes concurrently accessed by several processes. Incidentally,
mailbox types also provide precise information on the size and reachability of
mailboxes that may lead to valuable code optimizations.

  * •

We develop a mailbox type system for the _mailbox calculus_ , a mild extension
of the asynchronous $\pi$-calculus [44] featuring tagged messages, selective
inputs and first-class mailboxes. The mailbox calculus allows us to address a
broad range of systems with dynamic topology and varying number of processes
possibly using a mixture of concurrency models (including multi-mailbox
actors) and abstractions (such as locks and futures).

  * •

We prove three main properties of well-typed processes: the absence of
failures due to unexpected messages (_mailbox conformance_); the absence of
pending activities and messages in irreducible processes (_deadlock freedom_);
for a non-trivial class of processes, the guarantee that every message can be
eventually consumed (_junk freedom_).

  * •

We illustrate the expressiveness of mailbox types by presenting well-typed
encodings of known concurrent objects (locks and futures) and actor benchmarks
(atomic transactions and master-workers parallelism) and of binary sessions
extended with forks and joins. In discussing these examples, we emphasize the
impact of out-of-order message processing and of first-class mailboxes.

#### Structure of the paper.

We start from the definition of the _mailbox calculus_ and of the properties
we expect from well-typed processes (Section 2). We introduce mailbox types
(Section 3.1) and dependency graphs (Section 3.2) for tracking mailbox
dependencies in processes that use more than one. Then, we present the typing
rules (Section 3.3) and the soundness results of the type system (Section
3.4). In the latter part of the paper, we discuss a few more complex examples
(Section 4), related work (Section 5) and ideas for further developments
(Section 6). Additional definitions and proofs can be found in Appendices A–D.

##  2\. The Mailbox Calculus

$\begin{array}[t]{@{}rr@{~}c@{~}ll@{}}\textbf{Process}&P,Q\leavevmode\nobreak\
&::=\hfil\leavevmode\nobreak\
&\mathtt{\color[rgb]{0,0,0.6}done}&\text{(termination)}\\\
&\leavevmode\nobreak\ &|\hfil\leavevmode\nobreak\
&\mathsf{\color[rgb]{0,0.2,0}X}{}[\overline{u}]&\text{(invocation)}\\\
&\leavevmode\nobreak\ &|\hfil\leavevmode\nobreak\ &G&\text{(guarded
process)}\\\ &\leavevmode\nobreak\ &|\hfil\leavevmode\nobreak\
&u\texttt{!}\mathtt{\color[rgb]{0.3,0,0}m}{}[\overline{v}]&\text{(stored
message)}\\\ &\leavevmode\nobreak\ &|\hfil\leavevmode\nobreak\
&P\mathbin{\texttt{|}}Q&\text{(parallel composition)}\\\ &\leavevmode\nobreak\
&|\hfil\leavevmode\nobreak\ &(\nu a)P&\text{(mailbox restriction)}\\\ \\\
\textbf{Guard}&G,H\leavevmode\nobreak\ &::=\hfil\leavevmode\nobreak\
&\mathtt{\color[rgb]{0,0,0.6}fail}\leavevmode\nobreak\ u&\text{(runtime
error)}\\\ &\leavevmode\nobreak\ &|\hfil\leavevmode\nobreak\
&\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
u\texttt{.}P&\text{(mailbox deletion)}\\\ &\leavevmode\nobreak\
&|\hfil\leavevmode\nobreak\
&u\texttt{?}\mathtt{\color[rgb]{0.3,0,0}m}(\overline{\mathit{x}})\texttt{.}P&\text{(selective
receive)}\\\ &\leavevmode\nobreak\ &|\hfil\leavevmode\nobreak\
&G+H&\text{(guard composition)}\end{array}$ Table 1.  Syntax of the mailbox
calculus.

We assume given an infinite set of _variables_ $\mathit{x}$, $\mathit{y}$, an
infinite set of _mailbox names_ $a$, $b$, a set of _tags_
$\mathtt{\color[rgb]{0.3,0,0}m}$ and a finite set of _process variables_
$\mathsf{\color[rgb]{0,0.2,0}X}$. We let $u$, $v$ range over variables and
mailbox names without distinction. Throughout the paper we write
$\overline{e}$ for possibly empty sequences $e_{1},\dots,e_{n}$ of various
entities. For example, $\overline{u}$ stands for a sequence
$u_{1},\dots,u_{n}$ of names and $\\{\overline{u}\\}$ for the corresponding
set.

The syntax of the _mailbox calculus_ is shown in Table 1. The term
$\mathtt{\color[rgb]{0,0,0.6}done}$ represents the terminated process that
performs no action. The term
$u\texttt{!}\mathtt{\color[rgb]{0.3,0,0}m}{}[\overline{v}]$ represents a
message stored in mailbox $u$. The message has tag
$\mathtt{\color[rgb]{0.3,0,0}m}$ and arguments $\overline{v}$. The term
$P\mathbin{\texttt{|}}Q$ represents the parallel composition of $P$ and $Q$
and $(\nu a)P$ represents a restricted mailbox $a$ with scope $P$. The term
$\mathsf{\color[rgb]{0,0.2,0}X}{}[\overline{u}]$ represents the invocation of
the process named $\mathsf{\color[rgb]{0,0.2,0}X}$ with parameters
$\overline{u}$. For each process variable $\mathsf{\color[rgb]{0,0.2,0}X}$ we
assume that there is a corresponding _global process definition_ of the form
$\mathsf{\color[rgb]{0,0.2,0}X}(\overline{\mathit{x}})\triangleq P$. A guarded
process $G$ is a composition of actions. The action
$\mathtt{\color[rgb]{0,0,0.6}fail}\leavevmode\nobreak\ u$ represents the
process that fails with an error for having received an unexpected message
from mailbox $u$. The action
$\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\ u\texttt{.}P$
represents the process that deletes the mailbox $u$ if it is empty and then
continues as $P$. The action
$u\texttt{?}\mathtt{\color[rgb]{0.3,0,0}m}(\overline{\mathit{x}})\texttt{.}P$
represents the process that receives an
$\mathtt{\color[rgb]{0.3,0,0}m}$-tagged message from mailbox $u$ then
continues as $P$ with $\overline{\mathit{x}}$ replaced by the message’s
arguments. A compound guard $G+H$ offers all the actions offered by $G$ and
$H$. We assume that all actions in the same guard refer to the same mailbox
$u$. The notions of free and bound names of a process $P$ are standard and
respectively denoted by $\mathsf{fn}(P)$ and $\mathsf{bn}(P)$.

The operational semantics of the mailbox calculus is mostly conventional. We
use the structural congruence relation $\equiv$ defined below to rearrange
equivalent processes:

$\begin{array}[]{@{}*{3}{r@{~}c@{~}l}@{}}\mathtt{\color[rgb]{0,0,0.6}fail}\leavevmode\nobreak\
a+G\leavevmode\nobreak\ &\equiv\hfil\leavevmode\nobreak\
&G&G+H\leavevmode\nobreak\ &\equiv\hfil\leavevmode\nobreak\
&H+G&G+(H+H^{\prime})\leavevmode\nobreak\ &\equiv\hfil\leavevmode\nobreak\
&(G+H)+H^{\prime}\\\
\mathtt{\color[rgb]{0,0,0.6}done}\mathbin{\texttt{|}}P\leavevmode\nobreak\
&\equiv\hfil\leavevmode\nobreak\ &P&P\mathbin{\texttt{|}}Q\leavevmode\nobreak\
&\equiv\hfil\leavevmode\nobreak\
&Q\mathbin{\texttt{|}}P&P\mathbin{\texttt{|}}(Q\mathbin{\texttt{|}}R)\leavevmode\nobreak\
&\equiv\hfil\leavevmode\nobreak\
&(P\mathbin{\texttt{|}}Q)\mathbin{\texttt{|}}R\\\ \leavevmode\nobreak\
&\hfil\leavevmode\nobreak\ &&(\nu a)(\nu b)P\leavevmode\nobreak\
&\equiv\hfil\leavevmode\nobreak\ &(\nu b)(\nu a)P&(\nu
a)P\mathbin{\texttt{|}}Q\leavevmode\nobreak\ &\equiv\hfil\leavevmode\nobreak\
&(\nu a)(P\mathbin{\texttt{|}}Q)\quad\text{if
$a\not\in\mathsf{fn}(Q)$}\end{array}$

Structural congruence captures the usual commutativity and associativity laws
of action and process compositions, with $\mathtt{\color[rgb]{0,0,0.6}fail}$
and $\mathtt{\color[rgb]{0,0,0.6}done}$ acting as the respective units.
Additionally, the order of mailbox restrictions is irrelevant and the scope of
a mailbox may shrink or extend dynamically. The reduction relation
$\rightarrow$ is inductively defined by the rules

$\begin{array}[]{rr@{~}c@{~}ll}\hypertarget{rule:r-read}{\text{\scriptsize[{r-read}]}}&a\texttt{!}\mathtt{\color[rgb]{0.3,0,0}m}{}[\overline{c}]\mathbin{\texttt{|}}a\texttt{?}\mathtt{\color[rgb]{0.3,0,0}m}(\overline{\mathit{x}})\texttt{.}P+G\leavevmode\nobreak\
&\rightarrow\hfil\leavevmode\nobreak\
&P\\{\overline{c}/\overline{\mathit{x}}\\}\\\
\hypertarget{rule:r-free}{\text{\scriptsize[{r-free}]}}&(\nu
a)(\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
a\texttt{.}P+G)\leavevmode\nobreak\ &\rightarrow\hfil\leavevmode\nobreak\
&P\\\
\hypertarget{rule:r-def}{\text{\scriptsize[{r-def}]}}&\mathsf{\color[rgb]{0,0.2,0}X}{}[\overline{c}]\leavevmode\nobreak\
&\rightarrow\hfil\leavevmode\nobreak\
&P\\{\overline{c}/\overline{\mathit{x}}\\}&\text{if
$\mathsf{\color[rgb]{0,0.2,0}X}(\overline{\mathit{x}})\triangleq P$}\\\
\hypertarget{rule:r-par}{\text{\scriptsize[{r-par}]}}&P\mathbin{\texttt{|}}R\leavevmode\nobreak\
&\rightarrow\hfil\leavevmode\nobreak\ &Q\mathbin{\texttt{|}}R&\text{if
$P\rightarrow Q$}\\\
\hypertarget{rule:r-new}{\text{\scriptsize[{r-new}]}}&(\nu
a)P\leavevmode\nobreak\ &\rightarrow\hfil\leavevmode\nobreak\ &(\nu
a)Q&\text{if $P\rightarrow Q$}\\\
\hypertarget{rule:r-struct}{\text{\scriptsize[{r-struct}]}}&P\leavevmode\nobreak\
&\rightarrow\hfil\leavevmode\nobreak\ &Q&\text{if $P\equiv
P^{\prime}\rightarrow Q^{\prime}\equiv Q$}\end{array}$

where $P\\{\overline{c}/\overline{\mathit{x}}\\}$ denotes the usual capture-
avoiding replacement of the variables $\overline{\mathit{x}}$ with the mailbox
names $\overline{c}$. Rule [r-read] models the selective reception of an
$\mathtt{\color[rgb]{0.3,0,0}m}$-tagged message from mailbox $a$, which erases
all the other actions of the guard. Rule [r-free] is triggered when the
process is ready to delete the empty mailbox $a$ and no more messages can be
stored in $a$ because there are no other processes in the scope of $a$. Rule
[r-def] models a process invocation by replacing the process variable
$\mathsf{\color[rgb]{0,0.2,0}X}$ with the corresponding definition. Finally,
rules [r-par], [r-new] and [r-struct] close reductions under parallel
compositions, name restrictions and structural congruence. We write
$\rightarrow^{*}$ for the reflexive and transitive closure of $\rightarrow$,
we write $P\arrownot\rightarrow^{*}Q$ if not $P\rightarrow^{*}Q$ and
$P\arrownot\rightarrow$ if $P\arrownot\rightarrow Q$ for all $Q$.

Hereafter, we will occasionally use numbers and conditionals in processes.
These and other features can be either encoded or added to the calculus
without difficulties.

######  Example 2.1 (lock).

In this example we model a lock as a process that waits for messages from a
$\mathit{self}$ mailbox in which acquisition and release requests are stored.
The lock is either free or busy. When in state free, the lock
nondeterministically consumes an $\mathtt{\color[rgb]{0.3,0,0}acquire}$
message from $\mathit{self}$. This message indicates the willingness to
acquire the lock by another process and carries a reference to a mailbox into
which the lock stores a $\mathtt{\color[rgb]{0.3,0,0}reply}$ notification.
When in state busy, the lock waits for a
$\mathtt{\color[rgb]{0.3,0,0}release}$ message indicating that it is being
released:

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\mathsf{\color[rgb]{0,0.2,0}FreeLock}(\mathit{self})\leavevmode\nobreak\
&\triangleq\hfil\leavevmode\nobreak\
&\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
\mathit{self}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}done}\\\
\leavevmode\nobreak\ &+\hfil\leavevmode\nobreak\
&\mathit{self}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}acquire}(\mathit{owner})\texttt{.}\mathsf{\color[rgb]{0,0.2,0}BusyLock}{}[\mathit{self},\mathit{owner}]\\\
\leavevmode\nobreak\ &+\hfil\leavevmode\nobreak\
&\mathit{self}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}release}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}fail}\leavevmode\nobreak\
\mathit{self}\\\
\mathsf{\color[rgb]{0,0.2,0}BusyLock}(\mathit{self},\mathit{owner})\leavevmode\nobreak\
&\triangleq\hfil\leavevmode\nobreak\
&\mathit{owner}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}reply}{}[\mathit{self}]\mathbin{\texttt{|}}\mathit{self}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}release}\texttt{.}\mathsf{\color[rgb]{0,0.2,0}FreeLock}{}[\mathit{self}]\end{array}$

Note the presence of the
$\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\ \mathit{self}$ guard in
the definition of $\mathsf{\color[rgb]{0,0.2,0}FreeLock}$ and the lack thereof
in $\mathsf{\color[rgb]{0,0.2,0}BusyLock}$. In the former case, the lock
manifests the possibility that no process is willing to acquire the lock, in
which case it deletes the mailbox and terminates. In the latter case, the lock
manifests its expectation to be eventually released by its current owner. Also
note that $\mathsf{\color[rgb]{0,0.2,0}FreeLock}$ fails if it receives a
$\mathtt{\color[rgb]{0.3,0,0}release}$ message. In this way, the lock
manifests the fact that it can be released only if it is currently owned by a
process. A system where two users $\mathit{alice}$ and $\mathit{carol}$
compete for acquiring $\mathit{lock}$ can be modeled as the process

$(\nu\mathit{lock})(\nu\mathit{alice})(\nu\mathit{carol})(\mathsf{\color[rgb]{0,0.2,0}FreeLock}{}[\mathit{lock}]\mathbin{\texttt{|}}\mathsf{\color[rgb]{0,0.2,0}User}{}[\mathit{alice},\mathit{lock}]\mathbin{\texttt{|}}\mathsf{\color[rgb]{0,0.2,0}User}{}[\mathit{carol},\mathit{lock}])$
(1)

where

$\mathsf{\color[rgb]{0,0.2,0}User}(\mathit{self},\mathit{lock})\triangleq\mathit{lock}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}acquire}{}[\mathit{self}]\mathbin{\texttt{|}}\mathit{self}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}reply}(l)\texttt{.}(l\texttt{!}\mathtt{\color[rgb]{0.3,0,0}release}{}\mathbin{\texttt{|}}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
\mathit{self}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}done})$

Note that $\mathsf{\color[rgb]{0,0.2,0}User}$ uses the reference $l$ – as
opposed to $\mathit{lock}$ – to release the acquired lock. As we will see in
Section 3.3, this is due to the fact that it is this particular reference to
the lock’s mailbox – and not $\mathit{lock}$ itself – that carries the
capability to release the lock. $\blacksquare$

######  Example 2.2 (future variable).

A future variable is a one-place buffer that stores the result of an
asynchronous computation. The content of the future variable is set once and
for all by the producer once the computation completes. This phase is
sometimes called _resolution_ of the future variable. After the future
variable has been resolved, its content can be retrieved any number of times
by the consumers. If a consumer attempts to retrieve the content of the future
variable beforehand, the consumer suspends until the variable is resolved. We
can model a future variable thus:

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\mathsf{\color[rgb]{0,0.2,0}Future}(\mathit{self})\leavevmode\nobreak\
&\triangleq\hfil\leavevmode\nobreak\
&\mathit{self}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}resolve}(\mathit{x})\texttt{.}\mathsf{\color[rgb]{0,0.2,0}Present}{}[\mathit{self},\mathit{x}]\\\
\mathsf{\color[rgb]{0,0.2,0}Present}(\mathit{self},\mathit{x})\leavevmode\nobreak\
&\triangleq\hfil\leavevmode\nobreak\
&\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
\mathit{self}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}done}\\\
\leavevmode\nobreak\ &+\hfil\leavevmode\nobreak\
&\mathit{self}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}get}(\mathit{sender})\texttt{.}(\mathit{sender}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}reply}{}[\mathit{x}]\mathbin{\texttt{|}}\mathsf{\color[rgb]{0,0.2,0}Present}{}[\mathit{self},\mathit{x}])\\\
\leavevmode\nobreak\ &+\hfil\leavevmode\nobreak\
&\mathit{self}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}resolve}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}fail}\leavevmode\nobreak\
\mathit{self}\end{array}$

The process $\mathsf{\color[rgb]{0,0.2,0}Future}$ represents an unresolved
future variable, which waits for a $\mathtt{\color[rgb]{0.3,0,0}resolve}$
message from the producer. Once the variable has been resolved, it behaves as
specified by $\mathsf{\color[rgb]{0,0.2,0}Present}$, namely it satisfies an
arbitrary number of $\mathtt{\color[rgb]{0.3,0,0}get}$ messages from consumers
but it no longer accepts $\mathtt{\color[rgb]{0.3,0,0}resolve}$ messages.
$\blacksquare$

######  Example 2.3 (bank account).

Below we see the process definition corresponding to the actor shown in
Listing 1. The structure of the term follows closely that of the Scala code:

$\begin{array}[]{@{}rcl@{}}\mathsf{\color[rgb]{0,0.2,0}Account}(\mathit{self},\mathit{balance})&\triangleq&\mathit{self}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}debit}(\mathit{amount},\mathit{sender})\texttt{.}\\\
&&\mathit{sender}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}reply}{}\mathbin{\texttt{|}}\mathsf{\color[rgb]{0,0.2,0}Account}{}[\mathit{self},\mathit{balance}+\mathit{amount}]\\\
&+&\mathit{self}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}credit}(\mathit{amount},\mathit{recipient},\mathit{sender})\texttt{.}\\\
&&\mathit{recipient}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}debit}{}[\mathit{amount},\mathit{self}]\mathbin{\texttt{|}}{}\\\
&&\mathit{self}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}reply}\texttt{.}(\mathit{sender}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}reply}{}\mathbin{\texttt{|}}\mathsf{\color[rgb]{0,0.2,0}Account}{}[\mathit{self},\mathit{balance}+\mathit{amount}])\\\
&+&\mathit{self}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}stop}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
\mathit{self}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}done}\\\
&+&\mathit{self}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}reply}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}fail}\leavevmode\nobreak\
\mathit{self}\end{array}$

The last term of the guarded process, which results in a failure, corresponds
to the catch-all clause in Listing 1 and models the fact that a
$\mathtt{\color[rgb]{0.3,0,0}reply}$ message is not expected to be found in
the account’s mailbox unless the account is involved in a transaction. The
$\mathtt{\color[rgb]{0.3,0,0}reply}$ message is received and handled
appropriately in the $\mathtt{\color[rgb]{0.3,0,0}credit}$-guarded term.

We can model a deadlock in the case two distinct bank accounts attempt to
initiate a transaction with one another. Indeed, we have

$\begin{array}[]{@{}l@{}}\mathsf{\color[rgb]{0,0.2,0}Account}{}[\mathit{alice},10]\mathbin{\texttt{|}}\mathit{alice}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}credit}{}[2,\mathit{carol},\mathit{bank}]\mathbin{\texttt{|}}{}\\\
\mathsf{\color[rgb]{0,0.2,0}Account}{}[\mathit{carol},15]\mathbin{\texttt{|}}\mathit{carol}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}credit}{}[5,\mathit{alice},\mathit{bank}]\end{array}\rightarrow^{*}\begin{array}[]{@{}l@{}}\mathit{carol}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}debit}{}[2,\mathit{alice}]\mathbin{\texttt{|}}\mathit{alice}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}reply}\dots\mathbin{\texttt{|}}{}\\\
\mathit{alice}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}debit}{}[5,\mathit{carol}]\mathbin{\texttt{|}}\mathit{carol}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}reply}\dots\end{array}$

where both $\mathit{alice}$ and $\mathit{carol}$ ignore the incoming
$\mathtt{\color[rgb]{0.3,0,0}debit}$ messages, whence the deadlock.
$\blacksquare$

We now provide operational characterizations of the properties enforced by our
typing discipline. We begin with mailbox conformance, namely the property that
a process never fails because of unexpected messages. To this aim, we define a
process context $\mathscr{C}$ as a process in which there is a single
occurrence of an _unguarded hole_ $[\leavevmode\nobreak\ ]$:

$\mathscr{C}\leavevmode\nobreak\ \leavevmode\nobreak\ ::=\leavevmode\nobreak\
\leavevmode\nobreak\ [\leavevmode\nobreak\ ]\leavevmode\nobreak\
\leavevmode\nobreak\ \mid\leavevmode\nobreak\ \leavevmode\nobreak\
\mathscr{C}\mathbin{\texttt{|}}P\leavevmode\nobreak\ \leavevmode\nobreak\
\mid\leavevmode\nobreak\ \leavevmode\nobreak\
P\mathbin{\texttt{|}}\mathscr{C}\leavevmode\nobreak\ \leavevmode\nobreak\
\mid\leavevmode\nobreak\ \leavevmode\nobreak\ (\nu a)\mathscr{C}$

The hole is “unguarded” in the sense that it does not occur prefixed by an
action. As usual, we write $\mathscr{C}[P]$ for the process obtained by
replacing the hole in $\mathscr{C}$ with $P$. Names may be captured by this
replacement. A mailbox conformant process never reduces to a state in which
the only action of a guard is $\mathtt{\color[rgb]{0,0,0.6}fail}$:

######  Definition 2.4.

We say that $P$ is _mailbox conformant_ if
$P\arrownot\rightarrow^{*}\mathscr{C}[\mathtt{\color[rgb]{0,0,0.6}fail}\leavevmode\nobreak\
a]$ for all $\mathscr{C}$ and $a$.

Looking at the placement of the
$\mathtt{\color[rgb]{0,0,0.6}fail}\leavevmode\nobreak\ u$ actions in earlier
examples we can give the following interpretations of mailbox conformance: a
lock is never released unless it has been acquired beforehand (Example 2.1); a
future variable is never resolved twice (Example 2.2); an account will not be
notified of a completed transaction (with a
$\mathtt{\color[rgb]{0.3,0,0}reply}$ message) unless it is involved in an
ongoing transaction (Example 2.3).

We express deadlock freedom as the property that all irreducible residuals of
a process are (structurally equivalent to) the terminated process:

######  Definition 2.5.

We say that $P$ is _deadlock free_ if $P\rightarrow^{*}Q\arrownot\rightarrow$
implies $Q\equiv\mathtt{\color[rgb]{0,0,0.6}done}$.

According to Definition 2.5, if a deadlock-free process halts we have that:
(1) there is no sub-process waiting for a message that is never produced; (2)
every mailbox is empty. Clearly, this is not the case for the transaction
between $\mathit{alice}$ and $\mathit{carol}$ in Example 2.3.

######  Example 2.6 (deadlock).

Below is another example of deadlocking process using
$\mathsf{\color[rgb]{0,0.2,0}Future}$ from Example 2.2, obtained by resolving
a future variable with the value it does not contain yet:

$(\nu\mathit{f})(\nu
c)(\mathsf{\color[rgb]{0,0.2,0}Future}{}[\mathit{f}]\mathbin{\texttt{|}}\mathit{f}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}get}{}[c]\mathbin{\texttt{|}}c\texttt{?}\mathtt{\color[rgb]{0.3,0,0}reply}(\mathit{x})\texttt{.}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
c\texttt{.}\mathit{f}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}put}{}[\mathit{x}])$
(2)

Notice that attempting to retrieve the content of a future variable not
knowing whether it has been resolved is legal. Indeed,
$\mathsf{\color[rgb]{0,0.2,0}Future}$ does not fail if a
$\mathtt{\color[rgb]{0.3,0,0}get}$ message is present in the future variable’s
mailbox before it is resolved. Thus, the deadlocked process above is mailbox
conformant but also an instance of undesirable process that will be ruled out
by our static analysis technique (_cf._ Example 3.14). We will need dependency
graphs in addition to types to flag this process as ill typed. $\blacksquare$

A property stronger than deadlock freedom is fair termination. A fairly
terminating process is a process whose residuals always have the possibility
to terminate. Formally:

######  Definition 2.7.

We say that $P$ is _fairly terminating_ if $P\rightarrow^{*}Q$ implies
$Q\rightarrow^{*}\mathtt{\color[rgb]{0,0,0.6}done}$.

An interesting consequence of fair termination is that it implies _junk
freedom_ (also known as lock freedom [29, 38]) namely the property that every
message can be eventually consumed. Our type system does not guarantee fair
termination nor junk freedom in general, but it does so for a non-trivial sub-
class of well-typed processes that we characterize later on.

##  3\. A Mailbox Type System

In this section we detail the type system for the mailbox calculus. We start
from the syntax and semantics of mailbox types (Section 3.1) and of dependency
graphs (Section 3.2), the mechanism we use to track mailbox dependencies. Then
we present the typing rules (Section 3.3) and the properties of well-typed
processes (Section 3.4).

###  3.1. Mailbox Types

$\begin{array}[]{rrcll}\textbf{Type}&\tau,\sigma&::=&\texttt{?}E&\text{(input)}\\\
&&|&\texttt{!}E&\text{(output)}\\\ \\\
\textbf{Pattern}&E,F&::=&\mathbb{0}&\text{(unreliable mailbox)}\\\
&&|&\mathbb{1}&\text{(empty mailbox)}\\\
&&|&\mathtt{\color[rgb]{0.3,0,0}m}{[}\overline{\tau}{]}&\text{(atom)}\\\
&&|&E+F&\text{(sum)}\\\ &&|&E\cdot F&\text{(product)}\\\
&&|&E^{\ast}&\text{(exponential)}\end{array}$ Table 2.  Syntax of mailbox
types and patterns.

The syntax of mailbox types and patterns is shown in Table 2. Patterns are
_commutative regular expressions_ [11] describing the configurations of
messages stored in a mailbox. An atom
$\mathtt{\color[rgb]{0.3,0,0}m}{[}\overline{\tau}{]}$ describes a mailbox
containing a single message with tag $\mathtt{\color[rgb]{0.3,0,0}m}$ and
arguments of type $\overline{\tau}$. We let $\mathtt{M}$ range over atoms and
abbreviate $\mathtt{\color[rgb]{0.3,0,0}m}{[}\overline{\tau}{]}$ with
$\mathtt{\color[rgb]{0.3,0,0}m}$ when $\overline{\tau}$ is the empty sequence.
Compound patterns are built using sum ($E+F$), product ($E\cdot F$) and
exponential ($E^{\ast}$). The constants $\mathbb{1}$ and $\mathbb{0}$
respectively describe the empty and the unreliable mailbox. There is no
configuration of messages stored in an unreliable mailbox, not even the empty
one. We will use the $\mathbb{0}$ pattern for describing mailboxes from which
an unexpected message has been received. Let us look at a few simple examples.
The pattern $\mathtt{\color[rgb]{0.3,0,0}A}+\mathtt{\color[rgb]{0.3,0,0}B}$
describes a mailbox that contains either an $\mathtt{\color[rgb]{0.3,0,0}A}$
message or a $\mathtt{\color[rgb]{0.3,0,0}B}$ message, but not both, whereas
the pattern $\mathtt{\color[rgb]{0.3,0,0}A}+\mathbb{1}$ describes a mailbox
that either contains a $\mathtt{\color[rgb]{0.3,0,0}A}$ message or is empty.
The pattern
$\mathtt{\color[rgb]{0.3,0,0}A}\cdot\mathtt{\color[rgb]{0.3,0,0}B}$ describes
a mailbox that contains both an $\mathtt{\color[rgb]{0.3,0,0}A}$ message and
also a $\mathtt{\color[rgb]{0.3,0,0}B}$ message. Note that
$\mathtt{\color[rgb]{0.3,0,0}A}$ and $\mathtt{\color[rgb]{0.3,0,0}B}$ may be
equal, in which case the mailbox contains _two_
$\mathtt{\color[rgb]{0.3,0,0}A}$ messages. Finally, the pattern
$\mathtt{\color[rgb]{0.3,0,0}A}^{\ast}$ describes a mailbox that contains an
arbitrary number (possibly zero) of $\mathtt{\color[rgb]{0.3,0,0}A}$ messages.

A _mailbox type_ consists of a _capability_ (either ? or !) paired with a
pattern. The capability specifies whether the pattern describes messages to be
received from (?) or stored in (!) the mailbox. Here are some examples: A
process using a mailbox of type $\texttt{!}\mathtt{\color[rgb]{0.3,0,0}A}$
_must_ store an $\mathtt{\color[rgb]{0.3,0,0}A}$ message into the mailbox,
whereas a process using a mailbox of type
$\texttt{?}\mathtt{\color[rgb]{0.3,0,0}A}$ is guaranteed to receive an
$\mathtt{\color[rgb]{0.3,0,0}A}$ message from the mailbox. A process using a
mailbox of type $\texttt{!}(\mathtt{\color[rgb]{0.3,0,0}A}+\mathbb{1})$ _may_
store an $\mathtt{\color[rgb]{0.3,0,0}A}$ message into the mailbox, but is not
obliged to do so. A process using a mailbox of type
$\texttt{!}(\mathtt{\color[rgb]{0.3,0,0}A}+\mathtt{\color[rgb]{0.3,0,0}B})$
decides whether to store an $\mathtt{\color[rgb]{0.3,0,0}A}$ message or a
$\mathtt{\color[rgb]{0.3,0,0}B}$ message in the mailbox, whereas a process
using a mailbox of type
$\texttt{?}(\mathtt{\color[rgb]{0.3,0,0}A}+\mathtt{\color[rgb]{0.3,0,0}B})$
must be ready to receive both kinds of messages. A process using a mailbox of
type
$\texttt{?}(\mathtt{\color[rgb]{0.3,0,0}A}\cdot\mathtt{\color[rgb]{0.3,0,0}B})$
is guaranteed to receive both an $\mathtt{\color[rgb]{0.3,0,0}A}$ message and
a $\mathtt{\color[rgb]{0.3,0,0}B}$ message and may decide in which order to do
so. A process using a mailbox of type
$\texttt{!}(\mathtt{\color[rgb]{0.3,0,0}A}\cdot\mathtt{\color[rgb]{0.3,0,0}B})$
must store both $\mathtt{\color[rgb]{0.3,0,0}A}$ and
$\mathtt{\color[rgb]{0.3,0,0}B}$ into the mailbox. A process using a mailbox
of type $\texttt{!}{\mathtt{\color[rgb]{0.3,0,0}A}^{\ast}}$ decides how many
$\mathtt{\color[rgb]{0.3,0,0}A}$ messages to store in the mailbox, whereas a
process using a mailbox of type
$\texttt{?}{\mathtt{\color[rgb]{0.3,0,0}A}^{\ast}}$ must be prepared to
receive an arbitrary number of $\mathtt{\color[rgb]{0.3,0,0}A}$ messages.

To cope with possibly infinite types we interpret the productions in Table 2
coinductively and consider as types the regular trees [12] built using those
productions. We require every infinite branch of a type tree to go through
infinitely many atoms. This strengthened contractiveness condition allows us
to define functions inductively on the structure of patterns, provided that
these functions do not recur into argument types (_cf._ Definitions 3.1 and
3.7).

The semantics of patterns is given in terms of sets of multisets of atoms.
Because patterns include types, the given semantics is parametric in the
subtyping relation, which will be defined next:

######  Definition 3.1 (subpattern).

The _configurations_ of $E$ are inductively defined by the following
equations, where $\mathsf{A}$ and $\mathsf{B}$ range over multisets
$\langle\overline{\mathtt{M}}\rangle$ of atoms and $\uplus$ denotes multiset
union:

$\begin{array}[c]{@{}r@{~}c@{~}l@{}}\llbracket\mathbb{0}\rrbracket\leavevmode\nobreak\
&\stackrel{{\scriptstyle\text{\tiny def}}}{{=}}\hfil\leavevmode\nobreak\
&\emptyset\\\ \llbracket\mathbb{1}\rrbracket\leavevmode\nobreak\
&\stackrel{{\scriptstyle\text{\tiny def}}}{{=}}\hfil\leavevmode\nobreak\
&\\{\langle\rangle\\}\end{array}\qquad\begin{array}[c]{@{}r@{~}c@{~}l@{}}\llbracket
E+F\rrbracket\leavevmode\nobreak\ &\stackrel{{\scriptstyle\text{\tiny
def}}}{{=}}\hfil\leavevmode\nobreak\ &\llbracket E\rrbracket\cup\llbracket
F\rrbracket\\\ \llbracket E\cdot F\rrbracket\leavevmode\nobreak\
&\stackrel{{\scriptstyle\text{\tiny def}}}{{=}}\hfil\leavevmode\nobreak\
&\\{\mathsf{A}\uplus\mathsf{B}\mid\mathsf{A}\in\llbracket
E\rrbracket,\mathsf{B}\in\llbracket
F\rrbracket\\}\end{array}\qquad\begin{array}[c]{@{}r@{~}c@{~}l@{}}\llbracket\mathtt{M}\rrbracket\leavevmode\nobreak\
&\stackrel{{\scriptstyle\text{\tiny def}}}{{=}}\hfil\leavevmode\nobreak\
&\\{\langle\mathtt{M}\rangle\\}\\\ \llbracket
E^{\ast}\rrbracket\leavevmode\nobreak\ &\stackrel{{\scriptstyle\text{\tiny
def}}}{{=}}\hfil\leavevmode\nobreak\
&\llbracket\mathbb{1}\rrbracket\cup\llbracket E\rrbracket\cup\llbracket E\cdot
E\rrbracket\cup\cdots\end{array}$

Given a preorder relation $\mathrel{\mathscr{R}}$ on types, we write
$E\sqsubseteq_{\mathrel{\mathscr{R}}}F$ if
$\langle\mathtt{\color[rgb]{0.3,0,0}m}_{i}{[}\overline{\tau}_{i}{]}\rangle_{i\in
I}\in\llbracket E\rrbracket$ implies
$\langle\mathtt{\color[rgb]{0.3,0,0}m}_{i}{[}\overline{\sigma}_{i}{]}\rangle_{i\in
I}\in\llbracket F\rrbracket$ and
$\overline{\tau}_{i}\mathrel{\mathscr{R}}\overline{\sigma}_{i}$ for every
$i\in I$. We write $\simeq_{\mathrel{\mathscr{R}}}$ for
${\sqsubseteq_{\mathrel{\mathscr{R}}}}\cap{\sqsupseteq_{\mathrel{\mathscr{R}}}}$.

For example,
$\llbracket\mathtt{\color[rgb]{0.3,0,0}A}+\mathtt{\color[rgb]{0.3,0,0}B}\rrbracket=\\{\langle\mathtt{\color[rgb]{0.3,0,0}A}\rangle,\langle\mathtt{\color[rgb]{0.3,0,0}B}\rangle\\}$
and
$\llbracket\mathtt{\color[rgb]{0.3,0,0}A}\cdot\mathtt{\color[rgb]{0.3,0,0}B}\rrbracket=\\{\langle\mathtt{\color[rgb]{0.3,0,0}A},\mathtt{\color[rgb]{0.3,0,0}B}\rangle\\}$.
It is easy to see that $\sqsubseteq_{\mathrel{\mathscr{R}}}$ is a pre-
congruence with respect to all the connectives and that it includes all the
known laws of commutative Kleene algebra [11]: both $+$ and $\cdot$ are
commutative and associative, $+$ is idempotent and has unit $\mathbb{0}$,
$\cdot$ distributes over $+$, it has unit $\mathbb{1}$ and is absorbed by
$\mathbb{0}$. Also observe that $\sqsubseteq_{\mathrel{\mathscr{R}}}$ is
related covariantly to $\mathrel{\mathscr{R}}$, that is
$\overline{\tau}\mathrel{\mathscr{R}}\overline{\sigma}$ implies
$\mathtt{\color[rgb]{0.3,0,0}m}{[}\overline{\tau}{]}\sqsubseteq_{\mathrel{\mathscr{R}}}\mathtt{\color[rgb]{0.3,0,0}m}{[}\overline{\sigma}{]}$.

We now define subtyping. As types may be infinite, we resort to coinduction:

######  Definition 3.2 (subtyping).

We say that $\mathrel{\mathscr{R}}$ is a _subtyping relation_ if
$\tau\mathrel{\mathscr{R}}\sigma$ implies either

  1. (1)

$\tau=\texttt{?}E$ and $\sigma=\texttt{?}F$ and
$E\sqsubseteq_{\mathrel{\mathscr{R}}}F$, or

  2. (2)

$\tau=\texttt{!}E$ and $\sigma=\texttt{!}F$ and
$F\sqsubseteq_{\mathrel{\mathscr{R}}}E$.

We write $\leqslant$ for the largest subtyping relation and say that $\tau$ is
a _subtype_ of $\sigma$ (and $\sigma$ a _supertype_ of $\tau$) if
$\tau\leqslant\sigma$. We write $\lessgtr$ for ${\leqslant}\cap{\geqslant}$,
$\sqsubseteq$ for $\sqsubseteq_{\leqslant}$ and $\simeq$ for
$\simeq_{\leqslant}$.

Items 1 and 2 respectively correspond to the usual covariant and contravariant
rules for channel types with input and output capabilities [40]. For example,
$\texttt{!}(\mathtt{\color[rgb]{0.3,0,0}A}+\mathtt{\color[rgb]{0.3,0,0}B})\leqslant\texttt{!}\mathtt{\color[rgb]{0.3,0,0}A}$
because a mailbox of type
$\texttt{!}(\mathtt{\color[rgb]{0.3,0,0}A}+\mathtt{\color[rgb]{0.3,0,0}B})$ is
more permissive than a mailbox of type
$\texttt{!}\mathtt{\color[rgb]{0.3,0,0}A}$. Dually,
$\texttt{?}\mathtt{\color[rgb]{0.3,0,0}A}\leqslant\texttt{?}(\mathtt{\color[rgb]{0.3,0,0}A}+\mathtt{\color[rgb]{0.3,0,0}B})$
because a mailbox of type $\texttt{?}\mathtt{\color[rgb]{0.3,0,0}A}$ provides
stronger guarantees than a mailbox of type
$\texttt{?}(\mathtt{\color[rgb]{0.3,0,0}A}+\mathtt{\color[rgb]{0.3,0,0}B})$.
Note that
$\texttt{!}(\mathtt{\color[rgb]{0.3,0,0}A}\cdot\mathtt{\color[rgb]{0.3,0,0}B})\lessgtr\texttt{!}(\mathtt{\color[rgb]{0.3,0,0}B}\cdot\mathtt{\color[rgb]{0.3,0,0}A})$
and
$\texttt{?}(\mathtt{\color[rgb]{0.3,0,0}A}\cdot\mathtt{\color[rgb]{0.3,0,0}B})\lessgtr\texttt{?}(\mathtt{\color[rgb]{0.3,0,0}B}\cdot\mathtt{\color[rgb]{0.3,0,0}A})$,
to witness the fact that the order in which messages are stored in a mailbox
is irrelevant.

Mailbox types whose patterns are in particular relations with the constants
$\mathbb{0}$ and $\mathbb{1}$ will play special roles, so we introduce some
corresponding terminology.

######  Definition 3.3 (type and name classification).

We say that (a name whose type is) $\tau$ is:

  * •

_relevant_ if $\tau\not\leqslant\texttt{!}\mathbb{1}$ and _irrelevant_
otherwise;

  * •

_reliable_ if $\tau\not\leqslant\texttt{?}\mathbb{0}$ and _unreliable_
otherwise;

  * •

_usable_ if $\texttt{!}\mathbb{0}\not\leqslant\tau$ and _unusable_ otherwise.

A relevant name _must_ be used, whereas an irrelevant name may be discarded
because not storing any message in the mailbox it refers to is allowed by its
type. All mailbox types with input capability are relevant. A reliable mailbox
is one from which no unexpected message has been received. All names with
output capability are reliable. A usable name _can_ be used, in the sense that
there exists a construct of the mailbox calculus that expects a name with that
type. All mailbox types with input capability are usable, but
$\texttt{?}(\mathtt{\color[rgb]{0.3,0,0}A}\cdot\mathbb{0})$ is unreliable.
Both $\texttt{!}\mathtt{\color[rgb]{0.3,0,0}A}$ and
$\texttt{!}(\mathbb{1}+\mathtt{\color[rgb]{0.3,0,0}A})$ are usable. The former
type is also relevant because a process using a mailbox with this type must
(eventually) store an $\mathtt{\color[rgb]{0.3,0,0}A}$ message in it. On the
contrary, the latter type is irrelevant, since not using the mailbox is a
legal way of using it.

Henceforth we assume that all types are usable and that all argument types are
also reliable. That is, we ban all types like $\texttt{!}\mathbb{0}$ or
$\texttt{!}(\mathbb{0}\cdot\mathtt{\color[rgb]{0.3,0,0}m})$ and all types like
$\texttt{?}\mathtt{\color[rgb]{0.3,0,0}m}{[}\texttt{?}\mathbb{0}{]}$ or
$\texttt{!}\mathtt{\color[rgb]{0.3,0,0}m}{[}\texttt{?}\mathbb{0}{]}$. Example
A.5 in Appendix A.1 discusses the technical motivation for these assumptions.

######  Example 3.4 (lock type).

The mailbox used by the lock (Example 2.1) will have several different types,
depending on the viewpoint we take (either the lock itself or one of its
users) and on the state of the lock (whether it is free or busy). As we can
see from the definition of $\mathsf{\color[rgb]{0,0.2,0}FreeLock}$, a free
lock waits for an $\mathtt{\color[rgb]{0.3,0,0}acquire}$ message which is
supposed to carry a reference to another mailbox into which the capability to
release the lock is stored. Since the lock is meant to have several concurrent
users, it is not possible in general to predict the number of
$\mathtt{\color[rgb]{0.3,0,0}acquire}$ messages in its mailbox. Therefore, the
mailbox of a free lock has type

$\texttt{?}\mathtt{\color[rgb]{0.3,0,0}acquire}{[}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}reply}{[}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}release}{]}{]}^{\ast}$

from the viewpoint of the lock itself. When the lock is busy, it expects to
find one $\mathtt{\color[rgb]{0.3,0,0}release}$ message in its mailbox, but in
general the mailbox will also contain $\mathtt{\color[rgb]{0.3,0,0}acquire}$
messages corresponding to pending acquisition requests. So, the mailbox of a
busy lock has type

$\texttt{?}(\mathtt{\color[rgb]{0.3,0,0}release}\cdot\mathtt{\color[rgb]{0.3,0,0}acquire}{[}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}reply}{[}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}release}{]}{]}^{\ast})$

indicating that the mailbox contains (or will eventually contain) a single
$\mathtt{\color[rgb]{0.3,0,0}release}$ message along with arbitrarily many
$\mathtt{\color[rgb]{0.3,0,0}acquire}$ messages.

Prospective owners of the lock may have references to the lock’s mailbox with
type
$\texttt{!}\mathtt{\color[rgb]{0.3,0,0}acquire}{[}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}reply}{[}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}release}{]}{]}$
or
$\texttt{!}\mathtt{\color[rgb]{0.3,0,0}acquire}{[}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}reply}{[}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}release}{]}{]}^{\ast}$
depending on whether they acquire the lock exactly once (just like
$\mathit{alice}$ and $\mathit{carol}$ in Example 2.1) or several times. Other
intermediate types are possible in the case of users that acquire the lock a
bounded number of times. The current owner of the lock will have a reference
to the lock’s mailbox of type
$\texttt{!}\mathtt{\color[rgb]{0.3,0,0}release}$. This type is relevant,
implying that the owner must eventually release the lock. $\blacksquare$

###  3.2. Dependency Graphs

We use _dependency graphs_ for tracking dependencies between mailboxes.
Intuitively, there is a dependency between $u$ and $v$ if either $v$ is the
argument of a message in mailbox $u$ or $v$ occurs in the continuation of a
process waiting for a message from $u$. Dependency graphs have names as
vertices and undirected edges. However, the usual representation of graphs
does not account for the fact that mailbox names may be restricted and that
the multiplicity of dependencies matters. Therefore, we define dependency
graphs using the syntax below:

$\textbf{Dependency Graph}\qquad\varphi,\psi\leavevmode\nobreak\
\leavevmode\nobreak\ ::=\leavevmode\nobreak\ \leavevmode\nobreak\
\emptyset\leavevmode\nobreak\ \leavevmode\nobreak\ \mid\leavevmode\nobreak\
\leavevmode\nobreak\ \\{u,v\\}\leavevmode\nobreak\ \leavevmode\nobreak\
\mid\leavevmode\nobreak\ \leavevmode\nobreak\
\varphi\sqcup\psi\leavevmode\nobreak\ \leavevmode\nobreak\
\mid\leavevmode\nobreak\ \leavevmode\nobreak\ (\nu a)\varphi$

The term $\emptyset$ represents the empty graph which has no vertices and no
edges. The unordered pair $\\{u,v\\}$ represents the graph made of a single
edge connecting the vertices $u$ and $v$. The term $\varphi\sqcup\psi$
represents the union of $\varphi$ and $\psi$ whereas $(\nu a)\varphi$
represents the same graph as $\varphi$ except that the vertex $a$ is
restricted. The usual notions of free and bound names apply to dependency
graphs. We write $\mathsf{fn}(\varphi)$ for the free names of $\varphi$.

$\begin{array}[]{@{}c@{}}{\hbox{$\displaystyle\vbox{\hbox{\hskip
29.07637pt\vbox{\vbox{}\hbox{\hskip-29.07635pt\hbox{\hbox{$\displaystyle\displaystyle\\{u,v\\}\xlongrightarrow{u-v}\emptyset$}}}}}}$}}\leavevmode\nobreak\
\leavevmode\nobreak\
\hypertarget{rule:g-axiom}{\text{\scriptsize[{g-axiom}]}}\qquad{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
21.20052pt\vbox{\hbox{\hskip-21.2005pt\hbox{\hbox{$\displaystyle\displaystyle\varphi\xlongrightarrow{u-v}\varphi^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
37.71437pt\vbox{\vbox{}\hbox{\hskip-37.71436pt\hbox{\hbox{$\displaystyle\displaystyle\varphi\sqcup\psi\xlongrightarrow{u-v}\varphi^{\prime}\sqcup\psi$}}}}}}$}}\leavevmode\nobreak\
\leavevmode\nobreak\
\hypertarget{rule:g-left}{\text{\scriptsize[{g-left}]}}\qquad{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
21.17276pt\vbox{\hbox{\hskip-21.17274pt\hbox{\hbox{$\displaystyle\displaystyle\psi\xlongrightarrow{u-v}\psi^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
38.82545pt\vbox{\vbox{}\hbox{\hskip-38.82544pt\hbox{\hbox{$\displaystyle\displaystyle\varphi\sqcup\psi\xlongrightarrow{u-v}\varphi\sqcup\psi^{\prime}$}}}}}}$}}\leavevmode\nobreak\
\leavevmode\nobreak\
\hypertarget{rule:g-right}{\text{\scriptsize[{g-right}]}}\\\ \\\
{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
47.27481pt\vbox{\hbox{\hskip-47.2748pt\hbox{\hbox{$\displaystyle\displaystyle\varphi\xlongrightarrow{u-v}\psi$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle a\neq
u,v$}}}}\vbox{}}}\over\hbox{\hskip
38.42015pt\vbox{\vbox{}\hbox{\hskip-38.42014pt\hbox{\hbox{$\displaystyle\displaystyle(\nu
a)\varphi\xlongrightarrow{u-v}(\nu a)\psi$}}}}}}$}}\leavevmode\nobreak\
\leavevmode\nobreak\
\hypertarget{rule:g-new}{\text{\scriptsize[{g-new}]}}\qquad{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
53.56624pt\vbox{\hbox{\hskip-53.56624pt\hbox{\hbox{$\displaystyle\displaystyle\varphi\xlongrightarrow{u-w}\psi$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\psi\xlongrightarrow{w-v}\varphi^{\prime}$}}}}\vbox{}}}\over\hbox{\hskip
21.20052pt\vbox{\vbox{}\hbox{\hskip-21.2005pt\hbox{\hbox{$\displaystyle\displaystyle\varphi\xlongrightarrow{u-v}\varphi^{\prime}$}}}}}}$}}\leavevmode\nobreak\
\leavevmode\nobreak\
\hypertarget{rule:g-trans}{\text{\scriptsize[{g-trans}]}}\end{array}$ Table 3.
Labelled transitions of dependency graphs.

To define the semantics of a dependency graph we use the labelled transition
system of Table 3. A label $u-v$ represents a path connecting $u$ with $v$.
So, a relation $\varphi\xlongrightarrow{u-v}\varphi^{\prime}$ means that $u$
and $v$ are connected in $\varphi$ and $\varphi^{\prime}$ describes the
residual edges of $\varphi$ that have not been used for building the path
between $u$ and $v$. The paths of $\varphi$ are built from the edges of
$\varphi$ (_cf._ [g-axiom]) connected by shared vertices (_cf._ [g-trans]).
Restricted names cannot be observed in labels, but they may contribute in
building paths in the graph (_cf._ [g-new]).

######  Definition 3.5 (graph acyclicity and entailment).

Let $\mathsf{dep}(\varphi)\stackrel{{\scriptstyle\text{\tiny
def}}}{{=}}\\{(u,v)\mid\exists\varphi^{\prime}:\varphi\xlongrightarrow{u-v}\varphi^{\prime}\\}$
be the _dependency relation_ generated by $\varphi$. We say that $\varphi$ is
_acyclic_ if $\mathsf{dep}(\varphi)$ is irreflexive. We say that $\varphi$
_entails_ $\psi$, written $\varphi\Rightarrow\psi$, if
$\mathsf{dep}(\psi)\subseteq\mathsf{dep}(\varphi)$.

Note that $\sqcup$ is commutative, associative and has $\emptyset$ as unit
with respect to $\mathsf{dep}(\cdot)$ (see Appendix A.2). These properties of
dependency graphs are key to prove that typing is preserved by structural
congruence on processes. Note also that $\sqcup$ is _not_ idempotent. Indeed,
$\\{u,v\\}\sqcup\\{u,v\\}$ is cyclic whereas $\\{u,v\\}$ is not. The following
example motivates the reason why the multiplicity of dependencies is
important.

######  Example 3.6.

Consider the reduction

$P\stackrel{{\scriptstyle\text{\tiny def}}}{{=}}(\nu a)(\nu
b)(a\texttt{!}\mathtt{\color[rgb]{0.3,0,0}A}{}[b]\mathbin{\texttt{|}}a\texttt{!}\mathtt{\color[rgb]{0.3,0,0}B}{}[b]\mathbin{\texttt{|}}a\texttt{?}\mathtt{\color[rgb]{0.3,0,0}A}(\mathit{x})\texttt{.}a\texttt{?}\mathtt{\color[rgb]{0.3,0,0}B}(\mathit{y})\texttt{.}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
a\texttt{.}\mathit{x}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}m}{}[\mathit{y}])\rightarrow^{*}(\nu
b)b\texttt{!}\mathtt{\color[rgb]{0.3,0,0}m}{}[b]\arrownot\rightarrow$

and observe that $P$ stores two messages in the mailbox $a$, each containing a
reference to the mailbox $b$. The two variables $\mathit{x}$ and $\mathit{y}$,
which were syntactically different in $P$, have been unified into $b$ in the
reduct, which is deadlocked. Unlike previous examples of deadlocked processes,
which resulted from mutual dependencies between different mailboxes, in this
case the deadlock is caused by the same dependency $\\{a,b\\}$ arising twice.
$\blacksquare$

###  3.3. Typing Rules

$\begin{array}[]{@{}c@{}}\lx@intercol\textbf{Typing rules for
processes}\hfill\framebox{$\Gamma\vdash P{}::\smash{\varphi}$}\hfil\\\ \\\
{\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
23.88887pt\vbox{\vbox{}\hbox{\hskip-23.88887pt\hbox{\hbox{$\displaystyle\displaystyle\emptyset\vdash\mathtt{\color[rgb]{0,0,0.6}done}{}::\emptyset$}}}}}}$}}\leavevmode\nobreak\
\leavevmode\nobreak\
\hypertarget{rule:t-done}{\text{\scriptsize[{t-done}]}}\qquad{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
22.29861pt\vbox{\hbox{\hskip-22.2986pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{\color[rgb]{0,0.2,0}X}:(\overline{\mathit{x}}:\overline{\tau};\varphi)$}}}\vbox{}}}\over\hbox{\hskip
38.40979pt\vbox{\vbox{}\hbox{\hskip-38.40977pt\hbox{\hbox{$\displaystyle\displaystyle\overline{u}:\overline{\tau}\vdash\mathsf{\color[rgb]{0,0.2,0}X}{}[\overline{u}]{}::\varphi\\{\overline{u}/\overline{\mathit{x}}\\}$}}}}}}$}}\leavevmode\nobreak\
\leavevmode\nobreak\
\hypertarget{rule:t-def}{\text{\scriptsize[{t-def}]}}\qquad{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
30.85988pt\vbox{\hbox{\hskip-30.85988pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,a:\texttt{?}\mathbb{1}\vdash
P{}::\varphi$}}}\vbox{}}}\over\hbox{\hskip
38.30379pt\vbox{\vbox{}\hbox{\hskip-38.30377pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash(\nu
a)P{}::(\nu a)\varphi$}}}}}}$}}\leavevmode\nobreak\ \leavevmode\nobreak\
\hypertarget{rule:t-new}{\text{\scriptsize[{t-new}]}}\\\ \\\
{\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
61.92029pt\vbox{\vbox{}\hbox{\hskip-61.92027pt\hbox{\hbox{$\displaystyle\displaystyle
u:\texttt{!}{\mathtt{\color[rgb]{0.3,0,0}m}{[}\overline{\tau}{]}},\overline{v}:\overline{\tau}\vdash
u\texttt{!}\mathtt{\color[rgb]{0.3,0,0}m}{}[\overline{v}]{}::\\{u,\\{\overline{v}\\}\\}$}}}}}}$}}\leavevmode\nobreak\
\leavevmode\nobreak\
\hypertarget{rule:t-msg}{\text{\scriptsize[{t-msg}]}}\qquad{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
46.90448pt\vbox{\hbox{\hskip-46.90446pt\hbox{\hbox{$\displaystyle\displaystyle
u:\texttt{?}E,\Gamma\vdash G$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\vDash
E$}}}}\vbox{}}}\over\hbox{\hskip
55.5794pt\vbox{\vbox{}\hbox{\hskip-55.57939pt\hbox{\hbox{$\displaystyle\displaystyle\textstyle
u:\texttt{?}E,\Gamma\vdash
G{}::\\{u,\mathsf{dom}(\Gamma)\\}$}}}}}}$}}\leavevmode\nobreak\
\leavevmode\nobreak\
\hypertarget{rule:t-guard}{\text{\scriptsize[{t-guard}]}}\\\ \\\
{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
33.20331pt\vbox{\hbox{\hskip-33.20331pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma_{i}\vdash
P_{i}{}::\varphi_{i}\leavevmode\nobreak\
{}^{(i=1,2)}$}}}\vbox{}}}\over\hbox{\hskip
45.94511pt\vbox{\vbox{}\hbox{\hskip-45.94511pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma_{1}\mathbin{\|}\Gamma_{2}\vdash
P_{1}\mathbin{\texttt{|}}P_{2}{}::\varphi_{1}\sqcup\varphi_{2}$}}}}}}$}}\leavevmode\nobreak\
\leavevmode\nobreak\
\hypertarget{rule:t-par}{\text{\scriptsize[{t-par}]}}\qquad{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
69.5919pt\vbox{\hbox{\hskip-69.5919pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash
P{}::\psi$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\leqslant\Delta$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\varphi\Rightarrow\psi$}}}}}\vbox{}}}\over\hbox{\hskip
20.30028pt\vbox{\vbox{}\hbox{\hskip-20.30026pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
P{}::\varphi$}}}}}}$}}\leavevmode\nobreak\ \leavevmode\nobreak\
\hypertarget{rule:t-sub}{\text{\scriptsize[{t-sub}]}}\\\ \\\
\lx@intercol\textbf{Typing rules for guards}\hfill\framebox{$\Gamma\vdash
G$}\hfil\\\ \\\ {\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
32.46066pt\vbox{\vbox{}\hbox{\hskip-32.46065pt\hbox{\hbox{$\displaystyle\displaystyle
u:\texttt{?}\mathbb{0},\Gamma\vdash\mathtt{\color[rgb]{0,0,0.6}fail}\leavevmode\nobreak\
u$}}}}}}$}}\leavevmode\nobreak\ \leavevmode\nobreak\
\hypertarget{rule:t-fail}{\text{\scriptsize[{t-fail}]}}\qquad{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
20.30028pt\vbox{\hbox{\hskip-20.30026pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
P{}::\varphi$}}}\vbox{}}}\over\hbox{\hskip
38.87906pt\vbox{\vbox{}\hbox{\hskip-38.87904pt\hbox{\hbox{$\displaystyle\displaystyle
u:\texttt{?}\mathbb{1},\Gamma\vdash\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
u\texttt{.}P$}}}}}}$}}\leavevmode\nobreak\ \leavevmode\nobreak\
\hypertarget{rule:t-free}{\text{\scriptsize[{t-free}]}}\\\ \\\
{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
40.33618pt\vbox{\hbox{\hskip-40.33617pt\hbox{\hbox{$\displaystyle\displaystyle
u:\texttt{?}E,\Gamma,\overline{\mathit{x}}:\overline{\tau}\vdash
P{}::\varphi$}}}\vbox{}}}\over\hbox{\hskip
60.06654pt\vbox{\vbox{}\hbox{\hskip-60.06654pt\hbox{\hbox{$\displaystyle\displaystyle
u:\texttt{?}(\mathtt{\color[rgb]{0.3,0,0}m}{[}\overline{\tau}{]}\cdot
E),\Gamma\vdash
u\texttt{?}\mathtt{\color[rgb]{0.3,0,0}m}(\overline{\mathit{x}})\texttt{.}P$}}}}}}$}}\leavevmode\nobreak\
\leavevmode\nobreak\
\hypertarget{rule:t-in}{\text{\scriptsize[{t-in}]}}\qquad{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
40.4193pt\vbox{\hbox{\hskip-40.41928pt\hbox{\hbox{$\displaystyle\displaystyle
u:\texttt{?}E_{i},\Gamma\vdash G_{i}\leavevmode\nobreak\
{}^{(i=1,2)}$}}}\vbox{}}}\over\hbox{\hskip
54.49132pt\vbox{\vbox{}\hbox{\hskip-54.4913pt\hbox{\hbox{$\displaystyle\displaystyle
u:\texttt{?}(E_{1}+E_{2}),\Gamma\vdash
G_{1}+G_{2}$}}}}}}$}}\leavevmode\nobreak\ \leavevmode\nobreak\
\hypertarget{rule:t-branch}{\text{\scriptsize[{t-branch}]}}\end{array}$ Table
4.  Typing rules.

We use _type environments_ for tracking the type of free names occurring in
processes. A type environment is a partial function from names to types
written as $\overline{u}:\overline{\tau}$ or
$u_{1}:\tau_{1},\dots,u_{n}:\tau_{n}$. We let $\Gamma$ and $\Delta$ range over
type environments, we write $\mathsf{dom}(\Gamma)$ for the domain of $\Gamma$
and $\Gamma,\Delta$ for the union of $\Gamma$ and $\Delta$ when
$\mathsf{dom}(\Gamma)\cap\mathsf{dom}(\Delta)=\emptyset$. We say that $\Gamma$
is reliable if so are all the types in its range.

Judgments for processes have the form $\Gamma\vdash P{}::\varphi$, meaning
that $P$ is well typed in $\Gamma$ and yields the dependency graph $\varphi$.
Judgments for guards have the form $\Gamma\vdash G$, meaning that $G$ is well
typed in $\Gamma$. We say that a judgment $\Gamma\vdash P{}::\varphi$ is well
formed if $\mathsf{fn}(\varphi)\subseteq\mathsf{dom}(\Gamma)$ and $\varphi$ is
acyclic. Each process typing rule has an implicit side condition requiring
that its conclusion is well formed. For each global process definition
$\mathsf{\color[rgb]{0,0.2,0}X}(\overline{\mathit{x}})\triangleq P$ we assume
that there is a corresponding _global process declaration_ of the form
$\mathsf{\color[rgb]{0,0.2,0}X}:(\overline{\mathit{x}}:\overline{\tau};\varphi)$.
We say that the definition is _consistent_ with the corresponding declaration
if $\overline{\mathit{x}}:\overline{\tau}\vdash P{}::\varphi$. Hereafter, all
process definitions are assumed to be consistent. We now discuss the typing
rules in detail, introducing auxiliary notions and notation as we go along.

#### Terminated process.

According to the rule [t-done], the terminated process
$\mathtt{\color[rgb]{0,0,0.6}done}$ is well typed in the empty type
environment and yields no dependencies. This is motivated by the fact that
$\mathtt{\color[rgb]{0,0,0.6}done}$ does not use any mailbox. Later on we will
introduce a subsumption rule [t-sub] that allows us to type
$\mathtt{\color[rgb]{0,0,0.6}done}$ in any type environment with irrelevant
names.

#### Message.

Rule [t-msg] establishes that a message
$u\texttt{!}\mathtt{\color[rgb]{0.3,0,0}m}{}[\overline{v}]$ is well typed
provided that the mailbox $u$ allows the storing of an
$\mathtt{\color[rgb]{0.3,0,0}m}$-tagged message with arguments of type
$\overline{\tau}$ and the types of $\overline{v}$ are indeed
$\overline{\tau}$. The subsumption rule [t-sub] will make it possible to use
arguments whose type is a _subtype_ of the expected ones. A message
$u\texttt{!}\mathtt{\color[rgb]{0.3,0,0}m}{}[\overline{v}]$ establishes
dependencies between the target mailbox $u$ and all of the arguments
$\overline{v}$. We write $\\{u,\\{v_{1},\dots,v_{n}\\}\\}$ for the dependency
graph $\\{u,v_{1}\\}\sqcup\cdots\sqcup\\{u,v_{n}\\}$ and use $\emptyset$ for
the empty graph union.

#### Process invocation.

The typing rule for a process invocation
$\mathsf{\color[rgb]{0,0.2,0}X}{}[\overline{u}]$ checks that there exists a
global definition for $\mathsf{\color[rgb]{0,0.2,0}X}$ which expects exactly
the given number and type of parameters. Again, rule [t-sub] will make it
possible to use parameters whose types are subtypes of the expected ones. A
process invocation yields the same dependencies as the corresponding process
definition, with the appropriate substitutions applied.

#### Guards.

Guards are used to match the content of a mailbox and possibly retrieve
messages from it. According to rule [t-fail], the action
$\mathtt{\color[rgb]{0,0,0.6}fail}\leavevmode\nobreak\ u$ matches a mailbox
$u$ with type $\texttt{?}\mathbb{0}$, indicating that an unexpected message
has been found in the mailbox. The type environment may contain arbitrary
associations, since the $\mathtt{\color[rgb]{0,0,0.6}fail}\leavevmode\nobreak\
u$ action causes a runtime error. Rule [t-free] states that the action
$\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\ u\texttt{.}P$ matches a
mailbox $u$ with type $\texttt{?}\mathbb{1}$, indicating that the mailbox is
empty. The continuation is well typed in the residual type environment
$\Gamma$. An input action
$u\texttt{?}\mathtt{\color[rgb]{0.3,0,0}m}(\overline{\mathit{x}})\texttt{.}P$
matches a mailbox $u$ with type
$\texttt{?}(\mathtt{\color[rgb]{0.3,0,0}m}{[}\overline{\tau}{]}\cdot E)$ that
guarantees the presence of an $\mathtt{\color[rgb]{0.3,0,0}m}$-tagged message
possibly along with other messages as specified by $E$. The continuation $P$
must be well typed in an environment where the mailbox has type $\texttt{?}E$,
which describes the content of the mailbox after the
$\mathtt{\color[rgb]{0.3,0,0}m}$-tagged message has been removed. Associations
for the received arguments $\overline{\mathit{x}}$ are also added to the type
environment. A compound guard $G_{1}+G_{2}$ offers the actions offered by
$G_{1}$ and $G_{2}$ and therefore matches a mailbox $u$ with type
$\texttt{?}(E_{1}+E_{2})$, where $E_{i}$ is the pattern that describes the
mailbox matched by $G_{i}$. Note that the residual type environment $\Gamma$
is the same in both branches, indicating that the type of other mailboxes used
by the guard cannot depend on that of $u$.

The judgments for guards do not yield any dependency graph. This is
compensated by the rule [t-guard], which we describe next.

#### Guarded processes.

Rule [t-guard] is used to type a guarded process $G$, which matches some
mailbox $u$ of type $\texttt{?}E$ and possibly retrieves messages from it. As
we have seen while discussing guards, $E$ is supposed to be a pattern of the
form $E_{1}+\cdots+E_{n}$ where each $E_{i}$ is either $\mathbb{0}$,
$\mathbb{1}$ or of the form $\mathtt{M}\cdot F$. However, only the patterns
$E$ that are in _normal form_ are suitable to be used in this typing rule and
the side condition $\vDash E$ checks that this is indeed the case. We motivate
the need of a normal form by means of a simple example.

Suppose that our aim is to type a process
$u\texttt{?}\mathtt{\color[rgb]{0.3,0,0}A}\texttt{.}P+u\texttt{?}\mathtt{\color[rgb]{0.3,0,0}B}\texttt{.}Q$
that consumes either an $\mathtt{\color[rgb]{0.3,0,0}A}$ message or a
$\mathtt{\color[rgb]{0.3,0,0}B}$ message from $u$, whichever of these two
messages is matched first in $u$, and then continues as $P$ or $Q$
correspondingly. Suppose also that the type of $u$ is $\texttt{?}E$ with
$E\stackrel{{\scriptstyle\text{\tiny
def}}}{{=}}\mathtt{\color[rgb]{0.3,0,0}A}\cdot\mathtt{\color[rgb]{0.3,0,0}C}+\mathtt{\color[rgb]{0.3,0,0}B}\cdot\mathtt{\color[rgb]{0.3,0,0}A}$,
which allows the rules for guards to successfully type check the process. As
we have seen while discussing rule [t-in], $P$ and $Q$ must be typed in an
environment where the type of $u$ has been updated so as to reflect the fact
that the consumed message is no longer in the mailbox. In this particular
case, we might be tempted to infer that the type of $u$ in $P$ is
$\texttt{?}\mathtt{\color[rgb]{0.3,0,0}C}$ and that the type of $u$ in $Q$ is
$\texttt{?}\mathtt{\color[rgb]{0.3,0,0}A}$. Unfortunately, the type
$\texttt{?}\mathtt{\color[rgb]{0.3,0,0}C}$ does not accurately describe the
content of the mailbox after $\mathtt{\color[rgb]{0.3,0,0}A}$ has been
consumed because, according to $E$, the $\mathtt{\color[rgb]{0.3,0,0}A}$
message may be accompanied by _either_ a $\mathtt{\color[rgb]{0.3,0,0}B}$
message _or_ by a $\mathtt{\color[rgb]{0.3,0,0}C}$ message, whereas
$\texttt{?}\mathtt{\color[rgb]{0.3,0,0}C}$ only accounts for the second
possibility. Thus, the appropriate pattern to be used for typing this process
is
$\mathtt{\color[rgb]{0.3,0,0}A}\cdot(\mathtt{\color[rgb]{0.3,0,0}B}+\mathtt{\color[rgb]{0.3,0,0}C})+\mathtt{\color[rgb]{0.3,0,0}B}\cdot\mathtt{\color[rgb]{0.3,0,0}A}$,
where the fact that $\mathtt{\color[rgb]{0.3,0,0}B}$ may be found after
consuming $\mathtt{\color[rgb]{0.3,0,0}A}$ is made explicit. This pattern and
$E$ are equivalent as they generate exactly the same set of valid
configurations. Yet,
$\mathtt{\color[rgb]{0.3,0,0}A}\cdot(\mathtt{\color[rgb]{0.3,0,0}B}+\mathtt{\color[rgb]{0.3,0,0}C})+\mathtt{\color[rgb]{0.3,0,0}B}\cdot\mathtt{\color[rgb]{0.3,0,0}A}$
is in normal form whereas $E$ is not. In general the normal form is not
unique. For example, also the patterns
$\mathtt{\color[rgb]{0.3,0,0}B}\cdot\mathtt{\color[rgb]{0.3,0,0}A}+\mathtt{\color[rgb]{0.3,0,0}C}\cdot\mathtt{\color[rgb]{0.3,0,0}A}$
and
$\mathtt{\color[rgb]{0.3,0,0}A}\cdot(\mathtt{\color[rgb]{0.3,0,0}B}+\mathtt{\color[rgb]{0.3,0,0}C})$
are in normal form and equivalent to $E$ and can be used for typing processes
that consume messages from $u$ in different orders or with different
priorities.

The first ingredient for defining the notion of pattern normal form is that of
pattern residual $E/\mathtt{M}$, which describes the content of a mailbox that
initially contains a configuration of messages described by $E$ and from which
we remove a single message with type $\mathtt{M}$:

######  Definition 3.7 (pattern residual).

The _residual_ of a pattern $E$ with respect to an atom $\mathtt{M}$, written
$E/\mathtt{M}$, is inductively defined by the following equations:

$\begin{array}[]{r@{~}c@{~}ll}\mathbb{0}/\mathtt{M}=\mathbb{1}/\mathtt{M}\leavevmode\nobreak\
&\stackrel{{\scriptstyle\text{\tiny def}}}{{=}}\hfil\leavevmode\nobreak\
&\mathbb{0}\\\ (E^{\ast})/\mathtt{M}\leavevmode\nobreak\
&\stackrel{{\scriptstyle\text{\tiny def}}}{{=}}\hfil\leavevmode\nobreak\
&E/\mathtt{M}\cdot E^{\ast}\end{array}\leavevmode\nobreak\
\begin{array}[]{r@{~}c@{~}ll}\mathtt{\color[rgb]{0.3,0,0}m}{[}\overline{\tau}{]}/\mathtt{\color[rgb]{0.3,0,0}m}{[}\overline{\sigma}{]}\leavevmode\nobreak\
&\stackrel{{\scriptstyle\text{\tiny def}}}{{=}}\hfil\leavevmode\nobreak\
&\mathbb{1}&\text{if $\overline{\tau}\leqslant\overline{\sigma}$}\\\
\mathtt{\color[rgb]{0.3,0,0}m}{[}\overline{\tau}{]}/\mathtt{\color[rgb]{0.3,0,0}m}^{\prime}{[}\overline{\sigma}{]}\leavevmode\nobreak\
&\stackrel{{\scriptstyle\text{\tiny def}}}{{=}}\hfil\leavevmode\nobreak\
&\mathbb{0}&\text{if
$\mathtt{\color[rgb]{0.3,0,0}m}\neq\mathtt{\color[rgb]{0.3,0,0}m}^{\prime}$}\end{array}\leavevmode\nobreak\
\begin{array}[]{r@{~}c@{~}ll}(E+F)/\mathtt{M}\leavevmode\nobreak\
&\stackrel{{\scriptstyle\text{\tiny def}}}{{=}}\hfil\leavevmode\nobreak\
&E/\mathtt{M}+F/\mathtt{M}\\\ (E\cdot F)/\mathtt{M}\leavevmode\nobreak\
&\stackrel{{\scriptstyle\text{\tiny def}}}{{=}}\hfil\leavevmode\nobreak\
&E/\mathtt{M}\cdot F+E\cdot F/\mathtt{M}\end{array}$

If we take the pattern $E$ discussed earlier we have
$E/\mathtt{\color[rgb]{0.3,0,0}A}=\mathbb{1}\cdot\mathtt{\color[rgb]{0.3,0,0}C}+\mathtt{\color[rgb]{0.3,0,0}A}\cdot\mathbb{0}+\mathbb{0}\cdot\mathbb{1}+\mathtt{\color[rgb]{0.3,0,0}B}\cdot\mathbb{1}\simeq\mathtt{\color[rgb]{0.3,0,0}B}+\mathtt{\color[rgb]{0.3,0,0}C}$.
The pattern residual operator is closely related to Brzozowski’s derivative in
a commutative Kleene algebra [4, 24]. Unlike Brzozowski’s derivative, the
pattern residual is a partial operator:
$E/\mathtt{\color[rgb]{0.3,0,0}m}{[}\overline{\sigma}{]}$ is defined provided
that the $\overline{\sigma}$ are supertypes of all types $\overline{\tau}$
found in $\mathtt{\color[rgb]{0.3,0,0}m}$-tagged atoms within $E$. This
condition has a natural justification: when choosing the message to remove
from a mailbox containing a configuration of messages described by $E$, only
the tag $\mathtt{\color[rgb]{0.3,0,0}m}$ of the message – and not the type of
its arguments – matters. Thus, $\overline{\sigma}$ faithfully describe the
received arguments provided that they are supertypes of _all_ argument types
of _all_ $\mathtt{\color[rgb]{0.3,0,0}m}$-tagged message types in $E$. For
example, assuming
$\mathtt{\color[rgb]{0,0,0.6}nat}\leqslant\mathtt{\color[rgb]{0,0,0.6}int}$,
we have that
$(\mathtt{\color[rgb]{0.3,0,0}m}{[}\mathtt{\color[rgb]{0,0,0.6}int}{]}+\mathtt{\color[rgb]{0.3,0,0}m}{[}\mathtt{\color[rgb]{0,0,0.6}nat}{]})/\mathtt{\color[rgb]{0.3,0,0}m}{[}\mathtt{\color[rgb]{0,0,0.6}int}{]}$
is defined whereas
$(\mathtt{\color[rgb]{0.3,0,0}m}{[}\mathtt{\color[rgb]{0,0,0.6}int}{]}+\mathtt{\color[rgb]{0.3,0,0}m}{[}\mathtt{\color[rgb]{0,0,0.6}nat}{]})/\mathtt{\color[rgb]{0.3,0,0}m}{[}\mathtt{\color[rgb]{0,0,0.6}nat}{]}$
is not.

We use the notion of pattern residual to define pattern normal forms:

######  Definition 3.8 (pattern normal form).

We say that a pattern $E$ is in _normal form_ , written $\vDash E$, if
$E\vDash E$ is derivable by the following axioms and rules:

$E\vDash\mathbb{0}\qquad
E\vDash\mathbb{1}\qquad{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
22.74994pt\vbox{\hbox{\hskip-22.74992pt\hbox{\hbox{$\displaystyle\displaystyle
F\simeq E/\mathtt{M}$}}}\vbox{}}}\over\hbox{\hskip
19.41663pt\vbox{\vbox{}\hbox{\hskip-19.41661pt\hbox{\hbox{$\displaystyle\displaystyle
E\vDash\mathtt{M}\cdot
F$}}}}}}$}}\qquad{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
40.24432pt\vbox{\hbox{\hskip-40.24432pt\hbox{\hbox{$\displaystyle\displaystyle
E\vDash F_{1}$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
E\vDash F_{2}$}}}}\vbox{}}}\over\hbox{\hskip
25.43187pt\vbox{\vbox{}\hbox{\hskip-25.43187pt\hbox{\hbox{$\displaystyle\displaystyle
E\vDash F_{1}+F_{2}$}}}}}}$}}$

Essentially, the judgment $\vDash E$ verifies that $E$ is expressed as a sum
of $\mathbb{0}$, $\mathbb{1}$ and $\mathtt{M}\cdot F$ terms where $F$ is
(equivalent to) the residual of $E$ with respect to $\mathtt{M}$.

A guarded process yields all the dependencies between the mailbox $u$ being
used and the names occurring free in the continuations, because the process
will not be able to exercise the capabilities on these names until the message
from $u$ has been received.

#### Parallel composition.

Rule [t-par] deals with parallel compositions of the form
$P_{1}\mathbin{\texttt{|}}P_{2}$. This rule accounts for the fact that the
same mailbox $u$ may be used in both $P_{1}$ and $P_{2}$ according to
different types. For example, $P_{1}$ might store an
$\mathtt{\color[rgb]{0.3,0,0}A}$ message into $u$ and $P_{2}$ might store a
$\mathtt{\color[rgb]{0.3,0,0}B}$ message into $u$. In the type environment for
the parallel composition as a whole we must be able to express with a single
type the combined usages of $u$ in $P_{1}$ and $P_{2}$. This is accomplished
by introducing an operator that combines types:

######  Definition 3.9 (type combination).

We write $\tau\mathbin{\|}\sigma$ for the _combination_ of $\tau$ and
$\sigma$, where $\mathbin{\|}$ is the partial symmetric operator defined as
follows:

$\texttt{!}E\mathbin{\|}\texttt{!}F\stackrel{{\scriptstyle\text{\tiny
def}}}{{=}}\texttt{!}(E\cdot F)\qquad\texttt{!}E\mathbin{\|}\texttt{?}(E\cdot
F)\stackrel{{\scriptstyle\text{\tiny
def}}}{{=}}\texttt{?}F\qquad\texttt{?}(E\cdot
F)\mathbin{\|}\texttt{!}E\stackrel{{\scriptstyle\text{\tiny
def}}}{{=}}\texttt{?}F$

Continuing the previous example, we have
$\texttt{!}\mathtt{\color[rgb]{0.3,0,0}A}\mathbin{\|}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}B}=\texttt{!}(\mathtt{\color[rgb]{0.3,0,0}A}\cdot\mathtt{\color[rgb]{0.3,0,0}B})$
because storing one $\mathtt{\color[rgb]{0.3,0,0}A}$ message and one
$\mathtt{\color[rgb]{0.3,0,0}B}$ message in $u$ means storing an overall
configuration of messages described by the pattern
$\mathtt{\color[rgb]{0.3,0,0}A}\cdot\mathtt{\color[rgb]{0.3,0,0}B}$. When $u$
is used for both input and output operations, the combined type of $u$
describes the overall balance of the mailbox. For example, we have
$\texttt{!}\mathtt{\color[rgb]{0.3,0,0}A}\mathbin{\|}\texttt{?}(\mathtt{\color[rgb]{0.3,0,0}A}\cdot\mathtt{\color[rgb]{0.3,0,0}B})=\texttt{?}\mathtt{\color[rgb]{0.3,0,0}B}$:
if we combine a process that stores an $\mathtt{\color[rgb]{0.3,0,0}A}$
message into $u$ with another process that consumes both an
$\mathtt{\color[rgb]{0.3,0,0}A}$ message and a
$\mathtt{\color[rgb]{0.3,0,0}B}$ message from the same mailbox in some
unspecified order, then we end up with a process that consumes a
$\mathtt{\color[rgb]{0.3,0,0}B}$ message from $u$.

Notice that $\mathbin{\|}$ is a partial operator in that not all type
combinations are defined. It might be tempting to relax $\mathbin{\|}$ in such
a way that
$\texttt{!}(\mathtt{\color[rgb]{0.3,0,0}A}\cdot\mathtt{\color[rgb]{0.3,0,0}B})\mathbin{\|}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}A}=\texttt{!}\mathtt{\color[rgb]{0.3,0,0}B}$,
so as to represent the fact that the combination of two processes results in
an excess of messages that must be consumed by some other process. However,
this would mean allowing different processes to consume messages from the same
mailbox, which is not safe in general (see Example 3.10). For the same reason,
the combination of $\texttt{?}E$ and $\texttt{?}F$ is always undefined
regardless of $E$ and $F$. Operators akin to $\mathbin{\|}$ for the
combination of channel types are commonly found in substructural type systems
for the (linear) $\pi$-calculus [44, 38]. Unlike these systems, in our case
the combination concerns also the content of a mailbox in addition to the
capabilities for accessing it.

######  Example 3.10.

Suppose that we extend the type combination operator so that
$\texttt{?}(E\cdot F)=\texttt{?}E\mathbin{\|}\texttt{?}F$. To see why this
extension would be dangerous, consider the process

$\begin{array}[]{l}\left(u\texttt{!}\mathtt{\color[rgb]{0.3,0,0}A}{}[\mathtt{\color[rgb]{0.5,0,0.5}True}]\mathbin{\texttt{|}}u\texttt{?}\mathtt{\color[rgb]{0.3,0,0}A}(\mathit{x})\texttt{.}(\mathit{system}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}print\texttt{\\_}bool}{}[\mathit{x}]\mathbin{\texttt{|}}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
u\texttt{.}\mathtt{\color[rgb]{0,0,0.6}done})\right)\mathbin{\texttt{|}}{}\\\
\left(u\texttt{!}\mathtt{\color[rgb]{0.3,0,0}A}{}[\mathtt{\color[rgb]{0.5,0,0.5}2}]\mathbin{\texttt{|}}u\texttt{?}\mathtt{\color[rgb]{0.3,0,0}A}(\mathit{y})\texttt{.}(\mathit{system}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}print\texttt{\\_}int}{}[\mathit{y}]\mathbin{\texttt{|}}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
u\texttt{.}\mathtt{\color[rgb]{0,0,0.6}done})\right)\end{array}$

Overall, this process stores into $u$ a combination of messages that matches
the pattern
$\mathtt{\color[rgb]{0.3,0,0}A}{[}\mathtt{\color[rgb]{0,0,0.6}bool}{]}\cdot\mathtt{\color[rgb]{0.3,0,0}A}{[}\mathtt{\color[rgb]{0,0,0.6}int}{]}$
and retrieves from $u$ the same combination of messages. Apparently, $u$ is
used in a balanced way. However, there is no guarantee that the
$u\texttt{!}\mathtt{\color[rgb]{0.3,0,0}A}{}[\mathtt{\color[rgb]{0.5,0,0.5}True}]$
message is received by the process at the top and that the
$u\texttt{!}\mathtt{\color[rgb]{0.3,0,0}A}{}[\mathtt{\color[rgb]{0.5,0,0.5}2}]$
message is received by the process at the bottom. In fact, the converse may
happen because only the tag of a message – not the type or value of its
arguments – is used for matching messages in the mailbox calculus.
$\blacksquare$

We now extend type combination to type environments in the expected way:

######  Definition 3.11 (type environment combination).

We write $\Gamma\mathbin{\|}\Delta$ for the _combination_ of $\Gamma$ and
$\Delta$, where $\mathbin{\|}$ is the partial operator inductively defined by
the equations:

$\Gamma\mathbin{\|}\emptyset\stackrel{{\scriptstyle\text{\tiny
def}}}{{=}}\Gamma\qquad\emptyset\mathbin{\|}\Gamma\stackrel{{\scriptstyle\text{\tiny
def}}}{{=}}\Gamma\qquad(u:\tau,\Gamma)\mathbin{\|}(u:\sigma,\Delta)\stackrel{{\scriptstyle\text{\tiny
def}}}{{=}}u:\tau\mathbin{\|}\sigma,(\Gamma\mathbin{\|}\Delta)$

With this machinery in place, rule [t-par] is straightforward to understand
and the dependency graph of $P_{1}\mathbin{\texttt{|}}P_{2}$ is simply the
union of the dependency graphs of $P_{1}$ and $P_{2}$.

#### Mailbox restriction.

Rule [t-new] establishes that the process creating a new mailbox $a$ with
scope $P$ is well typed provided that the type of $a$ is
$\texttt{?}\mathbb{1}$. This means that every message stored in the mailbox
$a$ by (a sub-process of) $P$ is also consumed by (a sub-process of) $P$. The
dependency graph of the process is the same as that of $P$, except that $a$ is
restricted.

#### Subsumption.

As we have anticipated earlier in a few occasions, the subsumption rule
[t-sub] allows us to rewrite types in the type environment and to introduce
associations for irrelevant names. The rule makes use of the following notion
of subtyping for type environments:

######  Definition 3.12 (subtyping for type environments).

We say that $\Gamma$ is a _subtype environment_ of $\Delta$ if
$\Gamma\leqslant\Delta$, where $\leqslant$ is the least preorder on type
environments such that:

$\displaystyle\displaystyle{\hbox{\hskip 0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hbox{$\displaystyle\displaystyle\mathstrut$}}}\vbox{}}}\over\hbox{\hskip
24.66777pt\vbox{\vbox{}\hbox{\hskip-24.66777pt\hbox{\hbox{$\displaystyle\displaystyle
u:\texttt{!}\mathbb{1},\Gamma\leqslant\Gamma$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
11.70944pt\vbox{\hbox{\hskip-11.70944pt\hbox{\hbox{$\displaystyle\displaystyle\tau\leqslant\sigma$}}}\vbox{}}}\over\hbox{\hskip
35.90611pt\vbox{\vbox{}\hbox{\hskip-35.9061pt\hbox{\hbox{$\displaystyle\displaystyle
u:\tau,\Gamma\leqslant u:\sigma,\Gamma$}}}}}}$

Intuitively, $\Gamma\leqslant\Delta$ means that $\Gamma$ provides more
capabilities than $\Delta$. For example,
$u:\texttt{!}(\mathtt{\color[rgb]{0.3,0,0}A}+\mathtt{\color[rgb]{0.3,0,0}B}),v:\texttt{!}\mathbb{1}\leqslant
u:\texttt{!}\mathtt{\color[rgb]{0.3,0,0}A}$ since a process that is well typed
in the environment $u:\texttt{!}\mathtt{\color[rgb]{0.3,0,0}A}$ stores an
$\mathtt{\color[rgb]{0.3,0,0}A}$ message into $u$, which is also a valid
behavior in the environment
$u:\texttt{!}(\mathtt{\color[rgb]{0.3,0,0}A}+\mathtt{\color[rgb]{0.3,0,0}B}),v:\texttt{!}\mathbb{1}$
where $u$ has more capabilities (it is also possible to store a
$\mathtt{\color[rgb]{0.3,0,0}B}$ message into $u$) and there is an irrelevant
name $v$ not used by the process.

Rule [t-sub] also allows us to replace the dependency graph yielded by $P$
with another one that generates a superset of dependencies. In general, the
dependency graph should be kept as small as possible to minimize the
possibility of yielding mutual dependencies (see [t-par]). The replacement
allowed by [t-sub] is handy for technical reasons, but not necessary. The
point is that the residual of a process typically yields fewer dependencies
than the process itself, so we use [t-sub] to enforce the invariance of
dependency graphs across reductions.

######  Example 3.13.

We show the full typing derivation for $\mathsf{\color[rgb]{0,0.2,0}FreeLock}$
and $\mathsf{\color[rgb]{0,0.2,0}BusyLock}$ defined in Example 2.1. Our
objective is to show the consistency of the global process declarations

$\mathsf{\color[rgb]{0,0.2,0}FreeLock}:(\mathit{self}:\tau;\emptyset)\qquad\mathsf{\color[rgb]{0,0.2,0}BusyLock}:(\mathit{self}:\tau,\mathit{owner}:\rho;\\{\mathit{self},\mathit{owner}\\})$

where $\tau\stackrel{{\scriptstyle\text{\tiny
def}}}{{=}}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}acquire}{[}\rho{]}^{\ast}$
and $\rho\stackrel{{\scriptstyle\text{\tiny
def}}}{{=}}\texttt{!}{\mathtt{\color[rgb]{0.3,0,0}reply}{[}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}release}{]}}$.
In the derivation trees below we rename $\mathit{self}$ as $\mathit{x}$ and
$\mathit{owner}$ and $\mathit{y}$ to resonably fit the derivations within the
page limits. We start from the body of
$\mathsf{\color[rgb]{0,0.2,0}BusyLock}$, which is simpler, and obtain

${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
68.61295pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=137.22589pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-msg}{\text{\scriptsize[{t-msg}]}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\mathit{x}:\texttt{!}\mathtt{\color[rgb]{0.3,0,0}release},\mathit{y}:\rho\vdash\mathit{y}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}reply}{}[\mathit{x}]{}::\\{\mathit{y},\mathit{x}\\}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\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
43.8663pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=87.7326pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-def}{\text{\scriptsize[{t-def}]}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\mathit{x}:\tau\vdash\mathsf{\color[rgb]{0,0.2,0}FreeLock}{}[\mathit{x}]{}::\emptyset$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=189.16345pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-in}{\text{\scriptsize[{t-in}]}}$}}}\hbox{\kern
35.83574pt\hbox{$\displaystyle\mathit{x}:\sigma\vdash\mathit{x}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}release}\texttt{.}\mathsf{\color[rgb]{0,0.2,0}FreeLock}{}[\mathit{x}]$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=280.12503pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-guard}{\text{\scriptsize[{t-guard}]}}$}}}\hbox{\kern
74.64989pt\hbox{$\displaystyle\mathit{x}:\sigma\vdash\mathit{x}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}release}\texttt{.}\mathsf{\color[rgb]{0,0.2,0}FreeLock}{}[\mathit{x}]{}::\emptyset$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=638.05562pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-par}{\text{\scriptsize[{t-par}]}}$}}}\hbox{\kern
217.88184pt\hbox{$\displaystyle\mathit{x}:\tau,\mathit{y}:\rho\vdash\mathit{y}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}reply}{}[\mathit{x}]\mathbin{\texttt{|}}\mathit{x}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}release}\texttt{.}\mathsf{\color[rgb]{0,0.2,0}Lock}{}[\mathit{x}]{}::\\{\mathit{y},\mathit{x}\\}\sqcup\emptyset$}}}}$

where $\sigma\stackrel{{\scriptstyle\text{\tiny
def}}}{{=}}\texttt{?}{(\mathtt{\color[rgb]{0.3,0,0}release}\cdot\mathtt{\color[rgb]{0.3,0,0}acquire}{[}\rho{]}^{\ast})}$.

Concerning $\mathsf{\color[rgb]{0,0.2,0}FreeLock}$, the key step is rewriting
the pattern of $\tau$ in a normal form that matches the branching structure of
the process. To this aim, we use the property $E^{\ast}\simeq\mathbb{1}+E\cdot
E^{\ast}$ and the fact that $\mathbb{0}$ is absorbing for the product
connective:

${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\qquad\qquad\vdots\qquad\qquad\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
23.88895pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=47.7779pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-fail}{\text{\scriptsize[{t-fail}]}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\mathit{x}:\texttt{?}\mathbb{0}\vdash\mathtt{\color[rgb]{0,0,0.6}fail}\leavevmode\nobreak\
\mathit{x}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=150.87029pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-guard}{\text{\scriptsize[{t-guard}]}}$}}}\hbox{\kern
44.87953pt\hbox{$\displaystyle\mathit{x}:\texttt{?}\mathbb{0}\vdash\mathtt{\color[rgb]{0,0,0.6}fail}\leavevmode\nobreak\
\mathit{x}{}::\emptyset$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=270.20367pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-in}{\text{\scriptsize[{t-in}]}}$}}}\hbox{\kern
69.18509pt\hbox{$\displaystyle\mathit{x}:\texttt{?}(\mathtt{\color[rgb]{0.3,0,0}release}\cdot\mathbb{0})\vdash\mathit{x}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}release}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}fail}\leavevmode\nobreak\
\mathit{x}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=443.66537pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-branch}{\text{\scriptsize[{t-branch}]}}$}}}\hbox{\kern
91.9568pt\hbox{$\displaystyle\mathit{x}:\texttt{?}(\mathbb{1}+\mathtt{\color[rgb]{0.3,0,0}acquire}{[}\rho{]}\cdot\mathtt{\color[rgb]{0.3,0,0}acquire}{[}\rho{]}^{\ast}+\mathtt{\color[rgb]{0.3,0,0}release}\cdot\mathbb{0})\vdash{}\cdots+\mathit{x}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}release}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}fail}\leavevmode\nobreak\
\mathit{x}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=472.8842pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-guard}{\text{\scriptsize[{t-guard}]}}$}}}\hbox{\kern
101.01065pt\hbox{$\displaystyle\mathit{x}:\texttt{?}(\mathbb{1}+\mathtt{\color[rgb]{0.3,0,0}acquire}{[}\rho{]}\cdot\mathtt{\color[rgb]{0.3,0,0}acquire}{[}\rho{]}^{\ast}+\mathtt{\color[rgb]{0.3,0,0}release}\cdot\mathbb{0})\vdash{}\cdots+\mathit{x}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}release}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}fail}\leavevmode\nobreak\
\mathit{x}{}::\emptyset$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=502.10303pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-sub}{\text{\scriptsize[{t-sub}]}}$}}}\hbox{\kern
161.0324pt\hbox{$\displaystyle\mathit{x}:\tau\vdash\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
\mathit{x}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}done}+\cdots+\mathit{x}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}release}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}fail}\leavevmode\nobreak\
\mathit{x}{}::\emptyset$}}}}$

The elided sub-derivation concerns the first two branches of
$\mathsf{\color[rgb]{0,0.2,0}FreeLock}$ and is 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
23.88887pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=47.77774pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-done}{\text{\scriptsize[{t-done}]}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\emptyset\vdash\mathtt{\color[rgb]{0,0,0.6}done}{}::\emptyset$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=158.55812pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-free}{\text{\scriptsize[{t-free}]}}$}}}\hbox{\kern
42.59842pt\hbox{$\displaystyle\mathit{x}:\texttt{?}\mathbb{1}\vdash\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
\mathit{x}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}done}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2\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
66.46536pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=132.93073pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-def}{\text{\scriptsize[{t-def}]}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\mathit{x}:\tau,\mathit{y}:\rho\vdash\mathsf{\color[rgb]{0,0.2,0}BusyLock}{}[\mathit{x},\mathit{y}]{}::\\{\mathit{x},\mathit{y}\\}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=234.36157pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-in}{\text{\scriptsize[{t-in}]}}$}}}\hbox{\kern
3.31871pt\hbox{$\displaystyle\mathit{x}:\texttt{?}\mathtt{\color[rgb]{0.3,0,0}acquire}{[}\rho{]}\cdot\mathtt{\color[rgb]{0.3,0,0}acquire}{[}\rho{]}^{\ast}\vdash\mathit{x}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}acquire}(\mathit{y})\texttt{.}\mathsf{\color[rgb]{0,0.2,0}BusyLock}{}[\mathit{x},\mathit{y}]$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=585.73898pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-branch}{\text{\scriptsize[{t-branch}]}}$}}}\hbox{\kern
138.7157pt\hbox{$\displaystyle\mathit{x}:\texttt{?}(\mathbb{1}+\mathtt{\color[rgb]{0.3,0,0}acquire}{[}\rho{]}\cdot\mathtt{\color[rgb]{0.3,0,0}acquire}{[}\rho{]}^{\ast})\vdash\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
\mathit{x}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}done}+\mathit{x}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}acquire}(\mathit{y})\texttt{.}\mathsf{\color[rgb]{0,0.2,0}BusyLock}{}[\mathit{x},\mathit{y}]$}}}}$

The process (1), combining an instance of the lock and the users
$\mathit{alice}$ and $\mathit{carol}$, is also well typed. As we will see at
the end of Section 3.4, this implies that both $\mathit{alice}$ and
$\mathit{carol}$ are able to acquire the lock, albeit in some unspecified
order. $\blacksquare$

######  Example 3.14.

In this example we show that the process (2) of Example 2.2 is ill typed. In
order to do so, we assume the global process declaration

$\mathsf{\color[rgb]{0,0.2,0}Future}:(\mathit{self}:\texttt{?}(\mathtt{\color[rgb]{0.3,0,0}put}{[}\mathtt{\color[rgb]{0,0,0.6}int}{]}\cdot\mathtt{\color[rgb]{0.3,0,0}get}{[}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}reply}{[}\mathtt{\color[rgb]{0,0,0.6}int}{]}{]}^{\ast});\emptyset)$

which can be shown to be consistent with the given definition for
$\mathsf{\color[rgb]{0,0.2,0}Future}$. In the derivation below we use the
pattern $F\stackrel{{\scriptstyle\text{\tiny
def}}}{{=}}\mathtt{\color[rgb]{0.3,0,0}put}{[}\mathtt{\color[rgb]{0,0,0.6}int}{]}\cdot\mathtt{\color[rgb]{0.3,0,0}get}{[}\rho{]}^{\ast}$
and the types $\tau\stackrel{{\scriptstyle\text{\tiny
def}}}{{=}}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}put}{[}\mathtt{\color[rgb]{0,0,0.6}int}{]}$,
$\sigma\stackrel{{\scriptstyle\text{\tiny
def}}}{{=}}\texttt{?}(\mathtt{\color[rgb]{0.3,0,0}reply}{[}\mathtt{\color[rgb]{0,0,0.6}int}{]}\cdot\mathbb{1})$
and $\rho\stackrel{{\scriptstyle\text{\tiny
def}}}{{=}}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}reply}{[}\mathtt{\color[rgb]{0,0,0.6}int}{]}$:

${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
60.13368pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=120.26736pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-msg}{\text{\scriptsize[{t-msg}]}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\mathit{f}:\texttt{!}\mathtt{\color[rgb]{0.3,0,0}get}{[}\rho{]},c:\rho\vdash\mathit{f}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}get}{}[c]{}::\\{\mathit{f},c\\}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\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{$\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
43.15804pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=86.31607pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-msg}{\text{\scriptsize[{t-msg}]}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\mathit{f}:\tau,\mathit{x}:\mathtt{\color[rgb]{0,0,0.6}int}\vdash\mathit{f}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}put}{}[\mathit{x}]{}::\emptyset$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=192.68738pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-free}{\text{\scriptsize[{t-free}]}}$}}}\hbox{\kern
33.84421pt\hbox{$\displaystyle\mathit{f}:\tau,c:\texttt{?}\mathbb{1},\mathit{x}:\mathtt{\color[rgb]{0,0,0.6}int}\vdash\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
c\texttt{.}\mathit{f}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}put}{}[\mathit{x}]$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=299.54509pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-guard}{\text{\scriptsize[{t-guard}]}}$}}}\hbox{\kern
74.4148pt\hbox{$\displaystyle\mathit{f}:\tau,c:\texttt{?}\mathbb{1},\mathit{x}:\mathtt{\color[rgb]{0,0,0.6}int}\vdash\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
c\texttt{.}\mathit{f}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}put}{}[\mathit{x}]{}::\\{c,\mathit{f}\\}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=418.87848pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-in}{\text{\scriptsize[{t-in}]}}$}}}\hbox{\kern
132.73845pt\hbox{$\displaystyle\mathit{f}:\tau,c:\sigma\vdash
c\texttt{?}\mathtt{\color[rgb]{0.3,0,0}reply}(\mathit{x})\texttt{.}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
c\texttt{.}\mathit{f}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}put}{}[\mathit{x}]$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=504.84006pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-guard}{\text{\scriptsize[{t-guard}]}}$}}}\hbox{\kern
162.86098pt\hbox{$\displaystyle\mathit{f}:\tau,c:\sigma\vdash
c\texttt{?}\mathtt{\color[rgb]{0.3,0,0}reply}(\mathit{x})\texttt{.}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
c\texttt{.}\mathit{f}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}put}{}[\mathit{x}]{}::\\{c,\mathit{f}\\}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=760.69756pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-par}{\text{\scriptsize[{t-par}]}}$}}}\hbox{\kern
253.80278pt\hbox{$\displaystyle\mathit{f}:\texttt{!}(\mathtt{\color[rgb]{0.3,0,0}get}{[}\rho{]}\cdot\mathtt{\color[rgb]{0.3,0,0}put}{[}\mathtt{\color[rgb]{0,0,0.6}int}{]}),c:\texttt{?}\mathbb{1}\vdash\mathit{f}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}get}{}[c]\mathbin{\texttt{|}}c\texttt{?}\mathtt{\color[rgb]{0.3,0,0}reply}(\mathit{x})\texttt{.}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
c\texttt{.}\mathit{f}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}put}{}[\mathit{x}]{}::{-}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=789.91638pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-sub}{\text{\scriptsize[{t-sub}]}}$}}}\hbox{\kern
298.61542pt\hbox{$\displaystyle\mathit{f}:\texttt{!}F,c:\texttt{?}\mathbb{1}\vdash\mathit{f}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}get}{}[c]\mathbin{\texttt{|}}c\texttt{?}\mathtt{\color[rgb]{0.3,0,0}reply}(\mathit{x})\texttt{.}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
c\texttt{.}\mathit{f}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}put}{}[\mathit{x}]{}::{-}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=819.13521pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-new}{\text{\scriptsize[{t-new}]}}$}}}\hbox{\kern
309.50491pt\hbox{$\displaystyle\mathit{f}:\texttt{!}F\vdash(\nu
c)(\mathit{f}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}get}{}[c]\mathbin{\texttt{|}}c\texttt{?}\mathtt{\color[rgb]{0.3,0,0}reply}(\mathit{x})\texttt{.}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
c\texttt{.}\mathit{f}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}put}{}[\mathit{x}]){}::{-}$}}}}$

In attempting this derivation we have implicitly extended the typing rules so
that names with type $\mathtt{\color[rgb]{0,0,0.6}int}$ do not contribute in
generating any significant dependency. The critical point of the derivation is
the application of [t-par], where we are composing two parallel processes that
yield a circular dependency between $c$ and $\mathit{f}$. In the process on
the left hand side, the dependency $\\{\mathit{f},c\\}$ arises because $c$ is
sent as a reference in a message targeted to $\mathit{f}$. In the process on
the right hand side, the dependency $\\{c,\mathit{f}\\}$ arises because there
are guards concerning the mailbox $c$ that block an output operation on the
mailbox $\mathit{f}$. $\blacksquare$

######  Example 3.15 (non-deterministic choice).

Different input actions in the same guard can match messages with the same
tag. This feature can be used to encode in the mailbox calculus the non-
deterministic choice between $P_{1}$ and $P_{2}$ as the process

$(\nu
a)(a\texttt{!}\mathtt{\color[rgb]{0.3,0,0}m}{}\mathbin{\texttt{|}}a\texttt{?}\mathtt{\color[rgb]{0.3,0,0}m}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
a\texttt{.}P_{1}+a\texttt{?}\mathtt{\color[rgb]{0.3,0,0}m}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
a\texttt{.}P_{2})$ (3)

provided that $\Gamma\vdash P_{i}{}::\varphi_{i}$ for $i=1,2$. That is,
$P_{1}$ and $P_{2}$ must be well typed in the same type environment. Below is
the typing derivation for (3)

${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
30.28584pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=60.57169pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-msg}{\text{\scriptsize[{t-msg}]}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle a:\texttt{!}\mathtt{\color[rgb]{0.3,0,0}m}\vdash
a\texttt{!}\mathtt{\color[rgb]{0.3,0,0}m}{}{}::\emptyset$}}}}\hskip 5.0pt plus
1.0fil\penalty 2\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{$\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
15.23105pt\hbox{$\displaystyle\penalty 1\Gamma\vdash
P_{i}{}::\varphi_{i}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=74.92119pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-free}{\text{\scriptsize[{t-free}]}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma,a:\texttt{?}\mathbb{1}\vdash\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
a\texttt{.}P_{i}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=181.7789pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-guard}{\text{\scriptsize[{t-guard}]}}$}}}\hbox{\kern
45.9914pt\hbox{$\displaystyle\Gamma,a:\texttt{?}\mathbb{1}\vdash\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
a\texttt{.}P_{i}{}::\varphi$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=301.11229pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-in}{\text{\scriptsize[{t-in}]}},i=1,2$}}}\hbox{\kern
90.31374pt\hbox{$\displaystyle\Gamma,a:\texttt{?}(\mathtt{\color[rgb]{0.3,0,0}m}\cdot\mathbb{1})\vdash
a\texttt{?}\mathtt{\color[rgb]{0.3,0,0}m}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
a\texttt{.}P_{i}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=427.74107pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-branch}{\text{\scriptsize[{t-branch}]}}$}}}\hbox{\kern
105.92175pt\hbox{$\displaystyle\Gamma,a:\texttt{?}(\mathtt{\color[rgb]{0.3,0,0}m}\cdot\mathbb{1}+\mathtt{\color[rgb]{0.3,0,0}m}\cdot\mathbb{1})\vdash
a\texttt{?}\mathtt{\color[rgb]{0.3,0,0}m}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
a\texttt{.}P_{1}+a\texttt{?}\mathtt{\color[rgb]{0.3,0,0}m}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
a\texttt{.}P_{2}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=549.62193pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-guard}{\text{\scriptsize[{t-guard}]}}$}}}\hbox{\kern
159.4247pt\hbox{$\displaystyle\Gamma,a:\texttt{?}(\mathtt{\color[rgb]{0.3,0,0}m}\cdot\mathbb{1}+\mathtt{\color[rgb]{0.3,0,0}m}\cdot\mathbb{1})\vdash
a\texttt{?}\mathtt{\color[rgb]{0.3,0,0}m}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
a\texttt{.}P_{1}+a\texttt{?}\mathtt{\color[rgb]{0.3,0,0}m}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
a\texttt{.}P_{2}{}::\varphi$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=578.84076pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-sub}{\text{\scriptsize[{t-sub}]}}$}}}\hbox{\kern
185.9786pt\hbox{$\displaystyle\Gamma,a:\texttt{?}(\mathtt{\color[rgb]{0.3,0,0}m}\cdot\mathbb{1})\vdash
a\texttt{?}\mathtt{\color[rgb]{0.3,0,0}m}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
a\texttt{.}P_{1}+a\texttt{?}\mathtt{\color[rgb]{0.3,0,0}m}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
a\texttt{.}P_{2}{}::\varphi$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=775.00258pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-par}{\text{\scriptsize[{t-par}]}}$}}}\hbox{\kern
285.30542pt\hbox{$\displaystyle\Gamma,a:\texttt{?}\mathbb{1}\vdash
a\texttt{!}\mathtt{\color[rgb]{0.3,0,0}m}{}\mathbin{\texttt{|}}a\texttt{?}\mathtt{\color[rgb]{0.3,0,0}m}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
a\texttt{.}P_{1}+a\texttt{?}\mathtt{\color[rgb]{0.3,0,0}m}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
a\texttt{.}P_{2}{}::\varphi$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=804.2214pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-new}{\text{\scriptsize[{t-new}]}}$}}}\hbox{\kern
288.58205pt\hbox{$\displaystyle\Gamma\vdash(\nu
a)(a\texttt{!}\mathtt{\color[rgb]{0.3,0,0}m}{}\mathbin{\texttt{|}}a\texttt{?}\mathtt{\color[rgb]{0.3,0,0}m}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
a\texttt{.}P_{1}+a\texttt{?}\mathtt{\color[rgb]{0.3,0,0}m}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
a\texttt{.}P_{2}){}::(\nu a)\varphi$}}}}$

where $\varphi\stackrel{{\scriptstyle\text{\tiny
def}}}{{=}}\\{a,\mathsf{dom}(\Gamma)\\}$. The key step is the application of
[t-sub], which exploits the idempotency of $+$ (in patterns) to rewrite
$\mathtt{\color[rgb]{0.3,0,0}m}\cdot\mathbb{1}$ as the equivalent pattern
$\mathtt{\color[rgb]{0.3,0,0}m}\cdot\mathbb{1}+\mathtt{\color[rgb]{0.3,0,0}m}\cdot\mathbb{1}$.
$\blacksquare$

###  3.4. Properties of well-typed processes

In this section we state the main properties enjoyed by well-typed processes.
As usual, subject reduction is instrumental for all of the results that follow
as it guarantees that typing is preserved by reductions:

######  Theorem 3.16.

If $\Gamma$ is reliable and $\Gamma\vdash P{}::\varphi$ and $P\rightarrow Q$,
then $\Gamma\vdash Q{}::\varphi$.

Interestingly, Theorem 3.16 seems to imply that the types of the mailboxes
used by a process do not change. In sharp contrast, other popular behavioral
typing disciplines (session types in particular), are characterized by a
subject reduction result in which types reduce along with processes. Theorem
3.16 also seems to contradict the observations made earlier concerning the
fact that the mailboxes used by a process may have different types (Example
3.4). The type preservation guarantee assured by Theorem 3.16 can be explained
by recalling that the type environment $\Gamma$ in a judgment $\Gamma\vdash
P{}::\varphi$ already takes into account the overall balance between the
messages stored into and consumed from the mailbox used by $P$ (see Definition
3.11). In light of this observation, Theorem 3.16 simply asserts that well-
typed processes are steady state: they never produce more messages than those
that are consumed, nor do they ever try to consume more messages than those
that are produced.

A practically relevant consequence of Theorem 3.16 is that, by looking at the
type $\texttt{?}E$ of the mailbox $a$ used by a guarded process $P$ (rule
[t-guard]), it is possible to determine _bounds_ to the number of messages
that can be found in the mailbox as $P$ waits for a message to receive. In
particular, if every configuration of $E$ contains at most $k$ atoms with tag
$\mathtt{\color[rgb]{0.3,0,0}m}$, then at runtime $a$ contains at most
$\mathtt{\color[rgb]{0.3,0,0}m}$-tagged messages. As a special case, a mailbox
of type $\texttt{?}\mathbb{1}$ is guaranteed to be empty and can be statically
deallocated. Note that the bounds may change after $P$ receives a message. For
example, a free lock is guaranteed to have no
$\mathtt{\color[rgb]{0.3,0,0}release}$ messages in its mailbox, and will have
at most one when it is busy (see Example 3.13).

The main result concerns the soundness of the type system, guaranteeing that
well-typed (closed) processes are both mailbox conformant and deadlock free:

######  Theorem 3.17.

If $\emptyset\vdash P{}::\varphi$, then $P$ is mailbox conformant and deadlock
free.

Fair termination and junk freedom are not guaranteed by our typing discipline
in general. The usual counterexamples include processes that postpone
indefinitely the use of a mailbox with a relevant type. For instance, the
$\mathtt{\color[rgb]{0.3,0,0}m}$ message in the well-typed process $(\nu
a)(a\texttt{!}\mathtt{\color[rgb]{0.3,0,0}m}{}\mathbin{\texttt{|}}\mathsf{\color[rgb]{0,0.2,0}X}{}[a])$
where
$\mathsf{\color[rgb]{0,0.2,0}X}(\mathit{x})\triangleq{\mathsf{\color[rgb]{0,0.2,0}X}{}[\mathit{x}]}$
is never consumed because $a$ is never used for an input operation.

Nevertheless, fair termination is guaranteed for the class of finitely
unfolding processes:

######  Theorem 3.18.

We say that $P$ is _finitely unfolding_ if all maximal reductions of $P$ use
[r-def] finitely many times. If $\emptyset\vdash P{}::\varphi$ and $P$ is
finitely unfolding, then $P$ is fairly terminating.

The class of finitely unfolding processes obviously includes all finite
processes (those not using process invocations) but also many recursive
processes. For example, every process of the form $(\nu
a)(a\texttt{!}\mathtt{\color[rgb]{0.3,0,0}m}{}\mathbin{\texttt{|}}\cdots\mathbin{\texttt{|}}a\texttt{!}\mathtt{\color[rgb]{0.3,0,0}m}{}\mathbin{\texttt{|}}\mathsf{\color[rgb]{0,0.2,0}X}{}[a])$
where
$\mathsf{\color[rgb]{0,0.2,0}X}(\mathit{x})\triangleq\mathit{x}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}m}\texttt{.}\mathsf{\color[rgb]{0,0.2,0}X}{}[\mathit{x}]+\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
\mathit{x}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}done}$ is closed, well typed
and finitely unfolding regardless of the number of
$\mathtt{\color[rgb]{0.3,0,0}m}$ messages stored in $a$, hence is fairly
terminating and junk free by Theorem 3.18.

##  4\. Examples

In this section we discuss a few more examples that illustrate the
expressiveness of the mailbox calculus and of its type system. We consider a
variant of the bank account shown in Listing 1 (Section 4.1), the case of
master-workers parallelism (Section 4.2) and the encoding of binary sessions
extended with forks and joins (Sections 4.3 and 4.4).

⬇

1class Account(var balance: Double) extends AkkaActor[AnyRef] {

2 override def process(msg: AnyRef) {

3 msg match {

4 case dm: DebitMessage =>

5 balance += dm.amount

6 sender() ! ReplyMessage.ONLY

7 case cm: CreditMessage =>

8 balance -= cm.amount

9 val recipient = cm.recipient.asInstanceOf[ActorRef]

10 val future = ask(recipient, new DebitMessage(self, cm.amount))
\label{account.future.begin}

11 Await.result(future, Duration.Inf) \label{account.future.end}

12 sender() ! ReplyMessage.ONLY

13 case _: StopMessage => exit()

14 case message =>

15 val ex = new IllegalArgumentException("Unsupported␣message")

16 ex.printStackTrace(System.err)

17 }

18 }

19}

Listing 2: An Akka actor using futures from the Savina benchmark suite [27].

###  4.1. Actors using futures

Many Scala programs combine actors with futures [46]. As an example, Listing 2
shows an alternative version of the Account actor in Akka that differes from
Listing 1 in the handling of CreditMessages (lines
LABEL:account.future.begin–LABEL:account.future.end). The future variable
created here is initialized asynchronously with the result of the debit
operation invoked on recipient. To make sure that each transaction is atomic,
the actor waits for the variable to be resolved (line
LABEL:account.future.end) before notifying sender that the operation has been
completed.

This version of Account is arguably simpler than the one in Listing 1, if only
because the actor has a unique top-level behavior. One way of modeling this
implementation of Account in the mailbox calculus is to use
$\mathsf{\color[rgb]{0,0.2,0}Future}$, discussed in Example 2.2. A simpler
modeling stems from the observation that future in Listing 2 is used for a
one-shot synchronization. A future variable with this property is akin to a
mailbox from which the value of the resolved variable is retrieved exactly
once. Following this approach we obtain the process below:

$\begin{array}[]{@{}rcl@{}}\mathsf{\color[rgb]{0,0.2,0}Account}(\mathit{self},\mathit{balance})&\triangleq&\mathit{self}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}debit}(\mathit{amount},\mathit{sender})\texttt{.}\\\
&&\mathit{sender}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}reply}{}\mathbin{\texttt{|}}\mathsf{\color[rgb]{0,0.2,0}Account}{}[\mathit{self},\mathit{balance}+\mathit{amount}]\\\
&+&\mathit{self}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}credit}(\mathit{amount},\mathit{recipient},\mathit{sender})\texttt{.}\\\
&&(\nu\mathit{future})\left(\begin{array}[]{@{}l@{}}\mathit{recipient}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}debit}{}[\mathit{amount},\mathit{future}]\mathbin{\texttt{|}}{}\\\
\mathit{future}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}reply}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
\mathit{future}\texttt{.}\\\
(\mathit{sender}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}reply}{}\mathbin{\texttt{|}}\mathsf{\color[rgb]{0,0.2,0}Account}{}[\mathit{self},\mathit{balance}+\mathit{amount}])\end{array}\right)\\\
&+&\mathit{self}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}stop}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
\mathit{self}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}done}\\\
&+&\mathit{self}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}reply}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}fail}\leavevmode\nobreak\
\mathit{self}\end{array}$

Compared to the process in Example 2.3, here the notification from the
$\mathit{recipient}$ account is received from the mailbox $\mathit{future}$,
which is created locally during the handling of the
$\mathtt{\color[rgb]{0.3,0,0}credit}$ message. The rest of the process is the
same as before. This definition of $\mathsf{\color[rgb]{0,0.2,0}Account}$ and
the one in Example 2.3 can both be shown to be consistent with the declaration

$\mathsf{\color[rgb]{0,0.2,0}Account}:(\mathit{self}:\texttt{?}(\mathtt{\color[rgb]{0.3,0,0}debit}{[}\mathtt{\color[rgb]{0,0,0.6}int},\rho{]}^{\ast}\cdot\mathtt{\color[rgb]{0.3,0,0}credit}{[}\mathtt{\color[rgb]{0,0,0.6}int},\texttt{!}\mathtt{\color[rgb]{0.3,0,0}debit}{[}\mathtt{\color[rgb]{0,0,0.6}int},\rho{]},\rho{]}^{\ast}+\mathtt{\color[rgb]{0.3,0,0}stop}),\mathit{balance}:\mathtt{\color[rgb]{0,0,0.6}int};\emptyset)$

where $\rho\stackrel{{\scriptstyle\text{\tiny
def}}}{{=}}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}reply}$. In particular, the
dependencies between $\mathit{self}$ and $\mathit{future}$ that originate in
this version of $\mathsf{\color[rgb]{0,0.2,0}Account}$ are not observable from
outside $\mathsf{\color[rgb]{0,0.2,0}Account}$ itself.

The use of multiple mailboxes and the interleaving of blocking operations on
them may increase the likelyhood of programming mistakes causing mismatched
communications and/or deadlocks. However, these errors can be detected by a
suitable typing discipline such the one proposed in this paper. Types can also
be used to mitigate the runtime overhead resulting from the use of multiple
mailboxes. Here, for example, the typing of $\mathit{future}$ guarantees that
this mailbox is used for receiving a _single_ message and that
$\mathit{future}$ is empty by the time
$\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\ \mathit{future}$ is
performed. A clever compiler can take advantage of this information to
statically optimize both the allocation and the deallocation of this mailbox.

###  4.2. Master-workers parallelism

In this example we model a _master_ process that receives tasks to perform
from a _client_. For each task, the master creates a pool of _workers_ and
assigns each worker a share of work. The master waits for all partial results
from the workers before sending the final result back to the client and making
itself available again. The number of workers may depend on some quantity
possibly related to the task to be performed and that is known at runtime
only.

Below we define three processes corresponding to the three states in which the
master process can be, and we leave $\mathsf{\color[rgb]{0,0.2,0}Worker}$
unspecified:

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\mathsf{\color[rgb]{0,0.2,0}Available}(\mathit{self})\leavevmode\nobreak\
&\triangleq\hfil\leavevmode\nobreak\
&\mathit{self}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}task}(\mathit{client})\texttt{.}(\nu\mathit{pool})\mathsf{\color[rgb]{0,0.2,0}CreatePool}{}[\mathit{self},\mathit{pool},\mathit{client}]\\\
\leavevmode\nobreak\ &+\hfil\leavevmode\nobreak\
&\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
\mathit{self}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}done}\\\
\mathsf{\color[rgb]{0,0.2,0}CreatePool}(\mathit{self},\mathit{pool},\mathit{client})\leavevmode\nobreak\
&\triangleq\hfil\leavevmode\nobreak\
&\mathtt{\color[rgb]{0,0,0.6}if}\leavevmode\nobreak\ \textit{more workers
needed}\leavevmode\nobreak\ \mathtt{\color[rgb]{0,0,0.6}then}\\\
\leavevmode\nobreak\ &\hfil\leavevmode\nobreak\
&\quad(\nu\mathit{worker})(\mathit{worker}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}work}{}[\mathit{pool}]\mathbin{\texttt{|}}\mathsf{\color[rgb]{0,0.2,0}Worker}{}[\mathit{worker}])\mathbin{\texttt{|}}{}\\\
\leavevmode\nobreak\ &\hfil\leavevmode\nobreak\
&\quad\mathsf{\color[rgb]{0,0.2,0}CreatePool}{}[\mathit{self},\mathit{pool},\mathit{client}]\\\
\leavevmode\nobreak\ &\hfil\leavevmode\nobreak\
&\mathtt{\color[rgb]{0,0,0.6}else}\\\ \leavevmode\nobreak\
&\hfil\leavevmode\nobreak\
&\quad\mathsf{\color[rgb]{0,0.2,0}CollectResults}{}[\mathit{self},\mathit{pool},\mathit{client}]\\\
\mathsf{\color[rgb]{0,0.2,0}CollectResults}(\mathit{self},\mathit{pool},\mathit{client})\leavevmode\nobreak\
&\triangleq\hfil\leavevmode\nobreak\
&\mathit{pool}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}result}\texttt{.}\mathsf{\color[rgb]{0,0.2,0}CollectResults}{}[\mathit{self},\mathit{pool},\mathit{client}]\\\
\leavevmode\nobreak\ &+\hfil\leavevmode\nobreak\
&\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
\mathit{pool}\texttt{.}(\mathit{client}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}result}{}\mathbin{\texttt{|}}\mathsf{\color[rgb]{0,0.2,0}Available}{}[\mathit{self}])\end{array}$

The “$\mathtt{\color[rgb]{0,0,0.6}if}\leavevmode\nobreak\
\mathit{condition}\leavevmode\nobreak\
\mathtt{\color[rgb]{0,0,0.6}then}\leavevmode\nobreak\ P\leavevmode\nobreak\
\mathtt{\color[rgb]{0,0,0.6}else}\leavevmode\nobreak\ Q$” form used here can
be encoded in the mailbox calculus and is typed similarly to the non-
deterministic choice of Example 3.15. These definitions can be shown to be
consistent with the following declarations:

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\mathsf{\color[rgb]{0,0.2,0}Available}\leavevmode\nobreak\
&:\hfil\leavevmode\nobreak\
&(\mathit{self}:\texttt{?}\mathtt{\color[rgb]{0.3,0,0}task}{[}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}result}{]}^{\ast};\emptyset)\\\
\mathsf{\color[rgb]{0,0.2,0}CreatePool},\mathsf{\color[rgb]{0,0.2,0}CollectResults}\leavevmode\nobreak\
&:\hfil\leavevmode\nobreak\
&(\mathit{self}:\texttt{?}\mathtt{\color[rgb]{0.3,0,0}task}{[}\texttt{!}\mathtt{\color[rgb]{0.3,0,0}result}{]}^{\ast},\mathit{pool}:\texttt{?}\mathtt{\color[rgb]{0.3,0,0}result}^{\ast},\mathit{client}:\texttt{!}\mathtt{\color[rgb]{0.3,0,0}result};\\\
\leavevmode\nobreak\ &\hfil\leavevmode\nobreak\
&\phantom{(}\\{\mathit{pool},\mathit{self}\\}\sqcup\\{\mathit{pool},\mathit{client}\\})\end{array}$

The usual implementation of this coordination pattern requires the programmer
to keep track of the number of active workers using a counter that is
decremented each time a partial result is collected [27]. When the counter
reaches zero, the master knows that all the workers have finished their job
and notifies the client. In the mailbox calculus, we achieve the same goal by
means of a dedicated mailbox $\mathit{pool}$ from which the partial results
are collected: when $\mathit{pool}$ becomes disposable, it means that no more
active workers remain.

###  4.3. Encoding of binary sessions

Session types [23, 25] have become a popular formalism for the specification
and enforcement of structured protocols through static analysis. A session is
a private communication channel shared by processes that interact through one
of its _endpoint_. Each endpoint is associated with a _session type_ that
specifies the type, direction and order of messages that are supposed to be
exchanged through that endpoint. A typical syntax for session types in the
case of _binary sessions_ (those connecting exactly two peer processes) is
shown below:

$T,S\leavevmode\nobreak\ \leavevmode\nobreak\ ::=\leavevmode\nobreak\
\leavevmode\nobreak\ \mathtt{\color[rgb]{0,0,0.6}end}\leavevmode\nobreak\
\leavevmode\nobreak\ \mid\leavevmode\nobreak\ \leavevmode\nobreak\
\texttt{?}{[}\tau{]}.T\leavevmode\nobreak\ \leavevmode\nobreak\
\mid\leavevmode\nobreak\ \leavevmode\nobreak\
\texttt{!}{[}\tau{]}.T\leavevmode\nobreak\ \leavevmode\nobreak\
\mid\leavevmode\nobreak\ \leavevmode\nobreak\
T\mathbin{\with}S\leavevmode\nobreak\ \leavevmode\nobreak\
\mid\leavevmode\nobreak\ \leavevmode\nobreak\ T\mathbin{\oplus}S$

A session type $\texttt{?}{[}\tau{]}.T$ describes an endpoint used for
receiving a message of type $\tau$ and then according to $T$. Dually, a
session type $\texttt{!}{[}\tau{]}.T$ describes an endpoint used for sending a
message of type $\tau$ and then according to $T$. An external choice
$T\mathbin{\with}S$ describes an endpoint used for receiving a selection
(either $\mathtt{\color[rgb]{0.3,0,0}left}$ or
$\mathtt{\color[rgb]{0.3,0,0}right}$) and then according to the corresponding
continuation (either $T$ or $S$). Dually, an internal choice
$T\mathbin{\oplus}S$ describes an endpoint used for making a selection and
then according to the corresponding continuation. Communication safety and
progress of a binary session are guaranteed by the fact that its two endpoints
are linear resources typed by _dual_ session types, where the dual of $T$ is
obtained by swapping inputs with outputs and internal with external choices.

In this example we encode sessions and session types using mailboxes and
mailbox types. We encode a session as a non-uniform, concurrent object. The
object is “concurrent” because it is accessed concurrently by the two peers of
the session. It is “non-uniform” because its interface changes over time, as
the session progresses. The object uses a mailbox $\mathit{self}$ and its
behavior is defined by the equations for
$\mathsf{\color[rgb]{0,0.2,0}Session}_{T}(\mathit{self})$ shown below, where
$T$ is the session type according to which it must be used by one of the
peers:

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\mathsf{\color[rgb]{0,0.2,0}Session}_{\mathtt{\color[rgb]{0,0,0.6}end}}(\mathit{self})\leavevmode\nobreak\
&\triangleq\hfil\leavevmode\nobreak\
&\mathtt{\color[rgb]{0,0,0.6}free}\leavevmode\nobreak\
\mathit{self}\texttt{.}\mathtt{\color[rgb]{0,0,0.6}done}\\\
\mathsf{\color[rgb]{0,0.2,0}Session}_{\texttt{?}{[}\tau{]}.T}(\mathit{self})\leavevmode\nobreak\
&\triangleq\hfil\leavevmode\nobreak\
&\mathit{self}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}send}(x,s)\texttt{.}\mathit{self}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}receive}(r)\texttt{.}\\\
\leavevmode\nobreak\ &\hfil\leavevmode\nobreak\
&(s\texttt{!}\mathtt{\color[rgb]{0.3,0,0}reply}{}[x,\mathit{self}]\mathbin{\texttt{|}}r\texttt{!}\mathtt{\color[rgb]{0.3,0,0}reply}{}[\mathit{self}]\mathbin{\texttt{|}}\mathsf{\color[rgb]{0,0.2,0}Session}_{T}{}[\mathit{self}])\\\
\mathsf{\color[rgb]{0,0.2,0}Session}_{\texttt{!}{[}\tau{]}.T}(\mathit{self})\leavevmode\nobreak\
&\triangleq\hfil\leavevmode\nobreak\
&\mathsf{\color[rgb]{0,0.2,0}Session}_{\texttt{?}{[}\tau{]}.T}{}[\mathit{self}]\\\
\mathsf{\color[rgb]{0,0.2,0}Session}_{T\mathbin{\with}S}(\mathit{self})\leavevmode\nobreak\
&\triangleq\hfil\leavevmode\nobreak\
&\mathit{self}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}left}(s)\texttt{.}\mathit{self}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}receive}(r)\texttt{.}\\\
\leavevmode\nobreak\ &\hfil\leavevmode\nobreak\
&(s\texttt{!}\mathtt{\color[rgb]{0.3,0,0}reply}{}[\mathit{self}]\mathbin{\texttt{|}}r\texttt{!}\mathtt{\color[rgb]{0.3,0,0}left}{}[\mathit{self}]\mathbin{\texttt{|}}\mathsf{\color[rgb]{0,0.2,0}Session}_{T}{}[\mathit{self}])\\\
\leavevmode\nobreak\ &+\hfil\leavevmode\nobreak\
&\mathit{self}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}right}(s)\texttt{.}\mathit{self}\texttt{?}\mathtt{\color[rgb]{0.3,0,0}receive}(r)\texttt{.}\\\
\leavevmode\nobreak\ &\hfil\leavevmode\nobreak\
&(s\texttt{!}\mathtt{\color[rgb]{0.3,0,0}reply}{}[\mathit{self}]\mathbin{\texttt{|}}r\texttt{!}\mathtt{\color[rgb]{0.3,0,0}right}{}[\mathit{self}]\mathbin{\texttt{|}}\mathsf{\color[rgb]{0,0.2,0}Session}_{S}{}[\mathit{self}])\\\
\mathsf{\color[rgb]{0,0.2,0}Session}_{T\mathbin{\oplus}S}(\mathit{self})\leavevmode\nobreak\
&\triangleq\hfil\leavevmode\nobreak\
&\mathsf{\color[rgb]{0,0.2,0}Session}_{T\mathbin{\with}S}{}[\mathit{self}]\end{array}$

To grasp the intuition behind the definition of
$\mathsf{\color[rgb]{0,0.2,0}Session}_{T}(\mathit{self})$, it helps to recall
that each stage of a session corresponds to an interaction between the two
peers, where one process plays the role of “sender” and its peer that of
“receiver”. Both peers manifest their willingness to interact by storing a
message into the session’s mailbox. The receiver always stores a
$\mathtt{\color[rgb]{0.3,0,0}receive}$ message, while the sender stores either
$\mathtt{\color[rgb]{0.3,0,0}send}$, $\mathtt{\color[rgb]{0.3,0,0}left}$ or
$\mathtt{\color[rgb]{0.3,0,0}right}$ according to $T$. All messages contain a
reference to the mailbox owned by sender and receiver (respectively $s$ and
$r$) where they will be notified once the interaction is completed. A
$\mathtt{\color[rgb]{0.3,0,0}send}$ message also carries actual payload
$\mathit{x}$ being exchanged. The role of
$\mathsf{\color[rgb]{0,0.2,0}Session}_{T}(\mathit{self})$ is simply to forward
each message from the sender to the receiver. The notifications stored in $s$
and $r$ contain a reference to the session’s mailbox so that its type reflects
the session’s updated interface corresponding to the rest of the conversation.

Interestingly, the encoding of a session with type $T$ is undistinguishable
from that of a session with the dual type $\overline{T}$. This is natural by
recalling that each stage of a session corresponds to a single interaction
between the two peers: the order in which they store the respective messages
in the session’s mailbox is in general unpredictable but also unimportant, for