A Capability Calculus for Concurrency andDeterminism
TACHIO TERAUCHI
Tohoku University
and
ALEX AIKEN
Stanford University

This paper presents a static system for checking determinism (technically, partial confluence) ofcommunicating concurrent processes. Our approach automatically detects partial confluence inprograms communicating via a mix of different kinds of communication methods: rendezvous
channels, buffered channels, broadcast channels, and reference cells. Our system reduces thepartial confluence checking problem in polynomial time (in the size of the program) to the problem
of solving a system of rational linear inequalities, and is thus efficient.
Categories and Subject Descriptors: F.3.2 [Semantics of Programming Languages]: Program
analysis; D.3.3 [Language Classifications]: Concurrent programming structures
General Terms: Algorithms, Languages, Theory
Additional Key Words and Phrases: Determinism, Capabilities, Type Systems

1. INTRODUCTION
Deterministic programs are easier to debug and verify than non-deterministic programs, both for testing (or simulation) and for formal methods. However, sometimes programs are written as communicating concurrent processes, for speed or forease of programming, and therefore are possibly non-deterministic. In this paper,
we present a system that automatically proves more such programs to be deterministic than previous methods [Kahn 1974; König 2000; Edwards and Tardieu 2005],
and can encode linear type systems which can also be used to guarantee determinism [Nestmann and Steffen 1997; Kobayashi et al. 1999]. Our system is able tohandle programs communicating via a mix of different communication methods:
rendezvous channels, output buffered channels, input buffered channels (broadcast
channels), and reference cells. Section 3.2 shows a few examples that can be checkedby our system: producer consumer, token ring, and barrier synchronization.
We cast our system as a capability calculus [Crary et al. 1999]. The capability
This is a revised and extended version of a paper presented at the Concurrency Theory, [17th International] Conference, CONCUR 2006 pp.218-232, 2006. This work was supported by KAKENHI
20700019 and 2024001.
Permission to make digital/hard copy of all or part of this material without fee for personalor classroom use provided that the copies are not made or distributed for profit or commercial
advantage, the ACM copyright/server notice, the title of the publication, and its date appear, andnotice is given that copying is by permission of the ACM, Inc. To copy otherwise, to republish,
to post on servers, or to redistribute to lists requires prior specific permission and/or a fee.
c 20YY ACM 0164-0925/20YY/0500-0001 $5.00
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY, Pages 1–29.

2·

T. Terauchi and A. Aiken

calculus was originally proposed as a framework for reasoning about resources insequential computation and inspired a number of such applications [Smith et al.
2000; DeLine and Fähndrich 2001; Foster et al. 2002]. Recently, the frameworkhas been extended to reason about determinism in concurrent programs [Boyland
2003; Terauchi and Aiken 2005]. A key innovation of these systems is that they
allow concurrent imperative operations. However, these systems only reason about
synchronization at join points, and therefore cannot verify determinism of channelcommunicating processes. This paper extends the capability calculus to reason
about synchronization due to channel communications. The problem of finding aflow assignment can be reduced in polynomial time (in the size of the program)to the problem of solving a system of rational linear inequalities, for which many
efficient algorithms, such as the simplex algorithm and interior point methods,
exist. Therefore, in contrast to the more rigid, set-oriented approach taken in theoriginal capability calculus [Crary et al. 1999], not only are fractional capabilities
more flexible, but also more efficient for automatic inference.
This article is a revised and extended version of a conference paper with thesame title [Terauchi and Aiken 2006]. The main additions are a stronger notion ofdeterminism which guarantees (among other things) deterministic termination/nontermination, type inference details including a prototype implementation, the |operator, compatibility with a weak consistency memory model, and the proofs.
1.1 Utility of Concurrency and Determinism
Concurrency makes programs faster. For example, in the expression (a + b) × (c +d), a + b and c + d can be computed in parallel, thus overlapping the time tocompute one addition with the other. The importance of concurrency for speed
has increased in recent years as many predict that we will soon reach the limitsof sequential computation, if we have not already [Sutter and Larus 2005]. Also,
concurrency is convenient when program parts must be placed at distant locations,or when the application can be naturally designed as a union of concurrently runningcomponents, as often is the case in embedded systems [Edwards and Tardieu 2005].
However, concurrency is difficult to get right. For example, the assignments x := 1
and x:=2 may not occur in parallel as x could be either 1 or 2 after the assignments.
In current software practice, a predominant style of concurrency is to express
programs as sets of communicating processes. Each process runs sequentially at
its own speed (i.e., asynchronously1) and communicates with other processes via
shared resources such as channels, locks, and basic reference cells. Many popular
programming models, including message passing and shared memory programming,
are derivatives of this general model. The model is popular partly because of its
resemblance to sequential programming. Usually, few syntactic changes are needed
to extend a sequential language to this concurrent model. Also, the absence ofa global synchronizing clock makes the model ideal for situations requiring the
program parts to be placed at distant locations.
However, writing bug-free programs in this model is notoriously difficult due
to asynchronous accesses to shared resources, which introduce non-determinism.
1 We use the term in the sense of asynchronous circuits and systems, and not in the sense of

asynchronous process algebra [Honda and Tokoro 1992; Boudol 1992].
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

A Capability Calculus for Concurrency and Determinism·

3

For this reason, some advocate alternatives to this programming model [Lee 2006].
Instead, we believe that it is possible to keep this convenient model of programming
while (mostly) guaranteeing determinism, and we make a step toward this goal inthis paper.
Sometimes, notions such as race freedom and atomicity are used to reason about
possibly misbehaving concurrency. These properties can enforce, for example, that
there is no point in the program where x := 1 and x := 2 could simultaneously
execute. In contrast, determinism is an extensional property that can be statedpurely in terms of program semantics, that is, the program behaves semanticallythe same under the same conditions. Neither race freedom nor atomicity implies
determinism, nor vice versa.
Determinism is the norm in sequential programming which dominates the current
software practice. We believe most concurrent programs are also expected to behave
deterministically. This assumption appears to be reasonable not only for noninteractive applications (i.e., “batch processes”) such as scientific computing, butalso for interactive applications such as web servers because one would expect a
web server, in some state, to behave deterministically given a series of user requests(which could come from multiple users). At the least, non-determinism is not thereason for choosing concurrent over sequential computation.
Non-deterministic programs are difficult to debug because one cannot reproduce
the bug by just running the program again from the same initial state. Determinism
also helps formal methods. For example, in model checking, determinism implies
that there is no need to explore more than one (abstract) program path because
following any other paths would lead to an equivalent result [Groote and van dePol 2000; Blom and van de Pol 2002].
1.2 Utility of Non-Determinism
It seems rare for a real world application to require true non-determinism in thesense that a program’s specification requires the program to behave differently
from previous executions in an identical environment. However, harmless nondeterminism sometimes appears as an artifact of programming convenience.
While this paper makes a step toward making provable deterministic concurrency
practical, it may be difficult to completely eliminate non-determinism in reality.
Our analysis is preliminary in that it often prohibits harmless instances of nondeterminism. For example, internal actions of a program that do not affect the
program output are arguably harmless and allowed to be non-deterministic, but
our analysis demands determinism even for such actions. Our analysis does allow
some degree of non-determinism by letting the user specify the communication
channels that could be used for non-deterministic inputs and outputs. We leave as
future work understanding and accommodating a wider variety of harmless nondeterministic programming idioms.
2. A SIMPLE CONCURRENT LANGUAGE
We focus on the simple concurrent language shown in Figure 1. A program, p, isa parallel composition of finitely many processes. A process, i.s, is a sequential
statement s prefixed by a process index i. Process indices are used to connect
processes to their input buffers and stores. We drop process indices when it is
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

4·

T. Terauchi and A. Aiken
p ::= i.s
(process)s ::= s1 ; s2(sequence)| p1 || p2 (parallel composition)| if e then s1 else s2 (branch)e ::= c(channel)| while e do s(loop)| x(local variable)| skip(skip)| n(integer constant)| x := e(assignment)| e1 op e2 (integer operation)| !(e1 , e2 )(write channel)| ?(e, x)(read channel)
Fig. 1.

The syntax of the simple concurrent language.

convenient to do so. A sequential statement consists of the usual imperative features
as well as channel communication operations. Here, !(e1 , e2 ) means writing thevalue of e2 to the channel e1 , and ?(e, x) means storing the value read from thechannel e to the variable x. The variables are process-local, and so the only meansof communication are channel reads and writes. We use meta-variables x, y, z,
etc. for variables and c, d, etc. for channels.
The language cannot dynamically create channels or spawn new processes, butthese restrictions are imposed only to keep the main presentation to the novel
features of the system. Section 4.3 shows that techniques similar to previous workin the capability calculus can be used to handle dynamic channels and processes.
2.1 Channel Kinds
The literature on concurrency includes several forms of channels with distinct semantics. We introduce these channel kinds and show how they affect determinism.
If c and d are rendezvous channels, then the following program is deterministic2
because (x, y) = (1, 2) when the process terminates. This is because !(d, 2) waits
for !(c, 1) to complete, which in turn waits for the reader ?(c, x) to be available,
and this is only after the write !(d, 3) is completed, and therefore, the first write
to d is always 3 and the second write to d is always 2.
!(c, 1); !(d, 2) || !(d, 3); ?(c, x) || ?(d, y); ?(d, y)
The same program is non-deterministic if c is output buffered because !(c, 1) does
not need to wait for the reader ?(c, x), and therefore (x, y) could be (1, 2) or (1, 3).
While all the processes share one output buffer per channel, each process has its
own input buffer per channel. Therefore,!(c, 1); !(c, 2) || ?(c, x) || ?(c, y)is deterministic if c is input buffered because both read 1 from their input channel,
but not if c is output buffered or rendezvous. Input buffered channels are often
called broadcast channels, and are the basis of Kahn process networks [Kahn 1974].
We also consider a buffered channel whose buffer is overwritten by every write
but never modified by a read. Such a channel is equivalent to a reference cell. If c
is a reference cell, !(c, 1); !(c, 2) || ?(c, x) is not deterministic because !(c, 2) may
or may-not overwrite 1 in the buffer before ?(c, x) reads the buffer. The program
2 Here, we use the term informally. Determinism is formally defined in Section 2.2.

ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

A Capability Calculus for Concurrency and Determinism(S(i), e) ⇓ nn 6= 0(B, S, i.(if e then s1 else s2 ); s||p) → (B, S, i.s1 ; s||p)(S(i), e) ⇓ 0(B, S, i.(if e then s1 else s2 ); s||p) → (B, S, i.s2 ; s||p)(S(i), e) ⇓ n

IF2

n 6= 0(S(i), e) ⇓ 0(S(i), e) ⇓ e′

S ′ = S[i 7→ S(i) :: (x, e′ )](B, S, i.x := e; s||p) → (B, S ′ , i.s||p)WHILE1

WHILE2ASSIGN(S(i), e1 ) ⇓ c (S(i), e2 ) ⇓ e′2 (S(j), e3 ) ⇓ c¬buffered(c) S ′ = S[j 7→ S(j) :: (x, e′2 )](B, S, i.!(e1 , e2 ); s1 ||j.?(e3 , x); s2 ||p) → (B, S ′ , i.s1 ||j.s2 ||p)(S(i), e1 ) ⇓ c (S(i), e2 ) ⇓ e′2 buffered(c)B ′ = B.write(c, e′2 )(B, S, i.!(e1 , e2 ); s||p) → (B ′ , S, i.s||p)5

IF1(B, S, i.(while e do s1 ); s||p) → (B, S, i.s1 ; (while e do s1 ); s||p)(B, S, i.(while e do s1 ); s||p) → (B, S, i.s||p)

·

UNBUF

BUF1

(S(i), e) ⇓ c buffered(c)(B ′ , e′ ) = B.read(c, i) S ′ = S[i 7→ S(i) :: (x, e′ )](B, S, i.?(e, x); s||p) → (B ′ , S ′ , i.s||p)Fig. 2.

BUF2The operational semantics of the simple concurrent language.

is deterministic if c is any other channel kind. On the other hand,!(c, 1); !(c, 2); !(d, 3); ?(c, x) || ?(d, x); ?(c, y)is deterministic if c is a reference cell and d is rendezvous because both reads of chappen after !(c, 2) overwrites the buffer. But the program is not deterministic if
c is output buffered.
2.2 Operational Semantics
The operational semantics of the language is defined as a series of reductions fromstates to states. A state is represented by the triple (B, S, p) where B is a buffer,
S is a store.
A store is a mapping from process indices to histories of assignments where ahistory is a sequence of pairs (x, e), meaning e was assigned to x. We use metavariables h, h′ , etc. for histories. Let l :: l′ denote an append of lists l and l′ (l andl′ can be a singleton list). A lookup in a history is defined as: (h :: (x, e))(x) = e
and (h :: (y, e))(x) = h(x) if y 6= x. We use history instead of memory for the
purpose of defining determinism.
Expressions are evaluated entirely locally. The semantics of expressions are defined as: (h, c) ⇓ c, (h, x) ⇓ h(x), (h, n) ⇓ n, and (h, e1 op e2 ) ⇓ n if (h, e1 ) ⇓ n1
and (h, e2 ) ⇓ n2 and n = n1 [[op]]n2 where [[op]] is the standard semantics of the
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

6·

T. Terauchi and A. Aiken
8>
if c is output buffered>B[c 7→ enq(B(c), e)]>>< B[c 7→ henq(q , e), . . . , enq(q , e)i]n1B.write(c, e) =if c is input buffered>
where B(c) = hq1 , . . . , qn i>>>
:B[c 7→ e]
if c is a reference cell8′ ], e)
(B[c
→
7
q
>
>
if c is output buffered>>>
where B(c) = q and (q ′ , e) = deq(q)>>>< (B[c 7→ hq , . . . , q ′ , . . . , q i], e)n1iB.read(c, i) =>if c is input buffered
where
B(c)
=
hq
,
.
.
. , qi , . . . , qn i
1
>
>
>
>
′ , e) = deq(q )
>
(q
i
>
i
>
:
(B, B(c))
if c is a reference cellFig. 3.

Buffer operations.

operator op.
Figure 2 shows the reduction rules. The sequential composition operator ; isassociative. Also, we let s = s; skip = skip; s. The parallel composition operator|| is commutative and associative, e.g., p1 || p2 || p3 = p2 || p3 || p1 . Note thatthe rules only reduce the left-most processes, and so we rely on process re-ordering
to reduce other processes. We assume that the process indices are disjoint in any
program p. The rules IF1, IF2, WHILE1, and WHILE2 do not involve channel
communication and are self-explanatory. ASSIGN is also a process-local reduction
because variables are local. Here, S[i 7→ h] means {j 7→ S(j) | j 6= i ∧ j ∈dom(S)} ∪ {i 7→ h}. We use the same notation for other mappings.
UNBUF handles communication over rendezvous channels. The predicate¬buffered(c) says c is unbuffered (and therefore rendezvous). Note that the written
value e′2 is immediately transmitted to the reader. BUF1 and BUF2 handle communication over buffered channels, which include output buffered channels, input
buffered channels, and reference cells. The predicate buffered(c) says that c is abuffered channel. We write B.write(c, e′2 ) for the buffer B after e′2 is written to thechannel c, and B.read(c, i) for the pair (B ′ , e′ ) where e′ is the value process i readfrom channel c and B ′ is the buffer after the read.
Formally, a buffer B is a mapping from channels to buffer contents. If c is arendezvous channel, then B(c) = nil indicating that c is not buffered. If c is output
buffered, then B(c) = q where q is a FIFO queue of values. If c is input buffered,then B(c) = hq1 , q2 , . . . , qn i, i.e., a sequence of FIFO queues where each qi represents
the buffer content for process i. If c is a reference cell, then B(c) = e for some valuee. Let enq(q, e) be q after e is enqueued. Let deq(q) be the pair (q ′ , e) where q ′ is q
after e is dequeued. Buffer writes and reads are defined as shown in Figure 3. Notethat B.read(c, i) and B.write(c, e) are undefined if c is rendezvous.
We write P →∗ Q for 0 or more reduction steps from P to Q. We define partial
confluence and determinism.
Definition 2.1. Let Y be a set of channels. We say that P is partially confluent
with respect to Y if for any P →∗ P1 communicating only over channels in Y , andfor any P →∗ P2 , there exists a state Q such that P2 →∗ Q communicating only
over channels in Y and P1 →∗ Q.
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

A Capability Calculus for Concurrency and Determinism·

7

Definition 2.2. Let Y be a set of channels. We say that P is deterministic withrespect to Y if for each process index i, there exists a (possibly infinite) sequence
hi such that for any P →∗ (B, S, p) that communicates only over channels in Y ,(1) S(i) is a prefix of hi , and(2) if S(i) is shorter than hi , then there exists (B ′ , S ′ , p′ ) such that (B, S, p) →∗(B ′ , S ′ , p′ ) communicating only over channels in Y and S ′ (i) is longer than S(i).
Note that, because of (1), S ′ (i) is a prefix of hi in (2). Determinism implies thatfor any single process, interaction with the rest of the program is deterministic.
Condition (2) also implies that, if some processes deadlock they always deadlock.
Determinism and partial confluence are related in the following way.
Lemma 2.3. If P is partially confluent with respect to Y then P is deterministicwith respect to Y .
We leave the proof of this lemma to the appendix.
The definition of partial confluence is borrowed from [Kobayashi et al. 1999].
Because the operational semantics lacks explicit visible behavior, the definition ofdeterminism is somewhat different (if superficially) from the standard definitions
used in the literature [Hansen and Valmari 2006; Wang and Kwiatkowska 2006].
However, the definition is sufficient for programs taking inputs or interacting withan environment. An environment can be modelled by designating a process as
an “observation process” whose store contents can be observed. Behavior of anenvironment can be modelled by using operators with unknown (but deterministic)
semantics. Then, determinism implies the determinism of the transition systemmodulo the observables and stutter equivalence, that is, there is no ambiguity inthe observation (if the program does not communicate over channels in Y ).
Note that if a program taking inputs (in the form of initial configuration or interactively from the environment) is deterministic with respect to Y , then it simply
means that it has a deterministic input to output (in the form of the final resultof the program or interactively as communication to the environment) relationshipwhen communicating only over channels in Y , i.e., it does not mean that given any
input the program always appears to behave identically.
3. CALCULUS OF CAPABILITIESWe now present a capability calculus for ensuring partial confluence. While capability calculi are typically presented as a type system in the literature, we take adifferent approach and present the capability calculus as a dynamic system. We
then construct a type system to statically reason about the dynamic capability
calculus. This approach allows us to distinguish approximations due to the typeabstraction from approximations inherent in the capability concept. (We have taken
a similar approach in previous work [Terauchi and Aiken 2005].)
We informally describe the general idea. To simplify matters, we begin this initial
discussion with rendezvous channels and total confluence (i.e., confluence over all
channels). Given a program, the goal is to ensure that for each channel c, at mostone process can write c and at most one process can read c at any point in time.
To this end, we introduce capabilities r(c) and w(c) such that a process needs r(c)ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

8·

T. Terauchi and A. Aiken

to read from c and w(c) to write to c. Capabilities are distributed to the processes
at the start of the program and are not allowed be duplicated.
Recall the following confluent program from Section 2:
1.!(c, 1); !(d, 2) || 2.!(d, 3); ?(c, x) || 3.?(d, y); ?(d, y)Note that for both c and d, at most one process can read and at most one process
can write at any point in time. However, because both process 1 and process 2 write
to d, they must somehow share w(d). A novel feature of our capability calculus is
the ability to pass capabilities between processes. The idea is to let capabilities bepassed when the two processes synchronize, i.e., when the processes communicate
over a channel. In our example, we let process 2 have w(d) at the start of the
program. Then, when process 1 and process 2 communicate over c, we pass w(d)from process 2 to process 1 so that process 1 can write to d.
An important observation is that capability passing works in this example because!(d, 3) is guaranteed to occur before the communication on c because channel c isrendezvous. If c is buffered (recall that the program is not confluent in this case),
then !(c, 1) may occur before !(d, 3). Therefore, process 1 cannot obtain w(d) fromprocess 2 when c is written because process 2 may still need w(d) to write on d.
In general, for a buffered channel, while the read is guaranteed to occur after thewrite, there is no ordering dependency in the other direction, i.e., from the readto the write. Therefore, capabilities can be passed from the writer to the reader
but not vice versa, whereas capabilities can be passed in both directions whencommunicating over a rendezvous channel.
Special care is needed for reference cells. If c is a reference cell, the program
1.!(c, 1); !(c, 2)||2.?(c, x) is not deterministic although process 1 is the only writerand process 2 is the only reader. We use fractional capabilities [Boyland 2003;
Terauchi and Aiken 2005] such that a read capability is a fraction of the write capability. Capabilities can be split into multiple fractions, which allows concurrent
reads on the same reference cell, but must be re-assembled to form the write capability. Fractional capabilities can be passed between processes in the same way asother capabilities. Recall the following confluent program from Section 2 where cis a reference cell and d is rendezvous:
1.!(c, 1); !(c, 2); !(d, 3); ?(c, x) || 2.?(d, x); ?(c, y)
Process 1 must start with the capability to write c. Because both processes readfrom c after communicating over d, we split the capability for c such that one
half of the capability stays in process 1 and the other half is passed to process 2
via d. As a result, both processes obtain the capability to read from c. We haveshown previously that fractional capabilities can be derived in a principled way
from ordering dependencies [Terauchi and Aiken 2005].
We now formally present our capability calculus. Let
Capabilities = {w(c), r(c) | c is rendezvous or output buffered}∪{w(c) | c is input buffered} ∪ {w(c) | c is a reference cell}
A capability set C is a function from Capabilities to rational numbers in therange [0, 1]. If c is rendezvous, output buffered, or input buffered, C(w(c)) = 1(resp. C(r(c)) = 1) means that the capability to write (resp. read) c is in C. Read
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

A Capability Calculus for Concurrency and Determinism(S(i), e) ⇓ nn 6= 0(X, B, S, i.C.(if e then s1 else s2 ); s||p) → (X, B, S, i.C.s1 ; s||p)(S(i), e) ⇓ 0(X, B, S, i.C.(if e then s1 else s2 ); s||p) → (X, B, S, i.C.s2 ; s||p)(S(i), e) ⇓ nn 6= 0(X, B, S, i.C.(while e do s1 ); s||p)→ (X, B, S, i.C.s1 ; (while e do s1 ); s||p)(S(i), e) ⇓ 0(X, B, S, i.C.(while e do s1 ); s||p) → (X, B, S, i.C.s||p)(S(i), e) ⇓ e′

S ′ = S[i 7→ S(i) :: (x, e′ )](X, B, S, i.C.x := e; s||p) → (X, B, S ′ , i.C.s||p)Fig. 4.

·

9

IF1’

IF2’

WHILE1’

WHILE2’ASSIGN’The capability calculus: sequential reductions.

capabilities are not needed for input buffered channels because each process has its
own buffer. For reference cells, C(w(c)) = 1 means that the capability to write is inC, whereas C(w(c)) > 0 means that the capability to read is in C. To summarize,
we define the following predicates:
hasWcap(C, c) ⇔C(w(c)) = 1C(r(c)) = 1
hasRcap(C, c) ⇔ trueC(w(c)) > 0

if c is rendezvous or output buffered
if c is input buffered
if c is reference cell

To denote capability merging and splitting, we define:C1 + C2 = {cap 7→ C1 (cap) + C2 (cap) | cap ∈ Capabilities}
We define C1 − C2 = C3 if C1 = C3 + C2 . (We avoid negative capabilities.)
Figure 4 and Figure 5 show the reduction rules of the capability calculus. The
reduction rules (technically, labeled transition rules) are similar to those of the operational semantics with the following differences. Each concurrent process is prefixed
by a capability set C representing the current capabilities held by the process. The
rules in Figure 4 do not utilize capabilities and therefore are almost identical tothe operational semantics reduction rules. Note that capabilities are not passed
between processes. Figure 5 shows how capabilities are utilized at communication
points. UNBUF′ sends capabilities C from the writer process to the reader process
and sends capabilities C ′ from the reader process to the writer process. UNBUF′
checks whether the right capabilities are present by hasWcap(Ci , c)∧hasRcap(Cj , c).
The boolean value ℓ records whether the check succeeds. Because we are interested
in partial confluence with respect to some set Y of channels, we only check thecapabilities if c ∈ Y .
BUF1′ and BUF2′ handle buffered communication. Recall that the writer canpass capabilities to the reader. BUF1′ takes capabilities C ′ from the writer process
and stores them in X. BUF2′ takes capabilities C ′ from X and gives them to thereader process. The mapping X from channels to capability sets maintains the
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

10·

T. Terauchi and A. Aiken(S(i), e1 ) ⇓ c (S(i), e2 ) ⇓ e′2 (S(j), e3 ) ⇓ c¬buffered(c) S ′ = S[j 7→ S(j) :: (x, e′2 )]ℓ = (c ∈ Y ⇒ (hasWcap(Ci , c) ∧ hasRcap(Cj , c)))(X, B, S, i.Ci .!(e1 , e2 ); s1 ||j.Cj ?(e3 , x); s2 ||p)UNBUF’ℓ→ (X, B, S ′ , i.(Ci − C + C ′ ).s1 ||j.(Cj + C − C ′ ).s2 ||p)(S(i), e1 ) ⇓ c (S(i), e2 ) ⇓ e′2 buffered(c)S B ′ = B.write(c, e′2 )ℓ = (c ∈ Y ⇒ hasWcap(C, c)) C ′ = 0 if c is a reference cell
ℓ

BUF1’

(X, B, S, i.C.!(e1 , e2 ); s||p) → (X[c 7→ X(c) + C ′ ], B ′ , S, i.(C − C ′ ).s||p)(S(i), e) ⇓ c buffered(c)(B ′ , e′ ) = B.read(c, i) S ′ = S[i 7→ S(i) :: (x, e′ )]ℓ = (c ∈ Y ⇒ ¬hasRcap(C, c)) C ′ = 0 if c is a reference cell
ℓ

BUF2’

(X, B, S, i.C.?(e, x); s||p) → (X[c 7→ X(c) − C ′ ], B ′ , S ′ , i.(C + C ′ ).s||p)Fig. 5.

The capability calculus: communication reductions.

capabilities stored in each channel. Due to difficulty in reasoning statically andcompatibility with realistic memory models, our system does not allow passing
capabilities through reference cells (see Section 4.2 for the details).
We now formally state when our capability calculus guarantees partial confluence.
Let erase(X, B, S, i1 .C1 .s1 || . . . ||in .Cn .sn ) = (B, S, i1 .s1 || . . . ||in .sn ), i.e., erase()erases all capability information from the state. We use meta-variables P , Q, R,
etc. for states in the operational semantics and underlined meta-variables P , Q, R,
etc. for states in the capability calculus.
A well-formed state is a state in the capability calculus that does not carry
duplicated capabilities. More formally,
Pn
PDefinition 3.1. Let P = (X, B, S, i1 .C1 .s1 || . . . ||in .Cn .sn ). Let C = i=1 Ci +c∈dom(X) X(c). We say P is well-formed if for all cap ∈ dom(C), C(cap) = 1.
We define capability-respecting states. Informally, P is capability respecting withrespect to a set of channels Y if for any sequence of reductions from erase(P ),there exists a strategy to pass capabilities between the processes such that every
communication over the channels in Y occurs under the appropriate capabilities.
More formally,

Definition 3.2. Let Y be a set of channels and M be a set of states in thecapability calculus. M is said to be capability-respecting with respect to Y if for
any P ∈ M ,—P is well-formed, and—for any state Q such that erase(P ) → Q, there exists Q ∈ M such that,ℓerase(Q) = Q, P → Q, and if ℓ is not empty then ℓ = true.
We now state the main claim of this section.
Theorem 3.3. Let P be a state. Suppose there exists M such that M iscapability-respecting with respect to Y and there exists P ∈ M such that erase(P ) =ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

A Capability Calculus for Concurrency and Determinism·

11

P . Then P is partially confluent with respect to Y .
The theorem is a straightforward application of the following lemma.
Lemma 3.4. Let P be a state. Suppose there exists M such that M is capabilityrespecting with respect to Y and there exists P ∈ M such that erase(P ) = P .
Suppose P → P1 communicating only over channels in Y and P → P2 . Theneither P1 = P2 or there exists Q such that P2 → Q communicating only overchannels in Y and P1 → Q.
We leave the proof of this lemma to the appendix. We now prove Theorem 3.3.
Proof. Note that for any P ∈ M , if erase(P ) →∗ Q then there exists Q ∈ Msuch that erase(Q) = Q. Therefore, the proof is a standard proof by induction
using Lemma 3.4.
3.1 Static Checking of Capabilities
Theorem 3.3 tells us that to ensure that P is partially confluent, it is sufficient
to find a capability-respecting set containing some P such that erase(P ) = P . 3
Ideally, we would like to use the largest capability-respecting set, but such a set is
not recursive (because it is reducible from the halting problem). Instead, we use atype system to compute a safe approximation of the set.
We define four kinds of channel types, one for each channel kind.
τ ::= ch(ρ, τ, Ψ1 , Ψ2 )(rendezvous)| ch(ρ, τ, Ψ)(output buffered)| ch(ρ, τ, hΨ1 , . . . , Ψn i) (input buffered)| ch(ρ, τ )(reference cell)| int(integers)
Meta-variables ρ, ρ′ , etc. are channel handles. Let Handles be the set of channel
handles. Let StaticCapabilities = {w(ρ), r(ρ) | ρ ∈ Handles}. Meta-variables
Ψ, Ψ′ , etc. are mappings from some subset of StaticCapabilities to [0, 1]. We callsuch a mapping a static capability set. If cap ∈/ dom(Ψ), then we let Ψ(cap) = 0
for all cap ∈ StaticCapabilities. The rendezvous channel type can be read as
follows: the channel communicates values of type τ , any writer of the channel
sends capabilities Ψ1 , and any reader of the channel sends capabilities Ψ2 . For an
output buffered channel, because readers cannot send capabilities, only one static
capability set, Ψ, is present in its type. For an input buffered channel, the sequencehΨ1 , . . . , Ψn i lists capabilities such that each process i gets Ψi from a read. Recall
that our capability calculus does not allow passing of capabilities via reference cells.
Therefore, a reference cell type does not carry any static capability set.
Addition and subtraction of static capabilities is analogous to those of (actual)capabilities:
Ψ1 + Ψ2 = {cap 7→ Ψ1 (cap) + Ψ2 (cap) | cap ∈ dom Ψ1 ∪ dom Ψ2 }
Ψ1 − Ψ2 = Ψ3 if Ψ1 = Ψ3 + Ψ2
3 It is not a necessary condition, however. For example, !(c, 1)||!(c, 1)||?(c, x)||?(c, x) is confluent
but does not satisfy the condition.

ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

12·

T. Terauchi and A. Aiken

We say Ψ1 ≥ Ψ2 if there exists Ψ3 such that Ψ1 = Ψ2 + Ψ3 .
For channel type τ , hdl(τ ) is the handle of the channel, and valtype(τ ) is the typeof the communicated value. That is, hdl(ch(ρ, . . .)) = ρ and valtype(ch(ρ, τ, . . .)) =τ . Also, writeSend(τ ) (resp. readSend(τ )) is the set of capabilities sent by a writer(resp. reader) of the channel. More formally,
writeSend(ch(ρ, τ, Ψ1 , Ψ2 )) = Ψ1
writeSend(ch(ρ, τ, Ψ)) = ΨPwriteSend(ch(ρ, τ, hΨ1 , . . . , Ψn i)) = ni=1 ΨiwriteSend(ch(ρ,(τ )) = 0
Ψ2 if τ = ch(ρ, τ ′ , Ψ1 , Ψ2 )readSend(τ ) =0otherwise(0 is equivalent to the constant zero function λx.0, i.e., 0 (cap) = 0 for allcap ∈ Capabilities.) Similarly, writeRecv(τ ) (resp. readRecv(τ, i)) is the set ofcapabilities received by the writer (resp. the reader process i):writeRecv(τ ) = readSend(τ)(ΨireadRecv(τ, i) =writeSend(τ )if τ = ch(ρ, τ, hΨ1 , . . . , Ψn i)otherwise

Note that the writer of the input buffered channel ch(ρ, τ, hΨ1 , . . . , Ψn i)Pmust beable to send the sum of all capabilities to be received by each process (i.e., ni=1 Ψi ),whereas the reader receives only its own share (i.e., Ψi ).
For channel type τ , hasWcap(Ψ, τ ) and hasRcap(Ψ, τ ) are the static analog of
hasWcap(C, c) and hasRcap(C, c). More formally,
hasWcap(Ψ, τ ) ⇔Ψ(w(hdl(τ ))) = 1
Ψ(r(hdl(τ ))) = 1

hasRcap(Ψ, τ ) ⇔ trueΨ(w(hdl(τ ))) > 0

if τ is rendezvous or output bufferedif τ is input bufferedif τ is reference cell

A type environment Γ is a mapping from channels and variables to types suchthat for each channel c and d,—the channel type kind of Γ(c) coincides with the channel kind of c, and—if c 6= d then hdl(Γ(c)) 6= hdl(Γ(d)), i.e., each handle ρ uniquely identifies achannel. (Section 4.3 discusses a way to relax this restriction.)
We sometimes write Γ[c] to mean hdl(Γ(c)). Expressions are type-checked as follows:Γ ⊢ c : Γ(c)Γ ⊢ x : Γ(x)

Γ ⊢ n : intΓ ⊢ e1 : int Γ ⊢ e2 : intΓ ⊢ e1 op e2 : int

Figure 6 shows the type checking rules for statements. The judgements are of theform Γ, i, Ψ ⊢ s : Ψ′ where i is the index of the process that s appears in, Ψ thecapabilities before s, and Ψ′ the capabilities after s. SEQ, IF, WHILE, SKIP,
and ASSIGN are self-explanatory. WRITE handles channel writes and READ
handles channel reads. Here, confch(τ, Γ) is defined as:confch(τ, Γ) ⇔ ∃c.(Γ[c] = hdl(τ ) ∧ c ∈ Y )ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

A Capability Calculus for Concurrency and Determinism·

13

Γ, i, Ψ ⊢ s1 : Ψ1 Γ, i, Ψ1 ⊢ s2 : Ψ2
SEQΓ, i, Ψ ⊢ s1 ; s2 : Ψ2Γ ⊢ e : int

Γ, i, Ψ ⊢ s1 : Ψ1 Γ, i, Ψ ⊢ s2 : Ψ2 Ψ1 ≥ Ψ3
Γ, i, Ψ ⊢ if e then s1 else s2 : Ψ3

Γ ⊢ e : int

Γ, i, Ψ1 ⊢ s : Ψ2 Ψ2 ≥ Ψ1
Γ, i, Ψ ⊢ while e do s : Ψ1

Γ, i, Ψ ⊢ skip : ΨΓ ⊢ e1 : τSKIPΓ ⊢ e2 : valtype(τ )Ψ ≥ Ψ1Ψ2 ≥ Ψ3WHILEΓ ⊢ e : Γ(x)ASSIGNΓ, i, Ψ ⊢ x := e : Ψ

confch(τ, Γ) ⇒ hasWcap(Ψ, τ )Γ, i, Ψ ⊢ !(e1 , e2 ) : Ψ − writeSend(τ ) + writeRecv(τ )Γ⊢e:τΓ(x) = valtype(τ )confch(τ, Γ) ⇒ hasRcap(Ψ, τ )Γ, i, Ψ ⊢ ?(e, x) : Ψ − readSend(τ ) + readRecv(τ, i)Fig. 6.

IF

WRITE

READ

Type checking rules.

We write Γ ⊢ B(c) if the buffer B(c) is well-typed, i.e., Γ ⊢ e : valtype(Γ(c)) for
each value e stored in the buffer B(c). We write Γ ⊢ h if the history h is well-typed,i.e, Γ ⊢ h(x) : Γ(x) for each x ∈ dom(h). We write Γ ⊢ C : Ψ if Ψ represents C,
i.e., for each w(c) ∈ dom(C), Ψ(w(Γ[c])) = C(w(c)) and for each r(c) ∈ dom(C),Ψ(r(Γ[c])) = C(r(c)).
An environment for P consists of a type environment Γ for typing the channels
and variables, the starting static capability Ψi for each process i, and the mapping
W from handles to static capabilities representing X. Because variables are process
local, without the loss of generality, we assume that each process uses a disjoint setof variables.
Definition 3.5. Let P = (X, B, S, i1 .C1 .s1 || . . . ||in .Cn .sn ). We write (Γ, Ψ1 , . . . , Ψn , W )Pif
(1) For each c, Γ ⊢ B(c).
(2) For each i, Γ ⊢ S(i), Γ ⊢ Ci : Ψi , and Γ, i, Ψi ⊢ si : Ψ′i for some Ψ′i .
(3) For each c, Γ ⊢ X(c) : W (Γ[c]), i.e., W is a static representation of X.
Pn
P(4) Let Ψtotal = i=1 Ψi + ρ∈dom(W ) W (ρ). Then for each cap ∈ dom(Ψtotal ),Ψtotal (cap) = 1, i.e., there are no duplicated capabilities.

(5) For all output buffered channels c, W
= |B(c)| × writeSend(Γ(c)). For allP(Γ[c])
ninput buffered channels c, W (Γ[c]) = i=1 |B(c).i| × readRecv(Γ(c), i).

In the last condition, |B(c)| denotes the length of the queue B(c), and |B(c).i|
denotes the length of the queue for process i (for input buffered channels). The
condition ensures that there are enough capabilities in X for buffered reads. We
now state the main claim of this section.
Theorem 3.6. Let M = {P | ∃Env .Env ⊢ P }. Then M is capability-respectingwith respect to Y .
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

14·

T. Terauchi and A. Aiken

We leave the proof of this theorem to the appendix. The theorem is a kind of aprogress theorem, that is, reducing a well-typed state (i.e., a state in M ) results
in a well-typed state. In addition, we need to show that the reduction happens
under the appropriate capabilities to show that the state is capability-respecting.
Theorem 3.6 together with Theorem 3.3 implies that to check if P is confluent, it
suffices to find a well-typed P such that P = erase(P ). More formally,
Corollary 3.7. P is partially-confluent and deterministic with respect to Y if
there exists P and Env such that P = erase(P ) and Env ⊢ P .
Note that while the theorem implies that the static capability calculus is sound forthe dynamic capability calculus, it is not complete. An instance of incompletenessis flow-insensitivity of capability-passing discussed in Section 3.2. In general, theproblem whether P is (dynamically) capability respecting with respect to Y is
undecidable and so any decidable static system is necessarily incomplete.
3.2 Examples
Producer-Consumer:. Let c be an output buffered channel. The following programis a simple but common communication pattern of sender and receiver processes
being fixed for each channel; no capabilities need to be passed between processes.
1.while 1 do !(c, 1) || 2.while 1 do ?(c, x)
The type system can prove confluence by assigning the starting capabilities
0 [w(ρ) 7→ 1] to process 1 and 0 [r(ρ) 7→ 1] to process 2 where c : ch(ρ, int, 0 ).
Token Ring:. Let c1 , c2 , c3 be rendezvous and d be output buffered. The program
below models a token ring where processes 1, 2, and 3 take turns writing to d:
1.while 1 do (?(c3 , x); !(d, 1); !(c1 , 0))|| 2.while 1 do (?(c1 , x); !(d, 2); !(c2 , 0))|| 3.!(c3 , 0); while 1 do (?(c2 , x); !(d, 3); !(c3 , 0))|| 4.while 1 do ?(d, y)Recall that variables x and y are process local. The type system can prove
confluence by assigning the channel d the type ch(ρd , int, 0 ) and each ci thetype ch(ρci , int, 0 [w(ρd ) 7→ 1], 0 ), which says that a write to ci sends w(d) to thereader. The starting capabilities are 0 [r(ρc3 ) 7→ 1, w(ρc1 ) 7→ 1] for process 1,
0 [r(ρc1 ) 7→ 1, w(ρc2 ) 7→ 1] for process 2, 0 [r(ρc2 ) 7→ 1, w(ρc3 ) 7→ 1, w(ρd ) 7→ 1] forprocess 3, and 0 [r(ρd ) 7→ 1] for process 4.
Barrier Synchronization:. Let c1 , c2 , c3 be reference cells. Let d1 , d2 , d3 , d′1 , d′2 ,′d3 be input buffered channels. Consider the following program:
1.while 1 do (!(c1 , e1 ); !(d1 , 0); BR; ?(c1 , y); ?(c2 , z); ?(c3 , w); !(d′1 , 0); BR′ )|| 2.while 1 do (!(c2 , e2 ); !(d2 , 0); BR; ?(c1 , y); ?(c2 , z); ?(c3 , w); !(d′2 , 0); BR′ )|| 3.while 1 do (!(c3 , e3 ); !(d3 , 0); BR; ?(c1 , y); ?(c2 , z); ?(c3 , w); !(d′3 , 0); BR′ )Here, BR = ?(d1 , x); ?(d2 , x); ?(d3 , x) and BR′ = ?(d′1 , x); ?(d′2 , x); ?(d′3 , x). The
program is an example of barrier-style synchronization. Process 1 writes to c1 ,process 2 writes to c2 , process 3 writes to c3 , and then the three processes synchronize via a barrier so that none of the processes can proceed until all are done with
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

A Capability Calculus for Concurrency and Determinism·

15

their writes. Note that !(di , 0); BR models the barrier for each process i. Afterthe barrier synchronization, each process reads from all three reference cells before
synchronizing themselves via another barrier, this time modelled by !(d′i , 0); BR′ ,before the next iteration of the loop.
The type system can prove confluence by assigning the following types (assume
e1 , e2 , and e3 are of type int): c1 : ch(ρc1 , int), c2 : ch(ρc2 , int), c3 : ch(ρc3 , int), andfor each i ∈ {1, 2, 3},
di : ch(ρdi , int, h0 [w(ρci ) 7→ 31 ], 0 [w(ρci ) 7→ 13 ], 0 [w(ρci ) 7→ 31 ]i)d′i : ch(ρd′i , int, h0 [w(ρc1 ) 7→ 13 ], 0 [w(ρc2 ) 7→ 31 ], 0 [w(ρc3 ) 7→ 13 ]i)
The initial static capability set for each process i is 0 [w(ρci ) 7→ 1, w(ρdi ) 7→
1, w(ρd′i ) 7→ 1]. Note that fractional capabilities are passed at barrier synchronization points to enable reads and writes on c1 , c2 , and c3 .
Type inference fails if the program is changed so that d1 , d2 , d3 are also used forthe second barrier (in place of d′1 , d′2 , d′3 ) because while the first write to di must
send the capability to read ci , the second write to di must send to each process
j the capability to access cj , and there is no single type for di to express thisbehavior. This demonstrates the flow-insensitivity limitation of our type system,
i.e., a channel must send and receive the same capabilities every time it is used.
The modified program is still (dynamically) capability respecting because there isno such limitation to the dynamic capability system.
However, if synchronization points are syntactically identifiable (as in this example) then the program is easily modified so that flow-insensitivity becomes sufficientby using distinct channels at each syntactic synchronization point.4 In our example,
the first barrier in each process matches the other, and the second barrier in eachprocess matches the other. Synchronizations that are not syntactically identifiable
are often considered as a sign of potential bugs [Aiken and Gay 1998]. Note thatreference cells c1 and c2 are not used for synchronization and therefore need nosyntactic restriction.
4. DISCUSSION
4.1 Type Inference
The problem of finding P and Env such that P = erase(P ) and Env ⊢ P can betranslated to the problem of solving a system of rational linear inequalities. The
translation is divided into two phases. In the first phase, we look for a valid typederivation while ignoring static capabilities. More formally, we look for P ′ andEnv′ such that P = erase(P ′ ) and Env′ ⊢ P ′ by assuming ∀Ψ, τ.hasWcap(Ψ, τ ) =hasRcap(Ψ, τ ) = true. This is a simple type inference problem that can be solved,
for example, by a standard union-find based approach. (Note that it suffices tolet each Ψ = 0 and each C = 0 .) That is, we instantiate types appearing during
the type derivation by type variables α’s, and try to find a satisfying assignmentthat satisfies the set of constraints of the form α = ch(ρ, σ, . . .) and α = int where
the type language σ is defined as σ ::= α | int | ch(ρ, σ, . . .). If the constraints
4 This can be done without changing the implementation. See named barriers in [Aiken and Gay

1998].
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

16·

T. Terauchi and A. Aiken

cannot be satisfied at this phase, it indicates that P fails to satisfy a basic typesafety property (e.g., trying to use an integer typed value as a channel) or contains
channel handle aliases (see Section 4.3 for extensions to resolve this issue).
In the second phase, we use the channel handles computed in the first phase
to complete the typing. More formally, we look for P and Env such thatP = erase(P ), Env ⊢ P , and ∀c.Γ[c] = Γ′ [c] where Env = (Γ, Ψ1 , . . . , Ψn , W ) andEnv’ = (Γ′ , Ψ′1 , . . . , Ψ′n , W ′ ). Because every hdl(τ ) appearing in the type derivation
is known, the problem can be solvedbya satisfying assignments (for Ψ’s)P
Pfinding
for the constraints of the formΨ≥Ψ′ , Ψ(ρ) = 1, and Ψ(ρ) > 0. (The latter
two forms are induced by hasWcap(Ψ, τ ) and hasRcap(Ψ, τ ).) Let ρ1 , . . . , ρn be thechannel handles appearing in Γ′ . We represent each Ψ as a mapping from ρ1 , . . . , ρn
to n fresh rational
P numberP ′variables q1 , . . . qn such that Ψ(ρi ) = qi . Then, a capability
constraintΨ≥ΨP
can be represented by n rational inequality constraintsPP ′P
qn′ . Similarly, Ψ(ρ) = 1 becomes a constraint of theq1 ≥q1 , . . . , qn ≥form q = 1 where Ψ(ρ) = q, and Ψ(ρ) > 0 becomes a constraint of the form q > 0
where Ψ(ρ) = q. Because the range of a static capability is [0, 1], we also assert
1 ≥ q ≥ 0 for each q. These rational inequality constraints can be generated intime polynomial in the size of P (in contrast to the number of states of P , which
is often exponential or worse in the size of P for software programs), which canthen be solved efficiently by linear programming algorithms, such as the simplex
algorithm and interior point methods. Note the importance of being able to use
rational numbers not just for reference cells but for all channel kinds, which allows
us to reduce the problem into a system of rational linear inequalities instead of, say,a harder problem like integer programming. In fact, it is possible to show that thetype inference problem is NP-hard if we restrict capabilities to just integers insteadof rationals [Kobayashi 2007].
Theorem 4.1. Suppose the type system is altered such that for any capability
set Ψ appearing in the type derivation, Ψ(ρ) ∈ {0, 1} for all ρ. Then the set{P | ∃.Env , P .Env ⊢ P ∧ P = erase(P )} is NP-hard.
This two phased approach is similar to the type inference algorithm in our previous work [Terauchi and Aiken 2005], only simpler thanks to the absence of multiplication (which can actually be eliminated in quadratic time due to the structureof the constraints generated and thus is not a significant problem).
Megacz has implemented a prototype of the type inference algorithm [Megacz
2006] for the purpose of verifying determinism of FLEET programs. FLEET isan experimental computer architecture with a high degree of asynchronous concurrency [Coates et al. 2001]. The prototype implementation was also able to checkall of the examples used in the paper.
4.2 Memory Model Issues
Both the operational semantics (Section 2.2) and the dynamic capability calculus(Section 3) use the strict consistency memory model where every operation on thebuffer is serialized. While we do not give a formal proof, our system works evenwith a weak consistency memory model for reference cells. Weak consistency allows
non-synchronizing operations to be unserialized, and therefore is often consideredmore efficient than strict consistency for distributed computer architectures. Our
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

A Capability Calculus for Concurrency and Determinism·

17

system does not consider a reference cell access to be a synchronizing operation(and thus does not allow capability passing via reference cells). And therefore, oursystem does not require strict consistency for reference cells. Here is the intuitive
justification: the only issue is when one process, say i, writes to a reference cellwhile another process, say j, tries to read from it. But then the process i must havecapability = 1 for the reference cell, and so the the process j cannot read it because
it does not have the read capability. Therefore, the fact that capabilities can only
be passed via synchronizing communication is enough to guarantee soundness even
if reference cells are only weakly consistent.
As in the standard implementation of a weak consistency memory model, reference writes can be carried out locally such that changes are not necessarily broadcast before the next synchronization operation. In fact, the inferred capability setsfrom the type system give a conservative approximation of which writes must be
broadcast by the time next synchronizing operation happens. Such information
may prove useful to reducing the communication cost in weak consistency memory
model implementations.
Note that our system is of course sound even with a strict memory model that
could synchronize all reference cell operations. Indeed, the conference paper [Terauchi and Aiken 2006] uses such a dynamic system.
4.3 Extensions
We discuss extensions to our system which include coping with aliasing, encoding
linear types, and handling dynamic channel and process creation.
Regions. Aliasing becomes an issue when channels are used as values, e.g., as ina π-calculus program (indeed, π-calculus is so minimalistic that it requires channel
passing to express even the most basic programming idioms such as reference cells
and integers), though fortunately, this seems rare in applications such as FLEET
programs [Coates et al. 2001] and embedded systems [Edwards and Tardieu 2005].
For example, our type system does not allow two different channels c and d to
be passed to the same channel because two different channels cannot be given thesame handle. One way to resolve aliasing is to use regions so that each ρ represents
a set of channels. Then, we may give both c and d the same type ch(ρ, . . .) at
the cost of sharing w(ρ) (and r(ρ)) for all the channels in the region ρ. There
are two approaches to regions. One is to use a conservative may-alias analysis toautomatically infer regions. Another approach is to let the programmer explicitly
manage regions. The former may be more convenient, but the latter may give more
control to the programmer when combined with expressive quantified and recursive
types [Crary et al. 1999; Walker and Morrisett 2000]
Existential Abstraction and Linear Types. Another way to resolve aliasing is toexistentially abstract capabilities as ∃ρ.τ ⊗ Ψ. Existentially packing a capability set
results in subtracting the capabilities from the capabilities of the process packing
them. The capabilities are recovered by opening the existential package, i.e., thepacked capabilities are added to the capabilities of the process that opens them.
Existential types are equivalent up to renaming of bound channel handles,
i.e., ∃ρ.τ ⊗ Ψ = ∃ρ′ .τ [ρ′ /ρ] ⊗ Ψ[ρ′ /ρ] when ρ′ ∈/ freehandles(∃ρ.τ ⊗ Ψ) where
freehandles(τ ) is the set of free channel handles of τ . Following our previous
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

18·

T. Terauchi and A. Aiken

work [Terauchi and Aiken 2005], any type containing a capability set must be
handled carefully to prevent the duplication of capabilities. Therefore, we extend
the addition relation we used for capabilities to types as shown below.
∃ρ.τ1 ⊗ Ψ1 + ∃ρ.τ2 ⊗ Ψ2 = ∃ρ.(τ1 + τ2 ) ⊗ (Ψ1 + Ψ2 )
τ = int
τ +τ =ττ = ch(ρ, τ ′ , Ψ1 , Ψ2 )
τ +τ =ττ = ch(ρ, τ ′ , Ψ)
τ +τ =ττ + τ′ = τch(ρ, τ ) + ch(ρ, τ ′ ) = ch(ρ, τ )τ + τ′ = τch(ρ, τ, hΨ1 , . . . , Ψn i) + ch(ρ, τ ′ , hΨ1 , . . . , Ψn i) = ch(ρ, τ, hΨ1 , . . . , Ψn i)
τ1 + τ2 is undefined otherwise.
We can encode a linearly typed channel [Nestmann and Steffen 1997; Kobayashiˆ ) = ∃ρ.ch(ρ, τ, 0 , 0 ) ⊗ 0 [w(ρ) 7→ 1, r(ρ) 7→ 1] (for renet al. 1999] as: ch(τdezvous channels). Note that the type encapsulates both the channel and thecapability to access the channel. This reduces the aliasing problem because
all linear (rendezvous) channels communicating a value of the type τ can beˆ ). If necessary, we can split the type into the reader
given that same type ch(τˆˆ ) =type ?ch(τ ) = ∃ρ.ch(ρ, τ, 0 , 0 ) ⊗ 0 [r(ρ) 7→ 1] and the writer type !ch(τ∃ρ.ch(ρ, τ, 0 , 0 ) ⊗ 0 [w(ρ) 7→ 1]. Note that the reader type and the writer typeˆ ) = ?ch(τˆ ) + !ch(τˆ ). Furthermore, thisadd up to the linear channel type, i.e., ch(τencoding allows transitions to and from linearly typed channels to the capabilities
world, e.g., it is possible to use a linearly-typed channel multiple times. An analogous approach has been applied to express updatable recursive data structures in
the capability calculus [Walker and Morrisett 2000].
Dynamically Created Channels. Dynamically created channels can be handledin much the same way heap allocated objects are handled in the capability calculus [Crary et al. 1999] (we only show the rule for the case where c is rendezvous).
We borrow the syntax from π-calculus: νc.s creates a new channel named c, andthen executes s.
ρ∈/ freehandles(Ψ) ∪ freehandles(Ψ′ ) ∪ freehandles(Γ)Γ, c : ch(ρ, τ, Ψ1 , Ψ2 ), i, Ψ + 0 [w(ρ) 7→ 1][r(ρ) 7→ 1] ⊢ s : Ψ′Γ, i, Ψ ⊢ νc.s : Ψ′S
where freehandles(Γ) = τ ∈ran(Γ) freehandles(τ ). Existential abstraction allows
dynamically created channels to leave their lexical scope. An alternative approachis to place the newly created channel in an existing region. In this case, we canremove the hypothesis ρ ∈/ freehandles(Ψ) ∪ freehandles(Ψ′ ) ∪ freehandles(Γ) but wealso must remove the capabilities 0 [w(ρ) 7→ 1][r(ρ) 7→ 1].
Dynamically Spawned Processes. Dynamic spawning of processes can be typed
as follows. (For simplicity, we assume that the local store of the parent process is
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

A Capability Calculus for Concurrency and Determinism·

19

copied for the spawned process.)
Γ, m, Ψ2 ⊢ s : Ψ′ m ∈/ {1, . . . , n}Γ, i, Ψ1 + Ψ2 ⊢ spawn(s) : Ψ1
where n is the number of static (i.e., not dynamically spawned) processes. We
update readRecv(τ, i) as follows.

if τ = ch(ρ, τ, hΨ1 , . . . , Ψn i)ΨireadRecv(τ, i) = 0
if τ = ch(ρ, τ, hΨ1 , . . . , Ψn i) ∧ i ∈/ {1, . . . , n}writeSend(τ ) otherwise

Note that the premise m ∈/ {1, . . . , n} in the type rule is sufficient because
readRecv(τ, i) = 0 for any i ∈/ {1, . . . , n}.
Note that the spawned process may take capabilities from the parent process.
We can also express the classical | operator which combines process spawningand process joining such that s; (s1 |s2 ); s′ means do s, then do s1 and s2 in parallel,then do s′ .
Γ, m, Ψ1 ⊢ s1 : Ψ′1 Γ, i, Ψ2 ⊢ s2 : Ψ′2 m ∈/ {1, . . . , n}′′Γ, i, Ψ1 + Ψ2 ⊢ s1 |s2 : Ψ1 + Ψ2
Again, we assume that the local store of the parent process is copied for the spawned
processes.
With dynamic channel creation, it is possible to model | with spawn() and sequential composition.
s1 |s2 = νc.spawn(s1 ; !(c, 0)); s2 ; ?(c, x)
where x is a variable that does not appear anywhere else in the program. Notethat the type derivation with this encoding matches the type rule for |. (Below,
Γ′ = Γ, c : ch(ρ, int, Ψ′1 , 0 )).
Γ′ , i, Ψ1 + Ψ2 + 0 [w(ρ) 7→ 1][r(ρ) 7→ 1] ⊢ spawn(s1 ; !(c, 0)) : Ψ2 + 0 [r(ρ) 7→ 1]
Γ′ , i, Ψ2 + 0 [r(ρ) 7→ 1] ⊢ s2 ; ?(c, x) : Ψ′1 + Ψ′2 m ∈/ {1, . . . , n}
Γ′ , i, Ψ1 + Ψ2 ⊢ spawn(s1 ; !(c, 0)); s2 ; ?(c, x) : Ψ′1 + Ψ′2
Γ, i, Ψ1 + Ψ2 ⊢ νc.spawn(s1 ; !(c, 0)); s2 ; ?(c, x) : Ψ′1 + Ψ′2
where Γ, m, Ψ1 ⊢ s1 : Ψ′1 for m ∈/ {1, . . . , n} and Γ, i, Ψ2 ⊢ s2 : Ψ′2 .
4.4 Limitations
We discuss some limitations of our work. As mentioned in Section 4.1, the dynamic
capability calculus is undecidable5 , and so any sound static approximation for the
dynamic capability calculus would be incomplete.
One source of incompleteness is the flow-insensitivity of capability passing mentioned Section 3.2. Precisely, this means that a channel can only be used to transmit
the same capabilities regardless of when the communication happens. In practice,
5 This is easy to see via a reduction from the halting problem, e.g., for an arbitrary sequence codes that does not contain c, 1.s; !(c, 1) || 2.!(c, 2) is capability respecting with respect to c iff s does
not halt.
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

20·

T. Terauchi and A. Aiken

this implies that a channel used to synchronize processes sharing resource in one
way cannot be used to synchronize them in another way. For instance, if an output
buffered channel is used to allow a certain shared resource used by process 1 to
be used by process 2 temporarily, then the same output buffered channel cannot
be used by process 2 to give the capability to access the resource to some otherprocess.
Other sources of incompleteness are quite standard for a typical (non-dependent)
type-based analysis, e.g., our analysis is insensitive to branch conditions (and resultsof arithmetic expressions in general), and, so for example,
1.if 0 then !(c, 0) else skip || 2.!(c, 1)
would be reported to be non-deterministic.
Another source of incompleteness is due to the incompleteness of the dynamic
capability calculus relative to partial confluence. For example, even the dynamic
capability calculus is insensitive to the integer values sent across a channel, andso 1.!(c, 0) || 2.!(c, 0) where c is a buffered channel is not capability respectingwith respect to c even though it is partially confluent with respect to c. Also, thecapability calculus cannot reason about any determinism relying on commutativityof arithmetic operations.
Finally, the criteria that every aspect of the program must be deterministic may
be too strict for some real world applications.
We do not currently have the experience with realistic applications that would
allow us to judge how serious these limitations are in practice. Assuming some or
all of these issues needed to be addressed, We believe that it should be possible tocombine our analysis with more powerful (and perhaps more expensive) techniquessuch as state exploration based analyses, and relax the capability requirements toallow some degree of non-determinism when it is harmless.
5. RELATED WORK
We discuss previous approaches to checking and inferring determinism of communicating concurrent processes. Kahn process networks [Kahn 1974] restrict communication to input buffered channels with a unique sender process to guarantee
determinism. Edwards et al. [Edwards and Tardieu 2005] restricts communication
to rendezvous channels with a unique sender process and a unique receiver process
to model deterministic behavior of embedded systems. These models are the easycases for our system where capabilities are not passed between processes.
Linear type systems can infer partial confluence by checking that each channel isused at most once [Nestmann and Steffen 1997; Kobayashi et al. 1999]. Section 4.3
discusses how to express linearly typed channels in our system. A fundamental
difference between these “one-use-per-channel” approaches and our approach isthat our system allows a channel to be used multiple times, just that at any point
in time, only one process can write to it (and read from it, for a rendezvous or
output buffered channel).
König presents a type system that can be parameterized to check partial
confluence of π-calculus programs [König 2000]. König’s system corresponds
to the restricted case of our system where each (rendezvous) channel is givena type of the form ch(ρ, τ, 0 [w(ρ) 7→ 1], 0 [r(ρ) 7→ 1]), i.e., each channel must
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

A Capability Calculus for Concurrency and Determinism·

21

send its own write capability at writes and must send its own read capability at reads. Therefore, for example, while their system can check theconfluence of !(c, 1); ?(c, x)||?(c, x); !(c, 2), it cannot check the confluence of!(c, 1); !(c, 2)||?(c, x); ?(c, x).
The literature on process algebra has popularized the asynchronous π-calculus [Boudol
1992; Honda and Tokoro 1992], which is often studied in close conjunction with linear type systems [Kobayashi et al. 1999; Yoshida et al. 2004]. Here, the term
asynchronous is different from the notion we have been using in this paper. (Theprocesses in vanilla π-calculus are asynchronous in the sense of asynchronous circuits
and systems because they do not run in lock step.) Essentially, the asynchronous
π-calculus is π-calculus with the following restriction: a write to a channel cannot
be sequentially followed by an action (i.e., !(e, e′ ); s is not allowed). Because theasynchronous π-calculus is a subset of the (full) π-calculus, and our system canhandle the fragment of π-calculus without the non-deterministic choice (+) operator, the fragment of the asynchronous π-calculus without + can be handled by oursystem. In fact, our system is quite powerful even in this restricted setting. For
example, our approach can check that the following program is confluent.
!(c, 1)||?(d, x); !(c, 2)||?(c, y); (!(d, 0)|?(c, y))More exhaustive approaches for checking determinism and confluence have been
proposed in which the determinism and confluence are checked by explicitly exploring the program states [Groote and van de Pol 2000; Blom and van de Pol
2002; Hansen and Valmari 2006]. These approaches are precise, and are language
independent and thus potentially work with any model of concurrent computation.
However, an issue with these approaches is that their worst-case running time is atleast linear in the number of run-time states of the program, which can be muchlarger than the size of the program (indeed, it is common for a software program
to have a super-exponential number of states), whereas our algorithm can run intime polynomial in the size of the program. Recently, a compositional approachhas been proposed which may alleviate the problem [Wang and Kwiatkowska 2006].
Also, these methods have a somewhat different aim from our work because they aredesigned specifically to drive state space reduction instead of just checking determinism, i.e., in some sense, the price for exhaustive state space exploration is paidby state space reduction.
This work was motivated by our previous work on inferring confluence of functional languages with global mutable states [Terauchi and Aiken 2005] (see also
[Boyland 2003]). These systems can only reason about synchronization at join
points, and therefore cannot infer confluence of channel-communicating processes.
These systems were in turn motivated by the original capability calculus system [Crary et al. 1999], which was designed to reason about resource usage insequential programs. Whereas the original capability calculus uses rather rigid andcomplex set-oriented rules for manipulating (e.g., splitting and joining) capabilities, fractional capabilities are more flexible and cheaper to reason with because
capability manipulations are based on rational linear arithmetic.
We note that the idea that capabilities can be passed at channel communication points is analogous to ideas underlying various type systems for channelcommunicating processes [Kobayashi et al. 1995; Gordon and Jeffrey 2001; 2002;
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

22·

T. Terauchi and A. Aiken

Igarashi and Kobayashi 2004], for various applications ranging from authentication
protocol to deadlock freedom.
6. CONCLUSIONS
We have presented a system for inferring partial confluence of concurrent programs
communicating via a mix of different kinds of communication methods. We havecast our system as a capability calculus where fractional capabilities can be passed
at synchronizing channel communications, and have presented a type system forstatically inferring partial confluence by finding an appropriate capability passing
strategy in the calculus, which can be reduced in polynomial time to the problem
of solving a system of rational linear inequalities.
7. ACKNOWLEDGEMENTS
We thank Adam Megacz for implementing a type inference prototype [Megacz 2006]
as well as suggesting the | operator extension (Section 4.3), a feature missing fromthe conference paper [Terauchi and Aiken 2006] that was needed for expressing
some FLEET [Coates et al. 2001] programs. We also thank Naoki Kobayashi foruseful discussions, especially his observation that allowing rationals for every kindof capability provably decreases the computational complexity of type inference,
assuming P 6= NP.
REFERENCES
2002. Types and Effects for Asymmetric Cryptographic Protocols. IEEE Computer Society, Cape
Breton, Nova Scotia, Canada.
Aiken, A. and Gay, D. 1998. Barrier inference. In Proceedings of the 25th Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages. San Diego, California, 342–354.
Blom, S. and van de Pol, J. 2002. State space reduction by proving confluence. In Proceedingsof the 14th International Conference on Computer Aided Verification. Copenhagen, Denmark,596–609.
Boudol, G. 1992. Asynchrony and the pi-calculus. Tech. Rep. 1702, INRIA Sophia Antipolis.
May.
Boyland, J. 2003. Checking interference with fractional permissions. In Static Analysis, TenthInternational Symposium. San Diego, CA, 55–72.
Coates, W. S., Lexau, J. K., Jones, I. W., Fairbanks, S. M., and Sutherland, I. E. 2001.
Fleetzero: An asynchronous switching experiment. In 7th International Symposium on Advanced Research in Asynchronous Circuits and Systems (ASYNC 2001). IEEE Computer Society, Salt Lake City, UT, 173–.
Crary, K., Walker, D., and Morrisett, G. 1999. Typed memory management in a calculusof capabilities. In Proceedings of the 26th Annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages. San Antonio, Texas, 262–275.
DeLine, R. and Fähndrich, M. 2001. Enforcing High-Level Protocols in Low-Level Software. In
Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and
Implementation. Snowbird, Utah, 59–69.
Edwards, S. A. and Tardieu, O. 2005. Shim: a deterministic model for heterogeneous embedded
systems. In Proceedings of the 5th ACM International Conference On Embedded Software.
Jersey City, NJ, 264–272.
Foster, J. S., Terauchi, T., and Aiken, A. 2002. Flow-sensitive type qualifiers. In Proceedings ofthe 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation.
Berlin, Germany.
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

A Capability Calculus for Concurrency and Determinism·

23

Gordon, A. D. and Jeffrey, A. 2001. Typing correspondence assertions for communication
protocols. Theoretical Computer Science 45.
Groote, J. F. and van de Pol, J. 2000. State space reduction using partial tau-confluence. In
Proceedings of 25th International Symposium on the Mathematical Foundations of Computer
Science 2000. Bratislava, Slovakia, 383–393.
Hansen, H. and Valmari, A. 2006. Operational determinism and fast algorithms. In CONCUR 2006 - Concurrency Theory, 17th International Conference. Vol. 4137. Springer, Bonn,
Germany, 188–202.
Honda, K. and Tokoro, M. 1992. On asynchronous communication semantics. In Proceedingsof the ECOOP’91 Workshop on Object-Based Concurrent Computing. Springer-Verlag, 21–51.
Igarashi, A. and Kobayashi, N. 2004. A generic type system for the pi-calculus. TheoreticalCompututer Science 311, 1-3, 121–163.
Kahn, G. 1974. The semantics of a simple language for parallel programming. In Information
processing. Stockholm, Sweden, 471–475.
Kobayashi, N. 2007. Personal communication.
Kobayashi, N., Nakade, M., and Yonezawa, A. 1995. Static analysis of communication forasynchronous concurrent programming languages. In Static Analysis, Second International
Symposium. Glasgow, Scotland, 225–242.
Kobayashi, N., Pierce, B. C., and Turner, D. N. 1999. Linearity and the pi-calculus. ACM
Transactions on Programming Languages and Systems 21, 5 (Sept.), 914–947.
König, B. 2000. Analysing input/output-capabilities of mobile processes with a generic typesystem. In Proceedings of the 27th International Colloquium on Automata, Languages andProgramming. Geneva, Switzerland, 403–414.
Lee, E. A. 2006. The problem with threads. Tech. Rep. UCB/EECS-2006-1, EECS Department,
University of California, Berkeley. January 10.
Megacz, A. 2006.
CCCD implementation.
http://research.cs.berkeley.edu/project/cccdimpl/README.
Nestmann, U. and Steffen, M. 1997. Typing confluence. In Proceedings of FMICS ’97. 77–101.
Smith, F., Walker, D., and Morrisett, G. 2000. Alias Types. In 9th European Symposium on
Programming, G. Smolka, Ed. Lecture Notes in Computer Science, vol. 1782. Springer-Verlag,
Berlin, Germany, 366–381.
Sutter, H. and Larus, J. 2005. Software and the concurrency revolution. Queue 3, 7, 54–62.
Terauchi, T. and Aiken, A. 2005. Witnessing side-effects. In Proceedings of the 10th ACM
SIGPLAN International Conference on Functional Programming. ACM, Tallinn, Estonia, 105–
115.
Terauchi, T. and Aiken, A. 2006. A capability calculus for concurrency and determinism. In
CONCUR 2006 - Concurrency Theory, 17th International Conference. Vol. 4137. Springer,
Bonn, Germany, 218–232.
Walker, D. and Morrisett, G. 2000. Alias Types for Recursive Data Structures. In International Workshop on Types in Compilation. Montreal, Canada.
Wang, X. and Kwiatkowska, M. 2006. Compositional state space reduction using untangled
actions. In EXPRESS’06 13th International Workshop on Expressiveness in Concurrency.
Bonn, Germany, 16–28.
Yoshida, N., Berger, M., and Honda, K. 2004. Strong normalisation in the pi -calculus.
Information and Computation 191, 2, 145–202.

A. PROOFS
Lemma A.1. Suppose (B, S, p) →∗ (B ′ , S ′ , p′ ) and i ∈ dom(S). Then S(i) is aprefix of S ′ (i).
Proof. By induction on the reduction sequence.
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

·

24

T. Terauchi and A. Aiken

Lemma 2.3. If P is partially confluent with respect to Y then P is deterministicwith respect to Y .
Proof. Suppose P is partially confluent with respect to Y . We show (1). Let
i be a process index. For contradiction, suppose that there exist reductions P →∗(B1 , S1 , p1 ) and P →∗ (B2 , S2 , p2 ) both communicating only over channels in Y
such that neither S1 (i) nor S2 (i) is a prefix of the other. But because P is partiallyconfluent, there exists Q such that (B1 , S1 , p1 ) →∗ Q and (B2 , S2 , p2 ) →∗ Q. But
by Lemma A.1, such a Q cannot exist.
We now show (2). For contradiction, suppose (2) does not hold. Then it must be
the case that there exist reductions P →∗ (B1 , S1 , p1 ) and P →∗ (B2 , S2 , p2 ) bothcommunicating only over channels in Y such that S1 (i) is shorter than S2 (i) (andso S1 (i) is a prefix of S2 (i) because of (1)) and there exists no (B1′ , S1′ , p′1 ) suchthat (B1 , S1 , p1 ) →∗ (B1′ , S1′ , p′1 ) communicating only over channels in Y and S1′ (i)is longer than S1 (i). But because P is partially confluent, there exists Q such that
(B1 , S1 , p1 ) →∗ Q and (B2 , S2 , p2 ) →∗ Q communicating only over channels in Y .
But then Q is such a (B1′ , S1′ , p′1 ).
Lemma 3.4. Let P be a state. Suppose there exists M such that M is capabilityrespecting with respect to Y and there exists P ∈ M such that erase(P ) = P .
Suppose P → P1 communicating only over channels in Y and P → P2 . Theneither P1 = P2 or there exists Q such that P2 → Q communicating only overchannels in Y and P1 → Q.
Proof. We prove the result by case analysis on P → P1 . Note that because
P ∈ M , there exist P1 and P2 such that—erase(P1 ) = P1 and erase(P2 ) = P2 , and
ℓ

ℓ

1
2
P1 and P →P2 and neither ℓ1 nor ℓ2 is false.
—P →The case where P → P1 is a sequential reduction (i.e., IF1, IF2, WHILE1,
WHILE2, or ASSIGN) is trivial because a sequential reduction affects only one
process and does not interfere with other processes. Suppose P → P1 is:(S(i), e1 ) ⇓ c (S(i), e2 ) ⇓ e′2 (S(j), e3 ) ⇓ c¬buffered(c) S ′ = S[j 7→ S(j) :: (x, e′2 )](B, S, i.!(e1 , e2 ); s1 ||j.?(e3 , x); s2 ||p) → (B, S ′ , i.s1 ||j.s2 ||p)where P = (B, S, i.!(e1 , e2 ); s1 ||j.?(e3 , x); s2 ||p) and P1 = (B, S ′ , i.s1 ||j.s2 ||p). By
assumption, c ∈ Y . If P → P2 does not communicate over c, then the result follows
trivially. So suppose P → P2 communicates over c. Let i′ and j ′ be the processℓ2
P2 is between the writer process i′ and the reader process
indices such that P →j ′ . But because ℓ1 = ℓ2 = true, P being well-formed implies that i = i′ and j = j ′ .
Therefore, P1 = P2 .
Suppose P → P1 is:(S(i), e1 ) ⇓ c (S(i), e2 ) ⇓ e′2 buffered(c)B ′ = B.write(c, e′2 )](B, S, i.!(e1 , e2 ); s||p) → (B ′ , S, i.s||p)ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

A Capability Calculus for Concurrency and Determinism·

25

where P = (B, S, i.!(e1 , e2 ); s||p) and P1 = (B ′ , S, i.s||p). Suppose c is output
buffered or input buffered. By the assumption, c ∈ Y . If P → P2 does notcommunicate over c, then the result follows trivially. Also, if P → P2 is a readfrom c, then because buffers are FIFO, the result follows trivially. So supposeℓ2
P → P2 writes c. Let i′ be the process indices such that P →P2 is a write by′process i . But because ℓ1 = ℓ2 = true, P being well-formed implies that i = i′ .
Therefore, P1 = P2 .
The case where P → P1 reads an output buffered channel is similar. The casewhere P → P1 reads an input buffered channel follows trivially from the fact that
input buffers are process local.
Suppose c is a reference cell. By assumption, c ∈ Y . If P → P2 does not communicate over c, then the result follows trivially. So suppose P → P2 communicatesℓ2over c (read or write). Let i′ be the process indices such that P →P2 is a write ora read by process i′ . But because ℓ1 = ℓ2 = true, P being well-formed implies thati = i′ (so P → P2 is in fact a write). Therefore, P1 = P2 .
Suppose P → P1 is:(S(i), e) ⇓ c

buffered(c) (B ′ , e′ ) = B.read(c, i) S ′ = S[i 7→ S(i) :: (x, e′ )](B, S, i.?(e, x); s||p) → (B ′ , S ′ , i.s||p)where P = (B, S, i.?(e, x); s||p) and P1 = (B ′ , S ′ , i.s||p). Suppose c is a referencecell. By assumption, c ∈ Y . If P → P2 does not communicate over c, then the
result follows trivially. Also, if P → P2 is a read from c then because reading areference cell is non-destructive, the result follows trivially. So suppose P → P2
writes to c. But because ℓ1 = ℓ2 = true, P being well-formed implies that P → P2
is, in fact, not a write to c.
Lemma A.2. If Γ, i, Ψ1 ⊢ s : Ψ2 and Ψ′1 ≥ Ψ1 , then Γ, i, Ψ′1 ⊢ s : Ψ′2 for someΨ′2 ≥ Ψ2
Proof. By structural induction on the type derivation.
Lemma A.3. If Γ ⊢ h, Γ ⊢ e : τ , and (h, e) ⇓ e′ , then Γ ⊢ e′ : τ .
Proof. By structural induction on the type derivation.
Lemma A.4. Γ, i, Ψ ⊢ (s1 ; s2 ); s3 : Ψ′ iff Γ, i, Ψ ⊢ s1 ; (s2 ; s3 ) : Ψ′ .
Proof. By inspection of the type checking rules.
Theorem 3.6. Let M = {P | ∃Env .Env ⊢ P }. Then M is capability-respectingwith respect to Y .
Proof. It suffices to show that if Env ⊢ P , then
(1) P is well-formed, and(2) for any state Q such that erase(P ) → Q, there exists Q and Env′ such thatℓEnv′ ⊢ Q, erase(Q) = Q, P → Q, and if ℓ is not empty then ℓ = true.
Suppose Env ⊢ P . From the second, the third, and the fourth conditions of Env ⊢ P ,it follows that P is well-formed. Thus it suffices to show that (2) holds.
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

26·

T. Terauchi and A. Aiken

Let Q be a state such that erase(P ) → Q. Let P = erase(P ). Let(Γ, Ψ1 , . . . , Ψn , W ) = Env. We show that there exist Q, Ψ′1 , . . . , Ψ′n , and W ′ suchℓthat (Γ, Ψ′1 , . . . , Ψ′n , W ′ ) ⊢ Q, P → Q, and if ℓ is not empty then ℓ = true. (Soin fact, Env and Env′ share the same Γ, indicating the flow-insensitivity of oursystem.) We prove by case analysis on P → Q.
Throughout this proof, we implicitly use Lemma A.4 to convert a type derivation for any sequential composition s1 ; s2 ; . . . ; sn to a derivation for s1 ; (s2 ; . . . ; sn ).
Also, note that typability is invariant under process re-ordering and sequential skip
compositions (i.e., s = s; skip = skip; s).
Suppose P → Q is
(S(i), e) ⇓ n n 6= 0 S(B, S, i.(if e then s1 else s2 ); s||p) → (B, Si.s1 ; s||p)where P = (B, S, i.(if e then s1 else s2 ); s||p) and Q = (B, S, i.s1 ; s||p). Let(X, B, S, i.Ci .((if e then s1 else s2 ); s||p′ ) = P . Let Q = (X, B, S, i.Ci .s1 ; s||p′ ).
Note that erase(Q) = Q and P → Q. By assumption,Γ ⊢ e : int

Γ, i, Ψi ⊢ s1 : Ψi1 Γ, i, Ψi ⊢ s2 : Ψi2 Ψi1 ≥ Ψi3
Γ, i, Ψi ⊢ if e then s1 else s2 : Ψi3

Ψi2 ≥ Ψi3

Γ, i, Ψi ⊢ if e then s1 else s2 : Ψi3 Γ, i, Ψi3 ⊢ s : Ψi4
Γ, i, Ψi ⊢ (if e then s1 else s2 ); s : Ψi4
Therefore, by Lemma A.2, Γ, i, Ψi1 ⊢ s : Ψi5 for some Ψi5 . And so, Γ, i, Ψi ⊢s1 ; s : Ψi5 . Let Ψ′j = Ψj for each j ∈ {1 . . . n} and W ′ = W . Then it follows that(Γ, Ψ′1 , . . . , Ψ′n , W ′ ) ⊢ Q.
The cases where P → Q is IF2, WHILE1, or WHILE2 can be proven in asimilar manner.
Suppose P → Q is
(S(i), e) ⇓ e′ S ′ = S[i 7→ S(i) :: (x, e′ )](B, S, i.x := e; s||p) → (B, S ′ , i.s||p)where P = (B, S, i.x:=e; s||p) and Q = (B, S ′ , i.s||p). Let (X, B, S, i.Ci .x:=e; s||p′ ) =P . Let Q = (X, B, S ′ , i.Ci .s||p′ ). Note that erase(Q) = Q and P → Q. By assumption,Γ ⊢ e : Γ(x)Γ, i, Ψi ⊢ x := e : Ψi
Γ, i, Ψi ⊢ x := e : Ψi Γ, i, Ψi ⊢ s : Ψi1
Γ, i, Ψi ⊢ x := e; s : Ψi1
From Γ ⊢ S(i), Γ ⊢ e : Γ(x), and Lemma A.3, it follows that Γ ⊢ S ′ (i). Let Ψ′j = Ψjfor each j ∈ {1, . . . , n} and W ′ = nW . Then it follows that (Γ, Ψ′1 , . . . , Ψ′n , W ′ ) ⊢ Q.
Suppose P → Q is
(S(i), e1 ) ⇓ c (S(i), e2 ) ⇓ e′2 (S(j), e3 ) ⇓ c¬buffered(c) S ′ = S[j 7→ S(j) :: (x, e′2 )](B, S, i.!(e1 , e2 ); s1 ||j.?(e3 , x); s2 ||p) → (B, S ′ , i.s1 ||j.s2 ||p)ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

A Capability Calculus for Concurrency and Determinism·

27

where P = (B, S, i.!(e1 , e2 ); s1 ||j.?(e3 , x); s2 ||p) and Q = (B, S ′ , i.s1 ||j.s2 ||p). Let(X, B, S, i.Ci .!(e1 , e2 ); s1 ||j.Cj .?(e3 , x); s2 ||p′ ) = P . By assumption,Γ ⊢ e1 : τΓ ⊢ e2 : valtype(τ ) confch(τ, Γ) ⇒ hasWcap(Ψi , τ )Γ, i, Ψi ⊢ !(e1 , e2 ) : Ψi1
Γ, i, Ψi ⊢ !(e1 , e2 ) : Ψi1 Γ, i, Ψi1 ⊢ s : Ψi2
Γ, i, Ψi ⊢ !(e1 , e2 ); s : Ψi2Γ ⊢ e3 : τ ′Γ(x) = valtype(τ ′ ) confch(τ ′ , Γ) ⇒ hasRcap(Ψj , τ ′ )Γ, j, Ψj ⊢ ?(e3 , x) : Ψj1
Γ, j, Ψj ⊢ ?(e3 , x) : Ψj1 Γ, j, Ψj1 ⊢ s : Ψj2
Γ, j, Ψj ⊢ ?(e3 , x); s : Ψj2

where Ψi1 = Ψi − writeSend(τ ) + writeRecv(τ ) and Ψj1 = Ψj − readSend(τ ′ ) +readRecv(τ ′ , j). Lemma A.3 implies that Γ(c) = τ = τ ′ . Let C and C ′ be capability sets such that Γ ⊢ C : writeSend(τ ) and Γ ⊢ C ′ : readSend(τ ). Let
Q = (B, S ′ , i.(Ci − C + C ′ ).s1 ||j.(Cj + C − C ′ ).s2 ||p). Note that erase(Q) = Q.
Let Ψ′i = Ψi1 , Ψ′j = Ψj1 , and Ψ′k = Ψk for each k ∈ {1, . . . , n} \ {i, j}. Because
c must be rendezvous, Ψ′i + Ψ′j = Ψi + Ψj . Also, Γ ⊢ (Ci − C + C ′ ) : Ψ′i andΓ ⊢ (Cj + C − C ′ ) : Ψ′j . Therefore it follows that (Γ, Ψ′1 , . . . , Ψ′n , W ′ ) ⊢ Q.
Suppose c ∈ Y . Then confch(τ, Γ) and confch(τ ′ , Γ), and so hasWcap(Ψi , τ ) andhasRcap(Ψj , τ ′ ). Therefore, hasWcap(Ci , c) and hasRcap(Cj , c). Thus it follows
true
true
/ Y , then P → Q trivially.
that P → Q. On the other hand, if c ∈Suppose P → Q is
(S(i), e1 ) ⇓ c (S(i), e2 ) ⇓ e′2 buffered(c)B ′ = B.write(c, e′2 )(B, S, i.!(e1 , e2 ); s||p) → (B ′ , S, i.s||p)where P = (B, S, i.!(e1 , e2 ); s||p) and Q = (B ′ , S, i.s||p). Let (X, B, S, i.C.!(e1 , e2 ); s||p) =P . By assumption,Γ ⊢ e1 : τΓ ⊢ e2 : valtype(τ ) confch(τ, Γ) ⇒ hasWcap(Ψi , τ )Γ, i, Ψi ⊢ !(e1 , e2 ) : Ψi1
Γ, i, Ψi ⊢ !(e1 , e2 ) : Ψi1 Γ, i, Ψi1 ⊢ s : Ψi2
Γ, i, Ψi ⊢ !(e1 , e2 ); s : Ψi2where Ψi1 = Ψi −writeSend(τ )+writeRecv(τ ), and Γ and Ψi are from the definitionof Γ ⊢ P . Let C ′ be a capability set such that Γ ⊢ C ′ : writeSend(τ ). Let
Q = (X[c 7→ X(c) + C ′ ], B ′ , S, i.(C − C ′ ).s||p). Note that erase(Q) = Q. Let
W ′ = W [Γ[c] 7→ W (Γ[c]) + writeSend(τ )]. Note that ∀d.Γ ⊢ X[c 7→ X(c) + C ′ ](d) :W ′ (Γ[d]). Lemma A.3 implies that Γ(c) = τ . Let Ψ′i = Ψi1 and Ψ′j = Ψj for eachj ∈ {1,
P. . . , n} \ {i}. Because cPis not rendezvous, writeRecv(τ ) = 0 . Therefore,
Ψi + ρ∈dom(W ) W (ρ) = Ψ′i + ρ∈dom(W ′ ) W ′ (ρ). Also, Γ ⊢ (Ci − C) : Ψ′i . Also,for each d output buffered, W ′ (Γ[d]) = |B ′ (d)| × writeSend(Γ(d)), and for each d
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

·

28

T. Terauchi and A. Aiken

P
input buffered, W ′ (Γ[d]) = nj=1 |B ′ (d).j| × readRecv(Γ(d), j). Therefore it follows
that (Γ, Ψ′1 , . . . , Ψ′n , W ′ ) ⊢ Q.
Suppose c ∈ Y . Then confch(τ, Γ), and so hasWcap(Ψi , τ ). Therefore,
true
hasWcap(C, c). Thus it follows that P → Q. On the other hand, if c ∈
/ Y,
true

then P → Q trivially.
Suppose P → Q is
(S(i), e) ⇓ c buffered(c)(B ′ , e′ ) = B.read(c, i) S ′ = S[i 7→ S(i) :: (x, e′ )](B, S, i.?(e, x); s||p) → (B ′ , S ′ , i.s||p)where P = (B, S, i.?(e, x); s||p) and Q = (B ′ , S ′ , i.s||p). Let (X, B, S, i.C.?(e, x); s||p) =P . By assumption,Γ⊢e:τ

Γ(x) = valtype(τ ) confch(τ, Γ) ⇒ hasRcap(Ψi , τ )Γ, i, Ψi ⊢ ?(e, x) : Ψi1
Γ, i, Ψi ⊢ ?(e, x) : Ψi1 Γ, i, Ψi1 ⊢ s : Ψi2
Γ, i, Ψi ⊢ ?(e, x); s : Ψi2where Ψi1 = Ψi − readSend(τ ) + readRecv(τ, i). Let C ′ be a capability set suchthat Γ ⊢ C ′ : readRecv(τ, i). Let Q = (X[c 7→ X(c) − C ′ ], B ′ , S ′ , i.(C + C ′ ).s||p).
Note that erase(Q) = Q. Let W ′ = W [Γ[c] 7→ W (Γ[c]) − readRecv(τ, i)]. Note that∀d.Γ ⊢ X[c 7→ X(c) − C ′ ](d) : W ′ (Γ[d]). Lemma A.3 implies that Γ(c) = τ . Let
Ψ′i = Ψi1 and Ψ′j = Ψj for each j ∈ P{1, . . . , n} \ {i}. Because cP
is not rendezvous,
readSend(τ ) = 0 . Therefore, Ψi + ρ∈dom(W ) W (ρ) = Ψ′i + ρ∈dom(W ′ ) W ′ (ρ).
Also, for each d output buffered, P
W ′ (Γ[d]) = |B ′ (d)| × writeSend(Γ(d)), and for′each d input buffered, W (Γ[d]) = nj=1 |B ′ (d).j| × readRecv(Γ(d), j). Therefore it
follows that (Γ, Ψ′1 , . . . , Ψ′n , W ′ ) ⊢ Q.
Suppose c ∈ Y . Then confch(τ, Γ), and so hasRcap(Ψi , τ ). Therefore,
true
hasRcap(C, c). Thus it follows that P → Q. On the other hand, if c ∈/ Y , thentrue

P → Q trivially.
Theorem 4.1. Suppose the type system is altered such that for any capability
set Ψ appearing in the type derivation, Ψ(ρ) ∈ {0, 1} for all ρ. Then the set{P | ∃.Env , P .Env ⊢ P ∧ P = erase(P )} is NP-hard.
Proof. We prove the result by reduction from one-in-three 3-SAT, a restrictedversion of 3-SAT where a satisfying assignment must set exactly one literal in eachclause (instead of at least one) to 1. One-in-three 3-SAT is known to be NPcomplete.
Let φ = c1 ∧c2 ∧· · ·∧cm where each clause ci is of the form l1 ∨l2 ∨l3 where each li
is a literal, i.e., either a variable or a negation of a variable. Let {a1 , . . . , an } be theset of variables appearing in φ. For each variable ai , let ai and ai be distinct output
buffered channels, representing the literals a and ¬a, respectively. Let truech be a
distinct output buffered channel.
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.

A Capability Calculus for Concurrency and Determinism·

29

Let p be the following program consisting of n + 1 processes:
p = !(truech, 0); !(a1 , 0); !(a1 , 0)|| ?(a1 , x); ?(a1 , x); !(truech, 0); !(a2 , 0); !(a2 , 0)|| . . . || ?(an−1 , x); ?(an−1 , x); !(truech, 0); !(an , 0); !(an , 0)|| ?(an , x); ?(an , x); !(truech, 0)
For each literal l, let l∗ denote its representative channel, i.e., for a variable a,a∗ = a and (¬a)∗ = a. For each clause c = l1 ∨ l2 ∨ l3 , let pc be the process defined
as follows.
pc = ?(l1∗ , x); ?(l2∗ , x)?(l3∗ , x); !(truech, 0)
Let pφ = p || pc1 || pc2 || . . . || pcm . Let P = (B, {x 7→ 0}, pφ ) where B(c) is anempty queue for all channels c. We claim that φ is one-in-three 3SAT satisfiable
iff there exists Env and P such that Env ⊢ P and P = erase(P ) where the set ofchannels to be checked for partial confluence is {truech} (i.e., c ∈ Y ⇔ c = truech).
To see this, note that the typability of p implies that for each variable a, exactly
one of a and a sends the w(truech) capability on channel write. Thus p makes thechannels a and a represent the boolean value of the variable a. For each clause c,
the typability of pc ensures that exactly one of its literals are set to 1, i.e., receives
the w(truech) capability on channel read. Thus Γ ⊢ P implies that φ is one-in-three
3SAT satisfiable, and vice versa.

ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Month 20YY.