Fencing off Go:
Liveness and Safety for Channel-Based Programming
Nicholas Ng

Bernardo Toninho

Nobuko Yoshida
Ar

tifact

eu

OPL *
* P se * Consi

* Easy to
ed
R
nt

arXiv:1610.08843v3 [cs.PL] 28 Feb 2017

at e d

Categories and Subject Descriptors D.1.3 [Programming Techniques]: Concurrent Programming; D.2.4 [Software Engineering]:
Software/Program Verification; D.3.1 [Programming Languages]:
Formal Definitions and Theory; F.3.2 [Semantics of Programming
Languages]: Program analysis
Keywords Channel-based programming, Message-passing programming, Process calculus, Types, Safety and Liveness, Compiletime (static) deadlock detection

1.

Introduction

Do not communicate by sharing memory;
instead, share memory by communicating
Go language proverb [5, 49]
Go is a statically typed programming language designed with explicit concurrency primitives at the forefront, namely channels and

Ev

Go is a production-level statically typed programming language
whose design features explicit message-passing primitives and
lightweight threads, enabling (and encouraging) programmers to
develop concurrent systems where components interact through
communication more so than by lock-based shared memory concurrency. Go can only detect global deadlocks at runtime, but provides no compile-time protection against all too common communication mismatches or partial deadlocks.
This work develops a static verification framework for bounded
liveness and safety in Go programs, able to detect communication
errors and partial deadlocks in a general class of realistic concurrent programs, including those with dynamic channel creation and
infinite recursion. Our approach infers from a Go program a faithful representation of its communication patterns as a behavioural
type. By checking a syntactic restriction on channel usage, dubbed
fencing, we ensure that programs are made up of finitely many different communication patterns that may be repeated infinitely many
times. This restriction allows us to implement bounded verification
procedures (akin to bounded model checking) to check for liveness
and safety in types which in turn approximates liveness and safety
in Go programs. We have implemented a type inference and liveness and safety checks in a tool-chain and tested it against publicly
available Go programs.

ll Docum
We
e

Abstract

A EC *

st

* Complete

*

t
en

*

Imperial College London, UK
{j.lange, nickng, b.toninho, n.yoshida}@imperial.ac.uk

alu

Julien Lange

goroutines (i.e. lightweight threads), drawing heavily from process
calculi such as Communicating Sequential Processes (CSP) [23].
Concurrent programming in Go is mostly guided towards channelbased communication as a way to exchange data between goroutines, rather than more classical concurrency control mechanisms
(e.g. locks). Channel-based concurrency in Go is lightweight, offering logically structured flows of messages in large systems programming [3, 54], instead of “messy chains of dozens of asynchronous callbacks spread over tens of source files” [4, 39].
On the other hand, Go inherits most problems commonly found
in concurrent message-passing programming such as communication mismatches and deadlocks, offering very little in terms of
compile-time assurances of correct structuring of communication.
While the Go runtime includes a (sound) global deadlock detector,
it is ultimately inadequate for complex, large scale applications that
may easily be undermined by trivial mistakes or benign changes to
the program structure [20, 40], nor can it detect deadlocks involving
only a strict subset of a program’s goroutines (partial deadlocks).
Liveness and Safety of Communication While Go’s type system
does ensure that channels are used to communicate values of the
appropriate type, it makes no static guarantees about the liveness
or channel safety (i.e. channels may be closed in Go, and sending
on a closed channel raises a runtime error) of communication in
well-typed code. Our work provides a framework for the static
verification of liveness and absence of communication errors (i.e.
safety) of Go programs by extracting concurrent behavioural types
from Go source code (related type systems have been pioneered
by [48] and [28], among others). Our types can be seen as an
abstract representation of communication behaviours in the given
program. We then perform an analysis on behavioural types, which
checks for a bounded form of liveness and communication safety
on types and study the conditions under which our verification
entails liveness and communication safety of programs.
1.1

Overview

We present a general overview of the steps needed to perform our
analysis of concurrent Go programs.
Prime Sieve in Go To illustrate the challenges in analysing Go
programs, we begin by considering a rather concise implementation of a concurrent prime sieve (Listing 1, adapting the example
from [43] to output infinite primes). This seemingly simple Go program includes intricate communication patterns and concurrent behaviours that are hard to reason about in general due to the combination of (1) unbounded iterative behaviour, (2) dynamic channel
creation and (3) spawning of concurrent threads.
The program is made up of three functions: Generate, that
given a channel ch continuously sends along the channel an increasing sequence of integers starting from 2 (encoded as a for
loop without an exit condition); Filter, that given a channel

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

package main
func Generate(ch chan<- int) {
for i := 2; ; i++ { ch <- i } // Send sequence 2,3...
}
func Filter(in <-chan int, out chan<- int, prime int){
for { i := <-in // Receive value from ’in’.
if i%prime != 0 { out <- i } // Fwd ’i’ if factor.
}
}
func main() {
ch := make(chan int) // Create new channel.
go Generate(ch) // Spawn generator.
for i := 0; ; i++ {
prime := <-ch
ch1 := make(chan int)
go Filter(ch, ch1, prime) // Chain filter.
ch = ch1
}
}

Listing 1. Concurrent Prime Sieve.

for inputs in, one for outputs out, and a prime, continuously
forwards a number from in to out unless it is divisible by
prime; and main, which assembles the sieve by creating a new
synchronous channel ch, spawning the Generator thread (i.e.
go f(x) spawns a parallel instance of f) with the channel ch,
and then iteratively setting up a chain of Filter threads, where
the first filter is connected to the generator and the next Filter,
and so on. We note that with each iteration, a new synchronous
channel ch1 is created that is then used to link each filter instance.
The program spawns an infinite parallel composition of Filter
threads, each pair connected by a dynamically created channel; and
the execution of Generator and the Filter processes in the
sieve is non-terminating.
Types of Prime Sieve Our framework infers from the prime sieve
program the type t0 given by:
g(x)
f (x, y)
r (x)
t0 ()

,
,
,
,

x; ghxi
x; (y; f hx, yi ⊕ f hx, yi)
x; (new b)(f hx, bi | rhbi)
(new a)(ghai | rhai)

The type is described as a system of mutually recursive equations,
where the distinguished name t0 types the program entry point.
This language is equivalent to a subset of CCS [36] with recursion,
parallel and name creation, for which deciding liveness or safety
is in general undecidable [7, 8]. The type t0 specifies that main
consists of the creation of a new channel a and the two parallel
behaviours ghai and r hai. The type given by equation g(x), which
types the generator, identifies the infinite output behaviour along
the given channel x. The type equation f (x, y) specifies the filter
behaviour: input along x and then either output on y and recurse or
just recurse. Finally, we decompose the topology set-up as r(x)
which inputs along x and then, through the creation of a new
channel b, spawns a filter on x and b and recurses on b, creating
an infinite parallel composition of filters throughout the execution
of the program.
Our type-level analysis relies on the fact that types are able to
accurately model a program’s communication behaviour. The analysis proceeds in two steps: a simple syntactic check on channel usage in types, dubbed fencing, and a symbolic finite-state execution
of fenced types.
Fenced Types Intuitively, if types are fenced, then during their execution there can only be a finite set of channels, or a fence, shared
by finitely many types (threads). Moreover, fencing ensures that recursive calls under parallel composition eventually involve only local names, shared between finitely many threads. This guarantees

that a program consists of finitely many different communication
patterns (that may themselves be repeated infinitely many times).
For instance, the recursive call to r hbi in the equation r(x) is
fenced, since the recursive instances of r will not know the channel
parameter x hence they cannot spawn threads which share x. This
restriction enforces a “finite memory” property wrt. channel names,
insofar as given enough recursive unfoldings all the parameters of
the recursive call will be names local to the recursive definition.
Symbolic Semantics and Bounded Verification Fenced types can
be symbolically executed as CCS processes in a representative
finite-state labelled transition system that consists of a bounded
version of the generally unrestricted type semantics. This enables
us to produce decision procedures for bounded liveness and safety
of types, which deems the type t0 as bounded live and safe. In the
finite control case, the bounded correctness properties and their
unbounded ones coincide. The approach is similar to bounded
model checking, using a bound on the number of channels in a type
to limit its execution.
From Type Liveness to Program Liveness The final step is to
formally relate liveness and safety of types to their analogues
in Go programs. For the case of safety, safety of types implies
safety for programs. For the case of liveness, programs typically
rely on data values to guide their control flow (e.g. in conditional
branches) which are abstracted away at the type level. For instance,
the Filter function only outputs if the received value i is not
divisible by the given prime, but the type for the corresponding
process is given by f (x, y) which just indicates an internal choice
between two behaviours. The justification for the liveness of t0 is
that the internal choice always has the potential to enable the output
on y (assuming a fairness condition on scheduling). However, it is
not necessarily the case that a conditional branch is “equally likely”
to proceed to the then branch or the else branch. In § 5, we define the three classes of programs in which liveness of programs
and their types coincide.
1.2

Contributions

We list the main contributions of our work: To define and then
show the bounded liveness and safety properties entailed by our
analysis, we formalise the message-passing concurrent fragment of
the Go language as a process calculus (dubbed MiGo). The MiGo
calculus mirrors very closely the intended semantics of the channelbased Go constructs and allows us to express highly dynamical
and potentially complex behaviours (§ 2); We introduce a typing
system for MiGo which abstracts behaviours of MiGo as a subset of
CCS process behaviours (§ 3); We define a verification framework
for our type language based on the notion of fences and symbolic
execution, showing that for fenced types our symbolic semantics
is finite control, entailing the decidability of bounded liveness and
channel safety (i.e. the notions of liveness and channel safety wrt.
the symbolic semantics – § 4); We characterise the MiGo programs
whose liveness and safety are derived from our analysis on types
(§ 5); We show that our results are systematically extended to
asynchronous communication semantics (§ 6); we describe the
implementation of our analysis in a tool that we use to evaluate
our approach against open-source, publicly available Go programs
(§ 7).
Our implementation and benchmark examples are available online [2].

2. MiGo: A Core Language for Go
This section introduces a core calculus that models the message
passing concurrency features of the Go programming language,
dubbed MiGo (mini-go). Beyond sending and receiving data values

P, Q

:=
|
|
|
|
|
|
|
|

π; P
close u; P
select{πi ; Pi }i∈I
if e then P else Q
newchan(y:σ); P
P |Q | 0
Xhẽ, ũi
(νc)P
chσi::ṽ | c? hσi::ṽ

u
π
v
e
D
P
σ

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

a | x
u!hei | u?(y) | τ
n | true | false | x
v | not(e) | succ(e)
X(x̃) = P
{Di }i∈I in P
bool | int | . . .

Figure 1. Syntax of MiGo.
along channels, the Go language supports three key concurrency
features:
FIFO Queues. Message-passing in Go is achieved via an abstract notion of a lossless, order-preserving communication channel, implemented as a (bounded) FIFO-queue. When the bound on
the queue size is 0, communication is fully synchronous, whereas
with strictly positive bounds the communication is asynchronous
(i.e. sending is non-blocking if a queue is not full and, dually, receiving is non-blocking if a queue is not empty). The bound is defined upon channel creation and cannot be changed dynamically.
Goroutines. Go supports lightweight threads, dubbed goroutines, which denote the spawning of a thread to execute a function
concurrently with the main control flow of a program. This feature can be modelled by a combination of parallel composition and
process definitions.
Select. The select construct in Go encodes a form of guarded
choice, where each branch is guarded by an input or an output on
some channel. When multiple branches can be chosen simultaneously, one is chosen at random (through pseudo-random number
generation). It is also possible to encode a “timeout” branch in such
a choice construct.
Our fencing-based analysis is oblivious to buffer sizes, hence
we first focus on fully synchronous communication for ease of
presentation, addressing bounded asynchrony in § 6.
2.1

Syntax of MiGo

The syntax of the calculus is given in Figure 1, where P, Q range
over processes, π over communication prefixes, e, e0 over expressions and x, y over variables. We write ṽ and x̃ for a list of expressions and variables, respectively (we use · as a concatenation
operator). Programs are ranged over by P, consisting of a collection of mutually recursive process definitions (ranged over by D),
parameterised by a list of (expression and channel) variables. We
omit a detailed enumeration of types such as booleans, floatingpoint numbers, etc., which are typed with payload types σ. fn(P )
and fv(P ) denote the sets of free names and variables. Process variables X are bound by definitions D of the form of X(x̃) = P
where fv(P ) ⊆ {x̃} and fn(D) = ∅. We use u to range over channel names a or variables x.
The language constructs are as follows: a prefixed (or guarded)
process π; P denotes the behaviour π (a send action of e on u,
u!hei, a receive action on u, bound to y, u?(y), or an internal action τ ) followed by process P ; a close process close u; P
closes the channel u and continues as P ; a selection process
select{πi ; Pi }i∈I denotes a choice between the several Pi processes, where each Pi is guarded by a prefix πi . Thus, the choice
construct non-deterministically selects between any process Pi
whose guarding action can be executed (note that a τ action prefix
can always be executed, cf. § 2.2); the standard conditional process
if e then P else Q, parallel process P | Q, and the inactive process
0 (often omitted); a new channel process newchan(y:σ); P creates

a new channel with payload type σ, binding it to y in the continuation P ; process call Xhẽ, ũi denotes an instance of the process
definition bound to X, with formal parameters instantiated to ẽ and
ũ. Both restriction (νc)P and buffers at channel c denote runtime
constructs (i.e. not written explicitly by the programmer), where
the former denotes the runtime handle c for a channel bound in P
and a buffer for an open channel chσi::ṽ, containing messages ṽ of
type σ, or a buffer for a closed channel c? hσi::ṽ. A closed channel cannot be used to send messages, but may be used for receive
operations an unbounded number of times.
Our representation of a Go program as a program P in MiGo,
written {Di }i∈I in P , consists of a set of mutually recursive process definitions which encode all the goroutines and functions used
in the program, together with a process P that encodes the program
entry point (i.e. the main).
2.1.1

Example – Prime Sieve in MiGo

To showcase the MiGo calculus, we present a concurrent implementation of the sieve of Eratosthenes that produces the infinite
sequence of all prime numbers.
The implementation relies on a generator process G(n, c) that
outputs natural numbers and a filter process F (n, i, o) that filters
out divisible naturals. The code for the generator and filter processes are given below as definitions:
G(n, c)
F (n, i, o)

,
,

c!hni; Ghn+1, ci
i?(x); if (x%n 6= 0) then o!hxi; F hn, i, oi
else F hn, i, oi

Definition G stands for the generator process: given the natural
number n and channel c, G(n, c) sends the number n along c and
recurses on n+1. Definition F stands for the filter: given a natural
n and a pair of channels i and o, F (n, i, o) inputs a number x along
i and sends it on o if x is not divisible by n, followed by a recursive
call. We then need a way to chain filters together, implementing the
sieve:
R(c)

,

c?(x); newchan(c0 :int); (F hx, c, c0 i | Rhc0 i)

The process defined above inputs from the previous element in the
chain (either a generator or a filter), creates a new channel which is
then used to spawn a new filter process in parallel with a recursive
call to R on the new channel. Putting all the components together
we obtain the program:
{G(n, c), F (n, i, o), R(c)} in newchan(c:int); (G(2, c) | R(c))
As we make precise in § 4.2, the execution of the processes
is fenced insofar it is always the case that channels are shared
(finitely) by a finite number of processes. For instance, name c
above is only known to G(k, c) and F (2, c, c0 ). This point is crucial
to ensure the feasibility of our approach.
2.1.2

Example – Fibonacci in MiGo

We implement a parallel Fibonacci number generator that computes
the nth number of the Fibonacci sequence.
Fib(n, c) , if (n ≤ 1) then c!hni else newchan(c0 :int);
(Fibhn−1, c0 i | Fibhn−2, c0 i | c0 ?(x); c0 ?(y); c!hx+yi)
The definition F ib(n, c) above tests if the given number n is less
than or equal to 1. If so, it sends n on c and terminates. Otherwise,
the process creates a new channel c0 , which is then used to run two
parallel copies of Fib for the two predecessors of n. The parallel
instances are composed with inputs on c0 twice which are then
added and sent along c. A sample program that produces the 10th
element of the Fibonacci sequence is given below:
{Fib(n, c)} in newchan(c:int); (Fibh10, ci | c?(u); 0)

[SCOM ]

e↓v
c!hei; P | c?(y); Q | chσi::∅ −
→ P | Q {v/y} | chσi::∅
σ

c?(y); P | c? hσi::∅ −
→ P {v /y} | c? hσi::∅
[CLOSE ]
close c; P | chσi::ṽ −
→ P | c? hσi::ṽ
[TAU ]
τ; P −
→P
c∈
/ fn(P )
[NEWC ]
newchan(y:σ); P −
→ (νc)(P {c/y} | chσi::∅)

[SCLOSE ]

[PAR ]

P −
→ P0
P |Q−
→ P0 | Q

[RES ]

P −
→ P0
(νc)P −
→ (νc)P 0

[STR ]

P ≡Q−
→ Q0 ≡ P 0
P −
→ P0

[SEL ]

π j ; Pj | P −
→R j∈I
select{πi ; Pi }i∈I | P −
→R

e ↓ true
if e then P else Q −
→P

[IFF ]

[IFT ]

[DEF ]

e ↓ false
if e then P else Q −
→Q

P {ṽ,c̃/x̃} | Q → R ei ↓ vi X(x̃) = P ∈ {Di }i∈I
X(ẽ, c̃) | Q−
→R

Structural Congruence
P |Q≡Q|P
P | (Q | R) ≡ (P | Q) | R P | 0 ≡ P
(νc)(νd)P ≡ (νd)(νc)P (νc)0 ≡ 0 (νc)chσi::ṽ ≡ 0
P | (νc)Q ≡ (νc)(P | Q) (c 6∈ fn(P )) (νc)c? hσi::ṽ ≡ 0
Figure 2. Reduction Semantics.

On the other hand, the following program should be deemed not
live since the outputs from the recursive calls are never sent to the
initial Fib bad call and so the answer is never returned to the main
process (i.e. c?(u); 0 can never fire).
Fib bad (n, c) , newchan(c0 :int);
(Fib bad hn−1, c0 i | Fib bad hn−2, c0 i | c0 ?(x); c0 ?(y); c!hx+yi)
2.2

2.3

Liveness and Channel Safety

We define a notion of liveness and channel safety for programs
through barbs in processes (Definition 2.1). Liveness identifies the
ability of communication actions to always eventually fire. Channel
safety pertains to the semantics of channels in Go, where closing a
channel more than once or sending a message on a closed channel
raises a runtime error.
A common pattern in the usage of select in Go is to introduce
a timeout (or default) branch, which we model as a τ -guarded
branch. This notion of timeout makes the definition of liveness
slightly challenging. Consider the following:
P1 , select{a!hvi, b?(x); 0 , τ ; Pt }
P2 , select{a!hvi, b?(x); 0}

A select with a branch guarded by τ contains a branch that is always
enabled by default (since τ actions can always fire silently). Hence
if the continuation of the τ prefix Pt is live, then P1 is live. On the
other hand, P2 by itself cannot be live. For P2 to be live, it must be
composed with a process that can offer an input on a or an output
on b, with respective live continuations. Hence P2 | R1 is live.
However, P1 | Ri is not live unless Pt | Ri is live (i ∈ {1, 2}).
Accounting for these features, we formalise safety and liveness
properties, extending the notion of barbed process predicates [38].
Most of the definitions are given in a standard way, with some
specifics due to the ability to close channels: input barbs P ↓a ,
denoting that process P is ready to perform an input action on the
free channel name a; output barbs P ↓a are dual; a synchronisation
barb P ↓[a] , indicating that P can perform a synchronisation on a;
a channel close barb P ↓end[a] , denoting that P can close channel
a; and P ↓a? , denoting that P may send from closed channel
a. We highlight the predicate P ↓õ , where õ is a set of barbs,
which applies only for the select construct, stating that the barbs
of select{πi ; Pi }i∈I are those of all the processes that make up the
external choice, provided that all of them can exhibit a barb.
Definition 2.1 (Barbs). We define the predicates π ↓o , P ↓o and
P ↓õ with o, oi ∈ {a, a, [a], end[a], a? }.
c?(x) ↓c

c!hei ↓c

Operational Semantics

The semantics of MiGo, written P −
→ Q, is defined by the reduction rules of Figure 2, together with the standard structural congruence P ≡ Q (which includes ≡α ). For process definitions, we
implicitly assume the existence of an ambient set of definitions
{Di }i∈I . Our semantics follows closely the semantics of the Go
language: a channel is implemented at runtime by a buffer that is
open or closed. Once a channel is closed, it may not be closed again
nor can it be used for output. However, a closed channel can always
be the subject of an input action, where the received value is a bottom element of the corresponding payload data type. For now, we
impose a synchronous semantics (represented in Go with channel
of size 0), see § 6 for the asynchronous semantics.
Rule [SCOM ] specifies a synchronisation between a send and a
receive. Rule [SCLOSE ] defines inputs from closed channels, which
according to the semantics of Go are always enabled, entailing the
reception of a base value v σ of type σ. Rule [CLOSE ] changes the
state of a buffer from open (chσi::ṽ) to closed (c? hσi::ṽ). Rule
[NEWC ] creates a fresh channel c, instantiating it accordingly in the
continuation process P and creating the buffer for the channel.
Rule [SEL ] encodes a mixed non-deterministic choice, insofar as any
subprocess Pj that can exhibit a reduction may trigger the choice.
The rule [DEF ] replaces X by the corresponding process definition
(according to the underlying definition environment), instantiating
the parameters accordingly. The remaining rules are standard from
process calculus literature [46].

R1 , a?(y); 0
R2 , c?(y); 0

P ↓o
P | Q ↓o

π ↓o
π; Q ↓o

close c; Q ↓end[c] c? hσi::~v ↓c?

P ↓o a 6∈ fn(o)
(νa)P ↓o

P ↓o

P ≡Q
Q ↓o

Q {ẽ,ã/x̃} ↓o X(x̃) = Q
Xhẽ, ãi ↓o
∀i ∈ {1, .., n} : πi ↓oi
select{πi ; Pi }i∈{1,..,n} ↓{o1 ...on }

P ↓a

Q ↓a or Q ↓a?
P | Q ↓[a]

P ↓a πi ↓a
P ↓a or P ↓a? πi ↓a
P | select{πi ; Qi }i∈I ↓[a] P | select{πi ; Qi }i∈I ↓[a]
P ⇓o if P −
→∗ P 0 and P 0 ↓o with o ∈ {c, c, [c], end[c], c? }.
For example, we have that ¬(P1 ↓a ) for any a, whereas P2 ↓a,b .
Note that (P1 | R1 ) ↓[a] and (P2 | R1 ) ↓[a] ; and if Pt ↓o then
P1 ⇓o and if Pt ↓c then P1 | R2 ⇓[c] .
We may now define liveness and channel safety: a program
is live if, for all the reachable process states, (a) if the state can
perform an input or output action on a channel, the state can also
eventually perform a synchronisation on that channel; and, (b) if a
state can perform a set of actions (i.e. a select where all its guards
are non-τ ), the state can also eventually synchronise on one of the
action prefixes.
Definition 2.2 (Liveness). The program P satisfies liveness if for
all Q such that P −
→∗ (νc̃)Q:

T, S
T

:=
|
:=

κ; T | ⊕{Ti }i∈I | N{κi ; Ti }i∈I | (T | S) | 0
(new a)T | end[u]; T | tX hũi | (νa)T | bac | a?
κ := u | u | τ
{tXi (ỹi ) = Ti }i in S

The recursive process defined by X(c) receives a potentially unbounded number of positive integers, stopping when the received
value x is less than 0. To type such a commonplace programming
pattern, we allow the branches in the conditional to hold different
types (which are also incompatible by the usual branch subtyping).

Figure 3. Syntax of Types.
(a) If Q ↓a or Q ↓a then Q ⇓[a] .
(b) If Q ↓ã then Q ⇓[ai ] for some ai ∈ {ã}.
Channel safety states that in all reachable program states, channels are closed at most once and no process performs outputs on
closed channels, as specified by the semantics of the Go language.
Definition 2.3 (Channel Safety). The program P is channel safe
if for all Q such that P −
→∗ (νc̃)Q, if Q ↓a? then ¬(Q ⇓end[a] ) and
¬(Q ⇓a ).

3.

A Behavioural Typing System for MiGo

Go’s channel types are related to those of the π-calculus, where the
type of a channel carries the type of the objects that threads can
send and receive along the channel. Our typing system augments
Go’s channel types by also serving as a behavioural abstraction of
a valid MiGo program, where types take the form of CCS processes
with name creation.
3.1

Syntax of Types

The syntax of types T, S is given in Figure 3, mirroring closely
that of MiGo processes: The type κ; T denotes an output u, input
u along channel u, or an explicit τ action (often used to encode
timeouts in external choices), followed by the behaviour denoted
by type T . The type ⊕{Ti }i∈I represents an internal choice between the behaviours Ti , whereas N{κi ; Ti }i∈I denotes an external choice between behaviours Ti , respectively guarded by prefixes
κi which drive the choice. Types include parallel composition of
behaviours T | S, inaction 0 and channel creation (new a)T (binding a in T ). The type end[u]; T denotes the closing of channel u
followed by the behaviour T . The type variable tX hũi associated to
a process variable X, denotes the behaviour bound to variable tX
in the definition environment, with formal parameters instantiated
to ũ. The type {tXi (ỹi ) = Ti }i in S codifies a set of (parameterised) mutually recursive type definitions tXi (ỹi ) = Ti , bound
in S. This set of equations denoted by T is the type assigned to
top-level programs P.
The type constructs (νa)T , bac and a? denote the type representations of runtime channel bindings, open and closed buffers,
respectively. We write fn(T ) and fv(T ) for the free names and variables of type T , respectively; and n(T ) denotes the set of bound and
free names.
3.2

Typing System

We first explain the two essential differences from (linear or
session-based) type systems of the π-calculus [27, 28, 48]:
Sharing of Channels. We do not enforce linear (disjoint) channel usages, allowing processes to have races. For instance, the process below (with shared y) is typable:
newchan(y:bool); (y!htruei; 0 | y!hfalsei; 0 | y?(x); 0)
Conditionals. We do not enforce the same types of both
branches of the conditional. This design choice stems from the
fact that most real programs make use of conditionals precisely to
identify points where behaviours need to be different. For instance,
consider the following definition:
X(c) = c?(x); if x ≥ 0 then Xhci else 0

Process Typing The judgement (Γ ` P I T ) for processes is
defined in Figure 4 where Γ is a typing environment that maintains
information about channel payload types, types of bound communication variables and recursion variables, P is a process and T a
behavioural type.
We write Γ ` J for J ∈ Γ and Γ ` e : σ to state that the
expression e is well-typed according to the types of variables in
Γ. We write u:ch(σ) to denote that u stands for a channel with
payload type σ. We omit the typing rules of expressions e, given
that expressions only include basic data types. We write dom(Γ)
for the set of channel bindings in Γ.
The rules implement a very close correspondence between processes and their respective types: Rule hOUTi types output processes
with the output prefix type u; T , checking that the type of the object to be sent matches the payload type σ of channel u, and that
the continuation P has type T . The rule hINi for inputs is dual.
Rule hSELi types the select construct with the external choice type,
whereas rule hIFi types the conditional as a binary internal choice
between the type S corresponding to P and the type T corresponding to Q.
The typing rules for close, zero, parallel and τ are straightforward. Rule hNEWi allocates a fresh type-level channel name with
payload type σ. Rule hVARi matches a process variable with its
corresponding type variable, checking that the specified arguments
have the appropriate types.
Program Typing The judgement (Γ ` P I T ) is defined in
Figure 4. A process declaration X(x̃:σ̃, ỹ:ch(σ̃ 0 )) = P is matched
with tX (ỹ) = T , connecting the process level variable X with the
type variable t, where P may use any of the parameters specified in
the recursion variable. The typing rule for programs hDEFi assigns
a program the type {tXi (ỹi ) = Ti }i∈I in S, checking that each
definition is typed with tXi (ỹi ) = Ti and that the main process Q
has type S.
Runtime Process Typing The judgement (Γ `B P I T ) types
a process created after execution of a program (called runtime
process). B is a set of channels with associated runtime buffers
to ensure their uniqueness. Runtime channel bindings are typed by
rule hRESi, where given a process of type T that can use the buffered
channel c, we type (νc)P with (νc)T removing c from the set s
since it is local to P (and T ). Closed and open buffers are typed by
rules hCBUFFi and hBUFFi, respectively, noting that the set of active
buffers is a singleton containing the appropriate buffer reference.
The parallel rule hPARRi ensures that the buffers of both processes
do not overlap (hence only a single buffer for each name exists in
the context).
Notation 3.1. In the remainder of this paper, we refer to the type of
a program as a system of type equations T which is obtained from
the program by collecting all the types for definitions and adding
a distinguished unique definition t0 () = S for the program entry
point. We often write X0 to stand for the process variable of the
program entry point.

4.

Bounded Verification of Behavioural Types

This section introduces our main definition, fencing, and a bounded
verification of liveness and channel safety for types. Our development consists of the following steps:

Γ`P IT

Γ ` u:ch(σ) Γ, x:σ ` P I T
hINi
Γ ` u?(x); P I u; T

|SEL|

Γ`P IT
hTAUi
Γ ` τ; P I τ; T

Γ`P IT
Γ ` close u; P I end[u]; T

hSELi

hIFi

hZEROi

Γ`0I0

Γ, y:ch(σ) ` P I T c 6∈ dom(Γ) ∪ fn(T )
hNEWi
Γ ` newchan(y:σ); P I (new c)T {c/y}

Γ`PIT
Γ, Xi (σ̃i , ch(σ̃i0 )), x̃i :σ̃i , ỹi :ch(σ̃i0 ) ` Pi I Ti
Γ, X1 (σ̃1 , ch(σ̃10 )), ..., Xn (σ̃n , ch(σ̃n0 )) ` Q I S
hDEFi
Γ ` {Xi (x˜i , y˜i ) = Pi }i∈I in Q I {tXi (ỹi ) = Ti }i∈I in S
Γ `B P I T
Γ`P IT
hINTi
Γ `∅ P I T
hCBUFFi

hRESi

Γ ` a:ch(σ)
Γ `{a} a? hσi::ṽ I a?

hPARRi

Γ, c:ch(σ) `B P I T
Γ `B\c (νc)P I (νc)T
hBUFFi

Γ ` a:ch(σ)
Γ `{a} ahσi::ṽ I bac

Γ `B P I T Γ `B 0 Q I S B ∩ B 0 = ∅
Γ `B∪B 0 P | Q I (T | S)

Figure 4. Typing Rules (Processes and Programs).

Step 1. Define a syntactic restriction on types, dubbed a fence,
guaranteeing that whenever fenced types model a program that
spawns infinitely many processes, the program actually consists of finitely many communication patterns (which may be
repeated infinitely many times).
Step 2. Define a symbolic semantics for types, which generates
a representative finite-state labelled transition system (LTS)
whenever types validate the fencing predicate.
Step 3. Prove that liveness and channel safety are decidable for the
bounded symbolic executions of fenced types.
4.1

Types as Processes: Semantics

The semantics of our types is given by the labelled transition system
(LTS), extending that of CCS, defined in Figure 5. The labels,
ranged over by α and β, have the form:
α, β := a | a | τ | [a] | end[a] | end[a] | a?
Labels denote send and receive actions (a and a), silent transitions
τ , synchronisation over a channel [a], the request and acceptance

τ

β

0

T |S−
→T |S

a? −→ a?

a?

α

|RES -1|

T −
→ T0

|END|

T −
→T

end[a]

S −−−→ S 0

τ

T |S−
→ T 0 | S0
[a]

|RES -2|

α

00

end[a]

T −−−→ T 0

α

0 α

β = a, a?

end[a]; T −−−→ T

end[a]

|CLOSE|

fn(α) 6= {a}

T −
→ T 00

a

S−
→ S0
[a]

(νa)T −
→ (νa)T 0

T ≡α T 0

α

N{κi ; Ti }i∈I −
→ Tj
T | S −→ T 0 | S 0

end[a]

|CLD|

→ Tj
κj ; Tj −

T −
→ T0

τ

bac −−−→ a?

|EQ|

|COM|

(new a)T −
→ (νa)(T | bac)

|BUF|

Γ`P IT Γ`QIS
hPARi
Γ ` P | Q I (T | S)
Γ ` ẽ:σ̃ Γ ` ũ:ch(σ̃ 0 )
hVARi
Γ, X(σ̃, ch(σ̃ 0 )) ` Xhẽ, ũi I tX hũi

|BRA|

⊕{Ti }i∈I −
→ Tj
α

τ

τ; T −
→T

|TAU|
α

j∈I

T −
→ T0

|NEW|

Γ ` πi ; Pi I κi ; Ti
Γ ` select{πi ; Pi }i∈I I N{κi ; Ti }i∈I

Γ ` e : bool Γ ` P I S Γ ` Q I T
Γ ` if e then P else Q I ⊕{S , T }

a

a; T −
→T

|RCV|

α

|PAR|
hCLOSEi

a

→T
a; T −

|SND|

Γ ` u:ch(σ) Γ ` e : σ Γ ` P I T
hOUTi
Γ ` u!hei; P I u; T

T −→ T 0
τ

(νa)T −
→ (νa)T 0
α

|DEF|

T {ã/x̃} −
→ T0

t(x̃) = T

α

thãi −
→ T0

Figure 5. LTS Semantics of Types.

of channel closure (end[a] and end[a]), and send actions from a
closed channel a? . We write t(x̃) = T if t(x̃) = T is in T .
Rule |SND| (resp. |RCV|) allows a type to emit a send (resp.
receive) action on a channel a. Rules |SEL| and |BRA| model internal
and (mixed) external choices, respectively. Rule |COM| allows two
types to synchronise on a dual action (send with receive, or closed
channel with receive). Rule |NEW| creates a new (open) channel for
a. Rule |END|, together with rule |CLOSE|, allows a type to request
the closure of channel a. Rule |BUF| models a transition from an
open channel to a closed one, and rule |CLD| models the perpetual
ability of a closed channel to emit send actions. The other rules are
standard from CCS. In Figure 5, we omit the symmetric rules for
|CLOSE|, |PAR|, and |COM|. We define structural congruence rules over
types as follows:
T | S ≡ S | T T | (T 0 | S) ≡ (T | T 0 ) | S T | 0 ≡ T
(νa)(νb)T ≡ (νb)(νa)T (νa)0 ≡ 0 (νa)a? ≡ 0 (νa)bac ≡ 0
0
0
T | (νa)S ≡ (νa)(T | S) (a ∈
/ fn(T )) T ≡α T ⇒ T ≡ T
α

τ

→ ∪ ≡ and T −
→∗ −
→ if there exist T 0 and T 00
We write −
→ for −
α
such that T −
→∗ T 0 −
→ T 00 .
4.2

Fenced Types and Fencing Predicate

This section develops Step 1 by defining the fencing predicate. We
illustrate the key intuitions with an example.
Recall the prime sieve program (§ 2.1.1) given in § 1.1, as
inferred by the type system of § 3. We represent the execution wrt.
the semantics of § 4.1, via the diagram below.
t0hi

g ha0i f ha0, a1i f ha1, a2i

...

r ha0i

...

r ha1i

r ha2i

f hak−1, ak i f hak , ak+1i
r hak i

r hak+1i

...

...

In the diagram, a node represents an instance of a concurrently
executing type (or thread) and the arrows represent the parent-child
relation. For instance, t0 hi is the parent of gha0 i and rha0 i.
We observe that there are only finitely many kinds of concurrent
threads (i.e. t0 hi, ghai, f ha, bi, and rhai). Also given any name in
the diagram, e.g. a1 , it is shared only by finitely many threads. For
instance, a1 is “known” only to f ha0 , a1 i, f ha1 , a2 i, and rha1 i.
Note that this situation does not change during the execution of the
program because (1) types cannot exchange names in communi-

G ; ỹ ; z̃ `t T
bAXIOMc

bENDc

ỹ 6= ε ∨ ũ ≺ z̃
G ; ỹ ; z̃ `t thũi

∆ `t 0

bPARc

bDEF -∈c

shũi ∈ G
G ; ỹ ; z̃ `t shũi

G ; ε ; z̃ · ỹ `t T1 G ; ε ; z̃ · ỹ `t T2
G ; ỹ ; z̃ `t T1 | T2

t 6= s shũi ∈
/ G G · shũi ; ỹ ; z̃ `t T {ũ/x̃} s(x̃) = T
bDEF -∈c
/
G ; ỹ ; z̃ `t shũi
bSELc

bENDc

∀i ∈ I : ∆ `t Ti
∆ `t ⊕{Ti }i∈I

∆ `t T
∆ `t end[u]; T

bRESc

bBRAc

∀i ∈ I : ∆ `t Ti
∆ `t N{Ti }i∈I

∆ `t T
∆ `t (new a)T

bPREFc

∆ `t T
∆ `t κ; T

Figure 6. Rules for Fencing, where ∆ stands for G ; ỹ ; z̃.
cation and (2) the grand-children of, e.g. r ha1 i, do not know a1 ,
hence they cannot spawn further threads sharing that name.
Intuitively, we can observe that despite the fact that the prime
sieve generates an unbounded number of fresh channels and
threads, it consists of finitely many different communication patterns (i.e. the coloured regions above). It is this general pattern that
we capture with fencing.
4.2.1

Fencing Types

We introduce a judgement which ensures that a system of types is
fenced: given a finite set of names called fence, the types executing within that fence approximate a form of finite control. We use
judgements of the form G ; ỹ ; z̃ `t T to guarantee that a type definition t(x̃) = T is fenced; where G records previously encountered
recursive calls, ỹ represents the names that t can use if T is singlethreaded, and z̃ represents the names that a sub-term of T can use
if T is a multi-threaded type. We write ε for the empty environment. The judgement G ; ỹ ; z̃ `t T holds if it can be inferred by
the rules of Figure 6, which use a relation on sequences of names
that ensures a strictly decreasing usage of names, defined below.

is a parallel composition within T ), hence for each occurrence of a
t-recursion, at least one of the parameters must be forgotten. In the
prime sieve example, the types g(x) and f (x, y) always recurse on
the same parameters, but they do not include parallel composition.
While the type r(x) has a parallel composition, its parameter x is
“forgotten” at the rhbi recursive call (i.e. b ≺ x).
4.2.2

Examples on Fencing

No Fence We now give an example that does not validate the
fencing predicate. The types below model a program that spawns a
reader and a writer on a channel a infinitely many times.
w (x) , x; w hxi = Tw
r (x) , x; r hxi = Tr

We have: ε ; x ; ε `w Tw , ε ; x ; ε `r Tr , and ε ; ε ; ε `t0 T0
hold (since they do not feature any parallel composition). However,
ε ; x ; ε `t1 T1 does not hold. This is due to the fact that the axiom
bAXIOMc cannot be applied (i.e. ¬(x ≺ x)).
The topology induced by the type is given as:
t0 hi

Definition 4.2 (Fenced types). We say T is fenced (denoted by
Fenced(T )) if for all t(x̃) = T in T , either x̃ = ε or ε ; x̃ ; ε `t T
holds.
A consequence of fencing is that for each equation t(x̃) = T
such that x̃ 6= ε, either (1) T is single-threaded (i.e. there is no
parallel composition within T ), hence there is no restriction as to
the parameters t recurses on; or (2) T is multi-threaded (i.e. there

t1 hai
w hai

t1 hai

r hai w hai

t1 hai

r hai

w hai

r hai

We can observe that there are infinitely many instances of types that
“know” the name a.
Fibonacci Below, we give the types for the Fibonacci example,
cf. § 2.1.2.
fib(x)
t0 ()

,
,

x ⊕ (new b)(fibhbi | b; b; x | fibhbi)
(new a)(fibhai | a)

= Tfib
= T0

Observe that t0 () is trivially fenced since it has no parameter (cf.
Definition 4.2). The judgement ε ; x ; ε `fib Tfib also holds since
we have b ≺ x. Essentially, the equation fib validates the fencing
predicate because each recursively spawned child does not have
access to the parameter x. We illustrate the behaviour of this type
in the diagram below.
t0 hi

Definition 4.1 (≺-relation). We write ũ ≺ x̃ iff (1) x̃ = x1 · · · xn ,
(2) ũ = xk+1 · · · xn · a1 · · · ak , with k ≥ 1, and (3) ∀1 ≤ i ≤ n :
∀1 ≤ j ≤ k : xi 6= aj .
The relation ≺ enforces that types featuring parallel composition
have a “finite memory” wrt. the names over which they can recurse.
For instance, yza ≺ xyz, but xaz 6≺ xyz.
We comment on the key rules of Figure 6. Rule bPARc identifies
multi-threaded types by moving the ỹ environment to the z̃ environment. The axiom bAXIOMc states that thũi is fenced if either (i)
ỹ 6= ε, i.e. the type corresponding to t does not contain any parallel
composition; or (ii) ũ ≺ z̃ holds, i.e. any recursive call over t uses
strictly fewer (non newly created) names. The second part of the
premise guarantees that after a certain number of recursive calls,
the type t will have completely “forgotten” the names it started executing with; hence moving outside of the fence. Rules bDEF -∈c and
bDEF -∈c
/ deal with recursive calls to different type variables.

t1 (x) , w hxi | r hxi | t1 hxi = T1
t0 () , (new a)(t1 hai) = T0

fib hai
fib hb1 i
fib hb2 i

b1 ; b1 ; a

a
fib hb1 i

fib hb2 i b2 ; b2 ; b1 b3 ; b3 ; b1 fib hb3 i

fib hb3 i

Two fences are highlighted in the diagram: the {a}-fence includes
four parallel types (including the initial t0 ); while the {b1 }-fence
includes five components: one instance of fib(x) as well as two
of its recursive children and three instances of the non-recursive
component of fib.
4.3

Symbolic Semantics

For Step 2, we introduce a symbolic semantics for types, which is
parameterised by a bound on the number of free names that can be
used when unfolding a recursive call, e.g. thũi, by its corresponding definition. The overall purpose of the symbolic semantics is
that for any T such that Fenced(T ), the symbolic LTS of T is finite
state.
The symbolic semantics for types is given in Figure 7, where we
show only the interesting new rules. The other rules are essentially
those of Figure 5, with the additional parameters k and N as
expected. Rule |DEF| replaces its counterpart from Figure 5, while

∀i ∈ {1, . . . , n} : κi ↓oi
N{κi ; T }i∈{1,...,n} ↓{o1 ...on }

α

|DEF|

N C T {ã/x̃} −
→k N C T 0 t(x̃) = T ã ∩ N 6= ∅
α

N C thãi −
→k N C T 0

T ↓a κi ↓a
T | N{κi ; Si }i∈I ↓[a]

α

|R 1<|

N ] {a} C T −
→k N ] {a} C T 0 fn(α) 6= {a} |N | < k
α

N C (νa)T −
→k N C (νa)T 0
[a]

|R 2<|

N ] {a} C T −→k N ] {a} C T 0
α

|R 1≥|

|N | < k

τ

N C (νa)T −
→k N C (νa)T 0

N CT −
→k N C T 0

fn(α) 6= {a}
α

N C (νa)T −
→k N C (νa)T
[a]

|R 2≥|

N C T −→k N C T 0

|N | ≥ k
0

T ↓a

T 0 ↓a or T 0 ↓a?
T | T 0 ↓[a]

T ↓a or T ↓a? κi ↓a
T | N{κi ; Si }i∈I ↓[a]

Given k ∈ N, we write T ⇓ko if N C T −
→∗n N C T 0 and T 0 ↓o ,
with N = fn(T ), n = k + |N | and o ∈ {a, a, [a], end[a], a? }.
Observe that the predicate T ⇓ko is defined wrt. the symbolic
semantics. We write T ⇓o if T ⇓∞
o .
Definition 4.4 (Liveness). The system T satisfies k-liveness if for
all T such that ∅ C t0 hi −
→∗k ∅ C (νã)T ,
(a) If T ↓a or T ↓a then T ⇓k[a] .
(b) If T ↓ã then T ⇓k[ai ] for some ai ∈ ã.

|N | ≥ k

τ

→k N C (νa)T 0
N C (νa)T −

If T is ∞-live, then we say that T is live.

Figure 7. Symbolic Semantics for Types.

Consider the type equations below, where the reduction of t0 hi
leads to terms that are not k-live, for any k ≥ 0.

rules [R 1<] and |R 1≥| replace rule |RES -1|, and rules |R 2<| and |R 2≥|
replace |RES -2|.
In a term N C T , N can be seen as a subset of the free names
of T . Whenever a new name is encountered, e.g. through (νa)T ,
a is recorded in N as long as N has less than k elements. Rule
|DEF| states that a recursive call can only be unfolded if some of its
parameters are in N . Note that, in rule |DEF|, we assume that the
unfolding of a type is such that there is no clash with the names in
N.
α
For k ≥ 0, we write N C T −
→∗k −
→k if there exist T 0 and T 00
0 α
∗
→k N C T 00 .
such that N C T −
→k N C T −
We consider a fragment of the prime sieve example and show
its behaviour according to the symbolic semantics, with k = 1. We
have:
{a} C (νb)(ghai | f ha, bi | r hbi)

t1 (x) , (new b)(t1 hbi | b; x) t0 () , (new a)(t1 hai | a)
Intuitively, the system is not live since it is not possible to find a
synchronisation for, e.g. the receive action on a, within bounded
unfolding.
The definition of channel safety follows the same structure as
that of liveness.
Definition 4.5 (Channel Safety). The system T satisfies k-channel
safety if for all T such that ∅ C t0 hi −
→∗k ∅ C (νã)T , if T ↓a? then
¬(T ⇓kend[a] ) and ¬(T ⇓ka ).
If T is ∞-safe, then we say that T is channel safe.
Example We illustrate the need of a sufficiently large bound to
detect liveness errors with an example. Consider a variation of the
Prime Sieve example with a non-recursive filter:
f (x, y)

[a]

−
→∗1 −→1 {a} C (νb)(ghai | b; f ha, bi | r hbi)
at this point the process is stuck. The sub-term b; f ha, bi awaits to
synchronise on b, however the dual action on b is “hidden” in the
unfolding of rhbi, which cannot be unfolded by rule |DEF| since
b∈
/ {a} and, since k = 1, b cannot be added to the set of names. If
we set the bound to k = 2:
[b]
−
→∗2 −→2

4.4

{a, b} C ghai | f ha, bi | (new c)(f hb, ci | rhci)

Liveness and Channel Safety for Types

Following § 2.3, we define liveness and channel safety properties
for types. The definitions of liveness and channel safety rely on
barbs. The predicate T ↓a (resp. T ↓a ) denotes a type ready to
send (resp. receive) over channel a. Barb T ↓end[a] denotes a type
ready to close channel a and barb T ↓a? denotes a closed channel.
Barb T ↓[a] denotes a synchronisation over channel a. Barb T ↓õ
denotes a type that is waiting to synchronise over the actions in õ.
Definition 4.3 (Type Barbs). We define the predicates κ ↓o , T ↓o
and T ↓õ with o, oi ∈ {a, a, [a], end[a], a? }.
a ↓a

a ↓a
T ↓o
T | T 0 ↓o

κ ↓o
κ; T ↓o

end[a]; T ↓end[a]

T ↓o a ∈
/ fn(o)
(νa)T ↓o

T ↓o T ≡ T 0
T ↓o

T {ã/x̃} ↓o t(x̃) = T
thãi ↓o

a? ↓a?

x; y; x; y; x; y; x; y; 0

with g(x), r(x), and t0 () as in § 1.1. The system above is 2-live,
but not 3-live. A bound of 2 is too small to allow the symbolic
semantics to explore all the states of f (x, y); while a bound of 3
enables spawning another filter process, hence to explore all the
states of f (x, y).
4.5

{a, b} C ghai | b; f ha, bi | rhbi

,

Decidability of the Bounded Verification

We show that k-liveness and k-channel safety are decidable, noting
that these are defined wrt the symbolic semantics (Step 3).
The decidability result mainly follows from fencing, which ensures finite control over the symbolic semantics. The key idea is to
show that the set of non-equivalent terms reachable by the symbolic
semantics is finite. This is formalised below.
Lemma 4.1 (Finite Control). If Fenced(T ), then the set
{[T ]≡ | ∅ C t0 hi −
→∗k ∅ C T } is finite, for any finite k.
The crux of the proof is to show that the number of occurrences
of a type variable t is bounded in the maximal unfolding of a term
up-to a given set of names N . That is, an unfolding which unfolds
a term thãi only if ã ∩ N 6= ∅.
Theorem 4.1 (Decidability). For all T s.t. Fenced(T ), it is decidable whether or not T is k-live (resp. channel safe), for any k ≥ 0.
Theorem 4.1 follows from the fact that checking k-liveness
(resp. channel safety) is decidable over any finite LTS (finiteness
is guaranteed by Lemma 4.1).
Remark 4.1. It is not always possible to compute a finite k such
that k-liveness (resp. k-channel safety) implies general liveness

(resp. channel safety) of fenced types. However, if the types are
finite control (i.e., parallel composition does not appear under recursion), then liveness and channel safety are indeed decidable, see
e.g. [15].

Properties of MiGo

5.

We now make precise the properties our behavioural type analysis ensures on MiGo programs. We show that if a program P is
typed by a safe type, then P is safe according to Definition 2.3.
For liveness, we identify the classes of programs for which liveness of types implies program liveness. We note that type liveness
and safety refers to ∞-liveness and ∞-safety, respectively. Moreover, we recall that our bounded analysis on types implies its ∞counterpart only in the finite control fragment.
5.1

Type and Channel Safety in MiGo

The typing system of § 3 ensures that channel payloads always have
the expected type. This property is made precise by a standard subject reduction result, stating that the semantics of types simulates
the semantics of processes.
Theorem 5.1 (Subject Reduction). Let Γ `B P I T and P −
→
P 0 . Then there exists T 0 such that Γ `B 0 P 0 I T 0 with T −
→ T 0.
We prove that type safety implies program safety, using a correspondence between barbs. Hereafter we write P ⇓o including the
case o = ã.
Lemma 5.1. Suppose Γ `B P I T . If P ⇓o then T ⇓o .
Theorem 5.2 (Process Channel Safety). Suppose Γ ` P I T and
T is safe. Then P is safe.
5.2

Liveness of Limited Programs

The development in § 4 performs an analysis on our abstract representation of processes (i.e. the types), verifying liveness (Definition 4.4) for fenced types. Our goal is to ensure liveness of a general
class of typable programs. We divide programs into three classes to
discuss the issue of liveness.
The first class is a set of programs which have a path to terminate. In this class, a program that is typable with a live type can
always satisfy liveness.

respectively. Despite this program executing forever, both program
and type liveness hold. This class of programs is made precise in
Proposition 5.2, along with the issue of infinitely occurring conditionals, which are explained below.
5.3

Liveness of Infinitely Occurring Conditionals

As the third class, we consider infinitely running programs that
contain recursive variables in conditional branches. The behaviours
of conditionals in a program rely on data to decide which branch
is taken. On the other hand, at the type level, this information is
abstracted as an internal choice. This causes a mismatch between
program and type behaviours.
Revisiting the prime sieve example of § 2.1.1, consider the
definition of the filter process:
F (n, i, o)

,

i?(x); if (x%n 6= 0) then o!hxi; F hn, i, oi
else F hn, i, oi

whose type is given as: tF (i, o) = i; ⊕{o; tF hi, oi, tF hi, oi}.
Our analysis on types does indeed determine the types of the
prime sieve as live, even in the absence of terminating reduction sequences. In tF (i, o), we have an internal choice between a branch
that recurses back to tF and another that outputs along o and recurses back to tF . Thus, if we compose a call tF with a type that
denotes an infinite sequence of inputs along o, we deem such a
composition as live since all the inputs can eventually be synchronised with an output from tF , given that the semantics of internal
choice state that we may indeed move to either branch.
However, the type T of the prime sieve program is an abstract
approximation of the actual prime sieve implementation, where
the test x%n 6= 0 is not obviously guaranteed to ever succeed
given that it depends on received data (which is sent by either
the generator process G or a previous filter process). Thus, the
interplay of conditional branching and infinite recursion may in
general cause a disconnect between the semantics of the types and
those of the concrete processes. For instance, if the test x%n 6= 0
is replaced by false in the prime sieve example, its type is live
while the program is not. In the remainder of this section, we
make precise the conditions under which the semantics of infinite
processes and types simulate one another, thus implying liveness
(even in the presence of infinite branching).
To achieve our liveness results, we proceed as follows:

Definition 5.1 (May Converging Program). Let Γ ` P I T . We
write P ∈ May⇓ if for all X0 hi −
→∗ P , P −
→∗ 0.

Step 1. Define the notion of infinite conditional (Inf), identifying
a class of programs where conditional branches are executed
infinitely often.

Proposition 5.1. Assume Γ ` P I T and T is live. (1) Suppose
there exists P such that X0 hi −
→∗ P 6−
→. Then P ≡ 0; and (2) If
P ∈ May⇓, then P is live.

Step 2. Fill the gap between internal choices of types and conditionals by defining a ∗-conditional (if ∗ then P else Q) which
non-deterministically reduces to either P or Q (as the internal
choice ⊕{T, S}), allowing us to identify the subclass of Inf,
dubbed alternating conditionals (AC), where programs simulate
their non-deterministic conditional counterparts.

We note that the above statement does not restrict the programs to
be finite. A program with infinite reduction sequences can satisfy
liveness by Proposition 5.1. For instance:
{D1 , D2 } in newchan(b); newchan(c); (X1 hb, ci | X2 hb, ci)

Step 3. Prove that liveness of types implies liveness of programs in
AC.

with D1 = X1 (b, c) , select{c!hvi; X1 hb, ci , b!hwi; 0}
D2 = X2 (b, c) , select{c?(x); X2 hb, ci , b?(y); 0}
is live, as is its corresponding type.
The second class is a set of programs which do not contain infinitely occurring conditional branches (we discuss at length the
issues raised by the interplay of conditional branching and recursion in § 5.3). If such a process is assigned a live type, then it is
itself live. For example, any program which does not include conditionals or one with conditionals containing only finite processes
in both branches belong to this class. Consider a program obtained
from the one above by replacing 0 in D1 and D2 by X1 and X2 ,

Alternating and Non-deterministic Conditionals For Step 1, we
begin by defining a notion of infinite conditional (Definition 5.5) in
programs. Intuitively, we identify programs that reduce forever and
where conditional branches appearing under recursion have their
branches taken infinitely often.
Definition 5.2 (Marked Programs). Given a program P we define
its marking, written mark(P), as the program obtained by deterministically labelling every occurrence of a conditional of the form
if e then Q else R in P, as if n e then Q else R, such that n is distinct natural number for all conditionals in P.

Definition 5.3 (Marked Reduction Semantics). We define a marked
l
reduction semantics, written P −
→ Q, stating that program P reduces to Q in a single step, performing action l. The grammar of
action labels is defined as:
l :=  | n·L | n·R
where  denotes an unmarked action, n·L denotes a conditional
branch marked with the natural number n in which the then branch
is chosen, and n·R denotes a conditional branch in which the else

branch is chosen. We write P −
→ Q for P −
→ Q. The marked
reduction semantics replace rules [IFT ] and [IFF ] with:
e ↓ true

[IFTM ]

n·L

[IFFM ]

if n e then P else Q −−→ P

e ↓ false
n·R

if n e then P else Q −−→ Q

Definition 5.4 (Trace). We define an execution trace T of a process
P as the potentially infinite sequence of action labels ~l such that
l1
l2
P −→
P1 −→
. . . , with ~l = {l1 l2 . . . }. We write TP for the set of
all possible traces of a process P .
A trace of the marked reduction semantics identifies exactly
which branches were selected during the potentially infinite execution of a program.
We now define infinitely recurring conditionals. We use a reduction context Cr given by:
Cr

:=

[ ] | (P | Cr ) | (Cr | P ) | (νa)Cr

We write Cr [P ] for the process obtained by replacing P for the
hole [ ] in Cr .
Definition 5.5 (Infinite Conditional). We say that P has infinite conditional branches, written P ∈ Inf, iff mark(P ) −
→∗
Cr [if n e then Q1 else Q2 ] = R, for some n, and R has an infinite
trace where n·L or n·R appears infinitely often. We say that such
an n is an infinite conditional mark and write InfCond(P ) for the
set of all such marks.
The following statement implies that even programs which contain only infinite executions can be live if none of its conditionals
appear in traces infinitely often (i.e. our second class of programs).
Proposition 5.2 (Liveness for Finite Branching). Suppose Γ `
P I T and T is live and P 6∈ Inf. Then P is live.
The main purpose of Definition 5.7 is to identify infinitely running
processes where the behaviour of conditional branching approximates that of non-deterministic internal choice (i.e. the type-level
semantics of internal choice). To make this relationship precise, we
define a mapping from MiGo programs to programs where conditional branching is replaced by a form of non-deterministic branching. This step corresponds to Step 2.
Definition 5.6. The mapping (P )∗ replaces all occurrences of
if n e then Q else R, such that n ∈ InfCond(P ), with if ∗ then Q else R.
The reduction semantics of if ∗ then Q else R is defined as follows:
[IFT∗]

if ∗ then P else Q −
→P

[IFF∗]

Proposition 5.3 (∗-properties). Suppose Γ `B P I T . Then (1) if
P ∗ ∈ Inf then P ∗ ∈ AC; (2) If P ⇓o , then P ∗ ⇓o ; (3) if P ∗ ⇓o
then T ⇓o .
Liveness for Infinite Conditionals We now have defined the conditions under which programs simulate the behaviour of their types.
More precisely, when a program P is well-typed with some live
type T and P ∈ AC holds, then P must itself be live.
Theorem 5.3 (Liveness). Suppose Γ ` P I T and T is live and
P ∈ AC. Then P is live.
To summarise, we identified three significant classes of programs for which type liveness implies liveness: those with at least
one terminating path (Definition 5.1 and Proposition 5.1) such as
Fibonacci, cf. § 2.1.2; those for which their infinite traces do not
contain infinite occurrences of a given conditional (Proposition 5.2)
such as Dining Philosophers, cf. § 7.1; and, those with infinite
traces containing infinite occurrences of conditional branches (Definition 5.7 and Theorem 5.3) such as Prime Sieve, cf. § 2.1.1.
While a reasonable percentage of real-world programs are in the
first two classes, our empirical observations show that a substantial
amount of infinitely running programs (with infinitely occurring
conditionals) that are not in AC have redundant or erroneous conditionals.

6.

Bounded Asynchrony in MiGo

Our framework extends with relative ease to the asynchronous
communication variant of the Go language. As mentioned in § 2,
communication channels in Go are implemented as bounded FIFO
queues, where by default the buffer bound is 0 – synchronous
communication. For bounds greater than 0, communication is then
potentially asynchronous – sends do not block if the buffer is not
full and inputs do not block if the buffer is not empty.
Asynchrony significantly affects a program’s liveness. Consider
the following example:
P (x, y)

Recall that o ranges over any barbs, including ã. Moreover, observe that the mapping P ∗ only affects conditionals that are executed infinitely often (i.e. those whose behaviour may fail to be
captured by the type-level analysis). We do not require conditionals that are not in InfCond(P ) to necessarily match the barbs of
their non-deterministic counterpart, since their behaviour is already
over-approximated by the corresponding types.

x!h1i; y?(z) | y!h2i; x?(z)

A program that instantiates P (x, y) with synchronous communication channels will necessarily not be live since the output and input
actions in P are mismatched. However, with asynchronous channels, the output actions become non-blocking and the program is
indeed live – the output on x on the left-hand side can fire asynchronously, exposing the input on y which may then fire. Similarly
for the output on y and input on x on the right-hand side.
Processes and Typing To account for the buffer bounds in
the syntax of MiGo we add a bound n to channel creation,
newchan(y:σ, n); P . This number must be equal or greater to
zero and must be a literal. We also carry this information in runtime buffers: chσ, ni::ṽ and c? hσ, ni::ṽ (also replacing chσi::∅ and
c? hσi::ṽ by chσ, 0i::∅ and c? hσ, ni::ṽ for synchronous channels).
We add the reduction rules for asynchronous communication:

if ∗ then P else Q −
→Q

Definition 5.7 (Alternating Conditionals). We say that P has
alternating conditional branches, written P ∈ AC, iff P ∈ Inf
and if P −
→∗ (νc̃)Q then Q∗ ⇓o implies Q ⇓o .

,

[OUT ]
[INA ]

|ṽ| < n e ↓ v
c!hei; P | chσ, ni::ṽ −
→ P | chσ, ni::v · ṽ

c?(y); P | chσ, ni::ṽ · v −
→ P {v/y} | chσ, ni::ṽ

In all other rules that use buffers we add the buffer bound straightforwardly. The type system is fundamentally unchanged, now accounting for buffer bounds:
hNEWi

Γ, y:ch(σ, n) `s P I T c 6∈ dom(Γ) ∪ s ∪ fn(T )
Γ `s newchan(y:σ, n); P I (newn c)T {c/y}
|ṽ| = k
hBUFFi
Γ, a:ch(σ, n) `{a} ahσ, ni::ṽ I bacn
k

In contrast with the types and rules in Figure 4, (new a)T and bac
are replaced by (newn a)T and bacn
k , respectively, where k stands
for the number of elements in the buffer.
Liveness and safety of types are defined as in § 4.4, with two
extra rules for the definition of type barbs, pertaining to buffers. In
particular we need barbs for writing to a non-full buffer (P ↓• a )
and reading from a non-empty buffer (P ↓a• ), combined with the
following additional rules:
|ṽ| < n
ahσ, ni::ṽ ↓• a
P ↓a Q ↓• a
P | Q ↓[a]

verification outlined in § 4, checking bounded liveness and channel
safety of the types. An outline of our verification tool chain is
shown in Figure 8.
Gong
Behavioural types
GoInfer
go/ssa
package

|ṽ| ≥ 1
ahσ, ni::ṽ ↓a•

P ↓a• πi ↓a
P | select{πi ; Qi }i∈I ↓[a]

T ↓a T 0 ↓• a
T | T 0 ↓[a]

k≤1
bacn
k ↓a•

T ↓a• κi ↓a
T | N{κi ; Si }i∈I ↓[a]

Verification of Types The changes to the semantics of types are
straightforward. It is based on the LTS of § 4.1, where rule |NEW| and
|BUF| are replaced by their counterparts below, and four additional
rules |IN - B|, |OUT- B|, |PUSH| and |POP|.
|NEW|

τ

(newn a)T −
→ (νa)(T | bacn
0)
k<n

|IN - B|

bacn
k

•

a

−→

a

|PUSH|

T −
→ T0

|OUT- B|

bacn
k+1
•

[a]

end[a]

?
bacn
k −−−→ a

k≥1
a•
bacn
k −→
a•

a

S −→ S 0

|BUF|

|POP|

T −→ T 0

bacn
k−1
a

S−
→ S0

[a]

T | S −→ T 0 | S 0
T | S −→ T 0 | S 0
Observe that since types abstract away from values and channels
are attributed a unique payload type, the semantics does not model
message ordering.
With all the technical machinery in place for the bounded asynchronous setting, we replicate our main results. The proofs are
essentially identical to those in the synchronous setting. Indeed,
asynchrony affects our analysis only in the size of the models to
be checked (larger buffer sizes give larger LTSs). The symbolic
semantics executes the types up-to a limited number of channels,
which is orthogonal to the number of message a buffer can store,
cf. Figure 7.
Theorem 6.1 (Decidability – Asynchrony). For all T s.t. Fenced(T ),
it is decidable whether or not T is k-live (resp. channel safe), for
any k ≥ 0.
Theorem 6.2 (Process Channel Safety and Liveness – Asynchrony). Suppose Γ ` P I T .
1. If T is channel safe, then P is channel safe.
2. If T is live and either P ∈ May⇓, P 6∈ Inf or P ∈ AC, then P
is live.
With the revised semantics, the program
{P (x, y)} in newchan(x:int, 1); newchan(y:int, 1); P hx, yi
is correctly deemed as live, with the typing given by:
{tP (x, y) = (x; y | y; x)} in (new1 x)(new1 y)tP hx, yi

7.

Implementation

We have implemented our static analysis as a verification tool-chain
consisting of two parts: First, we analyse Go source code and infer
behavioural types (§ 3) based on a program’s usage of concurrency
primitives. The types are passed to a tool that implements the

written in Haskell

The tool checks input behavioural types for k-liveness
and k-channel safety.
GoInfer
written in Go
The tool loads source code, type-checks and builds
SSA IR using go/ssa package, then extracts communication from the SSA IR as behavioural types.

Load main()
Go source code

Figure 8. Workflow of our verification tool chain.

The barbs for asynchronous types, T ↓o , are given below:
k<n
bacn
k ↓• a

Gong

Type Inference Our type inference tool GoInfer is written in
Go, using the go/ssa1 package from Go project’s extra tools. The
package builds Go source code in Static Single Assignment (SSA)
representation, and provides an API to access the resulting SSA IR
programmatically. Starting from the program entry point, i.e. the
main() function in the main package, we transform the SSA IR
into a system of type equations T by converting each SSA block
into an individual type equation. The analysis and conversions
are context-sensitive, for example, channels created in different
instances of a function are different, and loops are unrolled if it
is possible to determine the bounds statically. We note that our
analysis is agnostic wrt. aliasing since we do not rely on linearity
of channels. In addition to inference, our tool can also check for
trivial conditionals that do not belong to any of the three classes of
programs defined in § 5.
Verification Our proof-of-concept verification tool Gong, written
in Haskell, inputs a system of type equations T representing a Go
program’s concurrent behaviour and performs liveness and channel
safety checks on the bounded symbolic semantics. Our representation of T makes use of the unbound package [53] to deal with
the binding structure of types. First, it checks if T is fenced. If
so, we generate all −
→k -reachable terms, where k is heuristicallycomputed. Finally, each of these terms are checked for k-liveness
and k-channel safety by identifying their barbs and successors.
7.1

Evaluation

We tested our tool-chain on the examples from the paper, from
works on static deadlock detection in Go [40], on open-source
Go programs from developer guides [43, 45] and GitHub [1], on
classic concurrency examples [18, 35], and on concurrent programs
translated to idiomatic Go from from [34].
Table 1 summarises the experimental results. The column “Go
programs” shows the names of the programs. In the columns
“Number of channels”, the number of channels given for programs
with bounded loops is precise since bounded loops are unrolled and
we can statically count the number of channels; for programs with
recursion, we count the channels that appear in the source code.
The columns “Time” show the inference and verification times
in seconds. We include a comparison with the tool from [40] to
demonstrate the extra expressiveness of our approach. If a program
is “Static”, it has no dynamic spawning of goroutines (a requirement for the usage of the tool of [40]).
forselect is a pattern described in [44] where an infinite
for loop and a select statement with two cases are combined to
repeatedly receive (or send). In our example we spawn two goroutines, where each goroutine has a for-select loop with compatible
1 http://golang.org/x/tools/go/ssa

Table 1. Go programs verified by our tool chain.
Examples

their approach (implemented as cond-recur in Table 1):

# chans
Analysis
[40]
LoC unbuf. buf. Live Safe Time (ms) Static Safe

sieve †
19
fib †
23
fib-async †
23
fact †
19
dinephil [18, 35] 56
jobsched
41
concsys [1]
112
36
fanin [40, 45]
fanin-alt [40]
37
mismatch [40]
26
fixed [40]
25
alt-bit [37]
74
40
forselect
cond-recur
32

2
2
1
2
3
0
2
3
3
2
2
0
3
2

0
0
1
0
0
1
0
0
0
0
0
2
0
0

X
X
X
X
X
X
×
X
×1
×
X
X
X
X

X
X
X
X
X
X
X
X
X
X
X
X
X
X

209.55
14638.4
32173.8
206.63
646921.76
48.12
323.75
89.14
209.02
26.59
24.58
405.78
31.01
34.08

×
×
×
×
×
×
×
X
X
X
X
X
X
X

if e1 then a!he2 i.Xha, bi else b?(z); 0,
select{a?(z); Y ha, bi, b!hi; 0}} in
newchan(a); newchan(b); (Xha, bi | Y ha, bi)

Finally, (3) it is unclear how their tool can deal with the ambiguity
of context sensitive inter-procedural analysis given their use of the
oracle tool and the syntactic approach taken in the implementation.
X
X
×
X
X
X
X

1

: testing for channel close state is not supported in this version
†: examples that are not finite control
The benchmarks were compiled with ghc 7.10.3 and go1.6.2 executed on Intel Core i5
@ 3.20GHz with 8GB RAM.

channel communication. In the for-select loop, one of the select
cases receives (or sends) a message then continues to the next iteration of the infinite loop; the other case breaks out of the loop
upon sending (or receiving) a message from the other goroutine so
that both goroutines exit the loop together. The exit condition is
non-deterministic (because of select), but the program is both live
and safe. cond-recur is similar to forselect, where one of
the two goroutines contains a for-select loop, but the other has an
ordinary for-loop so that the exit condition of the for-loop is deterministic.

8.

{X(a, b) =
Y (a, b) =

Related Work and Conclusion

Static Deadlock Detection in Synchronous Go There are two
recent works on static deadlock detection for synchronous Go [40,
47]. The work [40] extracts Communicating Finite State Machines [6] whose representation corresponds to session types [24,
48] from Go source code, and synthesises from them a global
choreography using the tool developed in [34]. If the choreography is well-formed, a program does not have a (partial) deadlock.
This approach is seriously limited due to the lack of expressiveness
of (multiparty) session types [26] and its synthesis theory. The approach expects all goroutines to be spawned before any communication happens at runtime. This is due to the fact that the synthesis
technique requires all session participants to be present from the
start of the global interaction, meaning that their work cannot handle most programs with dynamic patterns, such as spawning new
threads after communication started. The analysis is also limited to
unbuffered channels and does not support asynchrony. For instance,
our prime sieve example cannot be verified by their tool, and is in
fact used to clarify the limitations of their approach. Moreover, the
work is limited to the tool implementation, no theoretical property
nor formalisation is studied in [40].
The work of [47] uses the notion of forkable behaviours (i.e.
a regular expression extended with a fork construct) to capture
spawning behaviours of synchronous Go programs, developing a
tool based on this approach to directly analyse Go programs. Their
technique is sound but has some significant theoretical and practical limitations: (1) their analysis does not support asynchrony
(buffered channels), closing of channels or usages of the select construct with non-trivial case bodies; (2) while their liveness analysis
(when restricted to synchrony) targets the sound fragment of our
analysis, they are more conservative in their approach. For instance,
the following program which is verified as live in our approach (this
program belongs to May⇓ in our theory) is judged as a deadlock in

Behavioural Types Behavioural type-based techniques (see [27]
for a broad survey) have been developed for general concurrent
program analyses [28], such as deadlock-freedom [22, 30], lockfreedom [32, 42], resource usages [33] and information flow analysis [29].
All of the type-based techniques above differ from ours in
that we perform an analysis on types akin to bounded modelchecking, whereas their works take a type-checking based approach
to deadlock (or lock) freedom. Their techniques are sound against
all possible inputs of processes, but often too conservative. Our
approach is sound only for some subsets of possible inputs, but
less conservative. A potential limitation of their techniques is that
subtle changes in channel usage (that may not have a significant
effect on a program’s outcome) can produce significantly different
analysis outcomes (see discussion in [22] and [42]). Moreover, the
dependency tracking can be quite intricate and hard to implement
in a real language setting. Our fencing-based approach is more
easily implemented as a post-hoc analysis, covering a wide range
of Go programs, since it only limits names in recursive call sites
and does not explicitly depend on the ordering of communications
or on computing circularities of channels (provided the programs
are in one of the classes of § 5).
The work [22, 31] develops a deadlock detection analysis of
asynchronous CCS processes with recursion and new name creation. The analysis is able to reason about infinite-state systems
that create networks with an arbitrary number of processes, going
beyond those of [30] and [42]. Their approach uses an extension
of the typing system of [30] as a way to extract a so-called lam
term from a (typed) process. Lam terms track dependencies between channel usages as pairs of level names. Given a lam term, the
authors develop a sound and complete decision procedure for circularities in dependencies. By separating this decision procedure
from the type system, their system is able to accurately analyse
deadlock-free processes that are not possible in [30] and [42].
We first point out that the deadlock-freedom property of [22, 31]
does not match with our notion of liveness (which is closer to lock
freedom in [32, 42]). For instance, their analysis accepts program
Fib bad in § 2.1.2 as a deadlock-free process since a program that
loops non-productively is deadlock-free (but not lock-free).
While their analysis can soundly verify unfenced types, which
is by construction outside the scope of our work, we note that
the reduction of deadlock-freedom to circularity of lams in their
work excludes some natural communication patterns that are finitecontrol, which can be soundly checked by our type-level analysis.
Consider the following finite control program (described in [31]),
which can be directly interpreted as a MiGo type:
{A(x, y) =
B(x, y) =

x?(); y!hi; Ahx, yi,
x!hi; y?(); Bhx, yi} in
newchan(a); newchan(b); (Aha, bi | Bha, bi)

The program above consists of two threads that continuously send
and receive along the two channels a and b. This program, despite
being finite control (and deadlock-free) is excluded by their analysis. As described in [31], this happens due to their current formulation of the type system assigning a finite number of levels in
recursive channel usages, which entails that finite-control systems

that use channels infinitely often (such as the one above) can be
assigned circular lams, despite being deadlock-free. Our approach,
by not relying on such notions of circularity can tackle these finitecontrol cases in a sound manner.
The work of [42] studies a variation of [30, 32] that ensures
deadlock freedom and lock freedom of the linear π-calculus, with a
form of channel polymorphism. By relying on linearity, the system
in [42] rules out many examples that are captured by our work
(although it can in principle analyse unfenced types). The fib and
diningphilosopher examples denote patterns that are untypable
in [42], but can be verified in our tool. Our tool can also verify
programs morally equivalent to most examples discussed in [42],
see Table 1 in § 7.1.
Session Types The work on session types is another class of behavioural typing systems that rely crucially on linearity in channel types to ensure certain compatibility properties of structured
communication between two (binary [24]) or more (multiparty
[26]) participants. Progress (deadlock-freedom on linear channels)
is guaranteed within a single session, but not for multiple interleaved sessions. Several extensions to ensure progress on multiple
sessions have been proposed, e.g. [11, 13, 14]. Our main examples
are not typable in these systems for the same reasons described
in the above paragraph. Their systems do not ensure progress of
shared names, which are key in our examples.
A different notion of liveness called request-response is proposed in [16] based on binary session types. Their liveness means
that when a particular label of a branching type (a request) is selected, a set of other labels (its responses) is eventually selected.
The system requires a priori assumptions that a process must satisfy lock-freedom and annotations of response labels in types.
The works of [9, 10, 52] based on linear logic ensure progress
in the presence of multiple session channels, but the typing discipline disallows modelling of process networks with cyclic patterns (such as prime sieve). In these works, progress denotes both
deadlock and lock-freedom in the sense of [42]. However, to ensure
logical consistency general recursion is disallowed. In the presence
of general recursion [50], progress is weakened; ensuring all typable processes are deadlock-free but not necessarily lock-free. The
work of [51] studies a restricted form of corecursion that ensures
both deadlock- and lock-freedom in the context of logic-based processes. However, since the typing discipline ensures termination of
all computations it is too restrictive for a more practical setting such
as ours.
Effect Systems The work [41] introduces a type and effect system for a fragment of concurrent ML (including dynamic channel
creations and process spawning) with a predicate on types which
guarantees that typed programs are limited to a finite communication topology. Their types are only used to check whether a program has a finite communication topology, that is, whether a program uses a bounded number of channels and a bounded number
of processes. No analysis wrt. safe or live communication is given,
which is the ultimate goal of our work.
Conclusion and Future Work Since the early 1990s, behavioural
type theories which formalise “types as concurrent processes” [28]
have been studied actively in models for concurrency [27]. Up to
this point, there have been few opportunities to apply these techniques directly to a real production-level language. The Go language opens up such a possibility. This work proposes a static verification framework for liveness and safety in Go programs based
on a bounded execution of fenced behavioural types. We develop a
tool that analyses Go code by directly inferring behavioural types
with no need for additional annotations.
In future work we plan to extend our approach to account for
channel passing, and also lock-based concurrency control, enabling

us to verify all forms of concurrency present in Go. The results of
§ 4 suggest that it should be possible to encode our analysis as
a model checking problem, allowing us to: (1) exploit the performance enhancements of state of the art model checking techniques;
(2) study more fine-grained variants of liveness; (3) integrate model
checking into the analysis of conditionals to, in some scenarios, decide the program class (viz. § 5.3). Another interesting avenue of
future work is to explore the integration of type-checking based approaches into our framework, including those aimed at liveness and
termination-checking (such as [17, 25, 29, 32]). These techniques
eliminate false positives arising due to issues on divergence of processes, which are related to our classification of § 5, hence would
be useful to identify a set of processes which conform, e.g. Proposition 5.1. This would enable a more fine-grained analysis, taking
advantage of the strong soundness properties of this line of work.
Moreover, the latter mentioned works could be applied in order to
soundly approximate the program classification studied in § 5.3.

Acknowledgments
We gratefuly acknowledge Naoki Kobayashi for finding flaws in
Sections 4 and 5 in earlier versions of this work; as well as for detailed comments on Sections 7 and 8. The present version aims at
correcting these errors. In particular, we have revised the definition of liveness and safety for types (Definitions 4.4 and 4.5) and
removed theorems related to soundness of our analysis of general
liveness and safety for types. We have revised several remarks in
the comparison between our work and [22, 29, 30, 32] (§ 7 and 8).
We also would like to thank Elena Giachino, Raymond Hu and
Luca Padovani for fruitful discussions on this work, as well as the
anonymous referees for their comments. This work is partially supported by EPSRC EP/K034413/1, EP/K011715/1, EP/L00058X/1
and EP/N027833/1; and by EU FP7 612985 (UPSCALE) and
COST Action IC1405 (RC).

References
[1] Collection of Golang concurrency patterns. https://github.
com/stillwater-sc/concurrency.
[2] Tool chain. http://mrg.doc.ic.ac.uk/tools/gong.
[3] V. Agababov, M. Buettner, V. Chudnovsky, M. Cogan, B. Greenstein,
S. McDaniel, M. Piatek, C. Scott, M. Welsh, and B. Yin. Flywheel:
Google’s Data Compression Proxy for the Mobile Web. In NSDI 2015,
2015.
[4] D. G. Anderson. Experience with ePaxos: Systems Research using
Go. 2013. https://da-data.blogspot.co.uk/2013/10/
experience-with-epaxos-systems-research.html.
[5] Andrew Gerrand. Share Memory By Communicating. https://
blog.golang.org/share-memory-by-communicating.
[6] D. Brand and P. Zafiropulo. On communicating finite-state machines.
J. ACM, 30:323–342, April 1983.
[7] N. Busi, M. Gabbrielli, and G. Zavattaro. Replication vs. recursive
definitions in channel based calculi. In ICALP’03, pages 133–144,
2003.
[8] N. Busi, M. Gabbrielli, and G. Zavattaro. Comparing recursion,
replication, and iteration in process calculi. In ICALP’04, pages 307–
319, 2004.
[9] L. Caires and F. Pfenning. Session types as intuitionistic linear propositions. In CONCUR, volume 6269 of LNCS, pages 222–236. Springer,
2010.
[10] L. Caires, F. Pfenning, and B. Toninho. Linear logic propositions
as session types. Mathematical Structures in Computer Science,
26(3):367–423, 2016.
[11] M. Carbone, O. Dardha, and F. Montesi. Progress as compositional
lock-freedom. In COORDINATION, volume 8459 of LNCS, pages
49–64. Springer, 2014.

[12] S. Chaki, S. K. Rajamani, and J. Rehof. Types as models: model
checking message-passing programs. In POPL’02, pages 45–57, 2002.
[13] M. Coppo, M. Dezani-Ciancaglini, and N. Yoshida. Asynchronous
Session Types and Progress for Object-Oriented Languages. In
FMOODS’07, volume 4468 of LNCS, pages 1–31, 2007.
[14] M. Coppo, M. Dezani-Ciancaglini, N. Yoshida, and L. Padovani.
Global Progress for Dynamically Interleaved Multiparty Sessions.
MSCS, 26(2):238–302, 2016.
[15] M. Dam. Model checking mobile processes. Inf. Comput., 129(1):35–
51, Aug. 1996.
[16] S. Debois, T. T. Hildebrandt, T. Slaats, and N. Yoshida. Type-checking
liveness for collaborative processes with bounded and unbounded recursion. Logical Methods in Computer Science, 12(1), 2016.
[17] R. Demangeon, D. Hirschkoff, and D. Sangiorgi. Termination in
impure concurrent languages. In CONCUR’10, volume 6269 of LNCS,
pages 328–342. Springer, 2010.
[18] E. W. Dijkstra. Cooperating sequential process. Programming Languages, pages 43–112, 1965.
[19] E. D’Osualdo, J. Kochems, and C. L. Ong. Automatic verification of
erlang-style concurrency. In SAS, volume 7935 of LNCS, pages 454–
476. Springer, 2013.
[20] B. Fitzpatrick. go 1.5.1 linux/amd64 deadlock detection failed,
2015. https://github.com/golang/go/issues/12734#
issuecomment-142859447.
[21] S. Gay and M. Hole. Subtyping for Session Types in the Pi-Calculus.
Acta Informatica, 42(2/3):191–225, 2005.
[22] E. Giachino, N. Kobayashi, and C. Laneve. Deadlock analysis of
unbounded process networks. In CONCUR, volume 8704 of LNCS,
pages 63–77. Springer, 2014.
[23] C. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.
[24] K. Honda, V. T. Vasconcelos, and M. Kubo. Language primitives and
type disciplines for structured communication-based programming.
In ESOP’98, volume 1381 of LNCS, pages 22–138. Springer-Verlag,
1998.
[25] K. Honda and N. Yoshida. A uniform type structure for secure
information flow. ACM Trans. Program. Lang. Syst., 29(6), 2007.
[26] K. Honda, N. Yoshida, and M. Carbone. Multiparty Asynchronous
Session Types. In POPL’08, pages 273–284. ACM, 2008. A full
version in JACM: 63(1-9):1–67, 2016.
[27] H. Hüttel, I. Lanese, V. T. Vasconcelos, L. Caires, M. Carbone, P.M. Deniélou, D. Mostrous, L. Padovani, A. Ravara, E. Tuosto, H. T.
Vieira, and G. Zavattaro. Foundations of session types and behavioural
contracts. ACM Comput. Surv., 49(1):3:1–3:36, Apr. 2016.
[28] A. Igarashi and N. Kobayashi. A generic type system for the picalculus. Theor. Comput. Sci., 311(1-3):121–163, 2004.
[29] N. Kobayashi. Type-based information flow analysis for the picalculus. Acta Inf., 42(4-5):291–347, 2005.
[30] N. Kobayashi. A new type system for deadlock-free processes. In
CONCUR’06, volume 4137 of LNCS, pages 233–247, 2006.
[31] N. Kobayashi and C. Laneve. Deadlock analysis of unbounded process
networks. Inf. Comput., 252:48–70, 2017.
[32] N. Kobayashi and D. Sangiorgi. A hybrid type system for lockfreedom of mobile processes. TOPLAS, 32(5):16:1–16:49, May 2008.
[33] N. Kobayashi, K. Suenaga, and L. Wischik. Resource usage analysis
for the p-calculus. Logical Methods in Computer Science, 2(3), 2006.

[34] J. Lange, E. Tuosto, and N. Yoshida. From Communicating Machines
to Graphical Choreographies. In S. K. Rajamani and D. Walker,
editors, POPL’15, pages 221–232. ACM Press, 2015.
[35] J. Magee and J. Kramer. Concurrency: State Models &Amp; Java
Programs. John Wiley & Sons, Inc., New York, NY, USA, 1999.
[36] R. Milner. A Calculus of Communicating Systems, volume 92 of
Lecture Notes in Computer Science. Springer, Berlin, 1980.
[37] R. Milner. Communication and Concurrency. Prentice-Hall, Inc.,
Upper Saddle River, NJ, USA, 1989.
[38] R. Milner and D. Sangiorgi. Barbed bisimulation. In W. Kuich, editor,
ICALP, volume 623 of LNCS, pages 685–695. Springer-Verlag, 1992.
[39] I. Moraru, D. G. Andersen, and M. Kaminsky. There is More Consensus in Egalitarian Parliaments. In SOSP’13, pages 358–372, New
York, NY, USA, 2013. ACM.
[40] N. Ng and N. Yoshida. Static Deadlock Detection for Concurrent Go
by Global Session Graph Synthesis. In CC 2016, pages 174–184.
ACM, 2016.
[41] H. R. Nielson and F. Nielson. Higher-order concurrent programs with
finite communication topology (extended abstract). In POPL ’94,
pages 84–97. ACM, 1994.
[42] L. Padovani. Deadlock and Lock Freedom in the Linear π-Calculus.
In T. A. Henzinger and D. Miller, editors, CSL-LICS’14, pages 72:1–
72:10. ACM Press, 2014.
[43] Rob Pike. Go Concurrency Patterns, 2012. https://talks.
golang.org/2012/concurrency.slide.
[44] Sameer Ajamni. Advanced Go Concurrency Patterns, 2013. https:
//talk.golang.org/2013/advconc.slide.
[45] Sameer Ajmani. Go Concurrency Patterns: Pipelines and cancellation,
2014. https://blog.golang.org/pipelines.
[46] D. Sangiorgi and D. Walker. The π-Calculus: a Theory of Mobile
Processes. Cambridge University Press, 2001.
[47] K. Stadmüller, M. Sulzmann, and P. Thiemann. Static Trace-Based
Deadlock Analysis for Synchronous Mini-Go. In APLAS, volume
10017 of LNCS, 2016.
[48] K. Takeuchi, K. Honda, and M. Kubo. An Interaction-based Language
and its Typing System. In PARLE’94, volume 817 of LNCS, pages
398–413. Springer-Verlag, 1994.
[49] The Go Authors. Effective Go. https://golang.org/doc/
effective_go.html.
[50] B. Toninho, L. Caires, and F. Pfenning. Higher-order processes,
functions, and sessions: A monadic integration. In ESOP’13, pages
350–369, 2013.
[51] B. Toninho, L. Caires, and F. Pfenning. Corecursion and nondivergence in session-typed processes. In TGC’14, pages 159–175,
2014.
[52] P. Wadler. Proposition as Sessions. In ICFP’12, pages 273–286, 2012.
[53] S. Weirich and B. Yorgey. Unbound library. https://hackage.
haskell.org/package/unbound.
[54] M. Welsh.
Rewriting a large production system in Go.
2013. http://matt-welsh.blogspot.co.uk/2013/08/
rewriting-large-production-system-in-go.html.
[55] K. Yasukata, N. Kobayashi, and K. Matsuda. Pairwise reachability
analysis for higher order concurrent programs by higher-order model
checking. In CONCUR, volume 8704 of LNCS, pages 312–326.
Springer, 2014.

A.

Appendix for Section 4

A.1

Decidability
def

Definition A.1 (Size of T ). Define |T | = |T |∅ , where

0
if T = 0



0 G


1
+
|T
|
if T = α; T 0 , α ∈ {κ, end[a]}



0
G

+ |T |
if T = (νa)T 0 or (new a)T 0
1
P
G def
G
|T | =
|Ti |
if T = ⊕{Ti }i∈I or N{Ti }i∈I
 i∈I
G
G


|T
|
+
|T
|
if T = T1 | T2
1
2



|T 0 {ã/x̃}|G∪{t} if T = thãi, t ∈
/ G, t(x̃) = T 0



0
if T = thãi, t ∈ G
Definition A.2 (Limited Unfolding). Let Gk be the function from
dom(T ) to N that always returns k. The kth unfolding of T wrt. ã,
G
written Uãk (T ) is given by Uã k (T ), defined below.

α; UãG (T 0 )
if T = α; T 0 and




α ∈ {τ, a, a, end[a]}





0
if
T
=0



0
G

(T
)
if
T
= (νa)T 0
(νa)U

ã


0
G


if T = (new a)T 0
(new a)Uã (T )
G
G
if T = ⊕{Ti }i∈I
Uã (T ) = ⊕{Uã (Ti )}i∈I

G


(T
)}
if T = N{Ti }i∈I
N{U
i i∈I
ã



G
G

U
(T
)
|
U
(T
)
if T = T1 | T2
 ã 1
ã

2

G[t7→i−1]
0 b̃


/
x̃
)
if T = thb̃i, b̃ ∩ ã 6= ∅,
(T
U

ã



t(x̃) = T 0 ∈ T , G(t) = i > 0



thb̃i
if G(t) = 0 or b̃ ∩ ã = ∅
Lemma A.1 shows that there cannot be an infinitely decreasing
sequence ã1  · · ·  ãk  · · · , when unfolding a type. We note that
due to our convention that in t(x̃) = T , we have x̃ ⊆ fv(T ), a type
T can only remember the names it received as parameters.
Lemma A.1. Given a chain
ã1  ã2  · · ·  ãk

k > |ã1 |

such that ∀1 ≤ i < k : |ãi | = |ãi+1 |, and ∀1 ≤ i < k : a ∈
ãi ∧ a ∈
/ ãi+1
=⇒ ∀i < j ≤ k : a ∈
/ ãj . There exists
n ≤ |ã1 | such that ∀j ≥ n : ã1 ∩ ãj = ∅.
Proof. Relation ã ≺ b̃ implies that we must have
ã = aj+1 · · · ak · b1 · · · bj ≺ a1 · · · ak = b̃
with k ≥ 1 and j ≥ 1.
Hence, if we remove one element at each step of the chain (the
worst case), we obtain a chain of the form:
ã1 = a1 · · · ak  ã2 = a2 · · · ak · b1  · · ·
and, in general: ãi = ai · · · ak · b1 · · · bi−1 if i ≤ k; thus we have
ãi ∩ a˜1 = ∅ when i > k, as expected, since by assumption we have
∀1 ≤ i < k : a ∈ ãi ∧ a ∈
/ ãi+1 =⇒ ∀i < j ≤ k : a ∈
/ ãj
(i.e., once a has been removed from ãi it cannot appear again
further in the chain).
Lemma A.2 shows that the number of occurrences of a type
variable in the kth unfolding of T is bounded by a function of the
size of the syntactical tree of T .

Definition A.3 (Number of Occurrences of t in T ).

0
if T = 0



0


|T
|
if T = α; T 0 and α ∈ {κ, end[a]}

 0t


if T = (νa)T 0 or (new a)T 0
|T |t
|T |t = max({|Ti |t }i∈I ) if T = ⊕{Ti }i∈I or N{Ti }i∈I



if T = T1 | T2
|T1 |t + |T2 |t



1
if T = thãi



0
if T = shãi and s 6= t
Lemma A.2. If Fenced(T ), then for all t(x̃) = T ∈ T ,
∀k ≥ 0 : |Ux̃k (T )|t ≤ |T ||x̃|
Proof. To increase the number of occurrences of a variable, we
must have parallel processes, which implies that we must strictly
decrease the number of free names hence eventually reach process
that do no use any variables in x̃.
It is a simple observation that
∀k ≥ 0 : |Ux̃k (T )|t ≤ |T |k
Hence, the results holds trivially for any k < |x̃|.
Assume that the result does not hold by contradiction and take
k ≥ |x̃| such that
|Ux̃k (T )|t ≤ |T ||x̃|

and

|Ux̃k+1 (T )|t > |T ||x̃|

For the number of occurrences of t to increase strictly, we must
have
h
i
T = C C1 [thb̃i] | C2 [thc̃i]

since ◦ ; x̃ ; ◦ `t T , we must have b̃ ≺ x̃ and c̃ ≺ x̃, which implies,
by Lemma A.1, that the unfolding will terminate.
In particular, we have a strictly decreasing number of names
from x̃ further down in the tree. Thus after |x̃| unfoldings, no names
˜ (i.e., d˜ ∩ x̃ = ∅)
from x̃ will be left in each occurrences of thdi
and t cannot be unfolded further.
Lemma A.3. For all types T , if T ≡ T 0 or T −
→ T 0 , then
fn(T ) ⊇ fn(T 0 ).
Proof. Straightforward from the rules in Figure 5.
Lemma 4.1 (Finite Control). If Fenced(T ), then the set
{[T ]≡ | ∅ C t0 hi −
→∗k ∅ C T } is finite, for any finite k.
Proof. Under the symbolic semantics, by Lemma A.2, there can be
only a limited number of occurrences of each variable. Hence the
processes cannot unfold infinitely wide, therefore, by Lemma A.3,
only finitely many names are required. If infinitely many names are
created, they can be garbage collected by structural congruence, in
particular any type (νã) thb̃i can be replaced by (ν b̃) thb̃i if ã ⊇ b̃.
Finally, processes that differ only from their bound names can be
equated by alpha-equivalence.
Theorem 4.1 (Decidability). For all T s.t. Fenced(T ), it is decidable whether or not T is k-live (resp. channel safe), for any k ≥ 0.
Proof. By Lemma 4.1, the LTS generated by the k-symbolic semantics is finite state. Hence, checking k-liveness and k-safety is
decidable since the k-symbolic LTS is finite and thus each term is
using only finitely many names (after garbage collection).

B.

Appendix for Section 5

We use the following lemma for the proofs.
Lemma B.1 (Inversion). 1. If Γ `B P I T and P ≡ (νc)P 0
then T ≡ (νc)T 0 , with Γ0 `B 0 P 0 I T 0 , for some Γ0 and B 0 ,
with Γ ⊆ Γ0 and B ⊆ B 0 .
2. If Γ `s P I T and P ≡ P1 | P2 then T ≡ T1 | T2 , with
Γ `B1 P1 I T1 and Γ `B2 P2 I T2 , with B = B1 ∪ B2 .
Proof. Straightforward from the typing rules.
Theorem 5.1 (Subject Reduction). Let Γ `B P I T and P −
→
P 0 . Then there exists T 0 such that Γ `B 0 P 0 I T 0 with T −
→ T 0.
Proof. We use Lemma B.1 and similar inversion lemmas for other
constructs. Then the rest is straightforward by induction on typing
and case analysis on the semantics of processes.
Theorem 5.2 (Process Channel Safety). Suppose Γ ` P I T and
T is safe. Then P is safe.
Proof. Suppose X0 hi −
→∗ (νc̃)Q and Q ↓a? . Then by Lemma B.1,
there exists T such that Γ0 ` Q I T . By Lemma 5.1, we have
T ↓a? . Since T is safe, ¬(T ⇓end[a] ) and ¬(T ⇓a ). This implies,
by applying Lemma 5.1 again, ¬(Q ⇓end[a] ) and ¬(Q ⇓a ).
Proposition 5.1. Assume Γ ` P I T and T is live. (1) Suppose
there exists P such that X0 hi −
→∗ P 6−
→. Then P ≡ 0; and (2) If
P ∈ May⇓, then P is live.
Proof. Assume Γ ` P I T and T is live.
(1) Suppose by contradiction that X0 hi −
→∗ P 6−
→ but P 6≡ 0. Then
there exists Q such that P ≡ (νã)(Q) and Q ↓b or Q ↓b̃ for some
b or b̃. Then by Lemma 5.1, it contradicts T is live.
(2) By definition of liveness (there is always a path (τ -actions) to
reach the term 0, which is live).

Theorem 5.3 (Liveness). Suppose Γ ` P I T and T is live and
P ∈ AC. Then P is live.
Proof. If all conditionals in P are infinite, then the result follows
by Lemma B.3. Otherwise, by Lemma B.4 we can execute P until
there are no more finite conditionals, from which then the result
follows by Subject Reduction (Theorem 5.1) and Lemma B.3.

C.

k<n
bacn
k ↓• a

Proof. Suppose P 6∈ Inf and X0 hi →
− ∗ (ν~a)P . Then by Inversion
Lemma (Lemma B.1), there exists Γ0 `B P I T . Then P ⇓b iff
T ⇓b and P ⇓b̃ iff T ⇓b̃ since the reduction of T coincides with
the reduction of P . Hence P is live.

k≤1
bacn
k ↓a•

T ↓a T 0 ↓• a
T | T 0 ↓[a]

T ↓a• κi ↓a
T | N{κi ; Si }i∈I ↓[a]

Proofs of Theorems 6.1 and 6.2 Since the definitions of liveness
and safety stay the same, and since the semantics are essentially
isomorphic (the symbolic semantics is unaffected, notably) the
proofs are essentially identical with the synchronous cases.

D.

Appendix for Section 7

Below we present source code of the examples we created for our
evaluation.
D.1

forselect

The forselect program spawns two communicating for-select
loop and both goroutines terminate when channel term is used.
The choice of sending or receiving from the channels inside the
for-select loop is non-deterministically decided by the select
primitive in Go.
1

package main

2
3

import "fmt"

4
5
6
7

Proposition 5.2 (Liveness for Finite Branching). Suppose Γ `
P I T and T is live and P 6∈ Inf. Then P is live.

Appendix for Section 6 (Asynchrony)

Definition C.1 (Asynchronous type barbs).

8
9
10
11
12
13
14
15
16

func sel1(term, ch chan int, done chan struct{}) {
for {
select {
case <-term: // Receive termating message.
fmt.Println("sel1: recv")
done <- struct{}{}
return
case ch <- 1:
fmt.Println("sel1: send")
}
}
}

17

Proof of Theorem 5.3
Lemma B.2. Suppose Γ ` P I T , T is live and P is conditionalfree, then P is live.

18
19
20
21
22

Proof. Straightforward from the fact that all process moves are
strongly matched by type moves and T is live.
Lemma B.3. Suppose Γ ` P I T , T is live, P ∈ AC and P and
all marked conditionals in mark(P) are in InfCond, then P is live.

23
24
25
26
27
28
29

Proof. Since all conditionals in P are infinite, then by the definition
of AC and T being live gives us that P ⇓o iff T ⇓o , from which
the result follows.

30
31
32
33
34

Lemma B.4. Suppose Γ ` P I T , P ∈ AC, T is live and
mark(P) has a marked branch n that is not in InfCond(P). Then
P has an infinite trace in which n no longer appears.
Proof. By P ∈ AC it follows that P cannot have a finite trace, thus
the result follows by n 6∈ InfCond(P).

func sel2(term, ch chan int, done chan struct{}) {
for {
select {
case <-ch:
fmt.Println("sel2: recv")
case term <- 2: // Send terminating message.
fmt.Println("sel2: send")
done <- struct{}{}
return
}
}
}

35
36

func main() {
done := make(chan struct{})
term := make(chan int) // Terminating channel.
data := make(chan int)
go sel1(term, data, done)
go sel2(term, data, done)

37

<-done
<-done

38
39
40

}

D.2

cond-recur

The cond-recur program is similar to forselect but the
decision of when to terminate the for-select loop is determined by
a conditional in the x goroutine, rather than a terminating channel.

21
22
23
24
25

func morejob() bool {
i++
return i < 20
}

26
1

package main

2
3

28

import "fmt"

4
5
6
7
8
9
10
11
12
13
14
15
16
17

20
21
22
23
24
25
26
27
28
29
30
31
32

D.3

func main() {
done := make(chan struct{})
ch := make(chan int)
go x(ch, done) // Spawn a decision making
goroutine.
FINISH:
for {
select {
case x := <-ch:
fmt.Println(x)
case <-done: // Terminate message.
break FINISH // Break out of loop.
}
}
}

jobsched

The jobsched program sets up a shared job queue between two
workers to process the incoming jobs.
1

package main

2
3
4
5
6

import (
"fmt"
"time"
)

7
8

var i int

9
10
11
12
13
14
15
16
17
18
19
20

29
30

func x(ch chan int, done chan struct{}) {
i := 0
for {
if i < 3 { // This condition decides when to
terminate.
ch <- i
fmt.Println("Sent", i)
i++
} else {
done <- struct{}{} // Send terminate message
.
return
// Break out of loop.
}
}
}

18
19

27

func worker(id int, jobQueue <-chan int, done <-chan
struct{}) {
for {
select {
case jobID := <-jobQueue:
fmt.Println(id, "Executing job", jobID)
case <-done:
fmt.Println(id, "Quits")
return
}
}
}

31
32
33
34
35
36
37
38
39
40
41

E.

func producer(q chan int, done chan struct{}) {
for morejob() {
q <- i
}
close(done)
}
func main() {
jobQueue := make(chan int)
done := make(chan struct{})
go worker(1, jobQueue, done)
go worker(2, jobQueue, done)
producer(jobQueue, done)
time.Sleep(1 * time.Second)
}

Additional Discussion of Related Work

We discuss some additional related work.
Session types. Another key limitation of session typing is that
conditional branching is usually typed with the following rule:
Γ ` e:bool Γ ` P I ∆ Γ ` Q I ∆
Γ ` if e then P else Q I ∆
The rule above (even in the presence of subtyping, e.g. [21]) enforces that the communication behaviour of the two branches must
be fundamentally the same. This turns out to be too restrictive in
practice, where branching is mostly used to define the conditions
under which behaviour should indeed be morally different.
Model Checking. The classical work [12] verifies progress
properties (ϕ) of the π-calculus applying a LTL model checking
tool to types which take the form of CCS terms. To limit state-space
explosion, the work relies on an assume-guarantee reasoning technique. The work requires “user input” type signatures (annotations)
on processes. Our framework does not require such annotations.
The work [19] studies a verification of Erlang programs where
processes communicate via unbounded mailboxes and can be
spawned dynamically and potentially infinitely. Erlang programs
are modelled as vector addition systems (VAS) and a VAS-based
tool is used to check simple reachability properties. The model
is limited to a bounded number of channels, hence the topologies
represented in their work are more limited than those induced by
fenced types.
The work [55] uses higher-order model checking to verify a
concurrent calculus which features dynamic process creation. They
transform processes into higher-order recursion schemes, which in
turn generates action trees on which they can check whether two
threads enter the same critical section. Because the action trees
model executions only at the single process level (i.e. ignoring how
processes are interleaved and communicate with each other), it is
not straightforward to adapt their approach to verify our liveness
and safety properties.

