# Towards Efficient Verification of Parallel Applications with Mc SimGrid

Mathieu Laurent, Thierry Jéron, Martin Quinson

► To cite this version:

Mathieu Laurent, Thierry Jéron, Martin Quinson. Towards Efficient Verification of Parallel Applications with Mc SimGrid. FORTE 2025 - 45th International Conference on Formal Techniques for Distributed Objects, Components, and Systems, Carla Ferreira, Claudio A. Mezzina, Jun 2025, Lille, France. pp.1-21. hal-05042973v2

HAL Id: hal-05042973

https://hal.science/hal-05042973v2

Submitted on 13 May 2025

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
Towards Efficient Verification of Parallel
Applications
with Mc SimGrid

Mathieu Laurent, Thierry Jéron and Martin Quinson

Univ Rennes, Inria, CNRS, Irisa, Rennes, France

**Abstract.** Assessing the correctness of distributed and parallel applications is notoriously difficult due to the complexity of the concurrent behaviors and the difficulty to reproduce bugs. In this context, Dynamic Partial Order Reduction (DPOR) techniques have proved successful in exploiting concurrency to verify applications without exploring all their behaviors. However, they may lack of efficiency when tracking non-systematic bugs of real size applications. In this paper, we suggest two adaptations of the Optimal Dynamic Partial Order Reduction (ODPOR) algorithm with a particular focus on bug finding and explanation. The first adaptation is an out-of-order version called RFS ODPOR which avoids being stuck in uninteresting large parts of the state space. Once a bug is found, the second adaptation takes advantage of ODPOR principles to efficiently find the origins of the bug.

# 1 Introduction

We consider parallel applications made of interacting actors that can share the memory of a single computer, or can be geographically distributed across the network. These actors interact through message passing over the network, or through classical synchronization mechanisms such as mutexes or semaphores. This class of applications encompasses a large amount of real-world programs, such as message-passing ones that are commonly built upon the MPI standard [12] in High-Performance Computing, or classical multithreaded applications built for example upon the POSIX pthread standard [20]. These applications are notoriously difficult to get right as they add the challenges of concurrent and multithreaded applications (race conditions, deadlocks, livelocks) to the challenges linked to asynchronous message passing (communication mismatch), and memory coherency in distributed settings.

The main challenge to the correctness of these applications lies in the fact that the ordering of events changes the behavior. Moreover, triggering existing bugs also becomes challenging in such complex applications. The purpose of our work is therefore to design automatic verification methods that are both complete for a fixed input, and efficient for finding bugs in applications whose behaviors are supposed to be finite but possibly non-deterministic.

Testing can be efficient for detecting bugs in software. It can be made formal, in particular by synthesizing tests and their verdicts automatically from a
model of the system. Unfortunately, it suffers from non-completeness and its difficulty to reproduce bugs for distributed applications. Among formal verification techniques, model checking is complete. In its classical form it requires building a formal model by abstraction of the system behavior. Completeness is then relative to this model, not necessarily the real system. Moreover, it often does not scale to real size programs, which hampers completeness in practice. Software model checking is an alternative which focuses on the software code itself, releasing the user from the burden of building a formal model. This approach encompasses a set of techniques inspired from static analysis, model checking or automated proving, and proved to be scalable [13].

Among these, dynamic partial order reduction (DPOR) [11] comprises techniques that are complete (under some hypothesis), and exploit the independence of actions of concurrent actors to avoid explicitly traversing all behaviors. DPOR is stateless, meaning that system states are not stored, since they are too large. In the last decade, new developments proposed optimal solutions (see e.g. [1,2,24]). In the same time, those techniques have been tuned for relaxed memory models where even local actions may be independent (see e.g. [26,15]).

Our goal is to verify real parallel programs, for which we do not dispose of a model, but can execute their code. We build upon Mc SimGrid [23], a stateless model checker targeting parallel distributed applications that interact through message passing or through synchronization mechanisms (mutex, barrier, etc.). We use this tool as an experimental platform for the study of model checking techniques in this domain. Underneath, Mc SimGrid leverages the SimGrid simulator [8] to observe and control the execution of the applications under scrutiny.

In this paper, we propose adaptations of the ODPOR algorithm [1]. We want to improve the practical efficiency of ODPOR when searching for bugs. Indeed, even if ODPOR is complete and optimal, its depth-first search (DFS) nature may make it inefficient at detecting bugs by forcing the full exploration of uninteresting parts of the state space before reaching a bug. Our first contribution propose a variant of ODPOR based on an out-of-order traversal that increases the chance to detect bugs quickly. We also aim at increasing the usefulness of counter-examples when bugs are found, when the usually long sequences of actions reveal hard to analyze by humans. We define a notion of *critical transition*, which separates correct from incorrect executions in an execution path to a bug. It is thus part of the bug root cause. Our second contribution is to further adapt the ODPOR algorithm so that, when a bug is found, it efficiently searches this critical transition. All algorithms are implemented in the prototype Mc SimGrid and experimented on some benchmarks. The analysis of the experiments show promising results.

The rest of this article is organized as follows. Section 2 provides some background information about the considered class of applications, the limits of the programming model, and how classical DPOR techniques are leveraged to verify real distributed applications. Section 3 presents the contributions of this work, while Section 4 provides some preliminary experiments to evaluate these contributions. Section 5 concludes this paper by sketching possible future works.
## 2 Adapting Model Checking Techniques to the Verification of Parallel Applications

In this section, we first sketch the programming model for parallel applications implemented in Mc SimGrid. We then introduce the formalism necessary for DPOR algorithms, and then explain the principles of the ODPOR algorithm.

### 2.1 Extended Programming Model

Real parallel systems can be built with many programming interfaces, each containing many primitives. The amount of primitives makes it impractical to reason at that level to verify the resulting applications [21]. Instead, we build upon an abstract model entailing only about 20 actions. This reduced set of primitives are used at the core of the SimGrid simulator to mediate all interactions between interacting actors<fnref n="1" />, with the exception of direct memory sharing between actors. Over the years, this set of primitives was proven sufficient to represent a large class of parallel applications: [10] presents a SimGrid implementation of the MPI standard [12], that prevails in High-Performance Computing. [9] presents a SimGrid implementation of the POSIX pthread library, that is used by multithreaded UNIX applications. These near-complete reimplementations of the standards allow most of the applications written with these interfaces to run unmodified on top of SimGrid.

This programming model is composed of several subsystems, each proposing specific actions allowing actors to interact through shared objects: The network subsystem proposes mailbox objects allowing receiving actors to be matched with sending ones. The corresponding actions are asynchronous and non-blocking to meet the needs of the MPI interface: ASYNC_SEND and ASYNC_RECV (receive) represent the start of a background communication. The usual asynchronous communication pattern becomes the combination of an ASYNC_SEND and of an ASYNC_RECV immediately followed by a WAIT. This extension is mandatory to precisely model the MPI semantics as with the MPI Isend, MPI Irecv and MPI Wait primitives. The synchronization subsystem proposes four classical types of objects: mutex, semaphore, barrier, and POSIX condition variable. The corresponding actions implement classical operations such as lock/unlock, test and signal/broadcast for condition variables. Although the POSIX standard describes only synchronous versions of these operations, we refine them into an asynchronous action followed by a WAIT for symmetry with the network subsystem. Finally, WAITALL can be used to wait atomically for the completion of all actions in a given set while WAITANY blocks until the completion of an arbitrary action among a given set. This last action is non-deterministic in the sense that an actor executing it returns any of the terminated actions in the set. Similarly, RANDOM can be used to explore several alternate outcomes. For example, RANDOM({1, 2}) can return either 1 or 2.

<footnote n="1">¹ We use actor and process interchangeably to designate an entity interacting with others either by message passing or shared memory</footnote>
This programming model refines the one described in [22], enriched with the pthread semantics. It is probably sufficient to encode the semantics of other libraries such as the BSD sockets that base almost all Internet communications. The main limitation of this model is that it does not capture direct memory accesses. Memory reads and writes are not observable in our model for sake of verification efficiency. This implies that data races, for instance, are out of the scope of our study. Instead, we focus on bugs triggered by specific orderings of actions, such as deadlocks or assertion errors due to communication mismatch or synchronization misuses. Previous work have shown the importance of this class of bugs in real applications [7].

## 2.2 Notations and Definitions

Formally, we consider a parallel system composed of $n$ programs $p_1, \dots, p_n \in \mathbb{P}$. The global behaviour of this system can be described by a labelled transition system (LTS) $\mathcal{M} = (S, \mathbf{Act}, s_0, \mathcal{T})$ where $S$ is a set of states encoding local states of processes, contents of communication channels and status of synchronization objects, $s_0 \in S$ is the initial state where each process $p$ is in its initial state, communication channels are empty and synchronization objects free, $\mathbf{Act} = \bigcup_{i=1}^n \mathbf{Act}_i$ is the alphabet of actions, the disjoint union of local alphabets, $\mathcal{T} \subseteq S \times \mathbf{Act} \times S$ is the transition relation, each transition $(s, a, s') \in \mathcal{T}$ sometimes written $s \xrightarrow{a} s'$. We note $\mathbf{proc}((s, a, s')) = \mathbf{proc}(a) = p_i$ if $a \in \mathbf{Act}_i$ meaning that $s \xrightarrow{a} s'$ is executed by process $p_i$. We denote by enabled($s$) the set of transitions that can be taken from state $s$. In the following, we assume that actors are deterministic, i.e., for each $s \in S$, if $t_1, t_2 \in \mathbf{enabled}(s)$, then $\mathbf{proc}(t_1) \neq \mathbf{proc}(t_2)$. This allows one to identify the transitions in a given state by their actors. Our results and implementation hold for non-deterministic actors, but distinguishing the transitions outcomes of a given actor in a given state would make the notations artificially complex.

We restrict our study to acyclic LTS. An execution of $\mathcal{M}$ is a finite sequence of transitions starting in the initial state $E := t_1 \cdot t_2 \cdots t_n = (s_0, a_1, s_1) \cdot (s_1, a_2, s_2) \cdots (s_{n-1}, a_n, s_n) \in \mathcal{T}^*$ also written $s_0 \mathop{\mathop{\longrightarrow}\limits_{a_1 \cdot a_2 \cdots a_n}}^{a_1 \cdot a_2 \cdots a_n} s_n$. With the remark above, $E$ can also be written by its sequence of processes $\mathbf{proc}(t_1) \cdots \mathbf{proc}(t_n)$. $E$ is maximal when $\mathbf{enabled}(\mathbf{last}(E)) = \emptyset$. The following notations are introduced:

- $\mathbf{dom}(E) := \{1, \dots, n\}$, the range of transitions in $E$,

- $E_i := t_i$ for $i \in \mathbf{dom}(E)$, the $i^{th}$ transition of $E$,

- $E \cdot t := t_1 \cdots t_n \cdot t$, for $t = (s_n, a_{n+1}, s_{n+1})$, the concatenation of $E$ with $t$,

- $E \vdash t$ (or equivalently $E \vdash p$ where $p = \mathbf{proc}(t)$), for $t \in T$, the fact that $E \cdot t$ is a valid execution,

- $\mathbf{sub}(E, t_i) := t_1 \cdots t_i$ for $i \in \mathbf{dom}(E)$, the prefix of $E$, up to $t_i$ included,

- $\mathbf{pre}(E, i) := s_{i-1}$ for $i \in \mathbf{dom}(E)$, the state reached before executing $t_i$,

- $\mathbf{last}(E) := s_n$, the last state of the execution $E$.

For sake of algorithmic simplicity, we assume a property called persistency: an enabled process cannot be disabled before it executes some action. Formally,
for any execution $E$, any process $p \in \mathbb{P}$, if $E \vdash p$, then for any other process $q \neq p$, $E \vdash q$ implies $E \cdot q \vdash p$. Notice that in the programming model, persitency justifies to split blocking calls such as `MUTEX_LOCK` into a non-blocking `MUTEX_ASYNC_LOCK`, that adds the caller's ID to the list of actors requesting this mutex, followed by a blocking `MUTEX_WAIT`, that becomes enabled only when the caller's ID is first in that list. While an atomic `MUTEX_LOCK` would not be persistent (it gets disabled if another actor gets the lock), both `MUTEX_ASYNC_LOCK` and `MUTEX_WAIT` are actually persistent.

## 2.3 State Space Reduction using ODPOR

Dynamic partial order reduction (DPOR) [11] is a software model checking technique that exploits the independence between concurrent actions. To avoid the exploration of the full state space, it relies on the equivalence of executions by commutation of adjacent transitions carrying independent actions.

Intuitively, two actions are independent if firing one cannot enable or disable the other, and they commute, i.e. their execution order does not impact the final result. Formally, a valid *independency* relation for $\mathcal{M}$ is an irreflexive and symmetric relation $\mathcal{I} \subseteq \mathbf{Act} \times \mathbf{Act}$ such that, for any state $s \in S$ and any pair of *independent* actions $(a_1, a_2) \in \mathcal{I}$, we have:

- if there exists $s' \in S$ such that $s \xrightarrow{a_1} s'$, then $a_2 \in \mathit{enabled}(s)$ if and only if $a_2 \in \mathit{enabled}(s')$,

- if $a_1, a_2 \in \mathit{enabled}(s)$, then there exists $s' \in S$ such that $s \xrightarrow{a_1a_2} s'$ and $s \xrightarrow{a_2a_1} s'$.

The *dependency* relation $\mathcal{D} = \mathbf{Act} \times \mathbf{Act} \setminus \mathcal{I}$ is the complementary relation. In this paper we only consider a statically defined valid dependency relation, i.e., based on the semantics of the programming model of Mc SimGrid. For instance, we can state that `ASYNC_SEND` and `ASYNC_RECV` actions are always independent, while two `MUTEX_LOCK` concerned by the same mutex are dependent [22].

<table><caption>Fig. 1: A communication pattern using the *any* wildcard.</caption><thead><tr><th>P1</th><th>P2</th><th>P3</th></tr></thead><tbody><tr><td>ASYNC_SEND(P3)</td><td>ASYNC_SEND(P3)</td><td>ASYNC_RECV(from any); WAIT()</td></tr><tr><td></td><td></td><td>ASYNC_RECV(from P2) ; WAIT()</td></tr></tbody></table>

For a sequence of transitions $E = t_1 \cdots t_n$, the *happens-before* [18] relation $\rightarrow_E$ is the smallest transitively closed relation on $\mathrm{dom}(E)$ such that if $i < j$ and the actions carried by $t_i$ and $t_j$ are dependent then $i \rightarrow_E j$.
*Example 1.* Consider the execution $E = P_1 \cdot P_2 \cdot P_3 \cdot P_3$ from Fig. 1 (remember that a transition can be identified with its actor). We have that $E_1 \to_E E_2$ because two ASYNC_SEND actions to the same actor are dependent, and $E_3 \to_E E_4$ because actions from the same actors are causally ordered.

Let $\simeq$ be the equivalence relation on executions such that $E \simeq E'$ if $dom(E) = dom(E')$ and $\to_E = \to_{E'}$. A Mazurkiewicz's trace $[E]_{\simeq}$, is the class of executions equivalent for $\simeq$ and containing $E$.

DPOR algorithms aim at exploring the smallest number of executions while ensuring soundness of the exploration. This is ensured by exploring at least one execution per Mazurkiewicz's trace. To that extend, reduction algorithms aim at finding reversible races, i.e., identifying pairs of dependent transitions which inversion leads to a distinct Mazurkiewicz's trace. Formally, $t_i$ and $t_j$ with $i < j \in dom(E)$ are in reversible race, noted $i \preceq_E j$, when:

- $\mathbf{proc}(t_i) \neq \mathbf{proc}(t_j)$, and $i \to_E j$,

- there is no $k$ such that $i < k < j$, $i \to_E k$ and $k \to_E j$,

- for any $E' \in [E]_{\simeq}$ of the form $E' = F \cdot t_i \cdot t_j \cdot F'$, then $F \vdash t_j$.

The first condition states that $t_i$ and $t_j$ belong to different actors and are dependent, ensuring that their inversion produces a different Mazurkiewicz's trace. The second condition ensures that there is no intermediate transition that would be in reversible race with both of them. The last one ensures that $t_i$ does not enable $t_j$. We then get that if $i \preceq_E j$, there exists $E' \nsim E$ with $j \to_{E'} i$. The satisfaction of properties such as absence of deadlock or assertion violation is consistent with Mazurkiewicz's traces [11], meaning that for any such property $\varphi$, if $E \simeq E'$ then $\varphi \models E \iff \varphi \models E'$. The principle of a DPOR algorithm is then to verify those properties by building a so called "reduced LTS", where each Mazurkiewicz's trace is represented by at least one execution.

Optimal Dynamic Partial Order Reduction (ODPOR) [1] is a recent DPOR technique. Like other DPOR algorithms, ODPOR is based on a stateless depth-first exploration of a reduced state space. The exploration also uses a set of processes called *sleep set* to avoid exploring executions equivalent to already traversed ones. The original DPOR algorithm stores in each traversed execution $E$ a *persistent set*, i.e. a set of processes that should be visited later when backtracking, populated when a reversible race just after $E$ is detected in some continuation execution. The optimality of ODPOR is gained by associating to each traversed execution $E$ a more precise information called *wakeup tree*, a set of initial sequences that should be visited later when backtracking to $E$.

The crucial notion of *wakeup tree* is detailed now. First, we define *weak initials* of a sequence $w$ after a prefix $E: WI_{[E]}(w)$ is the set of processes $p$ s.t. there exists sequences $w'$ and $v$ satisfying $E \cdot w \cdot v \simeq E \cdot p \cdot w'$. Intuitively, $WI_{[E]}(w)$ are the processes in *enabled(E)* that have no happens-before predecessor in $w$. Let an *ordered tree* $(B, <)$ be a prefix-closed set of executions, each *node* being an execution and the *root* is the empty one $\langle \rangle$. A *wakeup tree* after a prefix $E$ written $WuT(E)$, relative to a set of processes $P$ (the sleep set in $E$) is then an ordered tree $(B, <)$ s.t.:
- for every leaf node $w \in B$, $WI_{[E]}(w) \cap P = \emptyset$,

- for every node $u.p$ and leaf $u.w$ in $B$, if $u.p \prec u.w$ then $p \notin WI_{[E.u]}(w)$.

Both conditions are necessary to achieve optimality of ODPOR, meaning that each Mazurkiewicz's trace is explored exactly once by the algorithm and no sleep-set-blocked (SSB) execution is visited (an SSB execution is an execution equivalent to an already explored one, but discovered lately when already partially explored). In fact, if $P$ above is the sleep set computed when backtracking to $E$, the first condition ensures that no SSB will be visited. The second condition prevents inserting a sequence for which a possibly equivalent prefix already exists in a given wakeup tree. We skip most details here, and report to [1] for the explanations on how to construct wakeup trees and the corresponding insertion and suppression operations. Simply remember that $WuT(E)$ is populated each time a reversible race at $E$ is detected on a complete continuation of $E$, and consists in inserting in order an initial execution sequence needed to reverse the race from $E$.

*Example 2.* The example shown in Fig. 1 contains a deadlock: if the `ASYNC_SEND` from $P_2$ is executed first and matches the `ASYNC_recv` (from any) of $P_3$ then the second `ASYNC_recv` of $P_3$ can never be fulfilled, and process $P_3$ can never make progress. On this simple example, both DPOR and ODPOR behave the same. They explore a first execution, e.g. $P_1 \cdot P_2 \cdot P_3 \cdot P_3$. After discovering a reversible race between the first and the second transitions (the two `ASYNC_SEND`), they try an execution with those two transitions reversed. While the DPOR will only force the execution of $P_2$ before $P_1$ (at the start of the program), ODPOR will force the whole sequence $P_2 \cdot P_3 \cdot P_3$ also before $P_1$. By further restricting the degree of freedom in the exploration, ODPOR achieves optimality.

Applying ODPOR to our programming model requires defining a valid static dependence relation [22]. It consists in a set of boolean functions, one for each pair of action types, that are used extensively during the ODPOR exploration of the application. The number of functions being quadratic in the number of actions types, covering the full API of both MPI and pthread with only 20 action types dramatically simplifies the definition of the dependence relation and is a serious argument over working directly at the API level (like in [25]).

# 3 Making Verification Efficient and Practical

This section details our two contributions, both being adaptations of ODPOR. In the first subsection we propose an out-of-order traversal of the reduced LTS aimed at improving the efficiency of ODPOR. In the second subsection, we further adapt ODPOR to better explain bugs exhibited during the traversal.

## 3.1 Directed Verification

In the last decade, DPOR variants have been developed with the objective of either reaching optimality, or improving the efficiency in a complete but sub-optimal exploration of the reduced LTS. However, for real size programs, even
reduced LTS may be too large to be explored exhaustively. The challenge that we address is then to increase the chance to quickly find bugs when they exist, while preserving optimality and completeness in the absence of bug.

We first notice that one of the main pitfalls of DPOR techniques, which may hamper their ability to quickly discover bugs, lays in their depth-first search nature. Indeed, depending on the first explored sequence, there is a risk that algorithms start in a region of the state space and spend a huge amount of time unsuccessfully trying to find bugs there, while a single try in a different area would perhaps immediately yield an answer. This problem is exemplified by slightly modifying the program of Fig. 1 as follows.

*Example 3.* Let us consider the program composed of the same $P_1$ and $P_2$, ending with the same actor $P_3$, but with some amount of synchronizations added in between. If (O)DPOR first explores $P_1 \cdot P_2$, it will then have to explore all its continuations before considering a (possibly faulty) run starting with $P_2 \cdot P_1$.

We thus want to maximize the likelihood of detecting undesired behaviors in real size applications that are too large even for reduction techniques to terminate. The idea behind our random-first search ODPOR (RFS ODPOR — presented in Algo. 1) is then to abandon the depth-first search nature of ODPOR. After encountering a maximal execution and computing reversible races, ODPOR would backtrack to a state of this execution with non-empty wakeup tree, *i.e.* from which some unexplored Mazurkiewicz trace remains. Instead, in RFS ODPOR we authorize to jump to any other state with non-empty wakeup tree. This gives much more flexibility to the algorithm in the order in which the reduced state space is built. We could use some heuristics to select the best candidate to continue the exploration.

As we explain now, since ODPOR is tight to the DFS traversal, the modifications are not immediate. We detail the changes required by the algorithm while preserving soundness and optimality.

*WuT and Tree:* as a DFS algorithm, the ODPOR algorithm only stored the stack of currently explored abstract states. Each such state is populated with a wakeup tree, eventually grown by sequences allowing to reverse races at this state. Wakeup trees are later explored when backtracking and then forgotten. This raises an issue in random-first order since starting to unfold wakeup trees before having fully populating them could lead to exploring a same trace twice, thus losing optimality.

We store currently explored executions in a tree-like structure *Tree*, as a counterpart to the call stack of the ODPOR DFS. It helps us traverse the state space at will and preserves optimality by its combination with wakeup trees. When a race is detected (line 17 of RFS ODPOR), a sequence *v* is inserted at a node *E'* in *Tree*, as described by Algorithm 2. The insertion generalizes the insertion in the *WuT* to the *Tree*. It finds the leftmost (in the exploration order) and longest non-contradictory prefix in *Tree*, and continues to the current *WuT* if necessary: when a weak initial *p* of *v* is found in the current node of the tree
<caption>**Algorithm 1 RFS ODPOR(s₀)**</caption>

1: initialize exploration-heads with the empty sequence $\langle\rangle$;
2: choose some $t \in enabled(s_0)$;
3: initialize WuT($\langle\rangle$) with $t$;
4: **while** exploration-heads $\neq \emptyset$ **do**
5:     choose $E \in exploration-heads$;
6:     choose $p$ among nodes of height one in WuT($E$);
7:     done($E$).add($p$);
8:     add $p$ as a child of $E$ in Tree;
9:     sleep($E \cdot p$) := $\{q \in sleep(E) \cup done(E) \mid (p, q) \notin D\}$;
10:    move the subtree of WuT($E$) rooted after $p$ to WuT($E \cdot p$);
11:    **if** WuT($E$) is empty **then**
12:        remove $E$ from exploration-heads;
13:        **if** $E \cdot p$ is maximal **then**
14:            **for** all $i, j \in dom(E \cdot p)$ **such that** $i \preceq_{E \cdot p} j$ **do**
15:                $E' := \text{sub}(E, E_{i-1})$;
16:                $v := \text{notdep}(E_i, E)$.proc($E_j$);
17:                **if** ($sleep(E') \cup done(E')_{<\text{proc}(E_i)}} \cap W I_{[E']}(v) = \emptyset$ **then**
18:                    $E'' := \text{Tree}[E']$.insert($v$);
19:                    exploration-heads.add($E''$);
20:                GarbageCollect($E \cdot p$);
21:            **else**
22:                **if** WuT($E \cdot p$) is empty **then**
23:                    choose $p' \in enabled(\text{last}(E \cdot p)) \setminus sleep(E \cdot p)$;
24:                    initialize WuT($E \cdot p$) with $p'$;
25:                exploration-heads.add($E \cdot p$);

$E$, a recursive call at node $E \cdot p$ is done with sequence $v \setminus p$, i.e. $v$ where the first occurence of $p$ in $v$, if any, is removed; when the algorithm fails to find such an action, it inserts $v$ in the WuT of the current node $E$, and returns $E$ so that ODPOR knows where to explore later.

*Sleep sets:* similar to ODPOR, we use sleep sets to memorize transitions that should not be taken by future explorations, because they start sequences equivalent to already explored ones. In RFS ODPOR, we would need to update sleep sets as soon as some children state is explored, not only when a left subtree is fully explored like in ODPOR. Unfortunately, directly adding those to the sleep set could result in missed executions, as illustrated by the following example.

<caption>**Algorithm 2 Tree[$E$].insert($v$)**</caption>

1: **for all** $p$ **in order of** done($E$) **do**
2:     **if** $p \in W I_{[E]}(v)$ **then**
3:         **return** Tree[$E \cdot p$].insert($v \setminus p$);
4:     insert $v$ in WuT($E$);
5:     **return** $E$;
*Example 4.* Consider an execution *E* leading to state *s*, from which we first explore *p*₁. Suppose that this exploration detects a race leading to insert a sequence starting with *p*₂ in *WuT(E)*. The algorithm then decides to explore that race without completing the exploration of the subtree *E* · *p*₁, hence we need to add *p*₁ to the sleep set so that explorations after *E* · *p*₂ do not execute *p*₁ right away. Now when we go back to *E* · *p*₁ and discover another race after *E* starting with *p*₂, if *p*₂ was already in the sleep set, the race would not be inserted in the *WuT*.

To tackle this issue, we must add some order information to the sleep sets.
In fact, we separate each sleep set into an inherited part, called *sleep(E)* in
the algorithm, and the set of processes explored from *E* ordered according to
insertion time, *done(E)*. When checking for a *weak initial* at line 17, we need
to intersect with the union of *sleep(E')* and those elements of *done(E')* inserted
before the considered one for the race, denoted *done(E')*<sub>*proc(Ei)*</sub>.

Memory management: we implement a procedure *GarbageCollect(E)* which keeps in *Tree* only nodes that could be useful in future explorations. Indeed, due to the ordering of *done(E)*, only explorations on the left of *E* may impact *WuT(E)*. Thus we need to detect when explored nodes cannot be impacted anymore and remove them. A leftmost leaf explored in *Tree* can thus be removed, which triggers *GarbageCollect(E)*. Recursively, a parent node *E'* with no remaining child in *Tree* and in *WuT(E')* is removed. When a parent node with children in *Tree* is found, the procedure recursively tries to close its remaining leftmost leaf. The recursion stops when called from a node with non-empty *WuT*, since it will be triggered again in a future exploration of a leaf in that *WuT*. RFS ODPOR memory consumption remains higher than its DFS counterpart as we need to keep in memory a subtree instead of a single stack. However, thanks to the *GarbageCollect* procedure, the random choice of an element in *exploration-heads* can be biased so that the total memory consumption remains under a given threshold. In fact, if the threshold is nearly reached, the exploration can be biased to leftmost nodes in order to release memory.

**Theorem 1.** *The RFS ODPOR algorithm is sound and optimal in the sense that its explores a unique execution per Mazurkiewicz's trace and explores no sleep-set-blocked execution.*

*Sketch of proof* For the following proof we consider that *GarbageCollect(E)* is disabled so that *Tree* contains all explored sequences, Considering *Tree* at the end of the algorithm, proving soundness boils down to proving that it contains all Mazurkiewicz trace. By contradiction, let us suppose that there exists some execution *E* uncovered by *Tree*, i.e. ∀*E'* ∈ *Tree*, *E* ∉ [*E'*]~. Consider *lg*<sub>*E*</sub> the longest sequence equivalent with a prefix of *E* which has an equivalent execution in *Tree*. Formaly, *lg*<sub>*E*</sub> is the longest sequence such that there exists *v*, *v'* ∈ *T*<sup>*</sup> and *E'* ∈ *Tree* satisfying *E* ≃ *lg*<sub>*E*</sub> · *v* and *E'* · *v'* ≃ *lg*<sub>*E*</sub> · *v'*. Among such sequences *E*, consider now the one with *lg*<sub>*E*</sub> of maximal length. By definition of *lg*<sub>*E*</sub>, there exists some *E'* equivalent to *lg*<sub>*E*</sub> in *Tree*, such that after *E'*, RFS ODPOR explored
some transitions $t_1, \dots, t_k$, but did not explore a transition $t$ that would have led to $E$. In particular, for each $i, t_i \notin WI_{[E']}(v)$ and there is a transition $t'_i$ in $v$ such that $D(t_i, t'_i)$, and each transition $v_1, \dots, v_l$ in $v$ before $t'_i$ is independent with $t_i$. Hence, due to independences, $E' \cdot v_1 \cdots v_l t_i t'_i$ is a possible prefix of a trace of the programm. If the RFS ODPOR explored that prefix at some point, the race between $t_i$ and $t'_i$ would lead to exploring their inversion. Therefore this prefix must not have been explored. But $|lg_{E' \cdot v_1 \cdots v_l t_i t'_i}| \ge |E' \cdot t_i| > |lg_E|$ contradicts the fact that $E$ is maximal for the length of $lg_E$.

To prove optimality, we show that "$Tree \cup \{WuT(E) | E \in Tree\}$ is a wakeup tree" is an invariant for RFS ODPOR, which is similar to the proof of optimality for ODPOR. The invariant is preserved thanks to the way insertion is done inside *Tree* and its prolongation in the *WuT*. In particular, respecting the order in *done* is crucial for verifying that if *u.p* ≺ *u.w* then *p* ∉ *WI*_{[E.u]}(*w*). Once the invariant is shown, if we suppose that two sequences in *Tree* are equivalent, we reach a contradiction with the properties of wakeup trees.

*Example of use: Busy-waiting.* Another interest of RFS ODPOR is its ability to tackle programs that use busy-waiting. This classical pattern in asynchronous parallel programming allows a process to perform computations while waiting for another process, typically through a while loop guarded by a test on a reception or a condition variable. In its extreme form, this pattern consists of an empty loop guarded by a test on an asynchronous action. This is commonly used in HPC to reduce the latency by ensuring that the communication thread remains executed on this empty loop rather than descheduled by the operating system. That way, incoming messages get handled immediately.

Unfortunately, this construct poses a challenge to verification. Indeed, the
application has an unbounded behavior consisting of an infinite number of tests.
However, this behaviors cannot arise in real systems, as it would imply that
the process in a busy-waiting loop executes infinitely often without the other
processes to execute at all. The natural fairness provided by real systems without
failures prevents such behaviors. A classical DFS ODPOR could find its way out
of the infinite loop by randomly trying other processes once in a while, but it may
waste time in the recursive exploration of nearby subtrees that also have that
infinite loop behavior. On the other hand, RFS ODPOR allows the exploration
to backtrack in a completely different area of the code where the busy-waiting
never occurs, hence spending more time effectively looking for a bug.

In [16], the authors propose a specific answer to this problem in the case of
spin loops for weak memory models. They transform busy-waiting into assume
statements (as explained in [17]) and perform important computations to de-
termine whether a given execution could be blocked before effectively visiting
it. This solution is not possible in our case since it requires access to variable
values, which is too costly in our context.

Other works propose to use techniques based on randomization to find bugs.
These techniques goes from randomizing the scheduler [5] to injecting randomly
generated Byzantine behaviors [6]. Using random in those approaches helps cover
a certain part of the program state space and returns results with certain prob-
abilistic guarantees. Those differ from our work in the sense that randomness
only helps us to order the exploration in the hope of finding a bug faster. In
particular, the exploration remains sound and will give a certain result, not a
probabilistic one.

## 3.2 Counter-Example Explainability

In this section, we focus on refining counter-examples found by previous algo-
rithm.

Counter-examples are helpful for developers to understand the flaws and
better correct them. Surprisingly, few work deal with explanability of counter-
examples [14]. Moreover, most work related to model checking need the full state
space to identify actions that cause bugs (see e.g. [3]). These techniques cannot
be applied in stateless model checking, the transition system of the application
is never explicitly built. We then propose to perform some sort of root cause
analysis as an extension of the ODPOR algorithm, and show how it also adapts
to our RFS ODPOR. Our notion of critical transition is close to the notion of
neighbourhood of [3] but contrary to their solution, our algorithm can be adaoted
to ODPOR.

The principle is the following. In a run *E* that fails a property, we call *critical transition* (CT) the last transitions *γ* after which the bug inevitably occurs. Formaly, let *ϕ* be a safety property, *E* such that *E* ≠ *ϕ*. The *critical transition* of *E*, is the unique transition *γ* = (*s*, *a*, *s*') ∈ *E* such that, calling *E'* the prefix of *E* ending in *s*, all maximal continuations of *E'* · *γ* violate *ϕ* and there exists a maximal continuation of *E'* satisfying *ϕ*.

*Example 5.* Let us recall that example 1 contains a deadlock, and that a possible counterexample is $P_2 \cdot P_1 \cdot P_3 \cdot P_3$. Now, if actors 1 and 2 have more code to execute, the counterexamples can become much longer. In fact, they can execute anything that does not interact with actor 3, and the deadlock will only be found when there are done. On the other hand, any execution starting with the action of actor 2 will lead to the deadlock. This is the critical transition to this bug, no matter what the other actions of actor 1 and 2 are.

We propose an algorithm to find the CT that takes advantage of the reduction operated by ODPOR. We illustrate the principles by Fig. 2. After finding a first faulty execution *E*, we switch to the CT mode and keep exploring the reduced state space until finding a correct execution. We then need to decide whether transitions in *E*, some of them with unexplored siblings, lead to correct or incorrect executions. Let *E* = *F* · *b*₁ · ... · *b*ₙ with *F* the prefix from which all alternative traces to *E* (the subtree rooted in *c*₁) have been explored and are correct, by definition. The critical transition is necessarily among *b*₁, ..., *b*ₙ. The set of states {*s*₁, ..., *s*ₙ} can always be partitionned into older ones *S*₁ = {*s*₁, ..., *s*ₖ} with non-empty sleep sets, and the younger ones *S*₂ = {*s*ₖ+₁, ..., *s*ₙ} with empty sleep sets. We can prove (see Appendix) that states in *S*₁ belong to correct executions, so that the critical section lead to a state in *S*₂. Starting
from $s_n$, the ODPOR algorithm then backtracks in $S_2$, using wakeup trees to explore alternatives, until finding a correct execution. The adaptation to RFS ODPOR is similar but requires special attention when the underlying program crashes as explained in the appendix.

<figure><img src="image_2.png" /><figcaption>Fig. 2: An exploration tree at some point during CTF+ODPOR algorithm.</figcaption></figure>

It is worth noting that the CT only identifies the last action that leads to an issue. For instance, in the case of a four-actor deadlock, where $P_1$ and $P_2$ are blocking each other while $P_3$ and $P_4$ are doing the same, the CT is not enough. It captures only the last occurring pair of deadlock. Furthermore, one can look at the causal past of the CT, i.e. the set of transitions executed before the CT, causally related to it. This is interesting since in most cases, it allows replicating the found bug with a much smaller counterexample. But again, the same four-actor deadlock shows this is not enough, and that, in the general case, the causal past does not fully reproduce the bug. In the future, we plan to refine the notion in order to tackle those cases where bugs are caused by apparently unrelated actions. This is mandatory in order to fully take advantage of the information conveyed by the CT.

# 4 Evaluation

We implemented a prototype of our algorithm in Mc SimGrid v3.36.1 to serve as a proof of concept. All experiments were run on Intel Xeon E5-2630 v3 at max 2.40GHz. Programs were compiled using gcc-10.2.1 with -O3 parameter.

## 4.1 Evaluating RFS overhead

In this first experiment, we compare the performance of our implementation of RFS with two state-of-the-art software model checker Nidhugg [1] and DPU [19] over examples taken from the latter evaluation. Nidhugg is an implementation of source-DPOR, a slightly different version of ODPOR that can encounter SSB executions. It is tuned to search pthread code for data races under weak memory models. DPU is a proof of concept implementing unfolding DPOR, an optimal
reduction algorithm based on partial event systems. DPU can only verify mu-
texes operations. The benchmark against which we are testing is composed of
examples taken from the SV-COMP [4] repository. These examples are bug-free,
and scalable in terms of number of processes.

<table><caption>Table 1: Performance comparison for exhaustive exploration. TO means the execution did not finish in 10 minutes while ERR reports a runtime error.</caption>
  <thead>
    <tr>
      <th colspan="2">Benchmark</th>
      <th colspan="2">DPU</th>
      <th colspan="2">Nidhugg</th>
      <th colspan="2">McSimGrid RFS</th>
    </tr>
    <tr>
      <th>Name</th>
      <th>Traces</th>
      <th>Time</th>
      <th>Mem</th>
      <th>Time</th>
      <th>Mem</th>
      <th>Time</th>
      <th>Mem</th>
    </tr>
  </thead>
  <tbody>
    <tr>
      <td>DISP(5,3)</td>
      <td>1482</td>
      <td>0.629</td>
      <td>55M</td>
      <td>6.314</td>
      <td>65M</td>
      <td>2.665</td>
      <td>50M</td>
    </tr>
    <tr>
      <td>DISP(5,4)</td>
      <td>15282</td>
      <td>6.285</td>
      <td>135M</td>
      <td>65.034</td>
      <td>65M</td>
      <td>28.445</td>
      <td>442M</td>
    </tr>
    <tr>
      <td>DISP(5,5)</td>
      <td>151032</td>
      <td>203.785</td>
      <td>973M</td>
      <td>TO</td>
      <td>65M</td>
      <td>289.361</td>
      <td>4191M</td>
    </tr>
    <tr>
      <td>DISP(5,6)</td>
      <td></td>
      <td>ERR</td>
      <td>1016M</td>
      <td>TO</td>
      <td>65M</td>
      <td>TO</td>
      <td>10798M</td>
    </tr>
    <tr>
      <td>MPAT(5)</td>
      <td>3840</td>
      <td>1.860</td>
      <td>80M</td>
      <td>1.203</td>
      <td>64M</td>
      <td>7.210</td>
      <td>144M</td>
    </tr>
    <tr>
      <td>MPAT(6)</td>
      <td>46080</td>
      <td>51.283</td>
      <td>420M</td>
      <td>16.273</td>
      <td>64M</td>
      <td>94.917</td>
      <td>1770M</td>
    </tr>
    <tr>
      <td>MPAT(7)</td>
      <td>645120</td>
      <td>TO</td>
      <td>1553M</td>
      <td>255.109</td>
      <td>64M</td>
      <td>TO</td>
      <td>12951M</td>
    </tr>
    <tr>
      <td>MPAT(8)</td>
      <td></td>
      <td>TO</td>
      <td>1603M</td>
      <td>TO</td>
      <td>64M</td>
      <td>TO</td>
      <td>17055M</td>
    </tr>
    <tr>
      <td>MPC(3,5)</td>
      <td>2958</td>
      <td>0.937</td>
      <td>61M</td>
      <td>37.662</td>
      <td>65M</td>
      <td>4.709</td>
      <td>75M</td>
    </tr>
    <tr>
      <td>MPC(4,5)</td>
      <td>313683</td>
      <td>ERR</td>
      <td>63M</td>
      <td>TO</td>
      <td>65M</td>
      <td>521.814</td>
      <td>6383M</td>
    </tr>
    <tr>
      <td>MPC(5,5)</td>
      <td></td>
      <td>TO</td>
      <td>1344M</td>
      <td>TO</td>
      <td>65M</td>
      <td>TO</td>
      <td>15693M</td>
    </tr>
    <tr>
      <td>PI(7)</td>
      <td>5040</td>
      <td>1.950</td>
      <td>66M</td>
      <td>ERR</td>
      <td>66M</td>
      <td>6.019</td>
      <td>71M</td>
    </tr>
    <tr>
      <td>PI(8)</td>
      <td>40320</td>
      <td>28.748</td>
      <td>273M</td>
      <td>ERR</td>
      <td>66M</td>
      <td>50.453</td>
      <td>555M</td>
    </tr>
    <tr>
      <td>PI(9)</td>
      <td>362880</td>
      <td>TO</td>
      <td>1128M</td>
      <td>ERR</td>
      <td>65M</td>
      <td>505.053</td>
      <td>5172M</td>
    </tr>
    <tr>
      <td>POKE(8)</td>
      <td>3700</td>
      <td>1.934</td>
      <td>99M</td>
      <td>146.232</td>
      <td>65M</td>
      <td>11.427</td>
      <td>186M</td>
    </tr>
    <tr>
      <td>POKE(9)</td>
      <td>5332</td>
      <td>2.913</td>
      <td>124M</td>
      <td>458.337</td>
      <td>65M</td>
      <td>18.004</td>
      <td>292M</td>
    </tr>
    <tr>
      <td>POKE(10)</td>
      <td>7384</td>
      <td>4.479</td>
      <td>152M</td>
      <td>TO</td>
      <td>64M</td>
      <td>26.799</td>
      <td>446M</td>
    </tr>
    <tr>
      <td>POKE(11)</td>
      <td>9904</td>
      <td>6.674</td>
      <td>193M</td>
      <td>TO</td>
      <td>65M</td>
      <td>38.861</td>
      <td>656M</td>
    </tr>
    <tr>
      <td>POKE(12)</td>
      <td>12940</td>
      <td>9.969</td>
      <td>242M</td>
      <td>TO</td>
      <td>65M</td>
      <td>53.417</td>
      <td>874M</td>
    </tr>
    <tr>
      <td>POKE(13)</td>
      <td>16540</td>
      <td>14.506</td>
      <td>310M</td>
      <td>ERR</td>
      <td>64M</td>
      <td>72.032</td>
      <td>1214M</td>
    </tr>
  </tbody>
</table>

The results are presented in Table 1. Experiments have a ten minutes timeout.
For each run, we report the time in seconds and the peak of memory consump-
tion by the applications. Nidhugg can not run on example PI as it involves C
primitives it does not cover. Overall, we observe that our RFS implementation
performs in the same order of magnitude as the state-of-the-art tools regarding
time. On the other hand, the memory consumption is higher. This was intended
as the algorithm may require to keep a tree rather than only a stack in memory.
As a conclusion, the overhead of the RFS approach is not a bottleneck for these
examples. If memory consumption becomes an issue on bigger examples, it is
still possible to tailor the order of exploration. For example when the memory
usage reaches a given threshold, the exploration could focus on leftmost states
so that the *GarbageCollect* procedure reclaims memory.
## 4.2 Evaluating RFS benefits for bug finding

To evaluate the benefits of changing the order of exploration, we ran our algorithm over three bugged codes that can be scaled at will either in the number of synchronizations or in the number of processes:

- *MPI-any* is the MPI code of the program in Fig. 1. The scaling factor is the number of *rendezvous* (*MPI Barriers*) between the sendings and the receptions. Those synchronizations consist of broadcasts. Hence, adding one *rendez-vous* effectively doubles the number of interleaving to consider.

- *philosophers-mutex-deadlock* is an implementation of the dining philosophers using one mutex per fork, scaling with the number of philosophers. A deadlock occurs if all philosopher pick their first fork before a philosopher considers its second fork.

- *philosophers-semaphore-deadlock* is a variant of the same program, with an additional semaphore restricting the number of philosophers allowed to pick forks. A deadlock occurs since the initial number of tokens in the semaphore equals the number of philosophers.

We ran four variants of ODPOR over these examples: DFS, Uniform-DFS, Uniform-RFS Branch and Uniform-RFS Step. DFS is the classical ODPOR algorithm from [1] running in an arbitrary depth-first search manner. When confronted to a choice, it picks the process with the smaller identifier. The Uniform-DFS variant resolves those choices with a uniform random pick. The last two variants both resolve choices with a uniform pick: the “Step” variant picks any element in *exploration-heads* at each step, while the “Branch” variant completes a branch before choosing any element in *exploration-heads*. Randomized explorations are run 100 times each, with 100 different seeds. The results depicted in Fig. 3 show the number of states explored before finding a deadlock when the scaling factor varies.

All runs of *MPI-any* (1st table) and *philosophers-mutex-deadlock* (2nd table) terminate in less than 5mn, while for *philosophers-semaphore-deadlock* (3rd table) some runs timeout after 10mn without finding a bug. For these runs, the number of states explored before timeout is used, allowing the box plots to depict the success rate of a given strategy for large applications. The number of timeouted runs (over 100) is written above each box plot.

The first experiment with *MPI-any* illustrates an example where the scaling is in number of operations per actor. In this case, randomizing the original DFS algorithm with Uniform-DFS helps keep the average time on a linear scale, but at least 25% of the executions still behave as badly as the worst-case scenario. On the opposite, both Step-RFS and Branch-RFS runs 75% of the time faster than the average for Uniform-DFS, with Branch-RFS behaving a bit better in that example. This is because Branch-DFS has the opportunity to explore a faulty execution each time it backtracks.

The other experiments are examples of scaling in the number of actors, with the semaphore variant having many more interleaving to consider. On the smaller example of *philosophers-mutex-deadlock*, it is hard to conclude to any trend. By
<figure><img src="image_3.png" /><figcaption>Fig. 3: Number of states explored before finding the deadlock at various scales.</figcaption></figure>
trying whole sequence and never a few steps, Branch-RFS is in average the slowest version, while Step-RFS tends to explore in parallel different sequences step-by-step, and faster reaches deadlocks that are located somewhere in the middle of the state space. The trend is more visible on the biggest example *philosophers-semaphore-deadlock*. In that case, for ten philosophers, only 4 executions out of 100 finished in under 10 minutes with Unfirom-DFS while other executions visit more than 10 millions nodes without finishing. Our solution performs better with Step-RFS finishing 98% of the times, visiting an average of only 12,000 nodes before finding the bug. Step-RFS does not behave like a BFS exploration as one could expect. This is due to the high restriction the reduction has on the state space. By extensively limiting the number of parallel branches opened at the same time, the reduction turns a simple random step variation into a working trade-off over the various situations. These preliminary experimental results are promising for the efficiency of our techniques to detect bugs in real-size applications.

In all these experiments, we also evaluated the CT overhead. The worst case is when the first explored execution leads to a fault, in which case CT must explore entirely the sub-tree around that run while it can reuse previously explored traces otherwise. That exploration is very fast in the two *philosophers* benchmarks as the critical transition is one of the last trace's actions, but takes more time for the first benchmark where the critical transition is the very first action in the trace. This is indeed the worst case for the CT algorithm, as it needs to exhaustively explore the reduced LTS searching for a correct execution which does not exist.

# 5 Conclusion and Future Work

In this paper, we proposed two adaptations of ODPOR, a state-of-the-art Dynamical Partial Order Reduction technique, focused on bug finding and explanation, implemented in Mc SimGrid. First, the RFS ODPOR variant allows arbitrary orderings of the state space exploration. This degree of freedom shows promising results in discovering faulty behaviors early. Second, we adapted further the ODPOR technique with a novel algorithm for counter-example explainability, based on the notion of critical transition, which requires minimal computation overhead. In the future, we plan to search for model specific heuristics in order to further accelerate RFS ODPOR in the presence of faults in the program. Thanks to its design, RFS ODPOR also paves the way for intensive parallelization through producer-consumer patterns. Finally, we aim at refining our notion of critical transition in order to explain counter-examples a step further.

# References

1. ABDULLA, P. A., ARONIS, S., JONSSON, B., AND SAGONAS, K. Optimal dynamic partial order reduction. In *The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14* (2014), S. Jagannathan and P. Sewell, Eds., ACM, pp. 373–384.
2. ABDULLA, P. A., ARONIS, S., JONSSON, B., AND SAGONAS, K. Source sets: A foundation for optimal dynamic partial order reduction. *J. ACM* **64**, 4 (2017), 25:1–25:49.

3. BARBON, G., LEROY, V., AND SALAÜN, G. Debugging of behavioural models using counterexample analysis. *IEEE Trans. Software Eng.* **47**, 6 (2021), 1184–1197.

4. BEYER, D. Software verification with validation of results (Report on SV-COMP 2017). In *Proc. TACAS* (2017), LNCS 10206, Springer, pp. 331–349.

5. BURCKHARDT, S., KOTHARI, P., MUSUVATHI, M., AND NAGARAKATTE, S. A randomized scheduler with probabilistic guarantees of finding bugs. *SIGPLAN Not.* **45**, 3 (Mar. 2010), 167–178.

6. BURCKHARDT, S., KOTHARI, P., MUSUVATHI, M., AND NAGARAKATTE, S. A randomized scheduler with probabilistic guarantees of finding bugs. *SIGPLAN Not.* **45**, 3 (Mar. 2010), 167–178.

7. CAI, Y., YAO, P., YE, C., AND ZHANG, C. Place your locks well: Understanding and detecting lock misuse bugs. In *32nd USENIX Security Symposium (USENIX Security 23)* (Anaheim, CA, Aug. 2023), USENIX Association, pp. 3727–3744.

8. CASANOVA, H., GIERSCH, A., LEGRAND, A., QUINSON, M., AND SUTER, F. Versatile, scalable, and accurate simulation of distributed applications and platforms. *Journal of Parallel and Distributed Computing* **74**, 10 (June 2014), 2899–2917.

9. COOPERMAN, G., AND QUINSON, M. Stthread: In-Vivo Model Checking of Multithreaded Programs. *The Art, Science, and Engineering of Programming* (2020).

10. DEGOMME, A., LEGRAND, A., MARKOMANOLIS, G. S., QUINSON, M., STILLWELL, M., AND SUTER, F. Simulating MPI applications: The SMPI approach. *IEEE Trans. Parallel Distrib. Syst.* **28**, 8 (2017), 2387–2400.

11. FLANAGAN, C., AND GODEFROID, P. Dynamic partial-order reduction for model checking software. In *Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005* (2005), J. Palsberg and M. Abadi, Eds., ACM, pp. 110–121.

12. FORUM, T. M. MPI: a message passing interface. In *Proceedings Supercomputing '93* (1993), B. Borchers and D. Crawford, Eds., ACM, pp. 878–883.

13. JHALA, R., AND MAJUMDAR, R. Software model checking. *ACM Computing Surveys (CSUR)* **41**, 4 (2009), 1–54.

14. KALEESWARAN, A. P., NORDMANN, A., VOGEL, T., AND GRUNSKE, L. A systematic literature review on counterexample explanation. *Information and Software Technology* **145** (2022), 106800.

15. KOKOLOGIANNAKIS, M., MARMANIS, I., GLADSTEIN, V., AND VAFEIADIS, V. Truly stateless, optimal dynamic partial order reduction. *Proceedings of the ACM on Programming Languages* **6**, POPL (2022), 1–28.

16. KOKOLOGIANNAKIS, M., MARMANIS, I., AND VAFEIADIS, V. Unblocking dynamic partial order reduction. In *Computer Aided Verification* (Cham, 2023), C. Enea and A. Lal, Eds., Springer Nature Switzerland, pp. 230–250.

17. KOKOLOGIANNAKIS, M., REN, X., AND VAFEIADIS, V. Dynamic partial order reductions for spinloops. In *2021 Formal Methods in Computer Aided Design (FMCAD)* (2021), pp. 163–172.

18. LAMPORT, L. Time, clocks, and the ordering of events in a distributed system. *Commun. ACM* **21**, 7 (July 1978), 558–565.

19. NGUYEN, H. T. T., RODRÍGUEZ, C., SOUSA, M., COTI, C., AND PETRUCCI, L. Quasi-optimal partial order reduction. In *Computer Aided Verification* (Cham, 2018), H. Chockler and G. Weissenbacher, Eds., Springer International Publishing, pp. 354–371.
20. NICHOLS, B., BUTTLAR, D., AND FARRELL, J. *Pthreads programming: A POSIX standard for better multiprocessing.* " O'Reilly Media, Inc.", 1996.

21. PALMER, R., GOPALAKRISHNAN, G., AND KIRBY, R. M. Semantics driven dynamic partial-order reduction of MPI-based parallel programs. In *Proceedings of the 2007 ACM Workshop on Parallel and Distributed Systems: Testing and Debugging* (2007), PADTAD '07, ACM, pp. 43–53.

22. PHAM, T. A. *Efficient state-space exploration for asynchronous distributed programs: Adapting unfolding-based dynamic partial order reduction to MPI programs.* PhD thesis, École normale supérieure de Rennes, France, 2019.

23. PHAM, T. A., JÉRON, T., AND QUINSON, M. Verifying MPI Applications with SimGridMC. In *Correctness 2017 - First International Workshop on Software Correctness for HPC Applications* (Denver, United States, Nov. 2017), pp. 28–33.

24. RODRÍGUEZ, C., SOUSA, M., SHARMA, S., AND KROENING, D. Unfolding-based partial order reduction. In *26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 14, 2015* (2015), L. Aceto and D. de Frutos-Escrig, Eds., vol. 42 of *LIPIcs*, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 456–469.

25. YANG, Y., CHEN, X., GOPALAKRISHNAN, G., AND KIRBY, R. M. Distributed dynamic partial order reduction based verification of threaded software. In *Proceedings of the 14th International SPIN Conference on Model Checking Software* (Berlin, Heidelberg, 2007), Springer-Verlag, p. 58–75.

26. ZHANG, N., KUSANO, M., AND WANG, C. Dynamic partial order reduction for relaxed memory models. In *Proceedings of the 36th ACM SIGPLAN conference on programming language design and implementation* (2015), pp. 250–259.
A Critical Transition Search: more details

We first recall what a critical transition is, before giving some details of the
CT-search algorithm using ODPOR, and a necessary adaptation required for
the RFS ODPOR algorithm.

Let $\varphi$ be a safety property, $E$ a faulty execution, i.e., $E \not\models \varphi$. The critical
transition of $E$, is the unique transition $\gamma = (s, a, s') \in E$ such that, calling $E'$
the prefix of $E$ ending in $s$:

- there exists a maximal continuation of $E'$ satisfying $\varphi$,

- all maximal continuation of $E' \cdot \gamma$ violate $\varphi$.

Since a critical transition characterizes the last step necessary to produce a
given bug, it requires the existence of a faulty execution. On the opposite side,
in the limit case when there is no correct execution, the critical transition is the
start transition.

We restart to explain the principle of the CT-search algorithm on a schematic
representation given by Fig. 2 of the general situation encountered while running
the CT algorithm. Let $E = F \cdot b_1 \cdots b_n$ be the first incorrect execution reached
during the exploration phase, with $F$ a prefix from which all alternative traces
to $E$ have been explored and are thus correct (as well as all their equivalent
executions). In the figure, the execution in the subtree rooted in $c_1$ examplifies
this: they have been explored previously and are all correct. Hence, the critical
transition is among $b_1, \dots, b_n$. Let the set of states $\{s_1, \dots, s_n\}$ be partitioned
into those with a non-empty sleep set, $S_1 = \{s_1, \dots, s_k\}$, and those with empty
sleep sets $S_2 = \{s_{k+1}, \dots, s_n\}$. This partition always has this form where both
parts are contiguous: indeed $s_1, \dots, s_n$ have no siblings yet, hence $\mathit{sleep}(s_n) \subseteq
\mathit{sleep}(s_{n-1}) \subseteq \dots \subseteq \mathit{sleep}(s_1)$. We perform a case analysis to prove that states
in $S_1$ are in a correct execution, and then show how the critical section can be
found among states in $S_2$:

**Non-empty sleep set:** let $s_i$, $1 \le i \le k$ be a state in $S_1$ thus with a non-empty sleep set, and let $p \in \mathit{sleep}(s_i)$. By definition of sleep-sets, there exists $e' \in \mathit{dom}(F)$ s.t., writing $F' = \mathit{pre}(F, e')$, $p \in \mathit{enabled}(F')$, $p$ has been explored after $F'$, and $p$ commutes with each action in $\mathit{proc}(e') \cdots b_1 \cdots b_{i-1}$. Intuitively, for $p$ to be in the sleep-set of $s_i$, a previous exploration diverging from $E$ must have been visited. That diverging exploration is of the form $F' \cdot p$, and $p$ must be independent with every action taken since that moment. Since the exploration backtracked from $F' \cdot p$, by the soundness of the ODPOR algorithm we can say that every trace starting by $F' \cdot p$ has been explored. In particular, every trace starting by $F' \cdot p \cdot \mathit{proc}(e') \cdots b_1 \cdots b_{i-1} \simeq F' \cdot \mathit{proc}(e') \cdots b_1 \cdots b_{i-1} \cdot p$ has been explored. Since $F \cdot b_1 \cdots b_n$ is the first incorrect execution encountered, $F' \cdot \mathit{proc}(e') \cdots b_1 \cdots b_{i-1} \cdot p$ must lead to correct executions only. Consequently, we can conclude that any state in $S_1$ belongs to a correct execution.

**Empty sleep set:** we now show how to search the CT in $S_2$. When reached
during backtracking, a state $s_i \in S_2$ has an empty sleep set, thus there was
no other explored execution equivalent to one continuing after $s_i$. Therefore, when backtracking at $s_i$, the executions starting by transitions not in the wakeup tree of $s_i$ are equivalent to some already explored ones (by soundness of the ODPOR algorithm). Hence, if we did not find a correct execution during the CT up to the state $s_i$, and we fully explored its wakeup tree, then there is no correct execution from state $s_i$. The CT algorithm can backtrack one step further.

*Preserving persistence after a crash* One remaining difficulty to solve is linked to the fact that programs are really executed in Mc SimGrid, and as ODPOR algorithms are stateless, we never dispose of the complete transition system. Consider a state *s* in which *enabled(s)* = {*p*₁, ..., *p*ₙ}, and such that executing *p*₁ leads to a crash of the program. The issue is that, of course, no other *p*ᵢ can be executed, since after executing *p*₁ the program execution does not exist anymore. Nevertheless, we need to preserve the soundness of the reduction and ensure that we give the opportunity to the algorithm to execute runs in other orders during CT-serach. In other words, when encountering a bug, the persistence property of the programming model may be lost. To overcome this difficulty, we need to adapt RFS ODPOR so that it keeps exploring other traces when reaching such crashes. This adaption is close to what is proposed by the author of ODPOR [1] in the case of non-persistent models. The difference is that we only adapt it for the very specific case of bugs encountered during CT, while covering the general case requires much more adaptation.