Witnessing Side-Effects ∗Tachio Terauchi

Alex Aiken

EECS Department
University of California, Berkeley
tachio@cs.berkeley.edu

Computer Science Department
Stanford University
aiken@cs.stanford.edu

Abstract
We present a new approach to the old problem of adding side effects
to purely functional languages. Our idea is to extend the languagewith “witnesses,” which is based on an arguably more pragmatic
motivation than past approaches. We give a semantic condition forcorrectness and prove it is sufficient. We also give a static checking
algorithm that makes use of a network flow property equivalent tothe semantic condition.
Categories and Subject Descriptors D.3.1 [Programming Languages]: Formal Definitions and Theory; D.3.3 [Programming
Languages]: Language Constructs and Features
General Terms
Keywords

Design, Languages, Theory

Functional languages, side-effects

order. For example, a program is allowed to read from a referencecell in two unordered contexts as well as write to two different cellsin two unordered contexts.
Besides providing new insights into the old problem of fittingside effects into functional languages for conventional von Neumann architectures, our work is motivated by the emergence ofcommercial parallel computer architectures (e.g., chip-multiprocessors
or “multi-core” chips) that encourage parallel programming. It is
well-known that the “explicit dependence” property of functional
languages makes parallelization easier for both programmers andcompilers.1 However, frequent use of side-effects, namely manual
destructive memory/resource updates, are believed to be importantfor programming high-performance parallel applications in practice. Hence a functional way to add side-effects without imposing
parallelism-destroying sequentiality may be of practical interest for
exploiting parallelism within these new architectures.

1. Introduction

1.1 Contributions and Overview

Adding side-effects to a purely functional language is a well-known
problem with a number of solutions [7, 9, 11, 15, 6, 1] with monads [10, 11, 7, 9] being arguably the most popular. In this paper,
we propose a new approach to this old problem by attacking itfrom a different angle. Instead of starting from a language theoretic point of view, we start by introducing a simple programming
feature called witnesses so that programs can explicitly order sideeffects. This feature is motivated by a pragmatic observation and isstraightforward. The catch is that, because it is so simple, it actually does not guarantee that a program is correct (i.e., that it can beviewed as a purely functional program). Instead, we argue that thefeature makes it easy for programmers to write correct programs.
We then formally state a natural semantic condition that is sufficient to guarantee correctness and give a static checking algorithm.
The result is a new framework for guaranteeing correctness of sideeffects in purely functional programs.
Besides arguably being more intuitive to programmers, our approach is more expressive than previous approaches. In particular,
our approach does not force side-effects to occur in a sequential

This paper makes the following contributions:∗ This research was supported in part by NASA Grant No. NNA04CI57A;NSF Grant Nos. CCR-0234689, CCR-0085949, and CCR-0326577. The
information presented here does not necessarily reflect the position or thepolicy of the Government and no official endorsement should be inferred.

Permission to make digital or hard copies of all or part of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor profit or commercial advantage and that copies bear this notice and the full citationon the first page. To copy otherwise, to republish, to post on servers or to redistributeto lists, requires prior specific permission and/or a fee.
ICFP’05 September 26–28, 2005, Tallinn, Estonia.
Copyright c 2005 ACM 1-59593-064-7/05/0009. . . $5.00.

• A simple language feature called witnesses that can be used toorder side-effects. (Section 2)• A semantic condition called witness race freedom for correct

usage of witnesses and a proof of its sufficiency. (Section 3)• An automatic algorithm for checking the afore-mentioned se-

mantic condition that makes use of a network flow property.
(Section 4)
The semantic condition is intuitive in the sense that it is directly
motivated by the implications of writing race-free programs. The
automatic algorithm is derived as a type inference algorithm fora substructural type system. The type system and its inference
problem are somewhat subtle and interesting in their own right.
Section 5 discusses related work. Section 6 concludes.

2. Preliminaries
We need a precise definition of what it means for side-effects to be“correct” within a functional language. A helpful idea is to showthat a program’s semantics is independent of a class of “functional”
program transformation rules. However, there is no consensus on
the right set of transformations. For example, the transformation(let x = e in e′ ) ≡ (e′ [x/e]) for x ∈/ free(e) is not always truein systems based on linear-types. (Here free(e) is the set of freevariables of e.)
To define correctness, we fix a set of program transformations
expressive enough to model different functional reduction strate1 But not easy, since there are other challenging issues such as selecting
the right granularity of parallelism, but these issues apply equally to otherlanguages and many solutions such as data-parallel operators and threadannotations already exist.

e

:=
|

x | i | λx.e | e e′ | let x = e in e′ | e ⊗ e′ | πi (e)write e1 e2 e3 | read e e′ | ref e | join e e′ | •E

Figure 1: The syntax of the language λwit .

App
Let

gies, including call-by-value, call-by-need (i.e., lazy-evaluation),and parallel evaluation.2 So, for example, a program that is invariant under this set of transformations evaluates to the same result
regardless of whether the evaluation order is call-by-value or callby-need. In parallel evaluation, invariance implies that a programis deterministic under any evaluation schedule.
For ease of exposition, we include the afore-mentioned programtransformations directly in the semantics as non-deterministic reduction rules. The correctness criteria then reduces to showing thata program is confluent with respect to this semantics. Also, for the
purpose of exposition, we restrict side-effects to imperative operations on first class references.
Figure 1 gives the syntax of λwit , a simple functional languagewith side-effects and witnesses. Note λwit has the usual features ofa functional language: variables x, integers i, function abstractions
λx.e, function applications e e′ , variable bindings let x = e in e′ ,pairs e ⊗ e′ , and projections πi (e) where i = 1 or i = 2. Bindings
let x = e in e′ can be recursive, i.e., x ∈ free(e). Three expression kinds work with references: reference writes write e1 e2 e3 ,reference reads read e e′ , and reference creations ref e. A read
read e e′ has a witness parameter e′ along with a reference parameter e such that it does not read the reference e until it sees thewitness e′ . (Section 3 defines the formal meaning of “seeing thewitness.”) Similarly, a write write e1 e2 e3 writes the expression
e2 to the reference e1 after it sees the witness e3 . After completionof the read, read e e′ returns a pair of the read value and a witness. Similarly, write e1 e2 e3 returns a witness after the write. In
general, any side-effect primitive returns a witness of performing
the corresponding side-effect; in the case of λwit , the side-effectprimitives are just write e1 e2 e3 and read e e′ .
Before describing the formal semantics of λwit , we describe
novel properties of λwit informally by examples.
Programs in λwit can use witnesses to order side-effects. For example, the following program returns 2 regardless of the evaluation
order because the read requires a witness of the write:
let x = (ref 1) in let w = (write x 2 •) in read x w(The symbol • is used for dummy witnesses.) On the other hand,
λwit does not guarantee correctness. For example, the following
λwit program has no ordering between the read and the write andhence may return 1 or 2 depending on the evaluation order:
let x = (ref 1) in let w = (write x 2 •) in read x •The expression kind join e e′ joins two witnesses by waiting
until it sees the witness e and the witness e′ and returning a witness. For example, the following program returns the pair 1 ⊗ 1
regardless of the evaluation order because the write waits until itsees witnesses of both reads:
let x = (ref 1) in
let y = (read x •) in let z = (read x •) inlet w = (write x 2 (join π2 (y) π2 (z))) in
π1 (y) ⊗ π1 (z)Note that the two reads may be evaluated in any order. In general,
witnesses are first class values and hence they can be passed to and
2 The results in Section 3 are general enough for most other functionaltransformations too, but the static checking algorithm requires a more
stringent definition.

:=
|
|

Pair
Write
Read
Ref
Join
ArriveGC

D ∪ {a 7→ E} | [ ] | E e | e E | E ⊗ e | e ⊗ E
πi (E) | write E e e′ | write e E e′ | write e e′ E
read e E | read E e | ref E | join E e | join e E(S, E[(λx.e) e′ ]) ⇒ (S, E[e[a/x]] ⊎ {a 7→ e′ })(S, E[let x = e in e′ ])⇒ (S, E[e′ [a/x]] ⊎ {a 7→ e[a/x]})(S, E[πi (e1 ⊗ e2 )]) ⇒ (S, E[ei ])(S, E[write ℓ e •]) ⇒ (S[ℓ ← a], E[•] ⊎ {a 7→ e})(S, E[read ℓ •]) ⇒ (S, E[S(ℓ) ⊗ •])(S, E[ref e]) ⇒ (S ⊎ {ℓ 7→ a}, E[ℓ] ⊎ {a 7→ e})(S, E[join • •]) ⇒ (S, E[•])(S, E[a] ⊎ {a 7→ e}) ⇒ (S, E[e] ⊎ {a 7→ e})
where e ∈ V(S, D ⊎ D′ ) ⇒ (S, D)
where ⋄ ∈/ dom(D′ ) ∧ dom(D′ ) ∩ free(D) = ∅Figure 2: The semantics of λwit .

returned from a function, captured in function closures, and evenwritten to and read from a reference. Witnesses are a simple featurethat can be used to order side-effects in a straightforward manner.
In the rest of this section, we describe the semantics of λwit
so that we can formally define when a λwit program is correct,
i.e., when it is confluent. Figure 2 shows the semantics of λwit ,which is defined via reduction rules of the form (S, D) ⇒ (S ′ , D′ )where S, S ′ are reference stores and D, D′ are expression stores.
A reference store is a function from a set of reference locations ℓ
to ports a, and an expression store is a function from a set of ports
to expressions. Here, expressions include any expression from thesource syntax extended with reference locations and ports. Given a
program e, evaluation of e starts from the initial state (∅, {⋄ 7→ e})
where the symbol ⋄ denotes the special root port. Ports are used
for evaluation sharing.3 The reduction rules are parametrized by
the evaluation contexts E. For an expression e, free(e) is the set offree variables, ports, and reference
S locations of e. For an expression
store D, free(D) = dom(D) ∪ e∈ran(D) free(e).
We briefly describe the reduction rules from top-to-bottom. The
rule App corresponds to a function application. For functions F
and F ′ , F ⊎ F ′ denotes F ∪ F ′ if dom(F ) ∩ dom(F ′ ) = ∅and is undefined otherwise. Thus App creates a fresh port a andstores e′ at a. The rule Let is similar. The rule Pair projects theith element of the pair. The rule Write creates a fresh port a,stores the expression e′ at the port a, and stores the port a at
the reference location ℓ. We use S[ℓ ← a] as a shorthand for{ℓ′ 7→ S(ℓ′ ) | ℓ′ ∈ dom(S) ∧ ℓ′ 6= ℓ} ∪ {ℓ 7→ a}. Note that we use
the dummy witness symbol • as the run-time representation of any
witness because only its presence is important to the semantics,
i.e., operationally, a witness is like a dataflow token in dataflow
machines. The rule Read reads from the reference location ℓ and,as noted above, returns the value paired with a witness. The rule
Ref creates a fresh location ℓ and a fresh port a, initializes a to theexpression e and ℓ to the port a. The rule Join takes two witnesses
and returns one witness.
The rule Arrive might look somewhat unfamiliar. Here V isthe set of “safe to duplicate” expressions. Partly for the sake of thestatic-checking algorithm to be presented later, we fix V to values
generated by the following grammar:
v := x | i | a | • | ℓ | v ⊗ v ′ | λx.e
3 In the literature, top-level let-bound variables often double as variables
and ports.

Arrive says that if e is safe to duplicate, then we can replace aby e; we say a safe to duplicate expression has arrived at port
a. In essence, while standard operational semantics for functional
languages [12, 8] implicitly combine Arrive with other rules, we
separate Arrive for increased freedom in the evaluation order.
Lastly, the rule GC garbage-collects unreachable (from the root
port ⋄) portions of the expression store.
Here is an example of a λwit evaluation:(∅, {⋄ 7→ (λx.read x •) ref 1})⇒ ({ℓ 7→ a}, {⋄ 7→ (λx.read x •) ℓ, a 7→ 1})⇒ ({ℓ 7→ a}, {⋄ 7→ read a′ •, a 7→ 1, a′ 7→ ℓ})⇒ ({ℓ 7→ a}, {⋄ 7→ read ℓ •, a 7→ 1, a′ 7→ ℓ})⇒ ({ℓ 7→ a}, {⋄ 7→ a ⊗ •, a 7→ 1, a′ 7→ ℓ})⇒ ({ℓ 7→ a}, {⋄ 7→ 1 ⊗ •, a 7→ 1, a′ 7→ ℓ})⇒ ({ℓ 7→ a}, {⋄ 7→ 1 ⊗ •})Ref
AppArriveRead
ArriveGC

The semantics is non-deterministic and therefore also allows otherreduction sequences for the same program. For example, we may
take an App step immediately instead of first creating a new reference by a Ref step:(∅, {⋄ 7→ (λx.read x •) ref 1})⇒ (∅, {⋄ 7→ read a •, a 7→ ref 1})

App

Before defining confluence, we point out several important
properties of this semantics. Firstly, note that the evaluation contexts E do not extend to subexpressions of a λ abstraction λx.e,i.e., we do not reduce under λ. The evaluation contexts also do notextend to subexpressions of an expression let x = e in e′ , bute and e′ may become available for evaluation via applications of
the Let rule. As with call-by-value evaluation or call-by-need evaluation, evaluation of an expression is shared. For example, in the
program (λx.x ⊗ x) e, the expression e is evaluated at most once.
The semantics of λwit has strictly more freedom in evaluation
order than both call-by-value and call-by-need. In particular, callby-need evaluation can be obtained by using the same reduction
rules but restricting the evaluation contexts to the following
E

:=
|
|

D ∪ {⋄ 7→ E} | [ ] | E e | πi (E) | write E e e′
write ℓ e E | read E e | read ℓ E
join E e | join • E

Call-by-value evaluation can be obtained by adding the following
contexts to the evaluation contexts of the call-by-need evaluation
E:=|. . . | (λx.e) E | E ⊗ e | v ⊗ E | write ℓ E •ref E |let x = E in e

in addition to restricting the rule App to the case e′ ∈ V , the rule
Let to the case e ∈ V , the rule Pair to the case e1 , e2 ∈ V , therule Write to the case e′ ∈ V , and the rule Ref to the case e ∈ V .4
Note that both lazy writes and strict writes are possible in λwit .
It is important to understand that we are only concerned withside-effects via references, and hence we are not concerned about
issues like the number of ports that are created during an evaluation.
Having defined the semantics, we can formally define when a
λwit program is confluent. To this end, we define observational
equivalence as the smallest reflexive and transitive relation D ≈D′ on expression stores satisfying:• D ≈ D[a/a′ ] where a ∈/ free(D)• D ≈ D[ℓ/ℓ′ ] where ℓ ∈/ free(D)That is, expression stores are observationally equivalent if they areequivalent up to consistent renaming of free ports and reference
locations. Let ⇒∗ be a sequence of zero or more ⇒.
4 Strictly speaking, the context let x = E in e is not in the semantics of
λwit . But λwit can simulate the behavior via a Let step and then reducing
e[a/x] which is now in an evaluation context.

D EFINITION 1 (Confluence). A program state (S, D) is confluent
if for any two states (S1 , D1 ) and (S2 , D2 ) such that (S, D) ⇒∗(S1 , D1 ) and (S, D) ⇒∗ (S2 , D2 ), there exist two states (S1′ , D1′ )and (S2′ , D2′ ) such that (S1 , D1 ) ⇒∗ (S1′ , D1′ ), (S2 , D2 ) ⇒∗(S2′ , D2′ ), and D1′ ≈ D2′ . A program e is confluent if its initialstate (∅, {⋄ 7→ e}) is confluent.
Note that the definition does not require any relation between reference location stores S1′ and S2′ . So, for example, a program thatwrites but never reads would be confluent. As shown before, λwit
contains programs that are not confluent. Indeed, the difference
between call-by-need and call-by-value is enough to demonstratenon-confluence:(λx.read x •) (let x = (ref 1) in let y = (write x 2 •) in x)
The above program evaluates to the pair 1 ⊗ • under call-by-needand to the pair 2 ⊗ • under call-by-value. No further reductions canmake the two states observationally equivalent. (Here we implicitly
read back the top-level expression from the root port instead of
showing the actual expression stores for brevity.)
We have shown earlier that witnesses can aid in writing correct
programs by directly ordering side-effects. Witnesses are first classvalues and hence can be treated like other expressions. For example, the program below captures a witness in a function which itself
returns a witness to ensure that reads and writes happen in a correct
order:
let x = ref 1 in
let w = write x 2 • inlet f = λy.read x w inlet z = (f 0) ⊗ (f 0) in
let w = write x 3 join π2 (π1 (z)) π2 (π2 (z)) in z
Note that a witness of the first write is captured in the function f .
Hence both reads from the two calls to f see a witness of the write.
A witness of each read is returned by f , and the last write waits
until it sees witnesses from both reads. Therefore, the result of the
program is (2⊗•)⊗(2⊗•) regardless of the evaluation order. Notethat the two calls to f , and thus the reads in the calls, can occur ineither order.

3. Witness Race Freedom
As discussed in Section 2, witnesses aid in writing correct programsin the presence of side-effects but do not enforce correctness. In thissection, we give a sufficient condition for guaranteeing confluence.
The guideline for writing a correct program should be intuitively
clear at this point: we ensure that reads and writes happen in somerace-free order by partially ordering them via witnesses. We now
make this intuition more precise. First, we formally define what wemean by the phrase “ side-effect A sees a witness of side effect B”
that we have used informally up to this point.
Intuitively, a trace graph is a program trace with all information
other than reads, writes, and witnesses elided. There are three kindsof nodes: read nodes read(ℓ), write nodes write(ℓ), and the joinnode join. Read and write nodes are parametrized by a reference
location ℓ. There is a directed edge (A, B) from node A to node
B if B directly sees a witness of A. A trace graph (V, E) isconstructed as the program evaluates a modified semantics:
Write
Read
Join

(S, E[write ℓ e A]) ⇒ (S[ℓ ← a], E[B] ⊎ {a 7→ e})
V:=V ∪ {B} where B is a new write(ℓ) node
E:=E ∪ {(A, B)}(S, E[read ℓ A]) ⇒ (S, E[S(ℓ) ⊗ B])
V:=V ∪ {B} where B is a new read(ℓ) node
E:=E ∪ {(A, B)}(S, E[join A B]) ⇒ (S, E[C])
V:=V ∪ {C} where C is a new join node
E:=E ∪ {(A, C), (B, C)}

Note that we now use nodes as witnesses instead of •. The line below each reduction rule shows the graph update action corresponding to that rule. The other rules remain unmodified and hence haveno graph update actions. An evaluation starts with V = E = ∅and performs the corresponding graph update when taking a Write
step, a Read step, or a Join step. Notice that a trace graph and theannotated semantics are only needed to state the semantic condition
for correctness and are not needed in the actual execution of a λwit
program.
We can now define what it means for a node A to see a witnessof a node B, a notion we have used informally until now.
D EFINITION 2. Given a trace graph, we say that a node A sees
a witness of a node B if there is a path from B to A in the tracegraph. We write B ; A.
The following is a trivial observation:
T HEOREM 1. If B ; A in a trace graph, then the side effectcorresponding to B must have happened before the side effectcorresponding to A in the evaluation that generated the tracegraph.
Clearly, any trace graph is acyclic.
Having defined trace graphs and the ; relation, we are now
ready to state the semantic condition for correctness. Before showing the condition formally, we informally motivate it by making
analogies to the conventional programming guideline for writing
correct concurrent programs: prevent race conditions.
We first note that a program could produce different trace graphs
depending on the choice of reductions, even when those tracegraphs are from terminating evaluations. Furthermore, it is not necessarily the case that such a program is non-confluent. Therefore,
instead of trying to argue about confluence by comparing different
trace graphs, we shall define a condition that can be checked byobserving each individual trace graph in isolation.
Let us write A : nodetype as a shorthand for a node A of type
nodetype. If we have A : read(ℓ) and B : write(ℓ), then we want
either A ; B or B ; A to ensure that A always happens before
B or B always happens before A because otherwise we may geta read-write race condition due to non-determinism. Also, for any
A : read(ℓ), if there are two nodes B1 , B2 : write(ℓ) such thatneither B1 ; B2 nor B2 ; B1 (so we do not know which write
occurs first) and A could happen after both B1 and B2 , then wewant C : write(ℓ) such that C ; A, B1 ; C and B2 ; C,because otherwise the read at A might depend on whether theevaluation chose to do B1 first or B2 first, i.e., we have anotherkind of race-condition. Perhaps somewhat surprisingly, satisfying
these two conditions turns out to be sufficient to ensure confluence.
We now formalizes this discussion. For B : write(ℓ), we use the!
shorthand B ; A if for any C : write(ℓ) such that C ; A andC 6= B, we have C ; B. Now, for any A : read(ℓ), there exists!
at most one B : write(ℓ) such that B ; A. Note that the second
condition above is equivalent to requiring that for any A : read(ℓ),
either there is no B : write(ℓ) such that B ; A or there is a!
B : write(ℓ) such that B ; A

A1 a

O

O !
O


a! a!

A2

A1

O

O

a! a!

B1

O !
O


B2
(a)

O !
O =}


=}
=} }=

B1

= A2
O
O !
O

B2

(b)

Figure 3: Possible orderings between pairs of reads and writes in awitness race free trace graph.
D EFINITION 3 (Witness Race Freedom). We say that a trace graph(V, E) is witness race free if for every location ℓ,• for every A : read(ℓ) ∈ V and B : write(ℓ) ∈ V, either

A ; B or B ; A, and• for every A : read(ℓ) ∈ V, either there is no B : write(ℓ) ∈ V

such that B ; A or there is a B : write(ℓ) ∈ V such that!
B ; A.
We say that a program e is witness race free if every trace graph ofe is witness race free.
T HEOREM 2. If e is witness race free then e is confluent.
The proof appears in our companion technical report [13].
While witness race freedom is a sufficient condition, it is notnecessary. For example, if for each reference location writes happen
to never change the location’s value, then the program is triviallyconfluent regardless of the order of reads and writes. Anotherexample is a program using implicit order of evaluation: e.g., in
λwit , expressions are not reduced under λ so a function body isevaluated only after a call. Hence a program that stores a function
in a reference location, reads the reference location to call thefunction, and then writes in the same reference location from thebody of the called function is confluent because the write always
happens after the read despite the write not seeing the witness of
the read.
Nevertheless, witness race freedom is “almost complete” in asense that if the only way to order two side-effects is to make one
see a witness of the other, and if we cannot assume anything about
what expressions are written and how the contents are used, then itis the weakest condition guaranteeing correctness. In particular, if
the trace graphs are the only information available about a program,then witness race freedom becomes a necessary condition.
The result in this section can be extended to most other functional program transformations, because witness race freedom isan entirely semantic condition. However, the static checking algorithm described in Section 4 is not as forgiving, which is why wehave restricted the set of program transformations to that of the semantics of λwit . For example, the algorithm is unsound for generalcall-by-name reduction.

4. Types for Statically Checking Witness Race
Freedom
While the concept of witnesses is straightforward, it may nevertheless be desirable to have an automated way of checking whether anarbitrary λwit program is witness race free. Witness race freedom
may be checked directly by checking every program trace, whichis computationally infeasible. Instead, we exploit a special property of witness-race-free trace graphs to design a sound algorithm
that can efficiently verify a large subset of witness-race-free λwit
programs.
The key observation is that any witness-race-free trace graphcontains for each reference location ℓ a subgraph that we shall call

e
R1

W1

A1

R2

W2

A2

R3

:=
|
|

x | i | λx.e | e e′ | let x = e in e′ | e ⊗ e′ | πi (e)write e1 e2 e3 | read e e′ | ref e e′ | join e e′ | •letreg x e
Figure 5: The syntax of λregwit .

Figure 4: A read-write pipeline with bottlenecks for a reference
location ℓ.
a read-write pipeline with bottlenecks. We shall design an algorithm
that detects these subgraphs instead of directly checking the witness
race freedom condition. Consider a witness-race-free trace graph.
Suppose there are A1 , A2 : write(ℓ) and B1 , B2 : read(ℓ) such!
!
that A1 6= A2 , A1 ; B1 and A2 ; B2 . Due to witness race
freedom, it must be the case that B2 ; A1 or A1 ; B2 . If theformer is the case, we have the relation as depicted in Figure 3 (a).
!
Suppose that the latter is the case. Then, since A2 ; B2 , it must
be the case that A1 ; A2 . Consider A2 and B1 . Due to witness
race freedom again, it must be the case that either A2 ; B1 or!
B1 ; A2 . But if A2 ; B1 , then since A1 ; B1 , it must be thecase that A2 ; A1 . But this is impossible since A2 ; A1 ; A2
forms a cycle. So it must be the case that B1 ; A2 , and we havethe relation as depicted in Figure 3 (b).
Further reasoning along this line of thought reveals that fora witness-race-free trace graph, for any reference location ℓ, the!
nodes in the set X = {A : write(ℓ) | ∃B : read(ℓ).A ; B}
are totally ordered (with ; as the ordering relation), and thatthese nodes partition all read(ℓ) nodes and write(ℓ) nodes in a way
depicted in Figure 4 where X = {A1 , . . . , An }. In the figure, each
Ri and Wi is a collection of nodes. No Ri contains a write(ℓ) nodeand no Wi contains a read(ℓ) nodes. Each Ai is one write(ℓ) node.
An arrow from X to Y means that there is a path from each write(ℓ)
node or read(ℓ) node in X to each write(ℓ) node or read(ℓ) nodein Y , except if a Wi contains no such node, then there is a pathfrom each read(ℓ) ∈ Ri to Ai . Each Ri for i 6= 1 must containat least one read(ℓ). Arrows just imply the presence of paths, andhence there can be more paths than the ones implied by the arrows,e.g., paths to/from nodes that are not in the diagram, paths to andfrom nodes in the same collection, and even paths relating thecollections in the diagram such as one that goes directly from Ri to
Ai , bypassing Wi .
The graph in Figure 4 can be described formally as a subgraphof the trace graph satisfying certain properties.
D EFINITION 4. Given a trace graph (V, E) and a reference location ℓ, we call its subgraph Gℓ a read-write pipeline with bottlenecks if Gℓ consists of collections of nodes R1 , R2 , . . . , Rn and
W1 , W2 , . . . , Wn with the following properties:
S• {A | A : read(ℓ) ∈ V} ⊆ nR,
Si=1 i• {A | A : write(ℓ) ∈ V} ⊆ ni=1 Wi ,• R1 , . . . , Rn , W1 , . . . , Wn , restricted to write(ℓ) nodes andread(ℓ) nodes are pairwise disjoint,• for each A : read(ℓ) ∈ Ri and B : write(ℓ) ∈ Wi , A ; B,
• for each Ri such that i 6= 1, there exists at least one A :read(ℓ) ∈ Ri , and• there exists A : write(ℓ) ∈ Wi for all i 6= n such that for all!
B : read(ℓ) ∈ Ri+1 and all C : write(ℓ) ∈ Wi , A ; B andC ; A.
Note that each collection Ri and Wi corresponds to the collectionof nodes marked by the same name in Figure 4 but with each

E

:=
|
|
|

App
Let
Pair
Write
Read
Ref
Join
LetRegArriveGC

D ∪ {a 7→ E} | [ ] | E e | e E | E ⊗ e | e ⊗ E
πi (E) | write E e e′ | write e E e′ | write e e′ E
read e E | read E e | ref E e | ref e E
join E e | join e E(R, S, E[(λx.e) e′ ])⇒ (R, S, E[e[a/x]] ⊎ {a 7→ e′ })(R, S, E[let x = e in e′ ])⇒ (R, S, E[e′ [a/x]] ⊎ {a 7→ e[a/x]})(R, S, E[πi (e1 ⊗ e2 )]) ⇒ (R, S, E[ei ])(R, S, E[write ℓ e •]⇒ (R, S[ℓ ← a], E[•] ⊎ {a 7→ e})(R, S, E[read ℓ •]) ⇒ (R, S, E[S(ℓ) ⊗ •])(R, S, E[ref e r])⇒ (R, S ⊎ {ℓ 7→ a}, E[ℓ] ⊎ {a 7→ e})(R, S, E[join • •]) ⇒ (R, S, E[•])(R, S, E[letreg x e])⇒ (R ⊎ {r}, S, E[e[a/x]] ⊎ {a 7→ r})(R, S, E[a] ⊎ {a 7→ e}) ⇒ (R, S, E[e] ⊎ {a 7→ e})
where e ∈ V(R, S, D ⊎ D′ ) ⇒ (R, S, D)
where ⋄ ∈/ dom(D′ ) ∧ dom(D′ ) ∩ free(D) = ∅Figure 6: The semantics of λreg
wit .

node Ai included in the collection Wi . The “bottlenecks” arethe Ai ’s. Note that a trace graph (V, E) actually contains a readwrite pipeline with bottlenecks per each reference location ℓ as a
subgraph Gℓ (but the subgraphs may not be disjoint because thepaths may involve other locations and share join nodes).
The following theorem formalizes our earlier informal discussion.
T HEOREM 3. A trace graph (V, E) is witness race free if and only
if it has a read-write pipeline with bottlenecks for every ℓ.
The proof appears in our companion technical report [13]. The
following is an immediate consequence:
C OROLLARY 1. A λwit program e is witness race free if and only
if every trace graph of e has a read-write pipeline with bottlenecks
for every reference location ℓ.
4.1 Regions
Corollary 1 reduces the problem of deciding whether a program e
is witness race free to the problem of deciding if every trace graphof e has a read-write pipeline with bottlenecks for every reference
location ℓ. Therefore it suffices to design an algorithm for solving
the latter problem. But before we do so, we make a slight change
to λwit to make the problem more tractable. In λwit , there is a readwrite pipeline with bottlenecks for each reference location ℓ, but
distinguishing dynamically allocated reference locations individually is difficult for a compile-time algorithm. Therefore, we add
regions to the language so that programs can explicitly group reference locations that are to be tracked together.
Figure 5 shows λreg
wit , λwit extended with regions. The syntax
contains two new expression kinds: letreg x e which creates anew region and ref e e′ which places the newly created reference
in region e′ ; ref e e′ replaces ref e. Figure 6 gives the semantics of
λreg
wit which differs from λwit in two small ways. First, a state now
contains a set of regions R. We use symbols r, r ′ , ri , etc. to denoteregions. Regions are safe to duplicated, i.e., r ∈ V . The R’s areused only for ensuring that the newly created region r at a LetReg
step is fresh. (We overload the symbol ⊎ such that R⊎R′ = R∪R′
if R ∩ R′ = ∅ and, is undefined otherwise.) Note that evaluation
contexts E do not extend to the subexpressions of letreg x e. The
second difference is that a Ref step now takes a region r along with
the initializer e to indicate that the newly created reference locationℓ belongs to the region r. Note that the semantics does not actuallyassociate the reference location ℓ and the region r, and therefore
grouping of reference locations via regions is entirely conceptual.5
Regions force programs to abide by witness race freedom at
the granularity of regions instead of at the granularity of individualreference locations. That is, instead of read(ℓ) nodes and write(ℓ)
nodes, we use read(r) nodes and write(r) nodes. Formally, a tracegraph for λreg
wit is constructed by the following graph construction
semantics:
Write

Read
Join
Ref

(R, K, S, E[write ℓ e A])⇒ (R, K, S[ℓ ← a], E[B] ⊎ {a 7→ e})
V:=V ∪ {B} where B is a new write(K(ℓ)) node
E:=E ∪ {(A, B)}(R, K, S, E[read ℓ A]) ⇒ (R, K, S, E[S(ℓ) ⊗ B])
V:=V ∪ {B} where B is a new read(K(ℓ)) node
E:=E ∪ {(A, B)}(R, K, S, E[join A B]) ⇒ (R, K, S, E[C])
V:=V ∪ {C} where C is a new join node
E:=E ∪ {(A, C), (B, C)}(R, K, S, E[ref e r])⇒ (R, K ⊎ {ℓ 7→ r}, S ⊎ {ℓ 7→ a}, E[ℓ] ⊎ {a 7→ e})Note that these reduction rules use an additional function K which
is a mapping from reference locations to regions. The mapping K
starts empty at the beginning of evaluation. Other reductions rules
are unmodified except that the function K is passed from left toright in the obvious way.
Since there is less information available in a λreg
wit trace graphthan in a λwit trace graph, the witness race freedom condition ismore conservative for λreg
wit . That is, we still need the condition
that for any A : write(r) and B : read(r), either A ; B or
B ; A. But we need to tighten the second condition so that for
any A : read(r) if there are B1 , B2 : write(r) such that B1 ; A
and B2 ; A, then either B1 ; B2 or B2 ; B1 . This condition isstrictly more conservative than for λwit , which only requires some!
C : write(r) such that C ; A in such a situation. The reason forthis conservativeness is that we do not know from a trace graph of
λreg
wit whether B1 and B2 both write to the same reference location.
Formally, witness race freedom for λreg
wit can be defined as follows.
D EFINITION 5 (Witness Race Freedom for λregwit ). We say that a
λreg
wit trace graph (V, E) is witness race free if for every region r,• for every A : read(r) ∈ V and B : read(r) ∈ V, either A ; B

or B ; A, and• for every A : read(r) ∈ V and B1 , B2 : write(r) ∈ V suchthat B1 ; A and B2 ; A, we have B1 ; B2 or B2 ; B1 .
T HEOREM 4. If a λreg
wit program e is witness race free, then e isconfluent.
5 Regions are traditionally coupled with some semantic meaning such as
memory management [14, 5]. It is possible to extend λreg
wit to do similar
things with its regions.

Proof (Sketch): For any evaluation of e, carry out the same reduction sequence with the trace graph building action of λwit , i.e., thetrace graph G generated is at the granularity of reference locations.
Then it is easy to see that if G satisfies the above two conditions, G
also satisfies the two conditions of Theorem 2. 2
It is easy to see that Definition 5 is the weakest possible restriction to the original witness race freedom under the region abstraction because for any λreg
wit trace graph that is not witness race
free, one can easily find a non-confluent program that produces thegraph.
In a witness-race-free trace graph for λreg
wit , the read-write
pipeline with bottlenecks for a region r consisting of the collections (R1 , . . . , Rn , W1 , . . . , Wn ) has the following property: eachset {A | A : write(r) ∈ Wi } for i 6= n can be totally ordered (with; as the ordering relation). The theorem below is immediate from
Corollary 1 under this additional property.
T HEOREM 5. A λreg
wit program e is witness race free if and only ifevery trace graph of e has a read-write pipeline with bottlenecks
for every region r.
This additional property helps in designing a static checking algorithm.
4.2 From Network Flow to Types
Now our goal is to design an algorithm for statically checking if
every trace graph of a λreg
wit program e has a read-write pipeline withbottlenecks for every region r. Our approach exploits a network
flow property of read-write pipelines with bottlenecks. Consider
a trace graph as a network of nodes with each edge (A, B) able
to carry any non-negative flow from A to B. (Recall edges are
directed.) As usual with network flow, we require that the total
incoming flow equal the total outgoing flow for every node in thegraph. Now, let us add a virtual source node AS and connect it
to every node B by adding an edge (AS , B). We assign incoming
flow 1 to AS . Then it is not hard to see that if there exists a readwrite pipeline with bottlenecks for the region r then there exists
flow assignments such that every read(r) node and write(r) node
gets a positive flow and every A : write(r) ∈ Wi for i 6= n gets aflow equal to 1.
It turns out that the converse also holds. That is, given a tracegraph, if there is a flow assignment such that each read(r) node andwrite(r) node gets a positive flow and each A : write(r) such that
there exists B : read(r) with A ; B gets a flow equal to 1, thenthere is a read-write pipeline with bottlenecks for the region r. By
Theorem 5, this implies that there exists such a flow assignment forevery region r if and only if the trace graph is witness race free.
Because edges in a trace graph are traces of witnesses, our idea
is to assign a type to a witness such that the type contains flow
assignments for each (static) region. We use this idea to design atype system such that a well-typed program is guaranteed to bewitness race free.
Formally, a witness type W is a function from the set of static
region identifiers RegIDs to rational numbers in the range [0, 1],
i.e., W : RegIDs → [0, 1]. The rational number W (ρ) indicatesthe flow amount for the static region identifier ρ in the witness type
W . We use the notation {ρ1 7→ q1 , . . . , ρn 7→ qn } to mean awitness type W such that W (ρ) = qi if ρ = ρi for some 1 ≤ i ≤ n
and W (ρ) = 0 otherwise. (We use the symbols q, qi , q ′ , etc for
non-negative rational numbers, including those larger than 1.)
The rest of the types are defined in Figure 7, including typesqinclude integer types int, function types τ → τ ′ , pair types τ ⊗ τ ′ ,′reference types ref (τ, τ , ρ), and region types reg(ρ). The nonq
negative rational number q in τ → τ ′ represents the number oftimes the function can be called. We allow the symbols q, q ′ , etc

τ

:=

q

int | τ → τ ′ | τ ⊗ τ ′ | ref (τ, τ ′ , ρ) | reg(ρ) | W

reg(ρ) + reg(ρ) = reg(ρ)
int + int = int
qFigure 7: The type language.

Γ; W ⊢ e : ττ ≥ τ′
Γ; W ⊢ e : τ ′Γ; W ⊢ i : intIntΓ(x) = τΓ; W ⊢ x : τSubΓ, x:τ ; W ⊢ e : τ

q+q ′

q′

q ′ ×qτ → τ′ × q = τ → τ′τ ⊗ τ ′ × q = (τ × q) ⊗ (τ ′ × q)
ref (τ, τ ′ , ρ) × q = ref (τ × q, τ ′ , ρ)W × q = {ρ 7→ W (ρ) × q | ρ ∈ RegIDs}

Dummy

Γ; W ⊢ • : ∅Γ; W1 ⊢ e : W2
Γ; W1 + W3 ⊢ e : W2 + W3

Var

q′

τ → τ′ + τ → τ′ = τ → τ′
τ1 ⊗ τ2 + τ3 ⊗ τ4 = (τ1 + τ3 ) ⊗ (τ2 + τ4 )
ref (τ1 , τ, ρ) + ref (τ2 , τ, ρ) = ref (τ1 + τ2 , τ, ρ)
W + W ′ = {ρ 7→ W (ρ) + W ′ (ρ) | ρ ∈ RegIDs}reg(ρ) × q = reg(ρ)
int × q = int

SourceFigure 9: Arithmetic over types.

′qΓ × q; W × q ⊢ λx.e : τ → τ ′q

Γ; W ⊢ e : τ → τ ′Γ′ ; W ′ ⊢ e ′ : τ′Γ + Γ ; W + W ′ ⊢ e e′ : τ ′

Abs

q≥1

Γ; W ⊢ e : τΓ′ ; W ′ ⊢ e ′ : τ ′′′Γ + Γ ; W + W ⊢ e ⊗ e′ : τ ⊗ τ ′Γ; W ⊢ e : τ1 ⊗ τ2
Γ; W ⊢ πi (e) : τi

App

Pair

Proj

Γ; W ⊢ e : τΓ′ ; W ′ ⊢ e′ : reg(ρ)′′Γ + Γ ; W + W ⊢ ref e e′ : ref (τ, τ, ρ)RefΓ1 ; W1 ⊢ e1 : ref (τ, τ ′ , ρ)
Γ2 ; W 2 ⊢ e 2 : τ ′Γ3 ; W 3 ⊢ e 3 : W
W (ρ) ≥ 1
Γ1 + Γ2 + Γ3 ; W1 + W2 + W3 ⊢ write e1 e2 e3 : W
Γ; W1 ⊢ e : ref (τ, τ ′ , ρ)
Γ ; W 2 ⊢ e′ : W
W (ρ) > 0
Γ + Γ′ ; W1 + W2 ⊢ read e e′ : W ⊗ τ(Γ, x:τ ) × q = (Γ × q), x:(τ × q)
Write

′

Γ, x:reg(ρ); W + {ρ 7→ q} ⊢ e : τq≤1ρ∈/ free(Γ) ∪ free(W ) ∪ free(τ )Γ; W ⊢ letreg x e : τ

Read

LetRegion

Γ; W1 ⊢ e : W
Γ; W2 ⊢ e′ : W ′′Γ + Γ ; W1 + W2 ⊢ join e e′ : W + W ′Γ; W ⊢ e′ [(let x = e in x)/x] : τe∈V+′Γ; W ⊢ let x = e in e : τΓ, x:τ ; W ⊢ e : τΓ′ , x:τ ; W ′ ⊢ e′ : τ ′τ ≥ τ × ∞ if x ∈ free(e)Γ + Γ′ ; W + W ′ ⊢ let x = e in e′ : τ ′right, except for the rule Sub which we defer to the end. The rules
Var and Int are standard. The rule Dummy gives a dummy witness• an empty witness type; note that ∅(ρ) = 0 for any static region
identifier ρ.
The rule Source uses additive arithmetic over types defined in
Figure 9. The rule adds W3 amount of flow from the virtual source
nodes (i.e., nodes AS from the first paragraph of this section) toW2 . In the type judgment relation Γ; W ⊢ e : τ , the witness type
W represents the flow the expression e receives from the virtual
source nodes. Therefore, the rule Source says that assuming that
we took W1 flow from the virtual source nodes in the precondition,
we are now taking W3 more.
In the rule Abs, we multiply the left hand side of the judgments
by the number of times that the function can be used. Multiplication
over type environments Γ is defined as follows:
So for example, if the λ abstraction λx.e captures a witness as afree variable y and that Γ(y) = W , then (Γ × q)(y) = W × q.
Thus if the function body requires W amount of flow in the witness,then we actually require W ×q amount of flow because the function
may be called q times.
In the rule App, the precondition q ≥ 1 says that the number oftimes the function can be used must be at least 1. The left hand sideof the two judgments in the precondition are added so that we cancompute the combined flow required for the expressions e and e′ .
Addition over type environments is defined as follows:(Γ, x:τ ) + (Γ′ , x:τ ′ ) = (Γ + Γ′ ), x:(τ + τ ′ )

Join

LetA

LetB

Figure 8: Type judgment rules.

to take the valuation ∞ to imply that the function can be called
arbitrarily many times. We use the following arithmetic relation:
q + ∞ = ∞, q × ∞ = ∞ for q 6= 0, and 0 × ∞ = 0.
Figure 8 shows the main type judgment rules. Our type systembelongs to the family of substructural type systems, which includes
linear types. We discuss the rules from top-to-bottom and left-to-

The rules Pair and Proj are self-explanatory.
In a reference type ref (τ, τ ′ , ρ), the static region identifier ρ
identifies the region where the reference belongs while the type τ isthe read type of the reference and the type τ ′ is the write type of thereference. Initially the read and write types are the same as seen in
the rule Ref. The rule Write matches the type of the to-be-assigned
expression e2 with the write type of the reference while the rule
Read uses the read type of the reference type. Note that we require
W (ρ) ≥ 1 at Write and W (ρ) > 0 at Read; both correspond to theflow requirement for writes and reads. The reason read-type/writetype separation is subtle. Consider the following expression where
the expressions e1 and e3 are witnesses and the expression e2 is aregion:let x = (ref e1 e2 ) in let w = (write x e3 •) in read x w
Suppose we just have read types so that the type system uses readtypes at instances Write as well as at instances Read. Then the typesystem is unsound (even without Sub) for the following reason.
The type system may assign some flow W to the occurrence ofτ1 ≤ τ1′τ ≥τ

τ2 ≥ τ2′q

q ≥ q′

Fresh(int) = intβ′Fresh(σ→σ) = Fresh(σ) → Fresh(σ)
where β is fresh
Fresh(σ ⊗ σ ′ ) = Fresh(σ) ⊗ Fresh(σ)
Fresh(ref (σ, σ ′ , ρ)) = ref (Fresh(σ), Fresh(σ ′ ), ρ)
Fresh(reg(ρ)) = reg(ρ)
Fresh(I) = {ρ 7→ α | ρ ∈ I}
where α is freshqτ1 → τ2 ≥ τ1′ → τ2′

τ1 ≥ τ1′τ2 ≥ τ2′τ1 ⊗ τ2 ≥ τ1′ ⊗ τ2′
τ1 ≥ τ1′τ2 ≤ τ2′
ref (τ1 , τ2 , ρ) ≥ ref (τ1′ , τ2′ , ρ)W (ρ) ≥ W (ρ) for all ρ ∈ RegIDs
W ≥ W′

Figure 11: Fresh.

Figure 10: Subtyping.

Γ, W ⊢b eI : τ, C
Γ, W + Fresh(I) ⊢a eI : τ + Fresh(I), C

the variable x at the write and some flow W ′ to the occurrenceof the variable x at the read. But there is no constraint to force
W = W ′ , so the type system can let W ′ > W while keeping
the sum W + W ′ fixed, i.e., we get more flow from a reference
than what was assigned to the reference. Separating read and write
types prevents this problem because addition and multiplication do
not act on write types.
The rule LetRegion introduces a fresh static region identifier ρ.
The witness type {ρ 7→ q} represents the virtual source node forthe new region. We constrain q ≤ 1 to ensure that we do not use
more than 1 unit total from the source.
The rule Join combines two witnesses by adding their types.
There are two rules, LetA and LetB, for the expression kind
let x = e in e′ . LetA is less conservative and should be usedwhenever x occurs more than once in e′ and e ∈ V + where V + isthe smallest set such that V + = V ∪ {let x = e in x | e ∈ V + }.
This rule corresponds to the usual substitution interpretation of letbased predicative polymorphism with the value restriction. LetB isused if e ∈/ V + or x occurs at most once in e′ . Here, free(τ ) is theset of static region identifiersSin the type τ where free(W ) = {ρ |W (ρ) 6= 0}, and free(Γ) = τ ∈ran(Γ) free(τ ).
Finally, we come return to Sub. The subtyping relation is defined in Figure 10. As usual, argument types of function types arecontravariant. Write types of reference types are also contravariant;this treatment of reference subtyping is identical to that of a typebased formulation of Andersen’s points-to analysis [4]. Intuitively,
the rule Sub expresses the observation that the flow graph property
may be relaxed so that the sum of the outgoing flow can be lessthan the sum of the incoming flow, i.e., if we could find a flow assignment satisfying the required flow constraints at reads and writes
under this relaxed condition, then we still have a read-write pipeline
with bottlenecks.
We say that a λreg
wit program e is well-typed if ∅; ∅ ⊢ e : τ forsome type τ . The following theorem states that the type system issound.

Γ, W ⊢b eσ : τ, Cσ∈
/ type I
Γ, W ⊢a eσ : τ, C

T HEOREM 6. If a λreg
wit program e is well-typed, then it is witness
race free.
The proof, which uses the network flow property, appears in thecompanion technical report [13].
We point out a few of the positive properties of this type system.
If a program contains no reads or writes and can be typed by astandard Hindley-Milner polymorphic type system, then it can also
be typed by our type system; for example, we may use the qualifier∞ for all function types and use 0 for all flows. In general, we cangive the ∞ qualifier to the function type of any function that does
not capture a witness (directly or indirectly). We can also assign
flow 0 to any flow for a region r that does not flow into a sideeffect primitive operating on the region r.

Figure 12: Type inference ⊢a .
The type system is quite expressive. In particular, it is able
to type all of the examples that were used as correct programs
up to this point in the paper (with straightforward modification
to translate λwit programs into λregwit ). In fact, assuming that foreach region r, write(r) nodes in each collection Wi are totallyordered, the type system is “complete” for the first-order fragment(i.e., no higher order functions) with no recursion and no storingof witnesses in references. That is, such a program e is witness
race free and well-typed by a standard Hindley-Milner type system
if and only if it is well-typed by our type system. We also show
later in Section 5 that the type system is more expressive than past
approaches.
The limitations of the type system are the standard ones: letbased predicative polymorphism, flow-insensitivity of reference
types, and unsoundness under call-by-name semantics; the latter
is a typical limitation of a non-linear substructural type system.
Another limitation is that the type system enforces for each regionr that write(r) nodes in every collection Wi are totally ordered
whereas witness race freedom permits an absence of ordering forthe case i = n; we believe that this is a minor limitation.
4.3 Inference
We next present a type inference algorithm. By Theorem 6, thisresults in an automatic algorithm for statically checking witness
race freedom.
At a high-level, our type system is a standard Hindley-Milner
type system with some additional rational arithmetic constraints.
Therefore we could perform inference by employing a standard
type inference technique to solve all type-structural constraints
while generating rational arithmetic constraints on the side, andthen solving the generated arithmetic constraints separately. Unfortunately, the arithmetic constraints may be non-linear since they
involve the multiplication of variables. Because there is no efficientalgorithm for solving general non-linear rational arithmetic constraints, we need to dive into lower-level details of the type system.
Let us separate type inference into two phases. The first phasecarries out type inference after erasing all rational numbers fromthe type system. That is, the types inferred in this phase are:σ:=

int | σ→σ ′ | σ ⊗ σ ′ | ref (σ, σ ′ , ρ) | reg(ρ) | I

where a type I is a subset of RegIDs. Intuitively, each type I represents the non-0 domain of some witness type W . The first phasecan be carried out by a standard Hindley-Milner type inference, al-beit with regions, which is no harder than type variables. We omit
the details of this phase. We may safely reject the program if thefirst phase fails. Otherwise we annotate each subexpression e by its
inferred type σ: eσ . In the second phase, we use the annotated program to generate the appropriate rational arithmetic constraints via
bottom-up type-inference. Let e be an annotated program. Then thegenerated constraints for e is C where Γ, W ⊢a e : τ, C for someΓ, W , and τ .
The second-phase type inference rules are separated into two
kinds, ⊢a (Figure 12) and ⊢b (Figure 13), which must occur instrictly interleaving manner. The purpose of ⊢a is to account for
the type judgment rule Source, whereas ⊢b accounts for all otherrules.
We should note that, strictly speaking, types τ appearing in thealgorithm are different from the ones in the type judgment rules.
That is, instead of rational numbers, the types τ in the algorithm
are qualified by rational number variables α, β, γ, etc. Also thedomain of a witness type W is not the entire RegIDs set but only
some subset of it. In other words, a witness type W is a partial
function from RegIDs to rational number variables. We re-define
the addition of witness types as follows to reflect the change:

τ = Fresh(σ){x:τ }, ∅ ⊢b xσ : τ, ∅∅, ∅ ⊢b i : int, ∅∅, ∅ ⊢b • : ∅, ∅Γ, W ⊢a e : τ, C

β is freshβ

Γ × β, W × β ⊢b λx.e : Γ(x) → τ, C
Γ1 , W 1 ⊢ a e 1 : τ 1 , C 1
Γ2 , W 2 ⊢ a e 2 : τ 2 , C 2
τ = Fresh(σ)τ ′ = Fresh(σ ′ )β is freshβ

C = C1 ∪ C2 ∪ {τ1 ≥ τ → τ ′ , β ≥ 1, τ2 ≥ τ }′Γ1 + Γ2 , W1 + W2 ⊢b eσ→σ
e2 : τ ′ , C
1Γ1 , W 1 ⊢ a e 1 : τ 1 , C 1
Γ2 , W 2 ⊢ a e 2 : τ 2 , C 2
Γ1 + Γ 2 , W 1 + W 2 ⊢ b e 1 ⊗ e 2 : τ 1 ⊗ τ 2 , C 1 ∪ C 2′

Γ, W ⊢a πi (e) : τ, C
τ1 = Fresh(σ) τ2 = Fresh(σ )Γ, W ⊢b πi (eσ1 ⊗σ2 ) : τi , C ∪ {τ ≥ τ1 ⊗ τ2 }
Γ2 , W 2 ⊢ a e 2 : τ 2 , C 2reg(ρ): ref (τ1 , τ2 , ρ), C1 ∪ C2
Γ1 + Γ2 , W1 + W2 ⊢b ref e1 e2

W + W′ ={ρ 7→ W (ρ) + W ′ (ρ) | ρ ∈ dom(W ) ∧ ρ ∈ dom(W ′ )}∪{ρ 7→ W (ρ) | ρ ∈ dom(W ) ∧ ρ ∈/ dom(W ′ )}′′∪{ρ 7→ W (ρ) | ρ ∈ dom(W ) ∧ ρ ∈/ dom(W )}Γ1 , W 1 ⊢ a e 1 : τ 1 , C 1

Γ1 , W 1 ⊢ a e 1 : τ 1 , C 1
Γ2 , W 2 ⊢ a e 2 : τ 2 , C 2
Γ3 , W 3 ⊢ a e 2 : τ 3 , C 3
τ = Fresh(σ)τ ′ = Fresh(σ ′ )′C = C1 ∪ C2 ∪ {τ1 ≥ ref (τ, τ , ρ), τ2 ≥ τ ′ , τ3 (ρ) ≥ 1}
Γ = Γ 1 + Γ2 + Γ3
W = W1 + W2 + W3
ref (σ,σ ′ ,ρ)Γ, W ⊢b write e1e2 e3 : τ3 , C

Γ1 , W 1 ⊢ a e 1 : τ 1 , C 1
Γ2 , W 2 ⊢ a e 2 : τ 2 , C 2
τ = Fresh(σ)τ ′ = Fresh(σ ′ )C = C1 ∪ C2 ∪ {τ1 ≥ ref (τ, τ ′ , ρ), τ2 (ρ) > 0}ref (σ,σ ′ ,ρ)Γ1 + Γ2 , W1 + W2 ⊢b read e1e2 : τ ⊗ τ2 , C

Γ, W ⊢a e : τ, C
Γ, W ⊢b letreg xreg(ρ) e : τ, C ∪ {W (ρ) ≤ 1}
Γ1 , W 1 ⊢ a e 1 : τ 1 , C 1
Γ2 , W 2 ⊢ a e 2 : τ 2 , C 2
Γ1 + Γ2 , W1 + W2 ⊢b join e1 e2 : τ1 + τ2 , C1 ∪ C2
Γ1 , W 1 ⊢ a e 1 : τ 1 , C 1
Γ2 , W 2 ⊢ a e 2 : τ 2 , C 2x∈/ free(e1 )C = C1 ∪ C2 ∪ {τ1 ≥ Γ2 (x)}
Γ1 + Γ2 , W1 + W2 ⊢b let x = e1 in e2 : τ2 , C
Γ1 , W 1 ⊢ a e 1 : τ 1 , C 1
Γ2 , W 2 ⊢ a e 2 : τ 2 , C 2
x ∈ free(e1 )C = C1 ∪ C2 ∪ {τ1 ≥ Γ1 (x) × ∞, τ1 ≥ Γ2 (x)}
Γ1 + Γ2 , W1 + W2 ⊢b let x = e1 in e2 : τ2 , C
Figure 13: Type inference ⊢b .

We also re-define the addition of type environments:Γ + Γ′ ={x:Γ(x) + Γ′ (x) | x ∈ dom(Γ) ∧ x ∈ dom(Γ′ )}∪{x:Γ(x) | x ∈ dom(Γ) ∧ x ∈/ dom(Γ′ )}∪{x:Γ′ (x) | x ∈ dom(Γ′ ) ∧ x ∈/ dom(Γ)}

Note that we omit annotations when they are not used (i.e., wesay e instead of eσ , etc.). There are only two cases for ⊢a . The firstcase is for expressions that were given a witness type I in the firstphase. In this case, we add Fresh(I) to τ and W to account for a
possible application of Source. Fresh is defined in Figure 11. The
second case is for expressions that were not given a witness type.
In this case, we simply pass the result of the subderivation ⊢b up.
We discuss a few representative ⊢b rules. Note that ⊢b rules aresyntax directed. In the case of a variable xσ , we create a fresh τfrom σ and pass {x:τ }, ∅ ⊢b xσ : τ, ∅ up to the parent derivation.
(Recall our type inference is bottom-up.) The case for integers anddummy witnesses are trivial. In the case of an abstraction λx.e,
we multiply Γ and W passed from the subderivation by β. In the′case of a function application eσ→σ
e2 , we add the constraints
1β{τ1 ≥ τ → τ ′ , β ≥ 1, τ2 ≥ τ } to connect arguments andreturns as well as requiring β to be at least 1. Note that the typerule Sub is implicitly incorporated in the constraints. In the caseref (σ,σ ′ ,ρ)e2 e3 , we add the constraint τ2 (ρ) ≥ 1 toof write e1
match the type rule Write. Note that the first phase guarantees
that ρ ∈ dom(τ3 ). In the case letreg xreg(ρ) e, the constraint
W (ρ) ≤ 1 is effective only when ρ ∈ dom(W ) as ρ ∈/ dom(W )implies that the region was not used at all. Note that there is no casecorresponding to the type rule LetA. Prior to running the algorithm,
we replace each occurrence of the expression let x = e in e′ inthe program by the expression e′ [(let x = e in x)/x] whenevere ∈ V and x occurs more than once in e′ .

As an example, consider the following program (a λreg
wit versionof the last example from Section 2):
letreg r
let x = ref 1 r in
let w = write x 2 • inlet f = λy.read x w inlet z = (f 0) ⊗ (f 0) in
let w = write x 3 join π2 (π1 (z)) π2 (π2 (z)) in z
Suppose the first phase assigns r the type reg(ρ). Assume eachlet-bound variable is treated monomorphically. The second phase
generates the following constraints for the let-bound expressions(slightly simplified for readability):

where Pos is defined as follows:p

Pos(τ → τ ′ ) = Neg(τ ) ∪ Pos(τ ′ ) ∪ {p}Pos(τ ⊗ τ ′ ) = Pos(τ ) ∪ Pos(τ ′ )Pos(ref (τ, τ ′ , ρ)) = Pos(τ ) ∪ Neg(τ ′ )Pos(W ) = ran(W )Neg(int) = Pos(int) = Neg(reg(ρ)) = Pos(reg(ρ)) = ∅pNeg(τ → τ ′ ) = Pos(τ ) ∪ Neg(τ ′ )Neg(τ ⊗ τ ′ ) = Neg(τ ) ∪ Neg(τ ′ )Neg(ref (τ, τ ′ , ρ)) = Neg(τ ) ∪ Pos(τ ′ )Neg(W ) = ∅{r:reg(ρ)}; ∅ ⊢a ref 1 r : ref (int, int, ρ), ∅Γ; {ρ 7→ γ1 + γ2 } ⊢a write x 2 • : {ρ 7→ γ1 + γ2 }, {γ1 ≥ 1}
where Γ = {x:ref (int, int, ρ)}β1int ⊗ {ρ 7→ α1 + γ3 }, C
Γ; W ⊢a λy.read x w : int →where Γ = {x:ref (int, int, ρ), w:{ρ 7→ α1 × β1 }}and W = {ρ 7→ γ3 × β1 }and C = {α1 + γ3 > 0}

Γ; ∅ ⊢a (f 0) ⊗ (f 0) : τ, C
β +βwhere Γ = {f :int 2→ 3 int ⊗ {ρ 7→ α2 }}and τ = (int ⊗ {ρ 7→ α2 }) ⊗ (int ⊗ {ρ 7→ α2 })and C = {β2 ≥ 1, β3 ≥ 1}
Γ; {ρ 7→ γ4 } ⊢a write x 3 . . . : {ρ 7→ α3 + α4 + γ4 }, C
where Γ = {x:ref (int, int, ρ), z :τ }and τ = (int ⊗ {ρ 7→ α3 }) ⊗ (int ⊗ {ρ 7→ α4 })and C = {α3 + α4 + γ4 ≥ 1}
The final constraints, after some simplification, is as follows:γ1 ≥ 1, 1 ≥ γ1 + γ2 + γ3 × β1 + γ4 , β1 ≥ β2 + β3 ,β2 ≥ 1, β3 ≥ 1, γ1 + γ2 ≥ α1 × β1 , α1 + γ3 > 0,
α1 + γ3 ≥ α2 , α3 + α4 + γ4 ≥ 1, α2 ≥ α3 , α2 ≥ α4Third, for any + that appears in a positive position of τ , i.e. insome p ∈ Pos(τ ), the polynomial p does not contain any β ∈ B.
Then the result follows from inspection of the subtyping rules. 2
The theorem implies that we can compute all assignments to thevariables in B by computing the minimum satisfying assignment
for C ′ = {β ≥ p | β ∈ B} ⊆ C. It is easy to see that such an
assignment always exists. (Recall that the range is non-negative.)
This problem can be solved in quadratic time by an iterative method
in which all variables are initially set to 0, and at each iteration the
new values for the variables are computed by taking the maximumof the right hand polynomials evaluated at the current values. It is
possible to show that if the minimum satisfying assignment for avariable β is some q < ∞, then the iterative method finds q for
β in 2|C ′ | iterations. Hence any variable changing after the 2|C ′ |thiteration can be safely set to ∞. All variables are then guaranteed
to converge within 3|C ′ | iterations. Because each iteration examines
every constraint, the overall time is at most quadratic in the size ofC′.
Substituting the computed assignments for B in C results inlinear rational constraints, which can be solved efficiently by alinear programming algorithm.

Note that the constraints are satisfiable, e.g., by the substitution
β1 = 2 β2 = β3 = γ1 = 1
α1 = α2 = α3 = α4 = 0.5
γ2 = γ3 = γ4 = 0
In general, a program e is well-typed if and only if the constraints C generated by type inference are satisfiable. So it suffices
to show that the satisfaction problem for any C generated by thetype inference algorithm can be solved.
To this end, we first note that because of the first phase, any
constraint τ ≥ τ ′ ∈ C can be reduced to a set of rational arithmetic
constraints of the form p ≥ p′ where p, p′ are rational polynomials.
The troublesome non-linearity comes from Γ × β and W × β in the
λx.e case. Let us focus our attention on the set B of variables usedin such multiplications. (Note that we have used β instead of α justfor this case in the pseudo-code to make it clear that these variables
are special.) We can show that the following holds:
T HEOREM 7. Let p  p′ ∈ C where  ∈ {≥, >}. If β ∈ Boccurs in the polynomial p, then it must be the case that  =≥,p = β, and that the polynomial p′ consists only of symbols in theset {+, ×, 1, ∞} ∪ B.
Proof (Sketch): Let Γ, W ⊢a e : τ, C. For any τ ′ ∈ Γ, × and +only appear at the top-level, i.e., not within argument and return
types of a function type. Secondly, we can show by induction thatwithin the type τ , × only appears in negative positions. Moreprecisely, for any p ∈ Pos(τ ), the polynomial p contains no ×

5. Related Work
Adding side-effects to a functional language is an old problem withmany proposed solutions. Here we compare our technique against
two of the more prominent approaches: linear types [15, 6, 1] andmonads [10, 11, 7, 9].
In linear types, there is an explicit world program value (orone world per region for languages with regions) that conceptually
represents the current program state. By requiring each world havea linear type, the type system ensures that the world can be updated
in place.
The linear type system can be expressed in our type system
by restricting every flow to 1, every witness to contain only one
flow, and designating one dummy witness to serve the role of the“starting” witness (or for regions, one dummy witness per region).
Thus our approach is more expressive than such an approach. Notethat this also implies that every function type can be restricted
to have either 1 or ∞ as the qualifier. It is easy to see that the
program is well-typed under this restriction if and only if it is welltyped by the linear type system. The restriction limits programs
to manipulate witnesses only in a linear fashion. In practice, this
implies that there can be no parallel reads, no dead witnesses,
no redundant witnesses, and no duplication of values containing
witnesses.

Our approach can implement monadic primitives as follows (forconcrete comparison, we use state monads [9]):newVar = λx.λy.let z = (ref x π2 (y)) in y ⊗ z
readVar = λx.λy.let z = (read x π1 (y)) in(π2 (z) ⊗ π2 (y)) ⊗ π1 (z)writeVar = λx.λw.λy.let z = (write x w π1 (y)) in(z ⊗ π2 (y)) ⊗ w>>= = λf.λg.λx.let y = (f x) in g π2 (y) π1 (y)returnST = λx.λy.y ⊗ x
runST e = letreg x π2 (e (• ⊗ x))
The idea behind these definitions is to implement each state monadof the type ST (α, τ ) as a function that takes a witness and theregion α as arguments and returns a witness, the region α, and avalue of the type τ . It is easy to see that if a state monad programis well-typed by the monadic type system, then it is also well-typed
with our type system using the above definitions for the monadic
primitives. Thus, our approach is more expressive than monads.
In practice, a monadic approach shares essentially the same
limitations as linear types; for example, side-effects are restricted
to a linear, sequential order. (In fact, it is not too hard to seethat we can actually implement monadic primitives with the linear
types restriction with only slightly longer code.) On the other hand,a monadic type system has an engineering advantage as it only
requires Hindley-Milner type inference.
In addition to the above technical differences, our approachdiffers from previous approaches in its design motivation. That is,while our language feature, witnesses, is motivated by a pragmatic
observation, understanding the motivation behind linear types andmonads (i.e., not just knowing how to use them) arguably requires
an appreciation of their underlying theory.
The technique used in our type system has some resemblance
to fractional permissions [2] which can guarantee non-interference
in imperative programs. Indeed, it may be possible to give an“interpretation” of witnesses as some relaxation of permissions orcapabilities [3] (after promoting permissions or capabilities to firstclass values) in situations where the program is witness race free.

6. Conclusions
We have presented a new approach to adding side-effects in purely
functional languages based on witnesses. We have stated a natural
semantic correctness condition called witness race freedom andproposed a type-based approach for statically checking witness
race freedom.

References[1] P. Achten, J. H. G. van Groningen, and R. Plasmeijer. High levelspecification of I/O in functional languages. In Proceedings of the
1992 Glasgow Workshop on Functional Programming, pages 1–17.
Springer-Verlag, 1993.

[2] J. Boyland. Checking interference with fractional permissions. In
R. Cousot, editor, Static Analysis, Tenth International Symposium,
volume 2694 of Lecture Notes in Computer Science, pages 55–72,
San Diego, CA, June 2003. Springer-Verlag.
[3] K. Crary, D. Walker, and G. Morrisett. Typed memory management
in a calculus of capabilities. In Proceedings of the 26th Annual
ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, pages 262–275, San Antonio, Texas, Jan. 1999.
[4] M. Fähndrich, J. S. Foster, Z. Su, and A. Aiken. Partial online cycle
elimination in inclusion constraint graphs. In Proceedings of the 1998
ACM SIGPLAN Conference on Programming Language Design and
Implementation, pages 85–96, Montreal, Canada, June 1998.
[5] D. Grossman, G. Morrisett, T. Jim, M. Hicks, Y. Wang, and J. Cheney.
Region-based memory management in Cyclone. In Proceedings ofthe 2002 ACM SIGPLAN Conference on Programming Language
Design and Implementation, Berlin, Germany, June 2002.
[6] J. C. Guzman and P. Hudak. Single-threaded polymorphic lambda
calculus. In Proceedings, Fifth Annual IEEE Symposium on Logicin Computer Science, pages 42–51, Philadelphia, Pennsylvania, June
1990.
[7] S. L. P. Jones and P. Wadler. Imperative functional programming. In
Proceedings of the 20th Annual ACM SIGPLAN-SIGACT Symposiumon Principles of Programming Languages, pages 71–84, Charleston,South Carolina, Jan. 1993.
[8] J. Launchbury. A natural semantics for lazy evaluation. In Proceedings of the 20th Annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, pages 144–154, Charleston,South Carolina, Jan. 1993.
[9] J. Launchbury and A. Sabry. Monadic state: Axiomatizationof type safety. In Proceedings of the 1997 ACM SIGPLAN
International Conference on Functional Programming, pages 227–
238, Amsterdam, The Netherlands, June 1997.
[10] E. Moggi. Notions of computation and monads. Information andComputation, 93(1):55–92, 1991.
[11] M. Odersky, D. Rabin, and P. Hudak. Call by name, assignment,
and the lambda calculus. In Proceedings of the 20th Annual
ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, pages 43–56, Charleston, South Carolina, Jan. 1993.
[12] G. D. Plotkin. Call-by-name, call-by-value and the lambda-calculus.
Theoretical Computer Science, 1:125–159, 1975.
[13] T. Terauchi and A. Aiken. Witnessing side-effects. Technicalreport, Computer Science Division, EECS Department, Universityof California, Berkeley.
[14] M. Tofte and J.-P. Talpin. Implementation of the typed call-by-value
λ-calculus using a stack of regions. In Proceedings of the 21st Annual
ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, pages 188–201, Portland, Oregon, Jan. 1994.
[15] P. Wadler. Linear types can change the world! In Proceedings ofthe third ACM SIGPLAN International Conference on Functional
Programming, pages 63–74, Baltimore, Maryland, Sept. 1998.