Sound Static Deadlock Analysis for C/Pthreads
(Extended Version)
Daniel Kroening

Daniel Poetzl

Peter Schrammel

University of Oxford
Oxford, UK

University of Oxford
Oxford, UK

University of Sussex
Brighton, UK

arXiv:1607.06927v1 [cs.PL] 23 Jul 2016

kroening@cs.ox.ac.uk

daniel.poetzl@cs.ox.ac.uk p.schrammel@sussex.ac.uk
Björn Wachter
University of Oxford
Oxford, UK

bjoern.wachter@gmail.com
ABSTRACT
We present a static deadlock analysis approach for C/pthreads.
The design of our method has been guided by the requirement to analyse real-world code. Our approach is sound
(i.e., misses no deadlocks) for programs that have defined
behaviour according to the C standard, and precise enough
to prove deadlock-freedom for a large number of programs.
The method consists of a pipeline of several analyses that
build on a new context- and thread-sensitive abstract interpretation framework. We further present a lightweight
dependency analysis to identify statements relevant to deadlock analysis and thus speed up the overall analysis. In our
experimental evaluation, we succeeded to prove deadlockfreedom for 262 programs from the Debian GNU/Linux distribution with in total 2.6 MLOC in less than 11 hours.

CCS Concepts
•Theory of computation → Program analysis;

Keywords
deadlock detection, lock analysis, static analysis, abstract
interpretation

1.

INTRODUCTION

Locks are the most frequently used synchronisation mechanism in concurrent programs to guarantee atomicity, prevent undefined behaviour, and hide weak-memory effects of
the underlying architectures. However, locks, if not correctly used, can cause a deadlock, where one thread holds
a lock that the other one needs and vice versa. Deadlocks
can have disastrous consequences such as the Northeastern
Blackout [34], where a monitoring system froze, and prevented detection of a local power problem, which brought
down the power network of the Northeastern United States.

In small programs, deadlocks may be spotted easily. However, this is not the case in larger software systems. So called
locking disciplines aim at preventing deadlocks but are difficult to maintain as the system evolves, and every extension
bears the risk of introducing deadlocks. For example, if the
order in which locks are acquired is different in different
parts of the code this may cause a deadlock.
The problem is exacerbated by the fact that deadlocks are
difficult to discover by means of testing. Even a test suite
with full line coverage is insufficient to detect all deadlocks,
and similar to other concurrency bugs, triggering a deadlock requires a specific thread schedule and set of particular
program inputs. Therefore, static analysis is a promising
candidate for a thorough check for deadlocks. The challenge is to devise a method that is scalable and yet precise
enough. The inherent trade-off between scalability and precision has gated static approaches to deadlock analysis, and
many previously published results had to resort to unsound
approximations in order to obtain scalability (we provide a
comprehensive survey of the existing static approaches in
Sec. 9).
We hypothesise that static deadlock detection can be performed with a sufficient degree of precision and scalability
and without sacrificing soundness. To this end, this paper
presents a new method for statically detecting deadlocks.
To quantify scalability, we have applied our implementation
to a large body of real-world concurrent code from the Debian GNU/Linux project.
Specifically, this paper makes the following contributions:
1. The first, to the best of our knowledge, sound static
deadlock analysis approach for C/pthreads that can
handle real-world code.
2. A new context- and thread-sensitive abstract interpretation framework that forms the basis for the analyses
that comprise our approach. The framework unifies
contexts, threads, and program locations via the concept of a place.
3. A novel lightweight dependency analysis which identifies statements that could affect a given set of program
expressions. We use it to speed up the pointer analysis by focusing it to statements that are relevant to
deadlock analysis.
4. We show how to build a lock graph that soundly captures a variety of sources of imprecision, such as maypoint-to information and thread creation in loops/recursions, and how to combine the cycle detection with

26
27
1
2
3

i n t main ( )
{
pthread_t t i d ;

4

28
29
30
31

p t h r e a d _ c r e a t e (& t i d , 0 ,
thread , 0 ) ;

5
6
7

32
33
34

pthread_mutex_lock (&m1 ) ;
pthread_mutex_lock (&m3 ) ;
pthread_mutex_lock (&m2 ) ;
func1 ( ) ;
pthread_mutex_unlock(&m2 ) ;
pthread_mutex_unlock(&m3 ) ;
pthread_mutex_unlock(&m1 ) ;

8
9
10
11
12
13
14
15

void ∗ t h r e a d ( )
{
pthread_mutex_lock (&m1 ) ;
pthread_mutex_lock (&m2 ) ;
pthread_mutex_lock (&m3 ) ;
x = 1;
pthread_mutex_unlock(&m3 ) ;
pthread_mutex_unlock(&m2 ) ;
pthread_mutex_unlock(&m1 ) ;

35

pthread_mutex_lock (&m4 ) ;
pthread_mutex_lock (&m5 ) ;
x = 2;
pthread_mutex_unlock(&m5 ) ;
pthread_mutex_unlock(&m4 ) ;

36
37
38
39
40
41

r e tu r n 0 ;

42

pthread_join ( tid , 0 ) ;

16

43

}

44

i n t func2 ( i n t a )
{
pthread_mutex_lock (&m5 ) ;
pthread_mutex_lock (&m4 ) ;
if (a)
x = 3;
else
x = 4;
pthread_mutex_unlock(&m4 ) ;
pthread_mutex_unlock(&m5 ) ;
r e tu r n 0 ;
}

17

int r ;
r = func2 ( 5 )

18
19
20

r e tu r n 0 ;

21
22

}

45
46
47
48
49

22
23
24
25

void func1 ( )
{
x = 0;
}

50
51
52
53
54
55

Figure 4: Example of a deadlock-free program

a non-concurrency check to prune infeasible cycles.
5. A thorough experimental evaluation on 715 programs
from Debian GNU/Linux with 7.1 MLOC in total and
up to 50KLOC per program.

2.

OVERVIEW

The design of our analyses has been guided by the goal
to analyse real-world concurrent C/pthreads code in a sound
way. Fig. 3 gives an overview of our analysis pipeline. An arrow between two analyses indicates that the target uses information computed by the source. We use a dashed arrow from the non-concurrency analysis to the cycle detection to indicate that the required information is computed
on-demand (i.e., the cycle detection may repeatedly query
the non-concurrency analysis, which computes the result in
a lazy fashion). All of the analyses operate on a graph representation of the program (introduced in Sec. 3.1). The
exception is the cycle detection phase, which only uses the
lock graph computed in the lock graph construction phase.
The pointer analysis, may- and must-lockset analysis, and
the lock graph construction are implemented on top of our
new generic context- and thread-sensitive analysis framework (described in detail in Sec. 3.2). To enable trade-off
between precision and cost, the framework comes in a flowinsensitive and a flow-sensitive version. The pointer analysis
was implemented on top of the former (thus marked with **
in Fig. 3), and the may- and must-lockset analysis and the
lock graph construction on top of the latter (marked with *).
The dependency analysis and the non-concurrency analysis
are separate standalone analyses.

Context and thread sensitivity.
Typical patterns in real-world C code suggest that an approach that provides a form of context-sensitivity is necessary to obtain satisfactory precision on real-world code,
as otherwise there would be too many false deadlock reports. For instance, many projects provide their own wrap-

pers for the functions of the pthreads API. Fig. 1, for example, shows a lock wrapper from the VLC project. An analysis that is not context-sensitive would merge the points-to
information for pointer p from different call sites invoking
vlc_mutex_lock(), and thus yield many false alarms.
Thread creation causes a similar problem. For every call
to pthread_create(), the analysis needs to be determine
which thread is created (i.e., the function identified by the
pointer passed to pthread_create()). This is straightforward if a function identifier is given to pthread_create().
However, similar to the case of lock wrappers above, projects
often provide wrappers for pthread_create(). Fig. 1 shows
a wrapper for pthread_create() from the memcached project.
The wrapper then uses the function pointer that is passed
to create_worker() to create a thread. Maintaining precision in such cases requires us to track the flow of function
pointer values from function arguments to function parameters. This is implemented directly as part of the analysis
framework (as opposed to in the full points-to analysis).

Dependency analysis.
Deadlock detection requires the information which lock
objects an expression used in a pthread_mutex_lock() call
may refer to. We compute this data using the pointer analysis, which is potentially expensive. However, it is easy to
see that potentially many assignments and function calls in
a program do not affect the values of lock expressions. Consider for example Fig. 4. The accesses to x cannot affect
the value of the lock pointers m1–m5. Further, the code in
function func1 cannot affect the values of the lock pointers,
and thus in turn the call func1() in line 11 cannot affect
the the lock pointers.
We have developed a lightweight context-insensitive, flowinsensitive analysis to identify statements that may affect a
given set of expressions. The result is used to speed up
the pointer analysis. The dependency analysis is based on
marking statements which (transitively) share common variables with the given set of expressions. In our case, the
relevant expressions are those used in lock-, create-, and
join-statements. For the latter two we track the thread ID
variable (first parameter of both) whose value is required
to determine which thread is joined by a join operation.
We give the details of the dependency analysis in Sec. 4.

Non-concurrency analysis.
A deadlock resulting from a thread 1 first acquiring lock m1
and then attempting to acquire m2 (at program location ℓ1 ),
and thread 2 first acquiring m2 and then attempting to acquire m1 (at program location ℓ2 ) can only occur when in a
concrete program execution the program locations ℓ1 and ℓ2
run concurrently. If we have a way of deciding whether two
locations could potentially run concurrently, we can use this
information to prune spurious deadlock reports. For this
purpose we have developed a non-concurrency analysis that
can detect whether two statements cannot run concurrently
based on two criteria.
Common locks. If thread 1 and thread 2 hold a common
lock at locations ℓ1 and ℓ2 , then they cannot both simultaneously reach those locations, and hence the deadlock cannot
happen. This is illustrated in Fig. 4. The thread main() attempts to acquire the locks in the sequence m1 , m3 , m2 , and
the thread thread() attempts to acquire the locks in the sequence m1 , m2 , m3 . There is an order inversion between m2
and m3 , but there is no deadlock since the two sections 8–14
and 28–34 (and thus in particular the locations 10 and 30)
are protected by the common lock m1 . The common locks

C program
1
2
3
4
1
2
3
4
5
6
7
8
9
10
11
12
13

void v l c _ mu t e x _ l o c k ( v l c _ mu t e x _ t ∗p ) {
i n t v a l = pthread_mutex_lock ( p ) ;
VLC_THREAD_ASSERT ( " l o c k i n g mutex " ) ;
}

function pointer
call removal

void c r e a t e _ wo r ke r ( void ∗(∗ func ) ( void ∗ ) ,
void ∗arg ) {
pthread_attr_t attr ;
int ret ;
p t h r e a d _ a t t r _ i n i t(& a t t r ) ;
if ( ( r e t=pthread_create (
&((THREAD∗) arg)−> t h r e a d _ i d ,
&a t t r , func , arg ) ) ! = 0 ) {
f p r i n t f ( s t d e r r , " E r r o r : %s\n " ,
strerror ( ret ) ) ;
exit (1 );
}
}

Figure 1: Lock and create wrappers

lock graph
construction *
yes
may lockset
analysis *

cycle detection

must lockset
analysis *

non-concurrency
check

pointer
analysis **

return removal

ICFA construction

ICFA

Figure 2: ICFA constr.

criterion has first been described by Havelund [18] (common
locks are called gatelocks there).
Create and join. Statements might also not be able to
run concurrently because of the relationship between threads
due to the pthread_create() and pthread_join() operations. In Fig. 4, there is an order inversion between the
locks of m5 and m4 by function func2(), and the locks of
m4 , m5 of thread thread(). Yet there is no deadlock since
the thread thread() is joined before func2() is invoked.
Our non-concurrency analysis makes use of the must lockset analysis (computing the locks that must be held) to
detect common locks. To detect the relationship between
threads due to create and join operations it uses a search
on the program graph for joins matching earlier creates. We
give more details of our non-concurrency analysis in Sec. 5.

3.

dependency
analysis

ANALYSIS FRAMEWORK

In this section, we first introduce our program representation, then describe our context- and thread-sensitive framework, and then describe the pointer analysis and lockset
analyses that are implemented on top of the framework.

3.1 Program Representation
Preprocessing. Our tool takes as input a concurrent C
program using the pthreads threading library. In a first step
the calls to functions through function pointers are removed.
A call is replaced by a case distinction over the functions
the function pointer could refer to. Specifically, a function
pointer can only refer to functions that are type-compatible
and of which the address has been taken at some point in the
code. This is illustrated in Fig. 5 (top). Functions f2() (address not taken) and f4() (not type-compatible) do not have
to be part of the case distinction. In a second step, functions
with multiple exit points (i.e., multiple return statements)
are transformed such as to have only one exit points (illustrated in Fig. 5 (bottom)).
Interprocedural CFAs. We transform the program into
a graph representation which we term interprocedural control flow automaton (ICFA). The functions of the program
are represented as CFAs [19]. CFAs are similar to control
flow graphs, but with the nodes representing program locations and the edges being labeled with operations. ICFAs
have additional inter-function edges modeling function entry, function exit, thread entry, thread exit, and thread join.
Fig. 4 shows a concurrent C program and Fig. 6 shows its
corresponding ICFA (leaving off thread exit and thread join
edges and the function func1()).

Figure 3: Analysis pipeline

We denote by Prog a program (represented as an ICFA),
by Funcs the set of identifiers of the functions, by L =
{ℓ0 , . . . , ℓn−1 } the set of program locations, by E the set
of edges connecting the locations, and by op(e) a function
that labels each edge with an operation. For example, in
Fig. 6, the edge between locations 49 and 52 is labeled with
the operation x=3, and the edge between locations 19 and
46 is labeled with the operation func entry(5, a).
We further write L(f ) for the locations in function f . Each
program location is contained in exactly one function. The
function func(ℓ) yields the function that contains ℓ. The set
of variable identifiers in the program is denoted by Vars.
We assume that all identifiers in Prog are unique, which can
always be achieved by a suitable renaming of identifiers.
We treat lock, unlock, thread create, and thread join as
primitive operations. That is, we do not analyse the body
of e.g. pthread_create() (as implemented in e.g. glibc on
GNU/Linux systems). Instead, our analysis only tracks the
semantic effect of the operation, i.e., creating a new thread.
Apart from intra-function edges we also have inter-function
edges that can be labeled with the five operations func entry,
func exit, thread entry, thread exit, and thread join.
A function entry edge (func entry) connects a call site to
the function entry point. The edge label also includes the
function call arguments and the function parameters. For
example, func entry(5, a) indicates that the integer literal 5
is passed to the call as an argument, which is assigned to
function parameter a. A function exit edge (func exit) connects the exit point of a function to every call site calling
the function. Our analysis algorithm filters out infeasible
edges during the exploration of the ICFA. That is, if a function entry edge is followed from a function f1 to function f2 ,
then the analysis algorithm later follows the exit edge from
f2 to f1 , disregarding exit edges to other functions.
A thread entry edge (thread entry) connects a thread creation site to all potential thread entry points. It is necessary
to connect to all potential thread entry points since often
a thread creation site can create threads of different types
(i.e., corresponding to different functions), depending on the
value of the function pointer passed to pthread_create().
Analogous to the case of function exit edges, our analysis
algorithm tracks the values of function pointers during the
ICFA exploration. At a thread creation site it thus can resolve the function pointer, and only follows the edge to the
thread entry point corresponding to the value of the function
pointer.
A thread exit edge connects the exit point of a thread
to the location following all thread creation sites, and a

no

func2(int a)
1
2
3
4
5
6
7
8
9

void f 1 ( ) { }
void f 2 ( ) { }
void f 3 ( ) { }
int f4 ( ) { }
...
. . . = &f 1 ;
. . . = &f 3 ;
. . . = &f 4 ;
fp ( ) ;

1
2

⇒

3
4
5
6

main()

...
i f ( fp== f 1 )
f1 ( ) ;
else
i f ( fp== f 3 )
f3 ( ) ;

46

5

lock(m5 )
47

8

lock(m4 )
func entry(5, a)

48
1
2
1
2
3
4
5
6
7
8

int f ( ) {
if ( . . . )
r e tu r n 0 ;
else
r e tu r n 1 ;
}
...
a = f ();

3
4
5
6

⇒

7
8
9
10
11
12
13

int f () {
int ret ;
if ( . . . )
ret = 0;
goto END;
else
ret = 1;
goto END;
END:
r e tu r n r e t ;
}
...
a = f ();

thread()
thread entry(thread, 0, par)
28

create(&tid, 0,
thread, 0)

lock(m1 )

lock(m3 )

lock(m2 )

9

30

...
39

[a 6= 0]

[a = 0]

...

49

51

16

x = 3

x = 4
52

return 0

unlock(m5 )

r = func2(3)
func exit(0, r)

40

unlock(m4 )

21

return 0

55

Figure 5: Function pointers and returns

join(tid, 0)
19

...
54

29

22

42

return 0
43

Figure 6: ICFA associated with the program in Fig. 4

thread join edge connects a thread exit point to all join operations in the program.

3.2 Analysis Framework – Overview
Our framework to perform context- and thread-sensitive
analyses on ICFAs is based on abstract interpretation [12].
It implements a flow-sensitive and flow-insensitive fixpoint
computation over the ICFA, and needs to be parametrised
with a custom analysis to which it delegates the handling of
individual edges of the ICFA. We provide more details and
a formalization of the framework in the next section.
Our analysis framework unifies contexts, threads, and program locations via the concept of a place. A place is a tuple (ℓ0 , ℓ1 , . . . , ℓn ) of program locations. The program locations ℓ0 , . . . , ℓn−1 are either function call sites or thread
creation sites in the program (such as, e.g., location 19 in
Fig. 6). The final location ℓn can be a program location
of any type. The locations ℓ0 , . . . , ℓn−1 model a possible
function call and thread creation history that leads up to
program location ℓn . We denote the set of all places for a
given program by P . We use the + operator to extend tuples, i.e., (ℓ0 , . . . , ℓn−1 ) + ℓn = (ℓ0 , . . . , ℓn−1 , ℓn ). We further
write |p| for the length of the place. We write p[i] for element i (indices are 0-based). We use slice notation to refer
to contiguous parts of places; p[i : j] denotes the part from
index i (inclusive) to index j (exclusive), and p[ : i] denotes
the prefix until index i (exclusive). We write top(p) for the
last location in the place.
As an example, in Fig. 6, place (19, 49) denotes the program location 49 in function func2() when it has been
invoked at call site 19 in the main function. If function
func2() were called at multiple program locations ℓ1 , . . . ,
ℓm in the main function, we would have different places
(ℓ1 , 49), . . . , (ℓm , 49) for location 49 in function func2(). Similarly, for the thread function thread() and, e.g., location
29, we have a place (5, 29) with 5 identifying the creation
site of the thread.
Each place has an associated abstract thread identifier,
which we refer to as thread ID for short. Given a place
p = (ℓ0 , . . . , ℓn ), the associated thread ID is either t = ()
(the empty tuple) if no location in p corresponds to a thread
creation site, or t = ℓ0 , . . . , ℓi , such that ℓi is a thread cre-

ation site and all ℓj with j > i are not thread creation sites.
It is in this sense that our analysis is thread-sensitive, as the
information computed for each place can be associated with
an abstract thread that way. We write get thread(p) for the
thread ID associated with place p.
The analysis framework must be parametrised with a custom analysis. The framework handles the tracking of places,
the tracking of the flow of function pointer values from function arguments to function parameters, and it invokes the
custom analysis to compute dataflow facts for each place.
The domain, transfer function, and join function of the
framework are denoted by Ds , Ts , and ⊔s , respectively,
and the domain, transfer function, and join function of the
parametrising analysis are denoted by Da , Ta , and ⊔a . The
custom analysis has a transfer function Ta : E × P →
(Da → Da ) and a join function ⊔a : Da × Da → Da .
The domain of the framework (parametrised by the custom analysis) is then Ds = Fpms × Da , the transfer function is Ts : E × P → (Ds → Ds ), and the join function is
⊔s : Ds × Ds → Ds .
The set Fpms is a set of mappings from identifiers to
functions which map function pointers to the functions they
point to. We denote the empty mapping by ∅. We further
write fpm(fp) = ⊥ to indicate that fp is not in dom(fpm)
(the domain of fpm). A function pointer fp might be mapped
by fpm either to a function f or to the special value d (for
“dirty”) which indicates that the analysed function assigned
to fp or took the address of fp. In this case we conservatively
assume that the function pointer could point to any thread
function.

3.3 Analysis Framework – Details
We now describe the formalization of the analysis framework which is shown in Fig. 7. The figure gives the flowsensitive variant of our framework. We refer to Appendix A
for the flow-insensitive version. The figure gives the domain,
join function ⊔s and transfer function Ts which are defined
in terms of the join function ⊔a and transfer function Ta
of the parametrising analysis (such as the lockset analyses
defined in the next section).
The function nexts (e, p) defines how the place p is updated
when the analysis follows the ICFA edge e. For example, on

Domain: Ds = Fpms × Da
s1s ⊔s s2s =(fpm, sa )
with s1s = (fpm 1 , s1a )
with s2s = (fpm 2 , s2a )
with fpm = fpm 1 ⊔fp fpm 2
with sa = s1a ⊔a s2a
fpm 1 ⊔fp fpm 2 = fpm
fpm(fp) =

d fpm 1 (fp) = d ∨ fpm 2 (fp) = d


v (fpm 1 (fp) = v ∧ (fp ∈
/ dom(fpm 2 ) ∨ fpm 2 (fp) = v))∨



⊥

(fpm 2 (fp) = v ∧ (fp ∈
/ dom(fpm 1 ) ∨ fpm 1 (fp) = v))
otherwise

the function returns to is added to the place (which is the
location following the call to the function). The thread entry
and func entry cases are delegated to entrys (p, ℓ). The first
case of the function handles recursion. If a location ℓ′′ of the
called function is already part of the place, then the prefix of
the place that corresponds to the original call to the function
is reused (first case). If no recursion is detected, the entry
location of the function is simply added to the current place
(second case). For intra-function edges (last case of nexts ),
the last location is removed from the place and the target
location of the edge is added.
The overall result of the analysis is a mapping s ∈ P →
(Fpms × Da ). The result is defined via a fixpoint equation [12]. We obtain the result by computing the least fixpoint (via a worklist algorithm) of the equation below (with
s0 denoting the initial state of the places):
s = s0 ⊔ λ p.

G

c

Ts Je, p′ K(s(p′ ))

p′ ,e s.t.np(p,p′ ,e)

With e = (ℓ1 , ℓ2 ), top(p) = ℓ1 , f = func(ℓ2 ), and n = |p|:
′

nexts (e, p) =

entrys (p, ℓ2 )
p[: n − 2] + ℓ2

p[: n − 1] + ℓ2

with np(p, p , (ℓ1 , ℓ2 )) = ℓ1 = top(p′ )∧
ℓ2 = top(p)∧
op(e) ∈ {thread entry, func entry}
op(e) ∈ {func exit, thread exit, thread join}
otherwise

nexts ((ℓ1 , ℓ2 ), p′ ) = p
with s ⊔ s′ = λ p. s(p) ⊔c s′ (p)

Ts Je, pK(ss ) = (∅, Ta Je, pK(sa ))

The equation involves computing the join over all places p′
and edges e in the ICFA such that np(p, p′ , e).
We next describe the definition of the transfer function
of the framework in more detail. The definition consists of
four cases: (1) function entry, (2) thread entry, (3) function
exit, thread exit, thread join, and (4) intra-function edges.
(1) When applying a function entry edge, a new function
pointer map fpm ′ is created by assigning arguments to parameters and looking up the values of the arguments in the
current function pointer map fpm. As in the following cases,
the transfer function Ta of the custom analysis is applied to
the state sa .
(2) Applying a thread entry edge to a state sc yields one
of two outcomes. When the value of the function pointer
argument thr matches the target of the edge (i.e., the edge
enters the same function as the function pointer points to),
then the function pointer map is updated with arg and par
(as in the previous case), and the transfer function of the
custom analysis is applied. Otherwise, the result is the bottom element ⊥c = (∅, ⊥a ).
(3) The function pointer map is cleared (as its domain
contains only parameter identifiers which are not accessible
outside of the function), and the custom transfer function is
applied.
(4) The custom transfer function is applied.
As is not shown for lack of space in Fig. 7, if a function
pointer fp is assigned to or its address is taken, its value is
set to d in fpm, thus indicating that it could point to any
thread function.

With e = (ℓsrc , ℓtgt ), op(e) = op, and ss = (fpm, sa ):

Implementation.

entrys (p, ℓ) =
 ′
p + ℓ′ + ℓ
p+ℓ

p = p′ + ℓ′ + ℓ′′ + p′′ ∧ func(ℓ′′ ) = f
otherwise

With
e
=
(ℓsrc , ℓtgt ),
func entry(arg 1 , . . . , arg k , par 1 , . . . , par k ),
(fpm, sa ):

op(e)
and ss

=
=

Ts Je, pK(ss ) =(fpm ′ , Ta Je, p K(sa ))
fpm ′ (par i ) =


arg i
fpm(arg i )

is func(arg i )
is func pointer(arg i )

With e = (ℓsrc , ℓtgt ), f = func(ℓtgt ), op(e) =
thread entry(thr , arg , par ), and ss = (fpm, sa ):

(fpm ′ , Ta Je, pK(sa )) match fp(fpm, thr , f )
Ts Je, pK(ss ) =
(∅, ⊥a )
otherwise
match fp(fpm, thr , f ) =
(is func pointer(thr ) ∧ fpm(thr ) ∈ {⊥, d, f }) ∨
(is func(thr ) ∧ thr = f )
With
e
=
(ℓsrc , ℓtgt ),
op(e)
{func exit, thread exit, thread join}, and ss = (fpm, sa ):

∈

Ts Je, pK(ss ) = (fpm, Ta Je, pK(sa ))
Figure 7: Context-, thread-, and flow-sensitive framework

a func exit edge, the last two locations are removed from the
place (which are the exit point of the function, and the location of the call to the function), and the location to which

During the analysis we need to keep a mapping from places
to abstract states (which we call the state map). However,
directly using the places as keys for the state maps in all
analyses can lead to high memory consumption. Our implementation therefore keeps a global two-way mapping (shared
by all analyses in Fig. 3) between places and unique IDs for
the places (we call this the place map). The state maps
of the analyses are then mappings from unique IDs to abstract states, and the analyses consult the global place map

Domain: 2Objs ∪ {{⋆}}

s1 ∪ s2 if s1 , s2 6= {⋆}
s1 ⊔ s2 =
{⋆}
otherwise
With op(e) =lock(a):
s ∪ vs(p, a)
T Je, pK(s) =
{⋆}

if s, vs(p, a) 6= {⋆}
otherwise

With op(e) = unlock(a):

∅


s − vs(p, a)
T Je, pK(s) =


s

if |s| = 1 ∧ s 6= {⋆}
if |s ∩ vs(p, a)| = 1∧
s 6= {⋆} ∧ vs(p, a) 6= {⋆}
otherwise

With op(e) ∈ {thread entry, thread exit, thread join}:

T Je, pK(s) = ∅
Figure 8: May lockset analysis

Below we first describe a semantic characterisation of dependencies between expressions and assignments, and then
devise an algorithm to compute dependencies based on syntax only (specifically, the variable identifiers occuring in the
expressions/assignments).

Semantic characterisation of dependencies.
Let AS = {e ∈ E(Prog) | is assign(op(e))} be the set of
assignment edges. Let exprs be a set of starting expressions.
Let further R(a), W (a) denote the set of memory locations
that an expression or assignment a may read (resp. write)
over all possible executions of the program. Let further
M (a) = R(a) ∪ W (a). Then we define the immediate dependence relation dep as follows (with ∗ denoting transitive
closure and ; denoting composition):
dep 1 ⊆ exprs × AS , (a, b) ∈ dep 1 ⇔ R(a) ∩ W (b) 6= ∅
dep 2 ⊆ AS × AS , (a, b) ∈ dep 2 ⇔ R(a) ∩ W (b) 6= ∅
dep = dep 1 ; dep ∗2

We use a standard points-to analysis that is an instantiation of the flow-insensitive version of the above framework
(see Appendix A). It computes for each place an element
of Vars → (2Objs ∪ {{⋆}}). That is, the set of possible values of a pointer variable is either a finite set of objects it
may point to, or {⋆} to indicate that it could point to any
object. We use vs(p, a) to denote the value set at place p
of pointer a. The pointer analysis is sound for concurrent
programs due to its flow-insensitivity [32].

If (a, b) ∈ dep 1 , then the evaluation of expression a may
read a memory location that is written to by assignment b.
If (a, b) ∈ dep 2 , then the evaluation of the assignment a may
read a memory location that is written to by the assignment b. If (a, b) ∈ dep, this indicates that the expression a
can (transitively) be influenced by the assignment b. We say
a depends on b in this case.
The goal of our dependency analysis is to compute the set
of assignments A = dep|( ,a)7→a (the binary relation A projected to the second component). However, we cannot directly implement a procedure based on the definitions above
as this would require the functions R(), W () to return the
memory locations accessed by the expressions/assignments.
This in turn would require a pointer analysis–the very thing
we are trying to optimise.
Thus, in the next section, we outline a procedure for computing the relation dep which relies on the symbols (i.e.,
variable identifiers) occuring in the expressions/assignments
rather then the memory locations accessed by them.

3.5 Lockset Analysis

Computing dependencies.

to translate between places and IDs when needed.
In the two-way place map, the mapping from places to
IDs is implemented via a trie, and the mapping from IDs to
places via an array that stores pointers back into the trie.
The places in a program can be efficiently stored in a trie
as many of them share common prefixes. We give further
details in Figure 16 in Appendix D.

3.4 Pointer Analysis

Our analysis pipeline includes a may lockset analysis (computing for each place the locks that may be held) and a
must lockset analysis (computing for each place the locks
that must be held). The former is used by the lock graph
analysis, and the latter by the non-concurrency analysis.
The may lockset analysis is formalised in Fig. 8 as a custom analysis to parametrise the flow-sensitive framework
with. The must lockset analysis is given in Appendix C.
Both the may and must lockset analyses makes use of the
previously computed points-to information by means of the
function vs(). In both cases, care must be taken to compute
sound information from the may-point-to information provided by vs(). For example, for the may lockset analysis on
an unlock(a) operation, we cannot just remove all elements
in vs(p, a) from the lockset, as an unlock can only unlock
one lock. We use ls a (p), ls u (p) to denote the may and must
locksets at place p.

4.

DEPENDENCY ANALYSIS

We have developed a context-insensitive, flow-insensitive
dependency analysis to compute the set of assignments and
function calls that might affect the value of a given set of expressions (in our case the expressions used in lock-, create-,
and join-statements). The purpose of the analysis is to speed
up the following pointer analysis phase (cf. Fig. 3).

In this section we outline how we can compute an overapproximation of the set of assignments A as defined above.
Let symbols(a) be a function that returns the set of variable
identifiers occuring in an expression/assignment. For example, symbols(a[i]->lock) = {a, i} and symbols(*p=q+1) =
{p, q}. As stated in Sec. 3.1, in our program representation
all variable identifiers in a program are unique. We first
define the relation sym 2 which indicates whether two assignments have common symbols:
sym 2 ⊆ AS × AS
(a, b) ∈ sym 2 ⇔ symbols(a) ∩ symbols(b) 6= ∅
Our analysis relies on the following property: If two assignments a, b can access a common memory location (i.e.,
M (a) ∩ M (b) 6= ∅), then (a, b) ∈ sym ∗2 . This can be seen
as follows. Whenever a memory region/location is allocated in C it initially has at most one associated identifier. For example, the memory allocated for a global variable x at program startup has initially just the associated
identifier x. Similarly, memory allocated via, e.g., a = (int
*)malloc(sizeof(int) * NUM) has initially only the associated identifier a. If an expression not mentioning x, such
as *p, can access the associated memory location, then the
address of x must have been propagated to p via a sequence
of assignments such as q=&x, s->f=q, p=s->f, with each of

the adjacent assignments having common variables. Thus, if
a, b can access a common memory location, then both must
be “connected” to the initial identifier associated with the
location via such a sequence. Thus, in particular, a, b are
also connected. Therefore, (a, b) ∈ sym ∗2 .
We next define the sym relation which also incorporates
the starting expressions:
sym 1 ⊆ exprs × AS
(a, b) ∈ sym 1 ⇔ symbols(a) ∩ symbols(b) 6= ∅
sym = sym 1 ; sym ∗2
As we will show below we have dep ⊆ sym and thus also
A = dep|( ,a)7→a ⊆ sym|( ,a)7→a . Thus, if we compute sym
above we get an overapproximation of A.
The fact that dep ⊆ sym can be seen as follows. Let
(a, b) ∈ dep. Then there are a1 , a2 , . . . , an , b such that (a1 , a2 )
∈ dep 1 ∪dep 2 , (a2 , a3 ) ∈ dep 2 , . . . , (an , b) ∈ dep 2 . Let (a′ , a′′ )
be an arbitrary one of those pairs. Then R(a) ∩ W (b) 6= ∅
by the definition of dep 1 and dep 2 . Thus M (a) ∩ M (b) 6= ∅.
As we have already argued above, if two expressions/assignments can access the same memory location then they must
transitively share symbols. Thus (a′ , a′′ ) ∈ sym 1 ∪ sym ∗2
must hold. Therefore, since we have chosen (a′ , a′′ ) arbitrarily, we have that all of the pairs above are contained
in sym 1 ∪ sym ∗2 and thus by the definition of sym and in
particular the transitivity of sym ∗2 we get (a, b) ∈ sym.
Thus, we can use the definition of sym above to compute
an overapproximation of the set of assignments that can affect the starting expressions as defined semantically in the
previous section.

Algorithm.
Algorithm 1 gives our dependency analysis. The first
phase (line 1, Algorithm 2) is based on the ideas from the
previous section and computes the set of assignments A that
can affect the given set of starting expressions exprs . It does
so by keeping a global set of variable identifiers I which is
initialised to the set of variables occuring in the starting expressions. Then the algorithm repeatedly iterates over the
program and checks whether the assignments contain common symbols with I (lines 8–12). If yes, all the symbols in
this assignment are also added to I, and the edge is recorded
in E. This is repeated until a fixpoint is reached (i.e., I has
not changed in an iteration). In addition to assignments,
symbols might also be propagated via functions calls and
thread creation (from arguments to parameters of the function/thread, and from the return expression to the left-hand
side of the call or the argument of the join). This is handled
in lines 13–21.
After we have gathered all affecting assignments, the second phase of the algorithm begins (Algorithm 1, lines 2–
8). This phase additionally identifies the function calls that
might affect the starting expressions. It is based on the
following observation. If a function does not contain any
affecting assignments, and any of the functions it calls do
not either (and those that this function calls in turn do not,
etc.), then the calls to the function cannot affect the starting expressions. The ability to prune function calls has a
potentially big effect on the performance of the analysis, as
it can greatly reduce the amount of code that needs to be
analysed.
In the following section we evaluate the performance and
effectiveness of the dependency analysis. Its effect on the
overall analysis is evaluated in Sec. 7.

Algorithm 1: Dependency analysis
Input : ICFA Prog , lock edges lock edges
Output: Set of affecting edges A
1 A ← affecting edges(Prog , lock edges )
2 F ← {f | e ∈ A ∧ f = func(src(e))}
3 Fh ← ∅
4 while F 6= ∅ do
5
remove f from F
6
Fh ← Fh ∪ {f }
7
E ← {e | func(tgt(e)) = f ∧
op(e) ∈ {func entry, thread entry}}
8
for e ∈ E do
9
A ← A ∪ {e}
10
f ′ ← func(src(e))
11
if f ′ ∈
/ Fh then
12
F ← F ∪ {f ′ }
13

return A

Evaluation.
We have evaluated the dependency analysis on a subset
of 100 benchmarks of the benchmarks given in Sec. 7. For
each benchmark the dependency analysis was invoked with
the set of starting expressions exprs being those occuring in
lock operations or as the first argument of create and join
operations. The results are given in the table below.
runtime
25th percentile
arithmetic mean
75th percentile

0.03 s
0.26 s
0.38 s

sign. assign.

sign. func.

0.3%
40.0%
72.2%

43.3%
63.3%
86.5%

The table shows that the average time (over all benchmarks)
to perform the dependency analysis was 0.26 s. The first and
last line give the 25th and 75th percentile. This indicates for
example that for 25% of the benchmarks it took 0.03 s or less
to perform the dependency analysis. The third and fourth
column evaluate the effectiveness of the analysis. On average, 40% of the assignments in a program were classified
as significant (i.e., potentially affecting the starting expressions). The data also shows that often the number of significant assignments was very low (in 25% of the cases it was
0.3% or less). This happens when the lock usage patterns
in the program are simple, such as using simple lock expressions (like pthread_mutex_lock(&mutex)) that refer to
global locks with simple initialisations (such as using static
initialization via PTHREAD_MUTEX_INITIALIZER).
The average number of functions classified as significant
was 63.3%. This means that on average 36.7% of the functions that occur in a program were identified as irrelevant by
the dependency analysis and thus do not need to be analysed
by the following pointer analysis.
Overall, the data shows that the analysis is cheap and able
to prune a significant number of assignments and functions.

5. NON-CONCURRENCY ANALYSIS
We have implemented an analysis (Algorithm 3) to compute whether two places p1 , p2 are non-concurrent. That is,
the analysis determines whether the statements associated
with the places p1 , p2 (i.e., the operations with which the
outgoing edges of top(p1 ), top(p2 ) are labeled) cannot execute concurrently in the contexts embodied by p1 , p2 .
Whether the places are protected by a common lock is
determined by computing the intersection of the must lock-

Algorithm 2: Affecting edges
function affecting edges(Prog , lock edges )
A ←S
lock edges
3
S ← e∈lock edges symbols(op(e))
4
R←∅
5
for e ∈ E(Prog) do
6
op ← op(e)
7
if op = (a = b) ∨
op = thread entry( , a, b) ∨
op = func exit(a, b) ∨
op = thread join(a, b) then
8
R ← R ∪ {symbols(a) ∪ symbols(b)}
9
else if op = func entry(arg 1 , . . . , arg n ,
par 1 , . . . , par n ) then
10
R ← R ∪ {symbols(arg i ) ∪ symbols(par i ) |
i ∈ {1, . . . , n}}
11
NM ← number map(R)
12
SM ← symbol map(R)
13
Nh , Sh ← ∅, ∅
14
while S 6= ∅ do
15
remove s from S
16
Sh ← Sh ∪ {s}
17
for n ∈ SM [s] do
18
if n ∈
/ Nh then
19
Nh ← Nh ∪ {n}
20
S ← S ∪ (NM [r] − Sh )

Algorithm 3: Non-concurrency analysis

1
2

24

for e ∈ E(Prog) do
if op = (a = b) ∨
op = func exit(a, b) ∨
op = thread join(a, b) then
if ((symbols(a) ∪ symbols(b)) ∩ Sh ) 6= ∅ then
A ← A ∪ {e}

25

return A

21
22

23

sets (lines 3–4). If the intersection is non-empty they cannot
execute concurrently and the algorithm returns true. Otherwise the algorithm proceeds to check whether the places are
non-concurrent due to create and join operations. This is
done via a graph search in the ICFA. First the length of the
longest common prefix of p1 and p2 is determined (line 5).
This is the starting point for the ICFA exploration. If there
is a path from ℓ1 to ℓ2 , it is checked that all the threads that
are created to reach place p1 are joined before location ℓ2
is reached (and same for a path from ℓ2 to ℓ1 ). This check
is performed by the procedure unwind (), the full details of
which we give in Appendix B.
We evaluated the non-concurrency analysis with respect
to what fraction of all the pairs of places p1 , p2 of a program
it classifies as non-concurrent. We found that on a subset
of 100 benchmarks of the benchmarks of Sec. 7, it classified
60% of the places corresponding to different threads as nonconcurrent on average. We give more data in Appendix B.

6.

LOCK GRAPH ANALYSIS

Our lock graph analysis consists of two phases. First, we
build a lock graph based on the lockset analysis. In the
second phase, we prune cycles that are infeasible due to
information from the non-concurrency analysis.

6.1 Lock Graph Construction

1
2
3
4
5
6
7
8
9
10
11
12

Input : places p1 , p2 , must locksets ls 1u , ls 2u
Output: true if p1 , p2 are non-conc., false otherwise
if p1 = p2 then
return true
if ls 1u ∩ ls 2u 6= ∅ then
return true
i ← |common prefix(p1 , p2 )|
r1 , r2 ← true, true
ℓ1 , ℓ2 ← p1 [i], p2 [i]
if has path(ℓ1 , ℓ2 ) then
r1 ← unwind(i, p1 , ℓ1 , ℓ2 )
if has path(ℓ2 , ℓ1 ) then
r2 ← unwind(i, p2 , ℓ2 , ℓ1 )
return r1 ∧ r2
(m:9)

m1

(m:5,t:29)

m2

(m:5,t:30)

(m:10)

m3

m4

(m:5,t:37)

m5

(m:19,f:47)

Figure 9: Lock graph for the program in Fig. 4 (t, m and f
are shorthand for thread, main and func2, respectively).
∗

∗

A lock graph is a directed graph L ∈ 2Objs ×P ×Objs (with
Objs ∗ = Objs ∪ {⋆}). Each node is a lock ∈ Objs ∗ , and
an edge (lock 1 , p, lock 2 ) ∈ Objs ∗ × P × Objs ∗ from lock 1 to
lock 2 is labelled with the place p of the lock operation that
acquired lock 2 while lock 1 was owned by the same thread
get thread(p). Hence, the directed edges indicate the order of
lock acquisition. Fig. 9 gives the lock graph for the example
program in Fig. 4.
We use the result of the may lockset analysis (Sec. 3.5) to
build the lock graph. Fig. 10 gives the lock graph domain
that is instantiated in our analysis framework. For each
lock operation in place p a thread may acquire a lock lock 2
corresponding to the value set of the argument to the lock
operation. This happens while the thread may own any lock
lock 1 in the lockset at that place. Therefore we add an edge
(lock 1 , p, lock 2 ) for each pair (lock 1 , lock 2 ).
Finally, we have to handle the indeterminate locks, denoted by ⋆. We compute the closure cl(L) of the graph
w.r.t. edges that involve ⋆ by adding edges from all predecessors of the ⋆ node to all other nodes, and to each successor
node of the ⋆ node, we add edges from all other nodes.

6.2 Checking Cycles in the Lock Graph
The final step is to check the cycles in the lock graph. For
this purpose we use the information from the non-concurrency
analysis. Each cycle c in the lock graph could be a potential
deadlock. A cycle c is a set of (distinct) edges; there is a
finite number of such sets. A cycle is a potential deadlock if
|c| > 1 ∧ all concurrent(c) where
all concurrent(c) ⇔
∀(lock 1 , p, lock 2 ), (lock ′1 , p′ , lock ′2 ) ∈ c :
¬non concurrent(p, p′ ) ∨
(get thread(p) = get thread(p′ ) ∧
multiple thread(get thread(p)))
and multiple thread(t) means that t was created in a loop or

Domain: 2Objs

∗

×P ×Objs ∗

103

s1 ⊔ s2 = s1 ∪ s2

102

With op(e) = lock(a):
T Je, pK(s) = s ∪ {(lock 1 , p, lock 2 ) | lock 1 ∈ ls a (p),
lock 2 ∈ vs(p, a)}
cl (s) = s ∪{(lock 1 , p, lock ) | (lock 1 , p, ⋆) ∈ s,
lock ∈ get locks(s) \ {lock 1 , ⋆}}
∪{(lock , p, lock 2 ) | (⋆, p, lock 2 ) ∈ s,
lock ∈ get locks(s) \ {lock 2 , ⋆}}

101
100
10−1
10−2
0

1

2

3

4

Figure 10: Lock graph construction

5
·104

(a) LOC vs. user time (timeout 1800 s)

recursion. Due to the use of our non-concurrency analysis
we do not require any special treatment for gate locks or
thread segments as in [3].

107
106

7.

EXPERIMENTS

105

We implemented our deadlock analyser as a pipeline of
static analyses in the CPROVER framework,1 and we performed experiments to support the following hypothesis: Our
analysis handles real-world C code in a precise and efficient way. We used 715 concurrent C programs that contain locks from the Debian GNU/Linux distribution, with
the characteristics shown in Fig. 12.2 The table shows that
the minimum number of different locks and lock operations
encountered by our analysis was 0. We found that this is
due to a small number of benchmarks on which the lock operations were not reachable from the main function of the
program (i.e., they were contained in dead code).
We additionally selected 8 programs and introduced deadlocks in them. This gives us a benchmark set consisting of
723 benchmarks with a total of 7.1 MLOC. Of these, 715
benchmarks are assumed to be deadlock-free, and 8 benchmarks are known to have deadlocks. The experiments were
run on a Xeon X5667 at 3 GHz running Fedora 20 with 64-bit
binaries. Memory and CPU time were restricted to 24 GB
and 1800 seconds per benchmark, respectively.

Results.
We correctly report (potential) deadlocks in the 8 benchmarks with known deadlocks. The results for the deadlockfree programs are shown in the following table grouped by
benchmark size (t/o. . . timed out, m/o. . . out of memory):
KLOC
0–5
5–10
10–15
15–20
20–50

analysed
252
269
86
93
15

proved
130
91
16
23
2

alarms
55
35
9
5
1

t/o
48
108
54
64
11

m/o
19
35
7
1
1

For 105 deadlock-free benchmarks, we report alarms that are
most likely spurious. The main reason for such false alarms
is the imprecision of the pointer analysis with respect to
dynamically allocated data structures. This leads to lock
operations on indeterminate locks (see statistics in Fig. 12).
This is a challenging issue to solve, as we discuss in Sec. 10.
Scatter plots in Figs. 11a and 11b illustrate how the tool
scales in terms of running time and memory consumption
with respect to the number of lines of code. The tool successfully analyzed programs with up to 40K lines of code.
1

Based on r6268 of http://www.cprover.org/svn/cbmc/trunk
2
Lines of code were measured using cloc 1.53.

104
103
0

1

2

3

4

5
·104

(b) LOC vs. memory consumption (memory limit 24 GB)

Figure 11: Experimental results

As the plots show, the asymptotic behaviour of the algorithms in terms of lines of code is difficult to predict since it
mostly depends on the complexity of the pointer analysis.
We evaluated the impact of the different analysis features
on a random selection of 83 benchmarks and break down
the running times into the different analysis phases on those
benchmarks where the tool does not time out or goes out
of memory: We found that the dependency analysis is effective at decreasing both the memory consumption and the
runtime of the pointer analysis. It decreased the memory
consumption by 27% and the runtime by 60% on average.
We observed that still the vast majority of the running time
(93%) of our tool is spent in the pointer analysis, which is
due to the often large number of general memory objects,
including all heap and stack objects that may contain locks.
May lock analysis (3%), must lock analyisis (2%), and lock
graph construction (2%) take less time; the run times for
the dependency analysis and the cycle checking (up to the
first potential deadlock) are negligible. For 80.2% of lock
operations the must lock analysis was precise.

Comparison with other tools.
We tried to find other tools to experimentally compare
with ours. However, we did not find a tool that handles
C code and with which a reasonable comparison could be
made. Other tools are either for Java (such as [29]), are
based solely on testing (Helgrind [1]), or are semi-automatic
lightweight approaches relying on user-supplied annotations
(LockLint [2]).

8. THREATS TO VALIDITY
This section discusses the threats to internal and external
validity of our results and the strategies we have employed
to mitigate them [15].

# lines of code
# Threads
# Threads in loop
# Locks
# Lock operations
Precise must analysis
Size of largest lockset
# indeterminate locking operations
# non-concurrency checks

max
41,749
163
162
16
30773
100%
8.0
2106.0
450.0

avg
8,376.5
3.8
2.1
1.5
331.6
80.2%
1.2
32.3
1.6

min
86
1
0
0
0
0%
1.0
0.0
0.0

Total analysis time (s)
Dependency analysis
Pointer analysis
May lockset analysis
Must lockset analysis
Lock graph construction
Cycles detection
Peak memory (GB)

max
1291.3
5.0
1185.1
345.4
29.9
31.3
327.4
24.0

avg
435.3
0.1
419.0
12.5
1.1
1.2
1.4
6.3

min
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.008

Figure 12: Benchmark characteristics and analysis statistics (for the 367 benchmarks with no time out or out of memory)
The main threat to internal validity concerns the correctness of our implementation. To mitigate this threat we have
continually tested our tool during the implementation phase,
which has resulted in a testsuite of 122 system-, unit-, and
regression-tests. To further test the soundness claim of our
tool on larger programs, we introduced deadlocks into 8 previously deadlock-free programs, and checked that our tool
correctly detected them. While we have reused existing locks
and lock operations to create those deadlocks, they might
nevertheless not correspond well to deadlocks inadvertently
introduced by programmers.
The threats to external validity concern the generalisability of our results to other benchmarks and programming languages. Our benchmarks have been drawn from a collection
of open-source C programs from the Debian GNU/Linux distribution [25] that use pthreads and contain lock operations,
from which we ran most of the smaller ones and some larger
ones. We found that the benchmark set contains a diverse
set of programs. However, we did not evaluate our tool on
embedded (safety- or mission-critical) software, a field that
we see as a prime application area of a sound tool like ours,
due to the ability to verify the absence of errors.
During the experiments we have used a timeout of 1800 s.
This in particular means that we cannot say how the tool
would fare for users willing to invest more time and computing power; in particular, the false positive rate could increase
as programs that take a long time to analyse are likely larger
and could have more potential for deadlocks to occur.
Finally, our results might not generalise to other programming languages. For example, while Naik et al. [29]
(analysing Java) found that the ability to detected common
locks was crucial to lower the false positive rate, we found
that it had little effect in our setting, since most programs
do not acquire more than 2 locks in a nested manner (see
Tab. 12, size of largest lockset).

9.

RELATED WORK

Deadlock analysis is an active research area. Since the
mid-1990s numerous tools, mainly for C and Java, have
been developed. One can distinguish dynamic and static
approaches. A common deficiency is that all these tools are
neither sound nor complete, and produce false positives and
negatives.

Dynamic tools.
The development of the Java PathFinder tool [18, 3] led
to ground-breaking work over more than a decade to find
lock acquisition hierarchy violation with the help of lock
graphs, exposing the issue of gatelocks, and segmentation
techniques to handle different threads running in parallel at
different times. [4, 21, 33] try to predict deadlocks in executions similar to the observed one. DeadlockFuzzer [21]
use a fuzzying technique to search for deadlocking executions. Multicore SDK [27] tries to reduce the size of lock
graphs by clustering locks; and Magiclock [10] implements

significant improvements on the cycle detection algorithms.
Helgrind [1] is a popular open source dynamic deadlock detection tool, and there are many commercial implementations of dynamic deadlock detection algorithms.

Static tools.
There are very few static deadlock analysis tools for C.
LockLint [2] relies on a user-supplied lock acquisition order,
and is thus not fully automatic. RacerX [13] focuses more
on fast analysis of large code bases than soundness. It performs a path- and context-sensitive analysis, but its pointer
analysis is very rudimentary. For Java there is Jlint2 [6],
a tool similar to LockLint. The tool Jade [29] consciously
uses a may analysis instead of a must analysis, which causes
unsoundness. The tools presented in [37] and [35] do not
consider gatelock scenarios, which leads to false alarms.

Other tools.
Some tools combine dynamic approaches and constraint
solving. For example, CheckMate [20] model-checks a path
along an observed execution of a multi-threaded Java program; Sherlock [14] uses concolic testing; and [33, 4] monitor runtime executions of Java programs. There are related
techniques to detect synchronisation defects due to blocking
communication, e.g. in message passing (MPI) programs [17,
11], for the modelling languages BIP (DFinder tool [7, 8])
or ABS (DECO tool [16]) that use similar techniques based
on lock graphs and may-happen-in-parallel information.

Dependency analysis.
Our dependency analysis is related to work on concurrent
program slicing [23, 24, 30] and alias analysis [9, 22]. Our
analysis is more lightweight than existing approaches as it
works on the level of variable identifiers only, as opposed to
more complex objects such as program dependence graphs
(PDG) or representations of possible memory layouts. Moreover, our analysis disregards expressions occuring in control
flow statements (such as if-statements) as these are not relevant to the following pointer analysis which consumes the
result of the dependency analysis. The analysis thus does
not produce an executable subset of the program statements
as in the original definition of slicing by Weiser [36].

Non-concurrency analysis.
Our non-concurrency analysis is context-sensitive, works
on-demand, and can classify places as non-concurrent based
on locksets or create/join. Locksets have been used in a similar way in static data race detection [13], and Havelund [3]
used locksets in dynamic deadlock detection to identify nonconcurrent lock statements. Our handling of create/join is
most closely related to the work of Albert et al. [5]. They
consider a language with asynchronous method calls and an
await statement that allows to wait for the completion of a
previous call. Their analysis works in two phases, the second
of which can be performed on-demand, and also provides a
form of context-sensitivity. Other approaches, which how-

ever do not work on-demand, include the work of Masticola
and Ryder [28] and Naumovich et al. [31] for ADA, and the
work of Lee et al. [26] for async-finish parallelism.

10. CONCLUSIONS
We presented a new static deadlock analysis approach for
concurrent C/pthreads programs. We demonstrated that
our tool can effectively prove deadlock freedom of 2.6 MLOC
concurrent C code from the Debian GNU/Linux distribution. Our experiments show that the pointer analysis is the
crucial component of a static deadlock analyser. It takes
most of the time, by far, and is the primary source for false
alarms when the arguments of lock operations cannot be
determined. In our evaluation, we observed that the limitations of our pointer analysis regarding dynamically allocated
data structures, e.g. when lock objects are stored in lists, are
the key reason for false alarms. Future work will focus on
addressing this limitation. Moreover, we will integrate the
analysis of pthread synchronisation primitives other than
mutexes, e.g. condition variables, and extend our algorithm
to Java synchronisation constructs. We also want to go beyond lock hierarchy violations, and will include the information from a termination analysis to detect loop-related
deadlocks. All this is part of a larger endeavour to show
synchronisation correctness and deadlock freedom of all concurrent C programs that use locks (currently 3748 programs
with 264.5 MLOC) in the Debian GNU/Linux distribution.

11. ACKNOWLEDGMENTS
This work is supported by ERC project 280053 and SRC
task 2269.002.

12. REFERENCES
[1] http://valgrind.org/info/tools.html#helgrind.
[2]
http://developers.sun.com/solaris/articles/locklint.html.
[3] R. Agarwal, S. Bensalem, E. Farchi, K. Havelund,
Y. Nir-Buchbinder, S. D. Stoller, S. Ur, and L. Wang.
Detection of deadlock potentials in multithreaded
programs. IBM Journal of Research and Development,
54(5):3, 2010.
[4] R. Agarwal and S. D. Stoller. Run-time detection of
potential deadlocks for programs with locks,
semaphores, and condition variables. In Workshop on
Parallel and Distributed Systems: Testing, Analysis,
pages 51–60. ACM, 2006.
[5] E. Albert, A. Flores-Montoya, and S. Genaim.
Analysis of may-happen-in-parallel in concurrent
objects. In FMOODS/FORTE, pages 35–51, 2012.
[6] C. Artho and A. Biere. Applying static analysis to
large-scale, multi-threaded Java programs. In
Australian Software Engineering Conference, pages
68–75. IEEE, 2001.
[7] S. Bensalem, M. Bozga, T. Nguyen, and J. Sifakis.
D-Finder: A tool for compositional deadlock detection
and verification. In CAV, volume 5643 of LNCS, pages
614–619. Springer, 2009.
[8] S. Bensalem, A. Griesmayer, A. Legay, T. Nguyen,
and D. Peled. Efficient deadlock detection for
concurrent systems. In Formal Methods and Models
for Codesign, pages 119–129. IEEE, 2011.
[9] M. G. Burke, P. R. Carini, J.-D. Choi, and M. Hind.
Flow-insensitive interprocedural alias analysis in the
presence of pointers. In LCPC, pages 234–250.
Springer, 1995.

[10] Y. Cai and W. K. Chan. Magiclock: Scalable
detection ofpotential deadlocks in large-scale
multithreaded programs. IEEE Trans. Software Eng.,
40(3):266–281, 2014.
[11] Z. Chen, X. Li, J. Chen, H. Zhong, and F. Qin.
SyncChecker: detecting synchronization errors
between MPI applications and libraries. In
International Parallel and Distributed Processing
Symposium, pages 342–353. IEEE, 2012.
[12] P. Cousot and R. Cousot. Abstract interpretation:
A unified lattice model for static analysis of programs
by construction or approximation of fixpoints. In
POPL, pages 238–252, 1977.
[13] D. R. Engler and K. Ashcraft. RacerX: effective, static
detection of race conditions and deadlocks. In
Symposium on Operating Systems Principles, pages
237–252. ACM, 2003.
[14] M. Eslamimehr and J. Palsberg. Sherlock: scalable
deadlock detection for concurrent programs. In
Foundations of Software Engineering, pages 353–365.
ACM, 2014.
[15] R. Feldt and A. Magazinius. Validity threats in
empirical software engineering research – an initial
survey. In SEKE, pages 374–379, 2010.
[16] A. Flores-Montoya, E. Albert, and S. Genaim.
May-happen-in-parallel based deadlock analysis for
concurrent objects. In FMOODS/FORTE, volume
7892 of LNCS, pages 273–288. Springer, 2013.
[17] V. Forejt, D. Kroening, G. Narayanaswamy, and
S. Sharma. Precise predictive analysis for discovering
communication deadlocks in MPI programs. In Formal
Methods, volume 8442 of LNCS, pages 263–278.
Springer, 2014.
[18] K. Havelund. Using runtime analysis to guide model
checking of Java programs. In SPIN, volume 1885 of
LNCS, pages 245–264. Springer, 2000.
[19] T. A. Henzinger, R. Jhala, R. Majumdar, and
G. Sutre. Lazy abstraction. In POPL, 2002.
[20] P. Joshi, M. Naik, K. Sen, and D. Gay. An effective
dynamic analysis for detecting generalized deadlocks.
In Foundations of Software Engineering, pages
327–336. ACM, 2010.
[21] P. Joshi, C. Park, K. Sen, and M. Naik. A randomized
dynamic program analysis technique for detecting real
deadlocks. In PLDI, pages 110–120. ACM, 2009.
[22] V. Kahlon, Y. Yang, S. Sankaranarayanan, and
A. Gupta. Fast and accurate static data-race detection
for concurrent programs. In CAV, pages 226–239.
Springer, 2007.
[23] J. Krinke. Static slicing of threaded programs. In
PASTE, pages 35–42. ACM, 1998.
[24] J. Krinke. Context-sensitive slicing of concurrent
programs. In ESEC/FSE, pages 178–187. ACM, 2003.
[25] D. Kroening and M. Tautschnig. Automating software
analysis at large scale. In MEMICS, pages 30–39, 2014.
[26] J. K. Lee, J. Palsberg, R. Majumdar, and H. Hong.
Efficient may happen in parallel analysis for
async-finish parallelism. In SAS, pages 5–23, 2012.
[27] Z. D. Luo, R. Das, and Y. Qi. Multicore SDK:
A practical and efficient deadlock detector for
real-world applications. In International Conference
on Software Testing, Verification and Validation,
pages 309–318. IEEE, 2011.
[28] S. P. Masticola and B. G. Ryder. Non-concurrency

analysis. In PPoPP, pages 129–138, 1993.
Domain: Di = Fpms × Da
[29] M. Naik, C. Park, K. Sen, and D. Gay. Effective static
deadlock detection. In International Conference on
s1i ⊔i s2i =s1i ⊔s s2i
Software Engineering, pages 386–396. IEEE, 2009.
[30] M. G. Nanda and S. Ramesh. Slicing concurrent
With e = (ℓ1 , ℓ2 ), top(p) = entry loc(ℓ1 ), f = func(ℓ2 ), and
programs. In ISSTA, pages 180–190. ACM, 2000.
n = |p|:
[31] G. Naumovich and G. S. Avrunin. A conservative data
flow algorithm for detecting all pairs of statement that
nexti (e, p) =
may happen in parallel. In FSE, pages 24–34, 1998.

[32] M. C. Rinard. Analysis of multithreaded programs. In
entrys (p, ℓ2 )
op(e) ∈ {thread entry, func entry}



SAS, pages 1–19. Springer, 2001.
p[: n − 2] + entry loc(ℓ2 ) op(e) ∈ {func exit, thread exit,
[33] F. Sorrentino. PickLock: A deadlock prediction

thread join}

approach under nested locking. In SPIN, volume 9232

p[:
n
−
1]
otherwise
of LNCS, pages 179–199. Springer, 2015.
[34] U.S.-Canada Power System Outage Task Force. Final
Ti Jf, pK =
Ti Je, pK
Report on the August 14, 2003 Blackout in the United
e s.t. P (f, e)
States and Canada: Causes and Recommendations,
2004.
http://energy.gov/sites/prod/files/oeprod/DocumentsandMedia/BlackoutFinal-Web.pdf.
Ti Je, pK(si ) = Ts Je, pK(si )
[35] C. von Praun. Detecting Synchronization Defects in
Multi-Threaded Object-Oriented Programs. PhD thesis,
Figure 13: Context-, thread-, and flow-insensitive frame2004.
work
[36] M. Weiser. Program slicing. In ICSE, pages 439–449,
1981.
[37] A. Williams, W. Thies, and M. D. Ernst. Static
APPENDIX
deadlock detection for Java libraries. In European
Conference on Object-Oriented Programming, volume
A. FLOW-INSENSITIVE FRAMEWORK
3586 of LNCS, pages 602–629. Springer, 2005.
In the flow-insensitive framework, the topmost location of
a place always corresponds to the entry point of a function.
That is, we associate a sound overapproximation of the data
flow facts that hold for all locations in the function with the
entry point of the function. Fig. 13 gives the formalization
of the context- and thread-sensitive flow-insensitive framework. It reuses many definitions from the flow-sensitive formalization of Fig. 7.
The result of the flow-insensitive analysis is defined as the
least fixpoint of the following equation:
s = s0 ⊔ λ p.Ti Jfunc(p), pK(s(p)) ⊔c
G
Ti Je, p′ K(s(p′ ))
c

p′ ,e s.t.np(p,p′ ,e)

with np(p, p′ , (ℓ1 , ℓ2 )) = func(ℓ1 ) 6= func(ℓ2 )
entry loc(ℓ1 ) = top(p′ ) ∧
entry loc(ℓ2 ) = top(p) ∧
nexti ((ℓ1 , ℓ2 ), p′ ) = p
with s ⊔ s′ = λ p. s(p) ⊔c s′ (p)

B.

NON-CONCURRENCY ANALYSIS

We describe how the analysis determines whether two
places p1 , p2 are non-concurrent due to the relationship between threads arising from create and join operations.
The analysis is based on performing a graph search in
the ICFA. It makes use of three basic functions on directed
graphs. The function has path(ℓ1 , ℓ2 ) returns true when
there is a path in the ICFA between locations l1 and l2 . The
function on all paths(ℓ1 , ℓ2 , ℓ3 ) returns true when all paths
in the ICFA from ℓ1 to ℓ3 pass through ℓ2 . It is implemented
by computing the set of dominators of ℓ3 (assuming ℓ1 to be
the entry point) and then checking whether ℓ2 is contained

in that set. The function in loop(l) returns true when there
is a path in the ICFA that starts and ends in ℓ.

12
13
14
1

Algorithm.
We explain the algorithm on an example (Fig. 14). The
example consists of four threads (including the main thread).
We want to determine whether the statements x=1 and x=2
are non-concurrent. We see that they cannot run concurrently as main() joins with thread1() before starting thread3()
and thread1() joins with thread2() before returning.
Let us now look at how our algorithm establishes this
fact. The algorithm is called with places p1 = (5, 14, 20) and
p2 = (8, 24). We have no locks in the example and hence
the must locksets are empty (line 3). Line 5 determines the
length of the longest common prefix of p1 and p2 (which is 0
in this case). This is the starting point for the exploration.
The algorithm then checks whether there is a path from 5
to 8 (line 8). If there would not be a path from either 5 to 8
or 8 to 5 this would mean that 5 and 8 occur in conflicting
branches (e.g., one in the then- and the other in the elsebranch of an if statement) and thus the places could not be
concurrent. In the current case there is a path from 5 to 8.
The algorithm then invokes unwind (), which checks that
the threads that are created to reach place p1 are all joined
before location 8 is reached. It does so by iterating over p
starting from the end. The operation top(p) returns the last
element of p, and the operation pop(p) returns p with the
last element removed.
The variable joined indicates whether the last thread that
was created has been joined yet. If the top element of p
corresponds to a create operation (line 10), then if joined is
false the function returns false. If not, then joined is set to
false, and the place corresponding to the create is recorded
in pc . Then, a matching join for the create is searched (line
16) by invoking the find () function.
The function find (pc , p, ℓ1 , ℓ2 ) takes the place pc , a place p,
and locations ℓ1 and ℓ2 . The locations ℓ1 and ℓ2 are in the
same function (let f = func(l1 )), and the place p has as top
element the call to the function f . The function find () looks
for a matching join to the create at place pc . It does so by
looking in the function f (lines 3–6), and (recursively) in the
callees of f (lines 7–14). The join must occur on all paths
between ℓ1 and ℓ2 (lines 5, 9). The call match(pc , p + ℓjoin )
checks that the join at place p + ℓjoin matches the create
at pc (i.e., the thread ID returned by the pthread_create()
is the same as the one passed to the pthread_join()).
If the creation site is in a loop, we additionally ensure that
the thread is joined also on each path that goes back to the
same location (lines 17–20). The final lines 21–31 are like
the loop body and handle the locations ℓ1 and ℓ2 .
For our example, for the first iteration of the while loop in
line 4 we have p = (5, 14, 20). In this case, 20 ∈
/ create locs ∧
joind in line 7 and we thus continue with the next iteration.
Now we have p = (5, 14) and 14 ∈ create locs and thus set
joined to false and record pc = (5, 14). The invocation of
find () (line 16) finds the join in line 16, and thus joined is
set to true. The while loop then terminates as |(5)| ≤ i + 1.
Lines 21–31 then look for a matching join for the create at
location 5. Again such a join is found and unwind () returns
true. The algorithm thus overall returns true.

2
3
4
5
6
7
8
9
10
11

i n t main ( )
{
pthread_t t i d 1 ;
pthread_t t i d 3 ;
pthread_create (
&t i d 1 , 0 , thread1 , 0 ) ;
pthread_join ( tid1 ) ;
pthread_create (
&t i d 3 , 0 , thread3 , 0 ) ;
r e tu r n 0 ;
}

15
16
17
18
19
20
21
22
23
24
25
26

void ∗ t h r e a d 1 ( ) {
pthread_t t i d 2 ;
pthread_create (
&t i d 2 , 0 , thread2 , 0 ) ;
pthread_join ( tid2 , 0 ) ;
r e tu r n 0 ;
}
void ∗ t h r e a d 2 ( ) {
x = 1;
r e tu r n 0 ;
}
void ∗ t h r e a d 3 ( ) {
x = 2;
r e tu r n 0 ;
}

Figure 14: Statements x=1 and x=2 are non-concurrent
Domain: 2Objs ∪ {{⋆}}
s1 ⊔ s2 = s1 ∩ s2
With op(e) =lock(a):
s ∪ vs(p, a)
T Je, pK(s) =
s

if |vs(p, a)| = 1 ∧ vs(p, a) 6= {⋆}
otherwise

With op(e) =unlock(a):
s − vs(p, a)
T Je, pK(s) =
∅

if vs(p, a) 6= {⋆}
otherwise

With op(e) ∈ {thread entry, thread exit, thread join}:
T Je, pK(s) = ∅
Figure 15: Must lockset analysis
threads. We then performed the non-concurrency check for
each of the 1000 pairs. The results are given in the table
below.
runtime
25th percentile
arithmetic mean
75th percentile

0.14s
4.07s
4.56s

n.c. places

n.c. lock places

47%
60%
79%

11%
43%
67%

The table shows that the average time (over all benchmarks)
it took to perform 1000 non-concurrency checks was 4.07s.
The first and last line give the 25th and 75th percentile.
This indicates for example that for 25% of the benchmarks it
took 0.14s or less to perform 1000 non-concurrency checks.
The third and fourth column evaluate the effectiveness of
the non-concurrency analysis. The third column shows that
on average our analysis classified 60% of the place pairs as
non-concurrent. The fourth column gives the same property
while only regarding places that correspond to lock operations. The number of places classified as non-concurrent is
lower in this case, which is expected as the code portions
using locks are those that can run concurrently with others.
Overall, the data shows that the non-concurrency analysis
is both fast and effective.

Evaluation.

C.

We have evaluated the non-concurrency analysis on a subset of 100 benchmarks of the benchmarks described in Sec. 7.
For each benchmark we randomly selected 1000 pairs of
places (p1 , p2 ) such that p1 and p2 correspond to different

Fig. 15 gives a formalisation of the must lockset analysis.
The must locksets can never contain the value ⋆.

D.

MUST LOCKSET ANALYSIS

FRAMEWORK IMPLEMENTATION

Algorithm 4: Find join
function find (pc , p, ℓ1 , ℓ2 )
f ← func(ℓ1 )
3
join locs ← {ℓ ∈ L(f ) | ∃e = (ℓ, ) : is join(op(e))}
4
foreach ℓjoin ∈ join locs do
5
if on all paths(ℓ1 , ℓjoin , ℓ2 ) ∧ match(pc, p + ℓjoin )
then
6
return true
1
2

13
14

entry edges ← {e = (ℓsrc , ℓtgt ) | func(ℓsrc ) =
f ∧ op(e) = func entry}
foreach (ℓsrc , ℓtgt ) ∈ entry edges do
if on all paths(ℓ1 , ℓsrc , ℓ2 ) then
p′ ← p + ℓsrc
f ′ ← func(ℓtgt )
r ← f ind(
pc ,
p′ ,
ℓtgt ,
exit loc(f ′ ))
if r then
return true

15

return false

7

8
9
10
11
12

ℓ1
ℓ2

ℓ3

1

2

0
0

1

2

Figure 16: Trie- and array-based place map data structure,
representing the two way mapping (ℓ1 ) ↔ 1, (ℓ1 , ℓ2 ) ↔ 0,
ℓ3 ↔ 2

Fig. 16 gives an example of a place map which contains
the mappings (ℓ1 ) ↔ 1, (ℓ1 , ℓ2 ) ↔ 0, and (ℓ3 ) ↔ 2. Unlike
in an ordinary trie, in our implementation the nodes also
have pointers to their parent (dashed arrows). This allows
to reconstruct a place from a pointer to a node in the trie.
For example, by starting from the leaf node labeled with 0
we can traverse the parent edges backwards to get the place
(ℓ1 , ℓ2 ).

E.

CORRECTNESS PROOFS

In this section, we show the correctness of our deadlock
analysis approach. We show that the may locksets computed
for each place overapproximate the sets of locks a thread
may hold in a concrete execution at that place. Based on
the correctness of the may locksets, we then show that our
lock graph overapproximates the potential lock allocation
graphs (LAGs). That is, we show that for each execution
prefix of the program for which there exists a cycle in the
LAG, there also is a cycle in the lock graph. We assume the
correctness of the pointer analysis and the correctness of the
non-concurrency analysis.

E.1

Preliminaries

In Sec. 3.3 we have formulated our analyses as a fixpoint

Algorithm 5: Unwind
function unwind (i, p, ℓ1 , ℓ2 )
2
create locs ← {ℓ | ∃e = (ℓ, ) : op(e) = thread entry}
3
joined ← true
4
while |p| > i + 1 do
5
ℓ ← top(p)
6
f ← func(ℓ)
7
if ℓ ∈
/ create locs ∧ joined then
8
p ← pop(p)
9
continue
10
if ℓ ∈ create locs then
11
if ¬joined then
12
return false
13
joined ← f alse
14
pc ← p
15
p ← pop(p)
16
joined ← find (pc , p, ℓ, exit loc(f ))
17
if in loop(ℓ) then
18
loop joined ← find (pc , p, ℓ, ℓ)
19
if ¬joined ∨ ¬loop joined then
20
return false
1

31

if ℓ1 ∈ create locs then
if ¬joined then
return false
joined ← f alse
pc ← p
if ¬joined then
p ← pop(p)
joined ← find (pc , p, ℓ1 , ℓ2 )
if in loop(ℓ1 ) then
loop joined ← find (pc , p, ℓ1 , ℓ1 )
return joined ∧ loop joined

32

return joined

21
22
23
24
25
26
27
28
29
30

computation over the ICFA. An analysis computes data flow
facts for each place (see the fixpoint equation in Sec. 3.3).
The analysis can also be viewed in a slightly different way:
as computing a fixpoint over a larger structure that we
term context-sensitive control-flow automaton (CCFA). The
CCFA for a program is just like the ICFA, but with the
nodes being places rather than locations. Two places p, p′
are connected by an edge if top(p) and top(p′ ) are connected
by an edge in the corresponding ICFA.
We denote a concrete execution (or execution prefix) of
a program as an interleaving E = (p1 , t1 , o1 )(p2 , t2 , o2 ) . . .
(pn , tn , on ). The pi are places, the ti are concrete thread
IDs, and the oi are execution instances of the operations
with which the edges connecting the places pi , pi+1 are labeled. We refer to the individual tuples that make up E
as steps. We use array subscript notation (0-based) to refer to individual elements of lists and tuples. For example,
E[0][2] refers to the third component of the first tuple of
execution E. We further use slice notation to refer to contiguous subsequences of executions. We further use slice
notation (e.g., E[n : m]) for contiguous subsequences of executions (see Sec. 3.2).
We denote an execution path (or an execution path prefix)
of a program as Ep = (p1 , op 1 )(p2 , op 2 ) . . . (pn , op n ). An execution path of a program is a path through its CCFA, starting at the entry point. Here the op i are the operations with
which the edges connecting the places are labeled (rather
than concrete instances of those operations).
Given a thread ID t (resp. abstract thread ID t′ ), we
denote by E|t (resp. Ep |t′ ) the executions (resp. execution
paths) projected to the steps of the given thread t (resp. abstract thread t′ ). We further denote by T (E) = {t | ( , t, ) ∈
E} the set of threads in execution E.3 A thread always
starts with a thread entry operation, thus we have (E|t)[0][2] =
thread entry(. . .) and (Ep |t′ )[0][1] = thread entry(. . .).
′

Property 1. Let E be an execution prefix and let E = E|t
(n = |E ′ |) be the execution of some thread t in E. Then,
there is an execution path prefix Ep (m = |Ep |) with
Ep [m − n : ]|(p, )7→p = E ′ |(p, , )7→p
The property holds by the shape of the CCFA (which directly derives from the shape of the ICFA). The property
states that for each execution E and thread t in E, there is
an execution path prefix Ep such that the sequence of places
visited by t and the sequence of places visited by the suffix
of Ep are the same.
We next define a concretisation function which states how
the result of the pointer analysis (and hence also the static
locksets) are interpreted.
Definition 1. Let A be the set of all locks that may be held
in any execution of a program. Then:

A ls = {⋆}
c(ls) =
ls otherwise
The function satisfies the property c(ls 1 ) ∪ c(ls 2 ) = c(ls 1 ∪
ls 2 ). We are now in a position to prove the correctness of
the may lockset analysis.

E.2

May lockset correctness

If E = (p1 , t1 , o1 ) . . . (pn , tn , on ) is an execution prefix we
denote by ls c (E) the concrete set of locks before executing
the final step (pn , tn , on ). This is the set of locks held by
3
We use the same notation (∈) to denote elements of sets
and lists.

thread tn at that step. A thread starts with an empty set
of locks held.
Theorem E.1. Let Prog be a program and let E = (p1 , t1 , o1 )
. . . (pn , tn , on ) be an execution prefix of Prog. Then:
ls c (E) ⊆ c(ls a (pn )).
Proof. Let t = tn and let E ′ = E|t. By Property 1 there
is an execution path Ep that ends in a sequence Ep′ which
consists of the same sequence of places as E ′ . We write
ls c (i) for the concrete lockset before executing step i of E ′ .
These locksets result from the execution of the program.
We write ls a (i) for the may lockset before handling step i
of Ep′ . These locksets are the result of applying the transfer
function defined in Fig. 8.
We next show by induction that the may locksets computed by our analysis for each step along Ep′ overapproximate the concrete locksets of E ′ at the corresponding steps.
That is, we show that for all 0 ≤ i < |E ′ | : ls c (i) ⊆ c(ls a (i)).
Each thread starts with an empty lockset. In our analysis
this is reflected by the clause (2) in Fig. 8. Hence the base
case ls c (0) = ∅ ⊆ ∅ = c(∅) = c(ls a (0)) holds.
We next show the induction step via a case distinction
based on whether step i is (1) a lock operation or (2) an
unlock operation.
(1) Let ls c (i) ⊆ c(ls a (i)) and let p = E ′ [i][0]. We show that
then also ls c (i + 1) ⊆ c(ls a (i + 1)) after a lock operation
lock(a). We perform a case distinction over the cases of the
definition of T J.K(ls a (i)) (see Fig. 8).
(Case 1) Let l be the concrete lock acquired. By the correctness of the pointer analysis, we have {l} ⊆ c(vs(p, a)).
Therefore:
ls c (i + 1) = ls c (i) ∪ {l} ⊆ c(ls a (i)) ∪ c(vs(p, a)) ⊆ c(ls a (i) ∪
vs(p, a)) = c(ls a (i + 1))
(Case 2) ls c (i + 1) ⊆ A = c({⋆}) holds since A is the set
of all locks.
(2) Let ls c (i) ⊆ c(ls a (i)) and let p = E ′ [i][0]. We show that
then also ls c (i + 1) ⊆ c(ls a (i + 1)) after an unlock operation
unlock(a). We perform a case distinction over the cases of
the definition of T J.K(ls a (i)) (see Fig. 8).
(Case 1) Since |ls a (i)| = 1 and ls a (i) 6= {⋆}, we also
have |ls c (i)| = 1. Therefore, ls c (i + 1) = ∅ ⊆ ∅ = c(∅) =
c(ls a (i + 1)).
(Case 2) Let l be the concrete lock released. Thus we
have l ∈ c(ls a (i)) and l ∈ c(vs(p, a)). Since |ls a (i) ∩
vs(p, a)| = 1 we have that c(ls a (i) ∩ vs(p, a)) = {l}. Thus,
c(ls a (i)−vs(p, a)) = c(ls a (i))−{l}. Therefore, ls c (i+1) =
ls c (i) − {l} ⊆ c(ls a (i)) − {l} = c(ls a (i) − vs(p, a)) =
c(ls a (i + 1)).
(Case 3) ls c (i+1) ⊆ ls c (i) and thus ls c (i+1) ⊆ c(ls a (i)) =
c(ls a (i + 1))
Thus, we have shown that the may lockset is an overapproximation of the concrete lockset at any step along Ep′ ,
and thus in particular also at the final step of Ep′ (i.e., at the
place associated with the final step of Ep′ ). We can now use
the properties of data flow analyses to complete the proof.
First, since the may lockset computed for the final place of
Ep is an overapproximation of the concrete lockset, it follows that the “meet over all paths” (MOP) at this place is an
overapproximation of the concrete locksets for all concrete
executions that might reach that place.

Second, the analysis given in Fig. 8 consists of a finite lattice with top element {⋆}, join function ⊔, and a monotonic
transfer function. Consequently, the minimal fixpoint solution (MFP) of the data flow equations overapproximates the
MOP solution. Therefore, since the MOP solution is sound,
the MFP solution is also sound.

E.3

Lock graph correctness

During a concrete execution of a program, each step of
the execution has an associated lock allocation graph (LAG).
The LAG has two types of nodes: threads and locks. There
is an edge from a lock node to a thread node if the lock is
assigned to that thread (allocation edge). There is an edge
from a thread node to a lock node if the thread has requested
the lock (a request edge). If the LAG at a certain step in
the execution has a cycle, then the involved threads have
deadlocked. Those threads cannot make any more steps (but
other threads might). We thus need to show that whenever
there is an execution that has a cyclic LAG, then our lock
graph also has a cycle c′ for which all concurrent(c′ ) holds.
We first show a lemma about the lock graph closure computation (see Fig. 10) that we will use later on.
Lemma E.2. Let ls 1 , ls 2 , ls 3 , ls 4 be nonempty static locksets, and let p, p′ be places. Let further l ∈ c(ls 2 ) and
l ∈ c(ls 3 ). Let L = {(lock 1 , p′′ , lock 2 ) | (lock 1 ∈ ls 1 ∧ lock 2 ∈
ls 2 ∧ p′′ = p) ∨ (lock 1 ∈ ls 3 ∧ lock 2 ∈ ls 4 ∧ p′′ = p′ )}. Then:
∀lock 1 ∈ ls 1 , lock 2 ∈ ls 4 : ∃lock :
(lock 1 , p, lock ), (lock , p′ , lock 2 ) ∈ cl (L)
Proof.
(1) Assume lock ∈ ls 2 , lock ∈ ls 3 (lock may be ⋆). Then, by
the definition of L above, for all locks lock 1 ∈ ls 1 , lock 2 ∈
ls 4 , (lock 1 , p, lock ), (lock , p′ , lock 2 ) ∈ L ⊆ cl (L).
(2) Assume ls 2 = {⋆}, lock ∈ ls 3 , lock 6= ⋆. Then for all
locks lock 1 ∈ ls 1 , lock 2 ∈ ls 4 , (lock 1 , p, ⋆), (lock , p′ , lock 2 ) ∈
L. Then in cl (L) there is an edge (lock 1 , p, lock ) by the
definition of cl ().
(3) Assume lock ∈ ls 2 , lock 6= ⋆, ls 3 = {⋆}. This case is
symmetric to (2).
We next show a lemma about the definition of all concurrent().
Lemma E.3. Let E be an execution prefix, let G be the
LAG at its final step, and let c be a cycle in G. Let t1 , . . . , tn
be the threads involved in the cycle c, and let (p1 , t1 , o1 ), . . . ,
(pn , tn , on ) be last steps of each thread involved in c in E.
Then for all pi , pj :
¬non concurrent(pi , pj )∨
(get thread(pi ) = get thread(pj ) ∧ multiple thread(pi ))
Proof. Since in E all steps (p1 , t1 , o1 ), . . . , (pn ), tn , on )
could reach a lock operation on which they blocked, they
must have been able to run concurrently in this execution.
Now for two places pi , pj , get thread(pi ) 6= get thread(pj ), it
follows that ¬non concurrent(pi , pj ) by the correctness of the
non-concurrency analysis.
Now assume get thread(pi ) = get thread(pj ). In this case
the places have the same abstract thread ID but they occur
in different concrete threads. This occurs when a thread
create operation occurs in a loop or a recursion (or the
call to the function that invokes the thread creation operation occurs in a loop or recursion, etc.). Then we have
multiple thread(pi ).
We can now show the main theorem stating the soundness
of our lock graph and cycle search.

Theorem E.4. Let Prog be a program and let E = (p1 , t1 , o1 )
. . . (pn , tn , on ) be an execution prefix of Prog. Then if the
LAG at the final step of E has a cycle, then the lock graph
of Prog has a cycle c′ with all concurrent(c′ ).
Proof. Let c denote a cycle in the LAG at the final step
of E. In this cycle, every thread and every lock occurs
exactly once. Let t, t′ be two threads involved in the cycle such that there are edges (l1 , t), (t, l2 ), (l2 , t′ ), (t′ , l3 ), for
locks l1 , l2 , l3 (we might have that l1 = l3 ).
Let n = |(E|t)|, m = |(E|t′ )|, and let (p, t, o) = (E|t)[n −
1], (p′ , t′ , o′ ) = (E|t′ )[m − 1] be the last steps of E|t, E|t′ .
The steps o, o′ are lock operations, i.e., o = lock(exp 1 : l2 ), o′ =
lock(exp 2 : l4 ) with expression exp 1 referring to l2 and expression exp 2 referring to l4 . That is, l2 is the lock requested
by o, and l4 is the lock requested by o′ . Moreover, l1 is in
the lockset ls c at the last step of E|t, and l2 is in the lockset
ls ′c at the last step of E|t′ .
The analysis visits each place at least once, hence the
transfer function (see Fig. 10) is also applied to the edges
outgoing from the places p and p′ . Applying the transfer
function to the lock edge starting at p adds edges from the
elements of ls a (p) to the elements of vs(p, exp 1 ) to the lock
graph L. Applying the transfer function to the lock edge
starting at p′ adds edges from the elements of ls a (p′ ) to the
elements of vs(p′ , exp 2 ) to the lock graph L. By the correctness of the may lockset analysis and the correctness of the
pointer analysis we have l2 ∈ c(vs(p, exp 1 )), l2 ∈ c(ls a (p′ ))).
Therefore, by Lemma E.2, it follows that for all locks lock 1 ∈
ls a (p), lock 2 ∈ vs(p′ , exp 2 ), there is a lock lock such that
(lock 1 , p, lock ), (lock , p′ , lock 2 ) ∈ L.
Thus, in the previous paragraph, we have shown that for
any portion of the cycle c consisting of adjacent threads
t, t′ and edges (l1 , t), (t, l2 ), (l2 , t′ ), (t′ , l3 ), there is a portion
(lock 1 , p, lock ), (lock , p′ , lock 2 ) in the lock graph. Therefore,
the lock graph also has a cycle c′ . The places p, p′ are the
places associated with the final steps of the threads in E
that are involved in the cycle c in the LAG. Hence, by
Lemma E.3, it follows that all concurrent(c′ ).

This figure "locs_mem_deadlock.png" is available in "png" format from:
http://arxiv.org/ps/1607.06927v1

This figure "locs_time_deadlock.png" is available in "png" format from:
http://arxiv.org/ps/1607.06927v1

