Partial-Order Reduction Is Hard

The goal of partial-order methods is to speed up explicit state exploration of concurrent systems. The state space of such systems grows exponentially with the number of processes. Fortunately, many runs of a concurrent system can usually be considered equivalent, so it is enough to explore only one run in each equivalence class. For example, if one process assigns $x:=2$ and another $y:=3$ then the order of execution of these two operations is usually irrelevant; the two interleavings are equivalent, and it is enough to explore only one of the two. This reduces the number of visited states as well as the exploration time. In some cases, the reductions are very substantial.

In recent years, we have seen novel applications of partial-order methods. One is proving the properties of concurrent programs [10], where equivalence between runs is not only used to reduce the number of proof objectives, but also to simplify proof objectives by choosing particular linearizations. Similarly, in symbolic executions [9] or in testing [28], partial-order can be used to limit the exploration space while still being exhaustive. Another application is verification of timed systems using recently developed local-time zones [15]. All these applications rely on explicit state enumeration, as opposed to symbolic methods such as SAT or BDDs.

The first partial-order methods were proposed about 35 years ago under the names of stubborn sets, persistent sets, or ample sets [34, 14, 20]. In 2005, Flanagan and Godefroid introduced stateless dynamic partial-order reductions [12], making stateless methods a focal point of subsequent research. In 2014, Abdulla et al. proposed a notion of trace-optimality¹¹1We use the term trace-optimality instead of simply optimality as in op.cit. to differentiate from state-optimality we consider in this paper. [1], and a race reversal technique, initiating a new cycle of work on stateless partial-order methods [6, 5, 18, 22, 23, 3, 21, 24, 4].

In this paper, we focus on stateful partial-order reduction methods, that have seen relatively less progress over the last two decades [29, 37, 8, 7]. A partial-order algorithm produces a reduced transition system containing a representative for each equivalence class of runs of the system. A stateless approach produces a tree of runs, but saves memory by storing only one run at a time. In contrast, a stateful approach keeps all visited states in memory so that an exploration can be stopped if a state is revisited. Each of the two approaches has its advantages. When the objective is to verify existing code by running an instrumentation of it, the states are too complex to keep in memory, so stateless exploration is the only solution. When verifying pseudocode, say of a mutual exclusion protocol, the number of non-equivalent runs may be several orders of magnitude bigger than the number of states, rendering the stateless approach infeasible. The stateful approach is then necessary.

Our first question is whether we can find a guiding principle for the stateful approach similar to the trace-optimality for the stateless approach. The example in Figure 1 shows why we cannot just settle on trace optimality. The two transition systems in the figure are both trace-optimal, since no two maximal paths are equivalent. But one is of linear size and the other is of exponential size. The obvious parameter for optimality of the stateful approach is the size of the transition system. So our question is whether a state-optimal, or close to optimal, partial-order algorithm can exist.

It is not difficult to see that getting a reduced system of exactly the minimal size is NP-hard. Our main result says something much stronger: even approximating the minimal size within a polynomial factor remains NP-hard (Theorem 5). This holds even for acyclic concurrent programs using only await and write instructions. Arguably, this looks like a minimal sensible set of instructions. If we allowed cycles then we could simulate await with active wait, reducing the set of instructions to just reads and writes.

This negative result justifies starting a systematic study of heuristics for stateful partial-order reduction. We propose an approach based on a notion of IFS oracle. This oracle expresses an important sub-problem encountered in partial-order reduction algorithms, namely avoiding so called sleep-blocked executions. Our proposal is to concentrate on the heuristics for this oracle to improve the efficiency of stateful methods. We justify this approach by showing that in the stateless setting, the IFS oracle gives a very simple trace-optimal algorithm. We show how to adapt this algorithm to the stateful approach. Finally, we narrow our study down to a special case, generalizing some settings considered in the stateless literature [5, 22], where the IFS oracle can be computed in linear time.

Before starting, we would like to shortly discuss the models of concurrent systems we are using. In recent years it is common to consider a model of processes with shared variables, eventually adding lock instructions. This is the model we are using for our lower bound. However, we also consider a stronger model of concurrent systems synchronizing on shared actions. This model can encode variables, and most of the synchronization mechanisms used in practice. For this reason we prefer this model for our positive results. Moreover, since the model is strong, our lower bound result is easier to prove for it, so it serves as a good intermediate step in our proof.

In this work we assume that programs are acyclic. Dealing with cycles in partial-order reduction is a separate problem from the reduction itself, and complicates the algorithms substantially. Finding a clean way of dealing with cycles in partial-order reduction is beyond the scope of this paper.

To summarize our three principal contributions are:

• $\mathrm{■}$

  A strong lower bound showing that, assuming $P\ne \text{NP}$, no deterministic algorithm can construct a reduced transition system for a concurrent program $\mathbb{P}$, of polynomial size relative to the minimal size of a reduced system for $\mathbb{P}$, while working in time polynomial in the size of its input and its output (Theorem 5). This holds even if every process in the program is acyclic and uses only await and write instructions.

• $\mathrm{■}$

  A notion of IFS oracle and a simple trace-optimal stateless algorithm using this oracle. We adapt this algorithm to the stateful approach.

• $\mathrm{■}$

  A special subcase of linear fully non-blocking systems, where the IFS oracle can be computed in linear time. This case covers some situations considered in the stateless partial-order reduction literature.

For our lower bounds we will consider a very simple standard model of concurrent programs with variables and locks. Variables range over finite domains, and locks are binary. The only operations on variables are write and await. The later operation blocks until the value of a variable is in a specified set of values. We do not need a read operation in our constructions, so we do not mention it to simplify the presentation.

A process is a directed acyclic graph with edges labeled by instructions. The instructions come from the set:

Here, $w(x,i)$ sets the value of variable $x$ to $i$, $await(x,I)$ blocks until the value of $x$ is in the set of values $I$, $\mathrm{𝑎𝑐𝑞}(l)$ acquires lock $l$, and $\mathrm{𝑟𝑒𝑙}(l)$ releases it. In case of acyclic processes, it is natural to have the blocking $await$ instruction. For example, all classical mutual exclusion algorithms rely on it. If we had cycles, $await$ could be simulated with an active wait.

A concurrent program $\mathbb{P}$ is a finite set of processes, over finite sets of variables and locks. Each variable has a finite domain. All variables and locks are global, meaning that they are shared by all processes. A conditional instruction is modeled by branching in the processes. The semantics of a program $\mathbb{P}$ is given by a transition system $\mathrm{TS}(\mathbb{P})$. Its states consist of a local state for each process, and a value for each variable and lock. In the initial state, each process is in its initial local state, and each variable and lock have value $0$. The transitions in $\mathrm{TS}(\mathbb{P})$ are defined according to the usual semantics of instructions from $\mathrm{\Sigma }$. Observe that $\mathrm{TS}(\mathbb{P})$ is acyclic since each process is acyclic.

We will also consider a much more flexible and expressive model, that we call concurrent system. It consists of a collection of processes synchronizing on common actions. Synchronization on actions can directly encode variables, locks, and many other synchronization primitives. In the context of this paper it will be easier to show the lower bound in this model than in the model with variables and locks. But, since the model is strong the lower bound result for this model is relatively weak. This is why we will eventually refine the lower bound construction to concurrent programs without locks.

A concurrent system $𝕊$ is determined by an alphabet $\mathrm{\Sigma }$ of abstract actions, and a set of processes that are graphs with edges labeled by actions. A process must be action deterministic: for every $s\in S$ and $a\in \mathrm{\Sigma }$ there is at most one $t$ with $s\stackrel{a}{⟶}t$. The term process is used both in the case of concurrent systems, and concurrent programs, but it will always be clear from the context which model we are using.

Every action $a$ has its domain, $\mathrm{𝑑𝑜𝑚}(a)$, that is a set of processes using it. We write $s_p\underset{p}{\overset{b}{⟶}}$ if there is an outgoing $b$-transition from state $s_p$ of process $p$. For a sequence of actions $v$ we write $\mathrm{𝑑𝑜𝑚}(v)$ for $\bigcup \{\mathrm{𝑑𝑜𝑚}(a):a\text{ appears in }v\}$, and $s_p\underset{p}{\overset{v}{⟶}}$ if there is a path labeled $v$ from $s_p$ in process $p$.

The semantics of a concurrent system $𝕊$ is a transition system $\mathrm{TS}(𝕊)$ whose states are tuples of states of process transition systems, $S={\prod }_{p\in \mathrm{𝑃𝑟𝑜𝑐}}{S}_p$; the initial state is the tuple consisting of initial states of each process, $s^0={\{s_p^0\}}_{p\in \mathrm{𝑃𝑟𝑜𝑐}}$; every action $a$ synchronizes processes involved in it: $s\stackrel{a}{⟶}{s}^{\prime }$ if $s_p\underset{p}{\overset{a}{⟶}}{s}_p^{\prime }$ for $p\in \mathrm{𝑑𝑜𝑚}(a)$, and $s_p^{\prime }=s_p$ for $p\notin \mathrm{𝑑𝑜𝑚}(a)$. We write $\text{<em class="ltx\_emph ltx\_font\_italic" style="color:\#0000FF;">enabled</em>}(s)$ for the set of actions labeling transitions outgoing from the global state $s$ of $\mathrm{TS}(𝕊)$.

Finally, we impose an acyclicity condition: for every action $a$, at least one of the processes in $\mathrm{𝑑𝑜𝑚}(a)$ must be acyclic. This guarantees that the global transition system is acyclic.

We will need to talk about runs in a transition system $\mathrm{TS}$, be it $\mathrm{TS}(\mathbb{P})$ for a concurrent program $\mathbb{P}$ or $\mathrm{TS}(𝕊)$ for a concurrent system $𝕊$. A run is a path in the transition system $\mathrm{TS}$, not necessarily from the initial state. We write $s\stackrel{v}{⟶}t$ if there is a run labeled with a sequence of actions $v$ from $s$ to $t$. Sometimes we write just $s\stackrel{v}{⟶}$ when $t$ is not relevant. A maximal run is a run reaching a terminal state – a state with no outgoing transitions. A full run is a maximal run starting in the initial state.

Figure 2 on the left shows Peterson’s mutual exclusion algorithm for $2$ processes. The middle-left picture shows its modeling as a concurrent program $\mathbb{P}=\{P_0,P_1\}$. It has three variables: $R_0$, $R_1$ and $T$ that range over $\{0,1\}$ as in the pseudocode. The middle-right picture shows the same algorithm modeled as a concurrent system $𝕊=\{P_0,P_1,R_0,R_1,T\}$. Processes $P_0$ and $P_1$ implement the code while the other processes model the variables $R[0]$, $R[1]$ and $T$. Action $r_i^j$ writes the value $j$ to variable $R[i]$. Action $r_i^{=0}$ checks if the variable $R[i]$ has value $0$; observe that it is enabled in the top state where $R[i]$ has value $0$, but not in the bottom state where it has value $1$. Similarly, for actions of $T$. Processes in $𝕊$ synchronize on common actions. For instance, $r_0^1$ synchronizes $P_0$ and $R_0$, while $t^{\ne 1}$ synchronizes $P_1$ with $T$. We write this as $\mathrm{𝑑𝑜𝑚}(r_0^1)=\{P_0,R_0\}$ and $\mathrm{𝑑𝑜𝑚}(t^{\ne 1})=\{P_1,T\}$. The transition system $\mathrm{TS}$ is shown on the right. It represents both $\mathrm{TS}(\mathbb{P})$ and $\mathrm{TS}(𝕊)$, although we have chosen to show labels from $𝕊$. Each full run corresponds to an execution of Peterson’s algorithm.

The initial motivation for partial-order reduction comes from the observation that some sequences of actions may be considered equivalent, and only one of the equivalent sequences needs to be explored. The equivalence relation on sequences is defined in terms of the independence relation on actions: two sequences are por-equivalent if one can be obtained from the other by permuting adjacent independent actions. We will use $\approx$ to denote a por-equivalence relation on sequences of actions. As we will see our arguments do not rely on a particular independence relation, as long as two actions using different processes and different resources are independent.

For concurrent programs with variables the classical independence relation says that two actions of different processes are independent if either they use different variables or they use the same variable and both of them are awaits. In particular lock operations are dependent.

For concurrent systems, the most common independence relation is the one coming from Mazurkiewicz trace theory [26]. Two actions $a,b\in \mathrm{\Sigma }$ are independent if they have disjoint domains: $aIb$ if $\mathrm{𝑑𝑜𝑚}(a)\cap \mathrm{𝑑𝑜𝑚}(b)=\mathrm{\varnothing }$.

It will also be useful to use the dual concept of dependent actions. Two actions are dependent, written $aDb$, if they are not independent. For example, when $\mathrm{𝑑𝑜𝑚}(a)\cap \mathrm{𝑑𝑜𝑚}(b)\ne \mathrm{\varnothing }$ in case of Mazurkiewicz independence. These notions are extended to sequences: $aIv$ means that $a$ is independent of all actions in $v$, and $aDv$ that $a$ is dependent on some action from $v$. We write $Da$ for the set of actions dependent on $a$.

The goal of partial-order reduction is to construct, for a given concurrent system $𝕊$ or a concurrent program $\mathbb{P}$, a reduced transition system representing all full runs in $\mathrm{TS}(𝕊)$ or $\mathrm{TS}(\mathbb{P})$ (recall that these are maximal runs from the initial state).

A general approach for constructing a reduced transition system is to determine for each state $s$ of $\mathrm{TS}$ a covering source set [1]: a subset of enabled actions that is sufficient to explore. For example, if every sequence starting from $b$ is equivalent to a sequence starting from $c$ then we may choose to include only $b$ in the source set. The notion of the first action modulo an equivalence relation $\approx$ on sequences is central for partial-order reduction.

We want a source set in a state to be large enough to contain a first action of at least one representative from every equivalence class of maximal runs from the state. Using the above definition this can be formulated as: a source set in $s$ should intersect every $\mathrm{𝑓𝑖𝑟𝑠𝑡}(u)$ for $u$ a maximal run from $s$. We formalize this as follows.

In particular, if $B$ contains all enabled actions from $s$ then $B$ is a covering source set at $s$. Intuitively, smaller covering source sets should give smaller reduced transition systems. This is not always true. A bigger but incomparable w.r.t. set inclusion covering source set may give a better reduction.

Observe that the notion of a covering source set depends on the por-equivalence relation $\approx$, as the definition of $\mathrm{𝑓𝑖𝑟𝑠𝑡}$ depends on it.

Suppose we have an assignment of a set of actions $\mathrm{𝑠𝑜𝑢𝑟𝑐𝑒}(s)$ for every state $s$ of $\mathrm{TS}$. We can use it to restrict the transition relation to transitions allowed by source sets: define $s\stackrel{a}{⟹}t$ when $s\stackrel{a}{⟶}t$ and $a\in \mathrm{𝑠𝑜𝑢𝑟𝑐𝑒}(s)$. If every $\mathrm{𝑠𝑜𝑢𝑟𝑐𝑒}(s)$ is a covering source set in $s$ then this restricted transition relation is enough.

This proposition allows us to construct a reduced transition system by keeping only $\stackrel{}{⟹}$ transitions and states reachable from the initial state using these transitions. We must underline though that source sets are not the only mechanism needed in partial-order reduction. Sleep-sets are another important ingredient (c.f. Remark 21).

Recall that the goal of partial-order reduction is to construct for a given program $\mathbb{P}$ or a given system $𝕊$, a reduced system that is sound and complete. Among such systems we would ideally like to construct one with the smallest number of states. We write $\mathrm{𝑚𝑖𝑛𝑇𝑆}(\mathbb{P})$ for the smallest number of states of a sound and complete reduced transition system for $\mathbb{P}$. Similarly, we write $\mathrm{𝑚𝑖𝑛𝑇𝑆}(𝕊)$ for a system $𝕊$. There may be several non-isomorphic transition systems with a minimal number of states.

Stateless algorithms use the concept of trace-optimality. This means that there are no two equivalent runs in the reduced transition system. As we have noted in the introduction, this concept is not very useful for our purposes. Indeed, the example from Figure 1 shows two trace-optimal transition systems, one of linear size and the other of exponential size. So in stateful partial-order reduction we should aim for a reduced transition system of small size. Even more so as there are also examples where the smallest reduced transition system is necessarily not trace-optimal.

In this section, we show that there is no polynomial-time algorithm for constructing a reduced transition system that is polynomially close to optimal. The next definition makes this precise.

The main result of this section is

We will prove this theorem in three steps. First we will consider concurrent systems. The flexibility of synchronization operations makes the constructions used in the proof much simpler, and the arguments can be supported by figures of a reasonable size. In the next step we adapt the construction to concurrent programs with locks and await. In the last step we eliminate locks. The proof is structured in such a way that the same statements need to be proved in each of the three steps.

In the light of the negative results from the previous section, it is clear that practical approaches to stateful partial-order reduction should be based on heuristics, and cannot aim at optimality, or even at approximate optimality up to a polynomial factor. In this section we propose a concrete problem, that when solved with a satisfactory heuristic should advance the quality of our partial-order methods. This approach also allows to make a link with stateless partial-order methods. It leads to a simple trace-optimal algorithm for the stateless case for a restricted class of concurrent systems.

We start with a simple algorithm for constructing trace-optimal reduced transition systems. It uses three ingredients that we describe in more details later.

• $\mathrm{■}$

  Lexicographic order on sequences allowing to determine a representative run for each class of a por-equivalence relation $\approx$.

• $\mathrm{■}$

  Sleep sets giving enough information about the exploration context.

• $\mathrm{■}$

  An oracle “includes first sets”, denoted $\mathrm{𝐼𝐹𝑆}$, permitting to avoid sleep-blocked runs.

Lexicographic ordering has been already used in the context of partial-order reduction [19]. Sleep sets are one of the classical concepts for partial-order methods [14]. $\mathrm{𝐼𝐹𝑆}$ oracle is a direct way of avoiding sleep-blocked executions, a well known challenge in partial-order reduction [1]. Our contribution here is to make the $\mathrm{𝐼𝐹𝑆}$ problem explicit. Without surprise at this stage, the $\mathrm{𝐼𝐹𝑆}$ problem is NP-hard, but we show one case where it is polynomial.

Let us fix a concurrent system $𝕊$. Let us also assume that we have some linear ordering on actions of $𝕊$. This determines a lexicographic ordering on sequences of actions. Given some equivalence relation on sequences we can use the lexicographic order to define representatives for equivalence classes of $\approx$ relation.

We are going to present an algorithm enumerating full lex-runs of $\mathrm{TS}(𝕊)$. For this we will use the “includes first set (IFS)” oracle. The idea is as follows. Suppose the algorithm has reached a state $s$ and produced a sleep set $\mathrm{𝑠𝑙𝑒𝑒𝑝}(s)$ containing actions that need not be explored from $s$. We would like to check if there is something left to be explored. We need to check if the exploration is not sleep-blocked, namely, if there is a maximal run $u$ from $s$ with $\mathrm{𝑓𝑖𝑟𝑠𝑡}(u)\cap \mathrm{𝑠𝑙𝑒𝑒𝑝}(s)=\mathrm{\varnothing }$. If there is such run, we need to explore one of the actions in $\mathrm{𝑓𝑖𝑟𝑠𝑡}(u)$ from $s$.

Listing 1 presents a very simple algorithm enumerating all full lex-runs of $\mathrm{TS}(𝕊)$. The algorithm also gives us an opportunity to explain sleep sets in details. Each node $n$ of the tree constructed by the algorithm is a pair consisting of a state of $\mathrm{TS}(𝕊)$, denoted $s(n)$, and a set of actions $\mathrm{𝑠𝑙𝑒𝑒𝑝}(n)$. For readability, we write $\text{<em class="ltx\_emph ltx\_font\_italic">enabled</em>}(n)$ instead of $\text{<em class="ltx\_emph ltx\_font\_italic" style="color:\#0000B3;">enabled</em>}(s(n))$, for the set of outgoing actions from $s(n)$.

Sleep sets are a very elegant mechanism to gather some information about the exploration context. They can be computed top-down when constructing an exploration graph. At the root, the sleep set is empty. For a node $n$ and a transition $n\stackrel{e}{⟶}{n}_e$ we have $\mathrm{𝑠𝑙𝑒𝑒𝑝}(n_e)=(\mathrm{𝑠𝑙𝑒𝑒𝑝}(n)\cup \{a_1,\mathrm{\dots },a_k\})-De$, where $a_1,\mathrm{\dots },a_k$ are labels of transitions from $n$ created before the $e$-transition; and the final $-De$ term means that we remove all the actions dependent on $e$. The intuition behind this formula is as follows. Assume that we keep an invariant:

(sleep-invariant): after exploration of a node $n$ for every maximal run $u$ from $s(n)$ in $\mathrm{TS}$ such that $\mathrm{𝑓𝑖𝑟𝑠𝑡}(u)\cap \mathrm{𝑠𝑙𝑒𝑒𝑝}(n)=\mathrm{\varnothing }$ we have a path $v$ from $n$ with $u\approx v$.

Then the formula for $\mathrm{𝑠𝑙𝑒𝑒𝑝}(n_e)$ says that we need not explore from $n_e$ a run starting, say, with $a_1$ if $a_{1}Ie$. This is because when looking from $n$ such a run has $a_1$ in its first set, and it has already been explored from $a_1$’s successor of $n$.

The algorithm from Listing 1 examines all enabled transitions in a node $n$ in our fixed order on actions. For every enabled transition $s(n)\stackrel{e}{⟶}{s}^{\prime }$ it uses the $\mathrm{𝐼𝐹𝑆}$ oracle in Line 10 to decide if it is necessary to explore it. If the answer is positive, then it creates node $n^{\prime }$ with an appropriate sleep set. If not, then it skips the transition. This guarantees that the algorithm is trace-optimal.

We could use this algorithm in stateless model-checking if we had an implementation of $\mathrm{𝐼𝐹𝑆}(s,B)$. In a stateful version, the algorithm is not very interesting as trees produced by this algorithm can be, and often are, orders of magnitude bigger than $\mathrm{TS}(𝕊)$, the transition system of $𝕊$ without any reduction. But we can modify the algorithm to produce a graph instead of a tree. For this we need to introduce a subsumption relation between nodes.

Observe that if $n$ subsumes $n^{\prime }$, all runs that are not sleep blocked from $n^{\prime }$ are also not sleep blocked from $n$. Thus replacing $n^{\prime }$ by $n$ still yields a sound and complete reduced transition system. Thus, we add subsumption to Listing 1 as shown in Listing 2. We first check if the successor $s^{\prime }$ of $s$ is subsumed by an existing node in line 11. If yes, then, instead of creating a new node, we add an edge to the subsuming node (line 12). Otherwise, we proceed as in Listing 1. Observe that the algorithm in Listing 2 builds a directed acyclic graph (DAG) instead of a tree, hence avoiding visiting a node more than once.

The new algorithm does not satisfy a statement as in Lemma 18 because edges added due to the subsumption relation may create paths that are not lex-runs. We can get a variant of this optimality property when looking at states. Let us call a state lex-useful if it appears on a full lex-run.

Our main result is a negative one, indicating that we cannot hope for too much in terms of theoretically good partial-order algorithms. It has been known before that certain existing partial-order methods are NP-hard [30], but here we show that no method can be both polynomially close to optimal and not NP-hard.

As we have explained in the introduction, we believe that stateful partial-order methods have applications, and that there are even more applications to come. In this context our negative result gives us an argument for looking at well motivated heuristics rather than for a theoretically grounded result. We propose a new schema of a partial-order reduction algorithm based on IFS test. While in general the test is NP-complete, we hope that good heuristics for this test can translate into progress in partial-order methods. This is a direction we are actively investigating.

There is a big variety of concurrent systems, in particular depending on communication operations between processes. We have exhibited one case when IFS test can be done in Ptime. Intuitively, it captures “fully non-blocking” situations. An interesting question is what happens in the forward non-blocking case [1], or maybe to some other formalization of non-blocking in the spirit wait-free operations [16] or MPI [27].