Deadlock-Free Typestate-Oriented Programming
Luca Padovania
a Dipartimento di Informatica, Università di Torino, Italy
Abstract Context. TypeState-Oriented Programming (TSOP) is a paradigm intended to help developers in
the implementation and use of mutable objects whose public interface depends on their private state. Under
this paradigm, well-typed programs are guaranteed to conform with the protocol of the objects they use.
Inquiry. Previous works have investigated TSOP for both sequential and concurrent objects. However, an
important difference between the two settings still remains. In a sequential setting, a well-typed program
either progresses indefinitely or terminates eventually. In a concurrent setting, protocol conformance is no
longer enough to avoid deadlocks, a situation in which the execution of the program halts because two or
more objects are involved in mutual dependencies that prevent any further progress.
Approach. In this work, we put forward a refinement of TSOP for concurrent objects guaranteeing that welltyped programs not only conform with the protocol of the objects they use, but are also deadlock free. The
key ingredients of the type system are behavioral types, used to specify and enforce object protocols, and
dependency relations, used to represent abstract descriptions of the dependencies between objects and detect
circularities that might cause deadlocks.
Knowledge. The proposed approach stands out for two features. First, the approach is fully compositional
and therefore scalable: the objects of a large program can be type checked in isolation; deadlock freedom
of an object composition solely depends on the types of the objects being composed; any modification/refactoring of an object that does not affect its public interface does not affect other objects either. Second, we
provide the first deadlock analysis technique for join patterns, a high-level concurrency abstraction with which
programmers can express complex synchronizations in a succinct and declarative form.
Grounding. We detail the proposed typing discipline for a core programming language blending concurrent
objects, asynchronous message passing and join patterns. We prove that the type system is sound and give
non-trivial examples of programs that can be successfully analyzed. A Haskell implementation of the type
system that demonstrates the feasibility of the approach is publicly available.
Importance. The static analysis technique described in this work can be used to certify programs written in a
core language for concurrent TSOP with proven correctness guarantees. This is an essential first step towards
the integration and application of the technique in a real-world developer toolchain, making programming
of such systems more productive and less frustrating.
Keywords concurrent objects, actors, deadlock freedom, static analysis, behavioral types

The Art, Science, and Engineering of Programming
Submitted

December 2, 2017

Published

March 29, 2018

doi

10.22152/programming-journal.org/2018/2/15
© Luca Padovani
This work is licensed under a “CC BY 4.0” license.
In The Art, Science, and Engineering of Programming, vol. 2, no. 3, 2018, article 15; 34 pages.

Deadlock-Free Typestate-Oriented Programming

1

Intoduction

The public interface of a mutable object may depend on its private state [6]. A
typical example is that of a file, which can be read or written if it is open, but not
if it is closed. Yet, in most programming languages the interface of files does not
specify any formal correlation between the availablity of read/write methods and the
state of the file on which they are invoked. At best, the textual description of these
methods warns the programmer about the intended usage protocol of files. Typestateoriented programming [17, 2, 42, 21] (TSOP for short) provides linguistic constructs and
types that facilitate the implementation and use of objects with structured protocols,
enabling the detection of protocol violations at compile time.
TSOP uses control-flow analysis to track the state of objects and to determine
whether a certain method invocation in a specific point of the program is valid or not.
This technique falls short for concurrent objects, those objects that may be accessed and
modified unpredictably by several concurrent processes. To overcome this difficulty,
Crafa and Padovani [16] have proposed a hybrid approach to concurrent TSOP that
combines compile-time checks and execution-time synchronizations. A significant gap
between the sequential and concurrent settings still remains, though. In a sequential
setting, the fact that a program conforms with the protocol of the objects it uses is
enough to guarantee that the program either progresses indefinitely or terminates
eventually. In a concurrent setting, this is no longer the case: there are programs
that conform with the protocol of the objects they use and yet their execution stops
prematurely because a deadlock has occurred. The aim of this work is to refine the
concurrent approach to TSOP put forward by Crafa and Padovani so as to prevent
these situations.
We see an instance of the problem in the following program, which creates a future
variable [4] and its user in an object-based language that supports concurrent TSOP
and uses asynchronous message passing as the sole interaction mechanism [16]:
1
2
3
4
5
6
7
8
9

new future : #FutureT
[ EMPTY
& Resolve(n)
| RESOLVED(n) & Get(r)
in future!EMPTY
&
new user : #UserT
[ READ(future)
| WRITE(future) & Reply(n)
in user!READ(future)

x future!RESOLVED(n)
x future!RESOLVED(n) & r!Reply(n) ]

x user!WRITE(future) & future!Get(user)
x user!DONE
& future!Resolve(n) ]

The future variable (lines 1–4) can be in one of two states. When it is EMPTY, future
accepts a Resolve message carrying some value n and becomes RESOLVED, storing
n in its state (line 2). When it is RESOLVED, future accepts a Get message carrying
a reference r to another object, sends the stored value n to r and remains in the
RESOLVED state (line 3). The future variable is EMPTY when initialized (line 4). The
user object (lines 6–9) can be in one of three states. When in state READ, user sends
a request to retrieve the content of future (a reference to a future variable stored in
user’s state) and spontaneously moves into the WRITE state (line 7). When in state

15:2

Luca Padovani
WRITE, user accepts a Reply message carrying a value n, resolves future with n and

moves into the DONE state (line 8). The object user is initialized in the READ state
(line 9) and, once in state DONE, becomes inert (it has no transitions from this state).
Since it is impossible for user to retrieve a value from future before future has
been resolved, this program will deadlock. Crafa and Padovani [16] have shown
that commutative regular expressions [12] can serve as natural type specifications for
concurrent object protocols: a type describes the set of legal message configurations
that can be targeted to objects with that type; commutativity of the connective ·
captures the fact that the order of concurrent message outputs is unpredicatble and
therefore irrelevant. As an example, a sensible type #FutureT for future is
(EMPTY · Resolve + RESOLVED) · ∗Get

which specifies that future is always either EMPTY or RESOLVED, that it must receive
exactly one Resolve message when it is EMPTY, and that it may receive any number
of Get messages regardless of its state. According to the type system of Crafa and
Padovani, user conforms with #FutureT and the above program is well typed. Unfortunately, the possibility of sending Get messages to future not knowing future’s state
is exploited to generate a circular dependency between future and user that leads to
a deadlock. To prevent deadlocks like this, we put forward an approach that combines
two complementary mechanisms. We keep using behavioral types such as #FutureT
to specify concurrent object protocols and impose restrictions and obligations on their
users. In addition, we track the dependencies between the objects to detect potentially
dangerous circularities. In the above program, the two outputs user!WRITE(future)
and future!Get(user) on line 7 hint at such a circularity between user and future.
Deadlocks in concurrent programming have been a longstanding issue and many
approaches aimed at deadlock prevention have been proposed. We will give a detailed
account of them in Section 6 but we anticipate that, among these works, our proposal
stands out for two features. First of all, it is compositional: deadlock freedom of
a compound system can be established solely using information gathered from its
sub-systems in isolation. It is never the case that, to successfully combine two welltyped sub-systems, the sub-systems must be re-analyzed or re-typed differently. The
analysis is necessarily conservative (deadlock freedom is undecidable in general),
but expressive enough to handle non-trivial programs. Second, our approach is the
first one that attacks the problem of deadlock analysis for concurrent objects with join
patterns [18, 19, 8, 40, 41, 22, 43]. Actors [24, 1, 23] are a special case of such objects.
We recall the formal model for concurrent TSOP [19, 16] and
formalize the notions of protocol-conformant and deadlock-free processes (Section 2).
Then, we walk through a series of simple examples to illustrate the key ideas of our
analysis technique (Section 3) before presenting the typing rules and their soundness
properties (Section 4). In the latter parts of the paper we discuss a few more complex
examples (Section 5) and related work (Section 6). Proofs and additional technical
material are in Appendix A. All the code in shaded background can be type checked
and possibly executed using CobaltBlue [34], a publicly available implementation of
the presented type system.
Structure of the paper

15:3

Deadlock-Free Typestate-Oriented Programming

Table 1

Syntax of the behaviorally typed Objective Join Calculus.

Process
Molecule
Pattern
Class
Type

2

P, Q
M, N
J, K
C, D
t, s

::=
::=
::=
::=
::=

done | u! M | P & Q | new a : t = [C ] in P
m(u) | M & N
m( x ) | J & K
JxP | C|D
0 | 1 | m( t ) | t + s | t · s | ∗t

A Formal Model for Concurrent Typestate-Oriented Programming

Following Crafa and Padovani [16] we use a typed version of the Objective Join
Calculus [19] as formal model for concurrent TSOP. We assume an infinite set of object
names ranged over by a, b, and a disjoint, infinite set of variables ranged over by x ,
y . We let u, v range over names, which are either object names or variables. We also
assume a set of message tags ranged over by m. We write e or e1 , . . . , en for sequences of
various entities and say that n is the length of the sequence. For example, u stands
for the sequence of names u1 , . . . , un . We write 〈e1 , . . . , en 〉 for multisets of entities.
When no ambiguity may arise, we occasionally drop the parentheses 〈 · · · 〉 and let
the sequence e1 , . . . , en denote the corresponding multiset 〈e1 , . . . , en 〉.
The syntax of the Objective Join Calculus is shown in Table 1 and comprises processes,
molecules, patterns, classes and types. The term done denotes the terminated process,
which does nothing. The term u! M denotes the process that sends the molecule M
to the object u. A molecule is a composition m1 (u1 ) & · · · & mk (uk ) of messages. Each
message m(u) consists of a tag m and a sequence of arguments u1 , . . . , un . We say that
n is the arity of the message and we just write m instead of m() when n = 0. Note
that a process u! M has no continuation, meaning that the calculus is asynchronous.
Sequential composition is modeled by means of explicit continuation passing. The
term P & Q denotes the parallel composition of P and Q. The term new a : t = [C ] in P
denotes a process that creates an object a of type t and class C and whose scope
is C and P . The type of an object specifies how the object is supposed to be used.
Syntax and semantics of types will be given later. A class consists of a finite set of
reaction rules J1 x P1 | · · · | Jn x Pn and determines how the object reacts to the
messages targeted to it. Each reaction J x P is made of a pattern J and a process P .
When a molecule of messages that matches the pattern J is targeted to the object, the
molecule is atomically consumed and the corresponding process P is spawned.
The definitions of free and bound names for processes are standard and omitted for
space reasons [19]. Hereafter we will consider processes equal modulo bound names.
The semantics of the Objective Join Calculus is akin to a chemical process [9]
whereby the state of the computation is a solution D  P consisting of a finite map D
from object names to object definitions and a multiset (or “soup”) P of molecules
and processes. The map D determines which chemical reactions may occur in P .
Chemical reactions consume molecules matching certain patterns from P and produce
new processes in P . The molecules and processes in P disgregate and recombine

15:4

Luca Padovani

Table 2
[done]
[new]
[par]
[join]
[red]

Semantics of the Objective Join Calculus.

 done
D  new a : t = [C ] in P, P
 P &Q
 a!(M & N )
a : t = C  a!σJ


 D, a : t = C


→
a:t=C


 P, P
a 6∈ fn(P )
 P, Q
 a! M , a!N
 σP
JxP∈C

depending on the temperature of the solution. Reflexivity [18] allows new chemical
reactions to be added to D dynamically, as the computation progresses.
More precisely, the semantics of the Objective Join Calculus is given by the relations
*, + and → defined in Table 2. As customary for the Objective Join Calculus [19],
in the table we only show the components of the solution that are affected by each
relation to avoid clutter. For example, rule [done] as shown in Table 2 actually stands
for D  done, P  D  P . The relations * and + change the temperature of the
solution by heating and cooling it, respectively. These trasformations are reversible and
defined by the four topmost rules. The rule [done] states that done terms evaporate
and condensate, as the temperature changes. The rule [new] moves object definitions
between processes and definitions. The side condition a 6∈ fn(P ) makes sure that no
occurrence of a is accidentally captured (when the solution heats up) and, conversely,
that no occurrence of a becomes free (when the solution cools down). Given that
we have assumed an infinite supply of object names and that we silently rename
bound names in processes, it is always possible to perform both transformations. The
rules [par] and [join] break and recompose processes and molecules. In the latter case,
molecules must be targeted to the same object a. There is only one reduction rule
[red] representing a non-reversible chemical reaction, which occurs when the solution
contains a molecule a! M targeted to some object a and M matches the left-hand side
J of a reaction J x P in the class of a. The matching is witnessed by a substitution
σ from variables to names such that σJ = M . In this case, the reaction fires: the
molecule M is atomically removed from the solution and replaced by the process P on
the right-hand side of the reaction with its free variables substituted according to σ.
Example 1. We may use these definitions to run the program discussed in Section 1. Initially, the only available messages are future!EMPTY (line 4) and user!READ(future)
(line 9). The second message triggers the first reaction of user (line 7) which generates
two further messages user!WRITE(future) and future!Get(user). At this point, no
combination of the available messages is capable of triggering any reaction, therefore
the execution halts.

Types specify how objects can be used and shared. Using an object means targeting
the object with one or more messages. There may be messages that are mutually
exclusive, so that only one of them can be chosen and sent, and others that can be
sent concurrently. There may be objects that can only be used by one process at a time
and others that can be shared. There are objects that must be used and others that
can be discarded. We specify these possibilities, obligations and prohibitions using a

15:5

Deadlock-Free Typestate-Oriented Programming

language of behavioral types akin to regular expressions, but where composition · is
commutative (Table 1).
The type 0 describes absurd objects: there is no legal way of using an object with
this type, and yet not using the object is disallowed as well. While this type is literally
useless for the programmer, its role is important in the theory of types that we will
develop and cannot be omitted altogether from the syntax. As we will see, 0 is the
top element of the type hierarchy and may be generated by a crucial operator on
types. The type 1 describes objects that can only be discarded. Any other usage (like
sending a message to the object) is forbidden. The message type m( t ) describes an
object that must be used as target for a single message with tag m and arguments of
type t . A process owning a reference to an object with this type has the obligation to
use the object as prescribed. Simply discarding the object is disallowed. We write M
for an arbitrary message type m( t ), we say that the length of t is the arity of M and
we write just m instead of m() when t is the empty sequence. Next we have three
connectives for building compound types. The sum + represents choice: an object of
type t + s must be used either as specified by t or as specified by s. For example, a
process owning a reference to an object of type a + b must send either an a message
or a b message to the object. Not using the object or sending both a and b messages
are disallowed. On the other hand, an object of type 1 + m may be either discarded (if
“used” as specified by 1) or used as target for an m message. The product · represents
concurrency: an object of type t · s must be used both as specified by t and also as
specified by s, by possibly concurrent processes owning references to it. For example,
a process owning a reference to an object of type a · b must send both an a message
and a b message to the object. Sending only either or none of them is disallowed.
The exponential ∗ represents unrestricted, possibly concurrent usage: an object of type
∗t may be used any number of times by possibly concurrent processes, each time as
specified by t . For example, a process owning a reference to an object of type ∗(a · b)
may send any number of a and b messages to the object, provided that the number of
‘a’ messages is the same as the number of ‘b’ messages. In addition to these types, in
the examples we occasionally use int or #Number to describe basic values.
To specify possibly infinite protocols, we interpret the productions for types in
Table 1 coinductively. In other words, we consider as types the possibly infinite trees
generated by those productions. We impose two restrictions on such type trees, namely
regularity and contractiveness. Regularity requires that each type tree is made of finitely
many distinct subtrees. This guarantees that the type is finitely representable, either
with the well-known µ-notation for recursive types or by means of a finite system
of equations [15]. Contractiveness requires that each infinite branch of a tree type
must go through infinitely many message types, so as to avoid types such as those
satisfying the equation t = t + t or t = ∗t , which do not provide any information.
We formalize the semantics of a type by means of its valid configurations, describing
which combinations of messages can be sent concurrently to an object with that type:

15:6

Luca Padovani

Definition 1 (valid configurations). Configurations, ranged over by A, B, are multisets
of message types. The valid configurations of a type t , denoted by J t K, are defined by
def

J0K = ;
def
J1K = {〈〉}
def

def

J t + sK = J t K ∪ JsK
def
J t · sK = {A ] B | A ∈ J t K ∧ B ∈ JsK}

def

JMK = {〈
M〉}
def S
J∗t K = i∈N J t i K

def

where t 0 = 1 and t i+1 = t · t i and ] denotes multiset union.
Contractiveness makes sure that the set of valid configurations is well defined,
since there is never any need to peek inside message types. As an exampe, we have
Ja · (b + c)K = {〈a, b〉, 〈a, c〉} meaning that an object of type a · (b + c) must be used as
target for either an ‘a’ and a ‘b’ message or an ‘a’ and a ‘c’ message. It follows that the
types a · (b + c) and 1 · a · (b + c) and a · b + a · c have the same valid configurations
and indeed they will be equivalent according to Definition 2. As another example, we
have J∗(a · b)K = J1K ∪ Ja · bK ∪ Ja · a · b · bK ∪ · · · = {〈〉, 〈a, b〉, 〈a, a, b, b〉, . . . }. Notice the
difference between 0 and 1. The only valid configuration of the latter is 〈〉, meaning
that not sending any message to an object of type 1 is allowed. On the other hand, 0
has no valid configurations at all, so there is no way to conform with it.
We are now ready to introduce subtyping:
Definition 2 (subtyping). Let ¶ be the largest relation on types such that t ¶ s and
〈mi (si )〉i∈I ∈ JsK imply 〈mi ( t i )〉i∈I ∈ J t K and si ¶ t i for every i ∈ I . We say that t is a
subtype of s (and s a supertype of t ) if t ¶ s holds. We say that t and s are equivalent,
written t ' s, iff t ¶ s and s ¶ t .
Subtyping is best understood bearing in mind the usual safe substitution principle:
if t ¶ s, then it is safe to replace an object of type s with an object of type t . For
example, we have a + b ¶ a: a process using an object of type a can (and must) send
an ‘a’ message to the object. This is also a valid usage of an object of type a + b,
which allows sending either an ‘a’ message or a ‘b’ message to the object. As usual,
subtyping is contravariant on argument types. For example, we have m(a) ¶ m(a + b).
A process using an object of type m(a + b) will send a message u( v ) to u and u will
use v for sending either an a message or a b message. Then, it is safe to send the
same message also to an object of type m(a), which will deterministically send an
a message to v . The properties of ¶ that have been exemplified so far are standard
for subtyping relations on object types. The original ingredient of ¶ is that it also
accounts for message combinations. For example, a · (b + c) ¶ a · c, since using an
object according to the type a · c is one of the allowed usages of an object of type
a · (b + c). In general, it is possible to show that ¶ includes all the laws of Commutative
Kleene Algebra [12]: both + and · are commutative and respectively have 0 and 1 as
neutral elements, + is idempotent, · distributes over + and is absorbed by 0. Other
notable laws include ∗t ¶ ∗t · ∗t and ∗t ¶ t , which allow an object of type ∗t to be
shared and used according to t by an arbitrary number of processes. Finally, ¶ is a
pre-congruence with respect to all type connectives [16].
We give characterizations of “usable” types – those describing objects that can be
used – and “relevant” types – those describing objects that must be used.
Definition 3. We say that t is usable if 0 6¶ t and that it is relevant if t 6¶ 1.

15:7

Deadlock-Free Typestate-Oriented Programming

A usable type has at least one (possibly empty) valid configuration and a relevant
type does not have 〈〉 among its valid configurations. The type 0 is relevant but
unusable and 1 is usable but irrelevant. Types like m or a + b or a · b are both usable
and relevant. We extend this terminology from types to the objects they describe.
The next notion we introduce is a “derivative” operator allowing us to compute the
residual of a type when we remove one or more message types with a given tag. This
operator is closely related to, and takes its name from, Brzozowski’s derivative [10].
Definition 4 (type derivative). We write M ≈ M0 if M and M0 have the same tag. The
derivative of a type t with respect to a message type M, written t[M], is defined by:
¨
def
def
1 if M ≈ M0
0[M] = 1[M] = 0
(t + s)[M] = t[M] + s[M]
def
0
M [ M] =
def
def
(∗t)[M] = t[M] · ∗t
(t · s)[M] = t · s[M] + t[M] · s
0 otherwise
def

The derivative of t with respect to A = 〈M1 , . . . , Mn 〉 is t[A] = t[M1 ] · · · [Mn ].1
If t is the protocol of an object, then t[m] is the residual protocol of the same object
after an m message has been sent to it. For example, if t = a · (b + c) and we send an
‘a’ message to the object, in order to conform with t we are still supposed to use the
object according to the type t[a] = a · (b + c)[a] + a[a] · (b + c) ' b + c. If instead we
send a ‘d’ message to the same object of type t , then we obtain t[d] ' 0. By sending
‘d’ we have violated the protocol t and now we are left with an unusable object. In
general, usability and relevance help us formalize conformance with, completion and
violation of an object’s protocol. If we have sent to an object of type t a multiset of
messages described by the configuration A and t[A] is still usable, then we conformed
with the object’s protocol. If t[A] is also irrelevant, then no more duties remain and
we have completed the object’s protocol. On the contrary, if t[A] is unusable, then we
have not used the object appropriately. Concerning protocol conformance, we have:
Definition 5 (conformant process). We say that P is a conformant process if, whenever
;  P =⇒ D, a : t = C  〈a!mi (ci )〉i∈I , P , then t[〈mi 〉i∈I ] is usable and, if t[〈mi 〉i∈I ] is
also relevant, then a occurs in P and/or in one of the ci for some i ∈ I .
In words, if a conformant process P sends some configuration 〈m1 , . . . , mn 〉 of messages to an object a with type t , then t[〈m1 , . . . , mn 〉] is usable, meaning that there is a
valid configuration of t that includes (but is not necessarily equal to) 〈m1 , . . . , mn 〉. That
is, P has not violated the protocol of a. Moreover, if t[〈m1 , . . . , mn 〉] is also relevant,
meaning that there are pending obligations with respect to a, then there is at least
one reference to a in the system that may be used for this purpose.
Concerning protocol completion, and therefore deadlock freedom, we have:
Definition 6 (deadlock-free process). We say that P is a deadlock-free process if,
whenever ;  P =⇒ D, a : t = C  〈a!mi (ci )〉i∈I , P (* ∪ +)∗ X→ and there are no
messages targeted to a in P , then t[〈mi 〉i∈I ] is irrelevant.
1

Strictly speaking, t[〈M1 , . . . , Mn 〉] depends on the order in which the Mi ’s are considered, but
it can be shown that all the possible outcomes are equivalent, cf. Lemma 2.

15:8

Luca Padovani

In words, if ;  P reduces to a state from which no further reductions are possible
and we consider the overall configuration 〈m1 , . . . , mn 〉 of messages targeted to an
object a of type t , then t[〈m1 , . . . , mn 〉] is irrelevant, meaning that 〈m1 , . . . , mn 〉 is a valid
configuration of t . That is, P has no unfulfilled obligations with respect to a.
Example 2. Consider again the program in Section 1 and recall from Example 1 that its
execution halts in a state consisting of the messages future!EMPTY, future!Get(user)
and user!WRITE(future). We have #FutureT[〈EMPTY, Get〉] ' Resolve ·∗Get which
is usable and relevant. Therefore, the program is conformant but not deadlock free. 
Note that this definition of deadlock freedom is more general than the mere absence
of junk messages. Specifically, Definiton 6 tolerates the presence unconsumed messages
targeted to a if this is allowed by its type t . This notion of deadlock freedom accounts
for the presence of state messages, such as RESOLVED in the case of future, which
need not be consumed in case no more users of the object remain (see Example 3). On
the other hand, we can obtain a particular instance of Definition 6 which is easier to
understand by taking I = ;. In this case, deadlock freedom translates as the property
that, if the system halts and no messages are targeted to an object a of type t , then it
is because the empty configuration of messages is valid for t .

3

Examples

In this section we use a series of simple programs to introduce the notion of object
dependency, the key mechanism at the base of our analysis technique. To keep the
discussion focused, we take the stance that the analysis should flag those programs
that leave unconsumed messages (which we call “junk”) when their execution halts.
As we have remarked at the end of the previous section, this is only a particular case
of undesirable program behavior captured by Definition 6.
The first program we consider concerns an object obj with a single reaction that
fires when obj receives both an A message and a B message:
new obj : *(A · B) [ A & B x done ] in obj!A

This program is unable to make any progress because there is no B message that
can form a molecule with the A message and trigger the only reaction of obj. As a
consequence, the A message cannot be consumed and becomes junk. Conversely, in
new obj : *(A · B) [ A & B x done ] in obj!A & obj!B & obj!B

there are too many B messages. One of them can combine with A and be consumed
by the reaction, but the other one becomes junk. Neither of these two programs is
conformant according to Definition 5 because their final state contains a B message,
the type (∗(A · B))[B] ' A · ∗(A · B) is relevant, and no other occurrence of obj exists
in the program. Indeed, they are both ill typed according to the typing discipline of
Crafa and Padovani [16], which ensures conformance of well-typed programs.
Unfortunately, conformance alone does not always suffice to prevent junk messages.
An example of conformant but deadlocked program is shown below:

15:9

Deadlock-Free Typestate-Oriented Programming

new obj 1 : *(A · B(A)) [ A & B(x) x x!A ] in
new obj 2 : *(A · B(A)) [ A & B(y) x y!A ] in obj 1 !B(obj 2 ) & obj 2 !B(obj 1 )

Here we have two objects obj1 and obj2 , each reacting to a molecule consisting of
one A message and one B message. There are two B messages respectively targeted
to obj1 and obj2 and, from a syntactic viewpoint, also two A messages targeted to
the same objects via the outputs y!A and x!A, respectively. However, the program is
deadlocked according to Definition 6 because neither reaction can fire and (∗(A · B))[B]
is relevant. The origin of the problem can be traced to the code following the last in,
where obj2 is the argument of a message targeted to obj1 , meaning that the obligation
to send an A message through this occurrence of obj2 may not be fulfilled until obj1 ’s
reaction fires. Symmetrically, obj1 is the argument of a message targeted to obj2 ,
meaning that the obligation to send an A message through this occurrence of obj1
may not be fulfilled until obj2 ’s reaction fires. It is this mutual dependency between
obj1 and obj2 that prevents the program from making any progress. What we learn
from this example is that the arguments of a message depend on the target of the very
same message and the presence of mutual dependencies may result into a deadlock.
A somewhat degenerate case of mutual dependency is shown in the program
new obj : *(A · B(A)) [ A & B(x) x x!A ] in obj!B(obj)

where the A message that is needed to fire the only reaction of obj is produced by the
reaction itself. Here we see that a self-dependency arises if the same object (obj in this
case) is both the target and an argument of the same message.
Regrettably, not all self-dependencies are so easy to spot. Sometimes they arise as
the result of more complex interactions. For example,
new obj 1 : *(A · B(A)) [ A & B(x) x x!A
] in
new obj 2 : *C(B(A),A) [ C(x,y)
x x!B(y) ] in obj 2 !C(obj 1 , obj 1 )

leads to a self-dependency on obj1 by the firing of the reduction of obj2 , when obj1 is
substituted in place of both x and y. Yet, x and y are syntactically different variables
in the source code of the program. The suspicious trait in this example is the fact
that obj1 occurs twice as argument in the same message. Preventing the same object
to occur more than once in a single message is a common strategy at the heart of
several type systems ensuring the absence of deadlocks [11, 44, 31]. Unfortunately,
the availability of join patterns that sets the Objective Join Calculus apart from other
models of communicating processes renders this strategy ineffective. For example
new obj 1 : *(A · B(A))
[ A
& B(x) x x!A
] in
new obj 2 : *(C(B(A)) · D(A)) [ C(x) & D(y) x x!B(y) ] in
obj 2 !C(obj 1 ) & obj 2 !D(obj 1 )

leads to the same self-dependency on obj1 as before, except that here obj1 is never
used twice in the same message. In this case, the only hint at a potential problem is
that the same dependency (of obj1 on obj2 ) arises twice. In summary, the multiplicity
of dependencies – and not just the presence or lack thereof – is relevant, even if these
dependencies do not form cycles.

15:10

Luca Padovani

Our type system flags as ill typed all the programs shown in this section by combining
the enforcement of object protocols with a mechanism that tracks object dependencies.
It is now time to look at the acutal typing rules and this mechanism in greater detail.

4

The Type System

As usual we need type environments for tracking the type of free names when typing
processes, patterns and molecules. We introduce the corresponding notation below.
Definition 7 (type environment). A type environment Γ is a partial map from names to
types equivalently written u1 : t 1 , . . . , un : t n or u : t . We write dom(Γ ) for the domain
of Γ , ; for the empty type environment, Γ (u) for the type associated with u in Γ when
u ∈ dom(Γ ) and Γ1 , Γ2 for the union of Γ1 and Γ2 when dom(Γ1 ) ∩ dom(Γ2 ) = ;.
If two processes share the same name u, they must be typed using type environments
whose respective domains are not disjoint. For example, if P uses u according to the
type t and Q uses u according to the type s, they will be typed in type environments
containing the associations u : t and u : s respectively. Overall, u is used by P & Q
according to the type t · s. To account for this possibility, we need to define a way of
combining type environments that is more flexible than disjoint union.
Definition 8 (type environment combination). The combination of Γ1 and Γ2 is the
type environment Γ1 · Γ2 such that dom(Γ1 · Γ2 ) = dom(Γ1 ) ∪ dom(Γ2 ) and defined by


if u ∈ dom(Γ1 ) \ dom(Γ2 )
Γ1 (u)
def
(Γ1 · Γ2 )(u) = Γ2 (u)
if u ∈ dom(Γ2 ) \ dom(Γ1 )


Γ1 (u) · Γ2 (u) if u ∈ dom(Γ1 ) ∩ dom(Γ2 )
In order to enforce deadlock freedom, the type system tracks dependencies between
objects to detect potentially dangerous circularities.
Definition 9. A dependency relation D is an irreflexive, symmetric and transitive
relation on names. We write dom(D) for the domain of D, we write u ∼ v for the
relation {(u, v), (v, u)} when u 6= v and D+ for the transitive closure of D.
As we have discussed in Section 3, a dependency is established between two names
u and v if they occur in the same message, as in u!m( v ). The rationale is that the
eventual use of v depends on the firing of a reaction of u allowing v to be received. The
following notion of compatibility characterizes those cases in which the combination
of two dependency relations is guaranteed not to generate mutual dependencies.
Definition 10 (compatibility and dependency union). We say that D1 and D2 are
compatible if D1 ∩ D2 = ; and (D1 ∪ D2 )+ is irreflexive. If D1 and D2 are compatible,
then we write D1 t D2 for (D1 ∪ D2 )+ . Otherwise, D1 t D2 is undefined.
In words, two dependency relations D1 and D2 are (mutually) compatible if they
have no dependency in common (D1 ∩ D2 = ;) and if their union does not generate any

15:11

Deadlock-Free Typestate-Oriented Programming

circular dependency by transitivity. The user of the future variable (Section 1) contains
the sub-processes user!WRITE(future) and future!Get(user). Each of them yields
def
the dependency relation D = {(user, future)} and D ∩ D = D 6= ;. This suggests that
the parallel composition of user!WRITE(future) and future!Get(user) is dangerous,
for the respective dependency relations are incompatible. A similar thing happens
between obj1 and obj2 in Section 3. To see the reason why it is important to also
check whether (D1 ∪ D2 )+ is irreflexive, consider the parallel composition


a!m( b) & c !m(d ) & a!m(c ) & b!m(d )
and observe that the four messages (read from left to right) respectively yield the
def
def
def
def
dependency relations D1 = {(a, b)}, D2 = {(c, d)}, D3 = {(a, c)} and D4 = {(b, d)}.
Note that (D1 t D2 ) ∩ (D3 t D4 ) = ;, meaning that the two top-level sub-processes
do not share any common dependency. However, if we combine all the relations
together we obtain (a, a) ∈ ((D1 t D2 ) ∪ (D3 t D4 ))+ . Indeed, D1 t D2 and D3 t D4
are incompatible because the transitive closure of their union is not irreflexive.
We proceed describing the typing rules, shown in Table 3. We start from the typing
rules for molecules, which derive judgments of the form Γ ` M :: t where Γ collects
the associations for all the arguments of the messages in M and t is the overall type
of the molecule, intended as the product of the message types of each message in
it. The rules [t-msg-m] and [t-comp-m] are straightforward, but for two caveats. First,
the side condition in [t-msg-m] makes sure that each message argument has a usable
type. Without this condition, which is crucial for the soundness of the type system, it
would be possible to have well-typed processes that violate protocols by exploiting
the property that 0 is the absorbing element of the · connective. A detailed account of
this phenomenon is given by Crafa and Padovani [16]. The second caveat is that the
two rules enforce a one-to-one correspondence between names in Γ and arguments
of M , meaning that there cannot be two equal arguments in the same molecule. Note
in particular the disjoint union Γ1 , Γ2 (as opposed to the combination Γ1 · Γ2 ) in the
conclusion of [t-comp-m]. This is a restriction compared to the original version of the
type system [16] that is necessary to enforce deadlock freedom (cf. Section 3).
The judgments for processes have the form Γ ` P • D, meaning that P is well typed
in Γ , which collects the names used by P , and yields the dependencies described by D.
According to [t-done], the terminated process is well typed in the empty environment
(it uses no names) and yields no dependencies.
Rule [t-send] deals with processes of the form u! M . The premise Γ ` M :: t verifies
that the molecule M is well typed in Γ and establishes its type t , which describes
how u is used in this process. The rule also establishes a dependency between the
target of the message u and each of the arguments occurring in M . Notice the disjoint
union u : t, Γ in the conclusion of the rule, indicating that u cannot occur as any of
the arguments in M , thereby excluding a self-dependency on u (cf. Section 3).
Rule [t-par] deals with parallel compositions P1 & P2 . Each Pi is required to be
well typed in a type environment Γi and yields the dependencies in Di . The overall
composition is well typed in the composition Γ1 · Γ2 , meaning that in general P1 and P2
are allowed to share the names of objects on which they operate concurrently. Recall

15:12

Luca Padovani

Typing rules.

Table 3

Γ `P •D

Typing rules for processes
[t-weak]

[t-done]

[t-new]

; ` done • ;

Γ,a : s ` P • D t ¶ s
Γ ` new a : t = [C ] in P • D \ a live(t, X)

Γ `P •D

a : t ` C :: X

Γ,u : 1 ` P • D
[t-send]

[t-par]

Γ ` M :: t
F
u : t, Γ ` u! M • v∈dom(Γ ) u ∼ v

Γ1 ` P1 • D1

Γ2 ` P2 • D2

Γ1 · Γ2 ` P1 & P2 • D1 t D2
Γ ` M :: t

Typing rules for molecules
[t-msg-m]

[t-comp-m]

u : t ` m(u) :: m( t )

Γ1 ` M1 :: t 1

t usable

Γ2 ` M2 :: t 2

Γ1 , Γ2 ` M1 & M2 :: t 1 · t 2
Γ ` J :: A

Typing rules for patterns
[t-comp-p]

[t-msg-p]

x : t ` m( x ) :: 〈m( t )〉

t usable

Γ1 ` J1 :: A1

Γ2 ` J2 :: A2

Γ1 , Γ2 ` J1 & J2 :: A1 ] A2
a : t ` C :: X

Typing rules for classes
[t-reaction]

x : s, a : s0 ` P • D t ¶ s
t 0 ¶ t 0 [A] · s0
a : t 0 ` J x P :: {A}
t0 ↓ A

x : t ` J :: A

Typing rule for solutions

[t-class]

a : t ` Ci :: Xi

(1≤i≤2)

a : t ` C1 | C2 :: X1 ∪ X2
`D P

[t-solution]
(i∈I)

{ai : si }i∈I ` & j∈J P j • D ∀i ∈ I : t i ¶ si
∀i ∈ I : live(t i , Xi )
` {ai : t i = Ci }i∈I  〈P j 〉 j∈J

ai : t i ` Ci :: Xi

15:13

Deadlock-Free Typestate-Oriented Programming

from Definition 10 that D1 t D2 is defined provided that D1 and D2 are compatible.
Therefore, [t-par] is applicable only in this case.
Rule [t-new] deals with object definitions of the form new a : t = [C ] in P . The
premise Γ , a : s ` P • D checks that the continuation P is well typed in a type
environment enriched with an association a : s for the object being defined. Notice
that t (the type of the object as declared in the program) and s (the type according to
which the object is used by P ) are not required to be equal. It suffices that P conforms
with t , which is expressed by the side condition t ¶ s. The premise a : t ` C :: X
checks that the object’s class is consistent with the object’s type. We will describe the
typing rules for classes in a moment. For the time being, it suffices to know that the
set X collects the multisets of tags corresponding to the patterns in C and is used to
understand which valid configurations of t are capable of triggering a reaction by
means of the side condition live(t, X). The predicate live(t, X) is defined thus:
Definition 11 (live object). For all t and sets of configurations X we have
def

live(t, X) ⇐⇒ ∀A ∈ J t K : (>B ∈ X : B ⊆ A) ⇒ ∀m(s) ∈ A : s ¶ 1
The meaning of live(t, X) is simpler than its definition suggests. In practice, live(t, X)
holds if, for any message m(s) of a valid configuration A of t that may become “junk”
(because A is unable to fire one of the reactions of the object), there are no unfulfilled
obligations with respect to any of its arguments (s ¶ 1). Note that, when A is the
empty configuration, there is obviously no reaction that can fire (all patterns match
at least one message) and the predicate holds vacuously. Example 3 illustrates the
liveness predicate for the future object of Section 1.
To complete the description of [t-new], the dependency relation D \ a yielded by a
definition for a is simply the restriction of D to dom(D) \ {a}.
The last typing rule for processes is [t-weak], whose only purpose is to introduce in
the type environment an association for a name u which is not used by a process. We
know that u is not used because the disjoint union u : 1 with Γ prevents u from being
in dom(Γ ). The type of u is necessarily 1, given that u is not used. For the same reason,
the dependencies yielded by P do not change. This rule is useful in combination with
[t-new] and [t-reaction], which make assumptions on the presence of given associations
in the type environment.
The typing rules [t-msg-p] and [t-comp-p] for patterns derive judgments of the form
Γ ` J :: A, meaning that J matches the configuration of messages A and binds the
arguments in Γ . The side condition in [t-msg-p] checks that message arguments are
usable, for the same reason discussed earlier for [t-msg-m]. The two rules enforce
variable linearity, ensuring that a pattern cannot bind the same argument twice.
The typing rules for classes derive judgments of the form a : t ` C :: X, meaning that
the class C of a is consistent with the type t of a. As we have anticipated, X collects
the configurations matched by the patterns in the reactions of C . The important rule
is [t-reaction], [t-class] being straightforward. A reaction J x P of an object a is well
typed if so is P . The premise x : t ` J :: A extracts from the pattern J the environment
x : t of arguments bound by J and the configuration A of messages matched by J .
The process P is checked in a type environment that contains associations x : s for the

15:14

Luca Padovani

arguments and one association a : s0 for a. That is, P is allowed to use the very same
object it belongs to, pretty much as Java methods are allowed to use this. The side
condition t ¶ s checks that P uses the arguments x conforming to their types. The
side condition t 0 ¶ t 0 [A] · s0 performs an analogous check, but concerns a itself and
is a little more involved. To grab the essence of the condition, recall that a reaction
consumes a configuration A of messages among those targeted to a and spawns a
copy of P which, in general, will produce new messages targeted to a according to the
type s0 . The reaction must maintain the overall configuration of messages targeted to
a valid according to the type t 0 of a, whence the side condition: after the reaction has
fired and the A messages have been consumed, the remaining messages targeted to a
will be in a configuration described by t 0 [A]. This type is combined with s0 , which
describes all the configurations of messages that P may target to a. The resulting
type must be a supertype of t 0 . The last side condition t 0 ↓ A makes sure that the
environment x : t correctly reports the type of the received arguments, considering
that within t 0 there may be different message types with the same tag and arity. The
predicate is formalized thus:
def

Definition 12. t ↓ 〈mi ( t i )〉i∈I ⇐⇒ {〈mi (s i )〉i∈I | 〈mi (s i )〉i∈I∪J ∈ J t K} = {〈mi ( t i )〉i∈I }.
In words t ↓ A holds if, given a pattern of an object of type t that matches a
configuration A of messages, the type of the arguments of the messages is uniquely
determined. As an example, suppose that t = A · m(s1 ) + B · m(s2 ) where s1 and s2
are different types. Then t ↓ 〈m(s1 )〉 does not hold, because a pattern that matches
only an m-tagged message might receive an argument of type s1 or s2 . On the other
hand, t ↓ 〈A, m(s1 )〉 holds since an m-tagged message in combination with an A-tagged
message can only have an argument of type s1 . Note that t ↓ A implies that t[A] is
usable. In other words, the reaction J x P is not dead code.
A possibly alarming aspect of [t-reaction] is that the dependency relation D yielded
by P does not play any role in the conclusion of the rule. One might wonder whether the
firing of the reaction could, in principle, introduce new dangerous dependencies that
were not present before. To see the reason why this is not possible, it is useful to look
back at the reduction rule [red] in Table 2. Before a reaction of a fires, the solution must
contain a process of the form a! M . From [t-send] and the typing rules for molecules,
we see that this process yields dependencies between a and all the arguments in M . In
other words, the dependency relation of a! M before the reduction is total. Given that
the only free names of P can be a and the arguments received from M , its dependency
relation D is necessarily included in a total one with the same domain. Note however
that P may indeed introduce new dependencies involving objects that are created by
P itself. These new dependencies are not visible in D because they have been removed
by the restriction operator \ that we have discussed with [t-new]. In summary, the fact
that classes cannot introduce dependencies that are not observable in their clients has
two fundamental consequences on the compositionality of our approach: first, there
is no need to record any information on the dependencies yielded by a class; second,
classes can be compiled separately and no global program analaysis is necessary in
order to ensure deadlock freedom.

15:15

Deadlock-Free Typestate-Oriented Programming

The only typing rule for solutions derives judgments of the form ` D  P . The
rule does not introduce new interesting elements. Basically, it checks that each object
definition in D is well typed and so is the parallel composition of all the processes
in P . The side conditions are exactly those we have already discussed for [t-new],
repeated here for all the object definitions in D .
Theorem 1 (soundness). If ; ` P • D, then P is conformant and deadlock free.
The proof of this theorem goes through a series of standard results, including type
preservation. The details are given in Appendix A.
def

Example 3. Given the type #FutureT = (EMPTY · Resolve(int) + RESOLVED(int))·
∗Get it is possible to obtain a typing derivation for the composition of the future
object in Section 1 and the user object defined as
new user : #UserT [ Reply(n) x System!Print(n) ]
in future!Resolve(42) & future!Get(user)

which resolves future and simultaneously attempts to retrieve its value.
In particular, for the future object we have that live(#FutureT, X) holds, where
X = {〈EMPTY, Resolve(int)〉, 〈RESOLVED(int), Get(Reply(int))〉}. Indeed, the
only valid configuration of #FutureT that is unable to trigger a reaction of future is
〈RESOLVED(int)〉 and int is (assumed to be) irrelevant. There is only one dependency between future and user established by the message future!Get(user). Therefore, according to Theorem 1, the program is both conformant and deadlock free. Note
that, when the execution of the program halts, the message future!RESOLVED(42)
is left unconsumed. According to Definition 6, the presence of this message is not a
violation of deadlock freedom because #FutureT[RESOLVED] is irrelevant. In other
words, #FutureT specifies that a message configuration consisting of a lone RESOLVED
message is legal for future, even if this configuration is unable to trigger any reaction
of future.


5

More Examples

In this section we show a few more well-typed programs that can be successfully
analyzed with the tool CobaltBlue that implements our type system. In order to deal
with more interesting examples, we introduce some syntactic sugar on top of the pure
Objective Join Calculus to model classes and synchronous operations.
5.1 Classes

A class is modeled as an object with a New operation that creates instances of the class
it represents. For example, below is the class of future variables:
1 class Future [ New(r) x
2
new this : #Future
3
[ EMPTY
& Resolve(n) x this!RESOLVED(n)
4
| RESOLVED(n) & Get(user) x user!Reply(n) & this!RESOLVED(n) ]

15:16

Luca Padovani

5
in this!EMPTY & r!Reply(this)
6 ]

The code on line 5 effectively corresponds to the constructor of the class, which
initializes the instance to the EMPTY state and sends a reference to the instance back to
the object r that issued the request. Besides the improved readability, the advantage
of using a dedicated class keyword instead of defining Future as a plain object is
that we inform CobaltBlue that Future is a stateless object: its only reaction has a
simple join pattern involving only one message, meaning that the use of Future cannot
contribute in creating any significant dependency between objects. This helps keeping
dependency relations small, reducing the possibility that mutual dependencies arise.
5.2 Synchronous Operations

In addition to asynchronous message passing, CobaltBlue provides syntactic sugar for
synchronous operations, namely messages from which we expect to receive a result.
As an example, we can model a deadlocking user with synchronous operations thus:
let future = Future.New in future!Resolve(future.Get)

This code creates an instance future of the class Future and attempts to resolve
future with the value it contains. Notice the use of the ‘.’ instead of ‘!’ when we send
a message and we expect to receive a result. This code is automatically desugared to:
1 new cont 1 [ Reply(future) x
2
new cont 2 [ CLOSURE(future) & Reply(n) x future!Resolve(n) ]
3
in cont 2 !CLOSURE(future) & future!Get(cont 2 ) ]
4 in Future!New(cont 1 )

The output of New targeted to Future is now at the bottom (line 4) and contains
the reference to a continuation object cont1 which will receive the fresh instance of
the future variable (line 1). When this happens, a Get message is sent to future along
with another continuation object cont2 to retrieve the value from the future variable
(line 3). Since the continuation also needs to access the future variable, we store a
reference to it into a CLOSURE message. When (hypothetically) the future variable
returns its content, the reaction on line 2 fires and future is resolved. By looking at
the desugared version of the code it is clear where the type checker spots the problem:
both outputs on line 3 involve cont2 and future. Hence, the intersection of their
dependency relations is not empty – it contains the pair (cont2 , future) – and their
parallel composition is ill typed. A well-typed variant of the program is
let future = Future.New in
future!Resolve(42) & System!Print(future.Get) & System!Print(future.Get)

where the future variable is resolved and queried by three independent processes.
In addition to synchronous messages, CobaltBlue supports conditional processes,
built-in arithmetic operators, anonymous object definitions and other extensions
that facilitate writing more complex examples. We will make use of some of these
extensions in the rest of the section, bearing in mind that they are all translated into
the core language presented in Section 2 before type checking.

15:17

Deadlock-Free Typestate-Oriented Programming
5.3 Gregory–Leibniz Approximation of π

We revisit a frequently used case study for the actor model which concerns the
computation of a finite approximation of π using the Gregory–Leibniz series:


∞
X
1 1 1
(−1)n
π=4
= 4 1 − + − + ···
2n + 1
3 5 7
n=0

To compute an approximation of π using this series, we devise a network of worker
processes, each responsible for a finite range of the series. We arrange the workers
as a binary tree so that each leaf takes care of computing a single term of the series
whereas each inner node collects the partial results from its children and sends their
sum back to its parent. Below is the implementation of the Worker class:
1 class Worker [ New(depth, from, parent) x
2
new this : #Worker
3
[ LEAF(n, parent) x parent!Reply(4. × (1 - (n % 2) × 2) / (2 × n + 1))
4
| BRANCH(parent) & Left(x) & Right(y) x parent!Reply(x + y) ]
5
in if depth = 0 then
6
this!LEAF(from, parent)
7
else
8
this!BRANCH(parent) &
9
let half = from + Number.Pow(2, depth - 1) in
10
Worker!New(depth - 1, from, [ Reply(v) x this!Left(v) ]) &
11
Worker!New(depth - 1, half, [ Reply(v) x this!Right(v) ])
12 ]
13 System!Print(Worker.New(10, 0))

The constructor is parametric in the depth of the tree to be built and the initial
index from of the series to compute. A worker is either a LEAF or a BRANCH. A LEAF
computes the term of the series corresponding to index n, sends the result to its parent
and terminates (line 3). A BRANCH waits for partial results x and y from both its left
and right children (note the use of a three-way pattern). As soon as it has collected
all the necessary information, it notifies parent and terminates (line 4). The body of
the constructor determines whether the worker is a leaf or a branch and sets its state
accordingly (lines 5–11). In the latter case, two children are spawned and assigned
appropriate ranges of the series to compute (lines 10–11). A critical aspect here is
that children answer their parent using a Reply message, whereas branches expect to
receive Left and Right messages. For this reason, the two children are not connected
directly with their parent branch, but rather with two anonymous objects whose only
purpose is to translate the Reply message coming from each child to a Left or Right
message directed to the parent, as appropriate. The last line creates a network with
2047 workers split into 1024 leaves and 1023 branches.
The program is well typed by taking the following type definitions
type
and
and
and

#Worker
#Leaf
#Branch
#Reply

=
=
=
=

#Leaf + #Branch + 1
LEAF(#Number, #Reply)
BRANCH(#Reply) · Left(#Number) · Right(#Number)
Reply(#Number)

15:18

Luca Padovani

hence from Theorem 1 we deduce that, if the program halts (it does), no workers have
been left behind. Indeed, LEAF and BRANCH have relevant arguments (#Reply 6¶ 1),
meaning that in a terminated program there cannot be such messages around.
5.4 Sieve of Eratosthenes

We model the sieve of Eratosthenes as a chain of objects generating and processing
a stream of natural numbers. At the leftmost end of the chain we have a Generator
object that produces an infinite stream of natural numbers, starting from 2. At the
rightmost end of the chain we have a Printer object that emits each number it receives
on the terminal. For each received number n, Printer creates a new Filter object
that removes from the stream all the subsequent numbers that are divided by n. This
way, Printer only receives and prints prime numbers.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

class Generator [ New(n, r) x
new this : #Generator
[ FROM(n) & Get(target) x this!FROM(n + 1) & target!Reply(n, this) ]
in this!FROM(n) & r!Reply(this)
]
class Filter [ New(k, source, r) x
new this : #Filter
[ READY(k, source) & Get(target) x this!WAIT(k, source, target)
| WAIT(k, source, target) x
let n, source = source.Get in
if n % k = 0 then this!WAIT(k, source, target)
else this!READY(k, source) & target!Reply(n, this) ]
in this!READY(k, source) & r!Reply(this)
]
class Printer [ New(source) x
new this : #Printer
[ RUN(source) x
let n, source = source.Get in
this!RUN(Filter.New(n, source)) & System!Print(n) ]
in this!RUN(source)
]
Printer!New(Generator.New(2))

The Generator (lines 1–5) has a single state FROM containing the next number
n in the stream. This is returned and incremented when the object receives a Get

message from the next object in the chain (line 3). The Printer object (lines 15–21)
also has a single state RUN containing a reference source to the object from which it
receives prime numbers. It repeatedly sends Get messages to source (line 18) and
installs a corresponding new Filter which becomes the new source of numbers for
the subsequent iteration (line 19). Each Filter (lines 6–14) is parametric in the factor
k it uses to filter out numbers from the stream and the source object from which it
retrieves numbers and can be in one of two states. When in state READY, the filter
waits for a Get request from the object target at its right. At this point, it moves to
state WAIT, where it stays as long as the number n retrieved from source is a multiple
of k (lines 10–11). As soon as the filter receives an n that is not a multiple of k, it
notifies target with the number and moves back to state READY (line 12).

15:19

Deadlock-Free Typestate-Oriented Programming

Given appropriate definitions for #Generator, #Filter and #Printer (see Appendix B),
the program is well typed and therefore deadlock free. Notice that the chain of objects
increases in size each time a new prime number is discovered and that deadlock
freedom guarantees that the program will run forever.

6

Related Work

We provide an overview of other type-based approaches to the enforcement of deadlock
freedom or similar properties in systems of interacting processes.
Several type systems ensuring deadlock freedom (and sometimes stronger properties) for processes communicating through channels annotate
channel types with levels describing the (abstract) moment in time the channel
is going to be used for an I/O action. Dependency relations between levels capture the causal dependencies between these actions and the absence of circular
dependencies implies deadlock freedom. The technique has been pioneered in the
π-calculus by Kobayashi [26, 27, 28] and later adapted to more specific communication models including binary sessions [32], the conversation calculus [38], the linear
π-calculus [33, 36, 35] and functional languages with linear communications [37].
Kobayashi [26] shows how the technique can be used for analyzing concurrent objects
modeled in the π-calculus. In general, tracking dependencies between the single I/O
actions (instead of whole channels or object names) allows for a more fine-grained
and precise analysis. For example, the type systems described by Padovani [33] and
Kobayashi and Laneve [29] can establish deadlock freedom for some classes of cyclic
process networks, whereas our typing discipline can only deal with acyclic object
networks. However, the more complex type structure of these works hampers compositionality. In particular, local changes to the network often have non-local effects of
the typeability of the system to the point that it may be necessary to re-assign level
annotations and re-type the smaller sub-systems. In particular, all of the aforementioned approaches except for [38, 29] use integer or natural numbers for representing
levels and the typeability of a parallel composition depends on the absolute value of
the levels in channel types.
Ordered I/O actions

Multiparty session types [25, 3] promote a top-down
methodology for the design of session-based communication systems guaranteeing
deadlock freedom among the participants of the session. In this approach, the network
topology and the sequence of interactions is described a priori in a specification
called global type (roughly, a finite-state automaton whose transitions correspond to
interactions) and checked for some mild consistency conditions. The specification is
then projected into local types that are matched against each process corresponding
to one of the participants of the session. If the local types and the participants do
match, the participants are guaranteed to communicate safely and without deadlocks.
This approach is viable when the whole system is being developed, but changes in the
network topology or in the number of participants may require a substantial re-design
Deadlock-freedom by design

15:20

Luca Padovani

of the global type. Also, deadlock freedom is guaranteed provided that participants
do not interleave communications on different sessions. Hybrid approaches that
relax this constraint and are based on a global ordering on sessions have also been
considered [13, 14].
There is a close relationship between
session types and linear logic propositions resulting in a Curry-Howard correspondence between proofs and session-based programs [11, 44, 31]. The deadlock-freedom
property guaranteed by the type systems in these works is a direct consequence of their
connection with linear logic, whereby each communication corresponds to a step of
cut elimination. Our approach to deadlock freedom has been inspired by these works
in the sense that the typing rules enforce a forest-like topology between concurrent
objects without requiring any form of type annotation or global order on actions. The
resulting compositionality of the type system is best illustrated by the typing rules for
classes ([t-reaction] and [t-class]), which do not propagate any of the dependencies
arising within a class outside the class itself. This means not only that objects can be
type checked independently, but also that if the code of an object changes but its public
interface does not, there is no need to re-check any of the other objects it interacts
with. There are also major differences between the aforementioned session-based
approaches and our own. First of all, session endpoints are linear resources, there are
no races and interactions are triggered by complementary input/output actions. On
the contrary, concurrent objects may be shared among several processes, there can be
concurrent attempts to access/modify them and several messages may be necessary
in order to trigger a reaction. Another technical difference with our approach is the
formulation of the typing rule for parallel composition. In the type systems for sessions
there are no explicit dependency relations and a parallel composition of two processes
is well typed provided that the composed processes share at most one session. This
condition is easy to check looking at the type environments of the two processes
and suffices to prevent cycles in the resulting network topology. However, it is not
as robust as compatibility with respect to the usual laws of structural congruence
(commutativity and associativity of parallel composition). This slightly complicates
the soundness proof of the type system and, more importantly, it implies that in order
to type a program it may be necessary to rearrange parallel compositions so that the
condition holds. This might not be always practical, if the bits that must be moved
around are in modules whose source code is not available or cannot be changed.
A recent work by Balzer and Pfenning [5] relaxes session typing disciplines in such a
way that a session endpoint may be shared among several processes. A shared endpoint
must be acquired before being used in mutual exclusion and then released. The sharing
is manifest in the sense that the type of a shareable endpoint is explicitly marked at
the points where acquisition and release can/must occur. In our type system, sharing
is also manifest in the sense that it is regulated by the · and ∗ type connectives. The
former one allows object sharing among a fixed number of processes. For example,
each inner node in the network of worker processes of Section 5.3 is shared between
its two children. The ∗ connective allows for unrestricted sharing. For example, a
future variable can be read by arbitrarily many users (Section 5.2). There is no need
Logically-inspired type systems for sessions

15:21

Deadlock-Free Typestate-Oriented Programming

for native mechanisms of object acquisition and release because they can be modeled
using structured synchronization patterns [16]. Balzer and Pfenning’s type system is
unable to ensure deadlock freedom when shared endpoints are involved, whereas our
type system ensures deadlock freedom even in the presence of shared objects. Another
key trait of Balzer and Pfenning’s type system is that it enforces equi-synchronization
on session endpoints: the state of an endpoint being released must be the same it had
at the time of acquisition. This constraint is relaxed in our model thanks to the use
of structured synchronization patterns. An acquisition request on a shared object is
suspended until the object moves into a state where the request can be satisfied. As
an example, all attempts to read an unresolved future variable remain pending until
the variable moves into the RESOLVED state (Section 5.2).
Go programs with shareable channels Lange, Ng, Toninho, and Yoshida [30] present
a type system for MiGo, a sub-language of Go focusing on communications and gor-

outines. The type system allows channels to be shared among several processes and
guarantees deadlock freedom for well-typed programs. From a methodological standpoint, this type system differs significantly from our own since the typing rules perform
little to no checks on the Go program being analyzed. Rather, the main purpose of the
typing rules is to synthesize a type that describes at an abstract level the communications performed by the program. In fact, the type of a program is a term of a first-order
process calculus such that liveness of the type (which is established by a subsequent
model checking phase) implies liveness of the corresponding program. Therefore,
even though the synthesis phase is compositional by definition, it is necessary to
perform a global analysis on the type corresponding to the whole program in order
to assess the absence of deadlocks. As the program is modified or expanded with
new components, the corresponding type must be synthesized and model checked
again. In contrast, our typing rules do not rely on any subsequent analysis, whence
the compositional enforcement of deadlock freedom. An advantage of the global
analysis is that it may result into better precision. For example, the modeling of the
dining philosophers discussed by Lange, Ng, Toninho, and Yoshida [30] is ill-typed in
our type system because it relies on a circular network topology. From a technical
standpoint, Lange, Ng, Toninho, and Yoshida limit the sharing of channels among a
finite number of processes. This property, called “fencing” in the paper, is key because
it implies finiteness of the state space analyzed by the model checker. Our type system
allows both finite and unrestricted sharing of objects by means of appropriate type
connectives, as previously discussed.
Bejleri, Mezini, and Eugster [7] define a sub-structural type system
for the e-calculus, a process calculus inspired to the Join calculus for modeling eventdriven, concurrent systems. Among the properties enforced by the type system is
progress, which is akin to deadlock freedom. The main difference between the ecalculus and the Objective Join Calculus is that in the former calculus messages carry
no arguments, thus none on the examples discussed in this paper can be modeled
as such. It could be interesting to investigate whether the type system presented
in this paper subsumes the one defined by Bejleri, Mezini, and Eugster as far as
Other approaches

15:22

Luca Padovani

deadlock freedom is concerned. Perera, Lange, and Gay [39] sketch a technique for
checking compatibility and compliance of concurrent objects. The technique is based
on communicating automata and on notions of automata composition rather than
types. Also in this case, systems where objects are created dynamically and messages
with arguments are not considered.

7

Concluding Remarks

Programming large-scale concurrent systems is notoriously difficult and error-prone.
Over the years, programmers have strived to make this activity less frustrating and
more productive by adopting specific programming models and abstractions. In this
work we propose a type-based approach for the compositional specification and
implementation of such systems. The approach extends and refines the TypestateOriented Programming paradigm [17, 2, 42, 21] to a concurrent setting and is based
on three key ingredients: a high-level model of concurrent objects with structured
synchronization patterns [18, 19], a behavioral type system for specifying concurrent
object protocols [16], and a mechanism that tracks dependencies between objects.
Compositionality of the approach is guaranteed by the fact that classes can be type
checked independently.
As shown by Crafa and Padovani [16], there are strong analogies between the
Objective Join Calculus [19] and actors [24, 1]. In particular, actors are a special
instance of concurrent objects where the synchronization patterns always match two
messages, one that represents the state of the actor and is always self-inflicted by the
actor with a so-called “become” operation, and another message that represents a
request sent to the actor from a different one. The state message determines which
requests the can be processed by the actor when it is in that state. Most of the examples
in this paper use binary synchronization patterns and therefore adhere to this scheme.
In fact, the actor model is the most popular programming framework to which our
analysis technique can be applied [23]. Our type system also provides a solution to
the quest for a behavioral typing discipline for actors posed by Fowler, Lindley, and
Wadler [20].
The proof-of-concept implementation of the type system [34] shows the feasibility
of our analysis technique. In the implementation, dependency graphs are conveniently
represented using a disjoint-set data structure, allowing for efficient union operations and compatibility checks. Overall, the machinery required for deadlock freedom
analysis adds negligible overhead compared to the original type system of Crafa and
Padovani [16]. An important challenge for future work concerns the integration and
application of the analysis technique described in this paper into a mainstream programming environment. Indeed, the type system makes use of exotic type connectives
and a structural subtyping relation which apparently elude the capabilities of type
systems commonly found in programming languages. One promising direction to
investigate is to devise a variation of the type system that applies to the object code or
bytecode of a program rather than its source code. This way, the type checker could

15:23

Deadlock-Free Typestate-Oriented Programming

be easily integrated in the development workflow as a separate, post-processing tool
without requiring changes to the source language and its compiler.
The author is grateful to the anonymous reviewers for their
questions and thoughtful comments on an early version of this paper.
Acknowledgements

References
[1] Gul Agha. Actors: A Model of Concurrent Computation in Distributed Systems.
MIT Press, 1986. ISBN 0-262-01092-5.
[2] Jonathan Aldrich, Joshua Sunshine, Darpan Saini, and Zachary Sparks. Typestateoriented programming. In Proceedings of the 24th ACM SIGPLAN Conference
Companion on Object-Oriented Programming Systems Languages and Applications
(OOPSLA’09), pages 1015–1022. ACM, 2009. doi:10.1145/1639950.1640073.
[3] Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna,
Pierre-Malo Deniélou, Simon J. Gay, Nils Gesbert, Elena Giachino, Raymond
Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos, and
Nobuko Yoshida. Behavioral Types in Programming Languages. Foundations
and Trends in Programming Languages, 3:95–230, 2016. doi:10.1561/2500000031.
[4] Henry G. Baker and Carl Hewitt. The incremental garbage collection of processes.
SIGART Newsletter, 64:55–59, 1977. doi:10.1145/872736.806932.
[5] Stephanie Balzer and Frank Pfenning. Manifest sharing with session types.
Proceedings of the ACM on Programming Languages, 1(ICFP):37:1–37:29, 2017.
doi:10.1145/3110281.
[6] Nels E. Beckman, Duri Kim, and Jonathan Aldrich. An empirical study of object
protocols in the wild. In Proceedings of the 25th European Conference on ObjectOriented Programming (ECOOP’11), volume LNCS 6813, pages 2–26. Springer,
2011. doi:10.1007/978-3-642-22655-7_2.
[7] Andi Bejleri, Mira Mezini, and Patrick Eugster. Cooperative decoupled processes:
the e-calculus and linearity. In Proceedings of the 15th International Conference
on Modularity (MODULARITY’16), pages 82–93. ACM, 2016. doi:10.1145/2889443.
2889449.
[8] Nick Benton, Luca Cardelli, and Cédric Fournet. Modern concurrency abstractions
for C#. ACM Transactions on Programming Languages and Systems, 26(5):769–
804, 2004. doi:10.1145/1018203.1018205.
[9] Gérard Berry and Gérard Boudol. The Chemical Abstract Machine. Theoretical
Compututer Science, 96(1):217–248, 1992. doi:10.1016/0304-3975(92)90185-I.
[10] Janusz A. Brzozowski. Derivatives of Regular Expressions. Journal of ACM,
11(4):481–494, 1964. doi:10.1145/321239.321249.
[11] Luís Caires and Frank Pfenning. Session Types as Intuitionistic Linear Propositions. In Proceedings of the 21th International Conference on Concurrency Theory

15:24

Luca Padovani

[12]
[13]

[14]

[15]
[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]

(CONCUR’10), LNCS 6269, pages 222–236. Springer, 2010. doi:10.1007/978-3-64215375-4_16.
John Conway. Regular Algebra and Finite Machines. William Clowes & Sons Ltd,
1971. ISBN 978-0486485836.
Mario Coppo, Mariangiola Dezani-Ciancaglini, Luca Padovani, and Nobuko
Yoshida. Inference of Global Progress Properties for Dynamically Interleaved
Multiparty Sessions. In Proceedings of the 15th International Conference on
Coordination Models and Languages (COORDINATION’13), LNCS 7890, pages
45–59. Springer, 2013. doi:10.1007/978-3-642-38493-6_4.
Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, and Luca
Padovani. Global Progress for Dynamically Interleaved Multiparty Sessions.
Mathematical Structures in Computer Science, 26:238–302, 2016. doi:10.1017/
S0960129514000188.
Bruno Courcelle. Fundamental Properties of Infinite Trees. Theoretical Computer
Science, 25:95–169, 1983. doi:10.1016/0304-3975(83)90059-2.
Silvia Crafa and Luca Padovani. The Chemical Approach to Typestate-Oriented
Programming. ACM Transactions on Programming Languages and Systems,
39:13:1–13:45, 2017. doi:10.1145/3064849.
Robert DeLine and Manuel Fähndrich. Typestates for objects. In Proceedings of the
18th European Conference on Object-Oriented Programming (ECOOP’04), volume
LNCS 3086, pages 465–490. Springer, 2004. doi:10.1007/978-3-540-24851-4_21.
Cédric Fournet and Georges Gonthier. The Reflexive CHAM and the Join-Calculus.
In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages (POPL’96), pages 372–385. ACM, 1996. doi:10.1145/
237721.237805.
Cédric Fournet, Cosimo Laneve, Luc Maranget, and Didier Rémy. Inheritance in
the Join Calculus. Journal of Logic and Algebraic Programming, 57(1-2):23–69,
2003. doi:10.1016/S1567-8326(03)00040-7.
Simon Fowler, Sam Lindley, and Philip Wadler. Mixing metaphors: Actors as
channels and channels as actors. In Proceedings of the 31st European Conference on
Object-Oriented Programming (ECOOP’17), volume 74 of LIPIcs, pages 11:1–11:28.
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. doi:10.4230/LIPIcs.
ECOOP.2017.11.
Ronald Garcia, Éric Tanter, Roger Wolff, and Jonathan Aldrich. Foundations of
typestate-oriented programming. ACM Transactions on Programming Languages
and Systems, 36(4):12, 2014. doi:10.1145/2629609.
Philipp Haller and Tom Van Cutsem. Implementing joins using extensible pattern
matching. In Proceedings of the 10th International Conference on Coordination
Models and Languages (COORDINATION’08), LNCS 5052, pages 135–152. Springer,
2008. doi:10.1007/978-3-540-68265-3_9.
Philipp Haller and Frank Sommers. Actors in Scala - concurrent programming for
the multi-core era. Artima, 2011. ISBN 978-0-9815316-5-6.

15:25

Deadlock-Free Typestate-Oriented Programming

[24] Carl Hewitt, Peter Bishop, and Richard Steiger. A Universal Modular ACTOR
Formalism for Artificial Intelligence. In Proceedings of the International Joint
Conference on Artificial Intelligence (IJCAI’73), pages 235–245. William Kaufmann,
1973.
[25] Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty Asynchronous
Session Types. Journal of ACM, 63(1):9, 2016. doi:10.1145/2827695.
[26] Naoki Kobayashi. A Type System for Lock-Free Processes. Information and
Computation, 177(2):122–159, 2002. doi:10.1006/inco.2002.3171.
[27] Naoki Kobayashi. Type-based information flow analysis for the pi-calculus. Acta
Informatica, 42(4-5):291–347, 2005. doi:10.1007/s00236-005-0179-x.
[28] Naoki Kobayashi. A New Type System for Deadlock-Free Processes. In Proceedings
of the 17th International Conference on Concurrency Theory (CONCUR’06), LNCS
4137, pages 233–247. Springer, 2006. doi:10.1007/11817949_16.
[29] Naoki Kobayashi and Cosimo Laneve. Deadlock analysis of unbounded process
networks. Information and Computation, 252:48–70, 2017. doi:10.1016/j.ic.2016.
03.004.
[30] Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. Fencing off
go: liveness and safety for channel-based programming. In Proceedings of the 44th
ACM SIGPLAN Symposium on Principles of Programming Languages (POPL’17),
pages 748–761. ACM, 2017. doi:10.1145/3093333.3009847.
[31] Sam Lindley and J. Garrett Morris. A semantics for propositions as sessions. In
Proceedings of the 24th European Symposium on Programming (ESOP’15), LNCS
9032, pages 560–584. Springer, 2015. doi:10.1007/978-3-662-46669-8_23.
[32] Luca Padovani. From Lock Freedom to Progress Using Session Types. In Proceedings of the 6th Workshop on Programming Language Approaches to Concurrency
and Communication-cEntric Software (PLACES’13), EPTCS 137, pages 3–19, 2013.
doi:10.4204/EPTCS.137.2.
[33] Luca Padovani. Deadlock and Lock Freedom in the Linear π-Calculus. In
Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer
Science Logic and the 29th Annual ACM/IEEE Symposium on Logic in Computer
Science (CSL-LICS’14), pages 72:1–72:10. ACM, 2014. doi:10.1145/2603088.2603116.
[34] Luca Padovani. CobaltBlue – Behavioral Type Checking for Concurrent Objects,
August 2017. URL: http://www.di.unito.it/~padovani/Software/CobaltBlue/index.
html.
[35] Luca Padovani. Type-Based Analysis of Linear Communications. In Behavioural
Types: from Theory to Tools, pages 193–217. River Publishers, 2017. doi:10.13052/rp9788793519817.
[36] Luca Padovani, Tzu-Chun Chen, and Andrea Tosatto. Type Reconstruction
Algorithms for Deadlock-Free and Lock-Free Linear π-Calculi. In Proceedings of the 17th International Conference on Coordination Models and Languages (COORDINATION’15), volume 9037 of LNCS, pages 83–98. Springer, 2015.
doi:10.1007/978-3-319-19282-6_6.

15:26

Luca Padovani

[37] Luca Padovani and Luca Novara. Types for Deadlock-Free Higher-Order Programs. In Proceedings of the IFIP International Conference on Formal Methods
and Techniques (FORTE’15), volume 9039 of LNCS, pages 3–18. Springer, 2015.
doi:10.1007/978-3-319-19195-9_1.
[38] Luca Padovani, Vasco T. Vasconcelos, and Hugo Torres Vieira. Typing Liveness
in Multiparty Communicating Systems. In Proceedings of the 16th International
Conference on Coordination Models and Languages (COORDINATION’14), LNCS
8459, pages 147–162. Springer, 2014. doi:10.1007/978-3-662-43376-8_10.
[39] Roly Perera, Julien Lange, and Simon J. Gay. Multiparty compatibility for
concurrent objects. In Proceedings of the 9th workshop on Programming Language
Approaches to Concurrency- and Communication-cEntric Software (PLACES’16),
volume EPTCS 211, pages 73–82, 2016. doi:10.4204/EPTCS.211.8.
[40] Claudio V. Russo. The Joins Concurrency Library. In Proceedings of the 9th
International Symposium on Practical Aspects of Declarative Languages (PADL’07),
LNCS 4354, pages 260–274. Springer, 2007. doi:10.1007/978-3-540-69611-7_17.
[41] Claudio V. Russo. Join patterns for visual basic. In Proceedings of the 23rd ACM
SIGPLAN Conference on Object-Oriented Programming Systems, Languages and
Applications (OOPSLA’08), pages 53–72. ACM, 2008. doi:10.1145/1449764.1449770.
[42] Joshua Sunshine, Karl Naden, Sven Stork, Jonathan Aldrich, and Éric Tanter. Firstclass state change in Plaid. In Proceedings of the 26th ACM SIGPLAN Conference on
Object-Oriented Programming Systems, Languages and Applications (OOPSLA’11),
pages 713–732. ACM, 2011. doi:10.1145/2048066.2048122.
[43] Aaron Joseph Turon and Claudio V. Russo. Scalable join patterns. In Proceedings
of the 26th ACM SIGPLAN Conference on Object-Oriented Programming Systems,
Languages and Applications (OOPSLA’11), pages 575–594. ACM, 2011. doi:10.1145/
2048066.2048111.
[44] Philip Wadler. Propositions as sessions. Journal of Functional Programming,
24(2-3):384–418, 2014. doi:10.1017/S095679681400001X.

A

Supplement to Section 4

A.1 Properties of Subtyping

We provide a semantic characterization of the derivative operator:
Lemma 1. For all t and M we have J t[M]K = {A | ∃A : 〈M0 〉 ] A ∈ J t K ∧ M ≈ M0 }.
Proof. The proof follows by an easy induction on t .
This result is useful to show that the derivative of a type with respect to a sequence
of message types is irrelevant of the order in which the single message types are
considered, modulo type equivalence.
Lemma 2. For all t , M1 and M2 we have t[M1 ][M2 ] ' t[M2 ][M1 ].

15:27

Deadlock-Free Typestate-Oriented Programming

Proof. We conclude J t[M1 ][M2 ]K = {A | ∃A : 〈M01 , M02 〉 ] A ∈ J t K ∧ M1 ≈ M01 ∧ M2 ≈ M02 } =
J t[M2 ][M1 ]K using Lemma 1.
Another useful auxiliary result which will be used in the following shows that the
derivatives of types related by subtyping are still related:
Lemma 3. If t ¶ s, then t[M] ¶ s[M].
Proof. Let 〈mi (s i )〉i∈I ∈ Js[M]K. From Lemma 1 we deduce 〈mi (s i )〉i∈J ∈ JsK for some J
such that J \ I is a singleton. From the hypothesis t ¶ s we deduce 〈mi ( t i )〉i∈J ∈ J t K
and si ¶ t i for all i ∈ J . From Lemma 1 we conclude 〈mi ( t i )〉i∈I ∈ J t[M]K.
A.2 Properties of Dependency Relations

In this section we prove the robustness of compatibility with respect to associativity
and name restriction. The first result in particular is key to be able to reason on
parallel compositions of processes without worrying about the order in which they
occur (Lemma 6).
Lemma 4. (D1 t D2 ) t D3 = D1 t (D2 t D3 ).
Proof. The result is easily proved by thinking of Di as the corresponding undirected
acyclic graph and observing that t correspond to the disjoint graph union.
Lemma 5. Let a 6∈ dom(D2 ). Then D1 and D2 are compatible if and only if D1 \ a and
D2 are compatible.
Proof. (⇒) Observe that D1 \a ⊆ D1 , hence D1 \a∩ D2 ⊆ D1 ∩ D2 = ; and (D1 \a∪ D2 )+
is acyclic if so is (D1 ∪ D2 )+ . (⇐) Using the hypothesis a 6∈ dom(D2 ) we deduce
D1 ∩ D2 = D1 \ a ∩ D2 ⊆ ;. Now, suppose by contradiction that (D1 ∪ D2 )+ has at least
one cycle, and consider one of minimal length. Such cycle must go through a, for
(D1 \ a ∪ D2 )+ is acyclic, hence there exist u and v with u 6= v such that (u, a) and (a, v)
are edges of this path. Neither of these edges can be in D2 , for a 6∈ dom(D2 ), hence
they must belong to D1 . But this contradicts the hypothesis that D1 was acyclic.
A.3 Subject Reduction

We will repeatedly use the next auxiliary result to rearrange parallel compositions of
processes in such a way that the interesting components can be grouped together.
Lemma 6. The following properties hold:
1. Γ ` P & Q • D if and only if Γ ` Q & P • D;
2. Γ ` P & (Q & R) • D if and only if Γ ` (P & Q) & R • D.
Proof. Item 1 is obvious and item 2 is easily proven using Lemma 4.
The next two results show that typing is preserved by heating and cooling rules.
Hereafter we write D1  D2 if D1 and D2 are compatible according to Definition 10.

15:28

Luca Padovani

Lemma 7. If ` D  P and D  P * D 0  P 0 , then ` D 0  P 0 .
Proof. We reason by cases on the heating rule being applied.
Then D = {ai : t i = Ci }i∈I = D 0 and P = done, P 0 and P 0 = {P j } j∈J . Let
def
Γ = {ai : t i }i∈I and P = & j∈J P j . From [t-solution] and Lemma 6 we deduce that
Γ ` done & P • D. From [t-par] we deduce that Γ = Γ1 · Γ2 and D = D1 ∪ D2 and
Γ1 ` done • D1 and Γ2 ` P • D2 and D1  D2 . From [t-done] we deduce that Γ1 = ; and
D1 = ;, therefore Γ = Γ2 and D = D2 . We conclude with one application of [t-solution].

[done]
def

Then D = {ai : t i = Ci }i∈I and P = new a : t = [C ] in P, P 00 and D 0 = D, a :
def
t = C and P 0 = P, P 00 where P 00 = {P j } j∈J and a 6∈ fn(P 00 ). Let Γ = {ai : t i }i∈I
def
and Q = & j∈J P j . From [t-solution] and Lemma 6 we deduce that Γ ` (new a : t =
[C ] in P) & Q • D for some D. From [t-par] we deduce that Γ = Γ1 ·Γ2 and D = D1 ∪ D2
and Γ1 ` new a : t = [C ] in P • D1 and Γ2 ` Q • D2 and D1  D2 . From [t-new] we
deduce that a : t ` C :: X and Γ1 , a : s ` P • D01 where t ¶ s and D1 = D01 \ a and
live(t, X). Using the hypothesis a 6∈ fn(P 00 ) we may assume, without loss of generality,
that a 6∈ dom(Γ2 ) and therefore a 6∈ dom(D2 ). From Lemma 5 we deduce that D01  D2 .
def
def
Let Γ 0 = (Γ1 , a : s) · Γ2 and D0 = D01 ∪ D2 and observe that Γ 0 = Γ , a : s. We derive
Γ 0 ` P & Q • D0 with one application of [t-par]. We conclude with one application of
[t-solution].
[new]

Then D = {ai : t i = Ci }i∈I and P = P & Q, P 00 and D 0 = D and P 0 = P, Q, P 00
where P 00 = {P j } j∈J . We conclude immediately from [t-solution] and Lemma 6.
[par]

Then D = {ai : t i = Ci }i∈I and P = a!(M1 & M2 ), P 00 and D 0 = D and P 0 =
def
def
a! M1 , a! M2 , P 00 where P 00 = {P j } j∈J . Let Γ = {ai : t i }i∈I and Q = & j∈J P j . From
[t-solution] and Lemma 6 we deduce that Γ ` a !(M1 & M2 ) & Q • D for some D.
From [t-par] we deduce that Γ = Γ1 · Γ2 and D = D1 ∪ D2 and Γ1 ` a!(M1 & M2 ) • D1
and Γ2 ` Q • D2 where D1  D2 . From [t-send] and [t-comp-m] F
we deduce that Γ1 =
a : t 1 · t 2 , Γ11 , Γ12 and Γ1i ` Mi :: t i for all 1 ≤ i ≤ 2 and D1 = u∈dom(Γ1 ) a ∼ u. Let
def F
D1i = u∈dom(Γ1i ) a ∼ u and observe that D11  D12 because dom(D1 )∩dom(D2 ) ⊆ {a}.
Furthermore D1 = D11 t D12 . We derive a : t i , Γ1i ` a! Mi • D1i for all 1 ≤ i ≤ 2 with
two applications of [t-send] and Γ ` (a! M1 & a! M2 ) & Q • D with two applications of
[t-par]. We conclude with one application of [t-solution].
[join]

Lemma 8. If ` D  P and D  P + D 0  P 0 , then ` D 0  P 0 .
Proof. We reason by cases on the cooling rule being applied.
Then D = {ai : t i = Ci }i∈I = D 0 and P 0 = done, P and P 0 = {P j } j∈J . Let
def
Γ = {ai : t i }i∈I and P = & j∈J P j . From [t-solution] and Lemma 6 we deduce that
Γ ` P • D. We derive Γ ` done & P • D using one application of [t-done] and one
application of [t-par]. We conclude with one application of [t-solution].

[done]
def

Then D = D 0 , a : t = C and P = P, P 00 and P 0 = new a : t = [C ] in P, P 00
where D 0 = {ai : t i = Ci }i∈I and P 00 = {P j } j∈J and a 6∈ fn(P 00 ). From [t-solution] and
Lemma 6 we deduce that there exist Γ , D and X such that dom(Γ ) = {a} ∪ {ai }i∈I
and t ¶ Γ (a) and t ¶ Γ (ai ) for every i ∈ I and a : t ` C :: X and Γ ` P & Q • D and
live(t, X). From [t-par] we deduce that there exist Γ1 , Γ2 , D1 and D2 such that Γ = Γ1 · Γ2
[new]

15:29

Deadlock-Free Typestate-Oriented Programming

and D = D1 ∪ D2 and Γ1 ` P • D1 and Γ2 ` Q • D2 and D1  D2 . Without loss of
generality, we may assume a 6∈ dom(Γ2 ) using the hypothesis a 6∈ dom(P 00 ). Hence
Γ1 = Γ10 , a : Γ (a). We derive Γ10 ` new a : t = [C ] in P • D1 \ a. From Lemma 5 we
deduce D1 \ a  D2 . We conclude with one application of [t-par] and one application
of [t-solution].
Then D = {ai : t i = Ci }i∈I and P = P, Q, P 00 and D 0 = D and P 0 = P & Q, P 00
where P 00 = {P j } j∈J . We conclude immediately from [t-solution] and Lemma 6.
[par]

Then D = {ai : t i = Ci }i∈I and P = a! M1 , a! M2 , P 00 and D 0 = D and P 0 =
def
def
a!(M1 & M2 ), P 00 where P 00 = {P j } j∈J . Let Γ = {ai : t i }i∈I and Q = & j∈J P j . From
[t-solution] and Lemma 6 we deduce that Γ ` (a ! M1 & a ! M2 ) & Q • D for some D.
From [t-par] we deduce that Γ = Γ1 · Γ2 and D = D1 t D2 and Γ1 ` a! M1 & a! M2 • D1
and Γ2 ` Q • D2 where D1  D2 . From [t-par] we deduce that Γ1 = Γ11 · Γ12 and
D1 = D11 t D12 and Γ1i ` a! Mi • D1i for all 1 ≤ i ≤ 2 where D11  D12 . From
[t-send] we deduce that there exist t 1 , t 2 , ∆11 and ∆12 such that Γ1i = a : t i , ∆1i and
F
∆1i ` Mi :: t i and D1i = u∈dom(∆1i ) a ∼ u for all 1 ≤ i ≤ 2. From D11  D12 we deduce
that dom(∆11 ) ∩ dom(∆12 ) = ;, for otherwise D11 ∩ D12 would not be empty, hence
Γ1 = a : t 1 · t 2 , ∆11 , ∆12 . We derive ∆11 , ∆12 ` M1 & M2 :: t 1 · t 2 with one application
of [t-comp-m]. We derive Γ1 ` a!(M1 & M2 ) • D1 with one application of [t-send]. We
conclude with one application of [t-solution].
[join]

The next Lemma relates the type environment used for typing a pattern with that
of a matching molecule. As expected, the types of the names in the environment of
the molecule are in general subtypes of those in the environment of the pattern.
Lemma 9. If Γ ` J :: A and ∆ ` σJ :: t 1 and t ↓ A and there exists t 2 such that t ¶ t 1 · t 2
and t 2 6' 0, then ∆ ¶ Γ .
Proof. From the typing rules for patterns and molecules
we deduce that Γ = {x i : t i }i∈I
Q
and A = 〈mi ( t i )〉i∈I and ∆ = {ai : si }i∈I and t 1 = i∈I mi (si ). From the hypothesis
t 2 6' 0 we deduce that there exists 〈m j (s j )〉 j∈J ∈ J t 2 K, where we may assume without
loss of generality that I ∩ J = ;. From the definition of J t 1 · t 2 K, we deduce that
〈mi (si )〉i∈I∪J ∈ J t 1 · t 2 K. From the hypothesis t ↓ A we deduce that whenever A1 ] A2 ∈
J t K and A ≈ A1 we have A = A1 . In particular, using the hypothesis t ¶ t 1 · t 2 we
deduce that 〈mi ( t i )〉i∈I∪J ∈ J t K and si ¶ t i for every i ∈ I . Then ∆ ¶ σΓ .
Because substitutions cannot merge syntactically different names, the substitution
lemma is a minor auxiliary result.
Lemma 10. If Γ ` P • D and σ is a bijection with dom(σ) = dom(Γ ), then σΓ ` σP •
σD.
Proof. A simple induction on the derivation of Γ ` P • D.
The final Lemma towards subject reduction shows that typing is preserved by
reductions.
Lemma 11. If ` D  P and D  P → D  P 0 , then ` D  P 0 .

15:30

Luca Padovani

Proof. We have D = a : t 0 = C, D 0 and J x P ∈ C and P = a!σJ, P 00 and P 0 = σP, P 00 ,
def
where D 0 = {ai : t i = Ci }i∈I and P 00 = {P j } j∈J . Let Q = & j∈J P j .
From [t-solution] and Lemma 6 we deduce that there exist s0 , Γ = {ai : si }i∈I , X and
D such that:
A a : t 0 ` C :: X
B a : s0 , Γ ` a!σJ & Q • D
C t 0 ¶ s0
Z t i ¶ si for every i ∈ I
From A, [t-class], [t-reaction] we deduce that there exist x , t , s, A, s1 , D01 such that:
D x : t ` J :: A
E x : s, a : s1 ` P • D01
F t ¶s
G t 0 ¶ t 0 [A] · s1
H t0 ↓ A
From B and [t-par] we deduce that there exist Γ1 , Γ2 , t 1 , t 2 , D1 and D2 such that:
I s0 = t 1 · t 2
J Γ = Γ1 · Γ2
D = D1 t D2
L a : t 1 , Γ1 ` a!σJ • D1
M a : t 2 , Γ 2 ` Q • D2
N D1  D2
If a 6∈ fn(Q) we can take t 2 = 1 using [t-weak]. From L and [t-send] we deduce that:
O Γ1 ` σJ :: t 1
F
P D1 = u∈dom(Γ ) a ∼ u.
1
def
Let c : r = Γ1 . Without loss of generality we may assume that σ is the bijection {x 7→ c}.
From D, G, H, I, O and Lemma 9 we deduce r ¶ t . From F and transitivity of ¶ we
def
obtain r ¶ s, therefore Γ1 ¶ Γ10 where Γ10 = c : s. From E and Lemma 10 we deduce
Q c : s, a : s1 ` σP • σD01
where dom(σD01 ) ⊆ {c, a}. From P we observe that u, v ∈ dom(D1 ) implies (u, v) ∈ D1 ,
therefore σD01 ⊆ D1 and σD01  D2 . From Q and M we derive
a : s1 · t 2 , Γ10 · Γ2 ` σP & Q • σD01 t D2 .
From D and O we deduce t 1 [A] ¶ 1. From C, I and Lemma 3 we deduce t 0 [A] ¶
(t 1 · t 2 )[A] = t 1 · t 2 [A] + t 1 [A] · t 2 ¶ t 2 . From G and the fact that ¶ is a pre-congruence
we obtain t 0 ¶ s1 · t 2 . We conclude with an application of [t-solution].
Subject reduction is a straightforward consequence of the previous results:
def

Theorem 2. Let =⇒ = (* ∪ + ∪ →)∗ . If ` ;  P and ;  P =⇒ D  P , then ` D  P .
Proof. Immediate consequence of Lemma 7, Lemma 8 and Lemma 11.

15:31

Deadlock-Free Typestate-Oriented Programming

A.4 Soundness

We begin by proving two auxiliary results concerning usable and relevant objects.
Lemma 12. If Γ , u : t ` P • D, then t is usable.
Proof. The result follows from a simple induction on the derivation of Γ , u : t ` P • D.
This proof makes key use of the side condition 0 6¶ t of rule [t-msg-m].
Lemma 13. If Γ , u : t ` P • D and t is relevant, then u ∈ fn(P).
Proof. The result follows from a simple induction on the derivation of Γ , u : t ` P •
D, noting that rule [t-done] cannot be applied (because it is only applicable on an
empty type environment) and [t-weak] cannot be used to eliminate u from the type
environment because t 6¶ 1 from the hypothesis that t is relevant.
Next are the separate proofs of conformance and deadlock freedom for processes
that are well-typed in the empty type environment.
Lemma 14. If ; ` P • D, then P is conformant.
Proof. Consider a reduction ;  P =⇒ D, a : t = C  〈a!mi (ci )〉i∈I , P where P =
def
〈P j 〉 j∈J . Let Q = & j∈J P j . From Theorem 2, [t-solution] and Lemma 4 we deduce that
there exist s, Γ , X and D such that a : t ` C :: X and a : s, Γ ` &i∈I a!mi (ci ) & Q • D
where t ¶ s. From [t-par] we deduce that there exist Γ1 , Γ2 , s1 , s2 , D1 and D2 such
that Γ = Γ1 · Γ2 and a : s1 , Γ1 ` &i∈I a!mi (ci ) • D1 and a : s2 , Γ2 ` Q • D2 and s = s1 · s2 .
From [t-par]
, [t-send] and [t-msg-m] we deduce that for every i ∈ I there exist t i such
Q
that s1 = i∈I mi ( t i ). From Lemma 12 we deduce that s2 is usable. From Lemma 3 we
deduce that t[〈mi 〉i∈I ] ¶ 1 · s2 ¶ s2 . We conclude that t[〈mi 〉i∈I ] is usable. Now suppose
that t[〈mi 〉i∈I ] is also relevant and that a does not occur in any of the ci for i ∈ I . From
transitivity of ¶ we deduce that s2 is relevant as well. From Lemma 13 we conclude
that a ∈ fn(Q).
Lemma 15. If ; ` P • D, then P is deadlock free.
Proof. We proceed by contradiction, assuming that there exists a reduction ;  P =⇒
D  P (*∪+)∗ X→ that violates the condition expressed in Definition 6. Without loss of
generality, we may assume that the solution D  P has been heated to the maximum
temperature, meaning that in P there are no done processes, no compound molecules,
no compound processes and no object definitions. In other words, we may assume that
P = 〈ai !mi (ci )〉i∈I . From Theorem 2 we know that D  P is well typed. In particular,
from [t-solution] we deduce that D = {ai : t i = Ci }i∈I and that there exist Xi such that
def
ai : t i ` Ci :: Xi and live(t i , Xi ) for all i ∈ I . Given Γ = {ai : t i }i∈I , we also deduce that
there exists D such that Γ ` &i∈I ai !mi (ci ) • D.
def
Now suppose that there exists i ∈ I such that t i [〈mk 〉k∈I,ak =ai ] 6¶ 1. We define P1 =
def
&k∈I,ak =ai ai !mi (ci ) and P2 = &k∈I,ak 6=ai ai !mi (ci ). From Lemma 6 we deduce that there
exist Γ1 , Γ2 , s1 , s2 , D1 , D2 such that Γ = ai : t i , (Γ1 · Γ2 ) and t i = s1 · s2 and D = D1 t D2
and ai : sh , Γh ` Ph • Dh for all 1 ≤ h ≤ 2. From [t-send], [t-comp-m] and [t-msg-m] we
deduce that s1 [〈mk 〉k∈I,ak =ai ] ¶ 1, therefore t i [〈mk 〉k∈I,ak =ai ] ¶ s1 [〈mk 〉k∈I,ak =ai ] · s2 ¶ s2

15:32

Luca Padovani

and s2 6¶ 1. From Lemma 13 we deduce that ai ∈ fn(P2 ). Given how P1 and P2 have
been defined, it must be the case that ai ∈ c j for some j ∈ I with ai 6= a j .
The next step is to deduce that t j [〈mk 〉k∈I,ak =a j ] 6¶ 1, and we do that by contradiction
too. If t j [〈mk 〉k∈I,ak =a j ] ¶ 1, then the multiset of messages targeted to a j is a valid
configuration A of t j . From live(t j , X j ) and the fact that the system cannot reduce any
further (in particular, no reaction of a j is able to fire), we deduce that all the arguments
of messages targeted to a j must have a type smaller than 1. This is absurd, because
we know that at least one of them contains an occurrence of ai with a type that is not
smaller than 1. In summary, starting from an object ai such that t i [〈mk 〉k∈I,ak =ai ] 6¶ 1
we have found another object a j 6= ai such that t j [〈mk 〉k∈I,ak =a j ] 6¶ 1 and furthermore
ai ∈ c j . This argument can now be iterated to build a finite set {ak !mk (ck )}k∈K ⊆ P
such that for every k ∈ K there exists ω(k) ∈ K \ {k} with ak ∈ cω(k) . This set can be
assumed to contain at least two elements. Without loss of generality, we also assume
that it is a minimal set with the aforementioned properties.
Being a subset of P , it must be the case that ∆ ` &k∈K ak !mk (ck ) • D0 for some
∆ and D0 . In addition, having K at least two elements, it must be possible to split
def
this parallel composition into two parts Q 1 and Q 2 such that Q h = &k∈Kh ak !mk (ck )
and Q h is well typed in isolation, for all 1 ≤ h ≤ 2. More precisely, from [t-par] we
deduce that there exist ∆1 , ∆2 , D01 and D02 such that ∆ = ∆1 · ∆2 and D0 = D01 t D02
and ∆h ` Q h • D0h for all 1 ≤ h ≤ 2 where D01  D02 . Now it must be the case that
there exist k1 and k2 such that kh ∈ Kh and ω(kh ) ∈ K3−h for all 1 ≤ h ≤ 2, or else we
would be able to find a smaller K with the aforementioned properties, whereas we
have chosen K to be minimal. From [t-send], we deduce that (akh , aω(kh ) ) ∈ D01 ∩ D02 ,
which contradicts D01  D02 . In conclusion, D  P satisfies the conditions expressed
in Definition 6 hence P is deadlock free.
Theorem 1. If ; ` P • D, then P is conformant and deadlock free.
Proof. Immediate consequence of Lemmas 14 and 15.

B

Supplement to Section 5

The program discussed in Section 5.4 is well typed by taking the following type
definitions:
type
and
and
and
and

#Get
#Reply
#Generator
#Filter
#Printer

=
=
=
=
=

Get(#Reply)
Reply(#Number,#Get)
FROM(#Number) · #Get
READY(#Number,#Get) · #Get + WAIT(#Number,#Get,#Reply)
RUN(#Get)

15:33

Deadlock-Free Typestate-Oriented Programming

About the author
Luca Padovani is Associate Professor at the Computer Science
Department of the University of Torino, where he leads the research group on Formal Methods for Software Development. Email:
luca.padovani@unito.it

15:34

