libcmc(3)

model-check C protocol cores

---
LIBCMC(3) Library Functions Manual LIBCMC(3)

libcmc, cmc_main, cmc_options_default, cmc_run_new, cmc_check, cmc_result_free, cmc_run_free, cmc_world_size, cmc_print_trace, cmc_write_replay, cmc_describe_action, cmc_out_push, cmc_cfg, cmc_nnodes, cmc_node, cmc_nreplies, cmc_reply, cmc_requests, cmc_why, cmc_world_init, cmc_enabled, cmc_apply, cmc_fingerprint — model-check C protocol cores

libcmc.a

#include <cmc.h>

int
cmc_main(int argc, char **argv, const CmcModelEntry *models, size_t nmodels);

void
cmc_options_default(CmcOptions *o);

CmcRun *
cmc_run_new(const CmcModel *m, const char *cfg, const char *const *props, const CmcOptions *o, char *err, size_t errlen);

void
cmc_check(CmcRun *r, CmcResult *res);

void
cmc_result_free(CmcResult *res);

void
cmc_run_free(CmcRun *r);

size_t
cmc_world_size(const CmcRun *r);

void
cmc_print_trace(CmcRun *r, const CmcAction *acts, int n, FILE *f);

int
cmc_write_replay(CmcRun *r, const char *path, const CmcAction *acts, int n);

void
cmc_describe_action(CmcRun *r, CmcAction a, FILE *f);

CmcOutput *
cmc_out_push(CmcOut *out, uint8_t kind);

CMC_INVARIANT(name, fn);

CMC_ACTION_PROPERTY(name, fn);

CMC_WITNESS_PROP(name, fn);

CMC_QUIESCENT_PROP(name, fn);

CMC_EVENTUALLY_PROP(name, fn);

const void *
cmc_cfg(const CmcWorld *w);

int
cmc_nnodes(const CmcWorld *w);

const void *
cmc_node(const CmcWorld *w, int node);

int
cmc_nreplies(const CmcWorld *w);

void
cmc_reply(const CmcWorld *w, int i, int *node, uint32_t *arg);

int
cmc_requests(const CmcWorld *w, int node);

void
cmc_why(CmcWhy *why, const char *fmt, ...);

Lower level

void
cmc_world_init(CmcRun *r, uint8_t *w);

int
cmc_enabled(CmcRun *r, const uint8_t *w, CmcAction *acts, int max);

int
cmc_apply(CmcRun *r, uint8_t *w, CmcAction a);

void
cmc_fingerprint(const uint8_t *p, size_t n, uint64_t fp[2]);

libcmc checks protocol logic written as pure C step functions. The product calls those functions to run the protocol; libcmc links the same object files and explores every order in which messages, timers, disk writes, client requests and crashes can reach them. cmc(7) describes the model, and cmc(1) the command line.

A program supplies three things:

  1. A CmcCore: the step code and the size of a node's state.
  2. A CmcModel: a core plus the properties to check against it.
  3. A () that calls cmc_main(), or that drives cmc_run_new() and cmc_check() itself.

typedef struct CmcCore {
	const char *name;
	size_t	state_size;	/* bytes per node */
	size_t	durable_size;	/* leading bytes that survive a crash */
	size_t	cfg_size;	/* at most 256 */
	void	(*cfg_default)(void *cfg);
	int	(*cfg_set)(void *cfg, const char *key, const char *val);
	int	(*nnodes)(const void *cfg);
	void	(*init)(const void *cfg, int node, void *state);
	void	(*step)(const void *cfg, int node, void *state,
		    const CmcEvent *ev, CmcOut *out);
	void	(*apply_persist)(const void *cfg, int node, void *durable,
		    const uint8_t *body, uint16_t len);
	void	(*describe)(const void *cfg, int node, const void *state,
		    FILE *f);			/* optional */
	void	(*describe_msg)(const void *cfg, const uint8_t *body,
		    FILE *f);			/* optional */
	int	(*direct_actions)(const void *cfg, const void *state,
		    CmcAction *acts, int max);	/* calibration only */
	void	(*describe_action)(const void *cfg, CmcAction a,
		    FILE *f);			/* calibration only */
	int	(*clients)(const void *cfg, int node);	/* optional */
} CmcCore;

A node's state is state_size bytes, fixed, with no pointers. The engine copies, compares and hashes it as bytes, so the core keeps it canonical: padding and unused slots zeroed, sets sorted.

() fills the core's settings; () applies one key=value and returns 0, or -1 to reject it. () returns the number of nodes, 1 to CMC_MAX_NODES (8). () sets a node's initial state.

() handles one event at one node. It must be total and deterministic, and may read only its arguments: no clock, randomness, globals, I/O or allocation. It changes the state in place and emits effects with cmc_out_push(). It must not change the first durable_size bytes; only (), which the engine calls when a persist reaches disk, may change them. A core with a non-zero durable_size must supply apply_persist().

(), if set, says which nodes take client requests; it reads the settings, never the state. () and () print states and message bodies in traces. () and () exist for calibration cores that port a shared-memory TLA+ specification (cmc(7)); a message-passing core leaves them NULL.

step() receives a CmcEvent:

typedef struct CmcEvent {
	uint8_t	kind;		/* CmcEventKind */
	uint8_t	src;		/* RECV, CONN_RESET: the peer */
	uint16_t len;		/* RECV, FLUSHED: bytes in body */
	uint32_t arg;		/* TIMER, WAKE: the id; CLIENT: request number */
	CmcAction action;	/* ACTION (calibration only) */
	const uint8_t *body;	/* RECV: the message; FLUSHED: the record */
} CmcEvent;

A message from src.
Timer arg fired.
The persist record in body is now durable.
Waiter arg was woken.
A client request, arg counting from 0 at this node.
The node crashed: its volatile bytes are zeroed and it is starting again.
The connection to src was reset, and the messages on it are gone.
Calibration cores only.

() appends an effect of the given kind to out, zeroes it and returns it for the core to fill in.

Send body (len bytes, at most CMC_MSG_MAX, 32) to dst.
Arm timer arg, 0 to 15.
Disarm timer arg.
Queue body as a disk write.
Queue a wake of waiter arg, 0 to 7.
Answer a client with arg. The engine appends the reply to the ghost log that properties read.

A core never writes out->o directly; the purity gate rejects source that does. Past CMC_OUT_MAX (16) effects in one step, () returns a scratch entry and the engine reports the overflow as a violation.

A property is a CmcProp, made with one of the macros below from a name and a function. State properties have the type

bool fn(const CmcWorld *w, CmcWhy *why);

and action properties

bool fn(const CmcWorld *pre, CmcAction a, const CmcWorld *post,
    CmcWhy *why);

()
Holds in every reachable state.
()
Holds on every transition, including those to states already seen.
()
Holds in some reachable state. A witness never reached fails the run: it means the other properties may hold only because the interesting states were never reached.
()
Holds in every state where nothing can happen, or where the only possible actions are timers that fire and change nothing.
()
Bounded liveness: from every reachable state, the fair schedule (no faults, no new clients) reaches a state where it holds within live_steps steps.

Each macro fills in a CmcProp whose kind is CMC_INV, CMC_ACTION_PROP, CMC_WITNESS, CMC_QUIESCENT or CMC_EVENTUALLY.

A property returns false to report a violation, and may explain it with (), which formats like printf(3).

Properties read the world through accessors. () returns node node's state and () the core's settings. () and () read the ghost log of client replies, in the order they were emitted. () returns the number of client requests delivered to a node, counted by the environment rather than by the core. Properties may read core state; the engine never calls them to decide which actions are possible.

CMC_VERSION is the release as a string, ‘MAJOR.MINOR.PATCH’, following semantic versioning. A change to <cmc.h> that breaks a core, a model or a caller written against an earlier release of the same major version is not made outside a major release; before 1.0.0, a minor release may make one, and CHANGELOG.md says so.

typedef struct CmcModel {
	const char *name;
	const CmcCore *core;
	const CmcProp *props;
	int	nprops;
	int	nalways;	/* the first nalways props are always checked */
} CmcModel;

typedef struct CmcModelEntry {
	const char *name;	/* the --model name */
	const CmcModel *m;
} CmcModelEntry;

A CmcAction is a 64-bit word. (kind, a, b, c, d) packs one; (), (), (), () and () unpack its kind (the top byte), three byte fields and a 32-bit field. An action property receives the action between its two worlds. In a message-passing core the kind is one of

a = destination, b = source, d = index of the message in the network.
The same fields; the message is lost.
The same fields; the message is duplicated.
a = node, b = timer.
a = node: its oldest pending persist completes.
a = node, b = waiter.
a = node.
a = node, b = how many pending persists reached disk.
a = node, b = the peer whose connection was reset.

A calibration core defines its own kinds.

typedef struct CmcOptions {
	CmcSearch search;	/* CMC_BFS, CMC_DFS, CMC_SIMULATE, CMC_REPLAY */
	int	max_depth;	/* DFS bound; simulation walk length */
	uint64_t seed;		/* simulation: first seed */
	uint64_t walks;		/* simulation: number of walks */
	uint64_t max_states;	/* 0: none; reaching it is incomplete */
	double	time_limit;	/* seconds; 0: none */
	bool	det;		/* determinism gate */
	bool	stop_on_witness; /* stop once every witness is reached */
	bool	quiet;		/* print no trace or progress */
	bool	coverage;	/* count states per action kind */
	int	progress_s;	/* progress line period; 0: off */
	const char *trace_out;	/* write a replay file on a violation */
	const char *replay_in;	/* CMC_REPLAY: the file */
	int	client_budget, drop_budget, dup_budget, crash_budget;
	int	net_cap, persist_cap, reply_cap;
	CmcNet	net;		/* CMC_NET_FIFO or CMC_NET_BAG */
	int	live_steps;	/* bound for eventually-properties */
	FILE	*out;		/* progress output; NULL: stdout */
} CmcOptions;

The fields are the options of cmc(1), which gives their defaults.

() parses the command line described in cmc(1), runs the check, prints TLC-style output, and returns the verdict, which the caller returns from main().

To drive the engine directly, fill a CmcOptions with (), change what is needed, and call () with the model, a settings string ‘key=value,...’ and a NULL-terminated list of property names, or NULL for all of them. On failure it returns NULL and writes the reason to err.

() runs the search and fills res. On a violation, res->prop names the property (‘cmc:engine’ for a broken engine rule), res->why explains it, and res->trace holds the res->trace_len - 1 actions from the initial state. () prints them state by state, and () saves them in the format --replay reads. () frees the trace; () frees the run.

() returns the bytes in one world: every node's state plus the environment. () prints one action.

Lower level

() writes the initial world into w, which holds cmc_world_size() bytes. () lists the actions possible in w and returns their number, or -1 if there are more than max. () applies one action in place. () is the 128-bit hash the visited-state table uses. These exist for the engine's own tests.

cmc_main() returns a CmcVerdict: CMC_PASS (0), CMC_VIOLATION (1), CMC_INCOMPLETE (2) or CMC_ERROR (3), the exit statuses listed in cmc(1).

cmc_run_new() returns NULL on a bad setting, an unknown property, a bound out of range, a durable part without apply_persist(), or a duplicating FIFO network. cmc_apply() returns 0, or -1 if the action is not possible or a core broke an engine rule. cmc_write_replay() returns 0, or -1 if the file cannot be written.

A complete model, with the core, two properties and main(), is in docs/_includes/snippets/quickstart.c in the source tree. The skeleton:

#include "cmc.h"

static const CmcCore my_core = {
	.name = "mine",
	.state_size = sizeof(MyState),
	.durable_size = offsetof(MyState, first_volatile),
	.cfg_default = my_cfg_default,
	.cfg_set = my_cfg_set,
	.nnodes = my_nnodes,
	.init = my_init,
	.step = my_step,
	.apply_persist = my_apply_persist,
};

static const CmcProp my_props[] = {
	CMC_INVARIANT(NoLostAck, no_lost_ack),
	CMC_WITNESS_PROP(Acked, acked),
};

static const CmcModel my_model = {
	.name = "mine", .core = &my_core,
	.props = my_props, .nprops = 2,
};

int
main(int argc, char **argv)
{
	static const CmcModelEntry models[] = {
		{"mine", &my_model},
	};

	return cmc_main(argc, argv, models, 1);
}

Build it against the library:

cc -std=c11 -Ilibcmc/include mine.c mine_core.o \
    libcmc/build/libcmc.a -o mycmc

8 nodes.
32 bytes per message or persist record.
16 effects per step.
2048 possible actions per state.
16 timers per node.
8 waiters per node.

Going past a limit is reported as a violation, never truncated.

cmc(1), cmc(7)

The library is C11 and uses only libc.

Greg Burd <greg@burd.me>

The library is single-threaded and has no symmetry reduction; the visited set and the search queue live in memory.

November 3, 2026 Debian

mdoc source: man/man3/libcmc.3