Building a Tiny Model Checker, Part 4

Sleep sets, partial-order reduction, and beyond.

In the previous posts, we incrementally built a tiny model checker:

• Part 1 introduced a cooperative scheduler capable of enumerating all interleavings.
• Part 2 added shared state and safety checking.
• Part 3 introduced blocking and waiting via AWAIT.

At that point, the checker was already capable of finding real concurrency bugs, but it explored far too many executions. This final post addresses that problem.

1. State-space explosion

The fundamental challenge in systematic exploration of concurrent programs is state-space explosion. Even very small programs can exhibit an enormous number of possible executions, caused solely by different interleavings of otherwise independent steps.

Taking the examples from the previous post, the SPSC ring buffer already yields hundreds of thousands of executions, whereas the ticket lock with just three tasks produces over half a million executions.

Most of these executions are redundant: they differ only in the order of operations that do not affect the observable behavior of the program.

To make systematic exploration practical, we must avoid exploring executions that are equivalent under reordering of independent steps.

Two steps are independent if swapping their execution order cannot affect the program’s observable behavior. In this checker, independence is defined conservatively.

Two memory accesses commute if and only if:

1. they access different locations, or
2. they are both reads of the same location.

All other transitions, including AWAIT, YIELD, and other operations, are treated as dependent.

This conservative choice is essential for soundness. If we ever classify two dependent transitions as independent, we may prune away a real bug.

2. Sleep sets

Sleep sets are a classical partial-order reduction technique. I first learned about them from the seminal paper “Model Checking for Programming Languages using VeriSoft” by Godefroid.

At a given scheduling point, the scheduler has a set of enabled transitions. Some of these transitions can be safely ignored, because exploring them would only lead to executions that are equivalent to ones explored elsewhere. A sleep set records exactly those transitions that should not be explored at the current point.

Let E(s) be the ordered list of enabled transitions at state s. If transition t ∈ E(s) is chosen, the sleep set Z for the successor state s' is computed as:

Z(s') = { u ∈ Z(s) | u ⫫ t } ∪ { u ∈ E(s) | u < t ∧ u ⫫ t }

Here:

• ⫫ denotes independence (commutativity),
• < is the fixed ordering of enabled transitions at s.

Intuitively, we keep sleepers that still commute with t, and we add earlier enabled transitions that commute with t, since they could have been taken instead.

3. Sleep sets in a replay-based checker

Sleep sets are traditionally presented in the context of a depth-first search algorithm with undo. As the search descends and backtracks, sleep sets are pushed and popped together with the program state (see Figure 3 / Algorithm 2 in Godefroid’s VeriSoft paper).

Our checker works very differently.

Instead of undoing transitions, it explores executions by replay:

1. Run the program from the initial state to completion.
2. Record the scheduling history.
3. Restart from the initial state.
4. Replay the prefix up to the next unexplored scheduling point.
5. Diverge and continue.

There is no in-place backtracking and no undo operation.

Nevertheless, sleep sets adapt naturally to this execution model because they are a local pruning criterion. At a given scheduling point, the sleep set depends only on the set of currently enabled transitions, the transition chosen at that point, and the current sleep set. None of this requires an undo mechanism.

In our replay-based explorer, the sleep set is reset at the beginning of each execution. Then, at each scheduling point, the sleep set is updated based on the chosen transition. If all enabled transitions are in the sleep set, the current execution is pruned immediately.

Here is the strategy used to pick the next task index:

(define (pick-next-tasks)
  (let* ((E *tasks*)
         (n (length E))
         (Z *sleepset*))
    (let-values (((idx hist) (pick/dfs *prev-hist*)))
      (set! *prev-hist* hist)
      (let ((k (next-nonsleep-index E Z idx)))
        (if (not k)
            ;; no choice left: prune this node
            #f
            (let ((Z' (sleepset-child E Z k)))
              (set! *sleepset* Z')
              (add-history k (- n 1))
              k))))))

Sleep sets show up here in two places:

• next-nonsleep-index skips transitions whose identities appear in the current sleep set Z.
• sleepset-child computes the sleep set for the successor scheduling point, based on the chosen transition.

This matches the intent of sleep sets: once all remaining transitions commute with previously explored ones, continuing the execution would only produce redundant interleavings.

Computing the child sleep set

Let E be the ordered list of enabled transitions at the current scheduling point, and let i be the index of the chosen transition.

The child sleep set is computed as:

(define (sleepset-child E Z i)
  (let* ((md-i (md-at E i)))
    (map car
      (filter (lambda (t)
                (commute? (cdr t) md-i))
              E))))

Conceptually, this implements the sleep-set update rule from the previous section: the next sleep set is derived from the chosen transition and the current enabled set, discarding transitions that do not commute with the chosen step.

Picking the next enabled transition

When selecting the next task to run, we skip transitions that are currently sleeping:

(define (next-nonsleep-index E Z i)
  (let loop ((k i))
    (cond ((>= k (length E)) #f)
          ((memq (task-id-at E k) Z) (loop (+ k 1)))
          (else k))))

If no such transition exists, the current execution is pruned,

Transition identity and task IDs

Sleep sets must refer to stable identities. Queue indices are not stable: tasks may block, resume, or terminate, causing indices to shift. Using indices turned out to be error-prone and led to unsound pruning and crashes.

A safer approach is to assign a task identifier (tid) to each task at spawn time:

(define *current-tid* (make-parameter 0))

(define (spawn thunk)
  (parameterize ((*current-tid* (new-tid)))
    ...))

Sleep sets store such tids, not queue indices. This is sound under the assumption that at most one enabled transition per task exists at any scheduling point.

That assumption holds here: each task has exactly one runnable continuation. If the checker were extended to allow multiple enabled transitions per task, sleep sets would need to track transition identities rather than task IDs.

For the complete implementation, see the full implementation.

Effect of sleep sets on exploration size

Sleep sets reduce the number of explored executions by pruning schedules that differ only by reordering of independent steps. The effect depends strongly on how much independent structure the program exposes.

Several patterns emerge:

• Shared counter: no reduction is expected. Each task effectively contributes a single atomic step, so there are no independent internal operations to reorder.
• Ring buffer: sleep sets collapse a very large number of redundant interleavings, because many reads and writes commute.
• Ticket lock: the reduction is significant, but the remaining executions still encode real ordering constraints imposed by the lock protocol.
• Message passing: sleep sets prune reorderings among receivers, but cannot eliminate schedules that differ in the relative timing between sender writes and receiver reads.

Intuitively, sleep sets aim to explore roughly one execution per Mazurkiewicz trace under the checker’s commutativity relation, rather than one execution per raw schedule. This explains both their effectiveness and their limits: only executions that are equivalent under reordering of independent transitions are pruned.

4. Extensions now that the checker exists

With the core checker complete, several extensions become natural.

ASSUME vs ASSERT

ASSERT rejects executions where a condition fails.

An ASSUME would instead prune executions that violate a condition:

(ASSUME (> x 0))

Semantically:

• ASSERT expresses a safety property.
• ASSUME restricts the explored behavior space.

A related primitive, STOP, would immediately terminate the current execution without failure. Both are straightforward to add in a replay-based explorer.

Waiting on multiple locations

AWAIT loc models busy-waiting on a single variable.

Many algorithms busy-wait on conditions involving multiple variables (e.g. Peterson’s lock). Modeling this precisely suggests extensions such as:

(AWAIT-ANY loc1 loc2 ...)

or even:

(AWAIT (lambda () condition-over-shared-state))

A simple but sound approach is to wake the task on any write to any referenced location, accepting spurious wake-ups to preserve correctness.

Atomic blocks and memory footprints

Currently, ATOMIC is treated as conflicting with everything. This is conservative and sound, but limits reduction.

A natural extension would be to track which locations are read or written inside an atomic block via user annotations. This would allow atomic blocks to commute when their footprints do not conflict.

RMW, CMPXCHG, and conditional writes

The current RMW primitive models an atomic read-modify-write, but cannot express conditional updates such as CMPXCHG. Modeling compare-and-exchange faithfully requires treating it as a read, followed by a potential write.

For commutativity, this means conservatively assuming conflicts with writes, even when the write does not occur.

CHOOSE inside atomic blocks

Originally, I considered disallowing CHOOSE inside ATOMIC. In the current design, however, this restriction is unnecessary: since atomic blocks are treated as conflicting with all other transitions, invoking CHOOSE inside an atomic block is sound. No commutativity-based pruning can cross the atomic boundary, so the nondeterministic choice remains fully explored.

If atomic blocks were later refined to commute selectively, CHOOSE would again become problematic, since it can affect control flow in ways not captured by memory footprints. For now, treating ATOMIC as fully conflicting keeps the semantics simple and correct.

5. Closing remarks

At the end of this series, the Tiny Model Checker (TMC) supports:

• systematic interleaving exploration,
• safety checking,
• blocking and waiting,
• and partial-order reduction via sleep sets.

The reduction implemented here is sound but not optimal. It prunes redundant executions locally, based on commutativity of enabled transitions, but it does not implement Dynamic Partial Order Reduction (DPOR). In particular, the checker does not retroactively introduce new backtracking points based on observed conflicts. All exploration decisions are made forward, during replay, rather than by conflict-driven backtracking.

That is a good place to stop – for now. In the future, I may try implementing TruSt, as described in “Truly Stateless, Optimal Dynamic Partial Order Reduction” by Kokologiannakis et al.

If you want to try out the code yourself, you can download:

• Tiny Model Checker v4,
• Shared counter example,
• Message passing example,
• SPSC ring buffer example,
• and Ticket lock example.

See also other parts of this series. Feedback is welcome – please send a message to my public inbox: ~db7/public-inbox@lists.sr.ht (Archive)

© 2024-2026 db7 — licensed under CC BY 4.0.