Inferring Channel Buffer Bounds via Linear
Programming
Tachio Terauchi1 and Adam Megacz2
1

Tohoku University
terauchi@ecei.tohoku.ac.jp
2
University of California, Berkeley
megacz@cs.berkeley.edu

Abstract. We present a static analysis for inferring the maximum amountof buffer space used by a program consisting of concurrently running processes communicating via buffered channels. We reduce the problem tolinear programming by casting the analysis as a fractional capability calculus system. Our analysis can reason about buffers used by multiple
processes concurrently, and runs in time polynomial in the size of the
program.

1

Introduction

We consider programs consisting of concurrently running processes communicating via buffered channels. Each process runs sequentially at its own speed, andsynchronizes by communicating over channels. Communications are buffered in
the sense that the messages may not be immediately sent to the receiver, but areheld at some place. But holding messages costs buffer resources. If the buffers
have a predetermined maximum size, unwanted behavior may happen if a processtries to send over a channel whose buffer is full. If the buffer is lossy, messages
could get lost. Otherwise, it could block or change the sender process’s control
flow. This paper presents a static analysis for obtaining a conservative boundon channel buffers so that such behavior never happens, that is, channel buffers
are used within their bounds. Such an analysis has application in determining a
program’s resource usage bound.
We cast our analysis as a capability calculus. The capability calculus is a static
system originally proposed for reasoning about resources in sequential computation [2]. We use the extension of the capability calculus to channel communicating concurrent programs to allow capabilities to be passed at synchronization
points [6]. We also use fractional capabilities [1, 5, 6] so that we can efficiently
infer capabilities via linear programming.
Our analysis can automatically discover some non-trivial buffer bounds. For
example, consider the program in Figure 1 consisting of two concurrently running
processes communicating via the channels foo and bar, used to transmit integer
values. The variables i, j, m, n are assumed to be initialized to some positive
integers. Process 1 reads from the channel bar and stores the read value inProcess 1
while i < mbar?(x);foo!(1);foo!(i);i := i + x

Process 2
while j < nbar!(j);foo?(y);foo?(z);j := j + y + z

Fig. 1. Example.

variable x, writes twice to foo, and then updates the variable i and repeats if
the loop condition is met. Process 2 writes once to bar and reads twice fromfoo, and then repeats if the loop condition is met. Buffer space to store only one
integer is needed for the channel bar. This is because when process 2 is about
to write to bar for the second time, process 1 must have already read the first
integer from bar as process 2’s write is preceded by the two reads from foo inthe previous iteration, which in turn were written by process 1 after the readfrom bar. The same argument holds by induction for the subsequent iterationof the loop. Similarly, the program only needs buffer space to store two integers
for the channel foo. Our analysis is able to automatically infer these optimal
bounds.
The rest of the paper is organized as follows. Section 2 introduces the syntax of the simple concurrent language we use to describe the analysis. Section 3
defines the operational semantics of the language and formally defines what itmeans for a program to run within a buffer bound. Section 4 presents the capability calculus which statically guarantees that a program runs within a bufferbound. Section 5 presents the analysis algorithm as a type inference algorithm
for the capability calculus. Section 6 discusses limitations of our work. Section 7
discusses related work. Section 8 concludes.

2

The Simple Concurrent Language

We focus on the simple concurrent language shown in Figure 2. The language isessentially the simple imperative language WHILE extended with concurrency
primitives. Formally, a program, p, is a parallel composition of finitely many
processes. A process, i.s, is a sequential statement s prefixed by a process index
i. A sequential statement consists of the usual imperative features as well as
primitives for buffered communications. Here, e1 !(e2 ) means writing the valueof e2 to the buffered channel e1 , and e?(x) means storing the value read fromthe channel e in variable x. The variables are process-local, and so the onlymeans of communication are channel reads and writes. We use meta-variables
x, x′ , etc. for variables and c, c′ , etc. for channels. Channels are first class andcan be used as values, that is, they can be assigned to variables or written tochannels. Binary integer operations such as +, −, ×, ≤, etc., are ranged over by
the symbol op.

p ::= i.s(process)| p1 || p2(parallel composition)s ::= s1 ; s2(sequential composition)| skip(skip)| if e then s1 else s2 (branch)| while e do s(loop)| x := e(assignment)| e1 !(e2 )(channel write)| e?(x)(channel read)e ::= c(channel constant)| x(local variable)| n(integer constant)| e1 op e2(integer operation)
Fig. 2. The syntax of the simple concurrent language.

To keep the presentation to the novel features of the analysis, this simple
language lacks the ability to create processes and channels dynamically, but it iseasy to extend the analysis to handle dynamic creation of processes and channels
by borrowing the techniques from [3, 6].

3

Operational Semantics

We define the following mathematical convention. Given a mapping (i.e., a settheoretic function) f , f [a 7→ b] is a mapping such that f [a 7→ b](a) = b andf [a 7→ b](a′ ) = f (a′ ) for a′ 6= a.
The operational semantics of the language is defined as a series of reductions
from states to states. A state is represented by the triple (B, S, p) where B is abuffer and S is a store.
A store is a mapping from process index to process store. A process store amapping from variables to values. We use symbols h, h′ , etc. to denote a process
store. Values are subset of expressions (e) defined as follows.
v ::= c | n
Figure 3 shows the evaluation rules. Expressions are evaluated entirely locally.
Their evaluation relation are of the form (h, e) ⇓ v and defined by the rules
Chan, Int, Var, and Op. Here, [[op]] is the standard semantics of the binary
operator op. The sequential composition operator ; is associative. Also, we letskip be a ; identity, that is, s = s; skip = skip; s. The parallel composition
operator || is commutative and associative, e.g., p1 || p2 || p3 = p2 || p3 || p1 .
Note that the process reduction rules only reduce the left-most process, and so
we rely on process re-ordering to reduce other processes. We assume that theprocess indices are disjoint in any program p. 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.

(h, c) ⇓ c(h, x) ⇓ h(x)

Var

Chan

(h, n) ⇓ n

Int(h, e1 ) ⇓ n1
(h, e2 ) ⇓ n2(h, e1 op e2 ) ⇓ n1 [[op]] n2

Op(S(i), e) ⇓ nn 6= 0(B, S, i.(if e then s1 else s2 ); s || p) → (B, S, i.s1 ; s || p)

If1(S(i), e) ⇓ 0(B, S, i.(if e then s1 else s2 ); s || p) → (B, S, i.s2 ; s || p)If2(S(i), e) ⇓ nn 6= 0(B, S, i.(while e do s1 ); s || p) → (B, S, i.s1 ; (while e do s1 ); s || p)(S(i), e) ⇓ 0(B, S, i.(while e do s1 ); s || p) → (B, S, i.s || p)(S(i), e) ⇓ v
S ′ = S[i 7→ S(i)[x 7→ v]](B, S, i.x := e; s || p) → (B, S ′ , i.s || p)While2

Assign(S(i), e1 ) ⇓ c(S(i), e2 ) ⇓ v
B ′ = B.write(c, v)(B, S, i.e1 !(e2 ); s || p) → (B ′ , S, i.s || p)(S(i), e) ⇓ c

While1Write(B ′ , v) = B.read(c)S ′ = S[i 7→ S(i)[x 7→ v]](B, S, i.e?(x); s || p) → (B ′ , S ′ , i.s || p)ReadFig. 3. The operational semantics of the simple concurrent language.

Write and Read handle communications over channels. We write
B.write(c, v) for the buffer B after v is written to the channel c, and B.read(c)for the pair (B ′ , v) where v is the value read from channel c and B ′ is the buffer
after the read.
Formally, a buffer B is a mapping from channels to buffer contents. We model
buffer contents as a bag of values. Buffer writes and reads are defined as follows.
B.write(c, v) = B[c 7→ B(c) ⊎ {v}]B.read(c) = (B[c 7→ S], v)if B(c) = S ⊎ {v}Here, ⊎ denotes bag union, e.g., {v} ⊎ {v} = {v, v}. Note that we are not concerned about the order of values written/read to/from a buffer, and so to allow
maximum generality, we model a buffer as a bag of values from which an arbitrary value can be read at a channel read provided that the bag is non-empty.
The operational semantics allows arbitrary many values to be stored in abuffer. In practice, buffers may be bounded due to physical resource constraints.
Exactly what happens if a sender tries to write to a full buffer is outside of thescope of the paper. The goal of the analysis is to infer buffer bounds to ensurethat such behavior never occurs. In contrast, a receiver is allowed to wait on an
empty buffer, allowing the processes to synchronize over a channel.
For simplicity, we assume that every value has the same size and occupies
the same amount of space in the buffers. We write P →∗ Q for zero or more
reduction steps from the state P to the state Q. We now formally define what
it means for a program to run within a buffer bound.
Definition 1. We say that the buffer bound of c in P is within n if for any(B, S, p) such that P →∗ (B, S, p), |B(c)| ≤ n.

4

The Capability Calculus

Our analysis returns a buffer bound for each channel in the program. To thisend, we design a capability calculus such that given a state P , we can obtain abuffer bound for each channel in P from the derivation for P in the calculus.
The capability calculus is a kind of a type system. The types are defined asfollows.
τ ::= ch(ρ, τ, Ψ ) (channels)| int(integers)
The type ch(ρ, τ, Ψ ) denotes a type of a channel used to send and receive values of
the type τ . Here, ρ is the handle of the channel. Let Handles be the set of channel
handles. Symbols Ψ , Ψ ′ , etc. represent capability mappings. A capability mapping
is a function from Handles to non-negative rational numbers augmented with∞, that is, Q+ ∪ {0, ∞}. We use the ordering q ≤ ∞ for all q ∈ Q+ ∪ {0, ∞},and the following arithmetic relation: q + ∞ = ∞, q × ∞ = ∞ for q 6= 0, and0 × ∞ = 0.
We say that Ψ such that Ψ (ρ) = q has q amount of ρ. We often refer toΨ itself as “capabilities”, with the understanding that we mean the amountof capabilities in Ψ . Capabilities are conceptual, that is, capabilities only exist
in the static type system world and do not appear in the dynamic semantics.
Conceptually, each process holds some amount of capabilities representing theamount of buffer space available for its use. For instance, a process holding
capabilities Ψ may write Ψ (ρ) many values to the buffers for channels with thehandle ρ. The capability mapping appearing in a channel type represent thecapabilities that are passed when communicating over that channel. That is,when two processes communicate over a channel having the type ch(ρ, τ, Ψ ), thesender process passes the capabilities Ψ to the receiver process.
We define arithmetic operations over capabilities. The addition and subtraction of capability mappings are defined point-wise as Ψ + Ψ ′ = λρ.Ψ (ρ) + Ψ ′ (ρ)
and Ψ − Ψ ′ = λρ.Ψ (ρ) − Ψ ′ (ρ). Because capabilities must be non-negative, Ψ − Ψ ′is undefined if Ψ (ρ) < Ψ ′ (ρ) for some ρ. We define the relation Ψ ≤ Ψ ′ point-wiseas ∀ρ ∈ Handles.Ψ (ρ) ≤ Ψ ′ (ρ). For convenience, we let 0 denote a constant capability mapping that maps all handles to 0, that is, 0 = λρ.0. Therefore, forexample, 0 [ρ 7→ 1] is a capability mapping that maps ρ to 1 and ρ′ to 0 for allρ′ 6= ρ.

Γ ⊢ c : Γ (c)Γ ⊢ x : Γ (x)Γ, Ψ ⊢ skip : Ψ

CHAN

VAR

SKIP

Γ ⊢ n : intΓ ⊢ e1 : intΓ ⊢ e2 : intΓ ⊢ e1 op e2 : intΓ ⊢ e : Γ (x)Γ, Ψ ⊢ x := e : ΨΓ, Ψ ⊢ s1 : Ψ1
Γ, Ψ1 ⊢ s2 : Ψ2
Γ, Ψ ⊢ s1 ; s2 : Ψ2Γ ⊢ e : int

Γ, Ψ ′ ⊢ s : Ψ ′′Ψ′ ≤ Ψ
Γ, Ψ ⊢ while e do s : Ψ ′OP

ASSIGNSEQΨ ′ ≤ Ψ1
Ψ ′ ≤ Ψ2
Γ, Ψ ⊢ s1 : Ψ1
Γ, Ψ ⊢ if e then s1 else s2 : Ψ ′Γ ⊢ e : int

INTΓ, Ψ ⊢ s2 : Ψ2

Ψ ′ ≤ Ψ ′′

IF

WHILE

Γ ⊢ e : ch(ρ, Γ (x), Ψ ′ )Γ, Ψ ⊢ e?(x) : Ψ + Ψ ′ + 0 [ρ 7→ 1]READΓ ⊢ e : ch(ρ, τ, Ψ ′ )Γ ⊢ e′ : τ′′Γ, Ψ ⊢ e!(e ) : Ψ − Ψ − 0 [ρ 7→ 1]

WRITE

Fig. 4. The type checking rules.

Figure 4 shows the type checking rules. The judgements for expressions areof the form Γ ⊢ e : τ , where Γ is a type environment mapping variables andchannels to their types. The rules VAR, CHAN, INT, and OP type expressions
and are self-explanatory.
The type judgements for the statements are of the form Γ, Ψ ⊢ s : Ψ ′ , whereΨ is the capabilities before the execution of s, and Ψ ′ is the capabilities after
the execution of s. SKIP, SEQ, and ASSIGN are self-explanatory. IF ensuresthat the capabilities at the branch join point cannot exceed the capabilities after
the then branch or the else branch. WHILE is similar to IF.
In READ, the hypothesis ensures that type of the received value agrees withthe type of the variable where the value is going to be stored. In the conclusionof READ, the capabilities Ψ ′ passed from the sender is added to the capabilities
held by the process. In addition, because a read frees a buffer space, we gain asingle buffer space, and so we add the capability 0 [ρ 7→ 1].
WRITE passes Ψ ′ to the receiver, and thus the capabilities Ψ ′ is subtracted
in the conclusion of the rule. The subtraction of capabilities is defined as Ψ1 −
Ψ2 = Ψ3 iff Ψ3 + Ψ2 = Ψ1 . In addition, because a write uses a buffer space,
we express this by subtracting 0 [ρ 7→ 1] in the conclusion. Note that the nonnegativity assumption of capabilities implies that Ψ (ρ) ≥ 1.
We define some notational shortcuts. Let writeSend(ch(ρ, τ, Ψ )) = Ψ andhdl(ch(ρ, τ, Ψ )) = ρ. Let HCB (ρ, Γ ) be the subset of the domain of B having thehandle ρ, that is,
HCB (ρ, Γ ) = {c ∈ dom(B) | hdl(Γ (c)) = ρ}Note that |HCB (ρ, Γ )| > 1 means that multiple channels have the same handleρ.
We write Γ ⊢ B(c) to mean that the buffer B(c) is well-typed, that is, foreach v ∈ B(c), Γ ⊢ v : τ , where Γ (c) = ch(ρ, τ, Ψ ) for some ρ, Ψ . We write Γ ⊢ hto mean that the process store h is well-typed, that is, Γ ⊢ h(x) : Γ (x) for eachx ∈ dom(h). Because variables are process local, without loss of generality, we
assume that each process uses a disjoint set of variables.
Definition 2 (Well-typed State). We writeΓ, Ψ1 , . . . , Ψn , ΨB ⊢ (B, S, i1 .s1 || . . . ||in .sn )if(1) For each channel c ∈ dom(B), Γ ⊢ B(c).
(2) For each ij , Γ ⊢ S(ij ).
(3) For each sj , Γ, Ψj ⊢ sj : Ψj′ for some Ψj′ .
P(4) ΨB = c∈dom(B) |B(c)| × writeSend(Γ (c)).
In (4), m × Ψ is defined as λρ.m × Ψ (ρ).
For simplicity, we have used simple types so that some programs are untypable (for instance, a program that uses integers as channels). But it is easy
to extend the system with sum types and recursive types so that all programs
become typable [4].
We now state the main result of this section which says that a well-typed
program runs within buffer bounds that can be obtained from its type derivation.
Theorem 1.
PnSuppose Γ, Ψ1 , . . . , Ψn , ΨB ⊢ (B, S, p). Suppose hdl(Γ (c)) = ρ. Let
Ψ
=
Ψ
+
B
j=1 Ψj . Then the buffer bound of c in (B, S, p) is within Ψp (ρ) +
Pp
′
|B(c
)|.
c′ ∈HCB (ρ,Γ )The key steps of the proof appear in the appendix.
4.1

ExampleRecall the following program from Section 1. Let us call this program p.
1.while i < m do (bar?(x); foo!(1); foo!(i); i := i + x) ||2.while j < n do (bar!(j); foo?(y); foo?(z); j := j + y + z)
Let B be an empty buffer, that is, B(foo) = B(bar) = ∅. Let S be a store suchthat S(1) maps i, m, x to some integer and S(2) maps j, n, y, z to some integer.

LetΓ = {i 7→ int, j 7→ int, m 7→ int, n 7→ int,
x 7→ int, y 7→ int, z 7→ int,
foo 7→ ch(ρfoo , int, 0 [ρbar 7→ 0.5]),
bar 7→ ch(ρbar , int, 0 [ρfoo 7→ 2])}
Ψ1 = ΨB = 0
Ψ2 = 0 [ρfoo 7→ 2][ρbar 7→ 1]
Then, we have Γ, Ψ1 , Ψ2 , ΨB ⊢ (B, S, p). The type of foo indicates that wheneverprocess 2 reads from foo, 0.5 amount of capability for bar is passed to process
2. Therefore, by reading foo twice, process 2 gains 0.5 + 0.5 = 1 buffer space forbar. Likewise, bar’s type says that reading bar once begets two buffer space forfoo.
Let Ψp = Ψ1 + Ψ2 + ΨB . Note that Ψp (ρfoo ) = 2 and Ψp (ρbar ) = 1, indicatingthat the buffer bound of foo is 2 in (B, S, p) and the buffer bound of bar is 1 in
(B, S, p). As argued in Section 1, these are the optimal bounds for the program.

5

Analysis Algorithm

Intuitively, the analysis algorithm is a type inference algorithm for the type system presented in Section 4. Because there are multiple type derivations possible
for a program, we would like to obtain a derivation that gives the smallest bufferbound for each channel. Our strategy is to reduce the problem to linear programming such that the buffer bound appears as the objective function to beminimized.
The analysis is separated in two phases. Informally, the first phase infers
everything about the type derivation except for the amount of capabilities. The
second phase uses linear programming to find the minimum amount of capabilities required to complete the type derivation.
5.1

Phase 1

The first phase is mostly a standard type-based analysis based on unification
constraints, generating capability constraints on the side. Figure 5 shows theconstraint generation rules. Here, α’s are type variables, ̺’s are channel handle variables, and ϕ’s are capability mapping variables. The inference rules are
straightforward constraint-based implementation of the type checking rules in
Figure 4.
The inference judgement for expressions, ∆ ⊢ e : α; C, is read “given theenvironment ∆, e is inferred to have the type α with the set of constraints
C.” The inference judgement for statements, ∆, ϕ ⊢ s : ϕ′ ; C is read “given
environment ∆, s is inferred to have the pre-capability ϕ and the post-capability
ϕ′ with the set of constraints C.”

α, ̺, ϕ fresh∆ ⊢ c : ∆(c); {ch(̺, α, ϕ) = ∆(c)}
α fresh∆ ⊢ n : α; {α = int}

INT

CHAN

∆ ⊢ x : ∆(x); ∅VAR∆ ⊢ e1 : α1 ; C1
∆ ⊢ e2 : α2 ; C2
α3 fresh∆ ⊢ e1 op e2 : α3 ; C1 ∪ C2 ∪ {α1 = α2 = α3 = int}
ϕ fresh∆, ϕ ⊢ skip : ϕ; ∅

OP

SKIP

∆ ⊢ e : α; C
ϕ fresh∆, ϕ ⊢ x := e : ϕ; C ∪ {α = ∆(x)}

ASSIGN∆, ϕ1 ⊢ s1 : ϕ′1 ; C1∆, ϕ2 ⊢ s2 : ϕ′2 ; C2′∆, ϕ1 ⊢ s1 ; s2 : ϕ2 ; C1 ∪ C2 ∪ {ϕ′1 = ϕ2 }SEQ

∆ ⊢ e : α; C∆, ϕ1 ⊢ s1 : ϕ′1 ; C1∆, ϕ2 ⊢ s2 : ϕ′2 ; C2ϕ, ϕ′ fresh′∆, ϕ ⊢ if e then s1 else s2 : ϕ ;C ∪ C1 ∪ C2 ∪ {α = int, ϕ1 = ϕ2 = ϕ, ϕ′ ≤ ϕ′1 , ϕ′ ≤ ϕ′2 }∆ ⊢ e : α; C∆, ϕ′ ⊢ s : ϕ′′ ; C ′ϕ fresh′∆, ϕ ⊢ while e do s : ϕ ; C ∪ C ′ ∪ {α = int, ϕ′ ≤ ϕ, ϕ′ ≤ ϕ′′ }WHILE∆ ⊢ e : α; C̺, ϕ, ϕ′ , ϕ′′ fresh′′′∆, ϕ ⊢ e?(x) : ϕ ; C ∪ {α = ch(̺, ∆(x), ϕ ), ϕ′′ = ϕ + ϕ′ + 0 [̺ 7→ 1]}∆ ⊢ e : α; C
∆ ⊢ e′ : α′ ; C ′̺, ϕ, ϕ′ , ϕ′′ fresh′′′∆, ϕ ⊢ e!(e ) : ϕ ;C ∪ C ′ ∪ {α = ch(̺, α′ , ϕ′ ), ϕ′′ = ϕ − ϕ′ − 0 [̺ 7→ 1]}

IF

READ

WRITE

Fig. 5. The type inference rules.

We initialize ∆ such that each ∆(x) and each ∆(c) is a fresh type variable.
We visit each AST node (expressions and statements) in a bottom up manner
to build the set of constraints.
The resulting set of constraints contains two kinds of constraints:(a) Type unification constraints: σ = σ ′(b) Capability inequality constraints: φ ≤ φ′where

σ ::= α | ch(̺, α, ϕ) | int
φ ::= ϕ | 0 [̺ 7→ 1] | φ + φ | φ − φNote that an equality constraint φ = φ′ can expressed by inequality constraints
φ ≤ φ′ and φ′ ≤ φ. The constraints of the kind (a) can be resolved by thestandard unification algorithm, which may create more constraints of the kind(b). In addition, it creates constraints of the form ̺ = ̺′ , which can also be
resolved by the standard unification algorithm. This leaves us with a set of
constraints of the kind (b).
5.2

Phase 2The second phase of the algorithm finds a satisfying solution to the remaining
constraints generated in the first phase. In general, there can be more than
one solution to these constraints. We find the minimum solution as follows. Let
p = i1 .s1 || . . . || in .sn be the program being analyzed. Phase 1 returns precapability ϕj for each process sj such that ∆, ϕj ⊢ sj : ϕ′j ; Cj . We create a freshPncapability mapping variable ϕp and add the constraint ϕp = j=1 ϕj .
Next, for each ̺ (that is, its equivalence class obtained via the unificationin phase 1), we instantiate a linear programmingPproblem using the remainingnconstraints together with the constraint ϕp =i=1 ϕi . More precisely, eachconstraint mapping variable ϕ is instantiated as a linear programming variable
ϕ(̺), and 0 [̺′ 7→ 1] is replaced by 1 if ̺′ = ̺ and by 0 otherwise. We also add
constraints ϕ(̺) ≥ 0 to ensure that each capability mapping is non-negative. The
objective function to minimize is ϕp (̺). For any solution to the set of constraints,
ϕp (̺) is a valid buffer bound on the channel with the handle ̺, and so minimizing
ϕp (̺) gives us the best possible buffer bound for the analysis.
We state the correctness of the analysis algorithm. We use the symbol η to denote a constraint solution, which is a sorted substitution mapping type variables
to types, channel handle variables to channel handles, and capability mapping
variables to capability mappings. A constraint solution becomes a mapping fromσ, ∆, and φ in the obvious way (we let η(0 [̺ 7→ 1]) = 0 [η(̺) 7→ 1]).
Definition 3. We write η |= C (“η solves C”) if– for each σ = σ ′ ∈ C, η(σ) = η(σ ′ ).
– for each φ ≤ φ′ ∈ C, η(φ) ≤ η(φ′ ).
Lemma 1.
– If ∆ ⊢ e : α; C and η |= C, then η(∆) ⊢ e : η(α).
– If ∆, ϕ ⊢ s : ϕ′ ; C and η |= C, then η(∆), η(ϕ) ⊢ s : η(ϕ).
Proof. By induction on the type derivation.
Theorem 2 (Soundness). Let p = i1 .s1 || . . . || in .sn . Supposeη |= {ϕp =

n
X
j=1

ϕj } ∪

n
[

Cj

j=1

where ∆, ϕj ⊢ sj : ϕ′j ; Cj for each sj . Let P = (B, S, p) such that B is anempty buffer (i.e., B(c) = ∅ for all channels c) and S is a store such thatη(∆) ⊢ S(ij ) for each ij , then the buffer bound of c in P is within η(ϕp )(ρ),
where ρ = hdl(η(∆)(c)).

Proof. Straightforward from Lemma 1 and Theorem 1.
We have implemented a prototype of the analysis algorithm, available at
http://research.cs.berkeley.edu/project/cccd-impl.
5.3

Analysis of The Algorithm

Linear programming is one of the most well studied problems in computer science. Algorithms with both good theoretical complexity and practical runningtimes are known. The instance of linear programming problem in phase 2 canbe solved in time polynomial in the size of the constraints by algorithms such as
interior points methods.
Therefore, the complexity of the algorithm is bound by the time phase 1
takes to generate the capability constraints, which is polynomial for our simple
concurrent language. In general, the complexity will increase if we include more
complex programming constructs such as data structures and functions if westick with the simple types. But this can be avoided by incorporating sum types
and recursive types [4].
5.4

ExampleWe demonstrate the algorithm on the running example.
1.while i < m do (bar?(x); foo!(1); foo!(i); i := i + x) ||2.while j < n do (bar!(j); foo?(y); foo?(z); j := j + y + z)
Suppose that the following environment ∆ was inferred in the first phase.
∆(i) = ∆(j) = ∆(m) = ∆(n) = int∆(x) = ∆(y) = ∆(z) = int∆(foo) = ch(̺foo , int, ϕfoo )∆(bar) = ch(̺bar , int, ϕbar )The capability constraints generated from analyzing process 1 are as follows(after some simplification).
ϕentr1 ≤ ϕexit1
ϕtemp11 = ϕentr1 + ϕbar + 0 [̺bar 7→ 1]
ϕtemp12 = ϕtemp11 − ϕfoo − 0 [̺foo 7→ 1]
ϕexit1 = ϕtemp12 − ϕfoo − 0 [̺foo 7→ 1]
Here, ϕentr1 is the capabilities at the while loop entry, ϕexit1 is the capabilities
at the loop exit, ϕtemp11 is the capabilities after the read bar?(x), and ϕtemp12
is the capabilities after the write foo!(1). The capability constraints generated
from analyzing process 2 are as follows (after some simplification).
ϕentr2 ≤ ϕexit2
ϕtemp21 = ϕentr2 − ϕbar − 0 [̺bar 7→ 1]
ϕtemp22 = ϕtemp21 + ϕfoo + 0 [̺foo 7→ 1]
ϕexit2 = ϕtemp22 + ϕfoo + 0 [̺foo 7→ 1]

Here, ϕentr2 is the capabilities at the while loop entry, ϕexit2 is the capabilities
at the loop exit, ϕtemp21 is the capabilities after bar!(j), and ϕtemp22 is thecapabilities after foo?(y).
The capabilities to minimize is ϕp = ϕentr1 + ϕentr2 , or more precisely,
ϕp (̺foo ) and ϕp (̺bar ). For ϕp (̺bar ), this reduces to solving the following linear
programming instance.
minimize entr1 + entr2
exit2 ≥ entr2
exit1 ≥ entr1
temp21 = entr2 − bar − 1
temp11 = entr1 + bar + 1
temp22 = temp21 + foo
temp12 = temp11 − fooexit2 = temp22 + foo
exit1 = temp12 − foo
We also add the constraint a ≥ 0 for each linear programming variable a appearing above. The minimum solution is attained at{entr1 = 0, entr2 = 1, bar = 0, foo = 0.5,
temp11 = 1, temp12 = 0.5, exit1 = 0,
exit2 = 1, temp21 = 0, temp22 = 0.5}
This gives us the bound entr1 + entr2 = 1. Similarly, solving for the minimum
ϕp (̺foo ) gives us the bound 2 for foo.

6

Limitations

Our analysis cannot infer a finite buffer bound for channels written in a (reachable) loop whose capabilities cannot be “balanced” at the loop exit. Consider
the following program.
1.i := 0; while i < 3 do (c!(0); i := i + 1)
Clearly, the buffer bound for the channel c is 3. But note that the WHILE
rule in Figure 4 requires the capabilities at the end of the loop to be greaterthan that of the start, and this is not possible for this loop due to c!(0). This
manifests in the analysis as ∞ returned as the bound (that is, there exists nofinite solution to the linear programming instance). This implies that any loopthat makes an “unbalanced send” must be unrolled prior to the analysis. Thisis actually an instance of the analysis’s insensitivity to branch conditions. The
issue just becomes most pronounced for loops.
Also, because of its simple flow&path-insensitive unification-based nature,
our analysis may equate different channels when channels are used as values(e.g., stored in variables and passed as messages). This leads to different channels
sharing the same buffer in the analysis. For example, analyzing the program
below, the analysis equates the channels c and d, and thus infers the bound 2
for both c and d even though the ideal bound is 1.
1.x := c; x := d || 2.c!(0) || 3.d!(0)Hence, the analysis may need to be coupled with a more powerful alias analysis
to analyze programs that extensively use channels as values.

7

Related Work

Closely related work is Kobayashi et al.’s type and effect system [3] for inferring
the upper bound on the number of pending inputs and outputs on rendezvous
channels. There are several differences from our work with theirs. One is that
their system relies more on the syntactic structure of the program to determine who is responsible to send and receive capabilities (viewing their effectconstraints as capability sends and receives). For instance, if there are multiple
reads in a succession then the last read is responsible for receiving all the necessary capabilities. In contrast, our analysis allows more freedom on who cansend and receive capabilities, and lets linear programming choose the optimal
amount of capabilities to send and receive. For example, in the program below,
the optimum buffer space for the channel c is 1, which our analysis is able toinfer.
1.c!(0) || 2.b?(x); a?(x); c!(1) || 3.c?(y); b!(0) || 4.a!(0)But because c!(1) is preceded immediately by a?(x), Kobayashi et al.’s system
infers the bound 2 instead. Another difference is the use of fractions (i.e., rationalarithmetic) that allows our system to have a polynomial time type inference via
linear programming. Also, some programs (e.g., the running example) require
fractions to infer the optimal buffer bound.
The main technique used in our analysis, passing of fractional capabilities,
was used for the purpose of checking determinism of concurrent programs [6].
Fractional capabilities were invented for the purpose of allowing concurrent readsof reference cells [1, 5], and capability calculus was originally proposed for reasoning about resources in sequential programs [2]. In previous applications offractional capabilities, linear programming was used only to find a satisfying
solution to a set of linear inequality constraints, whereas our work makes use of
the objective function to find the minimum solution.

8

Conclusions

We have presented a static analysis for inferring the buffer bound of concurrent
programs communicating via buffered channels. We have cast the analysis as acapability calculus with fractional capabilities where capabilities can be passed
at channel communication point. Our analysis reduces the problem to linear
programming and runs in time polynomial in the size of the program.

References
1. J. Boyland. Checking interference with fractional permissions. In Static Analysis,
Tenth International Symposium, pages 55–72, San Diego, CA, June 2003.
2. K. Crary, D. Walker, and G. Morrisett. Typed memory management in a calculusof capabilities. In Proceedings of the 26th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 262–275, San Antonio, Texas,
Jan. 1999.

3. N. Kobayashi, M. Nakade, and A. Yonezawa. Static analysis of communication
for asynchronous concurrent programming languages. In Static Analysis, Second
International Symposium, pages 225–242, Glasgow, Scotland, Sept. 1995.
4. B. Steensgaard. Points-to analysis in almost linear time. In Proceedings of the
23rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, pages 32–41, St. Petersburg Beach, Florida, Jan. 1996.
5. T. Terauchi and A. Aiken. Witnessing side-effects. In 10th ACM SIGPLAN International Conference on Functional Programming, pages 105–115, Tallinn, Estonia,
Sept. 2005.
6. T. Terauchi and A. Aiken. A capability calculus for concurrency and determinism. In
Concurrency Theory, 17th International Conference, volume 4137, pages 218–232,
Bonn, Germany, Aug. 2006.

A

Proof of Theorem 1

Lemma 2. Suppose Γ ⊢ e : τ , Γ ⊢ h, and (h, e) ⇓ v. Then Γ ⊢ v : τ .
Proof. By induction on the type derivation.
Lemma 3. Suppose Γ, Ψ1 , . . . , Ψn , ΨB ⊢ (B, S, p1 ) and (B, S, p1 ) → (B ′ , S ′ , p2 ).
Then there exist Ψ1′ , . . . , Ψn′ , ΨB′ such that(a) Γ, Ψ1′ , . . . , Ψn′ , ΨB′ P⊢ (B ′ , S ′ , p2 )
Pn
n
′
′
′
(b) Let Ψp = ΨPB +j=1 Ψj . Then, for each channel
j=1 Ψj and Ψp = ΨB +P
′ ′′c, Ψp (ρ) + c′ ∈HCB′ (ρ,Γ ) |B (c )| ≤ Ψp (ρ) + c′ ∈HCB (ρ,Γ ) |B(c′ )| where ρ =hdl(Γ (c)).
Proof. The proof is by case analysis on (B, S, p1 ) → (B ′ , S ′ , p2 ). We just show
the key cases. First, note that (b) can be restated so that the statement is “foreach ρ, ...” instead of “for each c, ... where ρ = hdl(Γ (c)).” We use this form as
it is more convenient.
Consider the case (B, S, p1 ) → (B ′ , S ′ , p2 ) is an instance of Write, that is,(S(ij ), e1 ) ⇓ c(S(ij ), e2 ) ⇓ v
B ′ = B.write(c, v)(B, S, ij .e1 !(e2 ); s || p) → (B ′ , S, ij .s || p)Without loss of generality, let j = 1. We haveΓ ⊢ e1 : ch(ρ, τ, Ψ ′ )Γ ⊢ e2 : τ′Γ, Ψ1 ⊢ e1 !(e2 ) : Ψ1 − Ψ − 0 [ρ 7→ 1]

PLet Ψ1′ = Ψ1 −Ψ ′ −0 [ρ 7→ 1]. Let Ψj′ = Ψj for j 6= 1. Let ΨB′ = c∈dom(B ′ ) |B ′ (c)|×writeSend(Γ (c)). Then we have Γ, Ψ1′ , . . . , Ψn′ , ΨB′ ⊢ (B ′ , S, ij .s || p). Thus (a)holds.
PP
By Lemma 2, hdl(Γ (c)) = ρ. Let Ψp′ = ΨB′ + nj=1 Ψj′ and Ψp = ΨB + nj=1 Ψj .
Clearly, for ρ′ 6= ρ,X
X|B(c′ )||B ′ (c′ )| = Ψp (ρ′ ) +Ψp′ (ρ′ ) +c′ ∈HCB ′ (ρ′ ,Γ )c′ ∈HCB (ρ′ ,Γ )

Also, because ΨB′ + Ψ1′ = ΨB + Ψ1 − 0 [ρ 7→ 1] and |B ′ (c)| = |B(c)| + 1,
X
X
|B(c′ )||B ′ (c′ )| = Ψp (ρ) +Ψp′ (ρ) +c′ ∈HCB ′ (ρ,Γ )c′ ∈HCB (ρ,Γ )Thus (b) holds.
Consider the case (B, S, p1 ) → (B ′ , S ′ , p2 ) is an instance of Read, that is,(S(ij ), e) ⇓ c (B ′ , v) = B.read(c)S ′ = S[ij 7→ S(ij )[x 7→ v]](B, S, ij .e?(x); s || p) → (B ′ , S ′ , ij .s || p)Without loss of generality, let j = 1. We haveΓ ⊢ e : ch(ρ, Γ (x), Ψ ′ )Γ, Ψ1 ⊢ e?(x) : Ψ1 + Ψ ′ + 0 [ρ 7→ 1]
PLet Ψ1′ = Ψ1 +Ψ ′ +0 [ρ 7→ 1]. Let Ψj′ = Ψj for j 6= 1. Let ΨB′ = c∈dom(B ′ ) |B ′ (c)|×writeSend(Γ (c)). Then we have Γ, Ψ1′ , . . . , Ψn′ , ΨB′ ⊢ (B ′ , S ′ , ij .s || p). Thus (a)holds.
Pn
Pn
By Lemma 2, hdl(Γ (c)) = ρ. Let Ψp′ = ΨB′ + j=1 Ψj′ and Ψp = ΨB + j=1 Ψj .
Clearly, for ρ′ 6= ρ,X
X|B(c′ )||B ′ (c′ )| = Ψp (ρ′ ) +Ψp′ (ρ′ ) +c′ ∈HCB ′ (ρ′ ,Γ )c′ ∈HCB (ρ′ ,Γ )Also, because ΨB′ + Ψ1′ = ΨB + Ψ1 + 0 [ρ 7→ 1] and |B ′ (c)| = |B(c)| − 1,
X
X
|B(c′ )||B ′ (c′ )| = Ψp (ρ) +Ψp′ (ρ) +c′ ∈HCB ′ (ρ,Γ )c′ ∈HCB (ρ,Γ )Thus (b) holds.
Theorem 1.
PnSuppose Γ, Ψ1 , . . . , Ψn , ΨB ⊢ (B, S, p). Suppose hdl(Γ (c)) = ρ. Let
Ψ
=
Ψ
+
B
j=1 Ψj . Then the buffer bound of c in (B, S, p) is within Ψp (ρ) +
Pp
′
|B(c
)|.
c′ ∈HCB (ρ,Γ )Proof. Straightforward from Lemma 3.