cmc(7)

the libcmc model: programs, worlds, the environment and its rules

---
CMC(7) Miscellaneous Information Manual CMC(7)

cmc — the libcmc model: programs, worlds, the environment and its rules

libcmc is an explicit-state model checker for protocol code written in C. It checks the program you ship: each node is that program, run unmodified as a process, and the checker is the network, the clock and the crash between them. It explores every interleaving of connections, messages, timeouts, crashes and lost messages, up to a bound, and checks invariants in every state it reaches. A model file says which program, which environment and which invariants; it carries no behaviour.

The engine has a second front end, in-process step functions (CmcCore), which is how it is calibrated against TLC; that model is described from Cores and worlds on. cmc(1) gives the command line, and libcmc(3) the C interface.

cmc --model-file starts one process per node, the same program each time, with the node number as its first argument. Each runs under seccomp user notification and under cmc-preload.so, which gives it a heap at fixed addresses and routes the clock and () to the checker. The checker answers every (), (), (), (), accept(), (), () and close() on a connection itself: no real socket forms. Node i listens on 127.0.0.1 port 20000 + i, and a connection goes to the node whose port was dialled.

A node that calls () or reads a connection with nothing the search has chosen to deliver stays blocked in the kernel. When every node is blocked or has exited the world is : the checker reads each node's state, checks the invariants, and the enabled actions are the next steps:

ACCEPT
A node in accept() takes a connection waiting at it.
DELIVER
A node reading a connection gets the oldest message on it; each connection is FIFO, as TCP is.
EOF
The peer is gone and the connection is drained: the read returns 0.
TIMEOUT
Timeout budget is left: a node waiting for input has its timer fire. A node reading a connection gets the one byte ‘T’ instead of a message; a node idle in accept() accepts a synthetic timer connection and reads ‘T’ from it. Either way the logical clock advances one second. This is how a server that waits for a request, or for a peer to connect, detects that it has waited long enough -- an election timeout.
CRASH
Crash budget is left: a live node dies.
DROP
Drop budget is left: the oldest message on a connection is lost.

A node's state is what it reports. After each change it writes a canonical encoding of its logical state, a length byte then the bytes, to file descriptor 3; what it has made durable it writes the same way to descriptor 193. A crash keeps only the durable encoding. The encoding must be canonical (the same logical state, the same bytes) and complete (everything the node's future depends on, its position in its own code included); anything left out lets the checker merge two states that differ, and miss a bug.

The world is every node's state, liveness and what it is blocked in, its open connections, every connection's messages in order, the connections waiting to be accepted, the ghost log of client replies, the budgets left and the logical clock. Its 128-bit fingerprint dedups states. The search is stateless: to expand a world the checker starts every node again and replays the actions that reached it. Breadth-first search gives a shortest counterexample; simulation takes seeded random walks and is never a pass.

A is a vtable over a fixed-size, pointer-free state per node. The engine treats that state as opaque bytes. A is every node's state followed by the environment the engine owns:

node states
The first durable_size bytes of each are durable.
header
Remaining budgets; per node, the clients left, armed timers, pending wakes, pending persists and pending connection resets.
network
The messages in flight.
persists
Each node's pending disk writes, oldest first.
replies
The ghost log of client replies, in emission order.

Every part is kept canonical, so two worlds are the same state exactly when their bytes are equal. The engine hashes the bytes into a 128-bit fingerprint and stores the fingerprints of the states it has seen.

In a message-passing core, an action becomes possible only through something a core emitted, or through an environment budget. The engine never reads a core's state to decide what can happen next:

DELIVER
A message is in flight (FIFO: only the head of its channel).
DROP
Drop budget is left. In FIFO mode a drop resets the connection.
DUP
Dup budget is left; bag mode only.
FIRE(n, t)
Node n armed timer t and has not cancelled it.
FLUSH(n)
Node n has a pending persist; the oldest completes first.
WAKE(n, w)
Node n emitted a wake of waiter w.
CLIENT(n)
Node n has client budget left.
CRASH(n, j)
Crash budget is left; the first j of the node's pending persists reach disk.
RESET(n, p)
A crash or a drop left node n a pending reset of its connection to p.

An action is one call to the node's () with the matching event. The engine then queues the sends, arms or cancels the timers, queues the persists and wakes, and appends the replies.

This rule is what separates libcmc from a simulator that consults the system under test: an oracle that reads a core's state to schedule it can hide exactly the bugs, such as lost wake-ups, that the check exists to find. Properties may read core state; the code that computes possible actions never calls them.

The engine owns the durable bytes. On FLUSH it applies the oldest pending record through the core's (), then delivers CMC_EV_FLUSHED to step(). step() must leave the durable bytes unchanged on every event; the engine compares them before and after each call.

CRASH(n, j) applies the first j pending records, zeroes the volatile bytes, the timers, the wakes and the remaining persists, empties every channel to and from n, marks a reset pending at each peer, and delivers CMC_EV_RESTART. Branching over j covers a write that reached disk before its completion was observed.

fifo
The default: one ordered channel per pair of nodes, as with TCP. It never duplicates.
bag
An unordered multiset that may duplicate, for transports without order. It allows more behaviour than FIFO, so a counterexample found in bag mode may be spurious for a protocol that relies on FIFO order.

Breadth-first search, the default, has the semantics of TLC run with one worker: a shortest counterexample, a depth that counts the initial state as 1, and exact counts of distinct and generated states. Depth-first search stops at a depth bound and reports a search that hit it as incomplete. Simulation runs seeded random walks. Replay runs a saved counterexample through the real cores.

A TLA+ specification of shared registers has no messages. A core that ports one sets (): the world is then one state, and the possible actions are the specification's disjuncts, applied through CMC_EV_ACTION. Only calibration cores do this. The engine is calibrated this way against TLC on 22 configurations of a published consensus specification, and must give the same verdicts, counterexample depths and distinct-state counts.

These are the rules that keep a pass meaningful. A change to the engine that breaks one is a bug, whatever else it improves. For the process front end they read: actions come only from what the programs did (dialled, wrote, blocked) and from budgets; the world holds everything the future depends on; a crash keeps only what a node declared durable; a bound, a cap, an unknown model-file key, a missing preload or a node silent in a call the checker does not model is an error or an incomplete search, never a pass.

  1. No omniscient oracle. Actions are enabled only by what a core emitted or by a budget.
  2. The world is the state. Everything that affects future behaviour lives in the world bytes, kept canonical, and nothing else does: not padding, not uninitialised bytes, not a global in the core.
  3. The engine owns durability. Only apply_persist() changes durable bytes, and a crash may keep any prefix of the pending persists.
  4. Limits are errors. Going past a cap is reported as a violation, never truncated.
  5. TLC semantics. Breadth-first search gives shortest counterexamples and exact counts, and the calibration rows match TLC.

Runs every step twice from copies of the same state and compares the outputs and the next states: a non-deterministic core fails.
purity gate
scripts/purity_gate.sh inspects a core's object files and sources: no calls but (), no writable or thread-local data, no clock, randomness, system-call or CPU-identification instructions, no ‘asm’, and no direct writes to out->o. scripts/purity_teeth.sh checks that the gate rejects a probe for each of these.
MemorySanitizer
Uninitialised reads, which --det cannot see.
planted bugs
Each ‘#if’ bug site in a core's shipped source must be caught, with the expected property, by search, by simulation and by replay.
calibration
The engine itself, against TLC.

Process front end: Linux x86-64; at most 8 nodes, 64 bytes per write, 128 messages in flight, 16 connections per node, 64 client replies, 64 bytes of reported state per node, and 255 for each budget. A target must be built -no-pie, use the port convention, and do its I/O through the calls above; a node that blocks in anything else for 10 seconds is an error. A read gets at most one write, a connect never fails, and () does not notify the peer.

In-process cores: at most 8 nodes, 32 bytes per message or persist record, 16 effects per step, 2048 possible actions per state, 16 timers and 8 waiters per node, 256 bytes of core settings, and 255 for each budget and cap.

cmc(1), libcmc(3)

docs/DESIGN.md and docs/WHY.md in the source tree, and the guide at https://gregburd.codeberg.page/libcmc/

libcmc was first released on November 3, 2026, with in-process cores only; the process front end followed. Its design follows CMC (Musuvathi et al., OSDI 2002) and Stateright, and takes bounded liveness from MaceMC.

Greg Burd <greg@burd.me>

November 5, 2026 Debian

mdoc source: man/man7/cmc.7