#  Using $\pi$-Calculus Names as Locks

Daniel Hirschkoff ENS de Lyon<EMAIL_ADDRESS>Karlsruhe
Institute of Technology Enguerrand Prebet Karlsruhe Institute of Technology
<EMAIL_ADDRESS>
###### Abstract

Locks are a classic data structure for concurrent programming. We introduce a
type system to ensure that names of the asynchronous $\pi$-calculus are used
as locks. Our calculus also features a construct to deallocate a lock once we
know that it will never be acquired again. Typability guarantees two
properties: deadlock-freedom, that is, no acquire operation on a lock waits
forever; and leak-freedom, that is, all locks are eventually deallocated.

We leverage the simplicity of our typing discipline to study the induced typed
behavioural equivalence. After defining barbed equivalence, we introduce a
sound labelled bisimulation, which makes it possible to establish equivalence
between programs that manipulate and deallocate locks.

##  1 Introduction

The $\pi$-calculus is an expressive process calculus based on the notion of
name, in which name-passing is the primitive notion of interaction between
processes. Processes of the $\pi$-calculus have been used to represent several
aspects of programming, like data structures, protocols, or constructs such as
functions, continuations, objects, and references. The $\pi$-calculus also
comes with a well-developed theory of behavioural equivalence. This theory can
be exploited to reason about contextual equivalence in programming languages,
by translating programs as $\pi$-calculus processes.

In this work, we follow this path for locks, a basic data structure for
concurrent programming. We study how $\pi$-calculus names can be used to
represent locks. We show that the corresponding programming discipline in the
$\pi$-calculus induces a notion of behavioural equivalence between processes,
which can be used to reason about processes manipulating locks. This approach
has been followed to analyse several disciplines for the usage of
$\pi$-calculus names: linearity [16], receptiveness [26], locality [17],
internal mobility [25], functions [24, 6], references [8, 22].

It is natural to represent locks in $A\pi$, the asynchronous version of the
$\pi$-calculus [2, 10]. A lock is referred to using a $\pi$-calculus name. It
is represented as an asynchronous output: the release of the lock. Dually, an
input represents the acquire operation on some lock.

In this paper, we introduce $\pi\mathrm{\ell w}$, a version of the
asynchronous $\pi$-calculus with only lock names. Two properties should be
ensured for names to be used as locks: first, a lock can appear at most once
in released form. Second, acquiring a lock entails the obligation to release
it. For instance, process $\ell_{1}(x).(\overline{\ell_{1}}\langle
x\rangle|\overline{\ell_{2}}\langle x\rangle)$ has these properties: the
process acquires lock $\ell_{1}$, then releases it, together with lock
$\ell_{2}$. We remark that this this process owns lock $\ell_{2}$, which is
released after $\ell_{1}$ is acquired. We show that a simple type system can
be defined to guarantee the two properties mentioned above.

When manipulating locks, it is essential to avoid the program from getting
stuck in a state where a lock needs to be acquired but cannot be released.
Consider the following process:

$P_{\mathsf{dl}}\quad\stackrel{{\scriptstyle\rm
def}}{{=}}\quad\ell_{1}(x).(\overline{\ell_{1}}\langle
x\rangle|\overline{\ell_{2}}\langle
x\rangle)~{}~{}|~{}~{}\ell_{2}(y).(\overline{\ell_{1}}\langle
y\rangle|\overline{\ell_{2}}\langle y\rangle).$

The subprocess on the left needs to acquire lock $\ell_{1}$, which is owned by
the other subprocess, and symmetrically: this is a deadlock. Our type system
rules out processes that exhibit this kind of cyclic dependency between locks.
This is achieved by controlling parallel composition: two processes in
parallel can share at most one lock name. Process $P_{\mathsf{dl}}$ thus
cannot be typed, because names $\ell_{1}$ and $\ell_{2}$ are shared between
the two subprocesses. The acyclicity property enjoyed by typable processes
yields deadlock-freedom.

To avoid situations where a lock is in released state and cannot be accessed,
$\pi\mathrm{\ell w}$ also features a construct to deallocate a lock, called
_wait_ , inspired from [13]. Process $\ell(\\!(x)\\!).P$ waits until no
acquire is pending on lock $\ell$, at which point it deallocates $\ell$,
reading the final value stored in $\ell$ as $x$. The reduction rule for wait
is

$(\boldsymbol{\nu}\ell)\big{(}\,\overline{\ell}\langle
v\rangle~{}|~{}\ell(\\!(x)\\!).P\,\big{)}~{}\rightarrow~{}P\\{\raisebox{2.15277pt}{\small$v$}\\!/\\!\mbox{\small$x$}\\}$
(1)

provided $\ell$ is not among the free names of $P$. In the reduction above,
the restriction on $\ell$ disappears after the last interaction involving
$\ell$ has taken place.

The main contributions of this work are the following:

  * •

We introduce $\pi\mathrm{\ell w}$, a $\pi$-calculus with higher-order locks
(in the sense that locks can be stored in locks) and lock deallocation. The
type system for $\pi\mathrm{\ell w}$ controls the usage and the sharing of
lock names between processes. We provide some examples to illustrate how locks
can be manipulated according to the programming discipline induced by types.

  * •

We show that typable processes in $\pi\mathrm{\ell w}$ enjoy deadlock- and
leak-freedom. The proofs rely on simple arguments involving the graph induced
by the sharing of locks among processes.

  * •

We analyse typed behavioural equivalence in $\pi\mathrm{\ell w}$. Types
restrict the set of contexts that can interact with processes, yielding a
coarser behavioural equivalence than in the untyped case.

We first introduce typed barbed equivalence, written $\simeq_{w}$. Relation
$\simeq_{w}$ is defined by observing the behaviour of processes when they are
placed in typable contexts. We then express the interactions between typed
processes and typed context by means of a Labelled Transition System (LTS)
that takes into account typing constraints. This allows us to introduce _typed
bisimilarity_ , $\approx_{w}$, the main proof technique to establish barbed
equivalence: we indeed prove soundness, that is,
$\approx_{w}\subseteq\simeq_{w}$.

We discuss several examples that help to understand how we can reason about
behavioural equivalence in $\pi\mathrm{\ell w}$. We are not aware of existing
labelled equivalences taking into account name deallocation in the
$\pi$-calculus.

Beyond $\pi\mathrm{\ell w}$, we believe that $\approx_{w}$ can be used as a
building block when reasoning in the $\pi$-calculus about programs that use
various features, among which locks.

The aforementioned contributions are presented in two steps. We first
introduce $\pi\mathrm{\ell}$, an asynchronous $\pi$-calculus with higher-order
locks. $\pi\mathrm{\ell w}$ is obtained by adding the wait construct to
$\pi\mathrm{\ell}$. Several important ideas can be presented in
$\pi\mathrm{\ell}$, and we can build on the notions introduced for
$\pi\mathrm{\ell}$ to extend them for $\pi\mathrm{\ell w}$.

We now highlight some of the technical aspects involved in our work.

The type system for $\pi\mathrm{\ell}$ guarantees deadlock-freedom, in the
sense that for typable processes, an acquire operation cannot be blocked
forever. This holds for _complete processes_ : a process is complete if for
every lock $\ell$ it uses, a release of $\ell$ is available. Availability need
not be immediate, for instance the release operation on lock $\ell$ may be
blocked by an acquire on $\ell^{\prime}$. We prove progress based on the fact
that the type system guarantees acyclicity of the dependence relation between
locks. Progress entails deadlock-freedom.

When adding the wait construct, we rely on a similar reasoning to prove leak-
freedom for $\pi\mathrm{\ell w}$, which in our setting means that all locks
are eventually deallocated. The type system for $\pi\mathrm{\ell w}$ is richer
than the one for $\pi\mathrm{\ell}$ not only because it takes wait into
account, but also because it makes it possible to transmit the obligation of
releasing or deallocating a lock via another lock. For instance, it is
possible, depending on the type of $\ell$, that in process
$\ell(\ell^{\prime}).P$, the continuation $P$ has the obligation not only to
release lock $\ell$, but also to deallocate $\ell^{\prime}$, or release
$\ell^{\prime}$, or both.

To define typed barbed equivalence in $\pi\mathrm{\ell}$, written $\simeq$, we
must take into account deadlock-freedom, which has several consequences.
First, we observe complete processes: intuitively, computations in
$\pi\mathrm{\ell}$ make sense only for such processes, and a context
interacting with a process should not be able to block a computation by never
performing some release operation. Second, all barbs are always observable in
$\pi\mathrm{\ell}$. In other words, if $\ell$ is a free name of a complete
typable process $P$, then $P$ can never loose the ability to release $\ell$.
This is in contrast with barbed equivalence in the $\pi$-calculus, or in CCS,
where the absence of a barb can be used to observe behaviours. We therefore
adopt a stronger notion of barb, where the value stored in a lock, and not
only the name of the lock, can be observed.

The ideas behind $\simeq$ are used to define $\simeq_{w}$, typed barbed
equivalence in $\pi\mathrm{\ell w}$. A challenge when defining typed
bisimilarity in $\pi\mathrm{\ell w}$ is to come up with labelled transitions
corresponding to the reduction in (1). Intuitively, if
$P\xrightarrow{\ell(\\!(v)\\!)}P^{\prime}$ ($P$ deallocates $\ell$ and
continues as $P^{\prime}$), we must make sure that this transition is the last
interaction at $\ell$. We define a typed LTS to handle name deallocation, and
show that bisimilarity is sound for barbed equivalence in $\pi\mathrm{\ell
w}$.

##### Paper outline.

We study $\pi\mathrm{\ell}$ in Section 2. We first expose the essential ideas
of our deadlock-freedom proof in $\mathrm{CCS}\ell$, a simple version of the
Calculus of Communicating Systems [19] with lock names. After extending these
results to $\pi\mathrm{\ell}$, we define barbed equivalence for
$\pi\mathrm{\ell}$, written $\simeq$. We provide a labelled semantics that is
sound for $\simeq$, and present several examples of behavioural equivalences
in $\pi\mathrm{\ell}$. In Section 3, we add the wait construct, yielding
$\pi\mathrm{\ell w}$. We show how to derive leak-freedom, and define a
labelled semantics, building on the ideas of Section 2. We discuss related and
future work in Section 4.

##  2 $\pi\mathrm{\ell}$, a Deadlock-Free Asynchronous $\pi$-Calculus

We present deadlock-freedom in the simple setting of $\mathrm{CCS}\ell$ in
Section 2.1. This approach is extended to handle higher-order locks in
$\pi\mathrm{\ell}$ (Section 2.2). We study behavioural equivalence in
$\pi\mathrm{\ell}$ in Section 2.3.

###  2.1 $\mathrm{CCS}\ell$: Ensuring Deadlock-Freedom using Composition

$\mathrm{CCS}\ell$ is a simplification of $\pi\mathrm{\ell}$, to present the
ideas underlying the type system and the proof of deadlock-freedom.
$\mathrm{CCS}\ell$ is defined as an asynchronous version of CCS with acquire
and release operations. We postulate the existence of an infinite set of _lock
names_ , written $\ell,\ell^{\prime},\ell_{1},\dots$, which we often simply
call names. $\mathrm{CCS}\ell$ processes are defined by the following grammar:
P ::= ℓ.P$~{}\big{|}~{}$$\overline{\ell}$$~{}\big{|}~{}$($\boldsymbol{\nu}$ℓ)
P$~{}\big{|}~{}$P_1—P_2. $\overline{\ell}$ is the release of lock $\ell$.
Process $\ell.P$ acquires $\ell$ and then acts as $P$—we say that $P$ performs
an _acquire on $\ell$_. There is no $\bm{0}$ process in $\mathrm{CCS}\ell$,
intuitively because we do not take into consideration processes with no lock
at all. Restriction is a binder, and we write $\mathrm{fln}(P)$ for the set of
free lock names in $P$. If $\mathbb{S}=\\{\ell_{1},\dots,\ell_{k}\\}$ is a set
of lock names, we write $(\boldsymbol{\nu}\mathbb{S})P$ for
$(\boldsymbol{\nu}\ell_{1})\dots(\boldsymbol{\nu}\ell_{k})P$.

The definition of structural congruence, written $\equiv$, and reduction,
written $\xrightarrow{}$, are standard. They are given in Appendix A.1.
Relation $\xRightarrow{}$ is the transitive reflexive closure of
$\xrightarrow{}$.

##### Type System.

To define the type system for $\mathrm{CCS}\ell$, we introduce typing
environments. We use $\gamma$ to range over sets of lock names. We write
$\gamma_{1}\\#\gamma_{2}$ whenever $\gamma_{1}\cap\gamma_{2}=\emptyset$. We
write $\gamma,\ell$ for the set $\gamma\uplus\\{\ell\\}$: the notation
implicitly imposes $\ell\notin\gamma$.

_Typing environments_ , written $\Gamma$, are sets of such sets, with the
additional constraint that these should be pairwise disjoint. We write
$\Gamma=\gamma_{1},\dots,\gamma_{k}$, for $k\geq 1$, to mean that $\Gamma$ is
equal to $\\{\gamma_{1},\dots,\gamma_{k}\\}$, with $\gamma_{i}\\#\gamma_{j}$
whenever $i\neq j$. The $\gamma_{i}$s are called the _components_ of $\Gamma$
in this case, and $\mathrm{dom}(\Gamma)$, the domain of $\Gamma$, is defined
as $\gamma_{1}\cup\dots\cup\gamma_{k}$. We write $\Gamma_{1}\\#\Gamma_{2}$
whenever $\mathrm{dom}(\Gamma_{1})\cap\mathrm{dom}(\Gamma_{2})=\emptyset$.

As for components $\gamma$, the notation $\Gamma,\gamma$ stands for a set (of
sets) that can be written as $\Gamma\uplus\\{\gamma\\}$. Using these two
notations together, we can write $\Gamma,\gamma,\ell$ to refer to a typing
environment containing a component that contains $\ell$. We sometimes add
parentheses, writing e.g. $\Gamma,(\gamma,\ell,\ell^{\prime})$, to ease
readability.

The typing judgement is of the form $\Gamma;\mathbb{R}\vdash P$, where
$\mathbb{R}$ is a set of lock names. If $\Gamma;\mathbb{R}\vdash P$, then
$\mathbb{R}$ is the set of locks owned by $P$, that must be released. Moreover
any component $\gamma$ of $\Gamma$ intuitively corresponds to a subprocess of
$P$ that only accesses the names in $\gamma$. Here, accessing a lock name
$\ell$ means either releasing $\ell$ or performing an acquire on $\ell$, or
both. The typing rules are as follows:
[Acq-C]$\Gamma,(\gamma,\ell);\mathbb{R},\ell\vdash P$
${\\{\mathsf{flatten}(\Gamma)\uplus(\gamma,\ell)\\}};\mathbb{R}\vdash\ell.P$

[Rel-C] $\Gamma,(\gamma,\ell);\\{\ell\\}\vdash\overline{\ell}$

[New-C] $\Gamma,(\gamma,\ell);\mathbb{R},\ell\vdash P$
$\Gamma,\gamma;\mathbb{R}\vdash(\boldsymbol{\nu}\ell)P$

[Par-C] $\Gamma_{1};\mathbb{R}_{1}\vdash
P_{1}$$\Gamma_{2};\mathbb{R}_{2}\vdash P_{2}$
$\Gamma_{1}\bullet\Gamma_{2};\mathbb{R}_{1}\uplus\mathbb{R}_{2}\vdash
P_{1}|P_{2}$ In rule Acq-C, operator $\mathsf{flatten}$ has the effect of
mergining all components in a typing environment into a single component. In
particular, if $\Gamma=\\{\gamma_{1},\dots,\gamma_{k}\\}$, then
$\mathsf{flatten}($$\Gamma$) stands for
$\gamma_{1}\uplus\dots\uplus\gamma_{k}$. Intuitively, the causal dependency
introduced by the prefix $\ell.P$ induces a dependence between $\ell$ and all
the locks in $P$, forcing these locks to belong to the same component.

In the typing rules, we write $\mathbb{R},\ell$ for
$\mathbb{R}\uplus\\{\ell\\}$, i.e., we suppose $\ell\notin\mathbb{R}$,
otherwise the typing rule cannot be applied. Lock $\ell$ is added to
$\mathbb{R}$ in rule Acq-C, to ensure that it will be released in the
continuation $P$, and in rule New-C, to ensure that a newly created lock is
initialised with a release. Correspondingly, rule Rel-C type-checks the
release of lock $\ell$ by imposing $\mathbb{R}=\\{\ell\\}$.

To type-check parallel composition, we use an operation to compose typing
environments, written $\Gamma_{1}\bullet\Gamma_{2}$. For this, we set
$\emptyset\bullet\Gamma=\Gamma$ and
$(\Gamma,\gamma)\bullet\Gamma^{\prime}=\mathsf{connect}(\gamma;\Gamma\bullet\Gamma^{\prime})$,
where $\mathsf{connect}(\gamma;\\{\gamma_{1},\dots,\gamma_{k}\\})$ is
undefined as soon as there is $i$ such that $\gamma\cap\gamma_{i}$ contains at
least two distinct elements, and otherwise is defined as
$\mathsf{connect}(\gamma;\\{\gamma_{1},\dots,\gamma_{k}\\})$ =
$\\{\gamma_{i}:\gamma_{i}\\#\gamma\\}$ ⊎
$\\{\gamma\cup\mathsf{flatten}(\\{\gamma_{i}:\gamma_{i}\cap\gamma\neq\emptyset\\})\\}$
. In rule Par-C, we impose that $\mathbb{R}_{1}$ and $\mathbb{R}_{2}$ are
disjoint: if lock $\ell$ must be released, then this is done either by $P_{1}$
or by $P_{2}$. Together with rule Rel-C, this guarantees that any
$\ell\in\mathbb{R}$ is released exactly once.

We present some examples to illustrate the type system.

######  Example 1.

Processes $\ell_{1}.(\overline{\ell_{1}}|\overline{\ell_{1}})$ and
$\ell_{1}.\ell_{2}.\overline{\ell_{1}}$ cannot be typed, because both violate
linearity in the usage of locks: the former releases lock $\ell_{1}$ twice,
and the latter does not release $\ell_{2}$ after acquiring it.

Process $P_{1}\stackrel{{\scriptstyle\rm
def}}{{=}}\ell_{1}.(\overline{\ell_{1}}|\overline{\ell_{2}})$ acquires lock
$\ell_{1}$, and then releases locks $\ell_{1}$ and $\ell_{2}$. Let
$\gamma_{12}=\\{\ell_{1},\ell_{2}\\}$; we can derive
$\\{\gamma_{12}\\};\\{\ell_{2}\\}\vdash P_{1}$: locks $\ell_{1}$ and
$\ell_{2}$ necessarily belong to the same component when typing $P_{1}$.
Similarly, we have $\\{\gamma_{12}\\};\\{\ell_{1}\\}\vdash P_{2}$ with
$P_{2}\stackrel{{\scriptstyle\rm
def}}{{=}}\ell_{2}.(\overline{\ell_{2}}|\overline{\ell_{1}})$. The typing
derivations for $P_{1}$ and $P_{2}$ cannot be composed, because of the
presence of $\gamma_{12}$ in both, so $P_{1}|P_{2}$ cannot be typed. This is
appropriate, since $P_{1}|P_{2}$ presents a typical deadlock situation, where
$\ell_{1}$ is needed to release $\ell_{2}$ and conversely.

On the other hand, process $P_{3}\stackrel{{\scriptstyle\rm
def}}{{=}}\ell_{1}.(\overline{\ell_{1}}|\overline{\ell_{2}})~{}|~{}\ell_{2}.\overline{\ell_{2}}~{}|~{}\ell_{1}.\overline{\ell_{1}}$
can be typed: we can derive
$\\{\gamma_{12}\\};\\{\ell_{2}\\}\vdash\ell_{1}.(\overline{\ell_{1}}|\overline{\ell_{2}})$
and
$\\{\\{\ell_{1}\\},\\{\ell_{2}\\}\\};\emptyset\vdash\ell_{2}.\overline{\ell_{2}}~{}|~{}\ell_{1}.\overline{\ell_{1}}$,
and we can compose these typing derivations, yielding
$\\{\gamma_{12}\\};\\{\ell_{2}\\}\vdash P_{3}$. Crucially, components
$\\{\ell_{1}\\}$ and $\\{\ell_{2}\\}$ are not merged in the second derivation
for the composition to be possible. Using similar ideas, we can define a
typable process made of three parallel components $P_{1},P_{2},P_{3}$ sharing
a single lock, say $\ell$, as long as each of the $P_{i}$ uses its own locks
besides $\ell$.

We can derive $\\{\gamma_{12}\\};\emptyset\vdash P_{4}$ with
$P_{4}\stackrel{{\scriptstyle\rm
def}}{{=}}\ell_{1}.\ell_{2}.(\overline{\ell_{2}}|\overline{\ell_{1}})$. We
observe that $P_{4}|P_{4}$ cannot be typed, although $P_{4}|P_{4}$ is ‘no more
deadlocked’ than $P_{4}$ alone.

The typing rules enforce $\mathbb{R}\subseteq\mathrm{dom}(\Gamma)$ when
deriving $\Gamma;\mathbb{R}\vdash P$. We say that $\ell$ is _available_ in
process $P$ if $P$ contains a release of $\ell$ which is not under an acquire
on $\ell$ in $P$. Intuitively, when $\Gamma;\mathbb{R}\vdash P$ is derivable,
$P$ is a well-typed process in which all lock names in $\mathbb{R}$ are
available in $P$. The type system thus guarantees a linearity property on the
release of names in $\mathbb{R}$. However, lock names are not _linear names_
in the sense of [16], since there can be arbitrarily many acquire operations
on a given lock. When all free lock names are available in $P$, i.e.
$\Gamma;\mathrm{fln}(P)\vdash P$, we say that $P$ is _complete_.

######  Lemma 2.

The type system enjoys invariance under $\equiv$ and subject reduction: $(i)$
If $\Gamma;\mathbb{R}\vdash P$ and $P\equiv P^{\prime}$, then
$\Gamma;\mathbb{R}\vdash P^{\prime}$. $(ii)$ If $\Gamma;\mathbb{R}\vdash P$
and $P\xrightarrow{}P^{\prime}$, then $\Gamma;\mathbb{R}\vdash P^{\prime}$ and
$\mathrm{fln}(P^{\prime})=\mathrm{fln}(P)$.

##### Deadlock-Freedom.

Intuitively, a deadlock in $\mathrm{CCS}\ell$ arises from an acquire operation
that cannot be performed. We say that a _terminated process_ is a parallel
composition of release operations possibly under some restrictions. A process
that contains at least an acquire and cannot reduce is a _stuck process_. So
in particular $\ell.\overline{\ell}$ is stuck; the context may provide a
release of $\ell$, triggering the acquire on $\ell$. On the other hand, if $P$
is a stuck process and complete, then $P$ is _deadlocked_ : intuitively, the
context cannot interact with $P$ in order to trigger an acquire operation of
$P$. Process $P_{\mathsf{dl}}$ from Section 1 is an example of a deadlock. We
show that a complete process can only reduce to a terminated process, avoiding
deadlocks.

The proof of deadlock-freedom for $\mathrm{CCS}\ell$ provides the structure of
the proofs for deadlock-freedom in $\pi\mathrm{\ell}$ and leak-freedom in
$\pi\mathrm{\ell w}$. It relies on progress: any typable process can reduce to
reach a terminated process. We first present some lemmas related to the
absence of cyclic structures in $\mathrm{CCS}\ell$.

######  Lemma 3 (Lock-connected processes).

We say that $P$ is _lock-connected_ if $\Gamma;\mathbb{R}\vdash P$ implies
$\Gamma=\Gamma^{\prime},\gamma$ for some $\Gamma^{\prime},\gamma$, with
$\mathrm{fln}(P)\subseteq\gamma$. In this situation, we also have
$\\{\gamma\\};\mathbb{R}\vdash P$. If $P$ and $Q$ are lock-connected and
$\mathrm{fln}(P)\cap\mathrm{fln}(Q)$ contains at least two distinct names,
then $P|Q$ cannot be typed.

The property in Lemma 3 does not hold if $P$ and $Q$ are not lock-connected:
take for instance
$P=Q=\ell_{1}.\overline{\ell_{1}}|\ell_{2}.\overline{\ell_{2}}$, then we can
derive $\\{\\{\ell_{1}\\},\\{\ell_{2}\\}\\};\emptyset\vdash P|Q$. By the
typing rule Acq-C, any process of the form $\ell.P$ is lock-connected. A
typical example of a lock-connected process is
$\ell_{1}.(\overline{\ell_{1}}|\overline{\ell_{2}})|\ell_{2}.(\overline{\ell_{2}}|\overline{\ell_{3}})$:
here $\gamma=\\{\ell_{1},\ell_{2},\ell_{3}\\}$. Processes similar to this one
are used in the following lemma.

######  Lemma 4 (No cycle).

We write $P\stackrel{{\scriptstyle\ell}}{{\longleftrightarrow}}Q$ when
$\ell\in\mathrm{fln}(P)\cap\mathrm{fln}(Q)$. Suppose there are $k>1$ pairwise
distinct names $\ell_{1},\dots,\ell_{k}$, and processes $P_{1},\dots,P_{k}$
such that
$\ell_{i}.P_{i}\stackrel{{\scriptstyle\ell_{i}}}{{\longleftrightarrow}}\ell_{(i+1)\\!\mod
k}.P_{(i+1)\\!\mod k}$ for $1\leq i\leq k$. Then $P_{1}|\dots|P_{k}$ is not
typable.

We use notation $\prod_{i}P_{i}$ for the parallel composition of processes
$P_{i}$.

######  Lemma 5 (Progress).

If $\Gamma;\mathrm{fln}(P)\vdash P$, then either $P\xrightarrow{}P^{\prime}$
for some $P^{\prime}$, or
$P\equiv(\boldsymbol{\nu}\widetilde{\ell})\prod_{i}\overline{\ell_{i}}$ where
the $\ell_{i}$s are pairwise distinct.

###### Proof.

Write $P\equiv(\boldsymbol{\nu}\widetilde{\ell})P_{0}\text{ with
}P_{0}=\prod_{i}\overline{\ell_{i}}~{}|~{}\prod_{j}\ell_{j}.P_{j}$. We let
$Q_{j}$ stand for $\ell_{j}.P_{j}$, and suppose that there is at least one
$Q_{j}$. We show that under this hypothesis $P_{0}$ can reduce.

If $\ell_{i}=\ell_{j}$ for some $i,j$, then $P_{0}$ can reduce. We suppose in
the following that this is not the case, and consider one of the $Q_{j}$s. By
typing, there exists a unique occurrence of $\ell_{j}$ available in $P_{0}$.
By hypothesis, this occurrence is not among the $\overline{\ell_{i}}$s.
Therefore, $\ell_{j}$ is available in $Q_{j^{\prime}}$ for some unique
$j^{\prime}$ with $j\neq j^{\prime}$.

We construct a graph having one vertex for each of the $Q_{j}$s. We draw an
edge between $Q_{j}$ and $Q_{j^{\prime}}$ when $\ell_{j}$ is available in
$Q_{j^{\prime}}$. By the reasoning we just made, each vertex is related to at
least one other vertex. So the graph necessarily contains a cycle. We can
apply Lemma 4 to derive a contradiction.

We make two remarks about the construction of the graph. First, two $Q_{j}$s
may start with an acquire at the same name. The corresponding vertices will
have edges leading to the same $Q_{j^{\prime}}$, and the construction still
works. Second, if there is only one $Q_{j}$, then the available release of
$\ell_{j}$ can synchronise with $Q_{j}$. ∎

By Lemma 5, we have that any typable process is not deadlocked. Thus, by
subject reduction, we can prove deadlock-freedom.

######  Proposition 6 (Deadlock-freedom).

If $\Gamma;\mathbb{R}\vdash P$ and $P\xRightarrow{}P^{\prime}$, then
$P^{\prime}$ is not deadlocked.

######  Remark 7.

As $\mathrm{CCS}\ell$ is finite, deadlock-freedom ensures that no acquire
operation waits forever in a complete typable process, and every complete
process reduces to a terminated process: if $\Gamma;\mathrm{fln}(P)\vdash P$,
then
$P\xRightarrow{}(\boldsymbol{\nu}\widetilde{\ell})\prod_{i}\overline{\ell_{i}}$
where the $\ell_{i}$s are pairwise distinct.

###  2.2 $\pi\mathrm{\ell}$: Deadlock-Freedom for Higher-Order Locks

##### Syntax and Operational Semantics of $\pi\mathrm{\ell}$.

$\pi\mathrm{\ell}$ extends $\mathrm{CCS}\ell$ with the possibility to store
_values_ , which can be either booleans or locks, in locks. In this sense,
$\pi\mathrm{\ell}$ features higher-order locks. Processes in
$\pi\mathrm{\ell}$ are defined as follows: P ::=
$\ell(\ell^{\prime})$.P$~{}\big{|}~{}$$\overline{\ell}\langle
v\rangle$$~{}\big{|}~{}$($\boldsymbol{\nu}$ℓ)P$~{}\big{|}~{}$P_1—P_2$~{}\big{|}~{}$$\bm{0}$$~{}\big{|}~{}$[v=v’]P_1,P_2
. $v,v^{\prime}$ denote _values_ , defined by
$v~{}::=~{}\ell~{}\big{|}~{}\mathtt{b}$, where
$\mathtt{b}~{}::=~{}\mathsf{tt}~{}\big{|}~{}\mathsf{ff}$ is a boolean value.
In addition to $\ell,\ell^{\prime}\dots$, we sometimes use also $x,y\dots$ to
range over lock names, to suggest a specific usage, like, e.g. in $\ell(x).P$.

Process $\overline{\ell}\langle\ell^{\prime}\rangle$ is a _release of $\ell$_,
and $\ell(\ell^{\prime}).P$ is an _acquire on $\ell$_; we say in both cases
that $\ell$ is the _subject_ (or that $\ell$ occurs in subject position) and
$\ell^{\prime}$ is the _object_. Restriction and the acquire prefix act as
binders, giving rise to the notion of bound and free names. As in
$\mathrm{CCS}\ell$, we write $\mathrm{fln}(P)$ for the set of free lock names
of $P$. $P\\{\raisebox{2.15277pt}{\small$v$}\\!/\\!\mbox{\small$\ell$}\\}$ is
the process obtained by replacing every free occurrence of $\ell$ with $v$ in
$P$. We say that an occurrence of a process $Q$ in $P$ is _guarded_ if the
occurrence is under an acquire prefix, otherwise it is said _at top-level_ in
$P$. Additional operators w.r.t. $\mathrm{CCS}\ell$ are the inactive process,
$\bm{0}$, and value comparison: $[v=v^{\prime}]P_{1},P_{2}$ behaves like
$P_{1}$ if values $v$ and $v^{\prime}$ are equal, and like $P_{2}$ otherwise.

Structural congruence in $\pi\mathrm{\ell}$ is defined by adding the following
axioms to $\equiv$ in $\mathrm{CCS}\ell$: [] P—$\bm{0}$ ≡ P

($\boldsymbol{\nu}$$\ell$)$\bm{0}$ ≡ $\bm{0}$

[v=v]P_1,P_2 ≡ P_1

[v=v’]P_1,P_2 ≡ P_2 if v≠v’ The last axiom above cannot be used under an
acquire prefix: see Appendix A.3 for the definition of $\equiv$. _Execution
contexts_ , are defined by
$E~{}::=~{}[\cdot]~{}\big{|}~{}E|P~{}\big{|}~{}(\boldsymbol{\nu}\ell)E$. The
axiom for reduction in $\pi\mathrm{\ell}$ is: $\overline{\ell}\langle
v\rangle$ — $\ell(\ell^{\prime})$.P →
P$\\{\raisebox{2.15277pt}{\small$v$}\\!/\\!\mbox{\small$\ell^{\prime}$}\\}$

$\xRightarrow{}$ is the reflexive transitive closure of $\xrightarrow{}$.
Labelled transitions, written $P\xrightarrow{\mu}P^{\prime}$, use actions
$\mu$ defined by $\mu~{}::=~{}\ell(v)~{}\big{|}~{}\overline{\ell}\langle
v\rangle~{}\big{|}~{}\overline{\ell}(\ell^{\prime})~{}\big{|}~{}\tau$, and are
standard [27]—we recall the definition in Appendix A.3.

##### The type system.

We enforce a sorting discipline for names [18], given by
$V::=\mathsf{bool}~{}\big{|}~{}L$ and $\Sigma(L)=V$: values, that are stored
in locks, are either booleans or locks. We consider that all processes we
write obey this discipline, which is left implicit. This means for instance
that when writing $\overline{\ell}\langle v\rangle$, $\ell$ and $v$ have
appropriate sorts; and similarly for $\ell(\ell^{\prime}).P$. In
$[v=v^{\prime}]P_{1},P_{2}$, we only compare values with the same sort.

[Acq] $\Gamma,({\gamma,\ell,\ell^{\prime}});\mathbb{R},\ell\vdash P$
$\\{\mathsf{flatten}(\Gamma)\uplus(\gamma,\ell)\\};\mathbb{R}\vdash\ell(\ell^{\prime}).P$

[Rel] $\Gamma,(\gamma,\ell,v);\\{\ell\\}\vdash\overline{\ell}\langle v\rangle$

[New]$\Gamma,(\gamma,\ell);\mathbb{R},\ell\vdash P$
$\Gamma,\gamma;\mathbb{R}\vdash(\boldsymbol{\nu}\ell)P$
[Par]$\Gamma_{1};\mathbb{R}_{1}\vdash P_{1}$$\Gamma_{2};\mathbb{R}_{2}\vdash
P_{2}$ $\Gamma_{1}\bullet\Gamma_{2};\mathbb{R}_{1}\uplus\mathbb{R}_{2}\vdash
P_{1}|P_{2}$

[Mat]$\Gamma;\mathbb{R}\vdash P_{1}$ $\Gamma;\mathbb{R}\vdash P_{2}$
$\Gamma;\mathbb{R}\vdash[v=v^{\prime}]P_{1},P_{2}$

Figure 1: Typing rules for $\pi\mathrm{\ell}$

The typing judgement is written $\Gamma;\mathbb{R}\vdash P$, where $\Gamma$
and $\mathbb{R}$ are defined like for $\mathrm{CCS}\ell$. We adopt the
convention that if $v$ is a boolean value, then $\gamma,v$ is just $\gamma$,
and similarly, $\gamma,\ell$ is just $\gamma$ if the sort of $\ell$ is
$\mathsf{bool}$. The operation $\Gamma_{1}\bullet\Gamma_{2}$ is the same as
for $\mathrm{CCS}\ell$.

The typing rules for $\pi\mathrm{\ell}$ are presented in Figure 1. Again, in
rules Acq and New, writing $\mathbb{R},\ell$ imposes $\ell\notin\mathbb{R}$,
otherwise the rule cannot be applied. Similarly, the notation
$\gamma,\ell,\ell^{\prime}$ is only defined when
$\gamma\\#\\{\ell,\ell^{\prime}\\}$ and $\ell\neq\ell^{\prime}$. Rule Rel
describes the release of a lock containing either a lock or a boolean value:
in the latter case, using the convention above, the conclusion of the rule is
$\\{\\{\ell\\}\\};\\{\ell\\}\vdash\overline{\ell}\langle\mathtt{b}\rangle$. In
rules Acq and Rel, the subject and the object of the operation should belong
to the same component. In $\mathrm{CCS}\ell$, only prefixing yields such a
constraint.

In rule Mat, we do not impose $\\{v,v^{\prime}\\}\in\mathrm{dom}(\Gamma)$. A
typical example of a process that uses name comparison is
$[\ell_{1}=\ell_{2}]\overline{\ell}\langle\mathsf{tt}\rangle,\overline{\ell}\langle\mathsf{ff}\rangle$:
in this process, $\ell_{1}$ and $\ell_{2}$ intuitively represent no threat of
a deadlock.

Before presenting the properties of the type system, we make some comments on
the discipline it imposes on $\pi$-calculus names when they are used as locks.

######  Remark 8 (An acquired lock cannot be stored).

In $\pi\mathrm{\ell}$, the obligation to release a lock cannot be transmitted.
Accordingly, $\ell^{\prime}\notin\mathbb{R}=\\{\ell\\}$ in rule Rel, and a
process like $\ell(\ell^{\prime}).\overline{\ell_{1}}\langle\ell\rangle$
cannot be typed. We return to this point after Proposition 11.

######  Remark 9 (Typability of higher-order locks).

Locks are a particular kind of names of the asynchronous $\pi$-calculus
(A$\pi$). Acquiring a lock that has been stored in another lock boils down to
performing a communication in A$\pi$. We discuss how such communications can
occur between typed processes.

In rule Rel, $\ell$ and $\ell^{\prime}$ must belong to the same component of
$\Gamma$. So intuitively, if a process contains
$\overline{\ell}\langle\ell^{\prime}\rangle$, this release is the only place
where these locks are used ‘together’. A reduction involving a well-typed
process containing this release therefore looks like
($\overline{\ell}\langle\ell^{\prime}\rangle$— P) — (ℓ(x).Q—Q’) → P —
Q$\\{\raisebox{2.15277pt}{\small$\ell^{\prime}$}\\!/\\!\mbox{\small$x$}\\}$ —
Q’ . Parentheses are used to suggest an interaction between two processes;
$\overline{\ell}\langle\ell^{\prime}\rangle|P$ performs the release, and
$\ell(x).Q|Q^{\prime}$ performs the acquire. Process $P$, which intuitively is
the continuation of the release, may use locks $\ell$ and $\ell^{\prime}$, but
not together, and similarly for $Q^{\prime}$. For instance we may have
$P=P_{\ell}|P_{\ell^{\prime}}$, where $\ell^{\prime}$ does not occur in
$P_{\ell}$, and vice-versa for $P_{\ell^{\prime}}$. Note also that
$\ell^{\prime}$ is necessarily fresh for $\ell(x).Q^{\prime}$: otherwise,
typability of $\ell(x).Q^{\prime}$ would impose $\ell$ and $\ell^{\prime}$ to
be in the same component, which would forbid the parallel composition with
$\overline{\ell}\langle\ell^{\prime}\rangle$.

Depending on how $P,Q$ and $Q^{\prime}$ are written, we can envisage several
patterns of usages of locks $\ell$ and $\ell^{\prime}$. A first example is
ownership transfer (or delegation): $\ell^{\prime}\notin\mathrm{fln}(P)$, that
is, $P$ renounces usage of $\ell^{\prime}$. $\ell^{\prime}$ can be used in
$Q$. Note that typing actually also allows
$\ell^{\prime}\in\mathrm{fln}(Q^{\prime})$, i.e., the recipient already knows
$\ell^{\prime}$.

A second possibility could be that $\ell$ is used linearly, in the sense that
there is exactly one acquire on $\ell$. In this case, we necessarily have
$\ell\notin\mathrm{fln}(P)\cup\mathrm{fln}(Q^{\prime})$—note that a release of
$\ell$ is available in $Q$, by typing. Linearity of $\ell$ means here that
exactly one interaction takes place at $\ell$. After that interaction, the
release on $\ell$ contained in $Q$ is _inert_ , in the sense that no acquire
can synchronise with it. We believe that this form of linearity can be used to
encode binary session types in an extended version of $\pi\mathrm{\ell}$,
including variants and polyadicity, along the lines of [15, 4, 5].

The type system for $\pi\mathrm{\ell}$ satisfies the same properties as in
$\mathrm{CCS}\ell$ (Lemma 2): invariance under structural congruence, merging
components and subject reduction. We also have progress and deadlock-freedom:

######  Lemma 10 (Progress).

Suppose $\Gamma;\mathrm{fln}(P)\vdash P$, and $P$ is not structurally
equivalent to $\bm{0}$. Then

  * •

either there exists $P^{\prime}$ such that $P\rightarrow P^{\prime}$,

  * •

or
$P\equiv(\boldsymbol{\nu}\widetilde{\ell})(\Pi_{i}\overline{\ell_{i}}v_{i})$
where the $\ell_{i}$s are pairwise distinct.

Like in $\mathrm{CCS}\ell$, a deadlocked process in $\pi\mathrm{\ell}$ is
defined as a complete process that is stuck.

######  Proposition 11 (Deadlock-freedom).

If $\Gamma;\mathbb{R}\vdash P$ and $P\xRightarrow{}P^{\prime}$, then
$P^{\prime}$ is not deadlocked.

The proof of deadlock-freedom is basically the same as for $\mathrm{CCS}\ell$.
The reason for that is that although the object part of releases plays a role
in the typing rules, it is not relevant to establish progress (Lemma 10). This
is the case because in $\pi\mathrm{\ell}$, it is not possible to store an
acquired lock in another lock (Remark 8).

It seems difficult to extend the type system in order to allow processes that
transmit the release obligation on a lock. This would make it possible to
type-check, e.g., process
$\ell(\ell^{\prime}).\overline{\ell_{1}}\langle\ell\rangle$, that does not
release lock $\ell$ but instead stores it in $\ell_{1}$. Symmetrically, a
process accessing $\ell$ at $\ell_{1}$ would be in charge of releasing both
$\ell_{1}$ and $\ell$. In such a framework, a process like
$(\boldsymbol{\nu}\ell_{1})(\overline{\ell_{1}}\langle\ell\rangle|\ell(x).\overline{\ell}\langle
x\rangle)$ would be deadlocked, because the inert release
$\overline{\ell_{1}}\langle\ell\rangle$ contains the release obligation on
$\ell_{1}$. The type system in Section 3 makes it possible to transmit the
obligation to perform a release (and similarly for a wait).

######  Remark 12.

Similarly to Remark 7, we have that $\Gamma;\mathrm{fln}(P)\vdash P$ implies
$P\xRightarrow{}(\boldsymbol{\nu}\widetilde{\ell})(\Pi_{i}\overline{\ell_{i}}v_{i})$
where the $\ell_{i}$s are pairwise distinct. As a consequence, the following
holds: if $\Gamma;\mathrm{fln}(P)\vdash P$, then for any
$\ell\in\mathrm{fln}(P)$, $P\xRightarrow{}\xrightarrow{\mu}$, where $\mu$ is a
release of $\ell$. This statement would be better suited if infinite
computations were possible in $\pi\mathrm{\ell}$. We leave the investigation
of such an extension of $\pi\mathrm{\ell}$ for future work.

###  2.3 Behavioural Equivalence in $\pi\mathrm{\ell}$

We introduce typed barbed equivalence ($\simeq$) and typed bisimilarity
($\approx$) for $\pi\mathrm{\ell}$. We show that $\approx$ is a sound
technique to establish $\simeq$, and present several examples of
(in)equivalences between $\pi\mathrm{\ell}$ processes.

####  2.3.1 Barbed Equivalence and Labelled Semantics for $\pi\mathrm{\ell}$

A typed relation in $\pi\mathrm{\ell}$ is a set of quadruples of the form
$(\Gamma,\mathbb{R},P,Q)$ such that $\Gamma;\mathbb{R}\vdash P$ and
$\Gamma;\mathbb{R}\vdash Q$. When a typed relation $\mathcal{R}$ contains
$(\Gamma,\mathbb{R},P,Q)$, we write $\Gamma;\mathbb{R}\vdash P\mathcal{R}Q$.
We say that a typed relation $\mathcal{R}$ is symmetric if
$\Gamma;\mathbb{R}\vdash P\mathcal{R}Q$ implies $\Gamma;\mathbb{R}\vdash
Q\mathcal{R}P$.

Deadlock-freedom has two consequences regarding the definition of barbed
equivalence in $\pi\mathrm{\ell}$, noted $\simeq$. First, only complete
processes should be observed, because intuitively a computation in
$\pi\mathrm{\ell}$ should not be blocked by an acquire operation that cannot
be executed.

Second, Proposition 11 entails that all weak barbs in the sense of A$\pi$ can
always be observed in $\pi\mathrm{\ell}$. In A$\pi$, a weak barb at $n$
corresponds to the possibility to reduce to a process in which an output at
channel $n$ occurs at top-level. We need a stronger notion of barb, otherwise
$\simeq$ would be trivial. That behavioural equivalence in $\pi\mathrm{\ell}$
is not trivial is shown for instance by the presence of non-determinism.
Consider indeed process $P_{c}\stackrel{{\scriptstyle\rm
def}}{{=}}(\boldsymbol{\nu}\ell)\big{(}\,\ell(x).(\overline{c}\langle
x\rangle|\overline{\ell}\langle
x\rangle)~{}|~{}\ell(y).\overline{\ell}\langle\mathsf{ff}\rangle~{}|~{}\overline{\ell}\langle\mathsf{tt}\rangle\,\big{)}$.
Then $P_{c}\xRightarrow{}\overline{c}\langle\mathsf{tt}\rangle$ and
$P_{c}\xRightarrow{}\overline{c}\langle\mathsf{ff}\rangle$ (up to the
cancellation of an inert process of the form
$(\boldsymbol{\nu}\ell)\overline{\ell}\langle\mathtt{b}\rangle$). We therefore
include the object part of releases in barbs. We write
$P\downarrow_{\overline{\ell}\langle\ell^{\prime}\rangle}$ if
$P\xrightarrow{\overline{\ell}\langle\ell^{\prime}\rangle}$, and
$P\downarrow_{\overline{\ell}(\boldsymbol{\nu})}$ if
$P\xrightarrow{\overline{\ell}(\ell^{\prime})}$. We use $\eta$ to range over
barbs, writing $P\downarrow_{\eta}$; the weak version of the predicate,
defined as $\xRightarrow{}\downarrow_{\eta}$, is written $P\Downarrow_{\eta}$.

######  Definition 13 (Barbed equivalence in $\pi\mathrm{\ell}$, $\simeq$).

A symmetric typed relation $\mathcal{R}$ is a _typed barbed bisimulation_ if
$\Gamma;\mathbb{R}\vdash P\mathcal{R}Q$ implies the three following
properties:

  1. 1.

whenever $P,Q$ are complete and $P\xrightarrow{}P^{\prime}$, there is
$Q^{\prime}$ s.t. $Q\xRightarrow{}Q^{\prime}$ and $\Gamma;\mathbb{R}\vdash
P^{\prime}\mathcal{R}Q^{\prime}$;

  2. 2.

for any $\eta$, if $P,Q$ are complete and $P\downarrow_{\eta}$ then
$Q\Downarrow_{\eta}$;

  3. 3.

for any $E,\Gamma^{\prime},\mathbb{R}^{\prime}$ s.t.
$\Gamma^{\prime};\mathbb{R}^{\prime}\vdash E[P]$ and
$\Gamma^{\prime};\mathbb{R}^{\prime}\vdash E[Q]$, and $E[P],E[Q]$ are
complete, we have $\Gamma^{\prime};\mathbb{R}^{\prime}\vdash
E[P]\,\mathcal{R}\,E[Q]$.

_Typed barbed equivalence_ , written $\simeq$, is the greatest typed barbed
bisimulation.

######  Lemma 14 (Observing only booleans).

We use $o,o^{\prime},\dots$ for lock names that are used to store boolean
values. We define $\simeq_{o}$ as the equivalence defined as in Definition 13,
but restricting the second clause to barbs of the form
$\downarrow_{\overline{o}\langle\mathtt{b}\rangle}$ and
$\Downarrow_{\overline{o}\langle\mathtt{b}\rangle}$. Relation $\simeq_{o}$
coincides with $\simeq$.

To define typed bisimilarity, we introduce _type-allowed transitions_. The
terminology means that we select among the untyped transitions those that are
fireable given the constraints imposed by types.

######  Definition 15 (Type-allowed transitions).

When $\Gamma;\mathbb{R}\vdash P$, we write
$[\Gamma;\mathbb{R};P]\xrightarrow{\mu}[\Gamma^{\prime};\mathbb{R}^{\prime};P^{\prime}]$
if $P\xrightarrow{\mu}P^{\prime}$ and one of the following holds:

  1. 1.

$\mu=\tau$, in which case $\mathbb{R}^{\prime}=\mathbb{R}$ and
$\Gamma^{\prime}=\Gamma$;

  2. 2.

$\mu=\overline{\ell}\langle v\rangle$, in which case
$(\gamma,\ell,v)\in\Gamma$ for some $\gamma$, and
$\mathbb{R}^{\prime},\ell=\mathbb{R}$, $\Gamma^{\prime}=\Gamma$;

  3. 3.

$\mu=\overline{\ell}(\ell^{\prime})$, in which case
$\Gamma=\Gamma_{0},(\gamma,\ell)$ for some $\Gamma_{0},\gamma$,
$\Gamma^{\prime}=\Gamma_{0},(\gamma,\ell,\ell^{\prime})$, and we have
$\mathbb{R}^{\prime},\ell=\mathbb{R},\ell^{\prime}$;

  4. 4.

$\mu=\ell(v)$, in which case there are $\Gamma_{0},\mathbb{R}_{0}$ s.t.
$\Gamma_{0};\mathbb{R}_{0}\vdash P|\overline{\ell}\langle v\rangle$, and
$\Gamma^{\prime}=\Gamma_{0},\mathbb{R}^{\prime}=\mathbb{R}_{0}$.

In item 3, $\ell$ is removed from the $\mathbb{R}$ component, and
$\ell^{\prime}$ is added: it is $P^{\prime}$’s duty to perform the release of
$\ell^{\prime}$, the obligation is not transmitted. An acquire transition
involving a higher-order lock merges two distinct components in the typing
environment: if
$[\Gamma_{0},(\gamma,\ell),(\gamma^{\prime},\ell^{\prime});\mathbb{R};P]\xrightarrow{\ell(\ell^{\prime})}[\Gamma^{\prime};\mathbb{R}^{\prime};P^{\prime}]$
(item 4 above), then
$\Gamma^{\prime}=\Gamma_{0},(\gamma\uplus\gamma^{\prime}\uplus\\{\ell,\ell^{\prime}\\})$
and $\mathbb{R}^{\prime}=\mathbb{R},\ell$ (and in particular
$\ell\notin\mathbb{R}$).

######  Lemma 16 (Subject Reduction for type-allowed transitions).

If
$[\Gamma;\mathbb{R};P]\xrightarrow{\mu}[\Gamma^{\prime};\mathbb{R}^{\prime};P^{\prime}]$,
then $\Gamma^{\prime};\mathbb{R}^{\prime}\vdash P^{\prime}$.

######  Definition 17 (Typed bisimilarity, $\approx$).

A typed relation $\mathcal{R}$ is a typed bisimulation if
$\Gamma;\mathbb{R}\vdash P\mathcal{R}Q$ implies that whenever
$[\Gamma;\mathbb{R};P]\xrightarrow{\mu}[\Gamma^{\prime};\mathbb{R}^{\prime};P^{\prime}]$,
we have

  1. 1.

either $Q\xRightarrow{\hat{\mu}}Q^{\prime}$ and
$\Gamma^{\prime};\mathbb{R}^{\prime}\vdash P^{\prime}\mathcal{R}Q^{\prime}$
for some $Q^{\prime}$

  2. 2.

or $\mu$ is an acquire $\ell(v)$, $Q|\overline{\ell}\langle
v\rangle\xRightarrow{}Q^{\prime}$ and
$\Gamma^{\prime};\mathbb{R}^{\prime}\vdash P^{\prime}\mathcal{R}Q^{\prime}$
for some $Q^{\prime}$,

and symmetrically for the type-allowed transitions of $Q$.

_Typed bisimilarity_ , written $\approx$, is the largest typed bisimulation.

We write $\Gamma;\mathcal{R}\vdash P\approx Q$ when
$(\Gamma;\mathbb{R},P,Q)\in\,\approx$. If $\Gamma;\mathbb{R}\vdash P\approx Q$
does not hold, we write $\Gamma;\mathbb{R}\vdash P\not\approx Q$, and
similarly for $\Gamma;\mathbb{R}\vdash P\not\simeq Q$.

Proposition 18 below states that relation $\approx$ provides a sound proof
technique for $\simeq$. The main property to establish this result is that
$\approx$ is preserved by parallel composition:
$\Gamma_{0};\mathbb{R}_{0}\vdash P\approx Q$ implies that for all $T$,
whenever $\Gamma;\mathbb{R}\vdash P|T$ and $\Gamma;\mathbb{R}\vdash Q|T$, we
have $\Gamma;\mathbb{R}\vdash P|T\approx Q|T$.

######  Proposition 18 (Soundness).

For any $\Gamma,\mathbb{R},P,Q$, if $\Gamma;\mathbb{R}\vdash P\approx Q$, then
$\Gamma;\mathbb{R}\vdash P\simeq Q$.

The main advantage in using $\approx$ to establish equivalences for $\simeq$
is that we can reason directly on processes, even if they are not complete.

####  2.3.2 Examples of Behavioural Equivalence in $\pi\mathrm{\ell}$

######  Example 19.

We discuss some equivalences for $\simeq$.

The equivalence
$\\{\\{\ell\\}\\};\emptyset\vdash\ell(x).\overline{\ell}\langle
x\rangle\simeq\bm{0}$, which is typical of A$\pi$, holds in
$\pi\mathrm{\ell}$. This follows directly from the definition of typed
bisimilarity, and soundness (Proposition 18).

We now let $P\stackrel{{\scriptstyle\rm
def}}{{=}}\ell(x).(\overline{\ell_{0}}\langle\mathsf{tt}\rangle|\overline{\ell}\langle
x\rangle)$ and $Q\stackrel{{\scriptstyle\rm
def}}{{=}}\overline{\ell_{0}}\langle\mathsf{tt}\rangle$, and consider whether
we can detect the presence of a ‘forwarder’ at $\ell$ when its behaviour is
interleaved with another process. $P$ and $Q$ have different barbs—they are
obviously not complete. It turns out that
$\\{\\{\ell,\ell_{0}\\}\\};\\{\ell_{0}\\}\vdash\ell(x).(\overline{\ell_{0}}\langle\mathsf{tt}\rangle|\overline{\ell}\langle
x\rangle)\not\simeq\overline{\ell_{0}}\langle\mathsf{tt}\rangle$. Indeed, let
us consider the context

$E\,\stackrel{{\scriptstyle\rm
def}}{{=}}\,[\cdot]~{}|~{}\ell_{0}(y).w(\\_).(\overline{w}\langle\mathsf{tt}\rangle|\overline{\ell_{0}}\langle
y\rangle)~{}|~{}w^{\prime}(\\_).(\overline{w^{\prime}}\langle\mathsf{tt}\rangle|\overline{\ell}\langle
v\rangle)~{}|~{}\overline{w}\langle\mathsf{ff}\rangle|\overline{w^{\prime}}\langle\mathsf{ff}\rangle,$

where $w,w^{\prime}$ are fresh names and $v$ is a value of the appropriate
sort. We have $E[Q]\xRightarrow{}Q^{\prime}$ with
$Q^{\prime}\not\downarrow_{\overline{w}\langle\mathsf{ff}\rangle}$ and
$Q^{\prime}\downarrow_{\overline{w^{\prime}}\langle\mathsf{ff}\rangle}$. On
the other hand, for any $P^{\prime}$ s.t. $E[P]\xRightarrow{}P^{\prime}$, if
$P^{\prime}\not\downarrow_{\overline{w}\langle\mathsf{ff}\rangle}$, then
$P^{\prime}\not\downarrow_{\overline{w^{\prime}}\langle\mathsf{ff}\rangle}$.

Contexts like $E$ above make it possible to detect when the process in the
hole has some interaction (here, with locks $\ell$ and $\ell_{0}$).

Using similar ideas, we can prove that

$\Gamma;\mathbb{R}\vdash\ell_{1}(x).\ell_{2}(y).P~{}\not\simeq~{}\ell_{2}(y).\ell_{1}(x).P\qquad\text{
for appropriate $\Gamma${} and $\mathbb{R}$.}$

Indeed, let us define $E_{w}\,\stackrel{{\scriptstyle\rm
def}}{{=}}\,\overline{w}\langle\mathsf{ff}\rangle~{}|~{}w(\\_).([\cdot]|\overline{w}\langle\mathsf{tt}\rangle)$,
where $\\_$ stands for an arbitrary lock name, that is not used. We can use
the context $[\cdot]~{}|~{}E_{w_{2}}[\overline{\ell_{2}}\langle
v_{2}\rangle]~{}|~{}\overline{\ell_{1}}\langle
v_{1}\rangle~{}|~{}\ell_{1}(z).E_{w_{1}}[\overline{\ell_{1}}\langle
z\rangle]$, for fresh names $w_{1},w_{2}$ and appropriate values
$v_{1},v_{2}$, to detect the order in which acquires on $\ell_{1}$ and
$\ell_{2}$ are made.

In the next two examples, we show equivalences that hold because we work in a
typed setting.

######  Example 20.

Suppose
$\Gamma;\mathbb{R},\ell\vdash\ell(x).P~{}|~{}\ell^{\prime}(y).(\overline{\ell}\langle
v\rangle~{}|~{}Q)$. Then we have $\Gamma;\mathbb{R},\ell\vdash$$\ell(x)$.P —
$\ell^{\prime}(y)$.($\overline{\ell}\langle v\rangle$ — Q) $\approx$
$\ell^{\prime}(y)$.($\overline{\ell}\langle v\rangle$ — Q — $\ell(x)$.P),
because intuitively the acquire on $\ell$ cannot be triggered by the context,
due to the presence of a release at $\ell$ in the process. (We remark in
passing that
$\Gamma;\mathbb{R},\ell\vdash\ell(x).P~{}|~{}\ell^{\prime}(y).(\overline{\ell}\langle
v\rangle~{}|~{}Q)$ iff
$\Gamma;\mathbb{R},\ell\vdash\ell^{\prime}(y).(\overline{\ell}\langle
v\rangle~{}|~{}Q~{}|~{}\ell(x).P)$, and in this case $\Gamma$ contains a
component of the form $(\gamma,\ell,\ell^{\prime},v)$.)

This law can be generalised as follows. We say that $\ell$ is _available_ in a
context $C$ if the hole does not occur in $C$ neither under a binder for
$\ell$, nor under an acquire on $\ell$. So for instance $\ell$ is not
available in $(\boldsymbol{\nu}\ell)[\cdot]$, in $\ell_{0}(\ell).[\cdot]$ or
in $\ell(x).[\cdot]$, and $\ell$ is available in
$\ell(x).\overline{\ell}\langle x\rangle~{}|~{}\overline{\ell}\langle
v\rangle~{}|~{}[\cdot]$. If $\ell$ is available in $C$, then
$\Gamma;\mathbb{R}\vdash$$\ell(x)$.P — C[$\overline{\ell}\langle v\rangle$]
$\approx$C[$\overline{\ell}\langle v\rangle$ — $\ell(x)$.P]  for appropriate
$\Gamma$ and $\mathbb{R}$.

######  Example 21.

Consider the following processes: P_1 = ($\boldsymbol{\nu}$ℓ_1)(
ℓ_1.ℓ_2.($\overline{\ell_{1}}$—$\overline{\ell_{2}}$) —
ℓ(x).ℓ_1.x.($\overline{\ell_{1}}$—$\overline{x}$—$\overline{\ell}\langle
x\rangle$) — $\overline{\ell_{1}}$—$\overline{\ell_{2}}$ )P_2 =
($\boldsymbol{\nu}$ℓ_1)( ℓ_1.ℓ_2.($\overline{\ell_{1}}$—$\overline{\ell_{2}}$)
— ℓ(x).x.ℓ_1.($\overline{\ell_{1}}$—$\overline{x}$—$\overline{\ell}\langle
x\rangle$) — $\overline{\ell_{1}}$—$\overline{\ell_{2}}$ ) Here we use a CCS-
like syntax, to ease readability. This notation means that acquire operations
are used as forwarders, i.e., the first component of $P_{1}$ and $P_{2}$
should be read as $\ell_{1}(y_{1}).\ell_{2}(y_{2}).(\overline{\ell_{1}}\langle
y_{1}\rangle|\overline{\ell_{2}}\langle y_{2}\rangle)$. Moreover, the two
releases available at top-level are
$\overline{\ell_{1}}\langle\mathsf{tt}\rangle|\overline{\ell_{2}}\langle\mathsf{tt}\rangle$,
and similarly for $\overline{x}\langle\mathsf{tt}\rangle$ (the reasoning also
holds if $\ell_{1}$ and $\ell_{2}$ are higher-order locks).

In the pure $\pi$-calculus, $P_{1}$ and $P_{2}$ are not equivalent, because
$\ell_{2}$ can instantiate $x$ in the acquire on $\ell$. We can show
$\\{\\{\ell_{2},\ell\\}\\};\\{\ell_{2}\\}\vdash P_{1}\approx P_{2}$ in
$\pi\mathrm{\ell}$, because the transition $\xrightarrow{\ell(\ell_{2})}$ is
ruled out by the type system.

##  3 $\pi\mathrm{\ell w}$, a Leak-Free Asynchronous $\pi$-Calculus

###  3.1 Adding Lock Deallocation

$\pi\mathrm{\ell w}$ is obtained from $\pi\mathrm{\ell}$ by adding the _wait
construct_ $\ell(\\!(\ell^{\prime})\\!).P$ to the grammar of
$\pi\mathrm{\ell}$. As announced in Section 1, the following reduction rule
describes how wait interacts with a release:
($\boldsymbol{\nu}$$\ell$)($\overline{\ell}\langle v\rangle$ —
$\ell(\\!(\ell^{\prime})\\!)$.P) →
P$\\{\raisebox{2.15277pt}{\small$v$}\\!/\\!\mbox{\small$\ell^{\prime}$}\\}$
$\ell$∉$\mathrm{fln}(P)$ The wait instruction deallocates the lock. The
continuation may use $\ell^{\prime}$, the final value of the lock. We say that
$\ell(\\!(\ell^{\prime})\\!)$ is a _wait on $\ell$_, and $\ell^{\prime}$ is
bound in $\ell(\\!(\ell^{\prime})\\!).P$.

Types in $\pi\mathrm{\ell w}$, written $\mathsf{T},\mathsf{T}^{\prime},\dots$,
are defined by
$\mathsf{T}~{}::=~{}\mathsf{bool}~{}\big{|}~{}\langle\mathsf{T}\rangle_{rw}$,
and _typing hypotheses_ are written $\ell:\mathsf{T}$. In
$\ell:\langle\mathsf{T}\rangle_{rw}$, $rw$ is called the _usage_ of $\ell$,
and $r,w\in\\{0,1\\}$ are the release and wait _obligations_ , respectively,
on lock $\ell$. So for instance a typing hypothesis of the form
$\ell:\langle\mathsf{T}\rangle_{10}$ means that $\ell$ must be used to perform
a release and cannot be used to perform a wait. An hypothesis
$\ell:\langle\mathsf{T}\rangle_{00}$ means that $\ell$ can only be used to
perform acquire operations. This structure for types makes it possible to
transmit the wait and release obligations on a given lock name via higher-
order locks.

Our type system ensures that locks are properly deallocated. In contrast to
$\pi\mathrm{\ell}$, this allows acquired locks to be stored without creating
deadlocks. For example, a process like
$(\boldsymbol{\nu}\ell_{1})(\overline{\ell_{1}}\langle\ell\rangle|\ell(x).\overline{\ell}\langle
x\rangle)$ is deadlocked if $\ell_{1}$ stores the release obligation of
$\ell$; however, it cannot be typed as it lacks the wait on $\ell_{1}$. Adding
a wait, e.g. $\ell_{1}(\\!(\ell)\\!).\overline{\ell}\langle v\rangle$ removes
the deadlock.

Typing environments have the same structure as in Section 2, except that
components $\gamma$ are sets of typing hypotheses instead of simply sets of
lock names. $\mathrm{dom}(\Gamma)$ is defined as the set of lock names for
which $\Gamma$ contains a typing hypothesis. We write
$\Gamma(\ell)=\mathsf{T}$ if the typing hypothesis $\ell:\mathsf{T}$ occurs in
$\Gamma$.

We reuse the notation for composition of typing environments.
$\Gamma_{1}\bullet\Gamma_{2}$ is defined like in Section 2.1, using the
$\mathsf{connect}$ operator, to avoid cyclic structures in the sharing of lock
names. Additionally, when merging components, we compose typing hypotheses.
For any $\ell$, if
$\ell:\langle\mathsf{T}_{1}\rangle_{r_{1}w_{1}}\in\mathrm{dom}(\Gamma_{1})$
and
$\ell:\langle\mathsf{T}_{2}\rangle_{r_{2}w_{2}}\in\mathrm{dom}(\Gamma_{2})$,
the typing hypothesis for $\ell$ in $\Gamma_{1}\bullet\Gamma_{2}$ is
$\ell:\langle\mathsf{T}\rangle_{(r_{1}+r_{2})(w_{1}+w_{2})}$, and is defined
only if $\mathsf{T}=\mathsf{T}_{1}=\mathsf{T}_{2}$, $r_{1}+r_{2}\leq 1$ and
$w_{1}+w_{2}\leq 1$.

[Acq-w]
$\Gamma,(\gamma,\ell:\langle\mathsf{T}\rangle_{1w},\ell^{\prime}:\mathsf{T})\vdash
P$
$\\{\mathsf{flatten}(\Gamma)\uplus(\gamma,\ell:\langle\mathsf{T}\rangle_{0w})\\}\vdash\ell(\ell^{\prime}).P$

[Rel-w]
$\Gamma_{00},(\gamma_{00},\ell:\langle\mathsf{T}\rangle_{10},v:\mathsf{T})\vdash\overline{\ell}\langle
v\rangle$

[Wait-w] $\\{\gamma,\ell^{\prime}:\mathsf{T}\\}\vdash P$
$\\{\gamma,\ell:\langle\mathsf{T}\rangle_{01}\\}\vdash\ell((\ell^{\prime})).P$

[New-w]$\Gamma,(\gamma,\ell:\langle\mathsf{T}\rangle_{11})\vdash P$
$\Gamma,\gamma\vdash(\boldsymbol{\nu}\ell)P$

[Par-w]$\Gamma_{1}\vdash P_{1}$$\Gamma_{2}\vdash P_{2}$
$\Gamma_{1}\bullet\Gamma_{2}\vdash P_{1}|P_{2}$

[Nil-w] $\emptyset\vdash\bm{0}$

[Mat-w]$\Gamma\vdash P_{1}$ $\Gamma\vdash P_{2}$
$\Gamma\vdash[v=v^{\prime}]P_{1},P_{2}$

Figure 2: Typing rules for $\pi\mathrm{\ell w}$

The typing rules are given in Figure 2. The rules build on the rules for
$\pi\mathrm{\ell}$, and rely on usages to control the release and wait
obligations. In particular, the set $\mathbb{R}$ in Figure 1 corresponds to
the set of locks whose usage is of the form $1w$ in this system. To type-check
an acquire, we can have usage $00$, but also $01$, as in, e.g.,
$\ell(\ell^{\prime}).(\overline{\ell}\langle\ell^{\prime}\rangle|\ell(\\!(x)\\!).P)$.
In rule Rel-w, we impose that all typing hypotheses in $\Gamma_{00}$ (resp.
$\gamma_{00}$) have the form $\ell:\langle\mathsf{T}\rangle_{00}$.

Several notions introduced for the type system of Section 2 have to be adapted
in the setting of $\pi\mathrm{\ell w}$. While in Section 2 we simply say that
a lock $\ell$ is available, here we distinguish whether a release of $\ell$ or
a wait on $\ell$ is available. If $P$ has a subterm of the form
$\ell(\\!(x)\\!).Q$ that does not occur under a binder for $\ell$, we say that
a wait on $\ell$ is _available_ in $P$. If $\overline{\ell}\langle v\rangle$
occurs in some process $P$ and this occurrence is neither under a binder for
$\ell$ nor under an acquire on $\ell$, we say that a release of $\ell$ is
_available_ in $P$. In addition, a release of $\ell$ (resp. wait on $\ell$) is
available in $P$ also if $P$ contains a release of the form
$\overline{\ell_{0}}\langle\ell\rangle$, which does not occur under a binder
for $\ell$, and if $\ell$’s type is of the form
$\langle\mathsf{T}\rangle_{1w}$ (resp. $\langle\mathsf{T}\rangle_{r1}$).

Like in $\pi\mathrm{\ell}$, a deadlocked process in $\pi\mathrm{\ell w}$ is a
complete process that is stuck. The notion of complete process has to be
adapted in order to take into account the specificities of $\pi\mathrm{\ell
w}$. First, the process should not be stuck just because a restriction is
missing in order to trigger a name deallocation. Second, we must consider the
fact that release and wait obligations can be stored in locks in
$\pi\mathrm{\ell w}$. As a consequence, when defining complete processes in
$\pi\mathrm{\ell w}$, we impose some constraints on the free lock names of
processes.

In $\pi\mathrm{\ell w}$, we say that _$\Gamma$ is complete_ if for any
$\ell\in\mathrm{dom}(\Gamma)$, either
$\Gamma(\ell)=\langle\mathsf{bool}\rangle_{10}$ or
$\Gamma(\ell)=\langle\langle\mathsf{T}\rangle_{00}\rangle_{10}$ for some
$\mathsf{T}$. To understand this definition, suppose $\Gamma\vdash P$ with
$\Gamma$ complete. Then we have, for any free lock name $\ell$ of $P$: $(i)$
the release of $\ell$ is available in $P$; $(ii)$ this release does not carry
any obligation; $(iii)$ the wait on $\ell$ is _not_ available in $P$. The
latter constraint means that if a $P$ contains a wait on some lock, then this
lock should be restricted.

The notion of leak-freedom we use is inspired from [13]. In our setting, a
situation where some lock $\ell$ is released and will never be acquired again
can be seen as a form of memory leak. We say that $P$ _leaks_ $\ell$ if
$P\equiv(\boldsymbol{\nu}\ell)(P^{\prime}|\overline{\ell}\langle v\rangle)$
with $\ell\notin\mathrm{fln}(P^{\prime})$. $P$ _has a leak_ if $P$ leaks
$\ell$ for some $\ell$, and is _leak-free_ otherwise.

######  Lemma 22 (Progress).

If $\Gamma\vdash P$ and $\Gamma$ is complete, then either
$P\xrightarrow{}P^{\prime}$ for some $P^{\prime}$, or
$P\equiv(\boldsymbol{\nu}\widetilde{\ell})(\Pi_{i}\overline{\ell_{i}}v_{i})$
where the $\ell_{i}$s are pairwise distinct.

For lack of space, the proof is presented in Appendix B. Again, it follows the
lines of the proof of Lemma 5. To construct a graph containing necessarily a
cycle, we associate to every acquire of the form $\ell(x).Q$ an available
release of $\ell$, which might occur in a release of the form
$\overline{\ell^{\prime}}\langle\ell\rangle$, if $\ell^{\prime}$ carries the
release obligation. Similarly, to every wait $\ell(\\!(x)\\!).Q$, we associate
an available release, or, if a release $\overline{\ell}\langle v\rangle$
occurs at top-level, an acquire on $\ell$, that necessarily exists otherwise a
reduction could be fired. Finally, using a similar reasoning, to every release
of $\ell$ at top-level, we associate a wait on $\ell$, or an acquire on
$\ell$.

A consequence of Lemma 22 is that $P\Rightarrow\bm{0}$ when $\emptyset\vdash
P$.

######  Proposition 23 (Deadlock- and Leak-freedom).

$\Gamma\vdash P$ and $P\xRightarrow{}P^{\prime}$, then $P^{\prime}$ neither is
deadlocked, nor has a leak.

######  Corollary 24.

Suppose $\Gamma,\gamma,\ell:\langle\mathsf{bool}\rangle_{10}\vdash P$, and
suppose that the usage of all names in $S=\mathrm{dom}(\Gamma,\gamma)$ is
$11$. Then
$(\boldsymbol{\nu}S)P\Downarrow_{\overline{\ell}\langle\mathtt{b}\rangle}$ for
some $\mathtt{b}$.

###### Proof.

Immediate by Lemma 22 and subject reduction. ∎

This property is used to define barbed equivalence below. It does not hold for
higher-order locks: simply discarding $x$, the lock stored in $\ell$, might
break typability if $\ell$ carries an obligation.

###  3.2 Typed Behavioural Equivalence in $\pi\mathrm{\ell w}$

####  3.2.1 Barbed Equivalence

In barbed equivalence in $\pi\mathrm{\ell}$ (Definition 13), we compare
complete $\pi\mathrm{\ell}$ processes, intuitively to prevent blocked acquire
operations from making certain observations impossible. Similarly, in
$\pi\mathrm{\ell w}$, we must also make sure that all wait operations in the
processes being observed will eventually be fired. For this, we need to make
the process complete (in the sense of Lemma 22), and to add restrictions so
that wait transitions are fireable.

However, in order to be able to observe some barbs and discriminate processes,
we rely on Corollary 24, and allow names to be unrestricted as long as their
type is of the form $\langle\mathsf{bool}\rangle_{10}$. This type means that
the lock is first order, and that the context has the wait obligation. In such
a situation, interactions at $\ell$ will never be blocked, the whole process
is deadlock-free, and eventually reduces to a parallel composition of releases
typed with $\langle\mathsf{bool}\rangle_{10}$. Accordingly, we say that a
$\pi\mathrm{\ell w}$ process $P$ is _wait-closed_ if $\Gamma\vdash P$ and for
any $\ell\in\mathrm{dom}(\Gamma)$,
$\Gamma(\ell)=\langle\mathsf{bool}\rangle_{10}$.

A typed relation in $\pi\mathrm{\ell w}$ is a set of triples $(\Gamma,P,Q)$
such that $\Gamma\vdash P$ and $\Gamma\vdash Q$, and we write $\Gamma\vdash
P\mathcal{R}Q$ for $(\Gamma,P,Q)\in\mathcal{R}$. Barbed equivalence in
$\pi\mathrm{\ell w}$ is defined like $\simeq$ (Definition 13), restricting
observations to wait-closed processes.

######  Definition 25 (Barbed equivalence in $\pi\mathrm{\ell w}$,
$\simeq_{w}$).

A symmetric typed relation $\mathcal{R}$ is a _typed barbed bisimulation_ if
$\Gamma\vdash P\mathcal{R}Q$ implies the three following properties:

  1. 1.

whenever $P,Q$ are wait-closed and $P\xrightarrow{}P^{\prime}$, there is
$Q^{\prime}$ s.t. $Q\xRightarrow{}Q^{\prime}$ and $\Gamma\vdash
P^{\prime}\mathcal{R}Q^{\prime}$;

  2. 2.

if $P,Q$ are wait-closed and $P\downarrow_{\eta}$ then $Q\Downarrow_{\eta}$;

  3. 3.

for any $E,\Gamma^{\prime}$ s.t. $\Gamma^{\prime}\vdash E[P]$ and
$\Gamma^{\prime}\vdash E[Q]$, and $E[P],E[Q]$ are wait-closed, we have
$\Gamma^{\prime}\vdash E[P]\,\mathcal{R}\,E[Q]$.

_Typed barbed equivalence_ in $\pi\mathrm{\ell w}$, written $\simeq_{w}$, is
the greatest typed barbed bisimulation.

In the second clause above, $\eta$ can only be of the form
$\overline{\ell}\langle\mathtt{b}\rangle$, for some boolean value
$\mathtt{b}$. Lemma 14 tells us that we could proceed in the same way when
defining $\simeq$.

####  3.2.2 Typed Transitions for $\pi\mathrm{\ell w}$, and Bisimilarity

We now define a LTS for $\pi\mathrm{\ell w}$. Transitions for name
deallocation are not standard in the $\pi$-calculus. To understand how we deal
with these, consider $\ell(\\!(\ell^{\prime})\\!).P|Q$: this process can do
$\xrightarrow{\ell(\\!(v)\\!)}$ only if $Q$ does not use $\ell$. Similarly, in
$\ell(\\!(\ell^{\prime})\\!).P|\ell(x).Q|\overline{\ell}\langle v\rangle$, the
acquire can be fired, and the wait cannot.

Instead of selecting type-allowed transitions among the untyped transitions
like in Section 2.3, we give an inductive definition of typed transitions,
written $[{\Gamma};{P}]\xrightarrow{\mu}[\Gamma^{\prime};{P^{\prime}}]$. This
allows us to use the rules for parallel composition in order to control the
absence of a lock, when a lock deallocation is involved. Technically, this is
done by refining the definition of the operator to compose typing contexts.

Actions of the LTS are defined as follows:
$\mu~{}::=~{}\ell(v)~{}\big{|}~{}\overline{\ell}\langle
v\rangle~{}\big{|}~{}\overline{\ell}(\ell^{\prime})~{}\big{|}~{}\tau~{}\big{|}~{}\ell((v))~{}\big{|}~{}\tau/\ell$.
Name $\ell$ plays a particular role in transitions along wait actions
$\ell(\\!(v)\\!)$ and _wait synchronisations_ $\tau/\ell$: since $\ell$ is
deallocated, we must make sure that it is not used elsewhere in the process.
We define $\Gamma_{1}\bullet_{\mu}\Gamma_{2}$ as being equal to
$\Gamma_{1}\bullet\Gamma_{2}$, with the additional constraint that
$\ell\notin\mathrm{dom}(\Gamma_{1})\cup\mathrm{dom}(\Gamma_{2})$ when
$\mu=\ell(\\!(v)\\!)$ or $\mu=\tau/\ell$, otherwise
$\Gamma_{1}\bullet_{\mu}\Gamma_{2}$ is not defined. The rules defining the LTS
are given on Figure 3. We define
$\mathrm{fln}(\overline{\ell}(\ell^{\prime}))=\mathrm{fln}(\tau/\ell)=\\{\ell\\}$,
and
$\mathrm{fln}(\ell(v))=\mathrm{fln}(\ell(\\!(v)\\!))=\mathrm{fln}(\overline{\ell}\langle
v\rangle)=\\{\ell,v\\}$ (with the convention that $\\{\ell,v\\}=\\{\ell\\}$ if
$v$ is a boolean value).

We comment on the transition rules. Rules TR, TA and TW express the meaning of
usages (respectively, $01$, $0w$ and $10$). In rule TT, $\ell$ is deallocated,
and the restriction on $\ell$ is removed. In rules TPT, TPTB we rely on
operation $\Gamma_{1}\bullet_{\mu}\Gamma_{2}$ to make sure that $\ell$ does
not appear in both parallel components of the continuation process, and
similarly for TPP in the case where $\mu$ involves deallocation of $\ell$.

Typability is preserved by typed transitions: if $\Gamma\vdash P$ and
$[{\Gamma};{P}]\xrightarrow{\mu}[\Gamma^{\prime};{P^{\prime}}]$, then
$\Gamma^{\prime}\vdash P^{\prime}$.

[TR]
$[{\\{\ell:\langle\mathsf{T}\rangle_{01},v:\mathsf{T}\\}};{\overline{\ell}\langle
v\rangle}]\xrightarrow{\overline{\ell}\langle v\rangle}[\emptyset;{\bm{0}}]$

[TA]
$[{\\{\gamma,\ell:\langle\mathsf{T}\rangle_{0w}\\}};{\ell(\ell^{\prime}).P}]\xrightarrow{\ell(v)}[\\{\gamma\\{\raisebox{2.15277pt}{\small$v$}\\!/\\!\mbox{\small$\ell^{\prime}$}\\},\ell:\langle\mathsf{T}\rangle_{1w}\\};{P\\{\raisebox{2.15277pt}{\small$v$}\\!/\\!\mbox{\small$\ell^{\prime}$}\\}}]$

[TW]
$[{\\{\gamma,\ell:\langle\mathsf{T}\rangle_{10}\\}};{\ell(\\!(\ell^{\prime})\\!).P}]\xrightarrow{\ell(\\!(v)\\!)}[\\{\gamma\\{\raisebox{2.15277pt}{\small$v$}\\!/\\!\mbox{\small$\ell^{\prime}$}\\}\\};{P\\{\raisebox{2.15277pt}{\small$v$}\\!/\\!\mbox{\small$\ell^{\prime}$}\\}}]$
[TN]
$[{\Gamma,\gamma,\ell:\langle\mathsf{T}\rangle_{11}};{P}]\xrightarrow{\mu}[P^{\prime};{\Gamma^{\prime},\gamma^{\prime},\ell:\langle\mathsf{T}\rangle_{11}}]$
$[{\Gamma,\gamma};{(\boldsymbol{\nu}\ell)P}]\xrightarrow{\mu}[\Gamma^{\prime},\gamma^{\prime};{(\boldsymbol{\nu}\ell)P^{\prime}}]$
$\ell$∉$\mathrm{fln}(\mu)$

[TO]
$[{\Gamma,\gamma,\ell^{\prime}:\mathsf{T}};{P}]\xrightarrow{\overline{\ell}\langle\ell^{\prime}\rangle}[P^{\prime};{\Gamma^{\prime},\gamma,\ell^{\prime}:\mathsf{T}^{\prime}}]$
$[{\Gamma,\gamma};{(\boldsymbol{\nu}\ell^{\prime})P}]\xrightarrow{\overline{\ell}(\ell^{\prime})}[P^{\prime};{\Gamma^{\prime},\gamma,\ell^{\prime}:\mathsf{T}^{\prime}}]$

[TT]
$[{\Gamma,\gamma,\ell:\langle\mathsf{T}\rangle_{11}};{P}]\xrightarrow{\tau/\ell}[\Gamma^{\prime},\gamma;{P^{\prime}}]$
$[{\Gamma,\gamma};{(\boldsymbol{\nu}\ell)P}]\xrightarrow{\tau}[\Gamma,\gamma;{P^{\prime}}]$

[TPC]
$[{\Gamma_{1}};{P}]\xrightarrow{\ell(v)}[\Gamma^{\prime}_{1};{P^{\prime}}]$
$[{\Gamma_{2}};{Q}]\xrightarrow{\overline{\ell}\langle
v\rangle}[\Gamma^{\prime}_{2};{Q^{\prime}}]$
$[{\Gamma_{1}\bullet\Gamma_{2}};{P|Q}]\xrightarrow{\tau}[\Gamma^{\prime}_{1}\bullet\Gamma^{\prime}_{2};{P^{\prime}|Q^{\prime}}]$

[TPB]
$[{\Gamma_{1}};{P}]\xrightarrow{\ell(\ell^{\prime})}[\Gamma^{\prime}_{1};{P^{\prime}}]$
$[{\Gamma_{2}};{Q}]\xrightarrow{\overline{\ell}(\ell^{\prime})}[\Gamma^{\prime}_{2};{Q^{\prime}}]$
$[{\Gamma_{1}\bullet\Gamma_{2}};{P|Q}]\xrightarrow{\tau}[\Gamma^{\prime}_{1}\bullet\Gamma^{\prime}_{2};{(\boldsymbol{\nu}\ell^{\prime})(P^{\prime}|Q^{\prime})}]$

[TPP] $[{\Gamma_{1}};{P}]\xrightarrow{\mu}[\Gamma^{\prime}_{1};{P^{\prime}}]$
$\Gamma_{2}\vdash Q$
$[{\Gamma_{1}\bullet\Gamma_{2}};{P|Q}]\xrightarrow{\mu}[\Gamma^{\prime}_{1}\bullet_{\mu}\Gamma_{2};{P^{\prime}|Q}]$

[TPT]
$[{\Gamma_{1}};{P}]\xrightarrow{\ell(\\!(v)\\!)}[\Gamma^{\prime}_{1};{P^{\prime}}]$
$[{\Gamma_{2}};{Q}]\xrightarrow{\overline{\ell}\langle
v\rangle}[\Gamma^{\prime}_{2};{Q^{\prime}}]$
$[{\Gamma_{1}\bullet\Gamma_{2}};{P|Q}]\xrightarrow{\tau/\ell}[\Gamma^{\prime}_{1}\bullet_{\tau/\ell}\Gamma^{\prime}_{2};{P^{\prime}|Q^{\prime}}]$

[TPTB]
$[{\Gamma_{1}};{P}]\xrightarrow{\ell(\\!(v)\\!)}[\Gamma^{\prime}_{1};{P^{\prime}}]$
$[{\Gamma_{2}};{Q}]\xrightarrow{\overline{\ell}(\ell^{\prime})}[\Gamma^{\prime}_{2};{Q^{\prime}}]$
$[{\Gamma_{1}\bullet\Gamma_{2}};{P|Q}]\xrightarrow{\tau/\ell}[\Gamma^{\prime}_{1}\bullet_{\tau/\ell}\Gamma^{\prime}_{2};{(\boldsymbol{\nu}\ell^{\prime})(P^{\prime}|Q^{\prime})}]$

Figure 3: $\pi\mathrm{\ell w}$, Typed LTS. We omit symmetric versions of rules
involving parallel compositions

Bisimilarity in $\pi\mathrm{\ell w}$ takes into account the additional
transitions w.r.t. $\pi\mathrm{\ell}$, and is sound for $\simeq_{w}$.

######  Definition 26 (Typed Bisimilarity in $\pi\mathrm{\ell w}$,
$\approx_{w}$).

A typed relation $\mathcal{R}$ is a typed bisimulation if $\Gamma\vdash
P\mathcal{R}Q$ implies that whenever
$[{\Gamma};{P}]\xrightarrow{\mu}[\Gamma^{\prime};{P^{\prime}}]$, we have

  1. 1.

either $Q\xRightarrow{\hat{\mu}}Q^{\prime}$ and $\Gamma^{\prime}\vdash
P^{\prime}\mathcal{R}Q^{\prime}$ for some $Q^{\prime}$

  2. 2.

or $\mu$ is an acquire $\ell(v)$, $Q|\overline{\ell}\langle
v\rangle\xRightarrow{}Q^{\prime}$ and $\Gamma^{\prime}\vdash
P^{\prime}\mathcal{R}Q^{\prime}$ for some $Q^{\prime}$,

  3. 3.

or $\mu$ is a wait $\ell(\\!(v)\\!)$,
$(\boldsymbol{\nu}\ell)(Q|\overline{\ell}\langle
v\rangle)\xRightarrow{}Q^{\prime}$ and $\Gamma^{\prime}\vdash
P^{\prime}\mathcal{R}Q^{\prime}$ for some $Q^{\prime}$,

  4. 4.

or $\mu=\tau/\ell$, $(\boldsymbol{\nu}\ell)Q\xRightarrow{}Q^{\prime}$ and
$\Gamma^{\prime}\vdash P^{\prime}\mathcal{R}Q^{\prime}$ for some $Q^{\prime}$,

and symmetrically for the typed transitions of $Q$. _Typed bisimilarity in
$\pi\mathrm{\ell w}$_, written $\approx_{w}$, is the largest typed
bisimulation.

######  Proposition 27 (Soundness).

For any $\Gamma,P,Q$, if $\Gamma\vdash P\approx_{w}Q$, then $\Gamma\vdash
P\simeq_{w}Q$.

######  Example 28.

The law $\ell(x).\overline{\ell}\langle x\rangle=\bm{0}$ holds in
$\pi\mathrm{\ell w}$, at type $\ell:\langle\mathsf{T}\rangle_{00}$, for any
$\mathsf{T}$.

Suppose $\Gamma\vdash\ell(x).P|\ell(\\!(y)\\!).Q$. Then we can prove
$\Gamma\vdash\ell(x).P|\ell(\\!(y)\\!).Q~{}\approx_{w}~{}\ell(x).(P~{}|~{}\ell(\\!(y)\\!).Q).$

Using this equivalence and the law of asynchrony, we can deduce
$\ell(\\!(x)\\!).P~{}\simeq_{w}~{}\ell(x).(\overline{\ell}\langle
x\rangle|\ell(\\!(x)\\!).P)$.

An equivalence between $\pi\mathrm{\ell}$ processes is also valid in
$\pi\mathrm{\ell w}$. To state this property, given $P$ in $\pi\mathrm{\ell}$,
we introduce $[\\![P]\\!]_{w}$, its translation in $\pi\mathrm{\ell w}$. The
definition of $[\\![P]\\!]_{w}$ is simple, as we just need to add wait
constructs under restrictions for $[\\![P]\\!]_{w}$ to be typable.

######  Lemma 29.

Suppose $\Gamma;\mathbb{R}\vdash P\approx Q$. Then
$\Gamma_{w}\vdash[\\![P]\\!]_{w}\approx_{w}[\\![Q]\\!]_{w}$ for some
$\pi\mathrm{\ell w}$ typing environment $\Gamma_{w}$.

This result shows that the addition of wait does not increase the
discriminating power of contexts. We refer to Appendix B for the definition of
$[\\![P]\\!]_{w}$ and a discussion of the proof of Lemma 29.

##  4 Related and Future Work

The basic type discipline for lock names that imposes a safe usage of locks by
always releasing a lock after acquiring it is discussed in [14]. This is
specified using _channel usages_ (not to be confused with the usages of
Section 3.1). Channel usages in [14] are processes in a subset of CCS, and can
be defined in sophisticated ways to control the behaviour of $\pi$-calculus
processes. The encoding of references in the asynchronous $\pi$-calculus
studied in [8] is also close to how locks are used in $\pi\mathrm{\ell w}$. A
reference is indeed a lock that must be released _immediately_ after the
acquire. The typed equivalence to reason about reference names in [8] has
important differences w.r.t. $\simeq_{w}$, notably because the deadlock- and
leak-freedom properties are not taken into consideration in that work.

The type system for $\pi\mathrm{\ell w}$ has several ideas in common with
[13]. That paper studies $\lambda_{\mathrm{lock}}$, a functional language with
higher-order locks and thread spawning. The type system for
$\lambda_{\mathrm{lock}}$ guarantees leak- and deadlock-freedom by relying on
duality and linearity properties, which entail the absence of cycles. In turn,
this approach originates in work on binary session types, and in particular on
concurrent versions of the Curry-Howard correspondence [11, 7, 29, 3, 28, 23].

$\pi\mathrm{\ell w}$ allows a less controlled form of interaction than
functional languages or binary sessions. Important differences are: names do
not have to be used linearly; there is no explicit notion of thread, neither a
fork instruction, in $\pi\mathrm{\ell w}$; reduction is not deterministic. The
type system for $\pi\mathrm{\ell w}$ controls parallel composition to rule out
cyclic structures among interacting processes.

The simplicity of the typing rules, and of the proofs of deadlock- and leak-
freedom, can be leveraged to develop a theory of typed behavioural equivalence
for $\pi\mathrm{\ell}$ and $\pi\mathrm{\ell w}$. Soundness of bisimilarity
provides a useful tool to establish equivalence results. Proving completeness
is not obvious, intuitively because the constraints imposed by typing prevent
us from adapting standard approaches. The way $\approx_{w}$ is defined should
allow us to combine locks with other programming constructs in order to reason
about programs featuring locks and, e.g., functions, continuations, and
references. Work in this direction will build on [20, 24, 6, 9, 22].

Our proofs of deadlock- and leak-freedom suggest that there is room for a
finer analysis of how lock names are used. It is natural to try and extend our
type system in order to accept more processes, while keeping the induced
behavioural equivalence tractable. A possibility for this is to add _lock
groups_ [13], with the aim of reaching an expressiveness comparable to the
system in [13]. In a given lock group, locks are ordered, which makes it
possible to analyse systems having a cyclic topology.

Relying on orders to program with locks is a natural approach, that has been
used to define expressive type systems for lock freedom in the $\pi$-calculus
[12, 14, 21]. In these works, some labelling is associated to channels or to
actions on channels, and the typing rules guarantee that it is always possible
to define an order, yielding lock-freedom. We plan to study how our type
system can be extended with lock groups or ideas from type systems based on
orders.

Rule (1) from Section 1 explains in a concise way how the wait operation
behaves. Part of the difficulty in Section 3 is in defining a labelled
semantics that is compatible with the ‘magic’ of executing a wait on $\ell$
only when the restriction can be put on top of the final release of $\ell$. We
plan to provide a more operational description of deallocation, using, e.g.,
reference counting as in [13]. $\pi\mathrm{\ell w}$ could then be seen as a
language to describe at high-level what happens at a lower level when using
and deallocating locks.

##### Acknowledgement.

We are grateful to Jules Jacobs for an interesting discussion about this work,
and for suggesting the reduction rule (1) from Section 1. We also thank the
anonymous referees for their helpful remarks and advices.

## References

  * [1]
  * [2] Roberto M. Amadio, Ilaria Castellani & Davide Sangiorgi (1998): _On Bisimulations for the Asynchronous pi-Calculus_.  Theor. Comput. Sci. 195(2), pp. 291–324, 10.1016/S0304-3975(97)00223-5.
  * [3] Luís Caires & Frank Pfenning (2010): _Session Types as Intuitionistic Linear Propositions_.  In Paul Gastin & François Laroussinie, editors: CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings, Lecture Notes in Computer Science 6269, Springer, pp. 222–236, 10.1007/978-3-642-15375-4_16.
  * [4] Ornela Dardha, Elena Giachino & Davide Sangiorgi (2017): _Session types revisited_.  Inf. Comput. 256, pp. 253–286, 10.1016/j.ic.2017.06.002.
  * [5] Ornela Dardha, Elena Giachino & Davide Sangiorgi (2022): _Session Types Revisited: A Decade Later_.  In: PPDP 2022: 24th International Symposium on Principles and Practice of Declarative Programming, Tbilisi, Georgia, September 20 - 22, 2022, ACM, pp. 12:1–12:4, 10.1145/3551357.3556676.
  * [6] Adrien Durier, Daniel Hirschkoff & Davide Sangiorgi (2018): _Eager Functions as Processes_.  In Anuj Dawar & Erich Grädel, editors: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, ACM, pp. 364–373, 10.1145/3209108.3209152.
  * [7] Simon J. Gay & Vasco Thudichum Vasconcelos (2010): _Linear type theory for asynchronous session types_.  J. Funct. Program. 20(1), pp. 19–50, 10.1017/S0956796809990268.
  * [8] Daniel Hirschkoff, Enguerrand Prebet & Davide Sangiorgi (2020): _On the Representation of References in the Pi-Calculus_.  In Igor Konnov & Laura Kovács, editors: 31st International Conference on Concurrency Theory, CONCUR 2020, LIPIcs 171, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 34:1–34:20, 10.4230/LIPIcs.CONCUR.2020.34.
  * [9] Daniel Hirschkoff, Enguerrand Prebet & Davide Sangiorgi (2021): _On sequentiality and well-bracketing in the $\pi$-calculus_.  In: 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, IEEE, pp. 1–13, 10.1109/LICS52264.2021.9470559.
  * [10] Kohei Honda & Mario Tokoro (1991): _An Object Calculus for Asynchronous Communication_.  In Pierre America, editor: ECOOP’91 European Conference on Object-Oriented Programming, Geneva, Switzerland, July 15-19, 1991, Proceedings, Lecture Notes in Computer Science 512, Springer, pp. 133–147, 10.1007/BFb0057019.
  * [11] Kohei Honda, Vasco Thudichum Vasconcelos & Makoto Kubo (1998): _Language Primitives and Type Discipline for Structured Communication-Based Programming_.  In Chris Hankin, editor: Programming Languages and Systems - ESOP’98, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings, Lecture Notes in Computer Science 1381, Springer, pp. 122–138, 10.1007/BFb0053567.
  * [12] Atsushi Igarashi & Naoki Kobayashi (2001): _A generic type system for the Pi-calculus_.  In Chris Hankin & Dave Schmidt, editors: Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK, January 17-19, 2001, ACM, pp. 128–141, 10.1145/360204.360215.
  * [13] Jules Jacobs & Stephanie Balzer (2023): _Higher-Order Leak and Deadlock Free Locks_.  Proc. ACM Program. Lang. 7(POPL), pp. 1027–1057, 10.1145/3571229.
  * [14] Naoki Kobayashi (2002): _Type Systems for Concurrent Programs_.  In Bernhard K. Aichernig & T. S. E. Maibaum, editors: Formal Methods at the Crossroads. From Panacea to Foundational Support, 10th Anniversary Colloquium of UNU/IIST, the International Institute for Software Technology of The United Nations University, Lisbon, Portugal, March 18-20, 2002, Revised Papers, Lecture Notes in Computer Science 2757, Springer, pp. 439–453, 10.1007/978-3-540-40007-3_26.
  * [15] Naoki Kobayashi (2007): _Type Systems for Concurrent Programs_.  Extended version of [14].
  * [16] Naoki Kobayashi, Benjamin C. Pierce & David N. Turner (1999): _Linearity and the pi-calculus_.  ACM Trans. Program. Lang. Syst. 21(5), pp. 914–947, 10.1145/330249.330251.
  * [17] Massimo Merro & Davide Sangiorgi (2004): _On asynchrony in name-passing calculi_.  Math. Struct. Comput. Sci. 14(5), pp. 715–767, 10.1017/S0960129504004323.
  * [18] R. Milner (1991): _The polyadic $\pi$-calculus: a tutorial_.  Technical Report ECS–LFCS–91–180, LFCS.  Also in Logic and Algebra of Specification, ed. F.L. Bauer, W. Brauer and H. Schwichtenberg, Springer Verlag, 1993.
  * [19] Robin Milner (1980): _A Calculus of Communicating Systems_.  Lecture Notes in Computer Science 92, Springer, 10.1007/3-540-10235-3.
  * [20] Robin Milner (1992): _Functions as Processes_.  Math. Struct. Comput. Sci. 2(2), pp. 119–141, 10.1017/S0960129500001407.
  * [21] Luca Padovani (2014): _Deadlock and lock freedom in the linear $\pi$-calculus_.  In Thomas A. Henzinger & Dale Miller, editors: Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14 - 18, 2014, ACM, pp. 72:1–72:10, 10.1145/2603088.2603116.
  * [22] Enguerrand Prebet (2022): _Functions and References in the Pi-Calculus: Full Abstraction and Proof Techniques_.  In Mikolaj Bojanczyk, Emanuela Merelli & David P. Woodruff, editors: 49th International Colloquium on Automata, Languages, and Programming, ICALP 2022, July 4-8, 2022, Paris, France, LIPIcs 229, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 130:1–130:19, 10.4230/LIPIcs.ICALP.2022.130.
  * [23] Pedro Rocha & Luís Caires (2023): _Safe Session-Based Concurrency with Shared Linear State_.  In Thomas Wies, editor: Programming Languages and Systems - 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, Lecture Notes in Computer Science 13990, Springer, pp. 421–450, 10.1007/978-3-031-30044-8_16.
  * [24] Davide Sangiorgi (1994): _The Lazy Lambda Calculus in a Concurrency Scenario_.  Inf. Comput. 111(1), pp. 120–153, 10.1006/inco.1994.1042.
  * [25] Davide Sangiorgi (1996): _pi-Calculus, Internal Mobility, and Agent-Passing Calculi_.  Theor. Comput. Sci. 167(1&2), pp. 235–274, 10.1016/0304-3975(96)00075-8.
  * [26] Davide Sangiorgi (1997): _The Name Discipline of Uniform Receptiveness (Extended Abstract)_.  In Pierpaolo Degano, Roberto Gorrieri & Alberto Marchetti-Spaccamela, editors: Automata, Languages and Programming, 24th International Colloquium, ICALP’97, Bologna, Italy, 7-11 July 1997, Proceedings, Lecture Notes in Computer Science 1256, Springer, pp. 303–313, 10.1007/3-540-63165-8_187.
  * [27] Davide Sangiorgi & David Walker (2001): _The Pi-Calculus - a theory of mobile processes_.  Cambridge University Press.
  * [28] Bernardo Toninho, Luís Caires & Frank Pfenning (2013): _Higher-Order Processes, Functions, and Sessions: A Monadic Integration_.  In Matthias Felleisen & Philippa Gardner, editors: Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, Lecture Notes in Computer Science 7792, Springer, pp. 350–369, 10.1007/978-3-642-37036-6_20.
  * [29] Philip Wadler (2014): _Propositions as sessions_.  J. Funct. Program. 24(2-3), pp. 384–418, 10.1017/S095679681400001X.

##  Appendix A Additional Material for Section 2

###  A.1 $\mathrm{CCS}\ell$, Operational Semantics

Structural congruence is the least congruence satisfying the following axioms:
P—Q≡Q—P

P—(Q—R)≡(P—Q)—R
P—($\boldsymbol{\nu}$$\ell$) Q≡($\boldsymbol{\nu}$$\ell$)(P—Q) if
$\ell$∉$\mathrm{fln}(P)$

($\boldsymbol{\nu}$$\ell$)($\boldsymbol{\nu}$$\ell$’)P≡($\boldsymbol{\nu}$$\ell$’)($\boldsymbol{\nu}$$\ell$)P

To define reduction, we introduce _execution contexts_ , $E$, given by
$E~{}::=~{}[\cdot]~{}\big{|}~{}E|P~{}\big{|}~{}(\boldsymbol{\nu}\ell)E$, where
$[\cdot]$ is the hole. $E[P]$ is the process obtained by replacing the hole in
$E$ with $P$.

Reduction is defined by the following rules: $\overline{\ell}$—$\ell$.P →P

P→P’ E[P]→E[P’]

Q≡PP→P’P’≡Q’ Q→Q’

###  A.2 $\mathrm{CCS}\ell$, Properties of the Type System

###### of Lemma 4.

We show by induction on $k$ that $\ell_{1}.P_{1}|\dots|\ell_{k-1}.P_{k-1}$ is
lock-connected: this holds because for every $i$, $\ell_{i}.P_{i}$ is lock-
connected, and because
$\ell_{i}.P_{i}\stackrel{{\scriptstyle\ell_{i}}}{{\longleftrightarrow}}\ell_{i+1}.P_{i+1}$
for all $i<k$.

Moreover, we know
$\ell_{k-1}.P_{k-1}\stackrel{{\scriptstyle\ell_{k-1}}}{{\longleftrightarrow}}\ell_{k}.P_{k}$
and
$\ell_{k}.P_{k}\stackrel{{\scriptstyle\ell_{k}}}{{\longleftrightarrow}}\ell_{1}.P_{1}$.
So names $\ell_{k-1}$ and $\ell_{k}$ belong to the free names both of
$\ell_{1}.P_{1}|\dots|\ell_{k-1}.P_{k-1}$ and of $\ell_{k}.P_{k}$. By Lemma 3,
this prevents $\ell_{1}.P_{1}|\dots|\ell_{k}.P_{k}$ from being typable. ∎

###  A.3 $\pi\mathrm{\ell}$, Operational Semantics

Structural congruence in $\pi\mathrm{\ell}$, written $\equiv$, is standard,
except for the treatment of mismatch. Indeed, the corresponding axiom cannot
be used under an acquire prefix.

To handle this, we introduce an auxiliary structural congruence relation,
written $\equiv_{\mathrm{r}}$. Relation $\equiv$ is the smallest equivalence
relation that satisfies the axioms for $\equiv$ in $\mathrm{CCS}\ell$, plus
the following ones [PNil] P—$\bm{0}$≡P

[RNil] ($\boldsymbol{\nu}$$\ell$)$\bm{0}$≡$\bm{0}$

[Mat] [v=v]P_1,P_2≡P_1

[Mis] [v=v’]P_1,P_2 ≡ P_2 if  v≠v’ and also the contextual axioms
[CPar]P≡QP—T≡Q—T

[CRes]P≡Q($\boldsymbol{\nu}$$\ell$)P≡($\boldsymbol{\nu}$$\ell$)Q

[CAcq]P$\equiv_{\mathrm{r}}$Q$\ell(\ell^{\prime})$.P≡$\ell(\ell^{\prime})$.Q

The last axiom refers to $\equiv_{\mathrm{r}}$, which is defined like
$\equiv$, except that Mis is omitted and Cacq is replaced by
[CAcqr]P$\equiv_{\mathrm{r}}$Q$\ell(\ell^{\prime})$.P$\equiv_{\mathrm{r}}$$\ell(\ell^{\prime})$.Q

##### Labelled Semantics for $\pi\mathrm{\ell}$.

Actions of the LTS are defined by
$\mu\quad::=\quad\ell(v)~{}\big{|}~{}\overline{\ell}\langle
v\rangle~{}\big{|}~{}\overline{\ell}(\ell^{\prime})~{}\big{|}~{}\tau$.

The set of free names of $\mu$ is defined by
$\mathrm{fln}(\overline{\ell}\langle
v\rangle)=\mathrm{fln}(\ell(v))=\\{\ell,v\\}$, $\mathrm{fln}(\tau)=\emptyset$
and $\mathrm{fln}(\overline{\ell}(\ell^{\prime}))=\\{\ell\\}$.

The set of bound names of $\mu$ is defined by $\mathrm{bln}(\mu)=\emptyset$,
except for $\mathrm{bln}(\overline{\ell}(\ell^{\prime}))=\\{\ell^{\prime}\\}$.

The transition rules are the following: $\overline{\ell}\langle
v\rangle$$\xrightarrow{\overline{\ell}\langle v\rangle}$$\bm{0}$

$\ell$($\ell$’).P$\xrightarrow{\ell(v)}$P$\\{\raisebox{2.15277pt}{\small$v$}\\!/\\!\mbox{\small$\ell^{\prime}$}\\}$

P$\xrightarrow{\overline{\ell}\langle\ell^{\prime}\rangle}$P’
($\boldsymbol{\nu}$$\ell$’)P$\xrightarrow{\overline{\ell}(\ell^{\prime})}$P’

P$\xrightarrow{\mu}$P’
($\boldsymbol{\nu}$$\ell$)P$\xrightarrow{\mu}$($\boldsymbol{\nu}$$\ell$)P’
$\ell$∉$\mathrm{fln}(\mu)$

P$\xrightarrow{\mu}$P’ P—Q$\xrightarrow{\mu}$P’—Q
$\mathrm{fln}(Q)$∩$\mathrm{bln}(\mu)$=$\emptyset$

P$\xrightarrow{\overline{\ell}\langle v\rangle}$P’ Q$\xrightarrow{\ell(v)}$Q’
P—Q$\xrightarrow{\tau}$P’—Q’

P$\xrightarrow{\overline{\ell}(\ell^{\prime})}$P’
Q$\xrightarrow{\ell(\ell^{\prime})}$Q’
P—Q$\xrightarrow{\tau}$($\boldsymbol{\nu}$$\ell$’)(P’—Q’)

P_1$\xrightarrow{\mu}$P’_1 [v=v]P_1,P_2$\xrightarrow{\mu}$P’_1

P_2$\xrightarrow{\mu}$P’_2 [v=v’]P_1,P_2$\xrightarrow{\mu}$P’_2 v≠v’

##  Appendix B Additional Material from Section 3

###  B.1 Leak-Freedom in $\pi\mathrm{\ell w}$

The proof of Lemma 22 follows the approach of the proof of Lemma 5. An
additional difficulty with respect to the latter proof is that release and
wait obligations on a given lock need not be explicit in the process, in the
sense that they can be stored in another lock.

###### Proof.

We first consider the situation where $\Gamma\vdash P_{0}$, $\Gamma$ is
complete, and we can write P_0 ≡ $(\boldsymbol{\nu}S)$(
∏_i$\overline{\ell_{i}}\langle v_{i}\rangle$ — ∏_j$\ell_{j}(x_{j})$.P_j —
∏_k$\ell_{k}(\\!(y_{k})\\!)$.Q_k) . We let
$P=\prod_{i}\overline{\ell_{i}}\langle
v_{i}\rangle~{}|~{}\prod_{j}\ell_{j}(x_{j}).P_{j}~{}|~{}\prod_{k}\ell_{k}(\\!(y_{k})\\!).{Q_{k}}$.

We introduce some terminology to reason about this decomposition. A _prime
process_ is a process of the form $\overline{\ell}\langle v\rangle$,
$\ell(x).P^{\prime}$ or $\ell(\\!(y)\\!).P^{\prime}$. Here “prime” refers to
the fact that such processes cannot be decomposed modulo $\equiv$. We call
_subject_ of a prime process the name that occurs in subject position in the
topmost prefix of that process: these are the $\ell_{i}$s, the $\ell_{j}$s and
the $\ell_{k}$s in the decomposition above.

We make the two following observations. First, for any
$\ell\in\mathrm{fln}(P)$, either $\ell\in\mathrm{fln}(P_{0})$, or a release of
$\ell$ and a wait on $\ell$ must be available, by typing. Second, none of the
$\ell_{i}$ is equal to one of the $\ell_{j}$, since otherwise $P_{0}$ could
reduce. Moreover, if some $\ell_{i}$ is equal to one of the $\ell_{k}$s, then
$P$ necessarily contains an acquire on $\ell_{i}$, since otherwise $P_{0}$
could reduce by performing a wait transition. In the following, we do not
consider the prime processes whose subject is in $\Gamma$. Recall that these
processes are outputs $\overline{\ell_{i}}\langle v_{i}\rangle$ with $v_{i}$
being either of type $\mathsf{bool}$ or $\langle\mathsf{T}\rangle_{00}$.

To derive a contradiction, we show that the subject of every prime process
occurs free in another prime process having a different subject. We examine
the three forms of prime processes.

  * •

Consider first $\ell_{j}(x_{j}).P_{j}$. The available _release of $\ell_{j}$_
cannot occur at top-level, since otherwise $P$ could reduce. The release
cannot be available under an acquire or wait prefix on $\ell_{j}$, by typing
and by definition of being available.

The release of $\ell_{j}$ may be available in one of the $P_{j^{\prime}}$s, or
in one of the $P_{k}$s occurring under a prefix at some lock name different
from $\ell_{j}$. In both cases, $\ell_{j}$ occurs in another prime process
having a different subject.

If the release on $\ell_{j}$ is available neither in the $P_{j}$s nor in the
$P_{k}$s, then there exists another release of the form
$\overline{\ell}\langle\ell_{j}\rangle$ for some $\ell$, that does not occur
under an acquire on $\ell_{j}$. We remark that $\ell$’s usage is of the form
$1w$, and that $\ell\neq\ell_{j}$.

Thus, the release of $\ell$ necessarily occurs in a prime process whose
subject is different from $\ell_{j}$.

  * •

Consider now $\ell_{k}(\\!(y_{k})\\!).{P_{k}}$. As above, we reason about the
_release of $\ell_{k}$_. The only difference is that the release of $\ell_{k}$
may occur at top-level. If this is the case, then there is necessarily an
acquire on $\ell_{k}$, otherwise $P$ could reduce. This acquire cannot occur
at top-level, since otherwise $P$ could reduce, by performing a wait
transition. Hence, there is a prime process whose subject is different from
$\ell_{k}$ that contains an acquire on $\ell_{k}$.

  * •

Consider $\overline{\ell_{i}}\langle v_{i}\rangle$. We reason about the _wait
on $\ell_{i}$_. If the wait on $\ell_{i}$ occurs at top-level, then, as above,
an acquire on $\ell_{i}$ must occur in $P$, since otherwise $P_{0}$ could
reduce. That acquire on $\ell_{i}$ cannot occur at top-level, since otherwise
$P$ could reduce. So in this case $\ell_{i}$ occurs in a prime process whose
subject is different from $\ell_{i}$.

If the wait on $\ell_{i}$ does not occur at top-level, then it can occur in a
prime process whose subject is different from $\ell_{i}$: that process cannot
start with an acquire on $\ell_{i}$ since otherwise $P$ could reduce.

The last possibility is that a subterm of the form
$\overline{\ell}\langle\ell_{i}\rangle$ occurs in some other prime process,
and $\ell$ carries the wait obligation. Reasoning as above, the subject of the
prime process cannot be $\ell_{i}$.

We have shown that every prime process in the decomposition above whose
subject is $\ell$ can be connected with a different prime process. Like in the
proofs of deadlock-freedom, we obtain a cycle, which is impossible by (the
counterpart of) Lemma 4.

∎

###  B.2 Translating a $\pi\mathrm{\ell}$ Process in $\pi\mathrm{\ell w}$

If $P$ is a $\pi\mathrm{\ell}$ process, $[\\![P]\\!]_{w}$ is its translation
into $\pi\mathrm{\ell w}$, defined as follows:
$[\\![(\boldsymbol{\nu}\ell)P]\\!]_{w}$ =
($\boldsymbol{\nu}$$\ell$)($[\\![P]\\!]_{w}$ — $\ell(\\!(x)\\!)$.$\bm{0}$)

$[\\![\ell(\ell^{\prime}).P]\\!]_{w}$ = $\ell$($\ell$’).$[\\![P]\\!]_{w}$

$[\\![\overline{\ell}\langle v\rangle]\\!]_{w}$ = $\overline{\ell}\langle
v\rangle$

$[\\![P_{1}|P_{2}]\\!]_{w}$ = $[\\![P_{1}]\\!]_{w}$ — $[\\![P_{2}]\\!]_{w}$

$[\\![[v=v^{\prime}]P_{1},P_{2}]\\!]_{w}$ =
[v=v’]$[\\![P_{1}]\\!]_{w}$,$[\\![P_{2}]\\!]_{w}$

To prove Lemma 29, we establish a correspondence between typing in
$\pi\mathrm{\ell}$ and in $\pi\mathrm{\ell w}$. If $\Gamma;\mathbb{R}\vdash
P$, the typing environment to type $P$ seen as a $\pi\mathrm{\ell w}$ process
is constructed by making sorts explicit, and by assigning usage $10$ for name
$\ell$ if $\ell\in\mathbb{R}$, and $00$ otherwise. Conversely, if
$P\in\pi\mathrm{\ell}$ can be typed as a $\pi\mathrm{\ell w}$ process with
$\Gamma_{w}\vdash P$, then we can suppose that $\Gamma_{w}$ does not contain
any usage of the form $r1$. We recover a $\pi\mathrm{\ell}$ typing for $P$ by
collecting all names having type usage $10$ in $\mathbb{R}$, and erasing type
information in the components of $\Gamma_{w}$, yielding $\Gamma$, so that
$\Gamma;\mathbb{R}\vdash P$.

This correspondence is extended to a correspondence between transitions, so
that a bisimulation relation in $\pi\mathrm{\ell}$ is also a bisimulation in
$\pi\mathrm{\ell w}$, via the aforementioned translation. To prove the latter
property, we rely on the equivalence
$\\{\\{v\\}\\}\vdash(\boldsymbol{\nu}\ell)(\overline{\ell}\langle
v\rangle|\ell(\\!(x)\\!).\bm{0})\approx_{w}\bm{0}$ in $\pi\mathrm{\ell w}$.