cmc(1)

explicit-state model checker for C protocol cores

---
CMC(1) General Commands Manual CMC(1)

cmc — explicit-state model checker for C protocol cores

cmc --model name [--tlc-cfg file | --cfg key=value[,...]] [--inv name[,...]] [--prop name[,...]] [--all-props] [--bfs | --dfs depth | --simulate] [--seed n] [--walks k] [--depth d] [--det] [--max-states n] [--time seconds] [--trace-out file] [--progress seconds] [--quiet] [--coverage] [--clients n] [--drops n] [--dups n] [--crashes n] [--net-cap n] [--persist-cap n] [--reply-cap n] [--net fifo | bag] [--live-steps k]

cmc --replay file [--inv names | --all-props]

cmc --model name --list

cmc --version

cmc explores every interleaving of a set of protocol nodes, the network between them, their timers, their disk writes and their crashes, up to the budgets given on the command line, and checks the named properties in every state it reaches. The nodes run the C step functions that the product itself links; see cmc(7) for the model and libcmc(3) for the interface a core implements.

There is no single cmc binary. A program that uses libcmc writes a () that passes its table of models to (), and links against libcmc.a; that program is its cmc. The binary built by this repository, build/cmc, carries the models hc (the calibration core), toy, and toy-bug1 to toy-bug3.

Output follows the wording of TLC, the TLA+ model checker, so the two can be compared line by line. Depth counts the initial state as 1.

name
The model to check, by its name in the program's model table. Required, except with --replay.
key=value[,...]
Core settings, passed to the core's (). May be given more than once; later settings override earlier ones, including those read by --tlc-cfg.
file
Read a TLC .cfg file: its become core settings, and its and become the properties to check.
name[,..., --prop name[,...]]
Check these properties. The two options are synonyms; each property's kind comes from the model.
Check every property of the model.
Print the model's property names and exit.
Print the libcmc version and exit.

A model may mark its first properties as always checked. At least one property must be named, or --all-props given.

Breadth-first search, the default. It finds a shortest counterexample, and its state counts are exact.
depth
Depth-first search to depth states. A search that reaches the bound without finishing is reported as incomplete, never as a pass.
Seeded random walks, not exhaustive. Walk i uses seed n+i; a violation is reported with the --seed and --walks 1 that reproduce it.
n
First seed for --simulate. Default 0.
k
Number of walks for --simulate. Default 1000.
d
Length of each walk, in states. Default 100.
file
Run a replay file written by --trace-out through the real cores, printing each state. The model, settings and budgets are taken from the file; an option on the command line that conflicts with the file is refused.
Determinism gate: run every step twice from copies of the same state and fail if the two runs differ in their outputs or their next state.
n
Stop after n distinct states.
seconds
Stop after seconds of wall time.

These options apply to message-passing cores (actor mode). Each budget is a count over the whole run, from 0 to 255.

n
Client requests each node may receive. Default 1.
n
Messages the network may lose. With --net fifo, a drop resets the connection and both ends are told. Default 0.
n
Messages the network may duplicate. Needs --net bag. Default 0.
n
Crashes, of any node. A crash keeps any prefix of the node's pending disk writes, loses the rest and the volatile state, resets its connections and restarts it. Default 0.
n
Messages in flight at once. Default 8.
n
Pending disk writes per node. Default 2.
n
Client replies recorded in the ghost log. Default 8.
fifo |
, the default, has one ordered channel per pair of nodes, as TCP does, and never duplicates. bag is an unordered multiset that may duplicate.
k
Bound, in steps of the fair schedule, for eventually-properties. Default 1000.

Going past a cap is reported as an engine error, never silently truncated.

file
On a violation, write the counterexample as a replay file.
seconds
Print a progress line every seconds during breadth-first search; 0 turns it off. Default 60.
Do not print the counterexample.
Print, for each action kind, the states it generated and the new distinct states it found.

*.replay
Replay files. A header names the model, settings and budgets; each following ‘act’ line is one action in hexadecimal, with its description as a comment.

0
No property was violated, and the search was complete for its mode: breadth-first or depth-first search finished, the walks ran, or the replay ended.
1
A property was violated, an engine rule was broken (determinism, durability, a cap), or a witness was never reached.
2
Incomplete: a state, time or depth limit stopped the search before it finished, with no violation found.
3
Usage error, a bad setting, or a replay file that cannot be run.

Check every property of the toy lock server:

$ build/cmc --model toy --all-props
...
Model checking completed. No error has been found.
...
49 states generated, 34 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 11.

Find the planted bug in toy-bug1, save the counterexample, and replay it:

$ build/cmc --model toy-bug1 --inv Mutex --trace-out bug1.replay
Error: Invariant Mutex is violated.
  2 clients in the critical section
...
$ build/cmc --replay bug1.replay --inv Mutex

Check a calibration configuration against its TLC result:

$ build/cmc --model hc \
    --tlc-cfg calib/hc/cfg/hc_paper_cp_n3_s1.cfg --det

Search a large space by random walks first:

$ ./mycmc --model mymodel --all-props --crashes 1 --drops 1 \
    --simulate --seed 7 --walks 100000 --depth 60

libcmc(3), cmc(7)

The guide and design notes: https://gregburd.codeberg.page/libcmc/

Greg Burd <greg@burd.me>

A pass covers only the budgets given. Raise --clients, --drops and --crashes until the bugs you planted are caught, and treat a run stopped by --max-states or --time as "no violation found in N states".

--net bag allows behaviour a FIFO transport never shows, so a counterexample found in bag mode may be spurious for a protocol that relies on FIFO order.

November 3, 2026 Debian

mdoc source: man/man1/cmc.1