arXiv:1802.03950v1 [cs.PL] 12 Feb 2018

Quasi-Optimal Partial Order Reduction
Huyen T.T. Nguyen1 , César Rodrı́guez1, Marcelo Sousa2 ,
Camille Coti1 , and Laure Petrucci1
1

Université Paris 13, Sorbonne Paris Cité, CNRS, France
2
University of Oxford, United Kingdom

Abstract. A dynamic partial order reduction (DPOR) algorithm is optimal when it always explores at most one representative per Mazurkiewicz trace. Existing literature suggests that the reduction obtained by
the non-optimal, state-of-the-art Source-DPOR (SDPOR) algorithm is
comparable to optimal DPOR. We show the first program with O(n)
Mazurkiewicz traces where SDPOR explores O(2n ) redundant schedules
and identify the cause of the blow-up as an NP-hard problem. Our main
contribution is a new approach, called Quasi-Optimal POR, that can
arbitrarily approximate an optimal exploration using a provided constant k. We present an implementation of our method in a new tool
called Dpu using specialised data structures. Experiments with Dpu,
including Debian packages, show that optimality is achieved with low
values of k, outperforming state-of-the-art tools.

1

Introduction

Dynamic partial-order reduction (DPOR) [1,2,3] is a mature approach to mitigate the state explosion problem in stateless model checking of multithreaded
programs. DPORs are based on Mazurkiewicz trace theory [4], a true-concurrency
semantics where the set of executions of the program is partitioned into equivalence classes known as Mazurkiewicz traces (M-traces). In a DPOR, this partitioning is defined by an independence relation over concurrent actions that is
computed dynamically and the method explores executions which are representatives of M-traces. The exploration is sound when it explores all M-traces, and
it is considered optimal [2] when it explores each M-trace only once.
Since two independent actions might have to be explored from the same
state in order to explore all M-traces, a DPOR algorithm uses independence
to compute a provably-sufficient subset of the enabled transitions to explore
for each state encountered. Typically this involves the combination of forward
reasoning (persistent sets [5] or source sets [2,6]) with backward reasoning (sleep
sets [5]) to obtain a more efficient exploration. However, in order to obtain
optimality, a DPOR is forced to compute sequences of transitions (as opposed
to sets of enabled transitions) that avoid visiting a previously visited M-trace.
These sequences are stored in a data structure called wakeup trees in [2] and
known as alternatives in [3].
In this paper, we prove that computing alternatives in an optimal DPOR
is an NP-complete problem. To the best our knowledge this is the first formal

w0
x0 = 7

(a)
w0

w1

w3

1

2

3

x0 = 0 5

w1
x1 = 8
i=0
4

c=1 6

w1

w2

2

3

i=0
4

master
i=c
xi = 0

w1

w2

w3

1

2

3

x0 = 0 5 c = 1 6

c=1
9

i = 1 10
x1 = 0

c=2 7

(b)

count
c=1
c=2

w2
x2 = 9

8
w0

c=2 7

11

c = 2 12

w0

w1

w2

1

2

3

c=1
9

w1

w1

1

2
i=2
15

c = 2 14
15 i = 2
16 x2 = 0

c=1
9

16
x2 = 0

14
c=2

17 w2

w0

w2

1

3

c=1
9

x1 = 0 i = 1 10
11
w1
12
13 c = 2

Fig. 1: (a): Programs; (b): Partially-ordered executions;
complexity result on the difference between non-optimal and optimal DPORs.
The program shown in Fig. 1 (a), which has O(n) M-traces (n is the number
of writer threads) illustrates a practical consequence of this result, as the nonoptimal, state-of-the-art SDPOR algorithm [2] can explore O(2n ) interleavings.
The program contains n := 3 writer threads w0 , w1 , w2 , each writing to a
different variable. The thread count increments n − 1 times a zero-initialized
counter c. Thread master reads c into variable i and writes to xi .
The statements x0 = 7 and x1 = 8 are independent because they produce
the same state regardless of their execution order. Statements i = c and any
statement in the count thread are dependent or interfering: their execution order
results in a different state. Similarly, xi = 0 interferes with exactly one writer
thread, depending on the value of i.
Using this independence relation, the set of executions of this program can
be partitioned into six M-traces, corresponding to the six partial orders shown
in Fig. 1 (b).
Thus, an optimal DPOR explores six executions (2n-executions for n writers). We now show why SDPOR explores O(2n ) in the general case. Conceptually, SDPOR is a loop that (1) runs the program, (2) identifies two dependent
statements that can be swapped, and (3) reverses them and re-executes the
program. It terminates when no more dependent statements can be swapped.
Consider the interference on the counter variable c between the master and
the count thread. Their execution order determines which writer thread interferes with the master statement xi = 0. If c = 1 is executed just before i = c,
then xi = 0 interferes with w1 . However, if i = c is executed before, then xi = 0
interferes with w0 . Since SDPOR does not track relations between dependent
statements, it will naively try to reverse the race between xi = 0 and all writer
threads, which results in exploring O(2n ) executions. In this program, exploring
only six traces requires understanding the entanglement between both interferences as the order in which the first is reversed determines the second.
As a trade-off solution between solving this NP-complete problem and potentially explore an exponential number of redundant schedules, we propose a
hybrid approach called Quasi-Optimal POR (QPOR) which can turn a nonoptimal DPOR into an optimal one. In particular, we provide a polynomial
algorithm to compute alternative executions that can arbitrarily approximate
the optimal solution based on a user specified constant k. The key concept is
a new notion of k-partial alternative, which can intuitively be seen as a “good

enough” alternative: they revert two interfering statements while remembering
the resolution of the last k − 1 interferences.
The major differences between QPOR and the DPORs of [2] are that: 1)
QPOR is based on prime event structures [7], a partial-order semantics that
has been recently applied to programs [3,8], instead of a sequential view to
thread interleaving, and 2) it computes k-partial alternatives with an O(nk )
algorithm while optimal DPOR corresponds to computing ∞-partial alternatives
with an O(2n ) algorithm. For the program shown in Fig. 1 (a), QPOR achieves
optimality with k = 2 because races are coupled with (at most) another race.
As expected, the cost of computing k-partial alternatives and the reductions
obtained by the method increase with higher values of k.
Finding k-partial alternatives requires decision procedures for traversing the
causality and conflict relations in event structures. Our main algorithmic contribution is to represent these relations as a set of trees where events are encoded as
one or two nodes in two different trees. We show that checking causality/conflict
between events amounts to an efficient traversal in one of these trees.
In summary, our main contributions are:
– Proof that computing alternatives for optimal DPOR is NP-complete (Sec. 4).
– Efficient data structures and algorithms for (1) computing k-partial alternatives in polynomial time, and (2) represent and traverse partial orders (Sec. 5).
– Implementation of QPOR in a new tool called Dpu and experimental evaluations against SDPOR in Nidhugg and the testing tool Maple (Sec. 6).
– Benchmarks with O (n) M-traces where SDPOR explores O(2n ) executions
(Sec. 6).
Furthermore, in Sec. 6 we show that: (1) low values of k often achieve optimality; (2) even with non-optimal explorations Dpu greatly outperforms Nidhugg;
(3) Dpu copes with production code in Debian packages and achieves much
higher state space coverage and efficiency than Maple.
Proofs for all our formal results are available in the appendix of the paper.

2

Preliminaries

In this section we provide the formal background used throughout the paper.
Concurrent Programs. We consider deterministic concurrent programs composed
of a fixed number of threads that communicate via shared memory and synchronize using mutexes (Fig. 1 (a) can be trivially modified to satisfy this).
Formally, a concurrent program is a structure P := hM, L, T, m0 , l0 i, where
M is the set of memory states (valuations of program variables, including instruction pointers), L is the set of mutexes, m0 is the initial memory state, l0 is
the initial mutexes state and T is the set of thread statements. A thread statement
t := hi, f i is a pair where i ∈ N is the thread identifier associated with the statement and f : M → (M × Λ) is a partial function that models the transformation
of the memory as well as the effect Λ := {loc} ∪ ({acq, rel} × L) of the statement with respect to thread synchronization. Statements of loc effect model

local thread code. Statements associated with hacq, xi or hrel, xi model lock
and unlock operations on a mutex x. Finally, we assume that (1) functions f are
PTIME-decidable; (2) acq/rel statements do not modify the memory; and (3)
loc statements modify thread-shared memory only within lock/unlock blocks.
When (3) is violated, then P has a datarace (undefined behavior in almost all
languages), and our technique can be used to find such statements, see Sec. 6.
We use labelled transition systems (LT S) semantics for our programs. We
associate a program P with the LT S MP := hS, →, A, s0 i. The set S := M ×
(L → {0, 1}) are the states of MP , i.e., pairs of the form hm, vi where m is the
state of the memory and v indicates when a mutex is locked (1) or unlocked (0).
The actions in A ⊆ N × Λ are pairs hi, bi where i is the identifier of the thread
that executes some statement and b is the effect of the statement. We use the
function p : A → N to retrieve the thread identifier. The transition relation → ⊆
hi,bi
′ ′
S × A × S contains a triple hm, vi −
−−→ hm , v i exactly when there is some
thread statement hi, f i ∈ T such that f (m) = hm′ , bi and either (1) b = loc and
v ′ = v, or (2) b = hacq, xi and v(x) = 0 and v ′ = v|x7→1 , or (3) b = hrel, xi and
v ′ = v|x7→0 . Notation fx7→y denotes a function that behaves like f for all inputs
except for x, where f (x) = y. The initial state is s0 := hm0 , l0 i.
a
′
Furthermore, if s −
→ s is a transition, the action a is enabled at s. Let enabl (s)
denote the set of actions enabled at s. A sequence σ := a1 . . . an ∈ A∗ is a
an
a1
sn . We define
run when there are states s1 , . . . , sn satisfying s0 −
→ s1 . . . −−→
state(σ) := sn . We let runs(MP ) denote the set of all runs and reach(MP ) :=
{state(σ) ∈ S : σ ∈ runs(MP )} the set of all reachable states.
Independence. Dynamic partial-order reduction methods use a notion called
independence to avoid exploring concurrent interleavings that lead to the same
state. We recall the standard notion of independence for actions in [5]. Two
actions a, a′ ∈ A commute at a state s ∈ S iff
a
′
′
′
′
– if a ∈ enabl (s) and s −
→ s , then a ∈ enabl (s) iff a ∈ enabl (s ); and
′
a.a
a′ .a
′
′
– if a, a′ ∈ enabl (s), then there is a state s′ such that s −
−→ s and s −−→ s .
Independence between actions is an under-approximation of commutativity. A
binary relation ♦ ⊆ A×A is an independence on MP if it is symmetric, irreflexive,
and every pair ha, a′ i in ♦ commutes at every state in reach(MP ).
In general MP has multiple independence relations, clearly ∅ is always one
of them. We define relation ♦P ⊆ A × A as the smallest irreflexive, symmetric
relation where hi, bi ♦P hi′ , b′ i holds if i 6= i′ and either b = loc or b = acq x
and b′ 6∈ {acq x, rel x}. By construction ♦P is always an independence.
Labelled Prime Event Structures. Prime event structures (pes) are well-known
non-interleaving, partial-order semantics [9,10,11]. Let X be a set of actions. A
pes over X is a structure E := hE, <, #, hi where E is a set of events, < ⊆ E ×E
is a strict partial order called causality relation, # ⊆ E × E is a symmetric,
irreflexive conflict relation, and h : E → X is a labelling function. Causality
represents the happens-before relation between events, and conflict between two
events expresses that any execution includes at most one of them. Fig. 2 (b)

shows a pes over N × Λ where causality is depicted by arrows, conflicts by
dotted lines, and the labelling h is shown next to the events, e.g., 1 < 5, 8 < 12,
2 # 8, and h(1) = h0, loci. The history of an event e, ⌈e⌉ := {e′ ∈ E : e′ < e},
is the least set of events that need to happen before e.
The notion of concurrent execution in a pes is captured by the concept
of configuration. A configuration is a (partially ordered) execution of the system,
i.e., a set C ⊆ E of events that is causally closed (if e ∈ C, then ⌈e⌉ ⊆ C) and
conflict-free (if e, e′ ∈ C, then ¬(e # e′ )). In Fig. 2 (b), the set {8, 9, 15} is a
configuration, but {3} or {1, 2, 8} are not. We let conf (E) denote the set of all
configurations of E, and [e] := ⌈e⌉ ∪ {e} the local configuration of e. In Fig. 2 (b),
[11] = {1, 8, 9, 10, 11}. A configuration represents a set of interleavings over X.
An interleaving is a sequence in X ∗ that labels any topological sorting of the
events in C. We denote by inter(C) the set of interleavings of C. In Fig. 2 (b),
inter ({1, 8}) = {ab, ba} with a := h0, loci and b := h1, acq mi.
The extensions of C are the events not in C whose histories are included in C:
ex (C) := {e ∈ E : e ∈
/ C ∧ ⌈e⌉ ⊆ C}. The enabled events of C are the extensions
that form a configuration with C, formally: en(C) := {e ∈ ex (C) : C ∪ {e} ∈ conf (E)}.
Finally, the conflicting extensions of C are the extensions that are not enabled:
cex (C) := ex (C) \ en(C). In Fig. 2 (b), ex ({1, 8}) = {2, 9, 15}, en({1, 8}) =
{9, 15}, and cex ({1, 8}) = {2}. See [12] for more information on pes concepts.
Parametric Unfolding Semantics. We recall the program pes semantics of [3,12]
(modulo notation differences). For a program P and any independence ♦ on MP
we define a pes UP,♦ that represents the behavior of P , i.e., such that the interleavings of its set of configurations equals runs(MP ). Fig. 2 shows an example.
Each event in UP,♦ is defined by a canonical name of the form e := ha, Hi,
where a ∈ A is an action of MP and H is a configuration of UP,♦ . Intuitively, e
represents the action a after the history (or the causes) H. In Fig. 2 (b), event 11
is hh0, acq mi, {1, 8, 9, 10}i and event 1 is hh0, loci, ∅i. Note the inductive nature
of the name, and how it allows to uniquely identify each event. We define the
state of a configuration as the one reached by any of its interleavings. Formally,
for C ∈ conf (UP,♦ ) we define state(C) as s0 if C = ∅ and as state(σ) for some
σ ∈ inter (C) if C 6= ∅. Despite its appearance state(C) is well-defined because
all sequences in inter (C) reach the same state, see [12] for a proof.
Definition 1 (Unfolding). Given a program P and some independence relation ♦ on MP := hS, →, A, s0 i, the unfolding of P under ♦, denoted UP,♦ , is
the pes over A constructed by the following fixpoint rules:
1. Start with a pes E := hE, <, #, hi equal to h∅, ∅, ∅, ∅i.
2. Add a new event e := ha, Ci to E for any configuration C ∈ conf (E) and
any action a ∈ A such that a is enabled at state(C) and ¬(a ♦ h(e′ )) holds
for every <-maximal event e′ in C.
3. For any new e in E, update <, #, and h as follows: for every e′ ∈ C, set
e′ < e; for any e′ ∈ E \C, set e′ # e if e 6= e′ and ¬(a ♦ h(e′ )); set h(e) := a.
4. Repeat steps 2 and 3 until no new event can be added to E; return E.

Thread 0:
x := 0
lock(m)
if (y == 0)
unlock(m)
else
lock(m’)
z := 2

Thread 1:
lock(m)
y := 1
unlock(m)

Thread 2:
lock(m’)
z := 3
unlock(m’)

h0, loci 1
h0, acq mi 2
h0, loci 3
h0, rel mi 4
h1, acq mi 5
h1, loci 6

(b)

(a)

h1, rel mi 7

15 h2, acq m′ i

8 h1, acq mi
9 h1, loci
10 h1, rel mi

16 h2, loci

11 h0, acq mi

17 h2, rel m′ i

12 h0, loci
13 h0, acq m′ i

18 h0, acq m′ i

14 h0, loci

19 h0, loci

Fig. 2: (a): a program P ; (b): its unfolding semantics UMP ,♦P .

Step 1 creates an empty pes with only one (empty) configuration. Step 2 inserts
a new event ha, Ci by finding a configuration C that enables an action a which is
dependent with all causality-maximal events in C. In Fig. 2, this initially creates
events 1, 8, and 15. For event 1 := hh0, loci, ∅i, this is because action h0, loci
is enabled at state(∅) = s0 and there is no <-maximal event in ∅ to consider.
Similarly, the state of C1 := {1, 8, 9, 10} enables action a1 := h0, acq mi, and
both h(1) and h(10) are dependent with a1 in ♦P . As a result ha1 , C1 i is an
event (number 11). Furthermore, while a2 := h0, loci is enabled at state(C2 ),
with C2 := {8, 9, 10}, a2 is independent of h(10) and ha2 , C2 i is not an event.
After inserting an event e := ha, Ci, Def. 1 declares all events in C causal
predecessors of e. For any event e′ in E but not in [e] such that h(e′ ) is dependent
with a, the order of execution of e and e′ yields different states. We thus set them
/ [8]
in conflict. In Fig. 2, we set 2 # 8 because h(2) is dependent with h(8) and 2 ∈
and 8 ∈
/ [2].

3

Unfolding-Based DPOR

This section presents an algorithm that exhaustively explores all deadlock states
of a given program (a deadlock is a state where no thread is enabled).
For the rest of the paper, unless otherwise stated, we let P be a terminating
program (i.e., runs(MP ) is a finite set of finite sequences) and ♦ an independence
on MP . Consequently, UP,♦ has finitely many events and configurations.
Our POR algorithm (Alg. 1) analyzes P by exploring the configurations
of UP,♦ . It visits all ⊆-maximal configurations of UP,♦ , which correspond to the
deadlock states in reach(MP ), and organizes the exploration as a binary tree.
Explore(C, D, A) has a global set U that stores all events of UP,♦ discovered
so far. The three arguments are: C, the configuration to be explored; D (for
disabled ), a set of events that shall never be visited (included in C) again; and
A (for add ), used to direct the exploration towards a configuration that conflicts
with D. A call to Explore(C, D, A) visits all maximal configurations of UP,♦
which contain C and do not contain D, and the first one explored contains C ∪A.

Algorithm 1: Unfolding-based POR exploration. See text for definitions.
1
2
3
4
5
6
7
8
9
10
11
12
13

Initially, set U := ∅,
and call Explore(∅, ∅, ∅).

14

Procedure Explore(C, D, A)
Add ex (C) to U
if en(C) ⊆ D return
if A = ∅
Choose e from en(C) \ D
else
Choose e from A ∩ en(C)
Explore(C ∪ {e}, D, A \ {e})
if ∃J ∈ Alt(C, D ∪ {e})
Explore(C, D ∪ {e}, J \ C)
U := U ∩ QC,D

16

15
17
18
19
20
21
22
23
24
25

Function cexp(C )
R := ∅
foreach event e ∈ C of type acq
et := pt(e)
em := pm(e)
while ¬(em ≤ et ) do
em := pm(em )
if (em < et ) break
em := pm(em )
ê := hh(e), [et ] ∪ [em ]i
Add ê to R
return R

The algorithm first adds ex (C) to U . If C is a maximal configuration (i.e.,
there is no enabled event) then line 5 returns. If C is not maximal but en(C) ⊆ D,
then all possible events that could be added to C have already been explored
and this call was redundant work. In this case the algorithm also returns and
we say that it has explored a sleep-set blocked (SSB) execution [2]. Alg. 1 next
selects an event enabled at C, if possible from A (line 7 and 9) and makes a
recursive call (left subtree) that explores all configurations that contain all events
in C ∪ {e} and no event from D. Since that call visits all maximal configurations
containing C and e, it remains to visit those containing C but not e. At line 11
we determine if any such configuration exists. Function Alt returns a set of
configurations, so-called clues. A clue is a witness that a ⊆-maximal configuration
exists in UP,♦ which contains C and not D ∪ {e}.
Definition 2 (Clue). Let D and U be sets of events, and C a configuration
such that C ∩ D = ∅. A clue to D after C in U is a configuration J ⊆ U such
that C ∪ J is a configuration and D ∩ J = ∅.
Definition 3 (Alt function). Function Alt denotes any function such that
Alt(B, F ) returns a set of clues to F after B in U , and the set is non-empty if
UM,♦ has at least one maximal configuration C where B ⊆ C and C ∩ F = ∅.
When Alt returns a clue J, the clue is passed in the second recursive call
(line 12) to “mark the way” (using set A) in the subsequent recursive calls at
line 10, and guide the exploration towards the maximal configuration that J
witnesses. Def. 3 does not define a concrete implementation of Alt. It rather
indicates how to implement Alt so that Alg. 1 terminates and is complete (see
below). Different PORs in the literature can be reframed in terms of Alg. 1.
SDPOR [2] uses clues that mark the way with only one event ahead (|J \ C| = 1)
and can hit SSBs. Optimal DPORs [2,3] use size-varying clues that guide the
exploration provably guaranteeing that any SSB will be avoided.

Alg. 1 is optimal when it does not explore a SSB. To make Alg. 1 optimal Alt
needs to return clues that are alternatives [3], which satisfy stronger constraints.
When that happens, Alg. 1 is equivalent to the DPOR in [3] and becomes optimal
(see [12] for a proof).
Definition 4 (Alternative [3]). Let D and U be sets of events and C a configuration such that C ∩ D = ∅. An alternative to D after C in U is a clue J
to D after C in U such that ∀e ∈ D : ∃e′ ∈ J, e # e′ .
Line 13 removes from U events that will not be necessary for Alt to find
clues in the future. The events preserved, QC,D := C ∪ D ∪ #(C ∪ D), include all
events in C ∪ D as well as every event in U that is in conflict with some event
in C ∪ D. The preserved events will suffice to compute alternatives [3], but other
non-optimal implementations of Alt could allow for more aggressive pruning.
The ⊆-maximal configurations of Fig. 2 (b) are [7] ∪ [17], [14], and [19].
Our algorithm starts at configuration C = ∅. After 10 recursive calls it visits
C = [7]∪[17]. Then it backtracks to C = {1}, calls Alt({1}, {2}), which provides,
e.g., J = {1, 8}, and visits C = {1, 8} with D = {2}. After 6 more recursive calls
it visits C = [14], backtracks to C = [12], calls Alt([12], {2, 13}), which provides,
e.g., J = {15}, and after two more recursive calls it visits C = [12] ∪ {15}
with D = {2, 13}. Finally, after 4 more recursive calls it visits C = [19].
Finally, we focus on the correctness of Alg. 1, and prove termination and
soundness of the algorithm:
Theorem 1 (Termination). Regardless of its input, Alg. 1 always stops.
Theorem 2 (Completeness). Let Ĉ be a ⊆-maximal configuration of UP,♦ .
Then Alg. 1 calls Explore(C, D, A) at least once with C = Ĉ.

4

Complexity

This section presents complexity results about only two non-trival steps in Alg. 1:
computing ex (C) and the call to Alt(·, ·). An implementation of Alt(B, F )
that systematically returns B would satisfy Def. 4, but would also render Alg. 1
unusable (equivalent to a DFS in MP ). On the other hand the algorithm becomes
optimal when Alt returns alternatives. Optimality comes at a cost:
Theorem 3. Given a finite pes E, some configuration C ∈ conf (E), and a
set D ⊆ ex (C), deciding if an alternative to D after C exists in E is NP-complete.
Theorem 3 assumes that E is an arbitrary pes. Assuming that E is the unfolding of a program P under ♦P does not reduce this complexity:
Theorem 4. Let P be a program and U a causally-closed set of events from
UP,♦P . For any configuration C ⊆ U and any D ⊆ ex (C), deciding if an alternative to D after C exists in U is NP-complete.

These complexity results lead us to consider (in next section) new approaches
that avoid the NP-hardness of computing alternatives while still retaining their
capacity to prune the search.
Finally, we focus on the complexity of computing ex (C), which essentially
reduces to computing cex (C), as computing en(C) is trivial. Assuming that E is
given, computing cex (C) for some C ∈ conf (E) is a linear problem. However, for
any realistic implementation of Alg. 1, E is not available, the very goal of Alg. 1
is to find all of its events. So a useful complexity result about cex (C) necessarily
refers to the orignal system under analysis. When E is the unfolding of a Petri
net [13] (see App. A for a formal definition), computing cex (C) is NP-complete:
Theorem 5. Let N be a Petri net, t a transition of N , E the unfolding of N
and C a configuration of E. Deciding if h−1 (t) ∩ cex (C) = ∅ is NP-complete.
Fortunately, computing cex (C) for programs is a much simpler task. Function
cexp(C), shown in Alg. 1, computes and returns cex (C) when E is the unfolding
of some program. We explain cexp(C) in detail in Sec. 5.3. But assuming that
functions pt and pm can be computed in constant time, and relation < decided
in O(log |C|), as we will show, clearly cexp works in time O(n2 log n), where
n := |C|, as both loops are bounded by the size of C.

5

New Algorithm for Computing Alternatives

This section introduces a new class of clues, called k-partial alternatives. These
can arbitrarily reduce the number of redundant explorations (SSBs) performed
by Alg. 1 and can be computed in polynomial time. Specialized data structures
and algorithms for k-partial alternatives are also presented.
Definition 5 (k-partial alternative). Let U be a set of events, C ⊆ U a
configuration, D ⊆ U a set of events, and k ∈ N a number. A configuration J is
a k-partial alternative to D after C if there is some D̂ ⊆ D such that |D̂| = k
and J is an alternative to D̂ after C.
A k-partial alternative needs to conflict with only k (instead of all) events
in D. An alternative is thus an ∞-partial alternative. If we reframe SDPOR in
terms of Alg. 1, it becomes an algorithm using singleton 1-partial alternatives.
While k-partial alternatives are a very simple concept, most of their simplicity
stems from the fact that they are expressed within the elegant framework of pes
semantics. Defining the same concept on top of sequential semantics (often used
in the POR literature [5,1,14,2,15,16]), would have required much more complex
device.
We compute k-partial alternatives using a comb data structure:
Definition 6 (Comb). Let A be a set. An A-comb c of size n ∈ N is an
ordered collection of spikes hs1 , . . . , sn i, where each spike si ∈ A∗ is a sequence
of elements over A. Furthermore, a combination over c is any tuple ha1 , . . . , an i
where ai ∈ si is an element of the spike.

It is possible to compute k-partial alternatives (and by extension optimal
alternatives) to D after C in U using a comb, as follows:
1. Select k (or |D|, whichever is smaller) arbitrary events e1 , . . . , ek from D.
2. Build a U -comb hs1 , . . . , sk i of size k, where spike si contains all events in
U in conflict with ei .
3. Remove from si any event ê such that either [ê] ∪ C is not a configuration
or [ê] ∩ D 6= ∅.
4. Find combinations he′1 , . . . , e′k i in the comb satisfying ¬(e′i # e′j ) for i 6= j.
5. For any such combination the set J := [e′1 ]∪. . .∪[e′k ] is a k-partial alternative.
Step 3 guarantees that J is a clue. Steps 1 and 2 guarantee that it will
conflict with at least k events from D, hence it will be a k-partial alternative.
It is straightforward to prove that the procedure above will find a k-partial
alternative to D after C in U iff one exists.
Steps 2, 3, and 4 require to decide whether a given pair of events is in conflict.
Similarly, step 3 requires to decide if two events are causally related. Efficiently
computing k-partial alternatives thus reduces to efficiently computing causality
and conflict between events.
5.1

Computing Causality and Conflict for PES events

In this section we introduce an efficient data structure for deciding whether two
events in the unfolding of a program are causally related or in conflict.
As in Sec. 3, let P be a program, MP its LTS semantics, and ♦P its independence relation (defined in Sec. 2). Additionally, let E denote the pes UMP ,♦P
of P extended with a new event ⊥ that causally precedes every event in UMP ,♦P .
The unfolding E represents the dependency of actions in MP through the
causality and conflict relations between events. By definition of ♦P we know
that for any two events e, e′ ∈ E:
– If e and e′ are events from the same thread, then they are either causally
related or in conflict.
– If e and e′ are lock/unlock operations on the same variable, then similarly
they are either causally related or in conflict.
This means that the causality/conflict relations between all events of one
thread can be tracked using a tree. For every thread of the program we define
and maintain a so-called thread tree. Each event of the thread has a corresponding
node in the tree. A tree node n is the parent of another tree node n′ iff the event
associated with n is the immediate causal predecessor of the event associated
with n′ . That is, the ancestor relation of the tree encodes the causality relations
of events in the thread, and the branching of the tree represents conflict. Given
two events e, e′ of the same thread we have that e < e′ iff ¬(e # e′ ) iff the tree
node of e is an ancestor of the tree node of e′ .
We apply the same idea to track causality/conflict between acq and rel
events. For every lock l ∈ L we maintain a separate lock tree, containing a
node for each event labelled by either hacq, li or hrel, li. As before, the ancestor

relation in a lock tree encodes the causality relations of all events represented in
that tree. Events of type acq/rel have tree nodes in both their lock and thread
trees. Events for loc actions are associated to only one node in the thread tree.
This idea gives a procedure to decide a causality/conflict query for two events
when they belong to the same thread or modify the same lock. But we still need
to decide causality and conflict for other events, e.g., loc events of different
threads. Again by construction of ♦P , the only source of conflict/causality for
events are the causality/conflict relations between the causal predecessors of the
two. These relations can be summarized by keeping two mappings for each event:
Definition 7. Let e ∈ E be an event of E. We define the thread mapping
tmax : E × N → E as the only function that maps every pair he, ii to the unique
<-maximal event from thread i in [e], or ⊥ if [e] contains no event from thread i.
Similarly, the lock mapping lmax : E × L → E maps every pair he, li to the
unique <-maximal event e′ ∈ [e] such that h(e′ ) is an action of the form hacq, li
or hrel, li, or ⊥ if no such event exists in [e].
The information stored by the thread and lock mappings enables us to decide
causality and conflict queries for arbitrary pairs of events:
Theorem 6. Let e, e′ ∈ E be two arbitrary events from resp. threads i and i′ ,
with i 6= i′ . Then e < e′ holds iff e 6 tmax (e′ , i). And e # e′ holds iff there is
some l ∈ L such that lmax (e, l) # lmax (e′ , l).
As a consequence of Theorem 6, deciding whether two events are related by
causality or conflict reduces to deciding whether two nodes from the same lock
or thread tree are ancestors.
5.2

Computing Causality and Conflict for Tree Nodes

This section presents an efficient algorithm to decide if two nodes of a tree are
ancestors. The algorithm is similar to a search in a skip list [17].
Let hN, ⋖, ri denote a tree, where N is a set of nodes, ⋖ ⊆ N × N is the
parent relation, and r ∈ N is the root. Let d(n) be the depth of each node in
the tree, with d(r) = 0. A node n is an ancestor of n′ if it belongs to the only
path from r to n′ . Finally, for a node n ∈ N and some integer g ∈ N such that
g ≤ d(n) let q(n, g) denote the unique ancestor n′ of n such that d(n′ ) = g.
Given two distinct nodes n, n′ ∈ N , we need to efficiently decide whether n is
an ancestor of n′ . The key idea is that if d(n) = d(n′ ), then the answer is clearly
negative; and if the depths are different and w.l.o.g. d(n) < d(n′ ), then we have
that n is an ancestor of n′ iff nodes n and n′′ := q(n′ , d(n)) are the same node.
To find n′′ from n′ , a linear traversal of the branch starting from n′ would
be expensive for deep trees. Instead, we propose to use a data structure similar
to a skip list. Each node stores a pointer to the parent node and also a number
of pointers to ancestor nodes at distances s1 , s2 , s3 , . . ., where s ∈ N is a userdefined step. The number of pointers stored at a node n is equal to the number of
trailing zeros in the s-ary representation of d(n). For instance, for s := 2 a node

at depth 4 stores 2 pointers (apart from the pointer to the parent) pointing to
the nodes at depth 4 − s1 = 2 and depth 4 − s2 = 0. Similarly a node at depth 12
stores a pointer to the ancestor (at depth 11) and pointers to the ancestors at
depths 10 and 8. With this algorithm computing q(n, g) requires traversing
log(d(n) − g) nodes of the tree.
5.3

Computing Conflicting Extensions

We now explain how function cexp(C) in Alg. 1 works. A call to cexp(C)
constructs and returns all events in cex (C). The function works only when the
pes being explored is the unfolding of a program P under the independence ♦P .
Owing to the properties of UP,♦P , all events in cex (C) are labelled by acq
actions. Broadly speaking, this is because only the actions from different threads
that are co-enabled and are dependent create conflicts in UP,♦P . And this is
only possible for acq statements. For the same reason, an event labelled by
a := hi, hacq, lii exists in cex (C) iff there is some event e ∈ C such that h(e) = a.
Function cexp exploits these facts and the lock tree introduced in Sec. 5.1
to compute cex (C). Intuitively, it finds every event e labelled by an hacq, li
statement and tries to “execute” it before the hrel, li that happened before e
(if there is one). If it can, it creates a new event ê with the same label as e.
Function pt(e) returns the only immediate causal predecessor of event e in
its own thread. For an acq/rel event e, function pm(e) returns the parent node
of event e in its lock tree (or ⊥ if e is the root). So for an acq event it returns
a rel event, and for a rel event it returns an acq event.

6

Experimental Evaluation

We implemented QPOR in a new tool called Dpu 3 (Dynamic Program Unfolder ). Dpu is a stateless model checker for multithreaded C programs using
POSIX threads. It uses the Clang compiler as the language front-end and the
LLVM infrastructure to instrument and JIT-compile the program. We natively
execute the instrumented program under a runtime that captures and controls
the calls to any pthread_* function. The input program is assumed to be datadeterministic (i.e., concurrency is the only source of non-determinism). It implements k-partial alternatives (k is an input), optimal POR, and context-switch
bounding [18].
DPU does not use data-races as a source of thread interference for POR. It
will not explore two execution orders for the two instructions that exhibit a datarace. However, it can be instructed to detect and report data races found during
the POR exploration. If requested, DPU will record all memory load/store operations in a compressed manner and use the tree-based data structures of Sec. 5.1
to find data-races. When requested, this detection happens for a user-provided
percentage of the executions explored by POR.
3

We make statically linked binaries, source code, and benchmarks available at:
https://www.dropbox.com/s/4i36q3n4zbeawqp/dpu-x86_64-v0.5.1.tar.gz.

Benchmark
Name

Dpu (k=1)
Th

Confs Time

Disp(5,2)
Disp(5,3)
Disp(5,4)
Disp(5,5)
Disp(5,6)

8
9
10
11
12

137
2K
15K
151K
?

0.8
1K
5.4
11K
58.5 105K
TO
TO
-

Mpat(4)
Mpat(5)
Mpat(6)
Mpat(7)
Mpat(8)

9
11
13
15
17

384
4K
46K
645K
?

0.5
2.4
50.6
TO
TO

0
0
0
-

MPC(2,5)
MPC(3,5)
MPC(4,5)
MPC(5,5)

8
9
10
11

60
3K
314K
?

0.6
26.5
TO
TO

6
7
8
9

120
720
5K
40K

0.4
0.7
3.5
48.1

14
15
16
17
18
19

3K
4K
5K
7K
10K
12K

Pi(5)
Pi(6)
Pi(7)
Pi(8)
Pol(7,3)
Pol(8,3)
Pol(9,3)
Pol(10,3)
Pol(11,3)
Pol(12,3)

Dpu (k=2)

SSB Time
0.4
1.3
16.4
476
TO

Dpu (k=3)

Dpu (optimal)

SSB Time SSB Time Mem

Nidhugg
Mem

SSB

0
1
213
2K
-

0.4
1.0
10.3
257
TO

37
37
87
729
1131

1.2
10.8
109
TO
TO

33
33
33
33
33

2K
13K
115K
-

-

N/A
N/A
N/A
TO
TO

-

0.5
2.7
73.2
TO
TO

37
37
214
660
689

0.6
1.8
21.5
359
TO

33
33
33
33
33

0
0
0
0
-

0
3K
-

1.7
391
TO

0
30K
-

0.4
1.7
296
TO

38
38
239
834

2.0
70.7
TO
TO

34
34
33
34

3K
90K
-

0.5
0.7
4.0
42.9

39
39
45
246

19.6
123
TO
TO

35
35
34
34

0
0
-

1.9
3.0
4.8
7.1
10.6
16.4

39
52
73
99
138
184

74.1
251
TO
TO
TO
TO

33
33
33
33
33
33

90K
274K
-

43
595
6K
53K
-

0.4
1.0
10.3
280
TO

N/A
N/A
N/A
TO
TO

560
50K
-

0.4
3.0
TO
TO

0
0
0
0

N/A
N/A
N/A
N/A

N/A
N/A
N/A
N/A

48.5
72K
153 214K
464 592K
TO
TO
TO
-

2.9
5.5
9.5
17.2
27.2
46.3

1K
1.9
3K
3.0
5K
4.8
9K
6.8
12K
9.7
20K 13.5

6
10
15
21
28
36

Time

Table 1: Comparing QPOR and SDPOR. Machine: Linux, Intel Xeon 2.4GHz. TO:
timeout after 8 min. Columns are: Th: nr. of threads; Confs: maximal configurations;
Time in seconds, Memory in MB; SSB: Sleep-set blocked executions. N/A: analysis
with lower k yielded 0 SSBs.
6.1

Comparison to SDPOR

In this section we investigate the following experimental questions: (a) How
does QPOR compare against SDPOR? (b) For which values of k do k-partial
alternatives yield optimal exploration?
We use realistic programs that expose complex thread synchronization patterns including a job dispatcher, a multiple-producer multiple-consumer scheme,
parallel computation of π, and a thread pool. Complex synchronizations patterns
are frequent in these examples, including nested and intertwined critical sections
or conditional interactions between threads based on the processed data, and
provide means to highlight the differences between POR approaches and drive
improvement. Each program contains between 2 and 8 assertions, often ensuring
invariants of the used data structures. All programs are safe and have between 90
and 200 lines of code. We also considered the SV-COMP’17 benchmarks, but almost all of them contain very simple synchronization patterns, not representative
of more complex concurrent algorithms. App. G provides the experimental data
of this comparison. On these benchmarks QPOR and SDPOR perform an almost
identical exploration, both timeout on exactly the same instances, and both find
exactly the same bugs.
In Table 1, we present a comparison between Dpu and Nidhugg [15], an
efficient implementation of SDPOR for multithreaded C programs. We run kpartial alternatives with k ∈ {1, 2, 3} and optimal alternatives. The number of

SSB executions dramatically decreases as k increases. With k = 3 almost no
instance produces SSBs (except MPC(4,5)) and optimality is achieved with
k = 4. Programs with simple synchronization patterns, e.g., the Pi benchmark,
are explored optimally both with k = 1 and by SDPOR, while more complex
synchronization patterns require k > 1.
Overall, if the benchmark exhibits many SSBs, the run time reduces as k increases, and optimal exploration is the fastest option. However, when the benchmark contains few SSBs (cf., Mpat, Pi, Poke), k-partial alternatives can be
slightly faster than optimal POR, an observation inline with previous literature [2]. Code profiling revealed that when the comb is large and contains many
solutions, both optimal and non-optimal POR will easily find them, but optimal POR spends additional time constructing a larger comb. This suggests that
optimal POR would profit from a lazy comb construction algorithm.
Dpu is faster than Nidhugg in the majority of the benchmarks because it
can greatly reduce the number of SSBs. In the cases where both tools explore
the same set of executions, Dpu is in general faster than Nidhugg because
it JIT-compiles the program, while Nidhugg interprets it. All the benchmark
in Table 1 are data-race free, but Nidhugg cannot be instructed to ignore dataraces and will attempt to revert them. Dpu was run with data-race detection
disabled. Enabling it will incur in approximatively 10% overhead. In contrast
with previous observations [2,15], the results in Table 1 show that SSBs can
dramatically slow down the execution of SDPOR.
6.2

Evaluation of the Tree-based Algorithms

We now evaluate the efficiency of our tree-based algorithms from Sec. 5 answering: (a) What are the average/maximal depths of the thread/lock sequential
trees? (b) What is the average depth difference on causality/conflict queries? (c)
What is the best step for branch skip lists?
We ran Dpu with an optimal exploration over a selection of 15 programs
from Table 1, whose unfoldings size range from 380 to 204K maximal configurations. In total, the 15 unfoldings contain 246 trees (150 thread trees and 96 lock
trees) with 5.2M nodes. Fig. 3 displays the average depth of the nodes in each
tree (subfigure a) and the maximum depth of the trees (subfigure b), for each of
the 246 trees.
While the average depth of a node is 22.7, as much as 80% of the trees have a
maximum depth of less than 8 nodes, and 90% of them less than 16 nodes. The
average of 22.7 is however larger because deeper trees contain proportionally
more nodes. The depth of the deepest node of every tree was between 3 and 77.
We next evaluate depth differences in the causality and conflict queries over
these trees. Sec. 6.2 and Sec. 6.2 respectively show the frequency of various depth
distances associated to causality and conflict queries made by optimal POR.
Surprisingly, depth differences are very small for both causality and conflict
queries. When deciding causality between events, as much as 92% of the queries
were for tree nodes separated by a distance between 1 and 4, and 70% had a
difference of 1 or 2 nodes. This means that optimal POR, and specifically the

Locks
Threads

Depth

Depth

70
60
50
40
30
20
10
0
0

20

40

60

80 100 120 140 160
Tree

(a) Average depth of the tree nodes

(c) Depth-distance frequency on causality
queries

80
70
60
50
40
30
20
10
0

Locks
Threads

0

20

40

60

80 100 120 140 160
Tree

(b) Maximum depth of the trees

(d) Depth-distance frequency on conflict
queries

Fig. 3: (a), (b): depths of trees; (c), (d): frequency of depth distances
procedure that adds ex (C) to the unfolding (which is the main source of causality
queries), systematically performs causality queries which are trivial with the
proposed data structures. The situation is similar for checking conflicts: 82% of
the queries are about tree nodes whose depth difference is between 1 and 4.
These experiments show that most queries on the causality trees require very
short walks, which strongly drives to use the data structure proposed in Sec. 5.
Finally, we chose a (rather arbitrary) skip step of 4. We observed that other
values do not significantly impact the run time/memory consumption for most
benchmarks, since the depth difference on causality/conflict requests is very low.
6.3

Evaluation Against the State-of-the-art on System Code

We now evaluate the scalability and applicability of Dpu on five multithreaded
programs in two Debian packages: blktrace [19], a block layer I/O tracing mechanism, and mafft [20], a tool for multiple alignment of amino acid or nucleotide
sequences. The code size of these utilities ranges from 2K to 40K LOC, and mafft
is parametric in the number of threads.
We compared Dpu against Maple [21], a state-of-the-art testing tool for
multithreaded programs, as the top ranked verification tools from SVCOMP’17
are still unable to cope with such large and complex multithreaded code. Unfortunately we could not compare against Nidhugg because the tool could not
deal with the (abundant) calls to the library in these programs.
Table 2 presents our experimental results. We ran Dpu with optimal exploration and executed the modified version of Maple used in [22]. In order to
test the effectiveness of the approaches in state space coverage and bug finding, we introduced bugs in 4 of the benchmarks (Add,Dnd,Mdl,pla). For the
safe benchmark Blk, we performed an exhaustive state space exploration using
Maple’s DFS mode. On this benchmark, Dpu outperformed Maple by several

orders of magnitude: Dpu explored up to 20K executions covering the entire
state space in 10s while Maple only explored up to 108 executions in 8 min.
For the remaining benchmarks, we used the random sched- Benchmark
Dpu
Maple
uler of Maple, considered to be Name
LOC Th Time Execs R Time Execs R
the best baseline for bug find- Add(3)
40K 3
24.3
2 U
2.7
2 S
40K 5
25.5
24 U 34.5
24 U
ing [22]. First, we ran Dpu to Add(5)
Add(7)
40K 7
48.1
720 U
TO
316 U
retrieve a bound on the number Add(9)
40K 9
TO
14K U
TO
329 U
Add(11)
40K 11
TO
14K U
TO
295 U
of random executions to answer
2K 2
0.9
1 S
4.6
1 S
whether both tools are able to Blk(5)
Blk(15)
2K 2
0.9
5 S 23.3
5 S
2K 2
1.0
180 S
TO
105 S
find the bug within the same num- Blk(18)
Blk(20)
2K 2
1.5 1147 S
TO
106 S
2K 2
2.6 5424 S
TO
108 S
ber of executions. Maple found Blk(22)
Blk(24)
2K 2
10.0
20K S
TO
105 S
bugs in all buggy programs (exDnd(2,4) 16K 3
11.1
80 U
122
80 U
cept for one variant in Add) even Dnd(4,2) 16K 5 11.8
96 S
151
96 S
Dnd(4,4) 16K 5
TO
13K U
TO
360 U
though Dpu greatly outperforms Dnd(6,2) 16K 7 149.3 4320 S
TO
388 S
and is able to achieve much more Mdl(1,4) 38K 7 26.1
1 U
1.4
1 U
Mdl(2,2) 38K 5
29.2
9 U 13.3
9 U
state space coverage.
6.4 Profiling a Stateless
POR

Mdl(2,3)
Mdl(3,2)
Mdl(4,3)

38K
38K
38K

5
7
9

46.2
31.1
TO

Pla(1,5)
Pla(2,4)
Pla(4,3)
Pla(6,3)

41K
41K
41K
41K

2
3
5
7

22.8
37.2
160.5
TO

576 U
256 U
14K U

1
80
1368
4580

TO
402
TO

U
1.7
U 142.4
U
TO
U
TO

304 U
256 U
329 U

1
80
266
269

U
U
U
U

We profiled Dpu on a selection of
7 programs from Table 1 to unTable 2: Comparing DPU with Maple (same
derstand the cost of each compo- machine). Columns are: LOC: lines of code; Exnent. Dpu spends between 30% ecs: nr. of executions; R: safe or unsafe. Remainand 90% of the run time execut- ing columns as before. Timeout: 8 min.
ing the program (65% in average).
The remaining run time is spent computing alternatives, distributed as follows:
adding events to the event structure (15% to 30%), building the spikes of a
new comb (1% to 50%), searching for solutions in the comb (less than 5%), and
computing conflicting extensions (less than 5%).
Counterintuitively, building the comb is more expensive than exploring it,
even in the optimal case. This is because filling the spikes with events is more
memory-intensive than exploring the comb, which exploits data locality.

7

Conclusion

We have shown that computing alternatives in an optimal DPOR exploration is
NP-complete. To mitigate this problem, we introduced a new approach to compute alternatives in polynomial time, approximating the optimal exploration
with a user-defined constant. Experiments conducted on benchmarks including
Debian packages show that our implementation outperforms current verification
tools and uses appropriate data structures. Our profiling results show that running the program is often more expensive than computing alternatives. Hence,
efforts in reducing the number of redundant executions, even if significantly
costly, are likely to reduce the overall execution time.

References
1. Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking
software. In: Principles of Programming Languages (POPL), ACM (2005) 110–121
2. Abdulla, P., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order
reduction. In: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’14), ACM, ACM (2014)
3. Rodrı́guez, C., Sousa, M., Sharma, S., Kroening, D.: Unfolding-based partial order
reduction. In: Proc. CONCUR. (2015) 456–469
4. Mazurkiewicz, A.: Trace theory. In: Petri Nets: Applications and Relationships to
Other Models of Concurrency. Volume 255 of LNCS. Springer (1987) 278–324
5. Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems
– An Approach to the State-Explosion Problem. Volume 1032 of LNCS. Springer
(1996)
6. Abdulla, P.A., Aronis, S., Jonsson, B., Sagonas, K.: Comparing source sets and
persistent sets for partial order reduction. In: Models, Algorithms, Logics and
Tools - Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th
Birthday. (2017) 516–536
7. Nielsen, M., Plotkin, G.D., Winskel, G.: Petri nets, event structures and domains.
In: Proc. of the International Symposium on Semantics of Concurrent Computation. Volume 70 of LNCS., Springer (1979) 266–284
8. Sousa, M., Rodrı́guez, C., D’Silva, V., Kroening, D.: Abstract interpretation with
unfoldings. CoRR abs/1705.00595 (2017)
9. Nielsen, M., Plotkin, G., Winskel, G.: Petri nets, event structures and domains,
part I. Theoretical Computer Science 13(1) (1981) 85–108
10. Esparza, J., Heljanko, K.: Unfoldings – A Partial-Order Approach to Model Checking. EATCS Monographs in Theoretical Computer Science. Springer (2008)
11. Esparza, J.: A false history of true concurrency: From Petri to tools. In Pol, J.v.d.,
Weber, M., eds.: Proc. SPIN. Volume 6349 of LNCS. Springer (2010) 180–186
12. Rodrı́guez, C., Sousa, M., Sharma, S., Kroening, D.: Unfolding-based partial order
reduction. CoRR abs/1507.00980 (2015)
13. McMillan, K.L.: Using unfoldings to avoid the state explosion problem in the
verification of asynchronous circuits. In Bochmann, G.v., Probst, D.K., eds.: Proc.
CAV’92. Volume 663 of LNCS., Springer (1993) 164–177
14. Yang, Y., Chen, X., Gopalakrishnan, G., Kirby, R.M.: Efficient stateful dynamic
partial order reduction. In: Model Checking Software (SPIN). Volume 5156 of
LNCS. Springer (2008) 288–305
15. Abdulla, P.A., Aronis, S., Atig, M.F., Jonsson, B., Leonardsson, C., Sagonas, K.:
Stateless model checking for TSO and PSO. In: International Conference on Tools
and Algorithms for the Construction and Analysis of Systems (TACAS), Springer
(2015) 353–367
16. Farzan, A., Holzer, A., Razavi, N., Veith, H.: Con2colic Testing. In: Proceedings of
the 2013 9th Joint Meeting on Foundations of Software Engineering. ESEC/FSE
2013, New York, NY, USA, ACM (2013) 37–47
17. Pugh, W.: Skip lists: A probabilistic alternative to balanced trees. In: Algorithms
and Data Structures, Workshop WADS ’89, Ottawa, Canada, August 17-19, 1989,
Proceedings. (1989) 437–449
18. Coons, K.E., Musuvathi, M., McKinley, K.S.: Bounded partial-order reduction.
In: OOPSLA. (2013) 833–848
19. blktrace: http://brick.kernel.dk/snaps/.

20. MAFFT: http://mafft.cbrc.jp/alignment/software/.
21. Yu, J., Narayanasamy, S., Pereira, C., Pokam, G.: Maple: A coverage-driven testing
tool for multithreaded programs. In: OOPSLA. (2012) 485–502
22. Thomson, P., Donaldson, A.F., Betts, A.: Concurrency testing using controlled
schedulers: An empirical study. TOPC 2(4) (2016) 23:1–23:37
23. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)
24. Murata, T.: Petri nets: Properties, analysis and applications. Proc. of the IEEE
77(4) (April 1989) 541–580

A

Additional Basic Definitions

In this section we introduce a number of definitions that were excluded from the
body of the paper owing to space constraints.
Labelled Transition Systems. We defined an LT S semantics for programs in
Sec. 2 without first providing a general definition of LT Ss. An LT S [23] is
a structure M := hΣ, →, A, s0 i, where Σ are the states, A the actions, → ⊆
a
′
Σ × A × Σ the transition relation, and s0 ∈ Σ an initial state. If s −
→ s is a
′
transition, the action a is enabled at s and a can fire at s to produce s . We
let enabl (s) denote the set of actions enabled at s.
A sequence σ := a1 . . . an ∈ A∗ is a run when there are states s1 , . . . , sn
a1
an
satisfying s0 −
sn . We define state(σ) := sn . We let runs(M ) denote
→ s1 . . . −−→
the set of all runs of M , and reach(M ) := {state(σ) ∈ Σ : σ ∈ runs(M )} the set
of all reachable states.
Prime Event Structures. Let E := hE, <, #i be a pes. Two events e, e′ ∈ E
are in immediate conflict if e # e′ but both ⌈e⌉ ∪ [e] and [e] ∪ ⌈e′ ⌉ are free of
conflict. Given a set U ⊆ E, we denote by #iU (e) the set of events in U that are
in immediate conflict with e.
Unfolding semantics of an LT S. In Sec. 2 we defined the unfolding semantics
of a program (Def. 1). Now we give a slightly more general definition for LT Ss.
The definitions are almost identical, the only differences are found in the first
three lines of the definition. In particular the four fixpoint rules are exactly the
same. The reason why we give now this definition over LT S is because we will
use it to define unfolding semantics for Petri nets in the proof of Theorem 5.
Definition 8 (Unfolding of an LT S [3]). Given an LT S M := hΣ, →, A, s0 i
and some independence relation ♦ ⊆ A × A on M , the unfolding of M under ♦,
denoted UM,♦ , is the pes over A constructed by the following fixpoint rules:
1. Start with a pes E := hE, <, #, hi equal to h∅, ∅, ∅, ∅i.
2. Add a new event e := ha, Ci to E for any configuration C ∈ conf (E) and
any action a ∈ A such that a is enabled at state(C) and ¬(a ♦ h(e′ )) holds
for every <-maximal event e′ in C.
3. For any new e in E, update <, #, and h as follows:
– for every e′ ∈ C, set e′ < e;
– for any e′ ∈ E \ C, set e′ # e if e 6= e′ and ¬(a ♦ h(e′ ));
– set h(e) := a.
4. Repeat steps 2 and 3 until no new event can be added to E; return E.
Obviously, both Def. 1 and Def. 8 produce the same unfolding when applied
to a program. That is, for any program P and independence ♦ on MP , we have
that UP,♦ (Def. 1) is equal to UMP ,♦ (Def. 8).

Petri nets. A Petri net [24] is a model of a concurrent system. Formally, a net is
a tuple N := hP, T, F, m0 i, where P and T are disjoint finite sets of places and
transitions, F ⊆ (P × T ) ∪ (T × P ) is the flow relation, and m0 : P → N is the
initial marking. N is called finite if P and T are finite. Places and transitions
together are called nodes.
For x ∈ P ∪ T , let • x := {y ∈ P ∪ T : (y, x) ∈ F } be the preset, and
x• := {y ∈ P ∪ T : (x, y) ∈ F } the postset of x. The state of a net is represented
by a marking. A marking of N is a function m : P → N that assigns tokens to
every place. A transition t is enabled at a marking m iff for any p ∈ • t we have
m(p) ≥ 1.
We give semantics to nets using transition systems. We associate N with
a transition system MN := hΣ, →, A, m0 i where Σ := P → N is the set of
markings, A := T is the set of transitions, and → ⊆ Σ × A × Σ contains a triple
t
′
•
m →
− m exactly when, for any p ∈ t we have m(p) ≥ 1, and for any p ∈ P
′
•
we have m (p) = m(p) − |{p} ∩ t| + |{p} ∩ t• |. We call N k-safe when for any
reachable marking m ∈ reach(MN ) we have m(p) ≤ k, for p ∈ P .

B

General Lemmas

For the rest of this section, we fix an LT S M := hΣ, A, →, s0 i and an independence relation ♦ on M . We assume that runs(M ) is a finite set of finite sequences.
Let UM,♦ := hE, <, #, hi be the unfolding of M under ♦, which we will abbreviate as U. Note that U is finite because of our assumption about runs(M ). We
assume that U is the input pes provided to Alg. 1. Finally, without loss of generality we assume that U contains a special event ⊥ that is a causal predecessor
of any other event in U.
Algorithm 1 is recursive, each call to Explore(C, D, A) yields either no recursive call, if the function returns at line 5, or one single recursive call (line 10),
or two (line 10 and line 12). Furthermore, it is non-deterministic, as e is chosen
from either the set en(C) \ D or the set A ∩ en(C), which in general are not
singletons. As a result, the configurations explored by it may differ from one
execution to the next.
For each run of the algorithm on U we define the call graph explored by Alg. 1
on that run as a directed graph hB, ⊲i representing the actual exploration of U.
Different executions will in general yield different call graphs.
The nodes B of the call graph are 4-tuples of the form hC, D, A, ei, where
C, D, A are the parameters of a recursive call made to the funtion Explore(·, ·, ·),
and e is the event selected by the algorithm immediately before line 10. More
formally, B contains exactly all tuples hC, D, A, ei satisfying that
– C, D, and A are sets of events of the unfolding U;
– during the execution of Explore(∅, ∅, ∅), the function Explore(·, ·, ·) has
been recursively called with C, D, A as, respectively, first, second, and third
argument;

– e ∈ E is the event selected by Explore(C, D, A) immediately before line 10
if en(C) 6⊆ D. When en(C) ⊆ D we define e := ⊥. 4
The edge relation of the call graph, ⊲ ⊆ B×B, represents the recursive calls made
by Explore(·, ·, ·). Formally, it is the union of two disjoint relations ⊲ := ⊲l ⊎ ⊲r ,
defined as follows. We define that
hC, D, A, ei ⊲l hC ′ , D′ , A′ , e′ i and that hC, D, A, ei ⊲r hC ′′ , D′′ , A′′ , e′′ i
iff the execution of Explore(C, D, A) issues a recursive call to, respectively,
Explore(C ′, D′ , A′ ) at line 10 and Explore(C ′′, D′′ , A′′ ) at line 12. Observe
that C ′ and C ′′ will necessarily be different (as C ′ = C ∪ {e}, where e ∈
/ C, and
C ′′ = C), and therefore the two relations are disjoint sets. We distinguish the
node
b0 := h∅, ∅, ∅, ⊥i
as the initial node, also called the root node. Observe that hB, ⊲i is by definition
a weakly connected digraph, as there is a path from the node b0 to every other
node in B. We refer to ⊲l as the left-child relation and ⊲r as the right child
relation.
Lemma 1. Let hC, D, A, ei ∈ B be a state of the call graph. We have that
–
–
–
–
–

D ∩ A = ∅;
event e is such that e ∈ en(C) \ D;
C is a configuration;
C ∪ A is a configuration and C ∩ A = ∅;
D ⊆ ex (C);

(1)
(2)
(3)
(4)
(5)

Proof. Proving (2) is immediate, assuming that (1) holds. In Alg. 1, observe
both branches of the conditional statement where e is selected. If e is slected by
the then branch, clearly e ∈ en(C) \ D. If e is selected by the else branch, clearly
/ D, as e ∈ A and A is disjoint with D. Therefore
e ∈ en(C). But, by (1) e ∈
e ∈ en(C) \ D. In both cases (2) holds, what we wanted to prove.
All remaining items, (1) and (3) to (5), will be shown by induction on the
length n ≥ 0 of any path
b0 ⊲ b1 ⊲ . . . ⊲ bn−1 ⊲ bn
on the call graph, starting from the initial node and leading to bn := hC, D, A, ei
For i ∈ {0, . . . , n} we define hCi , Di , Ai , ei i := bi .
We start showing (1). Base case. n = 0 and D = A = ∅. The result holds.
Step. Assume that Dn−1 ∩ An−1 = ∅ holds. We have
D ∩ A = Dn ∩ An = Dn−1 ∩ (An−1 \ {e}) = Dn−1 ∩ An−1 = ∅
4

Observe that in this case, if en(C) ⊆ D, the execution of Explore(C, D, A) never
reaches line 10.

because removing event e from A will not increase the number of events shared
by A and D.
We now show (3), also by induction on n. Base case. n = 0 and C = ∅. The
set ∅ is a configuration. Step. Assume Cn−1 is a configuration. If bn−1 ⊲l bn , then
C = Cn−1 ∪ {e} for some event e ∈ en(C), as stated in (2). By definition, C is
a configuration. If bn−1 ⊲r bn , then C = Cn−1 . In any case C is a configuration.
We show (4), by induction on n. Base case. n = 0. Then C = ∅ and A = ∅.
Clearly C ∪ A is a configuration and C ∪ A = ∅. Step. Assume that Cn−1 ∪ An−1
is a configuration and that Cn−1 ∩ An−1 = ∅. We have two cases.
– Assume that bn−1 ⊲l bn . If An−1 is empty, then A is empty as well. Clearly
C ∪ A is a configuration and C ∩ A is empty. If An−1 is not empty, then
C = Cn−1 ∪ {e} and A = An−1 \ {e}, for some e ∈ An−1 , and we have
C ∪ A = (Cn−1 ∪ {e}) ∪ (An−1 \ {e}) = Cn−1 ∪ An−1 ,
so C ∪ A is a configuration as well. We also have that C ∩ A = Cn−1 ∩ An−1
(recall that e ∈
/ C), so C ∩ A is empty.
– Assume that bn−1 ⊲r bn holds. Then we have C = Cn−1 and also A =
J \ Cn−1 for some J ∈ Alt(Cn−1 , D ∪ {e}). Since J is a clue, from Defs. 2
and 3, we know that Cn−1 ∪ J is a configuration. As a result,
C ∪ A = Cn−1 ∪ (J \ Cn−1 ) = Cn−1 ∪ J,
and therefore C ∪A is a configuration. Finally, by construction of A at line 12,
we clearly have C ∩ A = ∅.
We show (5), again, by induction on n. Base case. n = 0 and D = ∅.
Then (5) clearly holds. Step. Assume that (5) holds for hCi , Di , Ai , ei i, with
i ∈ {0, . . . , n − 1}. We show that it holds for bn . As before, we have two cases.
– Assume that bn−1 ⊲l bn . We have that D = Dn−1 and that C = Cn−1 ∪
{en−1 }. We need to show that for all e′ ∈ D we have ⌈e′ ⌉ ⊆ C and e′ ∈
/ C.
By induction hypothesis we know that D = Dn−1 ⊆ ex (Cn−1 ), so clearly
⌈e′ ⌉ ⊆ Cn−1 ⊆ C. We also have that e′ ∈
/ Cn−1 , so we only need to check
/ Dn−1 = D.
that e′ 6= en−1 . By (2) applied to bn−1 we have that en−1 ∈
That means that e′ 6= en−1 .
– Assume that bn−1 ⊲r bn . We have that D = Dn−1 ∪{en−1 }, and by hypothesis
we know that Dn−1 ⊆ ex (Cn−1 ) = ex (C). As for en−1 , by (2) we know that
en−1 ∈ en(Cn−1 ) = en(C) ⊆ ex (C). As a result, D ⊆ ex (C).
Lemma 2. Let b := hC, D, A, ei and b′ := hC ′ , D′ , A′ , e′ i be two nodes of the
call graph such that b ⊲ b′ . Then
– C ⊆ C ′ and D ⊆ D′ ;
– if b ⊲l b′ , then C ( C ′ ;
– if b ⊲r b′ , then D ( D′ .

(6)
(7)
(8)

Proof. If b ⊲l b′ , then C ′ = C ∪ {e} and D′ = D. Then all the three statements
hold. If b ⊲r b′ , then C ′ = C and D′ = D ∪{e}. Similarly, all the three statements
hold.
Lemma 3. If C ⊆ C ′ are two finite configurations, then en(C) ∩ (C ′ \ C) = ∅
iff C ′ \ C = ∅.
Proof. If there is some e ∈ en(C) ∩ (C ′ \ C), then e ∈
/ C and e ∈ C ′ , so C ′ \ C
′
′
is not empty. If there is some e ∈ C \ C, then there is some e′′ event that is
<-minimal in C ′ \ C. As a result, ⌈e′′ ⌉ ⊆ C. Since e′′ ∈
/ C and C ∪ {e′′ } is a
′′
′
′′
configuration (as C ∪{e } ⊆ C ), we have that e ∈ en(C). Then en(C)∩(C ′ \C)
is not empty.

C

Termination Proofs

Lemma 4. Any path b0 ⊲ b1 ⊲ b2 ⊲ . . . in the call graph starting from b0 is finite.
Proof. By contradiction. Assume that b0 ⊲ b1 ⊲ . . . is an infinite path in the call
graph. For 0 ≤ i, let hCi , Di , Ai , ei i := bi . Recall that U has finitely many events,
finitely many finite configurations, and no infinite configuration. Now, observe
that the number of times that Ci and Ci+1 are related by ⊲l rather than ⊲r is
finite, since every time Explore(·, ·, ·) makes a recursive call at line 10 it adds
one event to Ci , as stated by (7). More formally, the set
L := {i ∈ N : Ci ⊲l Ci+1 }
is finite. As a result it has a maximum, and its successor k := 1 + max< L is an
index in the path such that for all i ≥ k we have Ci ⊲r Ci+1 , i.e., the function
only makes recursive calls at line 12. We then have that Ci = Ck , for i ≥ k, and
by (5), that Di ⊆ ex (Ck ). Since U is finite, note that ex (Ck ) is finite as well.
But, as a result of (7) the sequence
Dk ( Dk+1 ( Dk+2 ( . . .
is an infinite increasing sequence. This is a contradiction, as for sufficiently large
j ≥ 0 we will have that Dk+j will be larger than ex (Ck ), yet Dk+j ⊆ ex (Ck ).
Theorem 1 (Termination). Regardless of its input, Alg. 1 always stops.
Proof. The statement of the theorem refers to Alg. 1, but we instead prove it
for Alg. 1. Remark that Alg. 1 makes calls to two functions, namely, Remove(·)
and Alt(·, ·). Clearly both of them terminate (the loop in Remove(·) iterates
over a finite set). Since we gave no algorithm to compute Alt(·), we will assume
we employ one that terminates on every input.
Now, observe that there is no loop in Alg. 1. Thus any non-terminating
execution of Alg. 1 must perform a non-terminating sequence of recursive calls,
which entails the existence of an infinite path in the call graph associated to the
execution. Since, by Lemma 4, no infinite path exist in the call graph, Alg. 1
always terminates.

D

Completeness Proofs

Lemma 5. Let b := hC, D, A, ei ∈ B be a node in the call graph and Ĉ ⊆ E an
arbitrary maximal configuration of U such that C ⊆ Ĉ and D ∩ Ĉ = ∅. Then
exactly one of the following statements holds:
–
–
–
–

Either C is a maximal configuration of U, or
C is not maximal but en(C) ⊆ D, or
e ∈ Ĉ and b has a left child, or
e∈
/ Ĉ and b has a right child.

Proof. If C is maximal, then the first statement holds and b has no successor in
the call graph, so none of the other three statements hold and we are done.
So assume that C is not maximal. Then en(C) 6= ∅. Now, if en(C) ⊆ D holds
then the second statement is true and none of the others is (as Alg. 1 does not
make any recursive call in this case).
So assume also that en(C) 6⊆ D. That implies that b has at least one left
child. If e ∈ Ĉ, then we are done, as the second statement holds and none of the
others hold.
So finally, assume that e ∈
/ Ĉ, we need to show that the third statement holds,
i.e. that b has right child. By Def. 3 we know that the set of clues returned by the
call to Alt(C, D∪{e}) will be non-empty, as there exists a maximal configuration
Ĉ such that C ⊆ Ĉ (by hypothesis) and
Ĉ ∩ (D ∪ {e}) = (Ĉ ∩ D) ∪ (Ĉ ∩ {e}) = Ĉ ∩ D = ∅.
This means that Alg. 1 will make a recursive call at line line 12 and b will have
a right child. This shows that the last statement holds. And clearly none of the
other statements holds in this case.
Lemma 6. For any node b := hC, D, ·, ei ∈ B in the call graph and any maximal
configuration Ĉ ⊆ E of U, if
C ⊆ Ĉ and D ∩ Ĉ = ∅,
then there is a node b′ := hC ′ , ·, ·, ·i ∈ B such that b ⊲∗ b′ and Ĉ = C ′ .
Proof. The proof works by explicitly constructing a path from b to b′ using an
iterated application of Lemma 5.
Since C ⊆ Ĉ and D ∩ Ĉ = ∅, we can apply Lemma 5 to b and Ĉ and conclude
that exactly one of the four statements in that Lemma will be true at b. If C is
maximal, then necessarily C = Ĉ and we are done. If C is not maximal, then
it must be the case that en(C) 6⊆ D and b has at least one left child. This is
because by Lemma 3 we have that
en(C) ∩ (Ĉ \ C) = ∅ iff Ĉ \ C = ∅.
Since C is not maximal Ĉ \ C 6= ∅ and we see that en(C)∩ Ĉ must be non-empty.
Now, since Ĉ and D are disjoint, the event(s) in en(C) ∩ Ĉ are not in D, and
so en(C) contains events which are not contained in D.

Since en(C) 6⊆ D we have that the second statement in Lemma 5 does not
hold, and so either the third or the fourth statement have to be hold.
Now, b has a left child and two cases are possible, either e ∈ Ĉ or not. If
e ∈ Ĉ we let b1 := hC1 , D1 , ·, e1 i be the left child of b, with C1 := C ∪ {e}
and D1 := D. If e ∈
/ Ĉ, then only the last statement of Lemma 5 can hold and
we know that b has a right child. Let b1 := hC1 , D1 , ·, e1 i, with C1 := C and
D1 := D ∪ {e} be that child. Observe that in both cases C1 ⊆ Ĉ and D1 ∩ Ĉ = ∅.
If C1 is maximal, then necessarily C1 = Ĉ, we take b′ := b1 and we have
finished. If not, we can reapply Lemma 5 at b1 and make one more step into
one of the children b2 of b1 . If C2 is still not maximal (thus different from Ĉ)
we need to repeat the argument starting from b2 only a finite number n of times
until we reach a node bn := hCn , Dn , ·, ·i where Cn is a maximal configuration.
This is because every time we repeat the argument on a non-maximal node bi we
advance one step down in the call graph, and by Lemma 4 all paths in the graph
starting from the root are finite. So eventually we find a leaf node bn where Cn
is maximal and satisfies Cn ⊆ Ĉ. This implies that Cn = Ĉ, and we can take
b′ := bn .
Theorem 2 (Completeness). Let Ĉ be a ⊆-maximal configuration of UP,♦ .
Then Alg. 1 calls Explore(C, D, A) at least once with C = Ĉ.
Proof. We need to show that for every maximal configuration Ĉ ⊆ E we can
find a node b := hC, ·, ·, ·i in B such that Ĉ = C. This is a direct consequence
of Lemma 6. Consider the root node of the tree, b0 := hC0 , D0 , A0 , ⊥i, where
C0 = D0 = A0 = ∅. Clearly C0 ⊆ Ĉ and D0 ∩ Ĉ = ∅, so Lemma 6 applies to Ĉ
and b0 , and establishes the existence of the aforementioned node b.

E

Complexity Proofs

Theorem 3. Given a finite pes E, some configuration C ∈ conf (E), and a
set D ⊆ ex (C), deciding if an alternative to D after C exists in E is NP-complete.
Proof. We first prove that the problem is in NP. Let us non-deterministically
choose a configuration J ⊆ E. We then check that J is an alternative to D
after C:
– J ∪ C is a configuration can be checked in linear time: The first condition
for J ∪ C to be a configuration is that ∀e ∈ J ∪ C : ⌈e⌉ ⊆ J ∪ C. Since
J is a configuration, this condition holds for all e ∈ J. Similarly, as C is
a configuration, it also holds for all e ∈ C. The second condition is that
∀e1 , e2 ∈ J ∪ C : ¬(e1 # e2 ). This is true for e1 , e2 ∈ J and e1 , e2 ∈ C.
If e1 ∈ J ∧ e2 ∈ C (or the converse), we have to effectively check that
¬(e1 # e2 ). Checking if two events e1 and e2 are in conflict is linear on the
size of [e1 ] ∪ [e2 ].
– Every event e1 ∈ D must be in immediate conflict with an event e2 ∈ J.
Thus, there are at most |D| · |J| checks to perform, each in linear time on
the size of [e1 ] ∪ [e2 ]. Hence, this is in O(n2 ).

We now prove that the problem is NP-hard, by reduction from the 3-SAT
problem. Let {v1 , . . . , vn } be a set of Boolean variables. Let φ := c1 ∧ . . . ∧ cm
be a 3-SAT formula, where each clause ci := li ∨ li′ ∨ li′′ comprises three literals.
A literal is either a Boolean variable vi or its negation vi .
Formula φ can be modelled by a PES Eφ := hE, <, #, hi constructed as
follows:
– For each variable vi we create two events ti and fi in E, and put them
in immediate conflict, as they correspond to the satisfaction of vi and vi ,
respectively.
– The set D of events to disable contains one event dj per clause cj . Such a
dj has to be in immediate conflict with the events modelling the literals in
clause cj . Hence it is in conflict with 1, 2, or 3 t or f events.
– There is no causality: <:= ∅.
– The labelling function shows the correspondence between the events and the
elements of formula φ, i.e. ∀ti ∈ E : h(ti ) = vi , ∀fi ∈ E : h(fi ) = vi and
∀dj ∈ E : h(dj ) = cj .
We now show that φ is satisfiable iff there exists an alternative J to D after
C := ∅ in E. This alternative is constructed by selecting for each event dj ∈ D
and event e in immediate conflict. By construction of Eφ , h(e) is a literal in clause
h(dj ) = cj . Moreover, C ∪ J = J must be a configuration. The causal closure is
trivially satisfied since < := ∅. The conflict-freeness implies that if ti ∈ J then
fi 6∈ J and vice-versa. Therefore, formula φ is satisfiable iff an alternative J to D
exists.
The construction of Eφ is illustrated in Fig. 4 for:
φ := (x1 ∨ x2 ∨ x3 ) ∧ (x1 ∨ x2 ) ∧ (x1 ∨ x3 )
{z
} | {z } | {z }
|
c1

c2

d1
c1

x1
t1

c3

d2
c2

x1

x2

f1

t2

d3
c3

x2

x3

x3

f2

t3

f3

Fig. 4: Example of encoding a 3-SAT formula.

Theorem 4. Let P be a program and U a causally-closed set of events from
UP,♦P . For any configuration C ⊆ U and any D ⊆ ex (C), deciding if an alternative to D after C exists in U is NP-complete.

Proof. Observe that the only difference between the statement of this theorem
and that of Theorem 3 is that here we assume the PES to be the unfolding of a
given program P under the relation ♦P .
As a result the problem is obviously in NP, as restricting the class of PESs
that we have as input cannot make the problem more complex.
However, showing that the problem is NP-hard requires a new encoding, as
the (simple) encoding given for Theorem 3 generates PESs that may not be the
unfolding of any program. Recall that two events in the unfolding of a program
are in immediate conflict only if they are lock statements on the same variable.
So, in Fig. 4, for instance, since t1 # f1 and f1 # d2 , then necessarily we should
have t1 # d2 , as all the three events should be locks to the same variable.
For this reason we give a new encoding of the 3-SAT problem into our
problem. As before, let V = {v1 , . . . , vn } be a set of Boolean variables. Let
φ := c1 ∧ . . . ∧ cm be a 3-SAT formula, where each clause ci := li ∨ li′ ∨ li′′ comprises three literals. A literal is either a Boolean variable vi or its negation vi .
As before, for a variable v, let pos(v) denote the set of clauses where v appears
positively and neg(v) the set of clauses where it appears negated. We assume
that every variable only appears either positively or negatively in a clause (or
does not appear at all), as clauses where a variable happens both positively and
negatively can be removed from φ. As a result pos(v) ∩ neg(v) = ∅ for every
variable v.
Let us define a program Pφ as follows:
– For each Boolean variable vi we have two threads in P , ti corresponding to
vi (true), and fi corresponding to vi (false). We also have one lock lvi .
– Immediately after starting, both threads ti and fi lock on lvi . This scheme
corresponds to choosing a Boolean value for variable vi : the thread that locks
first chooses the value of vi .
– For each clause cj ∈ φ, we have a thread dj and a lock lcj . The thread
contains only one statement which is locking lcj .
– For each clause cj ∈ pos(vi )∪neg(vi ), the program contains one thread rhvi ,cj i
(run for variable vi in clause cj ). This thread contains only one statement
which is locking lcj .
– After locking on lvi , thread ti starts in a loop all threads rhvi ,cj i , for cj ∈
pos(vi ). Since we do not have thread creation in our program model, we
start a thread as follows: for each thread rhvi ,cj i we create an additional lock
that is initially acquired. Immediately after starting, rhvi ,cj i tries to acquire
it. When ti wishes to start the thread, it just releases the lock, effectively
letting the thread start running.
– Similarly, after locking on lvi , thread fi starts in a loop all threads rhvi ,cj i ,
for cj ∈ neg(vi ).
When Pφ is unfolded, each statement of the program gives rise to exactly
one event in the unfolding. Indeed, by construction, each ti or fi thread starts
by a lock event and then causally lead to one r event per clause the variable vi
appears in. Any two of them concern different clauses and thus different locks,
and they are independent.

Let C := ∅ be an empty configuration, D := {d1 , . . . , dm }, and U the set of
all events in the unfolding of the program.
We now show that φ is satisfiable iff there exists an alternative J to D after
C := ∅ in UPφ ,♦Pφ . This alternative is constructed by selecting for each event
dj ∈ D and event e in immediate conflict. By construction of Pφ , it is a rhvi ,cj i
where vi is a literal in clause h(dj ) = cj . Moreover, C ∪ J = J must be a
configuration. In order to satisfy the causal closure, since
< := {hti , rhvi ,cj i i : cj ∈ pos(vi )} ∪ {hfi , rhvi ,cj i i : cj ∈ neg(vi )},
J must also contain the ti or fi preceding rhvi ,cj i . The conflict-freeness implies
that if ti ∈ J then fi 6∈ J and vice-versa. Therefore, formula φ is satisfiable iff
an alternative J to D exists.
There are at most 2|V | + |φ|(|V | + 1) events, so the construction can be
achieved in polynomial time. Therefore our problem is NP-hard.
The construction of UPφ is illustrated in Fig. 5 for:
φ := (x1 ∨ x2 ∨ x3 ) ∧ (x1 ∨ x2 ) ∧ (x1 ∨ x3 )
|
{z
} | {z } | {z }
c1

c2

d1
c1

d2
c2

lc 1

rhx1 ,c1 i

lc 2

rhx1 ,c3 i
x1
t1

lx 1

rhx1 ,c2 i

rhx2 ,c1 i

x1

x2

f1

t2

c3

d3
c3

lc 3

lx 2

rhx2 ,c2 i

rhx3 ,c1 i

x2

x3

f2

t3

rhx3 ,c3 i

lx 3

x3
f3

Fig. 5: Program unfolding encoding a 3-SAT formula.

Theorem 5. Let N be a Petri net, t a transition of N , E the unfolding of N
and C a configuration of E. Deciding if h−1 (t) ∩ cex (C) = ∅ is NP-complete.
Proof. Given a Petri net N := hP, T, F, m0 i, a transition t ∈ T , an independence
relation ♦ ⊆ T × T , the unfolding E := UMN ,♦ of N , and a configuration C of E,
we need to prove that deciding whether h−1 (t) ∩ cex (C) = ∅ is an NP-complete
problem.

We first prove that the problem is in NP. This is achieved using a guess and
check non-deterministic algorithm to decide the problem. Let us non-deterministically choose a configuration C ′ ⊆ C, in linear time on the input. A linearisation of C ′ is chosen and used to compute the marking m reached. We check
that m enables t and that for any <-maximal event e of C, ¬(h(e) ♦ t) holds.
Both tests can be done in polynomial time. If both tests succeed then we answer
yes, otherwise we answer no.
We now prove that the problem is NP-hard, by reduction from the 3-SAT
problem. Let V = {v1 , . . . , vn } be a set of Boolean variables. Let φ := c1 ∧. . .∧cm
be a 3-SAT formula, where each clause ci := li ∨ li′ ∨ li′′ comprises three literals. A
literal is either a Boolean variable vi or its negation vi . For a variable v, pos(v)
denotes the set of clauses where v appears positively and neg(v) the set of clauses
where it appears negated.
Given φ, we construct a 3-safe net Nφ , an independence relation ♦, a configuration C of the unfolding E, and a transition t from Nφ such that φ is satisfiable
iff some event in ex (C) is labelled by t :
– The net contains one place di per clause ci , initially empty.
– For each variable vi are two places si and s′i . Places si initially contain 1
token while places s′i are empty.
– For each variable vi , a transition pi takes into account positive values of the
variable. It takes a token from si , puts one in s′i (to move on to the other
possibility for this variable) and puts one token in all places associated with
clauses cj ∈ pos(vi ). This transition mimics the validation of clauses where
the variable appears as positive.
– For each variable vi , a transition ni takes into account negative values of the
variable. It takes a token from s′i and puts one token in all places associated
with clauses cj ∈ neg(vi ). It also removes one token from all places associated
with clauses cj ∈ pos(vi ), that have been marked by some pk transition. This
transition ni mimics the validation of clauses where the variable appears as
negative.
– Finally, a transition t is added that takes a token from all di . Thus, it can
only be fired when all clauses are satisfied, i.e. formula φ is satisfied.

⊞

The independence relation ♦ is the smallest binary, symmetric, irreflexive
relation such that pi ♦ pj exactly when i 6= j and pi ♦ nj exactly when i 6= j.
Recall that pi , ni correspond to respectively to the positive and negative valua:= T × T \ ♦ is
tions of variable vi . In other words, the dependence relation
the reflexive closure of the set
{hpi , ni i : 1 ≤ i ≤ n} ∪ {ht, pi i : 1 ≤ i ≤ n} ∪ {ht, ni i : 1 ≤ i ≤ n}
Relation ♦ is an independence relation because:
– ∀i 6= j, transitions pi and pj do not share any input place ;
– ∀i =
6 j, the intersection between p•i and • nj might not be empty, but nj is
always preceded by (and thus enabled after) pj (and not pi ). So firing pi
cannot enable, nor disable, pj , and firing pi and nj in any order reaches the
same state.

Finally, configuration C contains exactly one event per pi and one per ni ,
hence 2|V | events. This is because transition ni is dependent only of pi , and
independent of (thus concurrent to) any other transition in C. Thus formula
φ has a model iff there is an event e ∈ en(C) labelled by t. Indeed, initially
only positive transitions pi are enabled that assign a positive value to their
corresponding variable vi . They add a token in all places dj such that cj ∈
pos(vi ). Then, when a negative transition ni fires, it deletes the tokens from
these dj that had been created by pi since the variable cannot allow for validating
these clauses anymore. It also adds tokens in the dk such that ck ∈ neg(vi ) since
the clauses involving vi now hold. Therefore, the number of tokens in a place dj
is the number of variables (or their negation) that validate the associated clause.
Formula φ is satisfied when all clauses hold at the same time, i.e. each clause is
validated by at least one variable. Thus all places d must contain at least one
token (and enable t) for φ satisfaction.
The construction of Nφ is illustrated in Fig. 6 for:
φ := (x1 ∨ x2 ∨ x3 ) ∧ (x1 ∨ x2 ) ∧ (x1 ∨ x3 )
|
{z
} | {z } | {z }
c1

c2

s1

c3

s2

s3

p1

p2

p3

s′1

s′2

s′3

n1

n2

n3

d1

d2

d3

t
Fig. 6: Petri Net encoding a 3-SAT formula.

F

Proofs for Causality Trees

Theorem 6. Let e, e′ ∈ E be two arbitrary events from resp. threads i and i′ ,
with i 6= i′ . Then e < e′ holds iff e 6 tmax (e′ , i). And e # e′ holds iff there is
some l ∈ L such that lmax (e, l) # lmax (e′ , l).

Proof. Firstly, we show that e < e′ holds iff e = tmax (e′ , i) ∨ e < tmax (e′ , i).
– Direction ⇒. Assume that e < e′ . This implies that e ∈ ⌈e′ ⌉ and there
must exist ê ∈ [e′ ] such that ê = tmax(e′ , i). Since both e and ê are events
from thread i, and both are contained in [e′ ] they cannot be in conflict, but
¬(h(e) ♦ h(ê)). Then either e = ê or e < ê.
– Direction ⇐. Let ê := tmax (e′ , i). Since i 6= i′ we have that ê 6= e′ , and since
ê ∈ [e′ ] we have that ê < e′ . Let e ∈ E be any event such that either e = ê
or e < ê. We then have e 6 ê < e′ , so clearly e < e′ .
Now we show that e # e′ holds iff there is some l ∈ L such that lmax (e, l) #
lmax (e′ , l).
– Direction ⇒. Assume that e # e′ holds. Then necessary there exist events
e′1 ∈ [e] and e′2 ∈ [e′ ] such that e′1 #i e′2 . Since only lock events touching
the same variable are able to create immediate conflicts, we obviously know
that ∃l ∈ L : h(e′1 ) = h(e′2 ) = hacq, li. Since e′1 ∈ [e] then ∃e1 ∈ [e] : ∃e1 =
lmax (e, l). Similarly, ∃e2 ∈ [e′ ] : e2 = lmax (e′ , l). Both e1 and e2 are <maximal events, so e′1 < e1 or e′1 = e1 and e2 < e′2 or e2 = e′2 . The conflict
is inherited, having e′1 #i e′2 implies e1 # e2 .
– Direction ⇐. Assume that there is some l ∈ L such that lmax (e, l) #
lmax (e′ , l) and let e1 ∈ [e] : e1 = lmax (e, l) and e2 ∈ [e′ ] : e2 = lmax (e′ , l),
then e1 # e2 . Since e1 ∈ [e], we have e1 < [e]. Similarly, e2 ∈ [e′ ], i.e., e2 < e′ .
The conflict is inherited and e1 # e2 , so necessarily e # e′ .

G

Experiments with the SV-COMP’17 Benchmarks

In this section we present additional experimental results using the SV-COMP’17
benchmarks. In particular we use the benchmarks from the pthread/ folder.5
All benchmarks were taken from the official repository of the SV-COMP’17.
We modified almost all of them to remove the dataraces, using one or more
additional mutexes. All benchmarks have between 50 and 170 lines of code.
Most of them employ 2 or 3 threads but some of them reach up to 7 threads.
The first remark is that both tools correctly classified every benchmark as
buggy or safe. In Dpu we used QPOR with k = 1 and the exploration was
optimal on all benchmarks. That means that Nidhugg and Dpu are doing a
very similar exploration of the statespace in these benchmarks. As a result, it is
not surprising that both tools timeout on exactly the same benchmarks (5 out of
29). On the other hand most benchmarks in this suite are quite simple for DPOR
techniques: the longest run time for Dpu was 2.6s (and 4.5s for Nidhugg).
In general the run times for Nidhugg are slighly better than those of Dpu.
We traced this down to two factors. First, while Dpu is in general faster at
exploring new program interleavings, it has a slower startup time. Second, when
Dpu finds a bug, it does not stop and report it, it continues exploring the state
5

See https://github.com/sosy-lab/sv-benchmarks/releases/tag/svcomp17.

Benchmark

Dpu (k=1)

Nidhugg

Name

Time Bug

Time Bug

bigshot-p-false
bigshot-s2-true
bigshot-s-true
fib-bench-false
fib-bench-longer-false
fib-bench-longer-true
fib-bench-longest-false
fib-bench-longest-true
fib-bench-true
indexer-true
lazy01-false
queue-false
queue-longer-false
queue-longest-false
queue-ok-longer-true
queue-ok-longest-true
queue-ok-true
sigma-false
singleton-false
singleton-with-uninit-problems-true
stack-false
stack-longer-false
stack-longer-true
stack-longest-false
stack-longest-true
stack-true
stateful01-false
stateful01-true
twostage-3-false

0.46
0.45
0.45
0.87
2.57
2.23
TO
TO
0.89
TO
0.42
0.70
0.96
1.80
0.44
0.46
0.49
0.30
0.48
0.47
0.66
0.94
TO
1.85
TO
0.52
0.44
0.44
0.48

0.20
0.20
0.18
0.69
1.57
2.75
TO
TO
0.76
TO
0.82
0.21
0.53
0.53
0.29
0.37
0.19
0.24
0.21
0.20
0.21
1.50
TO
4.48
TO
0.35
0.20
0.19
0.40

y
n
n
y
y
n

n
y
y
y
y
n
n
n
y
y
n
y
y
y
n
y
n
y

y
n
n
y
y
n

n
y
y
y
y
n
n
n
y
y
n
y
y
y
n
y
n
y

Table 3: Comparing Dpu and Nidhugg on the pthread/ folder of the SV-COMP’17
benchmarks. Machine: Linux, Intel Xeon 2.4GHz. TO: timeout after 8 min. Columns
are: Time in seconds, Bug: y if the bug is detected, n if no bug is detected.

space of the program. This is in contrast to Nidhugg, which stops on the first
bug found. We will obviously implement a new mode in Dpu where the tool
stops on the first bug found, but for the time being this visibly affects Dpu on
bechmarks such as the queue-*-false, where Nidhugg is almost twice faster
than Dpu.

