ose. A common kind of concurrency
error is deadlock, which occurs when a set of threads is blocked each
trying to acquire a lock held by another thread in that set. Static and
dynamic (run-time) analysis techniques exist to detect deadlocks.
Havelunds GoodLock algorithm detects potential deadlocks at run-
time. However, it detects only potential deadlocks involving exactly two
threads. This paper presents a generalized version of the GoodLock algo-
rithm that detects potential deadlocks involving any number of threads.
Run-time checking may miss errors in unexecuted code. On the positive
side, run-time checking generally produces fewer false alarms than static
analysis.
This paper explores the use of static analysis to automatically reduce
the overhead of run-time checking. We extend our type system, Extended
Parameterized Atomic Java (EPAJ), which ensures absence of races and
atomicity violations, with Boyapati et al.s deadlock types. We give an al-
gorithm that infers deadlock types for a given program and an algorithm
that determines, based on the result of type inference, which run-time
checks can safely be omitted. The new type system, called Deadlock-
Free EPAJ (DEPAJ), has the added benet of giving stronger atomicity
guarantees than previous atomicity type systems.
1
Introduction
Concurrent programs are notorious for containing errors that are dicult to
reproduce and diagnose at run-time. Some common kind of programming er-
rors include deadlocks, data races and atomicity violations. A deadlock occurs
when each thread is blocked trying to acquire a lock held by another thread. A
data race occurs when two threads concurrently access a shared variable and at
least one of the accesses is a write. Atomicity is a common higher-level correct-
ness requirement that expresses non-interference between concurrently executed
methods. A method is atomic if every execution of the program is equivalent to
an execution in which that method is executed without being interleaved with
other concurrently executed methods. This paper focuses on detecting deadlocks.
This work was supported in part by NSF under Grant CCR-0205376 and CNS-
0509230 and ONR under Grants N00014-02-1-0363 and N00014-04-1-0722.
S. Ur, E. Bin, and Y. Wolfsthal (Eds.): Haifa Verication Conf. 2005, LNCS 3875, pp. 191207, 2006.
c Springer-Verlag Berlin Heidelberg 2006 192
R. Agarwal, L. Wang, and S.D. Stoller
The GoodLock algorithm [Hav00] detects potential deadlocks at run-time.
However, it detects only potential deadlocks involving two threads, i.e., each
of those threads is blocked trying to acquire a lock held by the other thread.
This paper presents a generalized version of GoodLock algorithm, that detects
potential deadlocks involving any number of threads in other executions of the
program.
Static analysis can also detect potential deadlocks. Boyapati, Lee and Rinard
[BLR02] introduce a type system that ensures Java programs are deadlock-free.
That type system extends Boyapati and Rinards Parameterized Race Free Java
(PRFJ) type system [BR01], which ensures Java programs are race-free.
Run-time checking and static analysis are both useful. Static analysis can
guarantee that all executions of a program are deadlock-free; run-time checking
cannot. However, due to limitations of the type system, some deadlock-free pro-
grams are not typable; the resulting warnings from the typechecker are called
false alarms
, and they may be dicult to diagnose. On the other hand, run-
time checking generally produces fewer false alarms than static analysis; this is
a signicant practical advantage, since diagnosing all of the warnings from static
analysis of large codebases may be expensive.
This paper extends our type system, Extended Parameterized Atomic Java
(EPAJ) [SAWS05], which ensures absence of races and atomicity violations, with
the deadlock types described in [BLR02]. The new type system, called Deadlock-
Free EPAJ (DEPAJ), ensures absence of deadlocks due to locks and, as an added
benet, gives stronger atomicity guarantees than EPAJ and Atomic Java [FQ03],
which do not consider deadlocks and hence may classify a method as atomic even
if it could deadlock in the middlesomething that cannot happen if the method
executes without interruption by other threads.
The type systems and run-time analysis algorithms considered in this paper
only attempt to detect potential deadlocks caused by locks. They do not consider
wait/notify or other forms of condition synchronization and hence do not detect
deadlocks due to them.
Manually annotating code with the necessary type annotations can be a signif-
icant burden, especially for legacy code. Type inference reduces the annotation
burden by automatically determining types for some or all parts of the program.
This paper presents a type inference algorithm for [BLR02]s basic deadlock
types.
Static analysis can be used to decrease the overhead of run-time checking, in
the following way. First, our type inference algorithm infers deadlock types for
the program. Run-time deadlock detection is then focused on fragments of code
which were not typable. The user can inspect the run-time warnings, which are
more likely to indicate real errors and can provide more detailed and specic
diagnostic information; then, if desired, the user can inspect warnings from the
typechecker. The goal is to reduce the overhead of run-time checking to a level
where it can be used unobtrusively throughout the testing process, or even in
deployed systems, instead of only during a limited period of testing focused on
concurrency errors. Detecting Potential Deadlocks
193
The rest of the paper is organized as follows. Sections 2, 3, 4 and 5 describe
run-time detection of potential deadlocks, deadlock types, type inference for
deadlock types, and our type system DEPAJ respectively. Section 6 presents
our techniques for focused run-time detection of potential deadlocks. Section 7
presents our experiments, Section 8 discusses related work.
2
Run-Time Detection of Potential Deadlocks
The GoodLock algorithm [Hav00] detects potential deadlocks at run-time. It
records a run-time lock tree for each thread. The run-time lock tree for a thread
represents the nested pattern in which locks are acquired by the thread. Each
node of the run-time lock tree is labeled with a lock and represents the thread
acquiring that lock. There is an edge from a node n
1
to a node n
2
if n
1
repre-
sents the most recently acquired lock that the thread holds when it acquires the
lock associated with n
2
. At each instant, each run-time lock tree has one node
designated as the current node; the path from the root of the tree to that node
represents the nested acquires of locks held by that thread at that instant. If a
thread re-acquires a lock that it already holds, its run-time lock tree does not
contain a node representing the re-acquire. When a thread acquires a lock that it
does not already hold, if there is already a child of the current node labeled with
that lock, that child becomes the current node, otherwise a new child labeled
with that lock is created and becomes the current node. At the end of the execu-
tion of the program, if there exist threads t
1
and t
2
and locks l
1
and l
2
such that
t
1
acquires l
2
while holding l
1
, and t
2
acquires l
1
while holding l
2
, then a warning
of potential deadlock is issued, unless there is a common lock, called a gate lock,
that is held by both threads when they acquire l
1
and l
2
; the gate lock prevents
the acquires of l
1
and l
2
from being interleaved in a way that leads to deadlock.
The worst-case time complexity of the algorithm is O(
|T |
3
× |T hread|
2
), where
|T | is the size of the largest run-time lock tree, and T hread is the set of threads.
However, this algorithm only detects potential deadlocks caused by interleaving
of lock acquires in two threads.
We present a generalized version of the GoodLock algorithm that detects
potential deadlocks involving any number of threads. In particular, it checks
whether there exist distinct threads t
0
, . . . , t
m
1
and locks l
0
, . . . , l
m
1
such that,
for all i = 0..m
1, t
i
holds lock l
i
while acquiring lock l
i+1 mod m
. Note that we
always ignore a thread re-acquiring a lock it already holds, so a thread acquiring
l
i+1 mod m
while holding l
i
implies l
i+1 mod m
and l
i
are dierent locks. In the
absence of other constraints on the schedule (e.g., due to gate locks or start-
join synchronization), such acquires can be interleaved in a way that leads to
deadlock. We call this the Potential for Deadlock from Locks Ignoring GateLocks
(PDL-IGL) condition.
The algorithm constructs a run-time lock tree for each thread during execu-
tion, as described above. At the end of the execution, it constructs a run-time
lock graph, which is a directed graph G = (V, E), where V contains all the
nodes of all the run-time lock trees, and the set E of directed edges contains (1) 194
R. Agarwal, L. Wang, and S.D. Stoller
tree edges: the directed (from parent to child) edges in each of the run-time lock
trees, and (2) inter edges: bidirectional edges between nodes that are labeled
with the same lock and that are in dierent run-time lock trees.
For a run-time lock graph G, a valid path is a path that does not contain
consecutive inter edges and such that nodes from each lock tree appear as at
most one consecutive subsequence in the path. Similarly, a valid cycle is a cycle
that does not contain consecutive inter edges and nodes from each thread appear
as at most one consecutive subsequence in the cycle.
As an example, Figure 1