must/
lib.rs

1//! A model checker for message-passing concurrency.
2//!
3//! `must` explores every distinct way the messages of a distributed protocol can be
4//! delivered and checks your assertions against all of them. It implements the Must
5//! optimal dynamic partial-order reduction (Enea et al., "Model Checking Distributed
6//! Protocols in Must", OOPSLA 2024): each meaningfully different execution is visited
7//! exactly once, with no duplicate interleavings.
8//!
9//! # Example
10//!
11//! Two peers race to send one message; a third thread receives one of them. The checker
12//! finds both outcomes and nothing else. `explore` builds the system afresh (once here,
13//! once per worker in a parallel run) and reports every outcome to the observer.
14//!
15//! ```
16//! use must::event::Model;
17//! use must::{explore, Config, CountingObserver, Ctx, System};
18//!
19//! let counter = CountingObserver::new();
20//! explore(
21//!     || {
22//!         let mut sys = System::new();
23//!         sys.add(|c: Ctx| async move { c.send(2, "ping", Model::P2p); });
24//!         sys.add(|c: Ctx| async move { c.send(2, "pong", Model::P2p); });
25//!         sys.add(|c: Ctx| async move {
26//!             let _msg = c.recv(|_| true).await;
27//!         });
28//!         sys
29//!     },
30//!     &counter,
31//!     Config::default(),
32//! );
33//! assert_eq!(counter.full(), 2); // reads "ping", or reads "pong"
34//! ```
35//!
36//! # Writing a process
37//!
38//! A process is an `async` block driven by a [`Ctx`]. It reads like ordinary code; the
39//! checker replays it under every consistent message ordering.
40//!
41//! - [`Ctx::send`] delivers a message under a chosen communication [`Model`].
42//! - [`Ctx::recv`] blocks for a matching message; [`Ctx::recv_timeout`] may instead
43//!   return `None`, modelling a timeout.
44//! - [`Ctx::nondet`] explores every value of a finite set (data non-determinism).
45//! - [`Ctx::assert_that`] reports a safety violation.
46//!
47//! Assertion failures, deadlocks, and non-terminating processes each surface as a
48//! distinct terminal outcome, reported to the observer.
49//!
50//! # How it works
51//!
52//! Every execution is an *execution graph*: events ordered per thread by program order
53//! (`po`), plus a reads-from relation (`rf`) linking each receive to the send it read
54//! (or to nothing, for a timeout). A communication model decides which graphs are
55//! *consistent*, i.e. which delivery orders are allowed. [`explore`] enumerates each
56//! consistent graph once, notifying an observer at every outcome.
57//!
58//! # Modules
59//!
60//! - [`event`]: events, labels, and the communication [`Model`].
61//! - [`graph`]: the execution graph and its queries.
62//! - [`consistency`]: well-formedness and the per-model consistency predicates.
63//! - [`runtime`]: the [`System`]/[`Ctx`] API that turns `async` processes into a
64//!   [`Program`].
65//! - [`scheduler`]: the scheduling policy the explorer follows.
66//! - [`explorer`]: the exploration itself, [`explore`].
67//! - [`observer`] / [`render`]: inspecting and displaying a run.
68//! - [`viz`]: dumping a run as a JSON trace.
69
70pub mod consistency;
71pub mod event;
72pub mod explorer;
73pub mod graph;
74pub mod intern;
75pub mod observer;
76pub mod program;
77pub mod render;
78pub mod runtime;
79pub mod scheduler;
80pub mod viz;
81
82pub use consistency::{
83    consistent, consistent_asyn, consistent_cd, consistent_mbox, consistent_p2p, well_formed,
84};
85pub use event::{Event, EventId, Label, Model, Pred, Tid, Val};
86pub use explorer::{explore, Config, Execution, ExecutionKind};
87pub use graph::ExecutionGraph;
88pub use observer::{
89    CountingObserver, ExecutionCollector, NullObserver, Observer, RecordingObserver, Step, StepKind,
90};
91pub use program::{Program, ThreadNext};
92pub use runtime::{Ctx, NondetFuture, RecvFuture, RecvTimeoutFuture, System, DEFAULT_MAX_EVENTS};
93pub use scheduler::{next_step, traces_of, NextStep};
94pub use viz::{Summary as TraceSummary, TraceObserver};
must/lib.rs

must/
lib.rs
