Checking Race Freedom via Linear Programming
Tachio Terauchi
Tohoku University
terauchi@ecei.tohoku.ac.jp

Abstract
We present a new static analysis for race freedom and race detection. The analysis checks race freedom by reducing the problem to (rational) linear programming. Unlike conventional static
analyses for race freedom or race detection, our analysis avoids
explicit computation of locksets and lock linearity/must-aliasness.
Our analysis can handle a variety of synchronization idioms that
more conventional approaches often have difficulties with, such as
thread joining, semaphores, and signals. We achieve efficiency byutilizing modern linear programming solvers that can quickly solve
large linear programming instances. This paper reports on the formal properties of the analysis and the experience with applying animplementation to real world C programs.
Categories and Subject Descriptors F.3.2 [Logics and Meaningof Programs]: Semantics of Programming Languages—Program
analysis; F.3.3 [Logics and Meaning of Programs]: Studies ofProgram Constructs—Type structure
General Terms
Keywords

Algorithms, Languages, Theory, Verification

Fractional Capabilities,Linear Programming

1. Introduction
Race condition occurs when one thread writes to a memory locationthat another thread is concurrently writing or reading. Race freedom, the absence of race conditions, is a basic building block fordeveloping and verifying shared-memory parallel programs, andstatic analysis for race freedom and race detection has been an active focus of research.
In many static (or dynamic) analyses for race freedom or race
detection, the central idea is to compute locksets. A lockset is theset of locks that are always held when accessing some memory
location (abstract memory location in static analyses) such that apotential race is detected when the lockset is empty. It is importantthat the locks in the locksets are linear [20] (or must-alias [17]),in the sense that each lock corresponds to a unique concrete lock.
Inferring locksets and lock linearity/must-aliasness statically canbe non-trivial, especially in the presence of non-lexically scoped
locks, that sometimes analyses make optimistic approximations.
Also, this approach is usually limited to locks and other lock likesynchronization idioms.

e

::=
|
|
|
|
|
|
|
|
|
|
|
|
|
|

x
n
let x = e1 in e2
if * then e1 else e2
while * do e
newtidspawn(e1 ){e2 }join eref e!ee1 := e2
newlock
freelock elock eunlock e(variable)(integer constant)(variable binding)(branch)(loop)(new thread identifier)(new thread)(thread join)(new reference cell)(reference read)(reference write)(new lock)(free lock)(lock acquire)(lock release)

Figure 1. The syntax of the simple concurrent language.
This paper presents a different approach for statically checking
race freedom. The key idea is to reduce the race checking problem
to a linear programming problem such that if there exists a solution
to the constructed linear programming instance, then the programis guaranteed to be race free. In contrast to previous approaches,
our approach only needs standard may-aliasing information, anddoes not require locksets and lock linearity/must-aliasness. By utilizing efficient linear programming algorithms, we achieve both
good theoretical computational complexity (polynomial in the sizeof the program), and good practical running times, without sacrificing soundness. The approach can be extended to synchronization
methods beyond simple lock-based idioms. The prototype implementation described in Section 3 handles programming idioms that
other analyses often have difficulties with, such as thread joining,
semaphores, signals, and read-write locks, as well as read only accesses and local accesses.
The rest of the paper is organized as follows. Section 2 introduces the key concepts with a toy language that contains only locks
and thread spawning/joining, and formally proves soundness. Section 3 discusses the implementation, LP-Race, a tool for detecting races in multithreaded C programs. Section 4 discusses related
work, Section 5 discusses open issues, and Section 6 concludes.

2. Formal Aspects
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.
PLDI’08, June 7–13, 2008, Tucson, Arizona, USA.
Copyright c 2008 ACM 978-1-59593-860-2/08/06. . . $5.00.

Figure 1 shows a simple first order expression language (with side
effects) we use to present the key concepts of the analysis. The
language is minimized in ordered to focus on the novel aspects of
the analysis. We briefly describe the syntax. Variables are ranged
over by meta variables x, x1 , etc. The construct let x = e1 in e2
binds the result of evaluating e1 to x and evaluates e2 . We write
e1 ; e2 for let x = e1 in e2 such that x is not free in e2 .
The language contains non-deterministic branches and loops. The

let x = ref 0 in
spawn(newtid){!x};x := 1(a)let x = ref 0 in
let t = newtid in
spawn(t){!x};join t;x := 1(b)

let x = ref 0 in
let l = newlock inspawn(newtid){
lock l;!x;
unlock l };lock l;x := 1;
unlock l(c)

Figure 2. Simple race (a), and race avoidance via thread joining(b) and locking (c).

(ι, κ, θ, F [if * then e1 else e2 ]) → (ι, κ, θ, F [e1 ])(ι, κ, θ, F [if * then e1 else e2 ]) → (ι, κ, θ, F [e2 ])

::=
::=
|
|

t.E | F ||p | p||F
let x = E in e | ref E | E := e | v := E | !Elock E | unlock E | freelock E
spawn(E){e} | join E(ι, κ, θ, F [let x = v in e]) → (ι, κ, θ, F [e[v/x]])(ι, κ, θ, F [join t] || t.v) → (ι, κ, θ, F [0])We formally define the semantics of the language. The semantics
is defined as small-step reductions from states to states. A state is aquadruple (ι, κ, θ, p) where ι is the set of currently allocated thread
identifiers, κ is the current lock state, a mapping from the currently
available locks to {U, L} where U denotes that the lock is unlocked
and L denotes that the lock is locked, θ is a store mapping locations
to values, and p is a program state. Values, v, are defined asv ::= t | l | ℓ | nwhere the symbol t ranges over thread identifiers, l ranges overlocks, and ℓ ranges over locations. A program state is defined asfollows.
e ::= · · · | v
p ::= t.e | p1 || p2
Here, e is extended with values. Intuitively, an (extended) expression prefixed by a thread identifier, t.e, denotes a thread with thethread identified by t whose current program counter is e, whereas
p1 || p2 denotes a parallel composition of threads. Therefore, aprogram state is a parallel composition of finitely many expressions prefixed by thread identifiers. We let the parallel composition
operator || be commutative and associative.
We define the following standard notational convention. Givena mapping (i.e., a set-theoretic function) f , f [a 7→ b] denotes the
mapping {c 7→ f (c) | c ∈ dom(f ) \ {a}} ∪ {a 7→ b}.
Figure 3 defines evaluation contexts. Figure 4 shows the reduction rules. If1, If2, Loop, and Let are straightforward. Note that
because the language is an expression language, every expression

Spawn

Join

ℓ∈
/ dom(θ)
Ref(ι, κ, θ, F [ref v]) → (ι, κ, θ[ℓ 7→ v], F [ℓ])(ι, κ, θ, F [!ℓ]) → (ι, κ, θ, F [θ(ℓ)])

2.1 The Semantics

Lett∈/ dom(ι)
NewT(ι, κ, θ, F [newtid]) → (ι ∪ {t}, κ, θ, F [t])Figure 3. The evaluation contexts
construct spawn(e1 ){e2 } creates a new thread to evaluate e2 . Here,e1 is a thread identifier that can be used at join e to join threads.
Multiple threads are allowed to have the same thread identifier. The
language contains reference cells, that could be written and read
concurrently. Finally, the language contains syntax for creating,deleting, acquiring, and releasing locks.
Figure 2 (a) shows a simple example program that contains aread write race. The spawned thread may read from the referencecell bound to the variable x while the spawner thread writes to it.
Such a race can be avoided by using locks, as shown in (c), or byusing join to wait until the other thread finishes, as shown in (b).

If2

Loop

(ι, κ, θ, F [while * do e)) →(ι, κ, θ, F [if * then (e; while * do e) else 0])(ι, κ, θ, F [spawn(t){e}]) → (ι, κ, θ, F [0] || t.e)
F
E

If1

Read

(ι, κ, θ, F [ℓ := v]) → (ι, κ, θ[ℓ 7→ v], F [0])

Write

l∈
/ dom(κ)
NewL(ι, κ, θ, F [newlock]) → (ι, κ[l 7→ U], θ, F [l])κ = κ′ ∪ {l 7→ U } l ∈/ dom(κ′ )(ι, κ, θ, F [freelock l]) → (ι, κ′ , θ, F [0])FreeLκ(l) = ULck(ι, κ, θ, F [lock l]) → (ι, κ[l 7→ L], θ, F [0])(ι, κ, θ, F [unlock l]) → (ι, κ[l 7→ U], θ, F [0])Ulck

Figure 4. The operational semantics.
needs to evaluate to a value if they terminate, and so we use 0 as
the “unit” value for expressions that are evaluated purely for theireffects.
NewT creates a fresh thread identifier. Spawn spawns a new
thread using the given thread identifier, and Join waits for a threadwith the thread identifier to finish. Ref allocates a new referencecell that can be read by Read and written by Write. NewL createsa new lock, initialized to unlocked status. If the lock is unlocked,
Lck may acquire the lock, setting the lock status to locked. Ulckreleases the lock, setting the lock status to unlocked. FreeL deletes
a lock if the lock is unlocked1 .
We write (ι1 , κ1 , θ1 , p1 ) →∗ (ι2 , κ2 , θ2 , p2 ) for zero or
more reduction steps from the state (ι1 , κ1 , θ1 , p1 ) to the state(ι2 , κ2 , θ2 , p2 ). We now formally define race freedom.
D EFINITION 2.1 (Race Freedom). A state (ι1 , κ1 , θ1 , p1 ) is said
to be race free if for any state (ι2 , κ2 , θ2 , p2 ) such that(ι1 , κ1 , θ1 , p1 ) →∗ (ι2 , κ2 , θ2 , p2 ), p2 is not of the following form.
• F1 [ℓ := v1 ] || F2 [ℓ := v2 ]1 This models pthread mutex destroy in the POSIX threads library.

• F1 [ℓ := v] || F2 [!ℓ]Γ, Ψ ⊢ x : Γ(x), ΨVARΓ, Ψ ⊢ n : int, Ψ

INT

2.2 The Type System
We formulate the analysis as a type inference problem for a typesystem. The type system guarantees that a typable program is race
free. The types are defined as follows.
τ

::=
|
|
|

ref(ρ, τ )intlock(Ψ)tid(Ψ)(reference cells)
integers(locks)(thread identifiers)

The type ref(ρ, τ ) denotes a type of a reference cell pointing to
the abstract location ρ, storing a value of the type τ . Symbols Ψ,Ψ1 , etc. range over capability mappings. A capability mapping is afunction from abstract locations to non-negative rational numbers[0, ∞).
Capability mappings denote access capabilities to abstract locations. Each thread holds some amount of capabilities, representing
the access capabilities of the thread. Intuitively, a thread holding capabilities Ψ such that Ψ(ρ) ≥ 1 is allowed to write to the abstract
location ρ, and a thread holding capabilities Ψ such that Ψ(ρ) > 0
is allowed read from the abstract location ρ (thus the write capability implies the read capability). The type system ensures that the total amount of capabilities summed across all live threads is at most
1 for any abstraction location. This property ensures race freedom
as there cannot be two threads, say holding capabilities Ψ1 and Ψ2
respectively, such that one thread can write to an abstract location
ρ, (i.e., Ψ1 (ρ) ≥ 1) while the other thread can read or write to it(i.e., Ψ2 (ρ) > 0), because then the total amount of capabilities forρ would exceed 1.
Threads may transfer capabilities at synchronization points,
which in this simple language, is when accessing locks and spawning and joining threads. The capabilities Ψ appearing in a lock
type lock(Ψ) represents the amount of capabilities transferred tothe thread when acquiring the lock, and transferred from when releasing the lock. The capabilities Ψ appearing in a thread identifier
type tid(Ψ) represents the amount of capabilities transferred to thejoiner thread by joining a thread with the thread identifier.
Figure 5 shows the type checking rules. The judgement are of
the form Γ, Ψ1 , ⊢ e : τ, Ψ2 where Γ is a type environment mapping
variables to their types, the pre-capability Ψ1 is the capabilities before the evaluation of e, the post-capability Ψ2 is the capabilities
after the evaluation of e, and τ is the type of e. VAR and INT are
self-explanatory. LET, IF, WHILE make sure that capabilities are“conserved” (i.e., not created out of thin air) through the sequential flow of computation. The inequality Ψ1 ≥ Ψ2 is defined as∀ρ.Ψ1 (ρ) ≥ Ψ2 (ρ).
Also, the subtraction of capabilities is defined point-wise as
Ψ1 − Ψ2 = λρ.Ψ1 (ρ) − Ψ2 (ρ). Note that because the rangeof any capability mapping is restricted to non-negative rationals,
the subtraction is undefined if the result is negative. Similarly, theaddition of capabilities is defined as Ψ1 +Ψ2 = λρ.Ψ1 (ρ)+Ψ2 (ρ).
NEWT, SPAWN, and JOIN type thread creation and thread
joining. At SPAWN, the parent thread gives part of its capabilities,
Ψ3 , to the newly created thread, and so Ψ2 − Ψ3 amount ofcapabilities are left for the continuation of the parent thread. The
capabilities that are left after the spawned thread finishes, Ψ4 , orat least a part of it (Ψ1 ), may be recovered by using the thread
identifier. At JOIN, the joiner thread gains capabilities from thejoined thread through the thread identifier.
REF, WRITE, and READ type reference cell accesses. As
remarked above, READ requires a positive amount of capability
for the abstract location, and WRITE requires capabilities at least
1. Because there is no notion of lockset, these rules do not assert
anything about which locks protect the reference cell. Note thatΓ, Ψ ⊢ e1 : τ1 , Ψ1 Γ[x 7→ τ1 ], Ψ1 ⊢ e2 : τ2 , Ψ2
LETΓ, Ψ ⊢ let x = e1 in e2 : τ2 , Ψ2
Γ, Ψ ⊢ e1 : τ, Ψ1
Γ, Ψ ⊢ e2 : τ, Ψ2

Ψ1 ≥ Ψ3Ψ2 ≥ Ψ3Γ, Ψ ⊢ if * then e1 else e2 : τ, Ψ3

IF

Γ, Ψ1 ⊢ e : τ, Ψ2 Ψ2 ≥ Ψ1 Ψ ≥ Ψ1
WHILEΓ, Ψ ⊢ while * do e : int, Ψ1
Γ, Ψ ⊢ newtid : tid(Ψ1 ), ΨΓ, Ψ ⊢ e1 : tid(Ψ1 ), Ψ2

NEWTΓ, Ψ3 ⊢ e2 : τ, Ψ4

Ψ4 ≥ Ψ1

Γ, Ψ ⊢ spawn(e1 ){e2 } : int, Ψ2 − Ψ3

SPAWN

Γ, Ψ ⊢ e : tid(Ψ1 ), Ψ2
JOINΓ, Ψ ⊢ join e : int, Ψ1 + Ψ2
Γ, Ψ ⊢ e : τ, Ψ1
REF
Γ, Ψ ⊢ ref e : ref(ρ, τ ), Ψ1
Γ, Ψ ⊢ e1 : ref(ρ, τ ), Ψ1

Γ, Ψ1 ⊢ e2 : τ, Ψ2

Ψ2 (ρ) ≥ 1

Γ, Ψ ⊢ e1 := e2 : int, Ψ2

WRITEΓ, Ψ ⊢ e : ref(ρ, τ ), Ψ1 Ψ1 (ρ) > 0
READΓ, Ψ ⊢ !e : τ, Ψ1
Γ, Ψ ⊢ newlock : lock(Ψ1 ), Ψ − Ψ1

NEWLΓ, Ψ ⊢ e : lock(Ψ1 ), Ψ2
FREELΓ, Ψ ⊢ freelock e : int, Ψ2 + Ψ1
Γ, Ψ ⊢ e : lock(Ψ1 ), Ψ2
LCKΓ, Ψ ⊢ lock e : int, Ψ2 + Ψ1
Γ, Ψ ⊢ e : lock(Ψ1 ), Ψ2
ULCK
Γ, Ψ ⊢ unlock e : int, Ψ2 − Ψ1
Figure 5. The type checking rules.

READ naturally allows parallel reads (i.e., read-only accesses),because n threads may each hold 1/n amount of capabilities forthe same abstract location and still satisfy the “at most 1” property.
NEWL types lock creations. As remarked above, releasing alock loses the amount of capabilities associated with the lock.
Because new locks are initialized to the unlocked state, we subtract
the capabilities as if the lock is unlocked. Dually, FREEL getsback the capability associated with the lock for destroying thelock. At LCK, the thread gains the capabilities, and at ULCK, thecapabilities are lost.
The simplicity of these rules may appear deceptive. Researchersfamiliar with lockset-based race analysis might have expected tosee a rule requiring the locks to be linear [20] (or must-alias [17]).
A formal proof of correctness appears at the end of the section.
To see how the type system avoids linearity/must-aliasness requirement, suppose the rule NEWL is replaced by the following un-sound rule.
Γ, Ψ ⊢ newlock : lock(Ψ1 ), Ψ

NEWL-unsoundConsider the following program.

Proof: By case analysis on the reduction. 2

let x = ref 0 in
let l1 = newlock in
let l2 = newlock inspawn(newtid){
lock l1; !x; unlock l1 };lock l2; x := 1; unlock l2
The program has a race on x because two threads concurrently
access x (by holding different locks). However, with NEWLunsound, the program would type check (cf. Definition 2.3) byassigning the type lock(Ψ) to both l1 and l2 such that Ψ(ρ) = 1
where x has the type ref(ρ, int). NEWL prevents such a situation
by making sure that capabilities (like Ψ above) are not created “outof thin air”. In practice, this implies that if the type system cannot
distinguish two locks that are alive at the same time such that atleast one of them is used to guard some location, then the type system may report a false positive because the total capability would
exceed 1 at one of the lock allocation point. The locality extension
discussed in Section 3.1.5 can soundly allow may-aliased live locks
to be used to guard locations in some situations.
We now define the notion of a well-typed state. We extend typeenvironments so that they map values to types as well as variables.
Non-integer values are typed by the following rule.
Γ, Ψ ⊢ v : Γ(v), ΨWe define the notion of a well-typed store.
D EFINITION 2.2 (Well-typed Store). We write Γ ⊢ θ if for eachℓ ∈ dom(θ), Γ, 0 ⊢ θ(ℓ) : τ, 0 where Γ(ℓ) = ref(ρ, τ ) for some ρ.
Here, 0 is the null capability, defined as 0 = λρ.0. Threads are
typed by the following rule, which says that the capabilities left at
the end of the thread is at least the capabilities obtainable by joining
the thread.
Γ, Ψ ⊢ e : Ψ1 Γ(t) = tid(Ψ2 ) Ψ1 ≥ Ψ2
Γ, Ψ ⊢ t.e : int, 0
Let cap(lock(Ψ)) = Ψ. Recall that any program state is a parallel
composition of finitely many threads, that is, it is of the form
t1 .e1 || t2 .e2 || . . . || tn .en where n is the number of threads.
D EFINITION 2.3 (Well-typed State). Let p = t1 .e1 || . . . || tn .en
such that there are no free variables in p. We write Γ ⊢ (ι, κ, θ, p)
if there exist Ψ1 , . . . , Ψn such that
(1) For all t ∈ ι, Γ(t) is a thread identifier type.
(2) For all l ∈ dom(κ), Γ(l) is a lock type.
(3) Γ ⊢ θ.
(4) For all i ∈ {1, . . . , n}, Γ, Ψi ⊢ ti .ei : int, 0 .
(5) Let U = {l | κ(l) = U}. Let
Ψ=

X
l∈U

cap(Γ(l)) +L EMMA 2.4 (Preservation). Suppose Γ ⊢ (ι1 , κ1 , θ1 , p1 ) and(ι1 , κ1 , θ1 , p1 ) → (ι2 , κ2 , θ2 , p2 ). Then, there exists Γ′ ⊇ Γ suchthat Γ′ ⊢ (ι2 , κ2 , θ2 , p2 ).

n
X

Ψi

i=1

Then ∀ρ.Ψ(ρ) ≤ 1
The first three conditions ensure that ι, κ, θ are well-typed. The
condition (4) states that all threads are well-typed. The condition(5) asserts thatPthe total amount of capabilities summed across all
threads (i.e.., ni=1 Ψi ) and
P the amount of capabilities obtainable
by acquiring locks (i.e.,l∈U cap(Γ(l))) is at most 1 for any
abstract location.
Well-typedness is preserved across reductions.

Note that the condition (5) of Definition 2.3 implies that a welltyped state cannot have two threads such that one thread is trying
to write to a location and the other thread is accessing the same
location. More formally,
L EMMA 2.5. Suppose p is of the form F1 [ℓ := v1 ] || F2 [ℓ := v2 ]or F1 [ℓ := v] || F2 [!ℓ]. Then for no Γ, Γ ⊢ (ι, κ, θ, p).
The soundness of the type system follows from the above lemmas.
T HEOREM 2.6. Suppose Γ ⊢ (ι, κ, θ, p). Then (ι, κ, θ, p) is race
free.
Proof: Straightforward from Lemma 2.4, Lemma 2.5, and Definition 2.1. 2
The type system is inspired by research on fractional permissions/capabilities. Fractional permissions were originally invented
to guarantee determinism of multithreaded programs in the presence of parallel reads [5]. The idea has been adopted in concurrent
separation logic [3], and has also been used to statically check determinism of channel communicating processes [21].
2.2.1 Example
Consider the following example which spawns threads in a loop,
and uses locks and joins to avoid races to the shared reference cells
bound to x and y.
let x = ref 0 in let y = ref 0 in
let t = newtid in let l = newlock inwhile * dospawn(t){let z = !y in lock l; x := z; unlock l};spawn(t){let z = !y in lock l; x := z; unlock l};join t; join t; y := 1
Let e be the code above, and let p = t1 .e. Consider the state({t1 }, ∅, ∅, p). Let Ψ1 = 0 [ρx 7→ 1][ρy 7→ 1]. Then we have∅, Ψ1 ⊢ ({t1 }, ∅, ∅, p), guaranteeing that Figure 2 (b) is race free.
The type derivation uses a type environment of the form
{ t1 7→ tid(0 ), x 7→ ref(ρx , int), y 7→ ref(ρy , int)
t 7→ tid(0 [ρy 7→ 0.5]), l 7→ lock(0 [ρx 7→ 1])}to type check the main body of e. Note that the type of t indicatesthat the spawned thread gets a fraction of the capability to accessy in read-only mode, which is combined at joins so that the mainthread can write to y after the threads finish. The type of l indicatesthat the spawned threads get the full (i.e., write) capability for x byacquiring l.
2.3 The Analysis Algorithm
Intuitively, the analysis algorithm is a type inference algorithm forthe type system presented in Section 2.2. The analysis is separated
in two phases. Informally, the first phase infers everything about thetype derivation except for the amount of capabilities. The second
phase uses linear programming to check if there exist an assignmentof capabilities that satisfies the capability constraints.
2.3.1 Phase 1
The first phase is mostly a standard unification-based inference,
generating capability constraints on the side. Figure 6 shows theconstraint generation rules. Here, α’s are type variables, ̺’s are abstract location variables, and ϕ’s are capability mapping variables.
These rules are straightforward syntax-directed inference rules forthe type rules from Figure 5.

ϕ freshα, ϕ fresh∆, ϕ ⊢ x : ∆(x), ϕ; ∅ ∆, ϕ ⊢ n : α, ϕ; {α = int}∆, ϕ ⊢ e1 : α1 , ϕ1 ; C1 ∆, ϕ2 ⊢ e2 : α2 , ϕ3 ; C2∆, ϕ ⊢ let x = e1 in e2 : α2 , ϕ3 ; C1 ∪ C2 ∪ {α1 = ∆(x), ϕ1 = ϕ2 }∆, ϕ ⊢ e1 : α, ϕ1 ; C1 ∆, ϕ′ ⊢ e2 : α′ , ϕ′1 ; C2∆, ϕ ⊢ if * then e1 else e2 : α, ϕ2 ; C1 ∪ C2 ∪ {α = α′ , ϕ = ϕ′ , ϕ1 ≥ ϕ2 , ϕ′1 ≥ ϕ2 }α, ϕ, ϕ1 fresh∆, ϕ1 ⊢ e : α, ϕ2 ; C α2 , ϕ fresh∆, ϕ ⊢ while * do e : α2 , ϕ1 ; C ∪ {α2 = int, ϕ2 ≥ ϕ1 , ϕ ≥ ϕ1 } ∆, ϕ ⊢ newtid : α, ϕ; {α = tid(ϕ1 )}∆, ϕ ⊢ e1 : α1 , ϕ2 ; C1 ∆, ϕ3 ⊢ e2 : α2 , ϕ4 ; C2 α, ϕ1 , ϕ5 fresh∆, ϕ ⊢ spawn(e1 ){e2 } : α, ϕ5 ; C1 ∪ C2 ∪ {α = int, α1 = tid(ϕ1 ), ϕ4 ≥ ϕ1 , ϕ5 = ϕ2 − ϕ3 }∆, ϕ ⊢ e : α, ϕ2 ; C α1 , ϕ1 , ϕ1 fresh∆, ϕ ⊢ e : α, ϕ1 ; C α1 , ̺ fresh∆, ϕ ⊢ join e : α1 , ϕ3 ; C ∪ {α = tid(ϕ1 ), α1 = int, ϕ3 = ϕ1 + ϕ2 } ∆, ϕ ⊢ ref e : α1 , ϕ1 ; C ∪ {α1 = ref(̺, α)}∆, ϕ ⊢ e1 : α1 , ϕ1 ; C1 ∆, ϕ′1 ⊢ e2 : α2 , ϕ2 ; C2 α, ̺ fresh∆, ϕ ⊢ e1 := e2 : α, ϕ2 ; C1 ∪ C2 ∪ {α = int, α1 = ref(̺, α2 ), ϕ1 = ϕ′1 , ϕ2 (̺) ≥ 1}
α, ϕ1 , ϕ′ fresh∆, ϕ ⊢ e : α, ϕ1 ; C α1 , ̺ fresh∆, ϕ ⊢ !e : α1 , ϕ1 ; C ∪ {α = ref(̺, α1 ), ϕ1 (̺) > 0} ∆, ϕ ⊢ newlock : α, ϕ′ ; {α = lock(ϕ1 ), ϕ′ = ϕ − ϕ1 }∆, ϕ ⊢ e : α, ϕ1 ; C∆, ϕ ⊢ freelock e : α′ , ϕ3 ; C ∪ {α′ = int, α = lock(ϕ2 ), ϕ3 = ϕ1 + ϕ2 }∆, ϕ ⊢ e : α, ϕ2 ; C α1 , ϕ1 , ϕ3 fresh∆, ϕ ⊢ lock e : α1 , ϕ3 ; C ∪ {α = lock(ϕ1 ), α1 = int, ϕ3 = ϕ2 + ϕ1 }∆, ϕ ⊢ e : α, ϕ2 ; C α1 , ϕ1 , ϕ3 fresh∆, ϕ ⊢ unlock e : α1 , ϕ3 ; C ∪ {α = lock(ϕ1 ), α1 = int, ϕ3 = ϕ2 − ϕ1 }Figure 6. The type inference rules.
The inference judgement, ∆, ϕ1 ⊢ e : α, ϕ2 ; C, reads “underthe environment ∆, e is inferred to have the type α, the precapability ϕ1 , the post-capability ϕ2 , with the set of constraints C.”
For simplicity, we assume that let-bound variables are distinct. We
initialize ∆ to map each variable to a fresh type variable. We visit
each AST node (i.e., expression) in a bottom up manner to build
the set of constraints.
The resulting set of constraints contains three kinds of constraints:(a) Type unification constraints: σ = σ ′ .
(b) Capability (in)equality constraints: φ = φ′ and φ ≥ φ′ .
(c) Access constraints: ϕ(̺) ≥ 1 and ϕ(̺) > 0.
where
σ ::= α | ref(̺, α) | int | lock(ϕ) | tid(ϕ)φ ::= ϕ | φ + φ | φ − φThe constraints of the kind (a) can be resolved by the standard
unification algorithm, which may create more constraints the kind(b). In addition, it creates constraints of the form ̺1 = ̺2 , which
can also be resolved by the standard unification algorithm. This
leaves us with a set of constraints of the kind (b) and (c).
Because we used simple types for the sake of exposition, theanalysis algorithm may fail at this point, for example, when the
program uses integers as locks. We may reject the program at thispoint. But it is easy to extend the system with sum types andrecursive types so that this phase never fails. We take such an
approach in the implementation described in Section 3.
2.3.2 Phase 2
The second phase of the algorithm finds a satisfying solution to theremaining constraints generated in the first phase so that the program is well-typed. We reduce the problem to linear programming
as follows. Let e be the program being analyzed. Phase 1 returns
pre-capability ϕe such that ∆, ϕe ⊢ e : τ, ϕ′ ; C for some τ, ϕ′ andC.
For each ̺ (that is, its equivalence class obtained by the unification in phase 1), we instantiate a linear programming problem using
the remaining constraints together with the constraint ϕe (̺) ≤ 1.
More precisely, each constraint mapping variables ϕ is instantiated as a linear programming variable ϕ(̺), and access constraints
ϕ(̺′ ) ≥ 1 and ϕ(̺′ ) > 0 are removed from the constraints if
̺′ 6= ̺. We add constraints ϕ(̺) ≥ 0 for each ϕ to ensure thatcapabilities are non-negative.
To apply linear programming algorithms that can only takenon-strict inequalities such as the one implemented in GLPK [1],we add a fresh linear programming variable ǫ and replace eachϕ(̺) > 0 with ϕ(̺) ≥ ǫ, and set the objective function to be ǫ. We
ask the linear programming solver to find a solution that maximizes
ǫ. If the solver returns a solution such that ǫ > 0, then we accept
the program as race free on the location ̺. Otherwise, we report a
possible race on ̺.

A write-write race is reported if the linear programming solver
cannot find any solution. A read-write race is reported if the linear
programming solver finds a solution but ǫ = 0.
2.3.3 Analysis of the Algorithm
We prove the correctness of the analysis algorithm. We use the symbol η to denote a constraint solution, which is a sorted substitution mapping type variables to types, abstract location variables toabstract locations, and capability mapping variables to capability
mappings. A constraint solution becomes a mapping from σ, ∆,and φ in the obvious way.
D EFINITION 2.7. We write η |= C (“η solves C”) if• for each σ = σ ′ ∈ C, η(σ) = η(σ ′ ).
• for each φ ≥ φ′ ∈ C, η(φ) ≥ η(φ′ ).
• for each φ = φ′ ∈ C, η(φ) = η(φ′ ).
• for each φ(̺) ≥ 1 ∈ C, η(φ)(η(̺)) ≥ 1.
• for each φ(̺) > 0 ∈ C, η(φ)(η(̺)) > 0.
• for each φ(̺) ≤ 1 ∈ C, η(φ)(η(̺)) ≤ 1.

L EMMA 2.8. Suppose ∆, ϕ1 ⊢ e : α, ϕ2 ; C and η |= C. Then,η(∆), η(ϕ1 ) ⊢ e : η(α), η(ϕ2 ).
Proof: By induction on the type derivation. 2
T HEOREM 2.9 (Soundness). Suppose ∆, ϕe ⊢ e : τ, ϕ; C and[η |= {ϕe (̺) ≤ 1} ∪ C
̺Let Γ = η(∆). Let x1 , . . . , xn be the free variables in e. Let
v1 , . . . , vn be such that Γ ⊢ vi : Γ(xi ) for each vi . Let ι,κ, θ be such that ι ∪ dom(κ) ∪ dom(θ) ∪ Z ⊇ {v1 , . . . , vn },Γ ⊢ θ, and κ(l) = L for each l ∈ dom(κ). Let t ∈/ ι. Then,({t} ∪ ι, κ, θ, t.e[v1 /x1 ] . . . [vn /xn ]) is race free.
Proof: Straightforward from Lemma 2.8 and Theorem 2.6. 2
We argue the theoretical computational complexity of the analysis algorithm. The instance of linear programming problem inphase 2 can be solved in time polynomial in the size of the constraints by algorithms such as interior points methods. Therefore,
the complexity of the algorithm is polynomial in the time phase
1 takes to generate the capability constraints, which is polynomialin the size of the program for our simple language. Therefore, thecomplexity of the analysis algorithm is polynomial in the size ofthe program.
In general, the complexity will increase if we include more complex programming constructs such as data structures and higher order functions if we stick with the simple types. But this can be
avoided by incorporating recursive types, as is done in the LP-Race
implementation.

3. LP-Race
We have implemented a prototype of the analysis algorithm, LPRace, a tool for detecting races in C programs. LP-Race uses
CIL [19] as a front-end to parse C files and handles the full-setof C.
3.1 Handling C Features
LP-Race extends the analysis framework to handle C features notcovered in the formalism detailed in Section 2. This includes structs
and unions, functions, and synchronization methods such as signaling and semaphores. This section highlights some of the notable
extensions.

3.1.1 Alias Analysis
C programs use pointers and arrays extensively. To generate a sensible set of abstract locations, LP-Race performs points-to analysis
and use the computed may-alias sets as abstract locations. For the
prototype implementation, we choose one-level-flow analysis [6, 7](with optimistic field sensitivity2 ), which is fast and known to produce good alias sets in practice. In principle, any may alias analysis
can be used to obtain abstract locations.
As remarked earlier, LP-Race uses sum types and recursive
types so that the first phase of the analysis never fails. This allows,
among other things, LP-Race to report all single-threaded C programs to be race free.
3.1.2 Generic Control Flow
C contains unstructured control flow such as gotos and breaks. To
handle generic control flow, LP-Race uses CIL to generate a control
flow graph for each function, and associate a fresh capability foreach node in the control flow graph. Then, for each successor nodeb of a node a, LP-Race adds the constraint ϕa ≥ ϕb where ϕa isthe capability associated with a and ϕb is the capability associatedwith b.
3.1.3 Functions
Because threads are typically created using function pointers, handling first class functions is crucial for analyzing multithreaded C
programs. We extend the type system with function types of theformτ ::= · · · | (Ψpre , ~τ ) → (Ψpost , τret )where ~τ are the arguments types (the notation ~a denotes a sequence), and τret is the return type. Intuitively Ψpre is the capability that the caller of the function must be holding, and Ψpost is
the capability that can be returned to the caller when the function
returns. Ψpre is taken from the entry node of the function body,and Ψret is the solution for the capability variable ϕret such thatfor each return node a in the function, LP-Race adds the constraint
ϕa ≥ ϕret where ϕa is the capability associated with a.
LP-Race type check function calls by the following rule.
Γ, Ψ ⊢ e : (Ψpre , τ1 , . . . , τn ) → (Ψpost , τret ), Ψ1∀i ∈ {1, . . . , n}.(Γ, Ψi ⊢ ei : τi , Ψi+1 )Ψn+1 = Ψpre + Ψkeep
Γ, Ψ ⊢ e(e1 , . . . , en ) : τret , Ψpost + Ψkeep
Here, Ψn+1 is the capability held by the caller just before entering
the function. Note that only a part of Ψn+1 , that is Ψpre , needs
to be given to the function. The remaining capabilities, Ψkeep is
kept by the caller and combined with the return capability of thefunction. This capability “flow around” technique provides context
sensitivity as each call site can use a different Ψkeep to avoid
conflating capabilities.
The flow around technique is inspired by similar ideas used in
Cqual [12] and Locksmith [20]. However, unlike Cqual or Locksmith, LP-Race does not require an effect analysis to determine
what to give to the function and what to keep, because the flow
around relation becomes just an additional set of linear equations
so that linear programming automatically discovers what to flow
around. Also, it is more general because it allows fractional amountof capabilities to be flown around.
Polymorphic Function Signatures A polymorphic (i.e., a context
sensitive) alias analysis [8, 7, 23, 14] can be used to generate
polymorphic types for functions. That is, we can quantify function
2 The fields of a struct/union are allowed to have different types and abstract

locations.

types by abstract locations so that functions are given types of theform∀~
ρ.(Ψpre , ~τ ) → (Ψpost , τret )This allows us to type check situations requiring parametric polymorphism, as in the code below.
int c, d;pthread_t tid1, tid2;
void *f(void *p) {*p = 1;}
void main(void) {pthread_create(&tid1, NULL, &f, &c);
pthread_create(&tid2, NULL, &f, &d);}Currently, LP-Race uses monomorphic one-level-flow analysis andso polymorphic function signatures cannot be obtained. We leaveextending LP-Race with polymorphic function signatures for futurework.
3.1.4 Synchronization Primitives
As remarked earlier, our analysis approach is not limited to locks.
Here, we discuss other kinds of synchronization primitives LPRace handles.
Signaling Perhaps the simplest form of synchronization is tosend a signal from one thread to another thread waiting for a signal.
For example, POSIX threads programs use conditional variables
for signaling. LP-Race gives signal primitives like a conditionalvariable the type of the form sig(Ψ) so that a send of a signal is
typed as follows.
Γ, Ψ ⊢ e : sig(Ψ1 ), Ψ2
Γ, Ψ ⊢ send e : int, Ψ2 − Ψ1

int c;
pthread_t tid1, tid2;
sem_t sem;void *f(void *) {sem_wait(&sem);c = 1;}
void main(void) {sem_init(&sem, 0, 0);
pthread_create(&tid1, NULL, &f, &c);
pthread_create(&tid2, NULL, &f, &c);
sem_post(&sem);
sem_post(&sem);}
Figure 7. Double semaphore post.

Ψr ≤ Ψw /NΓ, Ψ ⊢ newrwlock : rwlock(Ψr , Ψw ), Ψ − Ψw
Γ, Ψ ⊢ e : rwlock(Ψr , Ψw ), Ψ1
Γ, Ψ ⊢ rdlock e : int, Ψ1 + Ψr
Γ, Ψ ⊢ e : rwlock(Ψr , Ψw ), Ψ1
Γ, Ψ ⊢ rdunlock e : int, Ψ1 − ΨrΓ, Ψ ⊢ e : rwlock(Ψr , Ψw ), Ψ1
Γ, Ψ ⊢ wrlock e : int, Ψ1 + Ψw
Γ, Ψ ⊢ e : rwlock(Ψr , Ψw ), Ψ1
Γ, Ψ ⊢ wrunlock e : int, Ψ1 − Ψw

And a wait on a signal is typed as follows.
Γ, Ψ ⊢ e : sig(Ψ1 ), Ψ2
Γ, Ψ ⊢ wait e : int, Ψ2 + Ψ1

Figure 8. Read-write lock type rules.

Semaphores Semaphores are straightforward to handle in ourframework. A semaphore is given the type of the form sem(Ψ).
A post of a semaphore is typed as follows.

the type rules for read-write lock acquires and releases, which aremuch like those of regular locks, except that Ψw is used in write
mode and Ψr is used in read-only mode.
Here, newrwlock creates a new read write lock, rdlock e(rdunlock e) acquires (releases) the read-write lock e in readonly mode, and wrlock e (wrunlock e) acquires (releases) the
read-write lock e in write mode.
In the rule for newrwlock, N is the upper bound on the numberof threads. For instance, if a read-write lock l is used to guard
an abstract location ρ, then the type of l would be of the form
rwlock(Ψw , Ψr ) such that Ψw (ρ) ≥ 1. Obtaining a read lockgrants Ψr (ρ) ≤ Ψw (ρ)/N amount of capability, which could beless than 1, but is enough to do a read (i.e., greater than 0). It iseasy to prove that this scheme is sound when the program spawns
at most N threads.

Γ, Ψ ⊢ e : sem(Ψ1 ), Ψ2
Γ, Ψ ⊢ V e : int, Ψ2 − Ψ1
A wait on a semaphore is typed as follows.
Γ, Ψ ⊢ e : sem(Ψ1 ), Ψ2
Γ, Ψ ⊢ P e : int, Ψ2 + Ψ1
Unlike a lock release, a post of a semaphore is not idempotent.
For example, a race must be reported for the program in Figure 7.
It is not difficult to prove that type system is sound for semaphores
with their usual semantics of a post incrementing a counter and a
wait waiting for a counter to be positive and then decrementing thecounter.3 We omit the details for space.
Read-Write Locks LP-Race models read-write locks when theupper bound on the number of live threads are known. Read-write
locks are given types of the form rwlock(Ψr , Ψw ). Figure 8 show
3 This actually implies that the type rule for unlock is somewhat conser-

vative for double unlocking. However, unlocking an already unlocked lockis often considered a bug and has undefined behavior in many thread library specifications. Issues on recursive locking and unlocking is discussed
further in Section 5.

3.1.5 Local Accesses
Consider the program shown in Figure 9. The memory region
allocated in the function f is used only inside the function (which
include threads spawned by the function). To check that such local
uses of memory regions are race free, LP-Race performs an escapeanalysis to determine if an abstract location escapes through globals
or the function arguments or returns. Suppose ̺ does not escape.
Then, LP-Race adds the constraint ϕpre (̺) ≤ 1 where ϕpre is thecapability at the entry of the function, and removes the constraints

pthread_t tid1, tid2;
pthread_mutex_t lock;
void *g(void *q) {pthread_mutex_lock(&lock);*q = *q + 1;
pthread_mutex_unlock(&lock);}
void *f(void *) {int * p = malloc(sizeof(int));*p = 1;pthread_mutex_init(&lock, NULL);
pthread_create(&tid1, NULL, &g, p);pthread_create(&tid2, NULL, &g, p);}
void main(void) {pthread_create(&tid1, NULL, &f, NULL);
pthread_create(&tid2, NULL, &f, NULL);}
Figure 9. Local access example.
App
agetctracesmtprcretawq

Size
2.2
2.2
9.0
52.3

LP Instances
40
24
85
605

Warnings
15
12
42
14

Time
4
5
145
6855

Table 1. Experiment results.
of the form ϕ(̺) ≥ ϕpre (̺). This allows functions to use thelocally allocated locations in a race free manner.
3.1.6 Subtyping
LP-Race takes advantage of the one-level-flow points-to analysis
framework to do one level of subtyping (types are unified underpointers).
We show the subtyping rules for lock types. LP-Race extends
the lock type to lock(Ψin , Ψout ) such that Ψin is used at LCK andΨout is used at NEWL and ULCK. We assert Ψout ≥ Ψin , anduse the following subtyping rule.
Ψin ≥ Ψ′in Ψout ≥ Ψ′outlock(Ψin , Ψout ) ≤ lock(Ψ′in , Ψ′out )The idea is inspired by the read-type write-type separation forsubtyping reference cells. We type other synchronization primitives
similarly. This has the effect of reducing false-aliasing of locks.
3.2 Experiments
LP-Race is implemented in OCaml. LP-Race uses CIL 1.3.6 [19]as the frontend parser, and GLPK 4.2.1 [1] as the backend linear
programming solver. In general, any tool capable of solving asystem of rational linear inequalities can be used as the backend.
The code was compiled using OCaml 3.08 and gcc 3.4.4. The
experiments were run on a PC with a Intel T7200 2GHZ processor
with 2GB of RAM, running Cygwin inside Windows XP.
We ran LP-Race on several POSIX threads applications. We
chose three benchmarks from the Locksmith paper [20], aget,
ctrace and smtprc, mainly to check that the results from LP-Raceagree with their findings, and also tried a larger application, retawq,a multithreaded webserver, to see how LP-Race scales to larger
code base. Table 1 summarizes the results. The size column is thenumber of kilo lines of code after CIL merges the preprocessed

application files and filters out duplicate or unused definitions. The
time column is in seconds. The warnings column shows the numberof possible races reported.
It is worth noting that the warning counts are sensitive to theunderlying alias analysis. LP-Race currently distinguishes possible
races by alias sets only (after removing duplicates), therefore, forinstance, if we had used a very coarse alias analysis that returns
a single alias set containing all locations, then the analysis would
always report at most one warning. Also, with this method, even if
there are multiple races on the same alias set, only one warning isreported. Section 5 discusses issues regarding error reporting.
We reviewed the error reports. For aget, LP-Race was able to detect the races reported in [20]. For ctrace, LP-Race detects the tworaces reported in [20]. In addition, it reports ten false positives. Examining these false positives, as pointed out in [20], some appeared
to be due to semaphores. While LP-Race can handle standard
semaphore uses, ctrace contains a manual read-write semaphore
implemented with a counter, which LP-Race is not able to handle.
Replacing this manual read-write semaphore with LP-Race’s readwrite lock eliminated four false positives. The other false positives
are related to the unused lock problem discussed in Section 5, andaccesses to a global array indexed by thread identifiers. We also observed that the handling of join was necessary for eliminating one
false positive.
For smtprc, many of the warnings are false read-write races
reported due to loops spawning unbounded number of threads (cf.
Section 5). Manually unrolling the loops twice eliminates 19 false
positives. The other false positives are due to accesses to a global
data structure indexed by thread identifiers. We noticed that smtprc
dangerously releases a lock in a loop, which, according to the
POSIX threads specification, has undefined behavior. Such lockreleases could lead to a race if a thread can release a lock that otherthreads are holding (though this is implementation dependent). LPRace correctly reports warnings for such situations thanks to theconservative handling of recursive unlocks. For retawq, many of
the warnings appear to be false positives caused by false aliasing oflocations returned by memory allocation wrapper functions. One
warning appears to be a race, though seemingly benign.
3.2.1 Discussion
The backend of LP-Race, which dominates the running time, is embarrassingly parallel. The backend solves one linear programming
instance per an alias set containing a possibly thread shared location. The third column of Table 1 shows the number of instances
created, after some filtering to remove redundant instances. Eachlinear programming instance is nearly the same size for the samecode base and can be solved independently of the others. Therefore,
by solving each instance in parallel, in theory, we should get near
N times speedup with N parallel processors for applications withmore than N alias sets.
Also, because the running times are dominated by the backend,
the choice of the linear programming solver may affect the performance. We chose GLPK mostly out of convenience 4 , but GLPK
is by no means the fastest linear programming solver. Runningtimes often differ by several orders of magnitude across different
solvers [16]. We leave experimenting with other linear programming solvers for future work.

4. Related Work
Many static race analyses focus on lexically-scoped locking patterns such as the synchronized blocks in Java. The essence oflexically-scoped locking patterns can be cleanly captured as a
4 We based the implementation on a partial OCaml interface for GLPK [15].

lockset-based analysis based on the classical type and effect system. Early systems [9, 10, 13, 4] required the users to supply annotations, whereas more recent work [2, 11, 18, 17] infer locksets
automatically by utilizing powerful reasoning techniques such as
binary decision diagrams and SAT solvers.
A lockset-based analysis for non-lexically scoped locks is said
to require “flow-sensitivity” to infer locks held at each program
point [20, 22], and considered more difficult than that for lexicallyscoped locks. Like lockset-based analyses for scoped locks, theseanalyses are usually limited to locks and lock-like synchronization
patterns. An issue with handling non-lock synchronization patterns
like semaphores and signals is that it is ok for another thread to“release” a semaphore that another thread has “acquired”, while
such a behavior is uncommon for locks.5
Also, unlike that for scoped locks that has a straightforward
formalization as a type and effect system, a lockset-based analysis
for non-scoped locks are rarely formalized and proven sound.6 This
paper gives a simple formalization of non-scoped locks (as well asother synchronization patterns) in terms of capabilities.
Locksmith [20] is a lockset-based analysis that introduces thenotion of correlation analysis to reason about non-scoped locks
used in a context sensitive manner. Relay [22] is a lockset-based
analysis for non-scoped locks that has been applied to a much larger
code base (millions of lines) than the applications we analyzed
with LP-Race. To scale to such a large code base, they parallelize
the analysis to utilize a cluster of high performance machines.
As remarked in Section 3.2, LP-Race should also benefit fromparallel computation. We leave implementing parallelized LP-Racefor future work.
Both Relay and Locksmith employ a number of techniques totrade unlikely sources of unsoundness for precision or speed, suchas optimistic thread-sharedness assumptions and using C types torefine aliasing. Such techniques are important for analyzing largescale real-world programs. Many of such techniques affect only the“may alias” part of the analysis, and therefore, they should also be
adaptable to our framework.
The technique to reduce a static analysis problem to linear programming may be of independent interest. The approach was inspired by the idea of fractional permissions/capabilities, originallyproposed by Boyland [5] as a way to allow parallel reads while
guaranteeing determinism. The idea has been used to reason about
concurrent reads in separation logic [3], and also to check determinism of channel communicating processes [21]. This paper isthe first application of the fractional permissions/capabilities idea
to real world programs.

5. Open Issues
We identify the limitations of the current analysis system. We
address each issue and describe possible remedies.
The analysis does not handle recursive locks because it assumes
that a thread blocks when trying to acquire a lock that is already
held, regardless of who holds the lock. Therefore. If this condition is violated, it is easy to construct a program that gains an invalid amount of capabilities (i.e., greater than 1) by acquiring thesame lock multiple times. Effect-based approaches [9, 10, 13, 4]
can naturally express Java-style lexically-scoped recursive locks.
Effectively handling non-scoped recursive locks is an open issue[22].
One limitation that seems unique to our analysis (and possibly
to others based on the permissions/capabilities idea) occurs when
5 In fact, many threads libraries, including POSIX threads, condemns suchidioms as erroneous.
6 The Locksmith paper [20] formalizes by assuming that each access isannotated with the held locks.

a program spawns an unbounded number of live threads in a loop.
This implies that either the created threads start with no capability,or the loop head has an infinite amount of capabilities (which isinvalid for any program locations that are reachable). In practice,
this makes the analysis report some read-only access as a possible
read-write race. For example, a false race is detected in the program
below.
let x = ref 0 in
while * dospawn(newtid){ !x }Currently, we unroll thread allocating loops manually when LPRace reports a false read-write race.
A related issue is locks created early. The key argument used
to prove soundness is to interpret locks and other lock-like primitives to be “storing” the capabilities in their unlocked state (cf.
Definition 2.3). Therefore, once a lock is created, the capabilities
stored in the lock can prevent a thread from accessing the locations guarded by the lock even when there is no contention on thelocations. In particular, this makes some thread-local accesses untypable, as shown below.
let x = ref 0 in
let l = newlock in
x := 1;
spawn(newtid){ lock l; x := 0; unlock l}spawn(newtid){ lock l; x := 0; unlock l}Here, l must hold the full (i.e., 1) capability for x so that the
spawned threads can write to x. But this implies that x := 1 is
not typable because l is at an unlocked state at that point. A similar
issue appears when accesses are made when the lock is no longer
used (but before the lock is explicitly destroyed). Currently, we fix
such situations by manually moving lock allocation/deletion points
or by inserting a lock acquire/release pair around the unguarded
access. A more principled remedy is to infer program points that
can acquire a lock without contention, and allow such program
points to use the capabilities stored in the lock without actuallyacquiring the lock.
Another issue with our approach is error reporting. Because
the analysis does not compute locksets, LP-Race does not give a
feedback containing held locks at each program location when it
detects a possible race. This can make analyzing false positives
somewhat inconvenient. Currently, LP-Race reports the program
location and the kind (i.e., a read or a write) of accesses made to
the abstract location that failed the check, and whether the error isa possible write-write race or is a read-write race. How to concisely
represent the reason for the race (or a false positive) is an important
issue in race analysis. One approach that may work well with
LP-Race is an interactive debugging interface in which the user
specifies a subset of reported accesses as race free so that LP-Racere-solves the linear programing instance for that location with the
reduced accesses. With such a strategy, we can avoid re-running theentire analysis from scratch.

6. Conclusions
We have presented a new static analysis for race freedom that reduces the problem to linear programming. The analysis is quite
different from more traditional analyses and does not require computation of locksets nor lock linearity/must-aliasness. The analysis has a straightforward formalization as a permissions/capabilities
system, and enjoys benefits such as being able to handle a variety
of synchronization primitives. The preliminary experiment reports
encouraging results analyzing small to medium size multithreaded
C programs.

References[1] GNU Linear Programming Kit.
http://www.gnu.org/software/glpk/glpk.html.
[2] R. Agarwal and S. D. Stoller. Type inference for parameterized
race-free Java. In Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Proceedings,
pages 149–160.

[19] G. C. Necula, S. McPeak, S. P. Rahul, and W. Weimer. CIL:
Intermediate language and tools for analysis and transformation of c
programs. In Compiler Construction, 11th International Conference,
pages 213–228, Grenoble, France, Apr. 2002.
[20] P. Pratikakis, J. S. Foster, and M. W. Hicks. LOCKSMITH: contextsensitive correlation analysis for race detection. In Proceedings of the2006 ACM SIGPLAN Conference on Programming Language Design
and Implementation, pages 320–331, Ottawa, Ontario, Canada, June
2006.

[3] R. Bornat, C. Calcagno, P. W. O’Hearn, and M. J. Parkinson.
Permission accounting in separation logic. In Proceedings of the
32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles ofProgramming Languages, pages 259–270, Long Beach, California,
Jan. 2005.

[21] T. Terauchi and A. Aiken. A capability calculus for concurrency anddeterminism. In Concurrency Theory, 17th International Conference,
volume 4137, pages 218–232, Bonn, Germany, Aug. 2006.

[4] C. Boyapati, A. Salcianu, W. Beebee, Jr., and M. Rinard. Ownershiptypes for safe region-based memory management in real-time Java. In
Proceedings of the 2003 ACM SIGPLAN Conference on Programming
Language Design and Implementation, San Diego, California, June
2003.

[22] J. W. Voung, R. Jhala, and S. Lerner. RELAY: static race detection on
millions of lines of code. In Proceedings of the 6th joint meeting of theEuropean Software Engineering Conference and the ACM SIGSOFTInternational Symposium on Foundations of Software Engineering,
pages 205–214, Dubrovnik, Croatia, Sept. 2007.

[5] J. Boyland. Checking interference with fractional permissions. In
Static Analysis, Tenth International Symposium, pages 55–72, San
Diego, CA, June 2003.
[6] M. Das. Unification-based pointer analysis with directional
assignments. In Proceedings of the 2000 ACM SIGPLAN Conference
on Programming Language Design and Implementation, pages 35–
46, Vancouver B.C., Canada, June 2000.
[7] M. Das, B. Liblit, M. Fähndrich, and J. Rehof. Estimating the impactof scalable pointer analysis on optimization. In Static Analysis, EighthInternational Symposium, pages 260–278, Paris, France, July 2001.
[8] M. Fähndrich, J. Rehof, and M. Das. Scalable context-sensitive flow
analysis using instantiation constraints. In Proceedings of the 2000
ACM SIGPLAN Conference on Programming Language Design and
Implementation, pages 253–263, Vancouver B.C., Canada, June 2000.
[9] C. Flanagan and M. Abadi. Types for safe locking. In D. Swierstra,
editor, 8th European Symposium on Programming, volume 1576 of
Lecture Notes in Computer Science, pages 91–108, Amsterdam, The
Netherlands, Mar. 1999. Springer-Verlag.
[10] C. Flanagan and S. N. Freund. Type-based race detection for Java. In
Proceedings of the 2000 ACM SIGPLAN Conference on Programming
Language Design and Implementation, pages 219–232, Vancouver
B.C., Canada, June 2000.
[11] C. Flanagan and S. N. Freund. Type inference against races. In Static
Analysis, Eleventh International Symposium, pages 116–132, Verona,
Italy, August 2004.
[12] J. S. Foster, T. Terauchi, and A. Aiken. Flow-sensitive type
qualifiers. In Proceedings of the 2002 ACM SIGPLAN Conference
on Programming Language Design and Implementation, Berlin,
Germany, June 2002.
[13] D. Grossman. Type-safe multithreading in Cyclone. In Proceedingsof the 2003 ACM Workshop on Types in Language Design and
Implementation, pages 13–25, New Orleans, Louisiana, Jan. 2003.
[14] J. Kodumal and A. Aiken. The set constraint/cfl reachability
connection in practice. In Proceedings of the 2004 ACM SIGPLAN
Conference on Programming Language Design and Implementation,
pages 207–218, Washington DC, USA, June 2004.
[15] S. Mimram. ocaml-glpk. http://ocaml-glpk.sourceforge.net/.
[16] H. Mittelmann. Benchmarks for optimization software.
http://plato.asu.edu/bench.html.
[17] M. Naik and A. Aiken. Conditional must not aliasing for static
race detection. In Proceedings of the 34th Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, pages
327–338, Nice, France, Jan. 2007.
[18] M. Naik, A. Aiken, and J. Whaley. Effective static race detection
for Java. In Proceedings of the 2006 ACM SIGPLAN Conference on
Programming Language Design and Implementation, pages 308–319,
Ottawa, Ontario, Canada, June 2006.

[23] J. Whaley and M. S. Lam. Cloning-based context-sensitive pointeralias analysis using binary decision diagrams. In Proceedings of the2004 ACM SIGPLAN Conference on Programming Language Design
and Implementation, pages 131–144, Washington DC, USA, June
2004.