1

arXiv:1610.01188v4 [cs.PL] 22 Oct 2017

Data-centric Dynamic Partial Order Reduction
MAREK CHALUPA, Masaryk University
KRISHNENDU CHATTERJEE, Institute of Science and Technology, Austria
ANDREAS PAVLOGIANNIS, Institute of Science and Technology, Austria
NISHANT SINHA, Kena Labs
KAPIL VAIDYA, Indian Institute of Technology, Bombay

We present a new dynamic partial-order reduction method for stateless model checking of concurrent programs. A common approach for exploring program behaviors relies on enumerating the traces of the program,
without storing the visited states (aka stateless exploration). As the number of distinct traces grows exponentially, dynamic partial-order reduction (DPOR) techniques have been successfully used to partition the space
of traces into equivalence classes (Mazurkiewicz partitioning), with the goal of exploring only few representative traces from each class.
We introduce a new equivalence on traces under sequential consistency semantics, which we call the observation equivalence. Two traces are observationally equivalent if every read event observes the same write
event in both traces. While the traditional Mazurkiewicz equivalence is control-centric, our new deﬁnition is
data-centric. We show that our observation equivalence is coarser than the Mazurkiewicz equivalence, and in
many cases even exponentially coarser. We devise a DPOR exploration of the trace space, called data-centric
DPOR, based on the observation equivalence.
(1) For acyclic architectures, our algorithm is guaranteed to explore exactly one representative trace from
each observation class, while spending polynomial time per class. Hence, our algorithm is optimal wrt the
observation equivalence, and in several cases explores exponentially fewer traces than any enumerative
method based on the Mazurkiewicz equivalence.
(2) For cyclic architectures, we consider an equivalence between traces which is ﬁner than the observation
equivalence; but coarser than the Mazurkiewicz equivalence, and in some cases is exponentially coarser.
Our data-centric DPOR algorithm remains optimal under this trace equivalence.
Finally, we perform a basic experimental comparison between the existing Mazurkiewicz-based DPOR and
our data-centric DPOR on a set of academic benchmarks. Our results show a signiﬁcant reduction in both
running time and the number of explored equivalence classes.

1:2
1

M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya
INTRODUCTION

Stateless model-checking of concurrent programs. The veriﬁcation of concurrent programs is one of
the major challenges in formal methods. Due to the combinatorial explosion on the number of interleavings, errors found by testing are hard to reproduce (often called Heisenbugs [Musuvathi et al.
2008]), and the problem needs to be addressed by a systematic exploration of the state space. Model
checking [Clarke et al. 1999a] addresses this issue, however, since model checkers store a large
number of global states, it cannot be applied to realistic programs. One solution that is adopted
is stateless model checking [Godefroid 1996], which avoids the above problem by exploring the
state space without explicitly storing the global states. This is typically achieved by a scheduler,
which drives the program execution based on the current interaction between the processes. Wellknown tools such as VeriSoft [Godefroid 1997, 2005] and CHESS [Madan Musuvathi 2007] have
successfully employed stateless model checking.
Partial-Order Reduction (POR). Even though stateless model-checking addresses the global state
space issue, it still suﬀers from the combinatorial explosion of the number of interleavings, which
grows exponentially. While there are many approaches to reduce the number of explored interleavings, such as, depth-bounding and context bounding [Lal and Reps 2009; Musuvathi and Qadeer
2007], the most well-known method is partial order reduction (POR) [Clarke et al. 1999b; Godefroid
1996; Peled 1993]. The principle of POR is that two interleavings can be regarded as equivalent if
one can be obtained from the other by swapping adjacent, non-conﬂicting (independent) execution steps. The theoretical foundation of POR is the equivalence class of traces induced by the
Mazurkiewicz trace equivalence [Mazurkiewicz 1987], and POR explores at least one trace from
each equivalence class. POR provides a full coverage of all behaviors that can occur in any interleaving, even though it explores only a subset of traces. Moreover, POR is suﬃcient for checking
most of the interesting veriﬁcation properties such as safety properties, race freedom, absence of
global deadlocks, and absence of assertion violations [Godefroid 1996].
Dynamic
Partial-order
Reduction
(DPOR).
Dynamic
partial-order
reduction
(DPOR) [Flanagan and Godefroid 2005] improves the precision of POR by recording actually occurring conﬂicts during the exploration and using this information on-the-ﬂy. DPOR
guarantees the exploration of at least one trace in each Mazurkiewicz equivalence class when the
explored state space is acyclic and ﬁnite, which holds for stateless model checking, as usually the
length of executions is bounded [Flanagan and Godefroid 2005; Godefroid 2005; Musuvathi et al.
2008]. Recently, an optimal method for DPOR was developed [Abdulla et al. 2014]. We refer to
Section 8 for more detailed references to related work.
A fundamental limitation. All existing approaches for DPOR are based on the Mazurkiewicz equivalence, i.e., they explore at least one (and possibly more) trace from each equivalence class. A basic
and fundamental question is whether coarser equivalence classes than the Mazurkiewicz equivalence can be applied to stateless model checking and whether some DPOR-like approach can be
developed based on such coarser equivalences. We start with a motivating example.
1.1

A minimal motivating example

Consider a concurrent system that consists of two processes and a single global variable x shown in
Figure 1. Denote by w i and r i the write and read events to x by process pi , respectively. The system
consists of four events which are all pairwise dependent, except for the pair r 1, r 2 . Two traces t and
t ′ are called Mazurkiewicz equivalent, denoted t ∼M t ′ , if they agree on the order of dependent

Data-centric Dynamic Partial Order Reduction
Process p 1 :

1:3
Process p 2 :

1. write x;

1. write x;

2. read x;

2. read x;

Fig. 1. A system of two processes with two events each.
events. The traditional DPOR based on the Mazurkiewicz equivalence ∼M will explore at least one
representative trace from every class induced on the trace space by the Mazurkiewicz equivalence.
3
There exist 22 = 4 possible orderings of dependent events, as there are 23 possible interleavings, but
half of those reorder the independent events r 1 , r 2 , and thus will not be considered. The traditional
DPOR will explore the following four traces.
t 1 : w 1 , r 1, w 2 , r 2

t 2 : w 1 , w 2 , r 1, r 2

t 3 : w 2 , w 1 , r 1, r 2

t 4 : w 2 , r 2, w 1 , r 1

Note however that t 1 and t 4 are state-equivalent, in the sense that the local states visited by p1 and
p2 are identical in the two traces. This is because each read event observes the same write event
in t 1 and t 4 . In contrast, in every pair of traces among t 1 , t 2 , t 3 , there is at least one read event that
observes a diﬀerent write event in that pair. This observation makes it natural to consider two
traces equivalent if they contain the same read events, and every read event observes the same
write event in both traces. This example illustrates that it is possible to have coarser equivalence
than the traditional Mazurkiewicz equivalence.
1.2

Our contributions

In this work our contributions are as follows.
Observation equivalence. We introduce a new notion of observation equivalence (Section 3.1),
which is intuitively as follows: An observation function of a trace maps every read event to the
write event it observes under sequentially consistent semantics. In contrast to every possible ordering of dependent control locations of Mazurkiewicz equivalence, in observation equivalence two
traces are equivalent if they have the same observation function. The observation equivalence has
the following properties.
(1) Soundness. The observation equivalence is suﬃcient for exploring all local states of each process, and is thus suﬃcient for model checking wrt to local properties (similar to Mazurkiewicz
equivalence).
(2) Coarser. Second, we show that observation equivalence is coarser than Mazurkiewicz equivalence, i.e., if two traces are Mazurkiewicz equivalent, then they are also observation equivalent
(Section 3.1).
(3) Exponentially coarser. Third, we show that observation equivalence can be exponentially more
succinct than Mazurkiewicz equivalence, i.e., we present examples where the ratio of the number of equivalence classes between observation and Mazurkiewicz equivalence is exponentially
small (Section 3.2).
In summary, observation equivalence is a sound method which is always coarser, and in cases,
strictly coarser than the fundamental Mazurkiewicz equivalence.

1:4

M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya

Principal diﬀerence. The principal diﬀerence between the Mazurkiewicz and our new observation
equivalence is that while the Mazurkiewicz equivalence is control-centric, observation equivalence
is data-centric. The data-centric approach takes into account read-write and memory consistency
restrictions as opposed to the event-dependency relation of the Mazurkiewicz equivalence.
Data-centric DPOR. We devise a DPOR exploration of the trace space, called data-centric DPOR,
based on the observation equivalence. Our DPOR algorithm is based on a notion of annotations,
which are intended observation functions (see Section 4). The basic computational problem is,
given an annotation, decide whether there exists a trace which realizes the annotation. The complexity of the problem depends on the communication graph of the system, called the architecture. Intuitively, the nodes of the architecture represent the processes of the concurrent system,
and there is an (undirected) edge between two nodes if the respective processes access a common
shared variable. We show that the computational problem is NP-complete in general, but for the important special case of acyclic architectures we present a polynomial-time (cubic-time) algorithm
based on reduction to 2-SAT (details in Section 4). Our algorithm has the following implications.
(1) For acyclic architectures, our algorithm is guaranteed to explore exactly one representative
trace from each observation equivalence class, while spending polynomial time per class. Hence,
our algorithm is optimal wrt the observation equivalence, and in several cases explores exponentially fewer traces than any enumerative method based on the Mazurkiewicz equivalence
(details in Section 5).
(2) For cyclic architectures, we consider an equivalence between traces which is ﬁner than the
observation equivalence; but coarser than the Mazurkiewicz equivalence, and in many cases
is exponentially coarser. For this equivalence on traces, we again present an algorithm for
DPOR that explore exactly one representative trace from each observation class, while spending
polynomial time per class. Thus again our data-centric DPOR algorithm remains optimal under
this trace equivalence for cyclic architectures (details in Section 6).
Experimental results. Finally, we perform a basic experimental comparison between the existing
Mazurkiewicz-based DPOR and our data-centric DPOR on a set of academic benchmarks. Our
results show a signiﬁcant reduction in both running time and the number of explored traces.
2

PRELIMINARIES

In this section we introduce a simple model for concurrent programs that will be used for stating
rigorously the key ideas of our data-centric DPOR. Similar (but syntactically richer) models have
been used in [Abdulla et al. 2014; Flanagan and Godefroid 2005]. In Section 2.3 we discuss our
various modeling choices and possible extensions.
Informal model. We consider a concurrent system of k processes under sequential consistency
semantics. For the ease of presentation, we do not allow dynamic thread creation, i.e., k is ﬁxed
during any execution of the system. Each process is deﬁned over a set of local variables speciﬁc
to the process, and a set of global variables, which is common for all processes. Each process is
represented as an acyclic control-ﬂow graph, which results from unrolling the body of the process.
A process consists of statements over the local and global variables, which we call events. The
precise kind of such events is immaterial to our model, as we are only interested in the variables
involved. In particular, in any such event we identify the local and global variables it involves,
and distinguish between the variables that the event reads from and at most one variable that
the event writes to. Such an event is visible if it involves global variables, and invisible otherwise.

Data-centric Dynamic Partial Order Reduction

1:5

We consider that processes are deterministic, meaning that at any given time there is at most one
event that each process can execute. Given the current state of the system, a scheduler chooses
one process to execute a sequence of events that is invisibly maximal, that is, the sequence does
not end while an invisible event from that process can be taken. The processes communicate by
writing to and reading from the global variables. The system can exhibit nondeterministic behavior
which is solely attributed to the scheduler, by choosing nondeterministically the next process to
take an invisibly maximal sequence of events from any given state. We consider locks as the only
synchronization primitive, with the available operations being acquiring a lock and releasing a
lock. Since richer synchronization primitives are typically built using locks, this consideration is
not restrictive, and helps with keeping the exposition of the key ideas simple.
2.1

Concurrent Computation Model

Here we present our model formally. Relevant notation is summarized in Table 1.
Relations and equivalence classes. A binary relation ∼ on a set X is an equivalence relation iﬀ
∼ is reﬂexive, symmetric and transitive. Given an equivalence ∼R and some x ∈ X , we denote by
[x]R the equivalence class of x under ∼R , i.e.,
[x]R = {y ∈ X : x ∼R y}
The quotient set X /∼R := {[x]R | x ∈ X } of X under ∼R is the set of all equivalence classes of X
under ∼R .
Notation on functions. We write f : X →
7 Y to denote that f is a partial function from X to
Y . Given a (partial) function f , we denote by dom(f ) and img(f ) the domain and image set of f ,
respectively. For technical convenience, we think of a (partial) function f as a set of pairs {(x i , yi )}i ,
meaning that f (x i ) = yi for all i, and use the shorthand notation (x, y) ∈ f to indicate that
x ∈ dom(f ) and f (x) = y. Given (partial) functions f and д, we write f ⊆ д if dom(f ) ⊆ dom(д)
and for all x ∈ dom(f ) we have f (x) = д(x), and f = д if f ⊆ д and д ⊆ f . Finally, we write f ⊂ д
if f ⊆ д and f , д.
Model syntax. We consider a concurrent architecture P that consists of a ﬁxed number of processes
p1 , . . . , pk , i.e., there is no dynamic thread creation. Each process pi is deﬁned over a set of ni local
variables Vi , and a set of global variables G, which is common for all processes. We distinguish a
set of lock variables L ⊆ G which are used for process synchronization. All variables are assumed
to range over a ﬁnite domain D. Every process pi is represented as an acyclic control-ﬂow graph
CFGi which results from unrolling all loops in the body of pi . Every edge of CFGi is labeled,
and called an event. In particular, the architecture P is associated with a set of events E, a set of
read events (or reads) R ⊆ E, a set of write events (or writes) W ⊆ E. Furthermore, locks are
manipulated by a set of lock-acquire events L A ⊆ R and a set of lock-release events L R ⊆ W,
which are considered read events and write events respectively. The control-ﬂow graph CFGi of
process pi consists of events of the following types (where Vi = {v 1 , . . . , vni }, д ∈ G, l ∈ L,
fi : D ni → D is a function on ni arguments, and b : Vini → {True, False} is a boolean function
on ni arguments).
(1)
(2)
(3)
(4)

e
e
e
e

: v ← read д, in which case e ∈ R,
: д ← write f (v 1, . . . , vni ), in which case e ∈ W,
: acquire l, in which case e ∈ R,
: release l, in which case e ∈ W,

1:6

M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya
Vi = {v 1, . . . , v ni }

x
x
x
x

д ∈G

e : v ← read д

l ∈L

y

e∈R

e : д ← write f (v 1, . . . , v ni )
e : acquire l
e : release l

y

e∈W

y

e ∈ LA

y

e ∈ LR

e1 : b 1 (v 1, . . . , v ni )

y
..
.

x
em : bm (v 1, . . . , v ni )

z

Fig. 2. The control-flow graph CFGi is a sequential composition of these five atomic graphs.
(5) e 1 : b(v 1, . . . , vni ).
Each CFGi is a directed acyclic graph with a distinguished root node r i , such that there is a path
ri
x to every other node x of CFGi . Each node x of CFGi has either
(1) zero outgoing edges, or
(2) one outgoing edge (x, y) labeled with an event of a type listed in Item 1-4, or
(3) m ≥ 2 outgoing edges (x, y1 ), . . . , (x, ym ) labeled with events e j : b j (v 1, . . . , vni ) of Item 5, and
such that for all values of v 1, . . . , vni , we have b j (v 1, . . . , vn ) =⇒ ¬bl (v 1 , . . . , vni ) for all
j , l.In this case, we call x a branching node.
For simplicity, we require that if x is a branching node, then for each edge (x, y) in CFGi , the node
y is not branching. Indeed, such edges can be easily contracted in a preprocessing phase. Figure 2
provides a summary of the model syntax. We let Ei ⊆ E be the set of events that appear in CFGi of
process pi , and similarly Ri ⊆ R and Wi ⊆ W the sets of read and write events of pi . Additionally,
we require that Ei ∩ E j = ∅ for all i , j i.e., all Ei are pairwise disjoint, and denote by proc(e) the
process of event e. The location of an event loc(e) is the unique global variable it involves. Given
two events e, e ′ ∈ Ei for some pi , we write PS(e, e ′ ) if there is a path e
e ′ in CFGi (i.e., we write
′
′
PS(e, e ) to denote that e is ordered before e in the program structure).
We distinguish a set of initialization events W I ⊆ W with |W I | = |G| which are attributed
to process p1 , and are used to initialize all the global variables to some ﬁxed values. For every
initialization write event w I and for any event e ∈ Ei of process pi , we deﬁne that PS(w I , e)
(i.e., the initialization events occur before any event of each process). Figure 3 illustrates the above
deﬁnitions on the typical bank account example.
Model semantics. A local state of a process pi is a pair si = (x i , vali ) where x i is a node of CFGi
(i.e., the program counter) and vali is a valuation on the local variables Vi . A global state of P is a
tuple s = (val, s 1 , . . . , sk ), where val is a valuation on the global variables G and si is a local state
of process pi . An event e along an edge (x, y) of a process pi is enabled in s if si = (x, vali ) (i.e., the
program counter is on node x) and additionally,
(1) if e : acquire l, then val(l) = False, and
(2) if e : b j (v 1, . . . , vni ), then b j (vali (v 1 ), . . . , vali (vni )) = True.

Data-centric Dynamic Partial Order Reduction
Method: bool withdraw(int amount)

1
2
3
4
5
6
7
8

9
10

1:7

x1

Globals : int balance, lock l
Locals : bool success, int v
// 1. Try withdraw
success ← False
acquire(l)
v ← balance
if v − amount ≥ 0 then
balance ← v − amount
success ← True
release(l)
print(success)
// 2. Print balance
v ← balance
print(v)

e1 : acquire l

x2
x3

e2 : v ← read balance
e3 : b(v, amount)

Ei = {e 1 , . . . , e 7 }
Ri = {e 1 , e 2 , e 6 }
Wi = {e 4 , e 5 }
LiA = {e 1 }
LiR = {e 5 }

x4
e7 : ¬b(v, amount)
e
:
balance
← write f (v, amount, success)
x5
4
e5 : release l
x6
e6 : v ← read balance

x7

Fig. 3. (Left): A method withdraw executed whenever some amount is to be extracted from the balance of
a bank account.
(Right): Representation of withdraw in our concurrent model. The root node is x 1 . The program structure
orders PS(e 2 , e 4 ). We have loc(e 1 ) = loc(e 5 ) and loc(e 2 ) = loc(e 4 ) = loc(e 6 ).

In words, if e acquires a lock l, then e is enabled iﬀ l is free in s, and if x is a branching node,
then e is enabled iﬀ it respects the condition of the branch in s. Given a state s, we denote by
enabled(s) ⊆ E the set of enabled events in s, and observe that there is at most one enabled event
in each state s from each process. The execution of an enabled event e along an edge (x, y) of pi
in state s = (val, s 1 , . . . , sk ) results in a state s ′ = (val′, s 1 , . . . , si′, . . . , sk ), where si′ = (y, vali′ ). That
is, the program counter of pi has progressed to y, and the valuation functions val ′ and vali′ have
been modiﬁed according to standard semantics, as follows:
(1)
(2)
(3)
(4)

e
e
e
e

: v ← read д then vali′ (v) = val(д),
: д ← write f (v 1, . . . , vni ) then val′ (д) = f (vali (v 1 ), . . . , vali (vni )),
: acquire l then val′ (l) = True,
: release l then val ′(l) = False.
e

Moreover, val agrees with val ′ and vali agrees with vali′ on all other variables. We write s →
− s ′ to
′
denote that the execution of event e in s results in state s . Let S P be the ﬁnite set (since variables
range over a ﬁnite domain) of states of P. The semantics of P are deﬁned in terms of a transition
system A P = (S P , ∆, s 0 ), where s 0 is the initial state, and ∆ ⊆ S P × S P is the transition relation
such that
e
(s, s ′) ∈ A P iﬀ ∃e ∈ enabled(s) : s →
− s′
and either e is an initialization event, or the program counter of p1 has passed all initialization
e 1, ...e n
edges of p1 . We write s −−−−−−→ s ′ if there exists a sequence of states {s i }1≤i <n such that
e1

e2

en

s −→ s 1 −→ . . . s n−1 −−→ s ′
The initial state s 0 = (val, s 10 , . . . , sk0 ) is such that the value val(д) of each global variable д comes
from the unique initialization write event w with loc(w) = д, and for each si0 = (x i , vali ) we
have that x i = r i (i.e., the program counter of process pi points to the root node of CFGi ). For

1:8

M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya

simplicity we restrict S P to states s that are reachable from the initial state s 0 by a sequence of
e 1, ...,e n
events s 0 −−−−−−→ s. We focus our attention on state spaces S P that are acyclic.
Architecture topologies. The architecture P induces a labeled undirected communication graph
G P = (V P , E P , λ P ) where V P = {pi }i . There is an edge (pi , p j ) if processes pi , p j access a common
global variable or a common lock. The label λ(pi , p j ) is the set of all such global variables and locks.
We call P acyclic if G P does not contain cycles. The class of acyclic architectures includes, among
others, all architectures with two processes, star architectures, pipelines, tree-like and hierarchical
architectures.
Notation

Interpretation

P = (pi )ki=1

the concurrent architecture of k processes

G, V, L
E, W, R, L A ,
LR , W I
vali , val

the global, local and lock variables
the set of events, write, read, lock-acquire
lock-release and initialization events
valuations of local, global variables

enabled(s) ⊆ E

the set of enabled events in s

e 1, ...,e n

s −−−−−−−→

s′

sequence of events from s to s ′

the process, the global variable of event e
the control-ﬂow graph of process pi ,
CFGi , PS ⊆ E × E
and the program structure relation
G P = (V P , E P , λ P )
the communication graph of P
Table 1. Notation on the concurrent architecture.
proc(e), loc(e)

2.2

Traces

In this section we develop various helpful deﬁnitions on traces. Relevant notation is summarized
in Table 2.
Notation on traces. A (concrete, concurrent) trace is a sequence of events t = e 1 , . . . , e j such that
ei
for all 1 ≤ i < j, we have s i −1 −→ s i , where s i ∈ S P and s 0 is the initial state of P. In such a case, we
t
write succinctly s 0 →
− s j . We ﬁx the ﬁrst |G| events e 1 , . . . , e | G | of each trace t to be initialization
events that write the initial values to the global variables. That is, for all 1 ≤ i ≤ |G| we have
ei ∈ W, and hence every trace t starts with an initialization trace t I as a preﬁx. Given a trace t,
we denote by E(t) the set of events that appear in t, with R(t) = E(t) ∩ R the read events in t, and
with W(t) = E(t) ∩ W the write events in t, and let |t | = |E(t)| be the length of t. For an event
e ∈ E(t), we write int (e) ∈ N+ to denote the index of e in t. Given some ℓ ∈ N, we denote by t[ℓ]
the preﬁx of t up to position ℓ, and we say that t is an extension of t[ℓ]. We let enabled(t) denote
the set of enabled events in the state at the end of t, and call t maximal if enabled(t) = ∅. We
write TP for the set of all maximal traces of P. We denote by s(t) the unique state of P such that
t

s0 →
− s(t), and given an event e ∈ R(t) ∪ W(t), denote by valt (e) ∈ D the value that the unique
global variable of e has in s(t[int (e)]). We call a maximal trace t lock-free if the value of every lock
variable in s(t) is False (i.e., all locks have been released at the end of t). An event e is inevitable
in a trace t if every every lock-free maximal extension of t contains e. Given a set of events A,

Data-centric Dynamic Partial Order Reduction

1:9

we denote by t |A the projection of t on A, which is the unique subsequence of t that contains all
events of A ∩ E(t), and only those. A sequence of events t ′ is called the global projection of another
sequence t if t ′ = t |(R ∪ W).
Sequential traces. Given a process pi , a sequential trace τi is a sequence of events that correspond
to a path in CFGi , starting from the root node r i . Note that a sequential trace is only wrt CFGi , and
is not necessarily a trace of the system. The notation on traces is extended naturally to sequential
traces (e.g., E(τi ) and R(τi ) denote the events and read events of the sequential trace τi , respectively). Given k sequential traces τ1 , τ2 , . . . , τk , so that each τi is wrt pi , we denote by τ1 ∗τ2 ∗ . . . ∗τk
Ð
the (possibly empty) set of all traces t such that E(t) = 1≤i ≤k E(τi ).

Conﬂicting events, dependent events and happens-before relations. Two events e 1 , e 2 ∈
R ∪ W are said to conﬂict, written Confl(e 1 , e 2 ) if loc(e 1 ) = loc(e 2 ) and at least one is a write event.
The events are said to be in read-write conﬂict if e 1 ∈ R, e 2 ∈ W and Confl(e 1 , e 2 ). Two events
e 1 , e 2 are said to be independent [Flanagan and Godefroid 2005; Godefroid 1996] if p(e 1 ) , p(e 2 )
and
ei

(1) for each i ∈ {1, 2} and pair of states s 1 , s 2 such that s 1 −→ s 2 , we have that e 3−i ∈ enabled(s 1 )
iﬀ e 3−i ∈ enabled(s 2 ), and
e 1,e 2
e 2,e 1
(2) for any pair of states s 1 , s 2 such that e 1 , e 2 ∈ enabled(s 1 ), we have that s 1 −−−→ s 2 iﬀ s 1 −−−→ s 2 ,
and dependent otherwise. Following the standard approach in the literature, we will consider two
conﬂicting events to be always dependent [Godefroid 1997, Chapter 3] (e.g., two conﬂicting write
events are dependent, even if they write the same value). A sequence of events t induces a happensbefore relation →t ⊆ E(t) × E(t), which is the smallest transitive relation on E(t) such that
if

e 1 →t e 2

int (e 1 ) ≤ int (e 2 ) and e 1 and e 2 are dependent.

Observe that →t orders all pairwise conﬂicting events, as well as all the events of any process.
Notation

Interpretation

t, τi

a trace and a sequential trace

Confl(e 1 , e 2 )

conﬂicting events

t[ℓ], |t |

the preﬁx up to index ℓ, and length of t

E(t), W(t), R(t)

the events, write and read events of trace t

int (e), valt (e)

the index and value of event e in trace t

t |X

projection of trace t on event set X

enabled(t)

the enabled events in the state reached by t

→t

the happens-before relation on t

Ot

2.3

the observation function of t
Table 2. Notation on traces.

Discussion and Remarks

The concurrent model we consider here is minimalistic, to allow for a clear exposition of the ideas
used in our data-centric DPOR. Here we discuss some of the simpliﬁcations we have adopted to
keep the presentation simple.

1:10

M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya

Global variables and arrays. First, note that the location loc(e) of every event e ∈ R ∪ W is
taken to be ﬁxed in each CFGi . The dynamic access of a static, global data structure д based on
the value of a local variable v (e.g., accessing the element д[v] of a global array д) can be modeled
by using a diﬀerent global variable дi to encode the i-th location of д, and a sequence of branching
nodes that determine which дi should be accessed based on the value of v. Our framework can be
strengthened to allow use of global arrays directly, and our algorithms apply straightforwardly to
this richer framework. However, this would complicate the presentation, and is thus omitted in
the theoretical exposition of the paper. Arrays are handled naturally in our implementation, and
we refer to the Experiments Section 7.1 for a description.
Invisible computations. Each process pi is deterministic, and the only source of nondeterminism in the executions of the system comes from a nondeterministic scheduler that chooses an
enabled event to be executed from a given state. The model uses the functions f and b on events
e : д ← write f (v 1, . . . , v j ) and e : b(v 1, . . . , bn ) respectively to collapse deterministic invisible
computations of each process, and only consider the value that f writes on a global variable (in
addition to the side-eﬀects that f has on local the variables of process pi ). This is a standard approach in modeling concurrent systems, as interleaving invisible events does not change the set
of reachable local states of the processes.
Locks and synchronization mechanisms. We treat lock-acquire events as reads and lockrelease events as writes. In a trace t, a lock-acquire event e is considered to read the value of
the last lock-release event e ′ on the same lock l (or some initialization event Init if e is the ﬁrst
lock event on l in t). Our approach can be extended to richer communication (e.g., message passing) and synchronization primitives (e.g. semaphores, wait-notify), which are often implemented
using some low-level locking mechanism.
Maximal lock-free traces. We also assume that in every maximal trace of the system, every
lock-acquire is followed by a corresponding lock-release. Traces without this property are typically considered erroneous, and some modern programming languages even force this restriction
syntactically.
3

OBSERVATION TRACE EQUIVALENCE

In this section, we introduce the observation equivalence ∼O on traces, upon which in the later sections we develop our data-centric DPOR. We explore the relationship between the control-centric
Mazurkiewicz equivalence ∼M and the observation equivalence. In particular, we show that ∼O
reﬁnes ∼M , that is, every two traces that are equivalent under reordering of independent events
are also equivalent under observations. We conclude by showing that ∼O can be exponentially
more succinct, both in the number of processes, and the size of each process.
3.1

Mazurkiewicz and Observation Equivalence

In this section we introduce our notion of observation equivalence. We start with the classical
deﬁnition of Mazurkiewicz equivalence and then the notion of observation functions.
Mazurkiewicz trace equivalence. Two traces t 1 , t 2 ∈ TP are called Mazurkiewicz equivalent if
one can be obtained from the other by swapping adjacent, independent events. Formally, we write
∼M for the Mazurkiewicz equivalence on TP , and we have t 1 ∼M t 2 iﬀ
(1) E(t 1 ) = E(t 2 ), and

Data-centric Dynamic Partial Order Reduction

1:11

(2) for every pair of events e 1 , e 2 ∈ E(t 1 ) we have that e 1 →t1 e 2 iﬀ e 1 →t2 e 2 .
Observation functions. The concurrent model introduced in Section 2.1 follows sequential consistency [Lamport 1979], i.e., all processes observe the same order of events, and a read event of
some variable will observe the value written by the last write event to that variable in this order.
Throughout the paper, an observation function is going to be a partial function O : R →
7 W. A
trace t induces a total observation function Ot : R(t) → W(t) following the sequential consistency axioms. That is, Ot (r ) = w iﬀ
(1) int (w) < int (r ), and
(2) for all w ′ ∈ W(t) such that Confl(r , w ′) we have that int (w ′) < int (w) or int (w ′ ) > int (r ).
We say that t is compatible with an observation function O if O ⊆ Ot , and that t realizes O if
O = Ot .
Observation equivalence. We deﬁne the observation equivalence ∼O on the trace space TP as
follows. For t 1 , t 2 ∈ TP we have t 1 ∼O t 2 iﬀ E(t 1 ) = E(t 2 ) and Ot1 = Ot2 , i.e., the two observation
functions coincide.
We start with the following crucial lemma. In words, it states that if two traces agree on their
observation functions, then they also agree on the values seen by their common read events.
Lemma 3.1. Consider two traces t 1 , t 2 such that Ot1 ⊆ Ot2 . Then
• for all read events r ∈ R(t 1 ) we have that valt1 (r ) = valt2 (r ), and
• for all write events w ∈ W(t 1 ) ∩ W(t 2 ) we have that valt1 (w) = valt2 (w).
Proof. The proof is by induction on the preﬁxes of t 1 . We show inductively that for every 0 ≤
ℓ ≤ |t 1 |, for all global events e ∈ E(t 1 [ℓ]) we have that if e ∈ E(t 2 ) then valt1 (r ) = valt2 (r ). Note
that in the case where e = r is a read event, then r ∈ E(t 2 ) follows directly from Ot1 ⊆ Ot2 . The
claim is true for ℓ = 0, since in that case t 1 [ℓ] = ε and no event appears in t 1 [ℓ]. Now assume that
the claim holds for all preﬁxes t 1 [j] for 0 ≤ j ≤ ℓ, and let
e = arg

min

e ′ ∈E(t1 )\E(t1 [ℓ])

int1 (e ′ )

be the next global event in t 1 . We distinguish two cases based on the type of e.
• e = w ∈ W is a write event of the form д ← write f (v 1 , . . . , vni ), such that pi = proc(w).
Then the value of each local variable v j equals some α j = valt1 (r j ), with int1 (r j ) ≤ ℓ, and by the
induction hypothesis we have r j ∈ E(t 2 ) and valt1 (r j ) = valt2 (r j ) = α j . Since pi is deterministic,
it easily follows that if w ∈ E(t 2 ) then
valt2 (w) = f (valt1 (r 1 ), . . . , valt1 (r ni ))
= f (α 1 , . . . , α ni ) = f (valt2 (r 1 ), . . . , valt2 (r ni ))
= valt1 (w)
• e = r ∈ R is a read event, and let w = Ot1 (r ). Let pi = proc(w), and since pi is deterministic,
it easily follows from the induction hypothesis that r ∈ E(t 2 ), and moreover that valt1 (w) =
valt2 (w). Since Ot2 (r ) = w, we have that
valt2 (r ) = valt2 (w) = valt1 (w) = valt1 (r )
The desired result follows.

1:12

M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya


The following is an easy consequence of Lemma 3.1.
Lemma 3.2. Consider two traces t 1 , t 2 such that Ot1 ⊆ Ot2 and t 2 is maximal. Then (i) E(t 1 ) ⊆ E(t 2 ),
and (ii) for all events e ∈ R(t 1 ) ∪ W(t 1 ) we have that valt1 (e) = valt2 (e).
Soundness. Lemma 3.2 implies that two maximal traces which agree on their observation function
have the same observable behavior, i.e., each global event has the same value in the two traces.
Since all local states of each process can be explored by exploring maximal traces, it suﬃces to
explore all the (maximal) observation functions of P.
The Mazurkiewicz trace equivalence is control-centric, i.e., equivalent traces share the same order
between the dependent control locations of the program. In contrast, the observation trace equivalence is data-centric, as it is based on which write events are observed by the read events of each
trace. Note that two conﬂicting events are dependent, and thus must be ordered in the same way
by two Mazurkiewicz-equivalent traces. The formal relationship between the two equivalences is
established in the following theorem.
Theorem 3.3. For any two traces t 1 , t 2 ∈ TP , if t 1 ∼M t 2 then t 1 ∼O t 2 .
Proof. Consider any read event r ∈ R(t 1 ) and assume towards contradiction that Ot1 (r ) , Ot2 (r ).
Let w 1 = Ot1 (r ) and w 2 = Ot2 (r ). Since t 1 ∼M t 2 , we have that w 1 ∈ E(t 2 ) and w 2 ∈ E(t 1 ). Then
w 1 →t1 r and w 2 →t2 r , and one of the following holds.
(1) r →t1 w 2 , and since w 2 →t2 r then t 1 ,∼M t 2 , a contradiction.
(2) w 2 →t1 w 1 , and since t 1 ∼M t 2 we have that w 2 →t2 w 1 , and thus r →t2 w 1 . Since w 1 →t1 r , we have
t 1 ,∼M t 2 , a contradiction.
The desired result follows.


Mazurkiewizc-based

Observation-based

e 1′ : release l

e 1′ : release l

′
p1 e 2 : balance ← 4 p2

′
p1 e 2 : balance ← 4 p2

e1

e1

e1

e1

e2

e2

e2

e2

e4 : balance ← write f (v, amount, success)

e3

e3

e3

e3

e5 : release l

e4

e4

e4

e4

e6 : v ← read balance

e5

e5

e5

e5

e6

e6

e6

e6

x1
e1 : acquire l

x2
e2 : v ← read balance

x3
e3 : b(v, amount)

x4
x5
x6
x7

Fig. 4. Trace exploration on the system of Figure 3 with two processes, where initially balance ← 4 and
both withdrawals succeed.

Data-centric Dynamic Partial Order Reduction

1:13

Example 3.4 (Mazurkiewizc-based-based vs observation exploration.). Figure 4 illustrates the diﬀerence between the Mazurkiewicz and observation trace equivalence on the example of Figure 3.
Every execution of the system starts with an initialization trace t I that initializes the lock l to
False, and the initial value desposit = 4. Consider that p1 is executed with parameter amount = 1
and p2 is executed with parameter amount = 2, (hence both withdrawals succeed). The primed
events e 1′ , e 2′ represent the system initialization.
• (Left): The sequential trace of p1 , p2 .
• (Center): Trace exploration using the Mazurkiewicz equivalence ∼M . Solid lines represent the
happens-before relation enforced by the program structure. Dashed lines represent potential
happens-before relations between dependent events. A control-centric DPOR based on ∼M will
resolve scheduling choices by exploring all possible realizable sets of the happens-before edges.
• (Right): Trace exploration using the observation equivalence ∼O . Solid lines represent the
happens-before relation enforced by the program structure. This time, dashed lines represent
potential observation functions. Our data-centric DPOR based on ∼O will resolve scheduling
choices by exploring all possible realizable sets of the observation edges.
Both methods are guaranteed to visit all local states of each process. However, the data-centric
DPOR achieves this by exploring potentially fewer scheduling choices.
3.2

Exponential succinctness

As we have already seen in the example of Figure 1, Theorem 3.3 does not hold in the other direction, i.e., ∼O can be strictly coarser than ∼M . Here we provide two simple examples in which ∼O
is exponentially more succinct than ∼M . Traditional enumerative model checking methods of concurrent systems are based on exploring at least one trace from every partition of the Mazurkiewicz
equivalence using POR techniques that prune away equivalent traces (e.g. sleep sets [Godefroid
1996], persistent sets [Flanagan and Godefroid 2005], source sets and wakeup trees [Abdulla et al.
2014]). Such a search is optimal if it explores at most one trace from each class. Any optimal
enumerative exploration based on the observation equivalence is guaranteed by Theorem 3.3 to
examine no more traces than any enumerative exploration based on the Mazurkiewicz equivalence. The two examples show ∼O can oﬀer exponential improvements wrt two parameters: (i) the
number of processes, and (ii) the size of each process.
Example 3.5 (Two processes of large size). Consider the system P of k = 2 processes of Figure 5, and
for i ∈ {1, . . . , n}, j ∈ {1, 2}, denote by w ij (resp. r j ) the i-th write event (resp. the read event) of p j .
In any maximal trace, there are two ways to order the read events r 1, r 2 , i.e., r j occurs before r 3−j
3−j
j
for the two choices of j ∈ {1, 2}. In any such ordering, r 3−j can only observe either w n−1
or w n−1
,
j
3−j
j
whereas there are at most n +1 possible write events for r to observe (either w n or one of the w i ).

n
Hence TP /∼O has size O(n). In contrast, TP /∼M has size Ω( 2·n
n ) = Ω(2 ), as there are (2 ·n)! ways
to order the 2 · n write events of the two processes, but n! · n! orderings are invalid as they violate
the program structure. Hence, even for only two processes, the observation equivalence reduces
the number of partitions from exponential to linear.
Example 3.6 (Many processes of small size). We now turn our attention to a system P of k identical
processes p1 , . . . , pk with two events each, in Figure 6. There is only one global variable x, and each
process performs a read and then a write to x. There are O(k k ) realizable observation functions,
by choosing for each one among k read events, one among k write events it can observe. Hence
TP /∼O has size O(k k ). In contrast, the size of TP /∼M is Ω((k!)2 ). This holds as there are k! ways

1:14

M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya
Process p 1 :

Process p 2 :

1. write x

1. write x

2. write x

2. write x

...

...

n + 1. read x

n + 1. read x

Fig. 5. An architecture of two processes with n + 1 events each.
Process p 1 :

...

Process pk :

1. write x

1. write x

2. read x

2. read x

Fig. 6. An architecture of k processes with two events each.
to order the k write events, and for each such permutation there are k! ways to assign each of the
k read events to the write event that it observes. To see this second part, let w 1 , . . . , w k be any
permutation of the write events, and let r i be the read event in the same process as w i . Then r i can
be placed right after any w j with i ≤ j. Observe that TP /∼O is exponentially more succinct than
TP /∼M , as
Î
k−1
Ö
© ki=1 i · ⌈ ki ⌉
ª
Ω((k!)2 )
­
·
=
Ω
i ®® = Ω(2k ).
­
k
k
O(k )
k
i = ⌈ k2 ⌉+1
«
¬
3.3

Solution Overview

Traditional DPOR algorithms exploit the Mazurkiewicz equivalence, and use various techniques
such as persistent sets and sleep sets to explore each Mazurkiewicz class by few representative
traces. Our goal is to develop an analogous DPOR that utilizes the observation equivalence, which
by Theorem 3.3 is more succinct. In high level, our approach consists of the following steps.
(1) In Section 4 we introduce the concept of annotations. An annotation is a function from read
to write events, and serves as an intended observation function. Given an annotation, the goal
is to obtain a trace whose observation function coincides with the annotation. We restrict our
attention to a certain class of well-formed annotations, and show that although the problem
is NP-complete in general, it admits a polynomial time (in fact, cubic in the size of the trace)
solution in acyclic architectures.
(2) In Section 5 we present our data-centric DPOR. Section 5.1 introduces the notion of causal
past cones in a trace. The concept is similar to Lamport’s happens-before relation [Lamport
1978], and is used to identify past events that may causally aﬀect a current event in a trace. We
note that this concept is diﬀerent from the happens-before relation used in the Mazurkiewicz
equivalence. We use the notions of annotations and causal cones to develop our algorithm, and
prove its correctness and optimality (in Section 5.2).
(3) In Section 6 we extend our algorithm to cyclic architectures.
Table 1 and Table 2 summarize relevant notation in the proofs.

Data-centric Dynamic Partial Order Reduction
4

1:15

ANNOTATIONS

In this section we introduce the notion of annotations, which are intended constraints on the observation functions that traces discovered by our data-centric DPOR (DC-DPOR) are required to
meet.
Annotations. An annotation pair A = (A+ , A− ) is a pair of
(1) a positive annotation A+ : R →
7 W, and
(2) a negative annotation A− : R →
7 2W
such that for all read events r , if A+ (r ) = w, then we have Confl(r , w) and it is not the case
that PS(r , w). We will use annotations to guide the recursive calls of DC-DPOR towards traces
that belong to diﬀerent equivalence classes than the ones explored already, or will be explored by
other branches of the algorithm. A positive annotation A+ forces DC-DPOR to explore traces that
are compatible with A+ (or abort the search if no such trace can be generated). Since a positive
annotation is an “intended” observation function, we say that a trace t realizes A+ if Ot = A+ , in
which case A+ is called realizable. A negative annotation A− prevents DC-DPOR from exploring
traces t in which a read event observes a write event that belongs to its negative annotation set
(i.e., Ot (r ) ∈ A− (r )). In the remaining section we focus on positive annotations, and the problem
of deciding whether a positive annotation is realizable.
The value function valA+ . Given a positive annotation A+ , we deﬁne the relation <A+ ⊆ img(A+ )×
dom(A+ ) such that w <A+ r iﬀ (r , w) ∈ A+ . The positive annotation A+ is acyclic if the relation
PS∪ <A+ is a strict partial order (i.e., it contains no cycles). The value function valA+ : dom(A+ ) ∪
img(A+ ) → D of an acyclic positive annotation A+ is the unique function deﬁned inductively, as
follows.
(1) For each w ∈ img(A+ ) of the form w : д ← write f (v 1, . . . , vni ), we have valA+ (w) =
f (α 1 , . . . , α ni ), where for each α j we have
(a) α j = valA+ (r ) if there exists a read event r ∈ dom(A+ ) such that (i) r is of the form r : v j ←
read д ′ and (ii) PS(r , w) and (iii) there exists no other r ′ ∈ dom(A+ ) with PS(r , r ′) and which
satisﬁes conditions (i) and (ii).
(b) α j equals the initial value of vi otherwise.
(2) For each r ∈ dom(A+ ) we have valA+ (r ) = valA+ (A+ (r )).
Note that valA+ is well-deﬁned, as for any read event r that is used to deﬁne the value of a write
event w we have PS(r , w), and thus by the acyclicity of A+ , valA+ (r ) does not depend on valA+ (w).
Remark 1. If A+ is realizable then it is acyclic, and for any trace t that realizes A+ we have that
valt = valA+ .
Well-formed annotations and basis of annotations. A positive annotation A+ is called wellformed if the following conditions hold:
(1) A+ is acyclic.
(2) For every lock-release event e a ∈ img(A+ ) ∩ L A there is at most one lock-acquire event er ∩ L R
such that A+ (e a ) = er .
(3) There exist sequential traces (τi )i , one for each process pi , such that each τi ends in a global
event, and the following conditions hold.

1:16

M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya

(a) for every pair of lock-acquire events e a1 , e a2 ∈ E(τi ) ∩ L A such that inτi (e a1 ) < inτi (e a2 ) and
loc(e a1 ) = loc(e a2 ) there exists a lock release event er ∈ E(τi ) ∩ L R such that inτi (e a1 ) <
inτi (er ) < inτi (e a2 ) and loc(er ) = loc(e a1 ) = loc(e a2 ).
Ð
Ð
(b) i R(τi ) = dom(A+ ) and img(A+ ) ⊆ i W(τi ), i.e., (τi )i contains precisely the read events
of A+ and a superset of the write events.
(c) Each τi corresponds to a deterministic computation of process pi , where the value of every
global event e during the computation is taken to be valA+ (e).
The sequential traces (τi )i are called a basis of A+ if every τi is minimal in length. The following
lemma establishes properties of well-formedness and basis.
Lemma 4.1. Let X = dom(A+ ) ∪ img(A+ ) be the set of events that appear in a positive annotation A+ ,
and X i = X ∩ Ei the subset of events of X from process pi . The following assertions hold:
(1) If A+ is well-formed, then it has a unique basis (τi )i .
(2) ComputingÍthe basis of A+ (or concluding that A+ is not
Í well-formed) can be done in O(n) time,
where n = i (|τi |) if A+ is well-formed, otherwise n = i ℓi , where ℓi is the length of the longest
path from the root r i of CFGi to an event e ∈ X i .
(3) For every trace t that realizes A+ we have that A+ is well-formed and t ∈ τ1 ∗ . . . ∗ τk .
Proof. (1) Assume towards contradiction that A+ has two distinct bases (τi )i and (τi′ )i . Since each
sequential trace corresponds to a deterministic computation of the corresponding process using valA+ as the value function of global events, we have that each τi and τi′ share a preﬁx
relationship (i.e., one is preﬁx of the other). Since the two basis are distinct, for some j we have
that one of τ j and τ j′ is a proper preﬁx of the other. Assume w.l.o.g. that τ j′ is a strict preﬁx of τ j .
Then replacing τi with τi′ in (τi )i yields another basis, thus τi is not minimal, a contradiction.
(2) First, testing the conditions of Item 1 and Item 2 of well-formedness can be done in O(|A+ |)
time. We now outline the process of constructing the basis (τi )i . As a preprocessing step, we
compute for each process pi the unique event ei ∈ X i which is maximal wrt the program
structure PS. Note that if ei is not unique for each process, then A+ is not well-formed. This
requires O(|A+ |) time for all processes pi , simply by iterating over all events in X . Then, the
unique basis (τi )i can be constructed by executing each process locally, and using the value
function valA+ for assigning values to global events. The execution stops when ei is reached,
and the constructed sequential trace τi is returned. Finally, (τi )i constitute a basis of A+ if the
conditions (a) and (b) of Item 3 of well-formedness are met, which can be done in O(n) time.
(3) It follows easily from Remark 1 and the above construction that if t realizes A+ , then A+ must
be well-formed and t ∈ τ1 ∗ . . . ∗ τk .

4.1

The Hardness of Realizing Positive Annotations

A core step in our data-centric DPOR algorithm is constructing a trace that realizes a positive
annotation. That is, given a positive annotation A+ , the goal is to obtain a trace t (if one exists)
such that Ot = A+ , i.e., t contains precisely the read events of A+ , and every read event in t
observes the write event speciﬁed by A+ . Here, we show that the problem is NP-complete in the
general case. Membership in NP is trivial, since, given a trace t, it is straightforward to verify
that Ot = A+ in O(|t |) time. Hence our focus will be on establishing NP-hardness. For doing so,
we introduce a new graph problem, namely ACYCLIC EDGE ADDITION, which is closely related

Data-centric Dynamic Partial Order Reduction

1:17

to the problem of realizing a positive annotation under sequential consistency semantics. We ﬁrst
show that ACYCLIC EDGE ADDITION is NP-hard, and afterwards that the problem is polynomialtime reducible to realizing a positive annotation.
The problem ACYCLIC EDGE ADDITION. The input to the problem is a pair (G, H ) where
G = (V , E) is a directed acyclic graph, and H = {(x i , yi , zi )}i is a set of triplets of distinct nodes
such that
(1) x i , yi , zi ∈ V , (yi , zi ) ∈ E and (x i , yi ), (zi , x i ) < E, and
(2) each node x i and yi appears only once in H .
|
An edge addition set X = {ei }i|H
=1 for (G, H ) is a set of edges ei ∈ E such that for each ei we have
either ei = (x i , yi ) or ei = (zi , x i ). The problem ACYCLIC EDGE ADDITION asks whether there
exists an edge addition set X for (G, H ) such that the graph G X = (V , E ∪ X ) remains acyclic.

Lemma 4.2. ACYCLIC EDGE ADDITION is NP-hard.
Proof. The proof is by reduction from MONOTONE ONE-IN-THREE SAT [Garey and Johnson
1979, LO4]. In MONOTONE ONE-IN-THREE SAT, the input is a propositional 3CNF formula ϕ in
which every literal is positive, and the goal is to decide whether there exists a satisfying assignment
for ϕ that assigns exactly one literal per clause to True.
The reduction proceeds as follows. In the following, we let C and D range over the clauses and x i
over the variables of ϕ. We assume w.l.o.g. that no variable repeats in the same clause. For every
variable x i , we introduce a node w i′ ∈ V . For every clause C = (xC1 ∨xC2 ∨xC3 ), we introduce a pair
of nodes wCCj , rCCj ∈ V and an edge (wCCj , rCCj ) ∈ E, where j ∈ {1, 2, 3}. Additionally, we introduce
an edge (wCCj , wC′ l ) ∈ E for every pair j, l ∈ {1, 2, 3} such that j , l, and an edge (wC′ j , rCCl ) for each
j ∈ {1, 2, 3}, where l = (j + 1) mod 3 + 1. Finally, for every pair of clauses C, D and l 1 , l 2 ∈ {1, 2, 3}
such that Cl1 = D l2 = ℓ (i.e., C and D share the same variable x ℓ in positions l 1 and l 2 ), we add
edges (w Cℓ , r ℓD ), (w ℓD , r ℓC ) ∈ E. The set H consists of triplets of nodes (wC′ j , wCCj , rCCj ) for every clause
C and j ∈ {1, 2, 3}. Figure 7 illustrates the above construction.
Let X be an edge addition set that solves ACYCLIC EDGE ADDITION on input (G, H ) and note
that for every pair of triplets (w i′, w iC , r iC ), (w i′, w iD , r iD ) ∈ H , we have that (w i′, w iC ) ∈ X iﬀ
(w i′, w iD ) ∈ X , i.e., for every node w i′ , the set X contains either only all incoming, or only all
outgoing edges of w i′ speciﬁed by H . To see this, observe that if there exists such a pair of triplets
with (w i′, w iC ), (r iD , w i′) ∈ H , then G X = (V , E ∪ X ) would contain the cycle
w i′ → w iC → r iD → w i′
which contradicts that X is a solution to the problem. Given such an edge addition set X , we obtain
an assignment on the variables of ϕ by setting x i = True iﬀ X contains an edge (wC′ j , wCCj ) for some
clause C and j ∈ {1, 2, 3}. By the previous remark, the assignment of values to variables of ϕ is
well-deﬁned.
It is easy to verify that the construction takes polynomial time in the size of ϕ. In the following,
we argue that the answer to MONOTONE ONE-IN-THREE SAT is true iﬀ the answer to ACYCLIC
EDGE ADDITION is also true.
(⇒). Let X be a solution to ACYCLIC EDGE ADDITION on (G, H ), and we argue that every clause
C of ϕ contains exactly one variable set to True. Indeed, C contains at least one such variable,

1:18

M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya

otherwise G X would contain a cycle
rCC1 → wC′ 1 → rCC2 → wC′ 2 → rCC3 → wC′ 3 → rCC1
Similarly, C contains at most one variable of C set to True, as two such variables x i , x j would imply
that G X contains a cycle
w i′ → w iC → w j′ → w Cj → w i′
(⇐). Consider any satisfying assignment of ϕ, and construct an edge addition set X = {ei }i such
that for each triplet (w i′, w iC , r iC ) ∈ H we have

(w i′, w iC ), if x i = True
ei =
(r iC , w i′), if x i = False
Ð
Given a clause C, we denote by VC = i3=1 {wC′ i , wCCi , rCCi }, and by G X [VC ] the subgraph of G X
restricted to nodes in VC . We now argue that G X does not contain a cycle. Assume towards contradiction otherwise, and let C be such a cycle.
(1) If C contains a node of the form wCCj for some j ∈ {1, 2, 3} then C traverses the edge (wC′ j , wCCj ),
and thus x ℓ is assigned True, where ℓ = C j Since G X contains no edge of the form (r ℓD , w ℓ′ )
for any clause D, C must traverse an edge (w DDi , w ℓ′ ) for some clause D. Hence there is a ﬁrst
node w DDi traversed by C after w Cℓ , for some clause D and i ∈ {1, 2, 3} and thus G X contains
an edge (w D′ i , w DDi ), and hence x l is assigned True, where l = D i . By our choice of w DDi , the
node w D′ i can only be reached via the edge (r DDi , w D′ i ), which requires that x l is assigned False,
a contradiction.
(2) If C contains no node of the form wCCj , then it must be a cycle in G[VC ], for some clause C. The
only such cycle that traverses no wCCj can be
rCC1 → wC′ 1 → rCC2 → wC′ 2 → rCC3 → wC′ 3 → rCC1
which requires that all xCi are assigned False, for each i ∈ {1, 2, 3}, which contradicts that C
has a variable assigned True.
The desired result follows.



From ACYCLIC EDGE ADDITION to annotations. Finally, we argue that ACYCLIC EDGE ADDITION is polynomial-time reducible to realizing a positive annotation. Given an instance (G, H )
of ACYCLIC EDGE ADDITION, with G = (V , E), we construct an architecture P of k = 2 · |H |
processes (pi )i , and a positive annotation A+ . We assume, w.l.o.g., that the set of nodes V is precisely the set of nodes that appear in the triplets of H . Indeed, any other nodes can be removed
while maintaining the connectivity between the nodes in the triplets of H , and any edge addition
set X solves the problem in the original graph iﬀ it does so in the reduced graph. The construction
proceeds in two steps.
(1) For every triplet (x i , yi , zi ) ∈ H , we create two events w i ∈ W, r i ∈ R in pi such that PS(w i , r i ),
and an event w i′ in process p |H |+i . For all three events we set loc(r i ) = loc(w i ) = loc(w i′) = дi ,
where дi ∈ G is some fresh global variable of P. Finally, we introduce (r i , w i ) ∈ A+ . Given any
node u ∈ V , let e(u) denote the event associated with u.

Data-centric Dynamic Partial Order Reduction

1:19

ϕ = (x 1 ∨ x 2 ∨ x 3 ) ∧ (x 1 ∨ x 4 ∨ x 5 )
{z
}
|
{z
} |
C

w 1C

w 1′

w 2C

r 1C

r 2C

w 1D

w 4D

r 1D

r 4D

D

w 2′

w 3C

w 3′

r 3C

w 4′

w 5D

w 5′

r 5D

Fig. 7. The reduction of 3SAT over ϕ to ACYCLIC EDGE ADDITION over (G, H ). The nodes and solid edges
represent the graph G. The dashed edges represent the triplets in H .

(2) For every edge (u, v) we introduce a new global variable д ∈ G, and two events wu,v ∈ W,
ru,v ∈ R such that loc(wu,v ) = loc(ru,v ) = д. We make wu,v an event of the same process as e(u),
and ru,v an event of the same process as e(v), and additionally PS(e(u), wu,v ) and PS(ru,v , e(v)).
Finally, we introduce (ru,v , wu,v ) ∈ A+ .
Observe that the above construction is linear in the size of (G, H ). The following lemma states the
correctness of the reduction.
Lemma 4.3. The decision problem of ACYCLIC EDGE ADDITION on input (G = (V , E), H ) admits a
positive answer iﬀ the positive annotation A+ is realizable in P.
Proof. We present both directions of the proof.
• (⇒). Let t be any trace that realizes A+ . Observe that for any edge (u, v) ∈ E we have int (e(u)) <
int (e(v)), since PS(e(u), wu,v ) and PS(ru,v , e(v)) and A+ (ru,v ) = wu,v . Additionally, t satisﬁes
that either int (w i′) < w t (w i ), or int (r i ) < w t (w i′ ). In the former case we an edge (x i , yi ), and in
the latter case we add (zi , x i ) in an edge set X . Since t induces a total order on the vertices of
G, G X is acyclic, and thus X is an edge addition set for (G, H ).
• (⇐). If X is an edge addition set for (G, H ) then G X is acyclic and any topological order of the
vertices of G X = (V , E ∪ X ) induces a trace that realizes A+ .
The desired result follows.
4.2



Realizing Positive Annotations in Acyclic Architectures

We now turn our attention to a tractable fragment of the positive annotation problem. Here we
show that if P is an acyclic architecture, then the problem admits a polynomial-time solution (in
fact, cubic in the size of the constructed trace).
Intuition. The hardness of realizing positive annotations in general architectures comes from
transitivity constraints that ensure that the resulting happens-before relation is acyclic. That is,

1:20

M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya

for every triplet of events e 1 , e 2 , e 3 , deciding that (i) e 1 happens before e 2 and (ii) e 2 happens before e 3 must lead in (iii) e 1 happening before e 3 . In general architectures, such a triplet of events
is, in general, unrelated a-priori, and hence an algorithm that constructs a trace out of a positive
annotation need to make the above decisions (i)-(iii) consistently. In contrast, acyclic architectures
have the property that in every such triplet of events, a pair of them always belongs to the same
process and thus is ordered a-priori by the program structure. This allows to express transitivity
constraints by means of a 2SAT encoding. For example assume that e 2 , e 3 belong to the same process and e 2 is ordered before e 3 by the program structure. Then the transitivity constraints can be
simply encoded in a 2SAT clause (x e1,e2 ⇒ x e1,e3 ), where x e,e ′ is interpreted as a boolean variable
indicating that e happens before e ′ . Besides transitivity constraints, observe that positive annotation constraints can also be encoded in a 2SAT clause. That is, every positive annotation constraint
A+ (r ) = w can be encoded in a 2SAT clause (x w ′,r ⇒ x w ′,w ), for every write event w ′ , w that
conﬂicts with w.
Procedure Realize. Let P be an acyclic architecture, and A+ a positive annotation over P. We
describe a procedure Realize(A+ ) which returns a trace t that realizes A+ , or ⊥ if A+ is not realizable.
The procedure works in two phases. In the ﬁrst phase, Realize(A+ ) uses Lemma 4.1Ðto extract a
basis (τi )i of A+ . In the second phase, Realize(A+ ) determines whether the events of i E(τi ) can
be linearized in a trace t such that Ot = A+ . Informally, the second phase consists of constructing
Ð
a 2SAT instance over variables x e1,e2 , where e 1 , e 2 ∈ i E(τi ). Setting x e1,e2 to True corresponds to
making e 1 happen before e 2 in the witness trace t. The clauses of the 2SAT instance capture four
properties that each such ordering needs to meet, namely that
(1) the resulting assignment produces a total order (totality, antisymmetry and transitivity) between all of the events that appear in adjacent processes in the communication graph G P ,
(2) the produced total order respects the positive annotation, i.e., every write event w ′ that conﬂicts
with an annotated read/write pair (r , w) ∈ A+ must either happen before w or after r , and
(3) the produced total order respects the partial order induced by the program structure PS and
the positive annotation A+ .
The formal description of the second phase is given in Algorithm 1.
Lemma 4.4. Given a well-formed positive annotation A+ over a basis (τi )i , Realize constructs Í
a trace
t that realizes A+ (or concludes that A+ is not realizable) and requires O(n 3 ) time, where n = i |τi |.
Proof. We present the correctness proof and complexity analysis.
Correctness. We ﬁrst argue about correctness.
(1) If Realize returns a sequence of events t (Line 27) then clearly t is a trace since t respects
the program structure PS (Line 21), and by the deﬁnition of the well-formed annotation, lock
semantics are respected (i.e., critical regions protected by locks do not overlap). Additionally, t
realizes A+ , as the sequential consistency axioms are satisﬁed because of Line 18 and Line 21.
(2) If A+ is realizable by a trace t, then t is a linearization of E ∗ , thus for every pair of distinct
conﬂicting events (e 1 , e 2 ) ∈ E ∗ we have int (e 1 ) < int (e 2 ) (Line 21). By the sequential consistency
axioms, for every pair (r , w) ∈ A+ and w ′ , w with Confl(r , w ′) we have either int (w ′) < int (w)
or int (r ) < int (w ′) (Line 18). Finally, since t induces a total order on V , it is clearly transitive
(Line 10) and antisymmetric (Line 7). Hence the set of 2SAT clauses C is satisﬁable. It suﬃces
to argue that G ′ = (V ′, E ′) (Line 26) is acyclic, as then any topological order of G ′ will satisfy
the sequential consistency axioms (Line 18). Assume towards contradiction otherwise. If G ∗

Data-centric Dynamic Partial Order Reduction

1:21

Algorithm 1: Realize(A+ )
Input: A positive annotation A+ with basis (τi )i
Output: A trace t that realizes A+ or ⊥ if A+ is not realizable
1
2
3
4

5
6

7
8
9

10
11
12
13
14
15
16
17

18
19
20

21
22
23
24

25
26
27

Construct a directed graph G = (V , E) where
Ð
- V = i E(τi ), and
- E = {(e 1 , e 2 ) : (e 2 , e 1 ) ∈ A+ or PS(e 1 , e 2 )}
∗
G = (V , E ∗ ) ← the transitive closure of G
// A set C of 2SAT clauses over variables V C
C←∅
V C ← {xe1,e2 : e 1 , e 2 ∈ V and e 1 , e 2 and either proc(e 1 ) = proc(e 2 ) or (proc(e 1 ), proc(e 2 )) ∈ E P }
// 1. Antisymmetry clauses
foreach xe1,e2 ∈ V C do
C ← C ∪ {(xe1,e2 ⇒ ¬xe2,e1 ), (¬xe2,e1 ⇒ xe1,e2 )}
end
// 2. Transitivity clauses
foreach xe1,e2 ∈ V C do
foreach (e 2 , e 3 ) ∈ E ∗ do
C ← C ∪ {(xe1,e2 ⇒ xe1 ,e3 )}
end
foreach (e 3 , e 1 ) ∈ E ∗ do
C ← C ∪ {(xe1,e2 ⇒ xe3 ,e2 )}
end
end
// 3. Annotation clauses
foreach (r, w) ∈ A+ and w ′ ∈ V ∩ W s.t. Confl(r, w ′ ) do
C ← C ∪ {(xw ′,r ⇒ xw ′,w )}
end
// 4. Fact clauses
foreach (e 1 , e 2 ) ∈ E ∗ with e 1 , e 2 do
C ← C ∪ {(xe1,e2 )}
end
Compute a satisfying assignment f : V C → {False, True} |VC | of the 2SAT over C, or return ⊥ if C is
unsatisﬁable
E ′ ← E ∪ {(e 1 , e 2 ) : f (xe1,e2 ) = True}
Let G ′ = (V , E ′ )
return a trace t by topologically sorting the vertices of G ′

has a cycle, then A+ is not realizable, as t must linearize E ∗ . Hence G ∗ must be acyclic, Thus,
any cycle C in G ′ traverses an edge (e 1 , e 2 ) ∈ E ′ \ E ∗ , hence f (x e1,e2 ) = True. We distinguish
the following cases.
(a) If there exists a cycle C which traverses a single edge (e 1 , e 2 ) ∈ E ′ \ E ∗ , then there is a path
e2
e 1 traversing only edges of E ∗ . Since E ∗ is transitively closed, we have that (e 2 , e 1 ) ∈ E ∗
and hence f (x e2,e1 ) = True (Line 21). Thus, by antisymmetry, f (x e1,e2 ) = False (Line 7), a
contradiction.
(b) Otherwise, let C be a simple cycle in G ∗ that traverses the fewest number of edges in
E ′ \ E ∗ , and C must traverse at least two edges (e 1 , e 2 ), (e 3, e 4 ) ∈ E ′ \ E ∗ . Observe that

1:22

M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya
proc(e 1 ) , proc(e 2 ) and proc(e 3 ) , proc(e 4 ) as otherwise we would have (e 2 , e 1 ) ∈ E ∗
or (e 4 , e 3 ) ∈ E ∗ , and there would exist a cycle that traverses a single edge from E ′ \ E ∗
(namely, e 1 → e 2 → e 1 or e 3 → e 4 → e 3 ). Since P is acyclic, by construction (Line 6)
|{proc(e 1 ), proc(e 2 ), proc(e 3 ), proc(e 4 )}| = 2, hence, there exist two distinct processes pi , p j
such that
e 1 ∈ Ei

and

e 2 ∈ E j and e 3 , e 4 ∈ Ei ∪ E j

Observe that either (i) PS(e 4 , e 1 ) or (ii) PS(e 4 , e 2 ). We focus on case (i), as case (ii) is similar. Since PS(e 4 , e 1 ) and G ∗ is transitively closed, we have (e 4 , e 1 ) ∈ E ∗ . Additionally, since
proc(e 3 ) , proc(e 4 ) we have proc(e 3 ) = proc(e 2 ), and thus (e 2 , e 3 ) ∈ E ∗ . Since f (x e3,e4 ) = True,
by transitivity (Line 10), we have that f (x e3,e1 ) = True and thus, by transitivity again,
f (x e2,e1 ) = True. This leads to a contradiction, as (e 1 , e 2 ) ∈ E ′ \ E ∗ and thus f (x e1,e2 ) = True,
which violates the transitivity constraint (Line 10).
The desired result follows.
Complexity. The transitive closure requires O(n 3 ) time, since |V | = n. The set V C (Line 6) has O(n 2 )
variables and each of the loops for constructing clauses iterates over triplets of nodes, hence the
2SAT instance is constructed in O(n 3 ) time. Computing a satisfying assignment for C (or concluding that none exists) requires linear time in |C| [Aspvall et al. 1979], hence this step costs O(n 3 ).
Finally, constructing G ′ and computing a topological sorting of its vertices requires O(n 2 ) time in
total. The desired result follows.

The following theorem summarizes the results of this section.
Theorem 4.5. Consider any architecture P = (p)i and let A+ be any well-formed positive annotation
over a basis (τ )i . Deciding whether A+ is realizable is NP-complete. If P is acyclic, the problem can
Í
be solved in O(n 3 ) time, where n = i |τi |.
5

DATA-CENTRIC DYNAMIC PARTIAL ORDER REDUCTION

In this section we develop our data-centric DPOR algorithm called DC-DPOR and prove its correctness and compactness, namely that the algorithm explores each observation equivalence class
of TP once. We start with the notion of causal past cones, which will help in proving the properties
of our algorithm.
5.1

Causal Cones

Intuitively, the causal past cone of an event e appearing in a trace t is the set of events that precede
e in t and may be responsible for enabling e in t.
Causal cones. Given a trace t and some event e ∈ E(t), the causal past cone Pastt (e) of e in t is
the smallest set that contains the following events:
(1) if there is an event e ′ ∈ E(t) with PS(e ′, e), then e ′ ∈ Pastt (e),
(2) if e 1 ∈ Pastt (e), for every event e 2 ∈ E(t) such that PS(e 2 , e 1 ), we have that e 2 ∈ Pastt (e), and
(3) if there exists a read r ∈ Pastt (e)R, we have that Ot (r ) ∈ Pastt (e).
In words, the causal past cone of e in t is the set of events e ′ that precede e in t and may causally
aﬀect the enabling of e in t. Note that for every event e ′ ∈ Pastt (e) we have that e ′ →t e, i.e., every

Data-centric Dynamic Partial Order Reduction

1:23

event in the causal past cone of e also happens before e in t. However, the inverse is not true in
general, as e.g. for some read r we have Ot (r )→t r but possibly Ot (r ) < Pastt (r ).
Remark 2. If e ′ ∈ Pastt (e), then e ′ →t e and Pastt (e ′) ⊆ Pastt (e).
Remark 3. For every trace t and event e ∈ E(t) we have that t |(Pastt (e) ∪ e) is a valid trace.
The following lemma states the main property of causal past cones used throughout the paper.
Intuitively, if the causal past of an event e in some trace t 1 also appears in another trace t 2 , and the
read events in the causal past observe the same write events in both traces, then e is inevitable in
t 2 , i.e., every maximal extension of t 2 will contain e.
Lemma 5.1. Consider two traces t 1 , t 2 and an event e ∈ E(t 1 ) such that for every read r ∈ Pastt1 (e)
we have r ∈ E(t 2 ) and Ot1 (r ) = Ot2 (r ). Then e is inevitable in t 2 .
Proof. We argue that every event e ′ ∈ Pastt1 (e) ∪ {e} is inevitable in t 2 . Let t 2′ be any lock-free
maximal extension of t 2 . Assume towards contradiction that (Pastt1 (e) ∪ {e}) \ E(t 2′ ) , ∅, and let
em = arg

min

e ′ ∈(Pastt1 (e )∪{e })\E(t2′ )

int1 (e ′ )

be the ﬁrst such event in t 1 , and let pi = proc(em ) be the process of em . By Remark 2, for every
event e ′ ∈ Pastt1 (em ) we have e ′ ∈ Pastt1 (e), and since int1 (e ′) < int1 (em ), we have e ′ ∈ E(t 2′ ). Let
(x, y) be the edge of CFGi labeled with em . Since e ′ ∈ E(t 2′ ), the program counter of pi becomes x
at some point in t 2′ . We examine the number of outgoing edges from node x.
(1) If x has one outgoing edge, we distinguish whether em is a lock-acquire event or not.
(a) If em is not a lock-acquire event, then em is always enabled after e ′ in t 2′ , hence t 2′ is not
maximal, a contradiction.
(b) If em : acquire l, since t 2′ is a lock-free trace, l is released in s(t 2′ ), hence em ∈ enabled(t 2′ ) and
t 2′ is not maximal, a contradiction.
(2) If x has at least two outgoing edges then em is of the form em : b j (v 1 , . . . , vni ), where vi ∈ Vi
are local variables of pi . Let tem = t 2′ |Pastt1′ (em ). Since for every read r ∈ Pastt1 (e) we have
r ∈ E(t 2 ) and Ot1 (r ) = Ot2 (r ), by Remark 2, the same holds for reads r ∈ Pastt1 (em ), i.e.,
for every read r ∈ Pastt1 (em ) we have r ∈ E(t 2 ) and Ot1 (r ) = Ot2 (r ). It is easy to see that
additionally r ∈ E(tem ) and Ot1 (r ) = Otem (r ). Thus, we have Otem ⊆ Ot1 . By Lemma 3.1, we
have valtem (r ) = valt1 (r ) for every read r , and since pi is deterministic, the value of v on x is a
function of those reads, and thus each vi has the same value when the program counter of pi
reaches node x in t 1 and t 2′ . Since em appears in t 1 , em is always enabled after e ′ in t 2′ , hence t 2′
is not maximal, a contradiction.
The desired result follows.
5.2



Data-centric Dynamic Partial Order Reduction

Algorithm DC-DPOR. We now present our data-centric DPOR algorithm. The algorithm receives
as input a maximal trace t and annotation pair A = (A+, A− ), where t is compatible with A+ . The
algorithm scans t to detect conﬂicting read-write pairs of events that are not annotated, i.e, a
read event r ∈ R(t) and a write event w ∈ W(t) such that r < dom(A+ ) and ConflRW(r , w). If
w < A− (r ), then DC-DPOR will try to mutate r to w, i.e., the algorithm will push (r , w) in the

1:24

M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya

positive annotation A+ and call Realize to obtain a trace that realizes the new positive annotation.
If the recursive call succeeds, then the algorithm will push w to the negative annotation of r , i.e.,
will insert w to A− (r ). This will prevent recursive calls from pushing (r , w) into their positive annotation. Algorithm 2 provides a formal description of DC-DPOR. Initially DC-DPOR is executed on
input (t, A) where t is some arbitrary maximal trace, and A = (∅, ∅) is a pair of empty annotations.
Algorithm 2: DC-DPOR(t, A)
Input: A maximal trace t, an annotation pair A = (A+ , A− )
1

2
3

4
5
6
7
8
9
10
11

// Iterate over reads not yet mutated
foreach r ∈ E(t) \ dom(A+ ) in increasing index int (r ) do
// Find conflicting writes allowed by A−
foreach w ∈ E(t) s.t. Confl(r, w) and w < A− (r ) do
+ ← A+ ∪ {(r, w)}
Ar,w
// Attempt mutation and update A−
+ )
Let t ′ ← Realize(Ar,w
if t ′ , ⊥ then
t ′′ ← a maximal extension of t ′
A− (r ) ← A− (r ) ∪ {w }
+ , A− )
Ar,w ← (Ar,w
Call DC-DPOR(t ′′ , Ar,w )
end
end

We say that DC-DPOR explores a class of TP /∼O when it is called on some annotation input A =
(A+, A− ), where A+ is realized by some (and hence, every) trace in that class. The representative
trace is then the trace t ′ returned by Realize. The following two lemmas show the optimality of
DC-DPOR, namely that the algorithm explores every such class at most once (compactness) and
at least once (completeness). They both rely on the use of annotations, and the correctness of the
procedure Realize (Theorem 4.5). We ﬁrst state the compactness property, which follows by the
use of negative annotations.
Lemma 5.2 (Compactness). Consider any two executions of DC-DPOR on inputs (t 1 , A1 ) and (t 2 , A2 ).
Then A+1 , A+2 .
Proof. Examine the recursion tree T generated by DC-DPOR, where every node u is labeled with
the trace tu and annotation input Au = (Au+ , Au− ) given to DC-DPOR. Let x and y be the nodes that
correspond to inputs (t 1 , A1 ) and (t 1 , A2 ) respectively, and we argue that Ax , Ay . If x is an ancestor
+
of y, then when DC-DPOR was executed on input (t x , Ax ), a read r created Ar,w
in Line 3 on the
+
branch from x to the direction of y in T , with the property that r < dom(Ax ). Since the algorithm
never removes pairs (r , w) from the positive annotations, we have that (r , w) ∈ Ay , hence Ax , Ay .
A similar argument holds if y is an ancestor of x. Now consider the case that x and y do not have
an ancestor-descendant relationship. Let z be the lowest common ancestor of x and y in T , and z x
(resp. zy ) the child of z in the direction of x (resp. y). Let r x (resp. ry ) be the read on Line 3 that
generated Az+x (resp. Az+y ), i.e.,
Az+x = Az+ ∪ {(r x , w x )}

and Az+y = Az+ ∪ {(ry , wy )}

Data-centric Dynamic Partial Order Reduction

1:25

If r x = ry = r then w x , wy , thus Az+x (r ) , Az+y , and since the algorithm never removes pairs
(r , w) from positive annotations we have that Ax , Ay . Now assume that r x , ry , and w.l.o.g. that
int j (r x ) < int j (ry ). Then, before DC-DPOR(Azy ) is executed, Line 7 adds w x ∈ A− (r x ). Since the
algorithm never removes entries from the negative annotation, by Line 3, we have that (r x , w x ) <
Ay+ . In all cases we have Ax , Ay , as desired.

We now turn our attention to completeness, namely that every realizable observation function is
realized by a trace explored by DC-DPOR. The proof shows inductively that if t is a trace that
realizes an observation function O, then DC-DPOR will explore a trace ti that agrees with t on
the ﬁrst few read events. Then, Lemma 5.1 guarantees that the ﬁrst read event r on which the two
traces disagree appears in ti , and so does the write event w that r observes in O. Hence DC-DPOR
either will mutate r → w (if w < A− (r )), or it has already done so in some earlier steps of the
recursion (if w ∈ A− (r )).
Lemma 5.3 (Completeness). For every realizable observation function O, DC-DPOR generates a
trace t that realizes O.
Proof. Let T be the recursion tree of DC-DPOR. Given a node u of T , we denote by tu and Au =
(Au+, Au− ) the input of DC-DPOR on u. Since tu is always a maximal extension of a trace returned
by procedure Realize on input Au+ , by Lemma 4.4 we have that tu is compatible with Au+ , thus it
suﬃces to show that DC-DPOR is called with a positive annotation being equal to O. We deﬁne a
traversal on T with the following properties:
(1) If u is the current node of the traversal, then Au+ ⊆ O.
(2) If Au+ ⊂ O, then the traversal proceeds either
(a) to a node v of T with Au+ ⊂ Av+ ,
(b) to some other node of T ,
and Item 2b happens a ﬁnite number of times.
Observe that every time the traversal executes Item 2a, O agrees with Av+ on more reads than Au+ .
Since Item 2b is executed a ﬁnite number of times, any such traversal is guaranteed to reach a node
w with Aw = O.
The traversal starts from u being the root of T , and Item 1 holds as then Au+ = ∅ ⊆ O. Now consider
that the traversal is on any node u that satisﬁes Item 1. Since tu is a maximal extension of a trace
returned by procedure Realize on input Au+ , Lemma 4.4 guarantees that tu is a maximal trace that
realizes Au+ . Let t ∗ be a trace that realizes O, and r be the ﬁrst read of t ∗ not in Au+ , i.e.,
r = arg

min

r ′ ∈E(t ∗ )\dom(Au+ )

int ∗ (r ′)

and w = Ot ∗ (r ). Then for every r ′ ∈ Pastt ∗ (r ), we have int ∗ (r ′) < int ∗ (r ′) and thus r ′ ∈ E(tu ) and
Ot ∗ (r ′) = Otu (r ′). By Lemma 5.1, we have r ∈ E(tu ). Since int ∗ (w) < int ∗ (r ), a similar argument
yields that w ∈ E(tu ). We now distinguish two cases, based on whether w ∈ Au− (r ) or not.
(1) If w < Au− (r ), then in Line 4 the algorithm will generate a trace t ′ that is compatible with
the strengthened annotation Au+ ∪ (r , w), and call itself recursively on some child v of u with
Av+ = Au+ ∪ (r , w). The traversal proceeds to v and Item 1 holds, as desired.
(2) If w ∈ Au− (r ), then there exists a highest ancestor x of u in T where DC-DPOR was called
with (r , w) ∈ A−x . Following Line 7, this can only have happened if x has a sibling v in T with
(r , w) ∈ Av+ . Let z be the parent of x, v, and we have Az+ ⊂ Au+ ⊂ O, and Av+ = Az+ ∪ (r , w) ⊆ O.

1:26

M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya

Thus, the traversal proceeds to v and Item1 holds, as desired. In this case, we say that the
traversal backtracks to x through z.
Finally, we argue that Item 2b will only occur a ﬁnite number of times in the traversal. Since T is
ﬁnite, it suﬃces to argue that the traversal backtracks through any node z a ﬁnite number of times.
Indeed, ﬁx such a node z and let x 1 , x 2 , . . . be the sequence of (not necessarily distinct) children
of z that the traversal backtracks to, through z. Let r i be the unique read in dom(A+x i ) \ dom(Az+ ).
By Line 1, we have that intz (r i +1) < intz (r i ), hence no node repeats in the sequence (x i )i , and thus
the traversal backtracks through z a ﬁnite number of times. The desired result follows.

We thus arrive to the following theorem.
Theorem 5.4. Consider a concurrent acyclic architecture P of processes on an acyclic state space, and
n = maxt ∈TP |t | the maximum length of a trace of P. The algorithm DC-DPOR explores each class
of TP /∼O exactly once, and requires O |TP /∼O | · n 5 time.
Proof. Lemma 5.2 and Lemma 5.3 guarantee the optimality of DC-DPOR, i.e., that DC-DPOR
explores each class of TP /∼O exactly once. The time spent in each class is the time for attempting
all possible mutations on the witness trace t which is the trace used by the algorithm to explore
the corresponding observation function. There are at most n 2 such mutations, and according to
Theorem 4.5, each such mutation requires O(n 3 ) time to be applied (or conclude that t cannot be
mutated in the attempted way). The desired result follows.

We note that our main goal is to explore the exponentially large TP /∼O by spending polynomial
time in each class. The n 5 factor in the bound comes from a crude complexity analysis.
6

BEYOND ACYCLIC ARCHITECTURES

In the current section we turn our attention to cyclic architectures. Recall that according to Theorem 4.5, procedure Realize is guaranteed to ﬁnd a trace that realizes a positive annotation A+ ,
provided that the underlying architecture is acyclic. Here we show that the trace space of cyclic
architectures can be partitioned wrt an equivalence that is ﬁner than the observation equivalence,
but remains (possibly exponentially) coarser than the Mazurkiewicz equivalence. The current section makes a formal treatment of cyclic architectures with the aim to prove that exponentially
coarser equivalences can be used to guide the search. We refer to our implementation in Section 6
for a description of how cyclic architectures are handled in practice.
Intuition. Recall that the architecture of the concurrent system is an acyclic graph, where nodes
represent the processes of the system, and two nodes are connected by an edge if the respective
processes communicate over a common shared variable. In high level, our approach for handling
cyclic architectures consists of the following steps.
(1) We choose a set of edges X such that removing all edges in X makes the architecture acyclic.
Such a choice can be made arbitrarily.
(2) For every variable that is used by at least two processes which have an edge in X , we introduce
a fresh lock in the system.
(3) We transform the concurrent program so that every write event to every such variable is protected by its respective lock.

Data-centric Dynamic Partial Order Reduction

1:27

Intuitively, the new locks have the eﬀect that when calling the procedure Realize for realizing a
positive annotation A+ , all write events protected by these locks are totally ordered by A+ (via
the lock-acquire and lock-release events). Hence, Realize needs only to resolve orderings between
read/write events to variables that (by the choice of X ) create no cycles in the communication
graph.
Architecture acyclic reduction. Consider a cyclic architecture P, and the corresponding communication graph G P = (V P , E P , λ P ). We call a set of edges X ⊆ E P an all-but-two cycle set of
G P if every cycle of G P contains at most two edges outside of X . Given an all-but-two cycle set,
X ⊆ E P we construct a second architecture P X , called the acyclic reduction of P over X , by means
of the following process.
Ð
(1) Let Y = (pi ,p j )∈X λ P (pi , p j ) be the set of variables that appear in edges of the set X . We
introduce a set of new locks L O in P X such that we have exactly one new lock lд ∈ L O for
each variable д ∈ Y .
(2) For every process pi , every write event w ∈ Wi with loc(w) ∈ Y is surrounded by an acquire/release pair on the new lock variable l loc(w ) .
Observation equivalence reﬁned by an edge set. Consider a cyclic architecture P and X an
edge set of the underlying communication graph G P . We deﬁne a new equivalence on the trace
space TP as follows. Two traces t 1 , t 2 ∈ TP are observationally equivalent reﬁned by X , denoted by
∼XO , if the following hold:
(1) t 1 ∼O t 2 , and
(2) for every edge (pi , p j ) ∈ X , for every pair of distinct write events w 1 , w 2 ∈ W(t 1 ) ∩ (Wi ∪ Wj )
with loc(w 1 ) = loc(w 2 ) = д and д ∈ λ P (pi , p j ), we have that int1 (w 1 ) < int1 (w 2 ) iﬀ int2 (w 1 ) <
int2 (w 2 )
Clearly, ∼XO reﬁnes the observation equivalence ∼O . The following lemma captures that the
Mazurkiewicz equivalence reﬁnes the observation equivalence reﬁned by an edge set X .
Lemma 6.1. For any two traces t 1 , t 2 ∈ TP , if t 1 ∼M t 2 then t 1 ∼XO t 2 .
Proof. By Theorem 4.5, we have t 1 ∼O t 2 . Consider any pair of distinct write events w 1 , w 2 ∈
W(t 1 ) ∩ (Wi ∪ Wj ) with loc(w 1 ) = loc(w 2 ) = д and д ∈ λ P (pi , p j ), and observe that w 1 and w 2
are dependent. Hence, we have w 1 →t1 w 2 iﬀ w 1 →t2 w 2 , and thus int1 (w 1 ) < int1 (w 2 ) iﬀ int2 (w 1 ) <
int2 (w 2 ), as desired.

Exponential succinctness of ∼XO in cyclic architectures. Here we present a very simple cyclic
architecture where the observation equivalence ∼XO reﬁned by an all-but-two cycle set X is exponentially more succinct than the Mazurkiewicz equivalence ∼M . Consider the architecture P in
Figure 8, which consists of three processes and two single global variables x and y. We choose
an edge set as X = {(p1 , p2 )}, and X is an all-but-two cycle set of G P . We argue that ∼XO is exponentially more succinct than ∼M by showing exponentially many traces which are pairwise
equivalence under ∼XO but not under ∼M . Indeed, consider the set T which consists of all traces
such that the following hold
(1) All traces start with p1 executing to completion, then p2 executing its ﬁrst statement, and p3
executing its ﬁrst statement.
(2) All traces end with the last three events of p2 followed by the last two events of p3 .

1:28

M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya
Process p 1 :

Process p 2 :

Process p 3 :

1. write x

1. write x

1. write x

2. read x

2. write y

2. write y

...

...

n + 2. write y

n + 2. write y

n + 3. read y

n + 3. read y

n + 4. read x

n + 4. read x

Fig. 8. A cyclic architecture of three processes.

Note that |T | = 2·n
n as there are (2 · n)! ways to order the 2 · n write y events of the two processes,
but n! · n! orderings are invalid as they violate the program structure. All traces in T have the
same observation function, yet they are inequivalent under ∼M since every pair of them orders
two write y events diﬀerently. Finally, TP /∼XO is only exponentially large, and since
|(TP /∼M ) \ (TP /∼xO )| ≥ |T | − 1
we have that ∼XO is exponentially more succinct than ∼M .
Data-centric DPOR on a cyclic architecture. We are now ready to outline the steps of the datacentric DPOR algorithm on a cyclic architecture P, called DC-DPOR-Cyclic. First, we determine an
all-but-two cycle set X of the underlying communication graph G P = (V P , E P , λ P ), and construct
the acyclic reduction P X of P over X . The set X can be chosen arbitrarily, e.g. by letting |X | =
|E P | − 2 (i.e., adding in X all the edges of G P except for two). Then, we execute DC-DPOR on P X ,
with the following two modiﬁcations on the procedure Realize.
(1) Consider the graph G = (V , E) constructed in Line 1 of Realize (Algorithm 1). For every pair
of write events w, w ′ protected by some of the new locks ℓ ∈ L O , for every read event r such
that A+ (r ) = w, if (w, w ′) ∈ E then we add an edge (r , w) in E, and if (w ′, r ) ∈ E, then we add
an edge (w ′, w) in E.
(2) If at the end of Item 1 G has a cycle, Realize returns ⊥.
(3) In Line 6 we use the edge set E P X \X . Hence for every variable x e1,e2 used in the 2SAT reduction,
we have either proc(e 1 ) = proc(e 2 ) or (proc(e 1 ), proc(e 2 )) ∈ E P X \ X .
Lemma 6.2. Given a well-formed positive annotation A+ over a basis (τi )i , and the modiﬁed communication graph G ′P X = (V P X , E P X \X , λ P X ), Realize constructs a trace t that realizes A+ (or concludes
Í
that A+ is not realizable) and requires O(n 3 ) time, where n = i |τi |.
(Sketch). First, note that due to the new locks L O , A+ already induces a total order on the lockacquire and lock-release events that access the same lock lд ∈ L O . Hence A+ already induces a
total order between the write events that are protected by the same lock lд ∈ L O . Thus, given the
basis (τi )i , A+ is realizable iﬀ that total order respects A+ , and there is a way to order the remaining
pairwise dependent events between pairs of processes (pi , p j ) < X , such that the ordering respects
the sequential consistency axioms. The crucial property is that since X is an all-but-two cycle
set of G P , the transitivity (Line 10) and antisymmetry (Line 7) clauses ensure that a satisfying
assignment preserves acyclicity of the graph G ′ constructed in Line 26. The complexity analysis
is similar to Lemma 4.4.


Data-centric Dynamic Partial Order Reduction

1:29

We arrive at the following theorem.
Theorem 6.3. Consider a concurrent architecture P of processes on an acyclic state space, and
n = maxt ∈TP |t | the maximum length of a trace of P. Let X be an all-but-two cycle set of the communication graph G P . The algorithm DC-DPOR-Cyclic explores each class of TP /∼XO exactly once, and

requires O |TP /∼XO | · n 5 time.
Proof of Theorem 6.3. We argue that DC-DPOR-Cyclic is then optimal for the cyclic architecture
P wrt the equivalence ∼XO .
(1) (Compactness). For any two distinct positive annotations A+1 , A+2 examined by DC-DPOR when
exploring the trace space of P X , Lemma 5.2 guarantees that A+1 , A+2 . Let t 1 and t 2 be the traces
returned by Realize on inputs A+1 and A+2 respectively. Assume that t 1 is not a preﬁx of t 2 (the
argument is similar if t 2 is not a preﬁx of t 1 , and since A+1 , A+2 , it is not the case that each is a
preﬁx of the other). This implies that at least one of the following holds.
(a) There is a read event r ∈ E(t 1 ) such that (r , Ot1 (r )) < Ot2 , in which case two diﬀerent
classes of ∼O are explored. Since ∼XO reﬁnes ∼O it follows that two diﬀerent classes of ∼ OX
are explored.
(b) There is a lock-acquire event e a ∈ E(t 1 ) such that (e a , Ot1 (e a )) < Ot2 . In this case, the write
event w protected by the lock-acquire event e a either does not appear t 2 or there exists a
conﬂicting write event w ′ in t 1 such that t 1 and t 2 are ordered diﬀerently in t 1 and t 2 . Hence
the two annotations A+1 and A+2 are used to explore diﬀerent classes of ∼XO .
(2) (Completeness). Lemma 6.2 together with the completeness statement of Lemma 5.3 guarantees
that for every observation function O of the trace space of P X , there is an annotation function
A+ used by DC-DPOR such that O = A+ . Since the lock-acquire and lock-release events are
read and write events respectively, any two traces which have a diﬀerent order on a pair of
write events w, w ′ such that w and w ′ are protected by observable locks, will also be explored.
Finally, the maximum size of a trace in P is asymptotically equal to the maximum size of a trace
in P X , from which the complexity bound follows.

Theorem 6.3 establishes that for cyclic architectures, DC-DPOR-Cyclic explores a partitioning of
the trace space that is coarser than the Mazurkiewicz partitioning, and spends only polynomial
time per class. We refer to our implementation in Section 6 for a description of how cyclic architectures are handled in practice.
7

EXPERIMENTS

Here we report on the implementation and experimental evaluation of our data-centric DPOR
algorithm.
7.1

Implementation Details

Implementation. We have implemented our data-centric DPOR in C++, by extending the tool
Nidhugg1 . Nidhugg is a powerful tool that utilizes the LLVM compiler infrastructure, and hence
our treatment of programs is in the level of LLVM’s intermediate representation (IR). Concurrent
architectures are supported via POSIX threads.
1 https://github.com/nidhugg/nidhugg

1:30

M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya
p1

p2

p4

p3

p1

→

p3

p2

p4

Fig. 9. Converting a cyclic architecture to a star architecture which is acyclic. On the star, solid edges correspond to observation equivalence interleavings, and dashed edges correspond to Mazurkiewicz equivalence
interleavings.
Handling static arrays. The challenge in handling arrays (and other data structures) lies in the
diﬃculty of determining whether two global events access the same location of the array (and thus
are in conﬂict) or not. Indeed, this is not evident from the CFG of each process, but depends on
the values of indexing variables (e.g. the value of local variable i in an access to table[i]). DPOR
methods oﬀer increased precision, as during the exploration of the trace space, backtracking points
are computed dynamically, given a trace, where the value of indexing variables is known. In our
case, the value of indexing variables is also needed when procedure Realize is invoked to construct
a trace which realizes a positive annotation A+ . Observe that the values of all such variables are
determined by the value function valA+ , and thus in every sequential trace τi of the basis (τi )i of
A+ these values are also known. Hence, arrays are handled naturally by the dynamic ﬂavor of the
exploration.
Handling cyclic architectures. In order to eﬀectively handle cyclic architectures, we followed
the following process. Wlog, we considered that the input architecture always has the most diﬃcult topology, namely it is a clique. First, the cyclic architecture is converted to a star architecture,
by choosing some distinguished process p1 as the root of the star, and the remaining processes
p2 , . . . pk are the leaves. Recall that a a positive annotation yields a sequential trace for each process. We use the Mazurkiewicz equivalence to generate all possible Mazurkiewicz-based interleavings between traces of the leaf processes, and our observation equivalence to generate all possible
observation-based interleavings between the root and every leaf process. Hence the observation
equivalence is wrt the star sub-architecture, which is acyclic, and thus our techniques from Theorem 5.4 are applicable. We note that since the Mazurkiewicz interleavings always have to be generated among sequential traces (i.e., straight-line programs), we are generating them optimally (i.e.,
obtaining exactly one trace per Mazurkiewicz class) easily, using vector clocks [Mattern 1989]. See
Figure 9 for an illustration.
Optimizations. Since our focus is on demonstrating a new, data-centric principle of DPOR, we focused on a basic implementation and avoided engineering optimizations. We outline two straightforward algorithmic optimizations which were simple and useful.
(1) (Burst mutations). Instead of performing one mutation at a time, the algorithm performs a
sequence of several mutations at once. In particular, given a trace t, any time we want to add
a pair (r , w) to the positive annotation, we also add (r ′, Ot (r ′)), where r ′ ∈ Pastt (r ) ∪ Pastt (w)
ranges over all read events in the causal past of r and w in t. This makes the recursion tree
shallower, as now we do not need to apply any mutation (r , w), where w = Ot (r ), individually.
(2) (Cycle detection). As a preprocessing step, before executing procedure Realize on some positive
annotation A+ input, we test whether the graph G (in Line 1) already contains a cycle. The
existence of a cycle is a proof that A+ is not realizable, and requires linear instead of cubic time,
as the graph is sparse.

Data-centric Dynamic Partial Order Reduction
7.2

1:31

Experimental Results

We now turn our attention to the experimental results. Our comparison is with the Source-DPOR
algorithm from [Abdulla et al. 2014] and the tool Nidhugg that implements it [Abdulla et al. 2015].
To our knowledge, Source-DPOR is the latest and state-of-the-art DPOR which has implemented
for C programs.

Experimental setup. In our experiments, we have compared our data-centric DPOR, with the
Mazurkiewicz-based Source-DPOR introduced recently in [Abdulla et al. 2014] as an important
improvement over the traditional DPOR [Flanagan and Godefroid 2005]. Our benchmark set consists of synthetic benchmarks, as well as benchmarks obtained from the TACAS Competition on
Software Veriﬁcation (SV-COMP). Most of the benchmarks have tunable size, by specifying a loopunroll bound, or the number of threads running in parallel. In all cases, we compared th running
time and number of traces explored by DC-DPOR and Source-DPOR. We have set a timeout of 1
hour. All benchmarks were executed on an Ubuntu-based virtual machine, given 4GB of memory
and one 2GHz CPU.

Two synthetic benchmarks. First we analyze the two synthetic benchmarks lastzero and
opt_lock found in Table 3a and Table 3b, respectively. The benchmark lastzero was introduced
in [Abdulla et al. 2014] to demonstrate the superiority of Source-DPOR over the traditional DPOR
from [Flanagan and Godefroid 2005]. It consists of n threads writing to an array, and 1 thread
reading from it. We observe that our DC-DPOR explores exponentially fewer traces than SourceDPOR. In fact, the number of traces explored by our data-centric approach scales polynomially,
whereas the number explored by the Mazurkiewicz-based approach grows exponentially with the
number of threads. Consequently, our DC-DPOR runs much faster, and manages to scale on larger
input sizes. We note that the number of traces explored from Source-DPOR diﬀers from the number reported in [Abdulla et al. 2014]. This is natural as the implementation of [Abdulla et al. 2014]
handles programs written in Erlang, a functional language with concurrency mechanisms much
diﬀerent from C.

The benchmark opt_lock mimics an optimistic locking scheme of 2 threads. Each thread tries to
update some variable, and afterwards checks if it was interrupted. If not, it terminates, otherwise it
tries again, up to a total n number of attempts. Again, we see that the number of explored traces by
DC-DPOR grows polynomially, whereas the number explored by Source-DPOR grows exponentially. Hence, our algorithm manages to handle much larger input sizes than the Mazurkiewiczbased Source-DPOR. Recall that, as Theorem 5.4 states, this exponential reduction in the explored
traces comes with polynomial-time guarantees per trace.

1:32
Benchmark
lastzero(4)
lastzero(5)
lastzero(6)
lastzero(7)
lastzero(8)
lastzero(9)
lastzero(10)

M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya
Traces
Time (s)
DC-DPOR S-DPOR DC-DPOR S-DPOR
38
113
316
937
3,151
12,190
52,841

2,118
53,172
1,765,876
-

0.21
0.34
0.63
1.8
9.32
47.97
383.12

0.84
19.29
856
-

(a) Experiments on lastzero(n), for n + 1 threads. ’-’
indicates a timeout after 1 hour.

Benchmark
opt_lock(12)
opt_lock(13)
opt_lock(14)
opt_lock(15)
opt_lock(50)
opt_lock(100)
opt_lock(200)

Traces
Time (s)
DC-DPOR S-DPOR DC-DPOR S-DPOR
141
153
165
177
597
1,197
2,397

785,674
2,056,918
5,385,078
-

0.35
0.36
0.43
0.46
5.91
43.82
450.99

252.64
703.90
1,880.12
-

(b) Experiments on opt_lock(n), where n is the number of attempts to optimistically lock. ’-’ indicates
a timeout after 1 hour.

Table 3. Experimental results on two synthetic benchmarks.

lastzero(n): n + 1 processes

opt_lock(n): 2 processes and n attempts

Globals : int array[n + 1]

Globals : int last_id, x

4

// --------- Process j = 0 --------Locals : int i
i ←n
while array[i] , 0 do
i ←i −1
end

5

// --------- Process 1 < j ≤ n --------array[j] ← array[j − 1] + 1

// --------- Process 0 < j < 2 --------Locals : int i
i←0
while i < n do
i ←i +1
last_id ← j
x ← get_message(j)
if last_id = j then
return x
end
return-1

1
2
3

1
2
3
4
5
6
7
8
9

Benchmarks from SV-COMP. We now turn our attention to benchmarks from SV-COMP,
namely ﬁb_bench, pthread_demo, sigma_false and parker, which are found in Table 4a, Table 4b,
Table 4c and Table 4d, respectively. Similarly to our ﬁndings on the synthetic benchmarks, the datacentric DC-DPOR manages to explore fewer traces than the Mazurkiewicz-based Source-DPOR.
In almost all cases, our algorithm run much faster, oﬀering exponential gains in terms of time.
One exception is the benchmark parker, where our DC-DPOR is slower. Although the number of
traces explored is less than that of Source-DPOR, the latter method managed to spend less time in
discovering each trace, which led to a smaller overall time. We note, however, that the improvement of Source-DPOR over DC-DPOR appears to grow only as a small polynomial wrt the input
size. Recall that new traces are discovered by DC-DPOR using the procedure Realize, which can
take cubic time in the worst case (Theorem 4.5). Hence, we identify optimizations to Realize as an
important challenge that will contribute further to the scalability of our approach.
8

RELATED WORK

The analysis of concurrent programs is a major challenge in program analysis and veriﬁcation, and has been a subject of extensive study [Cadiou and Lévy 1973; Clarke et al. 1986;
Farzan and Kincaid 2012; Farzan and Madhusudan 2009; Lal and Reps 2009; Lipton 1975; Petri

Data-centric Dynamic Partial Order Reduction
Benchmark

Traces
Time (s)
DC-DPOR S-DPOR DC-DPOR S-DPOR

ﬁb_bench(4)
ﬁb_bench(5)
ﬁb_bench(6)

1,233
8,897
70,765

19,605
218,243
2,364,418

0.93
7.41
85.71

3.03
37.82
463.52

1:33
Benchmark
pthread_demo(8)
pthread_demo(10)
pthread_demo(12)

Traces
Time (s)
DC-DPOR S-DPOR DC-DPOR S-DPOR
256
1,024
4,096

12,870
184,756
2,704,156

0.37
1.23
5.30

3.17
49.51
884.99

(a) Experiments on fib_bench(n), where n is the loop- (b) Experiments on pthread_demo(n), where n is the
unroll bound.
loop-unroll bound.
Benchmark
sigma_false(6)
sigma_false(7)
sigma_false(8)
sigma_false(9)
sigma_false(10)

Traces
Time (s)
DC-DPOR S-DPOR DC-DPOR S-DPOR
16
22
29
37
46

10,395
135,135
2,027,025
-

0.22
0.26
0.28
0.38
0.44

2.57
38.41
658.27
-

(c) Experiments on sigma_false(n), where n is the
loop-unroll bound. ’-’ indicates a timeout after 1 hour.

Benchmark
parker(8)
parker(10)
parker(12)
parker(14)
parker(16)

Traces
Time (s)
DC-DPOR S-DPOR DC-DPOR S-DPOR
1,254
2,411
4,132
6,529
9,714

3,343
6,212
10,361
16,022
23,427

1.52
5.03
8.09
11.96
19.89

1.33
3.96
5.62
6.86
10.85

(d) Experiments on parker(n), where n is the loopunroll bound.

Table 4. Experimental results on four benchmarks from SV-COMP.

1962]. The hardness of reproducing bugs by testing, due to scheduling non-determinism, makes
model checking a very relevant approach [Alglave et al. 2013; Andrews et al. 2004; Clarke et al.
1999a; Godefroid 2005; Musuvathi and Qadeer 2007], and in particular stateless model checking
to combat the state-space explosion. To combat the exponential number of interleaving explosion
faced by the early model checking [Godefroid 1997], several reduction techniques have been proposed such as POR and context bounding [Musuvathi and Qadeer 2007; Peled 1993]. Several POR
methods, based on persistent set [Clarke et al. 1999b,b; Godefroid 1996; Valmari 1991] and sleep set
techniques [Godefroid 1997], have been explored. DPOR [Flanagan and Godefroid 2005] presents
on-the-ﬂy construction of persistent sets, and several variants and improvements have been considered [Lauterburg et al. 2010; Saarikivi et al. 2012; Sen and Agha 2006, 2007; Tasharoﬁ et al. 2012].
In [Abdulla et al. 2014], source sets and wakeup trees techniques were developed to make DPOR
optimal, in the sense that the enumerative procedures explores exactly one representative from
each Mazurkiewicz class. Other important works include normal form representation of concurrent executions [Kahlon et al. 2009] using SAT or SMT-solvers; or using unfoldings for optimal reduction in number of interleavings [Kähkönen et al. 2012; McMillan 1995; Rodríguez et al.
2015]. Techniques for transition-based POR for message passing programs have also been considered [Godefroid 1996; Godefroid et al. 1995; Katz and Peled 1992], and some works extend POR to
relaxed memory models [Abdulla et al. 2015; Wang et al. 2008].
Another direction of DPOR is SAT/SMT-based, such as Maximal Causality Reduction
(MCR) [Huang 2015], and SATCheck [Demsky and Lam 2015]. Such techniques require an NP oracle to guide each step of the search (i.e., a SAT/SMT solver), and thus suﬀer scalability issues. On
the other hand, they have the possibility of exploring fewer traces than the traditional DPOR methods. Among these works, MCR [Huang 2015] is closer to ours, hence we make a more extensive
reference to it.
Comparison with [Huang 2015]. Maximal Causality Reduction is a form of partial-order reduction that is based on coarsening the Mazurkiewicz equivalence. The main principle is to try and
explore traces in which read events observe diﬀerent values (as opposed to diﬀerent write events

1:34

M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya

as in our case). As a result, MCR can potentially create an equivalence that is coarser than the observation equivalence that we introduce here. However, the MCR approach is very diﬀerent from
ours, in the following three important aspects.
(1) MCR uses an SMT solver to explore each class of the partitioning. In other words, the MCR
relies on an NP-oracle, which has exponential worst-case complexity, even for exploring a
single class of the partitioning. In contrast, our approach spends provably polynomial time per
class. We also note that the experimental results of [Huang 2015, Page 9] identify the SMT
procedure as the bottleneck of the whole approach, and ask for an eﬃcient method for each
explored trace.
(2) MCR is not optimal wrt to its partitioning. In fact, many equivalence classes of the partitioning
can be explored exponentially many times. We provide here a minimal example. Consider the
program depicted in Figure 10a. We have two processes p1 , p2 , and two global variables x, y.
The ﬁrst processes is p1 = wy1 r x1 , and the second process is p2 = w x2 ry2 . Additionally, we let w x0
and wy0 denote the two initialization write events.

Process p2 :

Process p1 :
1. write y

1. write x

2. read x

2. read y

r x1 → w x2
ry2 → wy1

a

c

b

r x1 → w x2
e

d
(a)

ry2 → wy1

(b)

Fig. 10. A simple concurrent system of two processes, and the corresponding MCR exploration.

We now consider the MCR exploration of the above system.
(a) Initially, the process starts in node a with an empty seed interleaving. The process will
generate two seed interleavings {b, c}, forcing r x1 to observe the value of w x2 , and ry2 to observe
the value of wy1 , respectively.
(b) When in b, the process will create the seed interleaving {d }, forcing ry2 to observe the value
of wy1 .
(c) When in c, the process will create the seed interleaving {e}, forcing r x1 to observe the value
of w x2 .
Hence, all traces represented in the leaves {d, e} of the above tree have the same observation
function (and thus all reads observe the same values). In contract, the optimality of our algorithm guarantees that the exploration will never explore both d and e.
The example can easily be generalized to one where the MCR will explore the same class exponentially many times. The only principle necessary to make the example work is that diﬀerent
branches of the recursion can accumulate the same read-to-write observations in diﬀerent order, leading to the same read-to-write observations overall.
Hence, compared to our approach, MCR suﬀers an exponentiation in complexity in two parts:
(i) visiting each class of the partitioning exponentially many times, and (ii) using an NP-oracle
with exponential worst-case behavior for each visit.

Data-centric Dynamic Partial Order Reduction
9

1:35

CONCLUSIONS

We introduce the new observation equivalence on traces that reﬁnes the Mazurkiewicz equivalence and can even be exponentially more succinct. We develop an optimal, data-centric DPOR
algorithm for acyclic architectures based on this new equivalence, and also extend a ﬁner version
of it to cyclic architectures. There are several future directions based on the current work. First, it
is interesting to determine whether other, coarser equivalence classes can be developed for cyclic
architectures, which can be used by some enumerative exploration of the trace space. Another
promising direction is phrasing our observation equivalence on other memory models and developing DPOR algorithms for such models. Finally, it would be interesting to explore the engineering
challenges in applying our approach to real-life examples, such as using static analysis to obtain
the best way for transforming cyclic architectures to acyclic.
ACKNOWLEDGMENTS
The research was partly supported by Austrian Science Fund (FWF) Grant No P23499- N23, FWF
NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), and Czech
Science Foundation grant GBP202/12/G061.
REFERENCES
Parosh Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. 2014. Optimal Dynamic Partial Order Reduction
(POPL).
Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas.
2015. Stateless Model Checking for TSO and PSO. In TACAS.
Jade Alglave, Daniel Kroening, and Michael Tautschnig. 2013. Partial Orders for Eﬃcient Bounded Model Checking of
Concurrent Software. In CAV.
Tony Andrews, Shaz Qadeer, Sriram K. Rajamani, Jakob Rehof, and Yichen Xie. 2004. Zing: A Model Checker for Concurrent
Software. In CAV.
Bengt Aspvall, Michael F. Plass, and Robert Endre Tarjan. 1979. A linear-time algorithm for testing the truth of certain
quantiﬁed boolean formulas. IPL 8, 3 (1979), 121 – 123.
Jean-Marie Cadiou and Jean-Jacques Lévy. 1973. Mechanizable proofs about parallel processes. In SWAT.
E.M. Clarke, O. Grumberg, M. Minea, and D. Peled. 1999b. State space reduction using partial order techniques. STTT 2, 3
(1999), 279–287.
E. M. Clarke, E. A. Emerson, and A. P. Sistla. 1986. Automatic Veriﬁcation of Finite-state Concurrent Systems Using
Temporal Logic Speciﬁcations. ACM Trans. Program. Lang. Syst. 8, 2 (1986).
Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. 1999a. Model Checking. MIT Press, Cambridge, MA, USA.
Brian Demsky and Patrick Lam. 2015. SATCheck: SAT-directed Stateless Model Checking for SC and TSO. In Proceedings of
the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications
(OOPSLA 2015). ACM, New York, NY, USA, 20–36. https://doi.org/10.1145/2814270.2814297
Azadeh Farzan and Zachary Kincaid. 2012. Veriﬁcation of parameterized concurrent programs by modular reasoning about
data and control. In CAV.
Azadeh Farzan and P. Madhusudan. 2009. The Complexity of Predicting Atomicity Violations. In TACAS.
Cormac Flanagan and Patrice Godefroid. 2005. Dynamic Partial-order Reduction for Model Checking Software. In POPL.
Michael R. Garey and David S. Johnson. 1979. Computers and Intractability: A Guide to the Theory of NP-Completeness. W.
H. Freeman & Co., New York, NY, USA.
P. Godefroid. 1996. Partial-Order Methods for the Veriﬁcation of Concurrent Systems: An Approach to the State-Explosion
Problem. Springer-Verlag, Secaucus, NJ, USA.
Patrice Godefroid. 1997. Model Checking for Programming Languages Using VeriSoft. In POPL.
Patrice Godefroid. 2005. Software Model Checking: The VeriSoft Approach. FMSD 26, 2 (2005), 77–101.
Patrice Godefroid, Gerard J. Holzmann, and Didier Pirottin. 1995. State-space Caching Revisited. FMSD 7, 3 (1995), 227–241.
Jeﬀ Huang. 2015. Stateless Model Checking Concurrent Programs with Maximal Causality Reduction. In PLDI.

1:36

M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya

Kari Kähkönen, Olli Saarikivi, and Keijo Heljanko. 2012. Using Unfoldings in Automated Testing of Multithreaded Programs.
In ACSD.
Vineet Kahlon, Chao Wang, and Aarti Gupta. 2009. Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order
Reduction Technique. In CAV.
Shmuel Katz and Doron Peled. 1992. Deﬁning Conditional Independence Using Collapses. Theor. Comput. Sci. 101, 2 (1992),
337–359.
Akash Lal and Thomas Reps. 2009. Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis. FMSD
35, 1 (2009), 73–97.
Leslie Lamport. 1978. Time, Clocks, and the Ordering of Events in a Distributed System. Commun. ACM 21, 7 (1978),
558–565.
L. Lamport. 1979. How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs. IEEE Trans.
Comput. 28, 9 (1979), 690–691.
Steven Lauterburg, Rajesh K. Karmani, Darko Marinov, and Gul Agha. 2010. Evaluating Ordering Heuristics for Dynamic
Partial-order Reduction Techniques. In FASE.
Richard J. Lipton. 1975. Reduction: A Method of Proving Properties of Parallel Programs. Commun. ACM 18, 12 (1975),
717–721.
Tom Ball Madan Musuvathi, Shaz Qadeer. 2007. CHESS: A systematic testing tool for concurrent software. Technical Report.
Friedemann Mattern. 1989. Virtual Time and Global States of Distributed Systems. In Parallel and Distributed Algorithms.
North-Holland, 215–226.
A Mazurkiewicz. 1987. Trace Theory. In Advances in Petri Nets 1986, Part II on Petri Nets: Applications and Relationships to
Other Models of Concurrency. Springer-Verlag New York, Inc., 279–324.
K. L. McMillan. 1995. A Technique of State Space Search Based on Unfolding. FMSD 6, 1 (1995), 45–65.
Madanlal Musuvathi and Shaz Qadeer. 2007. Iterative Context Bounding for Systematic Testing of Multithreaded Programs.
SIGPLAN Not. 42, 6 (2007), 446–455.
Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, Gerard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. 2008.
Finding and Reproducing Heisenbugs in Concurrent Programs. In OSDI.
Doron Peled. 1993. All from One, One for All: On Model Checking Using Representatives. In CAV.
Carl Adam Petri. 1962. Kommunikation mit Automaten. Ph.D. Dissertation. Universität Hamburg.
César Rodríguez, Marcelo Sousa, Subodh Sharma, and Daniel Kroening. 2015. Unfolding-based Partial Order Reduction. In
CONCUR.
Olli Saarikivi, Kari Kahkonen, and Keijo Heljanko. 2012. Improving Dynamic Partial Order Reductions for Concolic Testing.
In ACSD.
Koushik Sen and Gul Agha. 2006. Automated Systematic Testing of Open Distributed Programs. In FASE.
Koushik Sen and Gul Agha. 2007. A Race-detection and Flipping Algorithm for Automated Testing of Multi-threaded
Programs. In HVC.
Traian Florin Şerbănuţă, Feng Chen, and Grigore Roşu. 2013. Maximal Causal Models for Sequentially Consistent Systems.
In RV.
Samira Tasharoﬁ, Rajesh K. Karmani, Steven Lauterburg, Axel Legay, Darko Marinov, and Gul Agha. 2012. TransDPOR: A
Novel Dynamic Partial-order Reduction Technique for Testing Actor Programs. In FMOODS/FORTE.
Antti Valmari. 1991. Stubborn Sets for Reduced State Space Generation. In Petri Nets.
Chao Wang, Zijiang Yang, Vineet Kahlon, and Aarti Gupta. 2008. Peephole Partial Order Reduction. In TACAS.

