Introduce Round-Robin Exploration and Relinearization Schemes

[maxwellpirtle]

Motivation

Explicit-state model checking algorithms are generally split into three main phases: exploration, race detection, and backtracking. During the exploration phase, the model checker selects an arbitrary thread schedule to explore. At each step of the exploration, race detection determines which future thread schedules need to be explored based on the current exploration and stores information about obtaining these schedules. In the case of DPOR, the potential schedules are stored in the backtrack set. Once exploration can no longer continue, either because there are no more threads to schedule (e.g., if all threads have exited) or because the program is in deadlock, the model checker backtracks until it encounters a point in the current exploration marked during the race detection phase to start a new exploration phase.

Historically, the McMini model checker selected the thread of lowest thread ID among those enabled threads during the exploration phase. However, this is problematic in programs with loops where a single thread may run for a long time before allowing other threads to run. Since many multithreaded bugs occur due to specific interactions between threads, rather than the execution of a single thread in isolation, McMini may not identify the problematic trace except after a large number of executions, due to the depth-first nature of DPOR. This scheduling strategy is especially problematic when limiting the depth of any given trace because one thread may consume all available scheduling slots without permitting other threads to be scheduled. Consequently, most races are missed in these cases. Although completeness is currently not guaranteed when limiting the total depth of a single trace, many bugs can still be identified even in this limited context if enough possible races are observed.

The pitfalls of the historic McMini scheduler motivates the need for a new exploration strategy. This PR introduces the round robin exploration strategy. In the round robin exploration strategy, McMini will whenever possible fairly schedule threads during exploration. This gives a chance for all threads to make progress and prevents starvation. Note that McMini must obey scheduling constraints imposed by the operations the threads run. For example, a thread attempting to acquire a locked mutex will not be eligible for scheduling until the lock is made available.

Round Robin Scheduling Pitfalls and Solutions

Round robin scheduling of threads during exploration enables McMini to detect bugs between interacting threads sooner, especially when using depth bounding. However, the resulting traces are hard to analyze because, by construction, threads are constantly selected only to execute a small number of operations (typically only a single operation) before being suspended in favor of scheduling other threads when possible. Constantly switching between thread actions is very challenging to analyze, even when given a trace leading to a bug.

To resolve the problem of producing traces that are difficult to analyze, this PR introduces relinearization. The key idea is that the true "useful" information encoded by a trace is the happens-before relation imposed upon it by the transitions in the trace. We observe that some operations are independent of one another, in the sense that reordering these operations with respect to one another doesn't change the final state (or bug) produced. Indeed, any particular trace is simply a specific linearization (ordering of operations) of the happens-before relation the trace represents. Given this observation, the goal is to reorganize the independent operations in a complex trace involving many thread context switches produced by during round robin exploration so as to minimize the total number of context switches.

The problem of minimizing context switches between threads in a trace can be seen as a graph problem. We can convert the transitions of a trace into an unweighed, colored DAG with nodes representing positions in the trace, edges representing happens-before dependencies, and using the thread executing each operation as the colors. Using the graph representation, the problem can be reformulated as such:

Consider a colored DAG, G, with vertices V and edges E and a coloring function f: V —> C (where C is a finite set of colors). A linearization L of the vertices of G is a sequence of vertices v_i such that the order of v_i obeys the DAG edge ordering: a node ‘u’ appears before any node with which a directed edge from that node to any other node (formally u < v in L iff (u,v) in E).

A colored linearization is the sequence of colors c_1, c_2, … of a linearization v_1, v_2, …, where c_i = f(v_i). Let h: L —>N denote the number of “inversions” in a linearization L. A linearization L has an inversion (v_i, v_i+1) iff f(v_i) != f(v_i+1). Let Inversions: L --> N counts the number of inversions of a colored linearization of G. Then MinInversions is the problem of finding argmin (Inv L) over all linearizations of G.

It turns out that this problem can be mapped to an instance of the Sequential Ordering Problem. Unfortunately, this problem is NP-Hard in the general case, but for the trace sizes McMini handles plus a some optimizations specific to MinInversions described in the comments, in practice producing such optimal traces is feasible using a mixed-integer programming (MIP) solver such as SCIP. Indeed, SCIP is used to produce such minimal schedules. To produce non-optimal, but still close-to-optimal, schedules, a greedy relinearization algorithm is also implemented.

Very detailed comments are contained in the source code explaining the different reasoning behind each block of code, so I won't go into detail here. See the comments in classic_dpor.cpp for more details.

Using New Features

Round Robin Exploration

Round robin exploration can be enabled using the --round-robin/-rr flag in McMini:

./mcmini -rr ./a.out

Greedy Relinearization

To enable relinearization using the greedy approach, you can use the --relinearize/-relin flags

./mcmini -relin ./a.out

This can be combined with round robin exploration to give

./mcmini -rr -relin ./a.out

Optimal Relinearization

To enable testing optimal relinearizations, SCIP must first be installed. Then, McMini must be compiled to use SCIP. To enable this, toggle the new MCMINI_USE_SCIP CMake option:

cmake -B build -DCMAKE_BUILD_TYPE=Debug -DMCMINI_USE_SCIP=YES

To run with optimal relinearization, use the -orelin flag

./mcmini -rr -orelin ./a.out

If McMini is not compiled with SCIP, -orelin falls back to using the greedy method -relin described above.

Misc Bug Fixes/Features

Several other smaller features are introduced by this PR

1. An important bug fix resolving an issue computing clock vectors was resolved. In short, the clock vectors that were used to compute the happens-before relation were incorrect (off-by-one). This also affected accumulating clock vectors during expansion.
2. Trace reporting was moved to the reporter class. The goal was to replace the callback function interface of model_checking::algorithm.
3. Some other features of classic McMini (such as quieting output) were also added to the command line.

[coderabbitai]

Important

• 🔍 Trigger review

This repository does not receive automatic reviews because it has fewer than 10 stars.

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro Plus

Run ID: 56d79fb0-f6ac-46c2-8110-5411ba154dd9

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}