Crate interweave 

Stateless model checking for small concurrent programs.

interweave explores the interleavings of concurrent processes and checks that every one of them is correct. Processes are written as ordinary Rust Futures and driven by a custom single-threaded, deterministic executor. Synchronization primitives — the built-in Atomic and an MPSC channel (Sender / Receiver) — are implemented from scratch so that every operation that can interact with another process becomes an explicit scheduling point: an .await that hands control back to the checker.

That strategy is Optimal DPOR (Abdulla et al., POPL’14): it explores exactly one interleaving per Mazurkiewicz equivalence class.

Example

A writer stores a value and a reader expects to see it — but nothing orders the two, so on the interleaving where the read beats the store the reader observes the initial value and fails. Optimal DPOR finds exactly that schedule:

use interweave::{World, explore};

fn racy(world: &mut World) {
    let x = world.atomic("x", 0);
    let writer = x.clone();
    world.spawn("writer", async move {
        writer.store(1).await;
        Ok(())
    });
    world.spawn("reader", async move {
        match x.load().await {
            1 => Ok(()),
            v => Err(format!("read {v} before the store landed").into()),
        }
    });
}

// `()` is the no-op observer. Optimal DPOR finds the schedule where the
// reader runs first and sees the initial `0`.
explore(&racy, &mut ()).expect_err("the reader can run before the writer");

How it fits together

• Build a program on a World: spawn the processes and create the shared objects they communicate through.
• Communicate through synchronization primitives whose every observable operation is a scheduling point — the built-in Atomic and unbounded MPSC channel (Sender / Receiver), or your own via Object and World::register.
• Explore with explore: it runs Optimal DPOR over the program and returns the first FailedState, or Ok(()) if no interleaving fails. An Observer watches the search through one Observer::step callback fired at each decision the algorithm makes — a Step::Visit for every state it reaches and a Step::Maximal for every complete interleaving, among other Step cases — delivered with a StepCx view.

Custom synchronization objects

Atomic is built on the same public surface you can use yourself: implement the Object trait for a from-scratch primitive (a lock, a channel, a barrier) so that each of its observable operations becomes a Transition the strategy schedules, then register it with World::register. See Object for the operation lifecycle and the dependency relation that drives the reduction, and examples/custom_object.rs for a tiny worked primitive.

Structs

Atomic

A cloneable handle to a shared atomic cell.

FailedState

A reproducible failure returned by explore.

ProcessError

The error reported when a process future returns Err, naming the process.

Receiver

The receiving half of an MPSC channel. It is intentionally not Clone, because the channel’s dependency relation assumes a single consumer.

Sender

The sending half of an MPSC channel; cloneable, so several producers can share it.

State

A node in the search tree: the program after a sequence of Transitions has been applied. An Observer receives one at every state the search reaches and inspects it — its trace, its world for resolving names and labels, whether it is_terminal, and any failure_reason.

StepCx

The read-only context accompanying a Step: the live State, the committed prefix, the per-depth sleep sets and pending operations, and the frontier wakeup tree. Everything is borrowed for the step call — clone out what you need to keep.

Transition

One schedulable step: a process performing one observable operation on one synchronization object — the unit the search picks at each scheduling point.

WakeupNode

A read-only view of one wakeup-tree node. Children are in ≺ (sibling) order; children()[0] is the ≺-minimal branch.

World

The program under test: a builder that owns the processes and synchronization objects created on it. A setup closure populates it via spawn, atomic, and channel. That closure must be deterministic — building the same objects in the same order every time.

Enums

FailureReason

Why a State makes no further progress, as reported by State::failure_reason and carried by a FailedState.

RaceOutcome

How the reordering of a reversible race (Step::Race’s v) resolved against the wakeup tree. insert_depth, where present, is the depth the fragment targets — the point just before the earlier racing event.

Step

A discrete decision of the Optimal DPOR driver, delivered to Observer::step together with a StepCx.

Traits

Object

A synchronization primitive as the model sees it: a small state machine whose every observable operation is a schedulable Transition.

Observer

A hook into the search, called as it explores.

Functions

explore

Enumerates interleavings of the program built by setup under Optimal DPOR.

Type Aliases

ObjectID

Index of an object in the World’s object table, assigned in registration order; doubles as the object’s identity. A custom Object receives its ObjectID from World::register and stamps it into every Transition it builds.

ProcessID

Index of a process in the executor’s process table; doubles as its identity. Exposed through Transition::pid.

ProcessResult

Output of a process future: Ok(()) on clean completion, or an error that the model surfaces as a crate::ProcessError.