Dynamic Partial-Order Reduction
for Model Checking Software
Cormac Flanagan
University of California at Santa Cruz
cormac@cs.ucsc.edu

Patrice Godefroid
Bell Laboratories, Lucent Technologies
god@bell-labs.com

ABSTRACTIn the context of the second approach, partial-order reduction seems (so far) to be the most eﬀective techniquefor reducing the size of the state space of concurrent software systems at the implementation level. Two main core
partial-order reduction techniques are usually considered:persistent/stubborn sets and sleep sets.
In a nutshell, the persistent/stubborn set technique [25, 9]
computes a provably-suﬃcient subset of the set of enabledtransitions in each visited state such that unselected enabledtransitions are guaranteed not to interfere with the execution of those being selected. The selected subset is called apersistent set, while the most advanced algorithms for computing such sets are based on the notion of stubborn sets [25,9]. These algorithms exploit information about “which operations on which communication objects each process might
execute in the future”. This information is typically obtained from a static analysis of the code. Minimally, such astatic analysis can simply attempt to identify objects accessible by a single process only, and then classify operations
on such objects as local (e.g., [5]).
In contrast, the sleep set technique (see [9]) exploits information on dependencies exclusively among the transitions
enabled in the current state, as well as information recorded
about the past of the search. Both techniques can be usedsimultaneously and are complementary [9].
In the presence of cycles in the state space, these techniques must be combined with additional conditions to makesure the transition selection is fair with respect to all processes in order to verify properties more elaborate than deadlock detection, such as checking arbitrary safety and livenessproperties. For instance, an ample set (see [2]) is a persistent set that satisﬁes additional conditions suﬃcient for
LTL model checking. Techniques for dealing with cycles aremostly orthogonal to the two “core” techniques mentioned
above, which are suﬃcient for detecting deadlocks.
In what follows, we will assume that the state spaces weconsider do not contain any cycles, and focus the discussion
on detecting deadlocks and safety-property violations suchas assertion failures (e.g., speciﬁed with assert() in C).
Note that acyclic state spaces are quite common in the context of model checking of software implementations: the execution of most software applications eventually terminates,
either because the application is input driven and reacts toexternal events speciﬁed in a test driver encoding only ﬁnite sequences of inputs, or because the execution length isbounded at run/test time and hence forced to terminate.
Unfortunately, existing persistent/stubborn set techniques
suﬀer from a severe fundamental limitation: in the context

We present a new approach to partial-order reduction formodel checking software. This approach is based on initially exploring an arbitrary interleaving of the various concurrent processes/threads, and dynamically tracking interactions between these to identify backtracking points where
alternative paths in the state space need to be explored. We
present examples of multi-threaded programs where our new
dynamic partial-order reduction technique signiﬁcantly reduces the search space, even though traditional partial-orderalgorithms are helpless.

Categories and Subject Descriptors
D.2.4 [Software Engineering]: Software/Program Veriﬁcation; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs

General Terms
Algorithms, Veriﬁcation, Reliability

Keywords
Partial-order reduction, software model checking

1.

INTRODUCTION

Over the last few years, we have seen the birth of the ﬁrst
software model checkers for programming languages such as
C, C++ and Java. Roughly speaking, two broad approaches
have emerged. The ﬁrst approach consists of automaticallyextracting a model out of a software application by staticallyanalyzing its code and abstracting away details, applying
traditional model checking to analyze this abstract model,
and then mapping abstract counter-examples back to thecode or reﬁning the abstraction (e.g., [1, 14, 4]). The second approach consists of systematically exploring the state
space of a concurrent software system by driving its executions via a run-time scheduler (e.g., [10, 27, 5]). Bothof these approaches to software model checking have theiradvantages and limitations (e.g., [11]).
Permission to make digital or hard copies of all or part of this work forpersonal or classroom use is granted without fee provided that copies are
not made or distributed for profit or commercial advantage and that copies
bear this notice and the full citation on the first page. To copy otherwise, torepublish, to post on servers or to redistribute to lists, requires prior specificpermission and/or a fee.
POPL’05, January 12–14, 2005, Long Beach, California, USA.
Copyright 2005 ACM 1-58113-830-X/05/0001 ...$5.00.

1the hash table are still explored, resulting in state explosion
and making model checking intractable for all but a small
number of threads.
We propose in this paper a new approach to partial-order
reduction that avoids the inherent imprecisions of static
alias analyses. Our new algorithm starts by executing the
program until completion, resolving nondeterminism completely arbitrarily, and it dynamically collects information
about how threads have communicated during this speciﬁc
execution trace, such as which shared memory locations wereread or written by which threads and in what order. Thisdata is then analyzed to add backtracking points along thetrace that identify alternative transitions that need to be
explored because they might lead to other execution traces
that are not “equivalent” to the current one (i.e., are notlinearizations of the same partial-order execution). The procedure is repeated until all alternative executions have been
explored and no new backtracking points need be added.
When the search stops, all deadlocks and assertion failuresof the system are guaranteed to have been detected.
For the Indexer example, if it is detected dynamicallyduring the ﬁrst execution trace of the program that the various threads access disjoint memory location, then no backtracking points are added along that trace, and the reduced
state space with our dynamic partial-order reduction is asingle path. This turns out to be the case for this programwith up to 11 threads, as we will show in Section 5.
The paper is organized as follows. After some backgrounddeﬁnitions, we present in Section 3 a general dynamic partialorder reduction algorithm for detecting deadlocks in acyclicstate spaces. In section 4, we discuss how to optimize thisalgorithm to the case of multithreaded programs. In Section 5, we present preliminary experimental results on somesmall examples. Section 6 discusses other related work, andwe conclude with Section 7.

Figure 1: Indexer Program.
Thread-global (shared) variables:
const int size = 128;
const int max = 4;
int[size] table;
Thread-local variables:
int m = 0, w, h;
Code for thread tid:
while (true) {w := getmsg();
h := hash(w);while (cas(table[h],0,w) == false) {h := (h+1) % size;}}
int getmsg() {if (m < max ) {return (++m) * 11 + tid;
} else {exit(); // terminate}}
int hash(int w) {return (w * 7) % size;}of concurrent software systems executing arbitrary C, C++or Java code, determining “which operations on which communication objects each process might execute in the future” with acceptable precision is often diﬃcult or impossible to compute precisely. If this information is too imprecise,persistent/stubborn sets techniques cannot prune the state
space very eﬀectively. Sleep sets can still be used, but usedalone, they can only reduce the number of explored transitions, not the number of explored states [9], and hencecannot avoid state explosion.
To illustrate the nature of this problem, consider the program Indexer shown in Figure 1, where multiple concurrent threads manipulate a shared hash table. Each thread
has a a thread identiﬁer tid ∈ {1, . . . , n} and receives anumber of incoming messages w and inserts each message
into the hash table at corresponding index h=hash(w). If ahash table collision occurs, the next free entry in the table
is used. All hash table entries are initially 0. The atomic
compare-and-swap instruction cas(table[h],0,w) checks if
table[h] is initially 0; if so, then it updates table[h] tow and returns true, and otherwise returns false (withoutchanging table[h]).
A static alias analysis for determining when two diﬀerent
threads can access the same memory location would need toknow all the possible messages received by all the threads
as well as predict the hash values computed for all suchmessages, for all execution paths. Since this is clearly notrealistic, static analyses conservatively assume that every
access to the hash table may access the same entry. The
latter is equivalent to treating the entire hash table as asingle shared variable, and prevents partial-order reduction
techniques from signiﬁcantly pruning the state space of thisprogram. Instead, all possible interleavings of accesses to

2. BACKGROUND DEFINITIONS
2.1 Concurrent Software Systems
We consider a concurrent system composed of a ﬁnite set
P of threads or processes, and deﬁne its state space using a
dynamic semantics in the style of [10]. Each process executes a sequence of operations described in a deterministic
sequential program written in a language such as C, C++ orJava. The processes communicate by performing atomic operations on communication objects, such as shared variables,
semaphores, locks, and FIFO buﬀers. In what follows, processes that share the same heap are called threads. Threads
are thus a particular type of processes. Unless otherwise
speciﬁed, the algorithms discussed in this paper apply toboth processes and threads.
Operations on communication objects are called visible
operations, while other operations are invisible. The execution of an operation is said to block if it cannot currently
be completed; for instance, an operation “acquire(l)” mayblock until the lock is released by an operation “release(l)”.
We assume that only executions of visible operations may
block.
A state of the concurrent system consists of the local
state LocalState of each process, and of the shared state2

SharedState of all communication objects:
State
LocalStates==

Figure 2: State space for Indexer example for two
threads T 1 and T 2 and max=1.

SharedState × LocalStates
P → LocalState

T1: cas(table[84],0,12)

For ls ∈ LocalStates , we write ls[p := l] to denote the mapthat is identical to ls except that it maps p to local state l.
A transition moves the system from one state to a subsequent state, by performing one visible operation of a chosen
process, followed by a ﬁnite sequence of invisible operationsof the same process, ending just before the next visible operation of that process. The transition tp,l of process p for
local state l ∈ LocalState is deﬁned via a partial function:

T2: cas(table[91],0,13)s0

terminating state

T2: cas(table[91],0,13)

T1: cas(table[84],0,12)

deﬁnition avoids including the (unnecessary) interleavingsof invisible operations as part of the state space (hence already reducing state explosion), while still being provably
suﬃcient for detecting deadlocks and assertion violations asshown in [10]. Also, a model checker for exploring such state
spaces needs only control and observe the execution of visible operations, as is done in the tool VeriSoft [10, 11].

tp,l : SharedState  LocalState × SharedState
Let T denote the set of all transitions of the system. A
transition tp,l ∈ T is enabled in a state s = g, ls (whereg ∈ SharedState and ls ∈ LocalStates ) if l = ls(p) and tp,l (g)is deﬁned. If t is enabled in s and tp,l (g) = g  , l , then we
say the execution of t from s produces a unique1 successortwstate s = g  , ls[p := l ], written s → s . We write s ⇒ s
to mean that the execution of the ﬁnite sequence w ∈ T ∗leads from s to s .
We deﬁne the behavior of the concurrent system as a transition system AG = (State, ∆, s0 ), where ∆ ⊆ State × Stateis the transition relation deﬁned by

2.2 Definitions for Partial-Order Reduction
We brieﬂy recall some basic principles of partial-order reduction methods. The basic observation exploited by thesetechniques is that AG typically contains many paths that
correspond simply to diﬀerent execution orders of the same
uninteracting transitions. When concurrent transitions are“independent”, meaning that their execution does not interfere with each other, changing their order of execution
will not modify their combined eﬀect. This notion of independency between transitions and its complementary notion,
the notion of dependency, can be formalized by the following
deﬁnition (adapted from [15]).

t(s, s ) ∈ ∆ iﬀ ∃t ∈ T : s → sand s0 is the initial state of the system.
In any given state s = g, ls, let next(s, p) = tp,ls(p) denote the (unique) next transition to be executed by process
p. For any transition tp,l , let proc(tp,l ) = p denote the process executing the transition (we thus assume all processes
have disjoint sets of transitions). A state in which no transition is enabled is called a deadlock, or a terminating state.
The state transformation resulting from the execution ofa transition may vary depending on the current state. For
instance, if the next visible operation of thread p in a states is read(x) in the program:

Definition 1. Let T be the set of transitions of a concurrent system and D ⊆ T × T be a binary, reﬂexive, andsymmetric relation. The relation D is a valid dependency
relation for the system iﬀ for all t1 , t2 ∈ T , (t1 , t2 ) ∈ D
(t1 and t2 are independent) implies that the two following
properties hold for all states s in the state space AG of thesystem:{if (read(x)) then i=0 else i=2}; write(x);t

1
1. if t1 is enabled in s and s →s , then t2 is enabled in
s iﬀ t2 is enabled in s ; andwhere x is a shared variable and i is a local variable, theinvisible operation(s) following read(x) will depend on thevalue of x. However, the transition t = next(s, p) is still
unique and can thus be viewed as the entire block between
the braces. Note that next(s, p) does not change even if
other processes execute other transitions changing the value
wof x from s: for all s such that s ⇒ s where w does not contain any transition from p, we have next(s , p) = next(s, p).
Consider again the Indexer example of Figure 1. Its state
space AG (for two threads and max=1) is shown in Figure 2.
Transitions in AG are labeled with the visible operation of
the corresponding thread transition being executed. Nondeterminism (branching) in AG is caused only by concurrency.
This state space contains a single terminating state (where
both threads are blocked on their exit() statement) since
the two threads access distinct hash table entries.
Observe how the above deﬁnition of state space collapses
purely-local computations into single transitions, by combining invisible operations with the last visible one. This

2. if t1 and t2 are enabled in s, then there is a uniquet1 t2 t2 t1 state s such that s ⇒s and s ⇒s.
Thus, independent transitions can neither disable nor enable each other, and enabled independent transitions commute. This deﬁnition characterizes the properties of possible“valid” dependency relations for the transitions of a given
system. In practice, it is possible to give easily-checkableconditions that are suﬃcient for transitions to be independent (see [9]). Dependency can arise between transitionsof diﬀerent processes that perform visible operations on thesame shared object. For instance, two acquire operations
on the same lock are dependent, and so are two write operations on the same variable; in contrast, two read operations on the same variable are independent, and so are two
write or compare-and-swap operations on diﬀerent variables(such as cas(table[84],0,12) and cas(table[91],0,13)
in the program of Figure 1). To simplify the presentation,
we assume in this paper that the dependency relation is notconditional [15, 9] and that all the transitions of a particular
process are dependent.

1
To simplify the presentation, we do not consider operations
that are nondeterministic [10] or that create dynamicallynew processes, although both features are compatible withthe algorithms and techniques discussed in the paper.

3

Traditional partial-order algorithms operate as classicalstate-space searches except that, at each state s reachedduring the search, they compute a subset T of the set oftransitions enabled at s, and explore only the transitions
in T . Such a search is called a selective search and may
explore only a subset of AG . Two main techniques for computing such sets T have been proposed in the literature:
the persistent/stubborn set and sleep set techniques. The
ﬁrst technique actually corresponds to a whole family of algorithms [25, 12, 13, 20], which can be shown to computepersistent sets [9]. Intuitively, a subset T of the set of transitions enabled in a state s of AG is called persistent in s if
whatever one does from s, while remaining outside of T , does
not interact with T . Formally, we have the following [12].

Given a transition sequence S, we use the following notation:• Si refers to transition ti ;• S.t denotes extending S with an additional transitiont;• dom(S) means the set {1, . . . , n};• pre(S, i) for i ∈ dom(S) refers to state si ; and• last(S) refers to sn+1 .
A transition t ∈ T can appear multiple times in a transition
sequence S. We write ti = tj to denote that transitions ti
and tj are occurrences of a same transition in T .
We say a transition t1 may be co-enabled with a transition
t2 if there may exist some state in which both t1 and t2 areboth enabled. For example, an acquire and release on thesame lock are never co-enabled, but two write operations on
the same variable may be co-enabled.
If two adjacent transitions in a transition sequence are
independent, then they can be swapped without changing
the overall behavior of the transition sequence. A transition sequence thus represents an equivalence class of similar sequences that can be obtained by swapping adjacentindependent transitions. To help reason about the equivalence class represented by a particular transition sequence,
we maintain a “happens-before” ordering relation on thesetransitions. The happens-before relation →S for a transition
sequence S = t1 . . . tn is the smallest relation on {1, . . . , n}such that

Definition 2. A set T ⊆ T of transitions enabled in astate s is persistent in s iﬀ, for all nonempty sequences oftransitions
t

tn−1

t

t

n
1
2
s1 →
s2 →
s3 . . . → sn →sn+1

from s in AG and including only transitions ti ∈ T , 1 ≤ i ≤n, tn is independent with all the transitions in T .
It is beyond the scope of this paper to review stubborn-setlike algorithms for computing persistent sets. In a nutshell,
these algorithms can exploit information on the static structure of the system being veriﬁed, such as “from its current
local state, process x could perform operation y on sharedobject z in some of its executions”, and inferred (approximated) by a static analysis of the system code. For instance,see [9] for several such algorithms and a comparison of theircomplexity.
The new partial-order reduction algorithm introduced in
the next section also explores at each visited state s the transitions in a persistent set in s. But unlike previously known
algorithms, these persistent sets are computed dynamically.
Before presenting this new algorithm, we brieﬂy recall
some properties of persistent sets that will be used later.
First, a selective search of AG using persistent sets is guaranteed to visit all the deadlocks in AG (see Theorem 4.3
in [9]). Moreover, if AG is acyclic, a selective search using
persistent sets is also guaranteed to visit all the reachable
local states of every process in the system (see Theorem
6.14 in [9]), and hence can be used to detect violations ofany property reducible to local state reachability, including
violations of local assertions and of safety properties.

3.

1. if i ≤ j and Si is dependent with Sj then i →S j;
2. →S is transitively closed.
By construction, the happens-before relation →S is a partialorder relation, often called a “Mazurkiewicz’s trace” [18, 9],
and the sequence of transitions in S is one of the linearizations of this partial order. Other linearizations of this partial order yield “equivalent” transition sequences that canbe obtained by swapping adjacent independent transitions.
We also use a variant of the happens-before relation to
identify backtracking points. Speciﬁcally, the relationi →S pholds for i ∈ dom(S) and process p if either
1. proc(Si ) = p or
2. there exists k ∈ {i + 1, . . . , n} such that i →S k andproc(Sk ) = p.

DYNAMIC PARTIAL-ORDER
REDUCTION

Intuitively, if i →S p, then the next transition of process pfrom the state last(S) is not the next transition of process
p in the state right before transition Si in either this transition sequence or in any equivalent sequence obtained byswapping adjacent independent transitions.
The new partial-order reduction algorithm is presented in
Figure 3. In addition to maintaining the current transition
sequence or search stack S, each state s in the stack S is also
associated with a “backtracking set”, denoted backtrack(s),which represents processes with a transition enabled in sthat needs to be explored from s.
Whenever a new state s is reached during the search, theprocedure Explore is called with the stack S with which thestate is reached. Initially (line 0), the procedure Explore iscalled with the empty stack as argument. In line 2, last(S)We present in this section a new partial-order reduction
algorithm that dynamically tracks interactions between processes and then exploits this information to identify backtracking points where alternative paths in the state space
AG need to be explored. The algorithm is based on a traditional depth-ﬁrst search in the (reduced) state space of thesystem.
The algorithm maintains the traditional depth-ﬁrst search
stack as a transition sequence executed from the initial states0 of AG . Speciﬁcally, a transition sequence S ∈ T ∗ is a(ﬁnite) sequence of transitions t1 t2 . . . tn where there exist
states s1 , . . . , sn+1 such that s1 is the initial state s0 and
t

t

n
1
s1 →
s2 . . . →sn+1

4

Figure 3: Dynamic Partial-Order Reduction Algorithm.
0

Initially: Explore(∅);

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

Explore(S) {let s = last(S);for all processes p {if ∃i = max({i ∈ dom(S) | Si is dependent and may be co-enabled with next(s, p) and i →S p}) {let E = {q ∈ enabled(pre(S, i)) | q = p or ∃j ∈ dom(S) : j > i and q = proc(Sj ) and j →S p};
if (E = ∅) then add any q ∈ E to backtrack(pre(S, i));else add all q ∈ enabled(pre(S, i)) to backtrack(pre(S, i));}}if (∃p ∈ enabled(s)) {backtrack(s) := {p};let done = ∅;while (∃ p ∈ (backtrack(s) \ done)) {add p to done;
Explore(S.next(s, p));}}}explored this way, the search from s is over and state s is
said to be “backtracked”.
Note that the algorithm of Figure 3 is stateless [10]: it does
not store previously visited states in memory since eﬃciently
computing a canonical representation for states of large concurrent (possibly distributed) software applications is problematic and prohibitively expensive. Backtracking can be
performed without storing visited states in memory, for instance by re-executing the program from its initial state, or“forking” new processes at each backtracking point, or storing only backtracking states using checkpointing techniques,or a combination of these [11].

is the state reached by executing S from the initial states0 . Then, for all processes p, the next transition next(s, p)of each process p in state s is considered (line 3). For eachsuch transition next(s, p) (which may be enabled or disabledin s), one then computes (line 4) the last transition i in S
such that Si and next(s, p) are dependent (cf. Deﬁnition 1)
and may be co-enabled, and such that i →S p.
If there exists such a transition i, there might be a race
condition or dependency between i and next(s, p), and hence
we might need to introduce a “backtracking point” in thestate pre(S, i), i.e., in the state just before executing thetransition i.2 This is determined in line 5 by computing theset E of processes q with an enabled transition in pre(S, i)that “happens-before” next(s, p) in the current partial order →S . Intuitively, if E is nonempty, the execution of all
the processes in E is necessary (although perhaps not sufﬁcient) to reach transition next(s, p) and to make it enable
in the current partial order →S ; in that case, it is therefore
suﬃcient to add any single one of the processes in E to the
backtracking set associated with pre(S, i). In contrast, if E
is empty, the algorithm was not able to identify a process
whose execution is necessary for next(s, p) to become enabled from pre(S, i); by default (line 7), the algorithm thenadds all enabled processes in backtrack(pre(S, i)).
Once the computation of possibly new backtracking pointsof lines 3–9 is completed, the search can proceed from thecurrent state s. If there are enabled processes in s (line 10),any one of those is selected to be explored by being added
to the backtracking set of s (line 11). As long as there areenabled processes in the backtracking set associated withthe current state s that have not been explored yet, those
processes will be executed one by one by the code of lines
13–15. When all the processes in backtrack(s) have been

To illustrate the recursive nature of our dynamic partial order reduction algorithm, consider two concurrent processes p1 and p2 sharing two variables x and y, and executing
the two programs:
p1 :
p2 :

x=1; x=2;
y=1; x=3;

Assume the ﬁrst (arbitrary and maximal) execution of thisconcurrent program is:
p1:x=1; p1:x=2; p2:y=1; p2:x=3;
Before executing the last transition p2:x=3 of process p2 , thealgorithm will add a backtracking point for process p2 justbefore the last transition of process p1 that is dependent withit (the transition p1:x=2), forcing the subsequent explorationof:
p1:x=1; p2:y=1; p2:x=3; p1:x=2;
Similarly, before executing the transition p2:x=3 in that second sequence, the algorithm will add a backtracking point
for process p2 just before p1:x=1, which in turn will force
the exploration of:2

Only the last transition i in S satisfying the constraints ofline 4 needs be considered: if there are other such transitions
j < i before i in S that require adding other backtracking
points, these are added later through the recursion of thealgorithm.

p2:y=1; p2:x=3; p1:x=1; p1:x=2;
5

E is empty, but instead of selecting a single otherprocess q enabled in pre(S, i) and not previously executed from pre(S, i), and to re-start a new persistentset computation in pre(S, i) with q as the initial process. However, to avoid circularity in this reasoning
and to ensure the correctness of this variant algorithm,
it is then necessary to “mark” process proc(ti ) in statepre(S, i) so that, if proc(ti ) is ever selected to be backtracked in pre(S, i) during this new persistent-set computation starting with q, yet another fresh persistentset computation may be needed in pre(S, i), and soon.

Note that the two possible terminating states (deadlocks)
and three possible partial-order executions of this concurrent
program are eventually explored. This example illustrates
why it is suﬃcient to consider only the last transition in S
in line 4 of our algorithm of Figure 3.
The correctness of the above algorithm is established via
the following theorem.
Theorem 1. Whenever a state s is backtracked during
the search performed by the algorithm of Figure 3 in an
acyclic state space, the set T of transitions that have been
explored from s is a persistent set in s.

4. IMPLEMENTATION

Proof: See Appendix.

In this section, we discuss how to implement the previous
general algorithm. We assume that the system has m processes p1 , . . . , pm ; that d is the maximum size of the search
stack; and that r is the number of transitions explored in
the reduced search space.

Since the algorithm of Figure 3 explores a persistent set inevery visited state, it is guaranteed to detect every deadlock
and safety-property violation in any acyclic state space (seeSection 2). The complexity of the algorithm depends on
how the happens-before relation →S is implemented and isdiscussed further in the next section.
Theorem 1 speciﬁes the type of reduction performed by
our new algorithm, as well as its complementarity and compatibility with other partial-order reduction techniques. In
particular, any algorithm for computing statically persistent sets, such as stubborn-set-like algorithms, can be usedin conjunction of the algorithm in Figure 3: in lines 5 and 7,
replace enabled(pre(S, i)) by P ersistentSet(pre(S, i))), andin line 10, replace enabled(s) by P ersistentSet(s), where
the function P ersistentSet(s) computes “statically” a persistent set T in state s and returns {proc(t) | t ∈ T }. These
modiﬁcations will restrict the search space to transitions
contained in the statically-computed persistent sets for each
visited state s, while using dynamic partial-order reduction
to further reﬁne these statically-computed persistent sets.
Moreover, sleep sets can also be used in conjunction with
the new dynamic technique, combined or not with staticallycomputed persistent sets. In our context (i.e., for acyclicstate spaces), sleep sets can be added exactly as describedin [10]. The known beneﬁts and limitations of sleep setscompared to persistent sets remain unchanged: used alone,they can only reduce the number of explored transitions, but
used in conjunction with (dynamic or static) persistent set
techniques, they can further reduce the number of states aswell [9].3

4.1 Clock Vectors
The implementation of the algorithm of Figure 3 is mostly
straightforward, apart from identifying the necessary backtracking points in lines 3–9, which requires deciding thehappens-before relation i →S p. A natural representation
strategy for the happens-before relation is to use clock vectors [17]. A clock vector is a map from process identiﬁers toindices in the current transition sequence S:
CV = P → N
We maintain a clock vector C(p) ∈ CV for each process p.
If process pi has clock vector C(pi ) = c1 , . . . , cm , then cj
is the index of the last transition by process pj such that
cj →S pi . More generally:i →S pif and only ifi ≤ C(p)(proc(Si ))Thus clock vectors allow us to decide the happens-before
relation i →S p in constant time.
We use max (·, ·) to denote the pointwise maximum of twoclock vectors; C[pi := ci ] to update the clock vector C sothat the clock for process pi is ci ; and ⊥ to denote theminimal clock vector:
max (c1 , .., cm , c1 , .., cm ) = max (c1 , c1 ), .., max (cm , cm )
c1 , . . . , cm [pi := ci ] = c1 , . . . , ci−1 , ci , ci+1 , . . . , cm 
⊥ = 0, . . . , 0

We conclude this section by brieﬂy discussing two optimizations of the algorithm of Figure 3.

Whenever we explore a transition of a process p, we need
to update the clock vector C(p) to be the maximum of theclock vectors of all preceding dependent transitions. For thispurpose, we also keep a clock vector C(i) for each index i in
the current transition sequence S.
Clock vectors can also be used to compute the set E asin line 5 of Figure 3. However, this requires O(m2 .d) time
per explored transition. Instead, for simplicity, our modiﬁed
algorithm just backtracks on all enabled processes in the casewhere p is not enabled in pre(S, i) (line 7). Note that thislast modiﬁcation is independent of the use of clock vectors.
Figure 4 presents a modiﬁed algorithm that maintains anduses these per-process and per-transition clock vectors. The
code at lines 14.1–14.5 that updates these clock vectors requires O(m.d) time per explored transition. Line 4 of thealgorithm searches for an appropriate backtracking point,

1. Since any process q in E can be added to the set
backtrack(pre(S, i)) in line 6, it is clearly preferable topick a process q that is already in backtrack(pre(S, i)),whenever possible, in order to minimize the size of
backtrack(pre(S, i)).
2. A more subtle optimization consists of not adding all
enabled processes to backtrack(pre(S, i)) in line 7 when
3

There is a nice complementarity between sleep sets and our
dynamic partial-order reduction algorithm: when a process
q is introduced in backtrack(pre(S, i)) in line 6 or 7 because of a potential conﬂict between i and next(s, p), there
is no point in executing Si following next(pre(S, i), q) before
next(s, p) is executed; this optimization is captured exactly
by sleep sets.
6

Figure 4: DPOR using Clock Vectors.

Figure 5: DPOR without Stack Traversals.

00Initially: Explore(∅, λx.⊥);

Explore(S, C) {let s = last(S);for all processes p {if ∃i = max({i ∈ dom(S) | Si is dependentand may be co-enabled with next(s, p)
and i ≤ C(p)(proc(Si ))}){5
if (p ∈ enabled(pre(S, i)))6then add p to backtrack(pre(S, i));7else add enabled(pre(S, i)) to backtrack(pre(S, i));
8
}
9
}
10
if (∃p ∈ enabled(s)) {11
backtrack(s) := {p};12
let done = ∅;13
while (∃ p ∈ (backtrack(s) \ done)) {14
add p to done;
14.1
let t = next(s, p);
14.2
let S  = S.t;
14.3
let cv = max {C(i) | i ∈ 1..|S| andSi dependent with t};
14.4
let cv2 = cv[p := |S  |];14.5
let C  = C[p := cv2, |S  | := cv2];
15
Explore(S  , C  );
16
}
17
}
18 }

Explore(S, C, L) {let s = last(S);for all processes p {let i = L(α(next (s, p)));if i = 0 and i ≤ C(p)(proc(Si )){5
if (p ∈ enabled(pre(S, i)))6then add p to backtrack(pre(S, i));7else add enabled(pre(S, i)) to backtrack(pre(S, i));
8
}
9
}
10
if (∃p ∈ enabled(s)) {11
backtrack(s) := {p};12
let done = ∅;13
while (∃ p ∈ (backtrack(s) \ done)) {14
add p to done;
14.1
let S  = S.next(s, p);
14.2
let o = α(next(s, p));14.3
let cv = max (C(p), C(o))[p := |S  |];14.4
let C  = C[p := cv, o := cv];
14.5
let L = if next(s, p) is a release
then Lelse L[o := |S  |];15
Explore(S  , C  , L );
16
}
17
}
18 }

1
2
3
4

1
2
3
4

and can be implemented as a sequential search through thetransition stack S. The worst-case time complexity of thisalgorithm is O(m.d.r).
The following invariants hold on each call to Explore: forall i, j ∈ dom(S) and for all p ∈ P:
i →S p iﬀ
i →S j iﬀ

Initially: Explore(∅, λx.⊥, λx.0);

To avoid a stack traversal for identifying backtracking
points, we also make some assumptions about the co-enabled
relation. Speciﬁcally, for any object o that is not a lock, we
assume that any two transitions that access o may be coenabled. (Even if two operations are never co-enabed, it isstill safe to assume that they may be co-enabled – this may
limit the amount of reduction obtained, but will not aﬀect
correctness.) We use an auxiliary variable L(o) to track theindex of the last transition that accessed o. When we consider a subsequent access to o by a transition next(s, p), we
need to ﬁnd the last dependent, co-enabled transition that
does not happen-before p. By our assumptions, the last access L(o) must be co-enabled and dependent with next(s, p),
as they both access the same object o, which is not a lock.
Therefore, L(o) is the appropriate backtracking point, provided L(o) does not happen-before p. In the case where
L(o) happens-before p, since the accesses to o are totallyordered, there cannot be any previous access to o that does
not happen-before p, and therefore no backtracking point isnecessary.
For a lock acquire, the appropriate backtracking point is
not the preceding release, since an acquire and a release on
the same lock are never co-enabled. Instead, the appropriate
backtracking point for a lock acquire is actually the preceding lock acquire. Hence, for any lock o, we use L(o) to record
the index of the last acquire (if any) on that lock.
Figure 5 contains a model checking algorithm based onthese ideas. On each call to Explore, ﬁnding backtracking points requires constant time per process, or O(m) time
per explored transition. The clock vector operations on

i ≤ C(p)(proc(Si ))i ≤ C(j)(proc(Si ))Using these invariants, we can show that the algorithm of
Figure 4 is a specialized version of the algorithm of Figure 3 (although it may conservatively add more backtracking
points in line 7).

4.2 Avoiding Stack Traversals
This section reﬁnes the previous algorithm to avoid traversing the entire transition stack S. Instead, we assume thateach transition t operates on exactly one shared object,which we denote by α(t) ∈ Object . In addition, we assume that two transitions t1 and t2 are dependent if andonly if they access the same communication object, that is,if α(t1 ) = α(t2 ). Under these assumptions, the dependence
relation is an equivalence relation and all accesses to an object o are totally ordered by the happens-before relation.
In this case, it is suﬃcient to only keep a clock vector
C(o) for the last access to each object o. The use of perobject instead of per-transition clock vectors signiﬁcantly
reduces the time and space requirements of our algorithm.
Maintaining these per-object clock vectors requires O(m)time per explored transition, as shown in lines 14.3–14.4 of
Figure 5.
7For conﬁgurations with up to 11 threads, since there areno conﬂicts in the hash table and each thread accesses different memory locations, the reduced state space with Dynamic POR is a single path. In comparison, the Static POR
quickly suﬀers from state explosion. When combined withsleep sets, Static POR performs better, but still cannot avoid
state explosion. Using a stateful search in addition to sleep
sets does not signiﬁcantly further reduce the number of explored transitions.

lines 14.3–14.4 also require O(m) time per explored transition. Thus, the overall time complexity of this algorithmis O(m.r). In the following section, we evaluate the performance of this optimized algorithm.
We can show that this algorithm implements Figure 3,
based on the following invariants that hold on each call to
Explore: for all i ∈ dom(S), for all p ∈ P, and for allo ∈ Object :i →S p iﬀ i ≤ C(p)(proc(Si ))L(o) = max {i ∈ dom(S) | α(Si ) = o and Si is not a release}

5.2 File System Benchmark

Note that this implementation supports arbitrary communication objects such as shared variables, but it requiresthat all operations on shared variables are dependent. In
particular, it does not exploit the fact that two concurrent
reads on a shared variable can commute. We could improve
the algorithm along these lines by recording two clock vectors for each shared variable, one for read accesses and forwrite accesses, and by using additional data structures tocorrectly identify backtracking points. The time complexityof the resulting algorithm is O(m2 .r). Due to space constraints we do not present this algorithm.

5.

Our second example in Figure 7 is derived from a synchronization idiom found in the Frangipani ﬁle system [24],and illustrates the statically-hard-to-predict use of sharedmemory that motivates this work. For each ﬁle, this example keeps a data structure called an inode that contains
a pointer to a disk block that holds the ﬁle data. Eachdisk block b has a busy bit indicating whether the block
has been allocated to an inode. Since the ﬁle system ismulti-threaded, these data structures are guarded by mutual exclusive locks. In particular, distinct locks locki[i]and lockb[b] protect each inode inode[i] and block busy
bit busy[b], respectively. The code for each thread picks an
inode i and, if that inode does not already have an associated block, the thread searches for a free block to allocate tothat inode. This search starts at an arbitrary block index,
to avoid excessive lock contention.
Figure 8 shows the number of transitions executed whenmodel checking this benchmark for 1 to 26 threads, using
each of the ten model checking algorithms. For No POR,
the search space quickly explodes, although sleep sets and astateful search provide some beneﬁt. Static POR identiﬁes
that all accesses to the inode and busy arrays are protectedby the appropriate locks, thus reducing the number of interleavings explored. Again, sleep sets help, but a statefulsearch does not provide noticable additional beneﬁt once
sleep sets are used. Indeed, the two lines in Figure 8 areessentially identical.
Static POR must conservatively consider that acquires ofthe locks locki[i] may conﬂict, and similarly for lockb[b].
In contrast, Dynamic POR dynamically detects that suchconﬂicts do not occur for up to 13 threads, thus reducing thesearch space to a single path. For larger numbers of threads,
since conﬂicts do occur, sleep sets provide additional beneﬁts
in combination with Dynamic POR.

EXPERIMENTAL EVALUATIONIn this section, we present a preliminary performance comparison of three diﬀerent partial-order reduction algorithms:• No POR: A straightforward model-checking algorithmwith no partial-order reduction.
• Static POR: A high-precision stubborn-set-like algorithm for statically computing persistent sets basedon a precise static analysis of the program.
• Dynamic POR: Our new dynamic partial-order reduction algorithm for multi-threaded programs shown in
Figure 5.
We describe the impact of using sleep sets in conjunction
with each algorithm. We also show the beneﬁt of extending
No POR and Static POR to perform a stateful search, wherevisited states are stored in memory and the model checking
algorithm backtracks whenever it visits a previously-visitedstate. We do not have a Dynamic POR implementationthat supports a stateful search, since it is not obvious how
to combine these ideas. Thus, we have ten model checking
conﬁgurations, and we evaluate each model checking conﬁguration on two benchmark programs.

5.1 Indexer Benchmark

5.3 Discussion

Our ﬁrst benchmark is the Indexer program of Figure 1,
where each threads inserts 4 messages into the shared hashtable. For this benchmark, since a static analysis cannot
reasonably predict with suﬃcient accuracy the conditions
under which hash table collisions would occur, Static POR
yields the same performance as No POR. For clarity, we donot show the results for No POR, since they are identicalto those for Static POR. Our experimental results are presented in Figure 6. The key for this ﬁgure is the same as
in Figure 8: we use triangles for Dynamic POR, circles for
Static POR, squares for No POR, dotted lines to indicate
a stateful search, and hollow objects to indicate the use of
sleep sets. Run-time is directly proportional to the numberof explored transitions in all these experiments.

The results obtained with the two previous benchmarks
clearly demonstrate that our dynamic partial-order reduction approach can sometimes signiﬁcantly outperform priorpartial-order reduction techniques.
However, note that Dynamic POR is not always strictly
better than Static POR, since Dynamic POR arbitrarily
picks the initial transition t from each state, and then dynamically computes a persistent set that includes t. In contrast, Static POR may be able to compute a smaller persistent set that need not include t. Since Static POR and Dynamic POR are compatible, they can be used simultaneously
and beneﬁt from each other’s strengths – these experiments
simply show that Dynamic POR can go much beyond Static
POR in cases where the latter is helpless.
8

Figure 8: Number of transitions explored for the File System Benchmarks.
File System Benchmark

Number of Transitions

1e+06

100000

10000

1000

100

10
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
Number of Threads

Dynamic POR, stateless, no sleep sets
Static POR, stateless, no sleep sets
Static POR, stateful, no sleep sets
No POR, stateless, no sleep sets
No POR, stateful, no sleep sets

Dynamic POR, stateless, sleep sets
Static POR, stateless, sleep sets
Static POR, stateful, sleep sets
No POR, stateless, sleep sets
No POR, stateful, sleep sets

Figure 7: File System Example.

Figure 6: Indexer Benchmark. (See Fig. 8 for key.)

Global variables:
const int NUMBLOCKS = 26;
const int NUMINODE = 32;
boolean[NUMINODE] locki;
int[NUMINODE] inode;boolean[NUMBLOCKS] lockb;
boolean[NUMBLOCKS] busy;

Indexer Benchmark

1e+06

Number of Transitions

100000Thread-local variables:
int i, b;
Code for thread tid:i := tid % NUMINODE;
acquire(locki[i]);if (inode[i] == 0) {b := (i*2) % NUMBLOCKS;
while (true) {acquire(lockb[b]);if (!busy[b]) {busy[b] := true;
inode[i] := b+1;
release(lockb[b]);break;}
release(lockb[b]);b := (b+1)%NUMBLOCKS;}}
release(locki[i]);exit();

10000

1000

100

10
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
Number of Threads

9

6.

RELATED WORK

additional processes or threads, dynamic memory allocation,or the dynamic creation of new communication channels between processes. In contrast, static analysis of such constructs is often diﬃcult or overly-approximate.
We therefore believe that the idea of dynamic partialorder reduction is signiﬁcant since it provides an attractive
and complementary alternative to the three known families of partial-order reduction techniques, namely persistent/stubborn sets, sleep sets and net unfoldings.
The algorithms presented in this paper can be used toprune acyclic state spaces while detecting deadlocks andsafety-property violations without any risk of incompleteness. In practice, these algorithms can be used for systematically and eﬃciently testing the correctness of any concurrent software system, whether its state space is acyclic ornot. However, in the presence of cycles, the depth of thesearch has to be bounded somehow, by simply using somearbitrary bound [10] for instance.
For application domains and sizes where computing canonical representations for visited system states is tractable,
such representations could be stored in memory and usedboth to avoid the re-exploration of previously visited states
and to detect cycles. It would be worth studying how to
combine the type of dynamic partial-order reduction introduced in this paper with techniques for storing states
in memory and with existing partial-order reduction techniques for dealing with cycles, liveness properties, and full
temporal-logic model checking (e.g., [26, 9, 2]).

Our dynamic partial-order reduction technique has some
general similarities with the “least-commitment search strategy” used in non-linear planners (e.g., see [3]) which originally inspired the work on partial-order reduction via netunfoldings [19], later extended from deadlock detection to
full model checking [6, 7]. Loosely speaking, the term “leastcommitment strategy” means that every enabled transitionis assumed by default not to interfere with any other concurrent transition, unless this assumption is proved wrong later
during the search. The net-unfolding technique uses an elaborate data structure, called net-unfolding, for representing
explicitly all the partial-order executions explored so far plus
all the nondeterminism (branching) to go from one to theother. In contrast, our technique only uses a partial-orderrepresentation →S of a single execution trace S. Anotherkey diﬀerence is that detecting deadlocks in a net-unfolding
is itself NP-hard in the size of the net-unfolding in general [19], while checking whether the current state is a deadlock is immediate with an explicit state-space exploration,
as in our approach. We are not aware of any implementationof the net-unfolding technique for languages (like C or Java)
more expressive than Petri-net-like formalisms. It would be
worth further comparing both approaches.
A number of recent techniques have considered various
kinds of exclusive access predicates for shared variables thatspecify synchronization disciplines such as “this variable isonly accessed when holding its protecting lock” [21, 22, 8,
5]. These exclusive access predicates can be leveraged to reduce the search space, while simultaneously being veriﬁed orinferred during reduced state-space exploration. However,these techniques do not work well when the synchronization
discipline changes during program execution, such as whenan object is initialized by its allocating thread without synchronization, and subsequently shared in a lock-protectedmanner by multiple threads. Also, these techniques would
not help in the case of the examples considered in the previous section. Note that dynamic partial-order reduction is
also compatible and complementary with these techniques.
Partial-order representations of execution traces [16] havealso been used for detecting invariant violations in distributed
systems (e.g., see [23]). In contrast with this prior work, we
exploit partial-order information to determine the possible
existence of execution traces that are not part of the current partial-order execution, and to introduce backtracking
points accordingly in order to prune the state space safely
for veriﬁcation purposes.

7.

Acknowledgements: We thank the anonymous reviewers for their helpful comments. This work was funded inpart by NSF CCR-0341658 and NSF CCR-0341179.

8. REFERENCES[1] T. Ball and S. Rajamani. The SLAM Toolkit. In
Proceedings of CAV’2001 (13th Conference on Computer
Aided Verification), volume 2102 of Lecture Notes in
Computer Science, pages 260–264, Paris, July 2001.
Springer-Verlag.
[2] E. M. Clarke, O. Grumberg, and D. A. Peled. Model
Checking. MIT Press, 1999.
[3] P. R. Cohen and E. A. Feigenbaum. Handbook of Artificial
Intelligence. Pitman, London, 1982.
[4] J. C. Corbett, M. B. Dwyer, J. Hatcliﬀ, S. Laubach, C. S.
Pasareanu, Robby, and H. Zheng. Bandera: Extracting
Finite-State Models from Java Source Code. In Proceedingsof the 22nd International Conference on Software
Engineering, 2000.
[5] M. B. Dwyer, J. Hatcliﬀ, V. R. Prasad, and Robby.
Exploiting Object Escape and Locking Information in
Partial Order Reduction for Concurrent Object-Oriented
Programs. To appear in Formal Methods in System Design,
2004.
[6] J. Esparza. Model Checking Using Net Unfoldings. Scienceof Computer Programming, 23:151–195, 1994.
[7] J. Esparza and K. Heljanko. Implementing LTL model
checking with net unfoldings. In Proceedings of the 8th
SPIN Workshop (SPIN’2001), volume 2057 of Lecture
Notes in Computer Science, pages 37–56, Toronto, May
2001. Springer-Verlag.
[8] C. Flanagan and S. Qadeer. Transactions for Software
Model Checking. In Proceedings of the Workshop on
Software Model Checking, pages 338–349, June 2003.
[9] P. Godefroid. Partial-Order Methods for the Verification ofConcurrent Systems – An Approach to the State-Explosion
Problem, volume 1032 of Lecture Notes in Computer
Science. Springer-Verlag, January 1996.

CONCLUSIONS

We have presented a new approach to partial-order reduction for model checking software. This approach is based on
dynamically tracking interactions between concurrent processes/threads at run time, and then exploiting this information using a new partial-order reduction algorithm to identify backtracking points where alternative paths in the state
space need to be explored.
In comparison to static partial-order methods, our algorithm is easy to implement and does not require a complicated and approximate static analysis of the program. In
addition, our dynamic POR approach can easily accommodate programming constructs that dynamically change thestructure of the program, such as the dynamic creation of10

volume 697 of Lecture Notes in Computer Science, pages
397–408, Elounda, June 1993. Springer-Verlag.
[27] W. Visser, K. Havelund, G. Brat, and S. Park. Model
Checking Programs. In Proceedings of ASE’2000 (15thInternational Conference on Automated Software
Engineering), Grenoble, September 2000.

[10] P. Godefroid. Model Checking for Programming Languages
using VeriSoft. In Proceedings of POPL’97 (24th ACM
Symposium on Principles of Programming Languages),
pages 174–186, Paris, January 1997.
[11] P. Godefroid. Software Model Checking: The VeriSoft
Approach. To appear in Formal Methods in System Design,
2005. Also available as Bell Labs Technical Memorandum
ITD-03-44189G.
[12] P. Godefroid and D. Pirottin. Reﬁning dependencies
improves partial-order veriﬁcation methods. In Proceedingsof CAV’93 (5th Conference on Computer Aided
Verification), volume 697 of Lecture Notes in Computer
Science, pages 438–449, Elounda, June 1993.
Springer-Verlag.
[13] P. Godefroid and P. Wolper. Using partial orders for theeﬃcient veriﬁcation of deadlock freedom and safety
properties. Formal Methods in System Design,2(2):149–164, April 1993.
[14] T. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy
Abstraction. In Proceedings of the 29th ACM Symposiumon Principles of Programming Languages, pages 58–70,
Portland, January 2002.
[15] S. Katz and D. Peled. Deﬁning conditional independence
using collapses. Theoretical Computer Science,
101:337–359, 1992.
[16] L. Lamport. Time, clocks, and the ordering of events in a
distributed system. Communications of the ACM,
21(7):558–564, 1978.
[17] F. Mattern. Virtual Time and Global States of Distributed
Systems. In Proc. Workshop on Parallel and Distributed
Algorithms, pages 215–226. North-Holland / Elsevier, 1989.
[18] A. Mazurkiewicz. Trace theory. In Petri Nets: Applications
and Relationships to Other Models of Concurrency,
Advances in Petri Nets 1986, Part II; Proceedings of an
Advanced Course, volume 255 of Lecture Notes in
Computer Science, pages 279–324. Springer-Verlag, 1986.
[19] K. McMillan. Using unfolding to avoid the state explosion
problem in the veriﬁcation of asynchronous circuits. In
Proc. 4th Workshop on Computer Aided Verification,
volume 663 of Lecture Notes in Computer Science, pages
164–177, Montreal, June 1992. Springer-Verlag.
[20] D. Peled. All from one, one for all: on model checking using
representatives. In Proc. 5th Conference on Computer
Aided Verification, volume 697 of Lecture Notes in
Computer Science, pages 409–423, Elounda, June 1993.
Springer-Verlag.
[21] S. D. Stoller. Model-Checking Multi-Threaded Distributed
Java Programs. International Journal on Software Tools
for Technology Transfer, 4(1):71–91, October 2002.
[22] S. D. Stoller and E. Cohen. Optimistic
Synchronization-Based State-Space Reduction. In
H. Garavel and J. Hatcliﬀ, editors, Proceedings of the 9thInternational Conference on Tools and Algorithms for theConstruction and Analysis of Systems (TACAS), volume2619 of Lecture Notes in Computer Science, pages 489–504.
Springer-Verlag, April 2003.
[23] S. D. Stoller, L. Unnikrishnan, and Y. A. Liu. Eﬃcient
Detection of Global Properties in Distributed Systems
Using Partial-Order Methods. In Proceedings of the 12th
Conference on Computer Aided Verification, volume 1855
of Lecture Notes in Computer Science, pages 264–279,
Chicago, July 2000. Springer-Verlag.
[24] C.A. Thekkath, T. Mann, and E.K. Lee. Frangipani: A
scalable distributed ﬁle system. In Proceedings of the 16th
ACM Symposium on Operating Systems Principles, pages
224–237, October 1997.
[25] A. Valmari. Stubborn sets for reduced state space
generation. In Advances in Petri Nets 1990, volume 483 ofLecture Notes in Computer Science, pages 491–515.
Springer-Verlag, 1991.
[26] A. Valmari. On-the-ﬂy veriﬁcation with stubborn sets. In
Proc. 5th Conference on Computer Aided Verification,

APPENDIX: Proof of Theorem 1
Let AG denote the state space of the system being analyzed,
and let s0 denote its unique initial state.
Deﬁne E(S, i, p) as:{ q ∈ enabled(pre(S, i)) |q = p or∃j ∈ dom(S) : j > i and q = proc(Sj ) and j →S p}
Deﬁne P C(S, j, p) as:
if
S is a transition sequence from s0 in AG
and i = max({i ∈ dom(S) | Si is dependent andco-enabled with next(last(S), p) and i →S p})
and i ≤ jthen
if E(S, i, p) = ∅then backtrack(pre(S, i)) ∩ E(S, i, p) = ∅else backtrack(pre(S, i)) = enabled(pre(S, i))Deﬁne the postcondition P C for Explore(S) as:∀p ∀w : P C(S.w, |S|, p)We ﬁrst show that the set of transition explored from eachreached state is a persistent set, provided the postcondition
holds for each recursive call to Explore(·).
Lemma 1. Whenever a state s reached after a transition
sequence S is backtracked during the search performed by
the algorithm of Figure 3, the set T of transitions that havebeen explored from s is a persistent set in s, provided thepostcondition P C holds for every recursive call Explore(S.t)
for all t ∈ T .
Proof. Lets =T =last(S){next(s, p) | p ∈ backtrack(s)}We proceed by contradiction, and assume that there exist
t1 , . . . , tn ∈ T such that:
1. S.t1 . . . tn is a transition sequence from s0 in AG and
2. t1 , . . . , tn−1 are all independent with T and3. tn is dependent with some t ∈ T .
By property of independence, this implies that t is enabledin the state last(S.t1 . . . tn−1 ) and hence co-enabled withtn . Without loss of generality, assume that t1 . . . tn is theshortest such sequence. We thus have that
∀1 ≤ i < n : i →t1 ...tn−1 n(If this was not true for some i, the same transition sequence without i would also satisfy our assumptions andbe shorter.) Let w denote the resulting (possibly empty)transition sequence produced by removing from t1 . . . tn−1
all the transitions ti (if any) such thati →t1 ...tn−1 proc(tn )11∀p : P C(S, |S|, p), and is directly established by lines 3–9of the algorithm of Figure 3.
(Inductive case) We assume that each recursive call to
Explore(S.t) satisﬁes its postcondition. That T is a persistent set in s then follows by Lemma 1. We show that
Explore(S) ensures its postcondition for any p and w suchthat S.w is a transition sequence from s0 in AG .
1. Suppose some transition in w is dependent with sometransition in T . In this case, we split w into X.t.Y ,where all the transitions in X are independent withall the transitions in T and t is the ﬁrst transition in
w that is dependent with some transition in T . Since
T is a persistent set in s, t must be in T (otherwise,
T would not be persistent in s). Therefore, t is independent with all the transitions in X. By property of
independence, this implies that the transition sequence
t.X.Y is executable from s. By applying the inductive
hypothesis to the recursive call Explore(S.t), we know
∀p : P C(S.t.X.Y, |S| + 1, p)
which implies (by the deﬁnition of P C) that∀p : P C(S.t.X.Y, |S|, p)
Since t is independent with all the transitions in X, wealso have that

By deﬁnition, S.w is itself a transition sequence from s0 in
AG and we havenext(last(S.w), proc(tn ))= next(last(S.t1 . . . tn ), proc(tn ))= tn(Although tn is enabled in last(S.t1 . . . tn−1 ), tn may nolonger be enabled in last(S.w), but this does not matterfor the proof.)
If proc(t) = proc(tn ) thent

= next(last(S), proc(t))= next(last(S.w), proc(t))= tnsince t is independent with all the transitions in w, contradicting that tn ∈ T . Hence proc(t) = proc(tn ).
Since t is in a diﬀerent process than tn and since t is
independent with all the transitions in w, we have
tn

=
=
=

next(last(S.w), proc(tn ))next(last(S.w.t), proc(tn ))next(last(S.t.w), proc(tn ))Let i = |S| + 1. Consider the postcondition
P C(S.t.w, i, proc(tn ))∀i ∈ dom(S.t.X.Y ) : i →S.t.X.Y p iﬀ

for the recursive call Explore(S.t). Clearly,

i →S.X.t.Y p

Therefore, by deﬁnition,i →S.t.w proc(tn )P C(S.t.X.Y, |S|, p) iﬀ P C(S.X.t.Y, |S|, p)(since t is in a diﬀerent process than tn and since t is independent with t1 , . . . , tn−1 ). In addition, we have (by deﬁnition of E):

We can thus conclude that∀p : P C(S.X.t.Y, |S|, p)
2. Suppose that all the transitions in w are independent
E(S.t.w, i, proc(tn )) ⊆with all the transitions in T and p ∈ backtrack(s).
{proc(t1 ), . . . , proc(tn−1 ), proc(tn )} ∩ enabled(s)ThenMoreover, we have by construction:(a) next(s, p) ∈ T ;(b) next(s, p) is independent with w;∀j ∈ dom(S.w) : j > i ⇒ j →S.t.w proc(tn )(c) p is a diﬀerent process from any transition in w;
Hence, by the postcondition P C for the recursive call Explore(S.t),(d) next(last(S.w), p) = next(last(S), p);either E(S.t.w, i, proc(tn )) is nonempty and at least one process in E(S.t.w, i, proc(tn )) is in backtrack(s), or E(S.t.w, i, proc(tn )) (e) ∀i ∈ dom(S) : i →S.w p iﬀ i →S p.
Thus, we have P C(S.w, |S|, p) iﬀ P C(S, |S|, p), and theis empty and all the processes enabled in s are in backtrack(s).
latter is directly established by the lines 3–9 of the alIn either cases, at least one transition among {t1 , . . . , tn } isgorithm for all p.
in T . This contradicts the assumption that t1 , . . . , tn ∈ T .
3. Suppose that all the transitions in w are independent
with all the transitions in T and p ∈ backtrack(s). Pickany t ∈ T . We then have that
We now turn to the proof of Theorem 1.
(a) proc(t) = p;
Theorem 1. Whenever a state s reached after a transi(b) t independent with all the transitions in w;
tion sequence S is backtracked during the search performed(c) next(last(S.w), p) = next(last(S.t.w), p);by the algorithm of Figure 3 in an acyclic state space, the(d) ∀i ∈ dom(S) : i →S.w p iﬀ i →S.t.w p.
postcondition P C for Explore(S) is satisﬁed, and the set T
Thus, we have P C(S.w, |S|, p) iﬀ P C(S.t.w, |S|, p). Byof transitions that have been explored from s is a persistent
applying the inductive hypothesis to the recursive call
set in s.
Explore(S.t), we know
Proof. Let∀p : P C(S.t.w, |S| + 1, p)
s = last(S)which implies (by the deﬁnition of P C) thatT = {next(s, p) | p ∈ backtrack(s)}∀p : P C(S.t.w, |S|, p)
The proof is by induction on the order in which states arewhich in turn implies
backtracked.
∀p : P C(S.w, |S|, p)(Base case) Since the state space AG is acyclic and since
as required.
the search is performed in depth-ﬁrst order, the ﬁrst backtracked state must be a deadlock where no transition is enabled. Therefore, the postcondition for that state becomes
12