# TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs

Samira Tasharofi, Rajesh K. Karmani, Steven Lauterburg, Axel Legay, Darko Marinov, Gul Agha

► To cite this version:

Samira Tasharofi, Rajesh K. Karmani, Steven Lauterburg, Axel Legay, Darko Marinov, et al. TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs. 14th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 32nd International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2012, Stockholm, Sweden. pp.219-234, 10.1007/978-3-642-30793-5_14 . hal-01528727

HAL Id: hal-01528727

https://inria.hal.science/hal-01528727

Submitted on 29 May 2017

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
TransDPOR: A Novel Dynamic Partial-Order
Reduction Technique for Testing Actor
Programs

Samira Tasharofi¹, Rajesh K. Karmani¹, Steven Lauterburg²,
Axel Legay³, Darko Marinov¹, and Gul Agha¹

¹ Department of Computer Science, University of Illinois, Urbana, IL 61801, USA
{tasharo1, rkumar8, marinov, agha}@illinois.edu

² Salisbury University, Salisbury, MD 21801, USA
stlauterburg@salisbury.edu

³ INRIA, Campus de Beaulieu, France
alegay@irisa.fr

**Abstract.** To detect hard-to-find concurrency bugs, testing tools try to systematically explore all possible interleavings of the transitions in a concurrent program. Unfortunately, because of the nondeterminism in concurrent programs, exhaustively exploring all interleavings is time-consuming and often computationally intractable. Speeding up such tools requires pruning the state space explored. Partial-order reduction (POR) techniques can substantially prune the number of explored interleavings. These techniques require defining a *dependency relation* on transitions in the program, and exploit independency among certain transitions to prune the state space.

We observe that actor systems, a prevalent class of programs where com-
putation entities communicate by exchanging messages, exhibit a depen-
dency relation among co-enabled transitions with an interesting prop-
erty: *transitivity*. This paper introduces a novel dynamic POR technique,
TransDPOR, that exploits the transitivity of the dependency relation in
actor systems. Empirical results show that leveraging transitivity speeds
up exploration by up to two orders of magnitude compared to existing
POR techniques.

# 1 Introduction

Concurrent programs are becoming increasingly important as multicore and net-
worked computing systems become the norm. A model of concurrent program-
ming that has been gaining popularity is the *actor model* [1]. The actor model is
used in many systems such as ActorFoundry, Asynchronous Agents, Charm++,
E, Erlang, and Scala.<fnref n="4" /> Actor programs consist of computing entities called ac-
tors (each with its own local state and thread of control) that communicate by
exchanging messages asynchronously. An actor *configuration* consists of the lo-
cal state of the actors and a set of *pending messages*. In response to receiving

<footnote n="4">⁴ For a more extensive list of actor systems, refer to [14].</footnote>
a message, an actor can update its local state, send messages, or create new
actors. At each step in the computation of an actor system [2], an actor from
the system is scheduled to process one of its pending messages. Assuming that
this processing terminates, the actor system transitions to a new configuration.

Concurrent systems, such as actor systems, present a significant challenge for
the testing and verification community. Such systems can exhibit exponentially
many different interleavings of concurrent transitions. In the case of actors, the
execution of an actor program can have different results from an exponentially
large number of potential interleavings of messages. The nondeterminism in actor
systems stems from the fact that multiple messages sent to the same actor may
be processed in different orders, thus resulting in different configurations, and
only some specific interleavings/configurations may reveal bugs.

A naïve exploration that would explore all the interleavings to reach all
possible system configurations does not scale. Partial-order reduction (POR)
techniques [5, 6, 8, 9, 11, 20, 22, 24–27, 29] can be applied to help mitigate the re-
sulting state-space explosion by exploring a representative subset of all possible
interleavings. POR techniques have been widely used for testing and verifica-
tion of concurrent protocols and software, including in tools such as SPIN [13],
VeriSoft [8], and Java PathFinder [28].

To prune state-space exploration, POR techniques explore a *subset* of the set of enabled transitions in each configuration. This subset should be selected such that by exploring only the transitions in the subset, all the properties of interest are guaranteed to be preserved. For example, in one of the popular POR techniques, this subset is defined as a *persistent set* [9]. POR techniques require the definition of a *dependency relation* between transitions in the system and then exploit the independency between certain transitions to compute this subset. A valid dependency relation is a reflexive and symmetric (but *not necessarily transitive*) binary relation on the transitions.

Traditionally, dependencies among transitions, such as in *persistent sets* [9] proposed by Godefroid, were computed via static analysis. More recently, Flanagan and Godefroid introduced a POR algorithm, called dynamic POR (DPOR), that relies on dynamic analysis for computing dependencies [6]. More precisely, this algorithm maintains for each configuration a *backtrack set* and updates the backtrack sets during the execution of a test program. Flanagan and Godefroid proved that the computed backtrack sets are persistent sets [6]. They show that DPOR can significantly improve on POR techniques based on static analysis by computing smaller persistent sets. Note that DPOR is *stateless*, i.e., it does not store states/configurations across different executions.

In this paper, we leverage the fact that actors do not share their states,
and we define a dependency relation between the transitions that is *transitive*
on the transitions enabled in the same configuration (called co-enabled transi-
tions). We present a new stateless dynamic POR algorithm, called *TransDPOR*
which extends DPOR to take advantage of the transitive dependency relations
in actor systems. We show that TransDPOR in some cases explores fewer con-
figurations/transitions than DPOR, but it never explores more. TransDPOR is
complete like DPOR, i.e., when the state space is acyclic, TransDPOR can reach
every deadlock or local safety violation in the system (space limitations do not
allow us to provide a proof of these properties in this version of the paper).

We implemented TransDPOR in Basset [17], a tool for the systematic testing of actor programs written in the Scala programming language [12] or the Actor-Foundry library for Java [21]. TransDPOR code is publicly available with Bas-set at http://mir.cs.illinois.edu/basset. We compare TransDPOR and DPOR (we previously adapted the original DPOR algorithm to work for actor systems [18]) on eight programs without bugs and three programs with bugs. The experimental results show that TransDPOR reduces the number of tran-sitions executed during state space exploration by 2.39x on average and up to 163.80x over DPOR. When we combine TransDPOR and DPOR with sleep sets (a traditional POR technique) [7], we find that TransDPOR can find bugs up to 2.56x faster than DPOR.

## 2 Illustrative Example

To illustrate how TransDPOR works, we use the simple actor program shown in Figure 1. It has four actors: one *master* (which is the entry point of the program), one *registry server*, and two *workers*. The registry keeps track of the actors registered in the system. The master first registers itself by sending its ID to the registry. It then creates two workers and sends them each a message with the registry's ID. After receiving the message, each worker sends its ID to the registry. In the comments for *send* statements, we labeled each of the five messages: *worker 1* and *worker 2* receive messages *w*₁ and *w*₂ respectively, and the registry eventually receives three messages—*r*₀, *r*₁, and *r*₂. In this example, the nondeterminism is the order in which the registry receives these three mes-sages and thus assigns the values for its three local variables. For example, the program could have a bug if it assumes that *r*₀ is received before *r*₁ and *r*₂.

We observe that without any assumption one would have to explore up to 5! permutations of the messages exchanged between actors. We will see that this number reduces considerably by using DPOR algorithms that consider a basic property in the actor model. In the actor model, actors have no shared states but only communicate by exchanging messages. Since processing a message in one actor cannot change the states of other actors, only the transitions that process the messages sent to the same actor are *dependent*. Hence, when exploring actor systems, to reach all local safety violations and deadlocks, it suffices to explore different interleavings of processing messages in each actor, i.e., it is not necessary to explore interleavings of processing messages across different actors. For example, if $m_a$ and $m_b$ respectively stand for processing message $m_a$ in actor a and message $m_b$ in actor b, it suffices to explore only one of interleavings $m_a.m_b$ or $m_b.m_a$.

Figure 1 shows the state spaces that DPOR and TransDPOR explore for our example program. Each node represents a configuration, and each edge shows a transition labeled with the message being processed.
<figure><img src="image_2.png" /></figure>

<figure><img src="image_3.png" /><figcaption>Fig. 1. The registry example and the state space explored by DPOR and TransDPOR.</figcaption></figure>

Let us first focus on DPOR. Specifically, this algorithm first executes an actor program to obtain an execution path and for each configuration keeps a *backtrack* set of all messages to be explored from that configuration. These sets start empty but grow as DPOR discovers dependencies among transitions. In our example, DPOR first executes the path $r_0.w_1.w_2.r_1.r_2$. Then, the algorithm observes that $r_1$ and $r_2$ are sent to the same *registry* actor, which makes them dependent. DPOR thus adds $r_2$ to the backtrack set of configuration 3. Moreover, because $r_1$ and $r_2$ are dependent with $r_0$ but not enabled in the initial configuration, DPOR adds the messages that can produce $r_1$ and $r_2$—namely, $w_1$ and $w_2$—to the backtrack set of the configuration 0 so that different interleavings of those messages with $r_0$ can be explored. After the first path, DPOR backtracks in a depth-first manner to configuration 3 and executes $r_0.w_1.w_2.r_2.r_1$. It then backtracks to configuration 0 and explores $w_1$ and $w_2$ from that configuration. Observe that some redundant paths such as $r_0.w_2.w_1.r_2.r_1$ have been removed from the exploration. In the end, DPOR explores 24 paths. Recall that DPOR is stateless, i.e., it does not store the history of previous explored paths and every time it backtracks to a configuration it chooses a message from backtrack set and runs the program nondeterministically.

While the above pruning is already an improvement over full exploration, it does not fully exploit the semantics of the actor model. More precisely, one can observe that adding $w_1$ to the backtrack set of the initial configuration would be
enough to explore all possible permutations of the messages processed in each
actor, i.e., all paths of the subtree that starts with $w_2$ are redundant. Intuitively
this is because only *registry* can receive more than one message and different
permutations of the three messages sent to the registry have been explored in
the previous paths. The same holds for the backtrack set of configuration 8 where
the subtree that starts with $r_1$ is redundant.

Our new POR algorithm TransDPOR detects these redundant paths and as
a result explores only 10 paths in this example (those *not* included in dotted
boxes in Figure 1). The main idea in TransDPOR is to add (at most) one new
message to the backtrack set for a configuration. After the newly added mes-
sage is explored, *only if it is necessary* TransDPOR adds more messages to the
backtrack set. TransDPOR implements this idea by attaching a boolean flag,
*freeze* flag, to each configuration. It only adds a message to the backtrack set
of a particular configuration if the *freeze* flag of that configuration is not set.
While initially this flag is not set in any configuration, TransDPOR sets this
flag when it adds a message to the backtrack set of a configuration. It resets the
flag when it backtracks to a configuration and explores a new message from that
configuration.

In the example, when TransDPOR adds $w_1$ to the backtrack set of config-
uration 0, it sets the *freeze* flag and that prevents the addition of $w_2$ to the
backtrack set of configuration 0. The same situation happens for the backtrack
set of configuration 8. That leads to smaller backtrack sets than DPOR for the
two configurations 0 and 8. This reduction is allowed due to the *transitivity*
of the dependency relation between the transitions that may be co-enabled in
a configuration, and we show that this reduction does not miss any bug that
DPOR can find. An example of adding all messages can be seen in configuration
15 (all three messages $r_0, r_1$, and $r_2$ are added to the backtrack set of the config-
uration). In this configuration, after exploring $r_0$, both $r_1$ and $r_2$ are dependent
with $r_0$, but TransDPOR only adds $r_1$ to the backtrack set of configuration 15.
The *freeze* flag prevents the addition of $r_2$ to the backtrack set at the same time.
Due to the transitivity of the dependency relation, $r_1$ and $r_2$ are also dependent.
Thus, after exploring $r_1$ from configuration 15, the *freeze* flag is reset and $r_2$ is
added to the backtrack set of configuration 15. The algorithm will end up adding
all three messages $r_0, r_1$, and $r_2$ to the backtrack set of configuration 15 and will
not miss any permutation of these three messages.

# 3 Actor Semantics

While the above example relied on an intuitive understanding of actors, we now
define the semantics of actor programs precisely. Formally, we view actor pro-
grams as state-transition systems. A (global) *state* of an actor program, termed
a *configuration*, in notation $\kappa = \langle \alpha, \mu \rangle$, consists of a map $\alpha : \mathcal{A} \to \mathcal{L}$, where $\mathcal{A}$ are
actor identifiers and $\mathcal{L}$ are possible local states, and a set of *pending* messages
$\mu \subseteq \mathcal{M}$, where $\mathcal{M}$ is the set of all possible messages in the system. We use $\mathbb{K}$ to
denote the set of all configurations in a system and $\mathit{pending}(\kappa)$ to denote the
set of pending messages for $\kappa \in K$. Each message is a tuple of receiver actor, content, and unique message identifier. Conceptually, the messages in $\mu$ can be partitioned according to their receiver actor, i.e., $\mu$ is a union of disjoint message sets, one for every actor in the system.

At each step in execution, an actor processes a message from its message set: the actor removes the message from its set and potentially updates its local state, sends messages to other actors or itself, and creates new actors. The processing can be viewed as a single, atomic macro-step [2] because actors do not share state [14]. The actor model allows constraints that enable or disable processing of some message by an actor depending on its local state. Formally, for an actor $a$, its constraint $c_a \subseteq L \times M$ is a predicate on the local state of the actor and the set of messages.

**Definition 1** The transition $t_m$ for a message $m$ is a partial function $t_m: K \to K$. For a given $\langle \alpha, \mu \rangle \in K$, let the receiver of $m$ be actor $a$ with the local state $s$ and constraint $c_a$; the transition $t_m$ is enabled if $t_m(\langle \alpha, \mu \rangle)$ is defined (i.e., $\alpha(a) = s$ and $m \in \mu$) and $\langle s, m \rangle \in c_a$. If $t_m$ is enabled, it can be executed and produces a new configuration, updating the local state of the actor from $s$ to $s'$, sending messages $out_s(t_m)$, and creating new actors with their initial local state $new_s(t_m)$:

$$ \langle \alpha, \mu \rangle \xrightarrow{t_m} \langle \alpha[a \mapsto s'] \cup new_s(t_m), \mu\{m\} \cup out_s(t_m) \rangle $$

We denote $msg(t_m) = m$ and $actor(t_m) = a$. We denote with $out(t_m)$ and $new(t_m)$ the sets of all new messages and actors, respectively, that the transition $t_m$ can create for any local state $s$. Observe that as is usual in actor semantics, we assume that the behavior of an actor in response to a message is deterministic. Moreover, we assume that all transitions terminate–this is a standard assumption in testing programs. Thus, the execution of a transition $t$ in a configuration $\kappa$ leads to a unique successor $\kappa'$ (up to the choice of fresh identifiers for new actors and messages).

# 4 Definitions for Partial-Order Reduction

We introduce several terms and definitions required for presenting our TransDPOR algorithm, following the DPOR presentation style of Flanagan and Godefroid [6]. Then we present an important property of the actor model that will be used to improve DPOR. Let $\tau$ be the set of all transitions in the system and $\tau^*$ be the set of all transition sequences. We write $\kappa \stackrel{\tau^*}{\Rightarrow} \kappa'$ to denote that the execution of finite sequence $\omega \in \tau^*$ leads from $\kappa$ to $\kappa'$. A configuration in which no transition is enabled is called a deadlock or terminating configuration. A transition sequence $S$ of an actor system is a (finite) sequence of transitions $t_1.t_2...t_n$ where there exist configurations $\kappa_0, ..., \kappa_n$ such that $\kappa_0$ is the initial configuration and $\kappa_0 \xrightarrow{t_1} \kappa_1 \xrightarrow{t_2} ... \xrightarrow{t_n} \kappa_n$. A transition sequence that ends in a deadlock or terminating configuration is called an execution path of the system.
We define an actor system as a transition system $A_G = \langle K, \Delta, \kappa_0 \rangle$, where $\Delta = \{\langle \kappa, \kappa' \rangle \mid \exists t \in \tau : \kappa \xrightarrow{t} \kappa' \}$ and $\kappa_0$ is the initial configuration. We first recap the general definition for a valid dependency relation between transitions [6], then we show how to adapt it to the actor model.

**Definition 2** Let $t_1$ and $t_2$ be two transitions of an actor system. We say that $t_1$ and $t_2$ are independent if for all configurations $\kappa$ in the state space $A_G$ of the system:

- if $t_1$ is enabled in $\kappa$ and $\kappa \xrightarrow{t_1} \kappa'$, then $t_2$ is enabled in $\kappa$ iff $t_2$ is enabled in $\kappa'$ (i.e., independent transitions cannot disable or enable each other); and

- if $t_1$ and $t_2$ are enabled in $\kappa$, there is a unique configuration $\kappa'$ such that $\kappa \xrightarrow{t_1,t_2} \kappa'$ and $\kappa \xrightarrow{t_2,t_1} \kappa'$ (i.e., enabled independent transitions must commute).

The reflexive and symmetric binary relation $D$ is a valid dependency relation on $\tau$ iff $D = \{(t_1, t_2) | t_1, t_2 \text{ are not independent transitions}\}$. The pair of transitions $(t_1, t_2)$ are said to be dependent iff they belong to a valid dependency relation.

We observe that for actor programs, a transition $t_m$ cannot be enabled until the receiver actor for $m$ is created and the message $m$ is sent ($m$ becomes pending). Second, once a message $m$ is sent to an actor $a$, only transitions of the actor $a$ can enable or disable the transition $t_m$ that processes the message $m$. In other words, the constraint $c_a$ does not depend on the global state but only on the local state of $a$ and the message $m$. Therefore, we can easily show that two transitions $t_1$ and $t_2$ are independent if $\text{actor}(t_1) \neq \text{actor}(t_2)$, $\text{msg}(t_1) \notin \text{out}(t_2)$, and $\text{actor}(t_1) \notin \text{new}(t_2)$. Based on these observations, we can cast Definition 2 in the actor programs setting to obtain the following proposition.

**Proposition 1.** Two transitions $t_1, t_2 \in \tau$ are dependent iff one of the following conditions holds:

- $\text{actor}(t_1) = \text{actor}(t_2)$; or

- $\text{msg}(t_1) \in \text{out}(t_2)$ or $\text{msg}(t_2) \in \text{out}(t_1)$; or

- $\text{actor}(t_1) \in \text{new}(t_2)$ or $\text{actor}(t_2) \in \text{new}(t_1)$.

Based on Proposition 1, one can extract an important property of our model, which will be used to improve over DPOR. We say that two transitions $t_1$ and $t_2$ may be co-enabled if there may exist some configuration in which both $t_1$ and $t_2$ are enabled. For a shorthand, we introduce a binary relation on transitions called *race relation*; we say that a pair of transitions $\langle t_1, t_2 \rangle$ are *in race* if they are dependent and may be co-enabled. A key observation is that if $\langle t_1, t_2 \rangle$ are in race, then $\text{actor}(t_1) = \text{actor}(t_2)$. Indeed, while our definition of dependency allows two other cases ($\text{msg}(t_1) \in \text{out}(t_2)$ or $\text{actor}(t_1) \in \text{new}(t_2)$), the transitions that satisfy those two other cases can never be co-enabled (because those cases require that the message or actor for $t_1$ be created after the execution of $t_2$). As a result, the following proposition holds.

**Proposition 2.** The race relation is reflexive, symmetric, and transitive.
Given a transition sequence, two adjacent transitions that are independent can be permuted without changing the behavior of the transition sequence. To formalize the set of equivalent transition sequences, we recap the happens-before relation presented in [6].

**Definition 3** The happens-before relation $\rightarrow_S$ for a transition sequence $S = t_1...t_n$ is the smallest relation on $\{1,...,n\}$ such that (1) if $i \le j$ and $t_i$ is dependent with $t_j$, then $i \rightarrow_S j$; and (2) $\rightarrow_S$ is transitively closed.

Since happens-before relation is a partial order [6], we introduce the following equivalence relation:

**Definition 4** Two transition sequences $S_1$ and $S_2$ are equivalent iff they have the same set of transitions, and they are linearizations of the same happens-before relation.

We use $[S]$ to denote the set of transition sequences that are equivalent to $S$.

# 5 TransDPOR: A New DPOR Algorithm

Figure 2 presents our TransDPOR algorithm, which explores the state space of an actor system dynamically in a depth-first manner. The underlined parts are the differences between TransDPOR and the original DPOR [6] adapted for actors. The input to the algorithm is a transition sequence $S$ (Line 1). Notation-wise, for a sequence $S = t_1...t_n$: $dom(S)$ is the set $\{1,...,n\}$; $S_i$ for $i \in dom(S)$ is transition $t_i$; $pre(S, i)$ for $i \in dom(S)$ is the configuration in which $t_i$ is executed; and $last(S)$ is the configuration reached after executing $S$. We denote with $next(\kappa, m)$ the transition that processes message $m$ in the configuration $\kappa$. Following [6], we also use a variant of the happens-before relation to determine if some messages are sent as the result of executing other transitions:

**Definition 5** In a transition sequence $S$, the relation $i \rightarrow_S m$ holds for $i \in dom(S)$ and message $m$ iff either (1) $m \in out(S_i)$ or (2) $\exists j \in dom(S)$ such that $i \rightarrow_S j$ and $m \in out(S_j)$.

Like DPOR, TransDPOR maintains a backtrack set *backtrack*(κ), which keeps the messages to be explored from each configuration κ in the input sequence $S$. The main difference is that, in addition, TransDPOR also uses a boolean flag *freeze*(κ). As explained in Section 2, this flag can prevent adding some messages to *backtrack*(κ), and hence it reduces the size of *backtrack*(κ). As we shall see, because of the transitivity of the race relation, TransDPOR can use this flag to improve over DPOR.

TransDPOR starts by finding the current configuration $\kappa$ for the input sequence $S$ (Line 2). For every message $m$ in *pending*(κ) (Line 3), it considers the transition $next(\kappa, m)$ for processing that message. It finds the *last* transition $i$ in the sequence $S$ which is in the race with $next(\kappa, m)$, i.e., $actor(S_i) = actor(next(\kappa, m))$ and $i \not\rightarrow_S m$. If the *freeze* flag is set in $pre(S, i)$, the algorithm
0: Initially: Explore(Ø);
1: Explore(S) {
2:   let κ = last(S);
3:   for all messages m ∈ pending(κ) {
4:     if ∃i = max({i ∈ dom(S) | Sᵢ is dependent and
                      may be co-enabled with next(κ, m) and i ≠ S m}) {
5:     if (¬freeze(pre(S, i))) {
6:       let E = {m' ∈ enabled(pre(S, i)) | m' = m or ∃j ∈ dom(S) | j > i and
                                          m' = msg(Sⱼ) and j → S m and
                                          j = min({j ∈ dom(S) | j > i and j → S m})};
7:       if (E \ backtrack(pre(S, i)) ≠ φ) {
8:         add any m' ∈ E to backtrack(pre(S, i));
9:         freeze(pre(S, i)) := true;
10:     } else add all m in enabled(pre(S, i)) to backtrack(pre(S, i)) */;
11:   } } 7
12:   let done = Ø;
13:   while (∃m ∈ (backtrack(κ) \ done)) {
14:     add m to done;
15:     freeze(κ) := false;
16:   }
17: }
18: }

<caption>Fig. 2. The TransDPOR algorithm (The differences with DPOR are underlined).</caption>

does not update the backtrack set for pre(S, i) (Line 4'); this line does not exist in
DPOR and is a major difference between TransDPOR and DPOR. Effectively,
this step prevents additional messages in backtrack(pre(S, i)) until the previ-
ously added message is explored by the algorithm. Due to the transitivity of our
race relation, we prove that the messages not added right away are added later if
necessary to explore them from κ. However, as TransDPOR does not add them
right away, it may terminate faster than DPOR. If freeze(pre(S, i)) is not set, the
algorithm next finds the message that should be added to backtrack(pre(S, i)) by
computing the set E (Line 5) from the messages whose transitions are enabled in
pre(S, i). If m is enabled in pre(S, i) it is added to E (m' = m); otherwise a mes-
sage m' is added to E if its transition is the first transition after S<sub>i</sub> that happens
before m (in this case, m is produced as a result of executing other transitions
after S<sub>i</sub>). Note that our approach for computing E differs from DPOR in that it
finds the minimum index j > i such that j happens before m, while DPOR finds
all j > i such that j happens before m. As a result of this change, E in our case
has at most one element. After computing E, if it contains a message that is not
already in backtrack(pre(S, i)), the message is added to backtrack(pre(S, i)),
and the freeze flag is set (Line 6). In DPOR, if E is not empty, it can have more
than one message, and the algorithm nondeterministically chooses one message
to add to backtrack(pre(S, i)) (hence "add any").
If $E$ is empty, then $m$ is in $\mathit{pending}(\mathit{pre}(S, i))$ but $t_m$ is not enabled in $\mathit{pre}(S, i)$. Intuitively, because of the transitivity of race relation, every enabled message in $\mathit{pre}(S, i)$ that can enable $t_m$ would be in race with $S_i$ (all of them belong to the same actor) and would be added to $\mathit{backtrack}(\mathit{pre}(S, i))$ either in the next iteration of the *for* loop or in the recursive calls to *Explore*. Therefore, TransDPOR does not add anything to $\mathit{backtrack}(\mathit{pre}(S, i))$ at this point (Line 7 is effectively deleted). In contrast, in DPOR, if $E$ is empty, the algorithm adds all messages from $E$ to $\mathit{backtrack}(\mathit{pre}(S, i))$.

After Lines 3-9 update the backtrack set of configurations seen previously in the sequence $S$, Lines 10-17 process the messages from the current configuration $\kappa$. The algorithm nondeterministically chooses an enabled message from $\kappa$ (Line 10) to initialize $\mathit{backtrack}(\kappa)$ (Line 11). It then processes all messages from the backtrack set that have not been explored before (Line 13). Every time the algorithm backtracks to $\kappa$ and explores a new message, it adds that message to the *done* set and resets the *freeze* flag (Line 14'). The algorithm finally recursively calls itself with the transition sequence extended with the $\mathit{next}(\kappa, m)$.

In our example in Section 2, once TransDPOR adds $w_1$ to $\mathit{backtrack}(\kappa_0)$, it sets $\mathit{freeze}(\kappa_0)$, which prevents from adding $w_2$ to $\mathit{backtrack}(\kappa_0)$. After the algorithm explores $w_1$ from $\kappa_0$, it resets $\mathit{freeze}(\kappa_0)$, but because none of the messages in paths that start with $w_1$ from $\kappa_0$ is in the race with $w_1$, no message is added to the $\mathit{backtrack}(\kappa_0)$ ($w_2$ is not added). Similarly, in $\kappa_8$, adding $w_2$ to $\mathit{backtrack}(\kappa_8)$ prevents from adding $r_1$. After exploring $w_2$ from $\kappa_8$, because none of the messages $r_0$, $r_1$, and $r_2$ are in the race with $w_2$, no message is added to $\mathit{backtrack}(\kappa_8)$ ($r_1$ is not added). On the other hand, consider $\kappa_{15}$. After exploring $r_0$, both $r_1$ and $r_2$ are in the race with $r_0$. Because of the *freeze* flag, the algorithm only adds $r_1$ to $\mathit{backtrack}(\kappa_{15})$. After exploring $r_1$ from $\kappa_{15}$, because of *transitivity* of race relation, $r_2$ is also in the race with $r_1$ and it is eventually added to $\mathit{backtrack}(\kappa_{15})$.

When the loop terminates, the exploration from $\kappa$ is finished, and the algorithm backtracks to the previous configuration. Note that the algorithm is stateless, i.e., it does not store states/configurations across different execution paths. However, it may store configurations for the current path on a stack, depending on the implementation strategy.

It is trivial to show that TransDPOR never explores more execution paths than DPOR. As a result of the changes that we have made in Lines 4' and 7 of the algorithm, in each call to *Explore*($S$), we add either fewer or the same number of messages to the backtrack set of each configuration $\kappa$.

Theorem 1 states that by starting from a fix initial configuration if $A_G$ is acyclic, TransDPOR will explore at least one execution path from each set of equivalent execution paths in $A_G$, i.e., it can detect any deadlock and local safety violation in the program [8].

**Theorem 1.** In a program $\mathcal{P}$, by starting from an initial configuration, let $A_G$ be the acyclic state-space graph and $A_R$ be the reduced state space explored by TransDPOR. If $\Omega_G$ and $\Omega_R$ denote the set of execution paths of $\mathcal{P}$ in $A_G$ and $A_R$ respectively, then $\forall \omega \in \Omega_G, \exists \omega' \in \Omega_R$ such that $\omega' \in [\omega]$.
# 6 Implementation and Evaluation

To compare TransDPOR and DPOR, we implemented TransDPOR in the Basset tool [17]. Basset provides an extensible environment for testing Java-based actor programs written in the Scala Actors library [12] or ActorFoundry [21]. We use vector clocks [16] to track the happens-before relation at runtime as shown in [24].

We use eight different subject programs in our evaluation. Each actor program was either originally implemented in ActorFoundry or ported to it for this evaluation. *fibonacci* computes the $n^{th}$ element in the Fibonacci sequence. In this case, we show the result for $n = 5$. *quicksort* is a distributed sorting implementation using a standard divide-and-conquer strategy to carry out the computation. *pi* is a porting of a publicly available [23] MPI example, which computes an approximation of $\pi$ by distributing the task among a set of worker actors. The results shown here are for a configuration with five worker actors. *pipesort* is a modified version of the sorting algorithm used in the dCUTE study [24]. *chameneos* is an implementation of the *chameneos-redux* benchmark from the Great Language Shootout (http://shootout.alioth.debian.org). *leader* is an implementation of a leader election algorithm previously used in the dCUTE study [24]. *shortpath* is an implementation of the Chandy-Misra shortest path algorithm [4]. This subject appears twice in the results: once for a graph with 4 nodes (*shortpath4*) and once for a graph with 5 nodes (*shortpath5*), where the two graphs are dissimilar. *regsim* is a server registration simulation. The numbers with the name of subjects, if available, represent the values of program parameters. We performed all experiments using Sun's JVM 1.6.0_20-b02 on a 2.93GHz Intel Core(TM)i7 running Ubuntu release 10.04.

Our recent work [18] shows that the effectiveness of DPOR techniques is highly sensitive to the *order* in which messages are explored. However, one cannot easily determine before the exploration which order will work the best. For that reason, we present results for three ordering heuristics, *ECA*, *LCA*, and *FIFO*. *ECA* sorts the messages based on the time they are sent in the ascending order. *ECA* sorts messages according to the creation time of the receiving actor in ascending order; messages for the *earliest created actor* are considered first. *LCA* is similar to *ECA* but sorts the actors in descending order of their creation time.

To illustrate the speedup that can be achieved using TransDPOR, we performed a set of nine experiments which compare explorations performed using DPOR with explorations performed using TransDPOR. Table 1 shows the results for these experiments. For each subject and DPOR technique, we show the number of paths executed in their entirety while exploring the specified subjects, the total number of transitions executed (across all execution paths), the total exploration time in seconds, and memory usage in MB. Since the length of paths might be different in a program, and the time is dependent on the platform and noise in the system, we focus on the number of explored transitions as the primary metric for comparison.

The experiments suggest that TransDPOR can explore up to *over two orders of magnitude* fewer transitions than DPOR. In all the experiments TransDPOR
<table><caption>Table 1. Comparison of TransDPOR and DPOR</caption><thead><tr><th rowspan="2">Heur.</th><th rowspan="2">Subject</th><th colspan="4">DPOR</th><th colspan="4">TransDPOR</th><th colspan="4">Speedup</th></tr><tr><th># of Paths</th><th># of Trans</th><th>time [sec]</th><th>mem [MB]</th><th># of Paths</th><th># of Trans</th><th>time [sec]</th><th>mem [MB]</th><th># of Paths</th><th># of Trans</th><th>time [sec]</th><th>mem [MB]</th></tr></thead><tbody><tr><td>FIFO</td><td rowspan="3">fib5</td><td>40</td><td>203</td><td>5</td><td>176</td><td>40</td><td>203</td><td>4</td><td>176</td><td>1.00x</td><td>1.00x</td><td>1.25x</td><td>1.00x</td></tr><tr><td>ECA</td><td>327</td><td>1650</td><td>28</td><td>455</td><td>203</td><td>1051</td><td>18</td><td>377</td><td>1.61x</td><td>1.57x</td><td>1.56x</td><td>1.21x</td></tr><tr><td>LCA</td><td>16</td><td>91</td><td>3</td><td>173</td><td>16</td><td>91</td><td>3</td><td>159</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>1.09x</td></tr><tr><td>FIFO</td><td rowspan="3">quicksort6</td><td>368</td><td>1586</td><td>26</td><td>343</td><td>368</td><td>1586</td><td>26</td><td>463</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>0.74x</td></tr><tr><td>ECA</td><td>3822</td><td>16766</td><td>264</td><td>381</td><td>1519</td><td>6992</td><td>115</td><td>751</td><td>2.52x</td><td>2.40x</td><td>2.30x</td><td>0.51x</td></tr><tr><td>LCA</td><td>32</td><td>156</td><td>4</td><td>197</td><td>32</td><td>156</td><td>4</td><td>179</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>1.10x</td></tr><tr><td>FIFO</td><td rowspan="3">pi5</td><td>120</td><td>931</td><td>16</td><td>265</td><td>120</td><td>931</td><td>16</td><td>374</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>0.71x</td></tr><tr><td>ECA</td><td>120</td><td>931</td><td>16</td><td>263</td><td>120</td><td>931</td><td>16</td><td>374</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>0.70x</td></tr><tr><td>LCA</td><td>19845</td><td>156070</td><td>2509</td><td>451</td><td>312</td><td>2452</td><td>40</td><td>376</td><td>63.61x</td><td>63.65x</td><td>62.73x</td><td>1.20x</td></tr><tr><td>FIFO</td><td rowspan="3">pipesort4</td><td>1791</td><td>8562</td><td>101</td><td>375</td><td>755</td><td>3541</td><td>45</td><td>375</td><td>2.37x</td><td>2.42x</td><td>2.24x</td><td>1.00x</td></tr><tr><td>ECA</td><td>288</td><td>1293</td><td>17</td><td>374</td><td>288</td><td>1293</td><td>18</td><td>450</td><td>1.00x</td><td>1.00x</td><td>0.94x</td><td>0.83x</td></tr><tr><td>LCA</td><td>5970</td><td>32385</td><td>361</td><td>375</td><td>2221</td><td>11999</td><td>136</td><td>451</td><td>2.69x</td><td>2.70x</td><td>2.65x</td><td>0.83x</td></tr><tr><td>FIFO</td><td rowspan="3">chameneos2</td><td>3240</td><td>19459</td><td>233</td><td>376</td><td>600</td><td>3673</td><td>44</td><td>376</td><td>5.40x</td><td>5.30x</td><td>5.30x</td><td>1.00x</td></tr><tr><td>ECA</td><td>19683</td><td>118197</td><td>1360</td><td>550</td><td>1728</td><td>10554</td><td>123</td><td>374</td><td>11.39x</td><td>11.20x</td><td>11.06x</td><td>1.47x</td></tr><tr><td>LCA</td><td>216</td><td>1231</td><td>16</td><td>375</td><td>216</td><td>1231</td><td>16</td><td>453</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>0.83x</td></tr><tr><td>FIFO</td><td rowspan="3">leader4</td><td>18098</td><td>107780</td><td>26872</td><td>336</td><td>14984</td><td>86889</td><td>37516</td><td>341</td><td>1.21x</td><td>1.24x</td><td>0.72x</td><td>0.99x</td></tr><tr><td>ECA</td><td>11957</td><td>68373</td><td>1207</td><td>240</td><td>11909</td><td>68125</td><td>1312</td><td>266</td><td>1.00x</td><td>1.00x</td><td>0.92x</td><td>0.90x</td></tr><tr><td>LCA</td><td>39238</td><td>236330</td><td>4301</td><td>634</td><td>27287</td><td>163030</td><td>3120</td><td>525</td><td>1.44x</td><td>1.45x</td><td>1.38x</td><td>1.21x</td></tr><tr><td>FIFO</td><td rowspan="3">shortpath4</td><td>238</td><td>910</td><td>12</td><td>261</td><td>238</td><td>910</td><td>12</td><td>261</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>1.00x</td></tr><tr><td>ECA</td><td>392</td><td>1464</td><td>20</td><td>262</td><td>392</td><td>1464</td><td>19</td><td>260x</td><td>1.00x</td><td>1.00x</td><td>1.05x</td><td>1.01x</td></tr><tr><td>LCA</td><td>640</td><td>2158</td><td>27</td><td>260</td><td>370</td><td>1337</td><td>17</td><td>264</td><td>1.73x</td><td>1.61x</td><td>1.59x</td><td>0.98x</td></tr><tr><td>FIFO</td><td rowspan="3">shortpath5</td><td>528</td><td>2443</td><td>32</td><td>454</td><td>528</td><td>2443</td><td>33</td><td>372</td><td>1.00x</td><td>1.00x</td><td>0.97x</td><td>1.22x</td></tr><tr><td>ECA</td><td>2658</td><td>8476</td><td>104</td><td>368</td><td>1170</td><td>3737</td><td>49</td><td>261</td><td>2.27x</td><td>2.27x</td><td>2.12x</td><td>1.41x</td></tr><tr><td>LCA</td><td>1865</td><td>7076</td><td>93</td><td>375</td><td>1272</td><td>4704</td><td>61</td><td>375</td><td>1.47x</td><td>1.50x</td><td>1.52x</td><td>1.00x</td></tr><tr><td>FIFO</td><td rowspan="3">regsim</td><td>211750</td><td>590835</td><td>14440</td><td>989</td><td>1320</td><td>3607</td><td>64</td><td>76</td><td>160.42x</td><td>163.80x</td><td>225.63x</td><td>13.01x</td></tr><tr><td>ECA</td><td>208034</td><td>591454</td><td>14782</td><td>989</td><td>1950</td><td>5434</td><td>93</td><td>79</td><td>106.68x</td><td>108.84x</td><td>158.95x</td><td>12.52x</td></tr><tr><td>LCA</td><td>720</td><td>1962</td><td>34</td><td>64</td><td>720</td><td>1962</td><td>36</td><td>66</td><td>1.00x</td><td>1.00x</td><td>0.94x</td><td>0.97x</td></tr><tr><td colspan="11" style="text-align: right;">Max</td><td>160.42x</td><td>163.80x</td><td>225.63x</td><td>13.01x</td></tr><tr><td colspan="11" style="text-align: right;">Average</td><td>2.39x</td><td>2.39x</td><td>2.38x</td><td>1.18x</td></tr></tbody></table>

has a speedup for at least one heuristic, and it is *never* the case that the use of TransDPOR results in more executed transitions than DPOR. Although the speedup in transitions executed can at times be small (e.g., only 1.24x or less for leader), it can be also quite significant. For chameneos, the speedup is over 11x, and for regsim, it is over 163x. The regsim experiment using DPOR did not complete in 4 hours for either FIFO or ECA.

**Combining with Sleep Sets:** Sleep sets is a POR technique based on the history of exploration [7]. Specifically, sleep sets record the transitions that have already been explored from a particular configuration, and avoid exploring them in successor configurations until some condition is met. Sleep sets can further prune the number of transitions and configurations that are explored [8]. In the case where the state space is acyclic (which is the assumption in this paper), sleep sets can be combined with dynamic POR in exactly the same way as static POR [6]. We implemented a variant of TransDPOR that is combined with sleep sets and compared it with the combination of DPOR with sleep sets.

In addition to the eight programs used in our initial experiment, we added three more programs. These programs have such a large state space that the exploration times out without sleep sets. diningphil is an implementation of the dining philosopher protocol in ActorFoundry. minesweeper is a simulation of the minesweeper game written using the Scala Actors library. le-erlang is an implementation of a fault-tolerant leader election algorithm for Erlang that had been running on Ericsson switches. Some bugs were found in the program by Arts et al. [3] in the presence of node failures. We re-implemented the buggy program in ActorFoundry in order to test it using our tool.
<table><caption>Table 2. Comparison of TransDPOR+Sleep sets and DPOR+Sleep sets</caption><thead><tr><th rowspan="2">Heur.</th><th rowspan="2">Subject</th><th colspan="4">DPOR+S</th><th colspan="4">TransDPOR+S</th><th colspan="4">Speedup</th></tr><tr><th># of Paths</th><th># of Trans</th><th>time [sec]</th><th>mem [MB]</th><th># of Paths</th><th># of Trans</th><th>time [sec]</th><th>mem [MB]</th><th># of Paths</th><th># of Trans</th><th>time [sec]</th><th>mem [MB]</th></tr></thead><tbody><tr><td>FIFO</td><td rowspan="3">fib5</td><td>16</td><td>101</td><td>3</td><td>173</td><td>16</td><td>101</td><td>3</td><td>173</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>1.00x</td></tr><tr><td>ECA</td><td>16</td><td>139</td><td>4</td><td>159</td><td>16</td><td>139</td><td>4</td><td>173</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>0.92x</td></tr><tr><td>LCA</td><td>16</td><td>91</td><td>3</td><td>174</td><td>16</td><td>91</td><td>3</td><td>174</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>1.00x</td></tr><tr><td>FIFO</td><td rowspan="3">quicksort6</td><td>32</td><td>179</td><td>5</td><td>181</td><td>32</td><td>179</td><td>5</td><td>181</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>1.00x</td></tr><tr><td>ECA</td><td>32</td><td>272</td><td>7</td><td>269</td><td>32</td><td>272</td><td>7</td><td>270.00x</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>1.00x</td></tr><tr><td>LCA</td><td>32</td><td>156</td><td>5</td><td>194</td><td>32</td><td>156</td><td>5</td><td>193</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>1.01x</td></tr><tr><td>FIFO</td><td rowspan="3">pi5</td><td>120</td><td>931</td><td>17</td><td>264</td><td>120</td><td>931</td><td>17</td><td>376</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>0.70x</td></tr><tr><td>ECA</td><td>120</td><td>931</td><td>17</td><td>266</td><td>120</td><td>931</td><td>17.00</td><td>263.00</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>1.01x</td></tr><tr><td>LCA</td><td>120</td><td>1236</td><td>22</td><td>377</td><td>120</td><td>990</td><td>18</td><td>456</td><td>1.00x</td><td>1.25x</td><td>1.22x</td><td>0.83x</td></tr><tr><td>FIFO</td><td rowspan="3">pipesort4</td><td>288</td><td>1448</td><td>20</td><td>378</td><td>288</td><td>1422</td><td>20</td><td>377</td><td>1.00x</td><td>1.02x</td><td>1.00x</td><td>1.00x</td></tr><tr><td>ECA</td><td>288</td><td>1293</td><td>19</td><td>376</td><td>288</td><td>1293</td><td>18</td><td>376</td><td>1.00x</td><td>1.00x</td><td>1.06x</td><td>1.00x</td></tr><tr><td>LCA</td><td>288</td><td>1944</td><td>27</td><td>376</td><td>288</td><td>1935</td><td>27</td><td>376</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>1.00x</td></tr><tr><td>FIFO</td><td rowspan="3">chameneos2</td><td>216</td><td>1681</td><td>23</td><td>378</td><td>216</td><td>1453</td><td>20</td><td>377</td><td>1.00x</td><td>1.16x</td><td>1.15x</td><td>1.00x</td></tr><tr><td>ECA</td><td>216</td><td>1826</td><td>24</td><td>374</td><td>216</td><td>1530</td><td>21</td><td>376</td><td>1.00x</td><td>1.19x</td><td>1.14x</td><td>0.99x</td></tr><tr><td>LCA</td><td>216</td><td>1231</td><td>17</td><td>376</td><td>216</td><td>1231</td><td>17</td><td>375</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>1.00x</td></tr><tr><td>FIFO</td><td rowspan="3">leader4</td><td>492</td><td>3125</td><td>43</td><td>454</td><td>492</td><td>3097</td><td>43</td><td>372</td><td>1.00x</td><td>1.01x</td><td>1.00x</td><td>1.22x</td></tr><tr><td>ECA</td><td>492</td><td>3267</td><td>45</td><td>376</td><td>492</td><td>3218</td><td>42</td><td>377</td><td>1.00x</td><td>1.02x</td><td>1.07x</td><td>1.00x</td></tr><tr><td>LCA</td><td>492</td><td>3311</td><td>46</td><td>680</td><td>492</td><td>3311</td><td>46</td><td>377</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>1.80x</td></tr><tr><td>FIFO</td><td rowspan="3">shortpath4</td><td>126</td><td>473</td><td>8</td><td>261</td><td>126</td><td>473</td><td>8</td><td>262</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>1.00x</td></tr><tr><td>ECA</td><td>126</td><td>489</td><td>8</td><td>260</td><td>126</td><td>489</td><td>8</td><td>260</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>1.00x</td></tr><tr><td>LCA</td><td>126</td><td>522</td><td>9</td><td>262</td><td>126</td><td>502</td><td>8</td><td>262</td><td>1.00x</td><td>1.04x</td><td>1.13x</td><td>1.00x</td></tr><tr><td>FIFO</td><td rowspan="3">shortpath5</td><td>296</td><td>1408</td><td>22</td><td>375</td><td>296</td><td>1408</td><td>22</td><td>375</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>1.00x</td></tr><tr><td>ECA</td><td>296</td><td>1031</td><td>16</td><td>264</td><td>296</td><td>997</td><td>17</td><td>265</td><td>1.00x</td><td>1.03x</td><td>0.94x</td><td>1.00x</td></tr><tr><td>LCA</td><td>296</td><td>1228</td><td>20</td><td>376</td><td>296</td><td>1218</td><td>19</td><td>451</td><td>1.00x</td><td>1.01x</td><td>1.05x</td><td>0.83x</td></tr><tr><td>FIFO</td><td rowspan="3">regsim</td><td>720</td><td>3453</td><td>37</td><td>376</td><td>720</td><td>2019</td><td>22</td><td>377</td><td>1.00x</td><td>1.71x</td><td>1.68x</td><td>1.00x</td></tr><tr><td>ECA</td><td>720</td><td>4054</td><td>47</td><td>375</td><td>720</td><td>2152</td><td>26</td><td>452</td><td>1.00x</td><td>1.88x</td><td>1.81x</td><td>0.83x</td></tr><tr><td>LCA</td><td>720</td><td>1962</td><td>22</td><td>264</td><td>720</td><td>1962</td><td>22</td><td>375</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>0.70x</td></tr><tr><td>FIFO</td><td rowspan="3">regsim-2-level</td><td>1296</td><td>8636</td><td>141</td><td>427</td><td>1296</td><td>5537</td><td>92</td><td>417</td><td>1.00x</td><td>1.56x</td><td>1.53x</td><td>1.02x</td></tr><tr><td>ECA</td><td>1296</td><td>14990</td><td>267</td><td>558</td><td>1296</td><td>7486</td><td>129</td><td>560</td><td>1.00x</td><td>2.00x</td><td>2.07x</td><td>1.00x</td></tr><tr><td>LCA</td><td>1296</td><td>6481</td><td>115</td><td>381</td><td>1296</td><td>6295</td><td>111</td><td>381</td><td>1.00x</td><td>1.03x</td><td>1.04x</td><td>1.00x</td></tr><tr><td>FIFO</td><td rowspan="3">diningphil</td><td>31</td><td>1375</td><td>38</td><td>524</td><td>31</td><td>1375</td><td>37</td><td>524</td><td>1.00x</td><td>1.00x</td><td>1.03x</td><td>1.00x</td></tr><tr><td>ECA</td><td>31</td><td>2082</td><td>55</td><td>348</td><td>31</td><td>1662</td><td>44</td><td>366</td><td>1.00x</td><td>1.25x</td><td>1.25x</td><td>0.95x</td></tr><tr><td>LCA</td><td>31</td><td>1333</td><td>38</td><td>374</td><td>29</td><td>1147</td><td>33</td><td>407</td><td>1.07x</td><td>1.16x</td><td>1.15x</td><td>0.92x</td></tr><tr><td colspan="12">Buggy programs (Exploration stops at first bug instance.)</td></tr><tr><td>FIFO</td><td>diningphil</td><td>1</td><td>15</td><td>2</td><td>112</td><td>1</td><td>15</td><td>2</td><td>112</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>1.00x</td></tr><tr><td>ECA</td><td rowspan="2">(deadlock)</td><td>16</td><td>915</td><td>29</td><td>340</td><td>16</td><td>767</td><td>22</td><td>342</td><td>1.00x</td><td>1.19x</td><td>1.32x</td><td>0.99x</td></tr><tr><td>LCA</td><td>1</td><td>15</td><td>2</td><td>112</td><td>1</td><td>15</td><td>2</td><td>112</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>1.00x</td></tr><tr><td>FIFO</td><td rowspan="3">minesweeper</td><td>1</td><td>29</td><td>3</td><td>163</td><td>1</td><td>29</td><td>2</td><td>163</td><td>1.00x</td><td>1.00x</td><td>1.50x</td><td>1.00x</td></tr><tr><td>ECA</td><td>2710</td><td>15577</td><td>484</td><td>717</td><td>2710</td><td>15381</td><td>499</td><td>744</td><td>1.00x</td><td>1.01x</td><td>0.97x</td><td>0.96x</td></tr><tr><td>LCA</td><td>6993</td><td>69350</td><td>1950</td><td>1041</td><td>6993</td><td>55430</td><td>1651</td><td>893</td><td>1.00x</td><td>1.25x</td><td>1.18x</td><td>1.17x</td></tr><tr><td>FIFO</td><td rowspan="3">le-erlang3-failure</td><td>457</td><td>1976</td><td>41</td><td>462</td><td>452</td><td>1944</td><td>27</td><td>427</td><td>1.01x</td><td>1.02x</td><td>1.52x</td><td>1.08x</td></tr><tr><td>ECA</td><td>30</td><td>174</td><td>4</td><td>241</td><td>30</td><td>174</td><td>4</td><td>236</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>1.02x</td></tr><tr><td>LCA</td><td>233738</td><td>759109</td><td>14401</td><td>2020</td><td>93640</td><td>296229</td><td>3557</td><td>1557</td><td>2.50x</td><td>2.56x</td><td>4.05x</td><td>1.30x</td></tr><tr><td>FIFO</td><td rowspan="3">le-erlang4</td><td>2209</td><td>11006</td><td>169</td><td>605</td><td>2191</td><td>10146</td><td>155</td><td>586</td><td>1.01x</td><td>1.08x</td><td>1.09x</td><td>1.03x</td></tr><tr><td>ECA</td><td>1</td><td>27</td><td>2</td><td>112</td><td>1</td><td>27</td><td>2</td><td>112</td><td>1.00x</td><td>1.00x</td><td>1.00x</td><td>1.00x</td></tr><tr><td>LCA</td><td>198713</td><td>698759</td><td>14405</td><td>2011</td><td>88505</td><td>277440</td><td>3924</td><td>1383</td><td>2.25x</td><td>2.52x</td><td>3.67x</td><td>1.45x</td></tr><tr><td colspan="12">Max 2.50x 2.56x 4.05x 1.45x</td></tr><tr><td colspan="12">Average 1.16x 1.22x 1.40x 1.08x</td></tr></tbody></table>

The results are presented in Table 2. For le-erlang, our tool was able to find all the previously known bugs in the algorithm (in the presence of node failures). We also tested the algorithm for four processes and without a failure-recovery scenario. To our surprise, our tool detected a new bug, which allows the program to reach a state in which no leader is elected. We contacted the developers and they confirmed the new bug.

The combination with sleep sets reduces the improvement as sleep sets already prune many redundant transitions; however TransDPOR is always equal to or better than DPOR in terms of paths and transitions. For seven experiments, TransDPOR provides the speedup of over 1.20x for at least one heuristic. Note that it is not obvious from the program what may be a good heuristic, and the results table suggests the same. For example, ECA is the best heuristic for le-erlang, and FIFO is the best for minesweeper. Moreover, different compo-
nents of a single application, such as the regsim-2-level, may have different good heuristics for exploration.

Overall, the results suggest that our algorithm combined with sleep sets out-
performs the combination of DPOR and sleep sets. We achieved speedup as high
as 2x for the regsim benchmark as shown in Table 2. TransDPOR is also very
efficient when exploring programs with bugs. We consistently find the bug faster
than DPOR. Even in the presence of sleep sets, we were able to find the bugs
up to 2.56x faster than DPOR.

7 Related Work

One of the earliest POR approaches is based on computing persistent (or stub-
born) sets [8, 9, 27] and the related technique of ample sets [22]. Persistent sets
can be computed statically or dynamically. Using static analysis for computing
persistent sets [8] suffers from conservative approximation, resulting in coarse
persistent sets. Therefore, *dynamic POR* (DPOR) techniques [6], which com-
pute the persistent sets on the fly, have been proposed to yield more accurate
persistent sets. Another variation of persistent (or stubborn) is *weak persistent
sets* [9, 27], which can generate smaller sets and lead to better reduction. This
reduction needs additional knowledge about the transitions that enable and dis-
able each other, which may not be easy to compute during the exploration.

Sen and Agha proposed a DPOR technique for testing multi-threaded pro-
grams [25], as well as for testing distributed message-passing programs [24]. Both
papers present an operational definition of the set of transitions to be explored
from a state, and the presented algorithms are conceptually similar to that in [6].
Kastenberg and Rensink proposed a new DPOR which is based on *probe sets* for
handling dynamic creation and destroying of processes and objects [15]. Probe
sets relies on abstract enabling and disabling relations among actions, rather
than associated sets of concurrent processes. The authors show that their tech-
nique leads to a better reduction in comparison to persistent sets.

Recently a new partial-order reduction technique called cartesian POR was
proposed, which is based on *cartesian semantics* [11] and stateful exploration.
The authors provide an operational definition, and present a dynamic algorithm
that overcomes the acyclic state space restriction in stateless approaches. The
technique is shown to improve over optimal persistent sets for some examples.
The cartesian approach trades space for time since the approach requires storing
program states precisely.

Lei and Carver [19] propose a technique that explores only one interleaving
from each partial order. However their technique assumes FIFO channels and re-
quires a non-trivial amount of memory for storing interleavings that are yet to be
explored. Message Passing Interface (MPI) [10] is a popular environment for writ-
ing message-passing programs. MPI programs are more constrained than actor
programs. Specifically, MPI processes assume FIFO channels and usually have
matched sends and receives. Vakkalanka et al. [26] proposed a stateless DPOR
technique for MPI programs, called POE, which exploits these constraints. POE
can produce only one interleaving for large MPI programs that do not have an
MPI wild-card receive.

8 Conclusions and Future Work

We have proposed a new stateless DPOR technique called TransDPOR for
message-passing (actor) systems. We exploit the transitivity of a dependency
relation between co-enabled transitions in actor systems to achieve faster explo-
ration than the existing DPOR based on persistent sets. Experimental results
suggest that TransDPOR can substantially reduce the number of transitions ex-
ecuted during state space exploration by up to 163.80x compared to DPOR, and
it can detect bugs up to 2.56x faster than DPOR. TransDPOR code is available
with Basset at http://mir.cs.illinois.edu/basset.

Although we applied our algorithm for message-passing systems, we believe
that the technique discussed in this paper may be applicable to shared-memory
multi-threaded programs if a dependency relation between the co-enabled tran-
sition is defined so that it is transitive. However, the detailed discussion in this
regard is outside the scope of this paper. We also plan to explore the possibility
of combining our algorithm with stateful exploration.

9 Acknowledgments

We would like to thank Yaniv Eytani, Bobak Hadidi, Vilas Jagannath, Timo Lat-
vala, and P. Madhusudan for discussions and other assistance during the course
of this project, and Nicholas Chen, Stas Negara, Milos Gligoric, Mohsen Vakilian,
and the participants of the software engineering seminar at UIUC for comments
on a draft of this paper. This material is based upon work partially supported by
US Department of Energy under Grant No. DOE DE-FG02-06ER25752 and the
National Science Foundation under Grant Nos. CCF-0916893, CNS-0851957,
CCF-0746856, and CNS-0509321, and by the AFRL and the AFOSR under
agreement number FA8750-11-2-0084.

References

1. G. Agha. *Actors: A Model of Concurrent Computation in Distributed Systems*. MIT Press, Cambridge, MA, USA, 1986.

2. G. Agha, I. A. Mason, S. Smith, and C. Talcott. A foundation for actor computation. *Journal of Functional Programming*, 7(01):1–72, 1997.

3. T. Arts, K. Claessen, and H. Svensson. Semi-formal development of a fault-tolerant leader election protocol in Erlang. *LNCS*, 3395:140–154, 2005.

4. K. M. Chandy and J. Misra. Distributed computation on graphs: Shortest path algorithms. *ACM*, 1982.

5. J. Esparza. Model checking using net unfoldings. *Science of Computer Programming*, 23(2-3):151–195, 1994.
6. C. Flanagan and P. Godefroid. Dynamic partial-order reduction for model checking software. In *POPL*, pages 110–121, 2005.

7. P. Godefroid. Using partial orders to improve automatic verification methods. In *CAV*, pages 176–185, 1991.

8. P. Godefroid. *Partial-Order Methods for the Verification of Concurrent Systems-An Approach to the State-Explosion Problem*. LNCS. 1996.

9. P. Godefroid and D. Pirottin. Refining dependencies improves partial-order verification methods. In *CAV*, pages 438–449, 1993.

10. W. Gropp, S. Huss-Lederman, A. Lumsdaine, E. Lusk, B. Nitzberg, W. Saphir, and M. Snir. MPI: The Complete Reference: Vol 2, The MPI-2 Extensions, 1998.

11. G. Gueta, C. Flanagan, E. Yahav, and M. Sagiv. Cartesian partial-order reduction. *Model Checking Software*, pages 95–112, 2009.

12. P. Haller and M. Odersky. Actors that unify threads and events. *Lecture Notes in Computer Science*, 4467:171, 2007.

13. G. Holzmann. The model checker SPIN. *IEEE Transactions on Software Engineering*, 23(5):279–295, 1997.

14. R. K. Karmani, A. Shali, and G. Agha. Actor frameworks for the JVM platform: A comparative analysis. In *PPPJava*, pages 11–20, 2009.

15. H. Kastenberg and A. Rensink. Dynamic partial order reduction using probe sets. In *CONCUR*, pages 233–247, 2008.

16. L. Lamport. Time, clocks, and the ordering of events in a distributed system. *Communications of the ACM*, 1978.

17. S. Lauterburg, M. Dotta, D. Marinov, and G. Agha. A framework for state-space exploration of Java-based actor programs. In *ASE*, pages 468–479, 2009.

18. S. Lauterburg, R. K. Karmani, D. Marinov, and G. Agha. Evaluating ordering heuristics for dynamic partial-order reduction techniques. In *FASE*, pages 308–322, 2010.

19. Y. Lei and R. H. Carver. Reachability testing of concurrent programs. *IEEE Transactions on Software Engineering*, 32:382–403, 2006.

20. K. McMillan. Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In *CAV*, pages 164–177, 1992.

21. Open Systems Laboratory, University of Illinois at Urbana-Champaign. *The Actor Foundry: A Java-based Actor Programming Environment*, 1998-09.

22. D. Peled. All from one, one for all: On model checking using representatives. In *CAV*, pages 409–423, 1993.

23. Pi code. www-unix.mcs.anl.gov/mpi/usingmpi/examples/simplempi/main.htm.

24. K. Sen and G. Agha. Automated systematic testing of open distributed programs. In *FASE 2006*, volume 3922 of LNCS, pages 339–356, 2006.

25. K. Sen and G. Agha. A race-detection and flipping algorithm for automated testing of multi-threaded programs. *Lecture Notes in Computer Science*, 4383:166, 2007.

26. S. S. Vakkalanka, G. Gopalakrishnan, and R. M. Kirby. Dynamic verification of MPI programs with reductions in presence of split operations and relaxed orderings. In *CAV*, pages 66–79, 2008.

27. A. Valmari. Stubborn sets for reduced state space generation. In *ATPN*, pages 491–515, 1991.

28. W. Visser, K. Havelund, G. P. Brat, S. Park, and F. Lerda. Model checking programs. *Autom. Softw. Eng.*, 10(2):203–232, 2003.

29. C. Wang, Z. Yang, V. Kahlon, and A. Gupta. Peephole partial order reduction. In *TACAS*, pages 382–396, 2008.