Your first model

A write that must survive a crash, a planted bug, and the counterexample libcmc prints for it.

---
  1. The state
  2. The step function
  3. The core
  4. The properties
  5. main()
  6. Run it
  7. Plant the bug
  8. What to take from this

This page builds a complete model in one C file: a client writes a value to a server, the server makes it durable and then acknowledges it, and the property is that a write the client saw acknowledged survives a crash. Then it plants the classic bug, acknowledging before the write is durable, and shows libcmc finding it.

Every code block here is a region of docs/_includes/snippets/quickstart.c. make check builds that file and checks that it behaves as this page says.

The state

A node’s state is a fixed-size struct of plain bytes, with no pointers. The engine copies, compares and hashes it as bytes, so unused fields must stay zero. Both nodes use the same layout; the first durable_size bytes are what survives a crash.


enum
{
	SERVER = 0, CLIENT = 1		/* node numbers */
};
enum
{
	M_WRITE = 1, M_ACK			/* message kinds, body[0] */
};

/* Every node has this layout.  The first byte is durable. */
typedef struct QsState
{
	uint8_t		value;			/* durable: the server's stored value */
	uint8_t		restarted;		/* the server has come back from a crash */
	uint8_t		writer;			/* whom to acknowledge once the write is durable */
	uint8_t		pad;
} QsState;

Tested source: docs/_includes/snippets/quickstart.c

The step function

step() handles one event at one node. It reads only its arguments: no clock, no randomness, no globals, no I/O. It changes the state in place and emits effects through cmc_out_push().

The client sends a write when it gets a client request, and reports the acknowledgement as a reply. The server asks for its write to be made durable (CMC_OUT_PERSIST) and acknowledges when the engine tells it the write reached disk (CMC_EV_FLUSHED).


static void
qs_send(CmcOut *out, int dst, uint8_t kind, uint8_t val)
{
	CmcOutput  *o = cmc_out_push(out, CMC_OUT_SEND);

	o->dst = (uint8_t) dst;
	o->len = 2;
	o->body[0] = kind;
	o->body[1] = val;
}

static void
qs_step(const void *cfg, int node, void *sv, const CmcEvent *ev, CmcOut *out)
{
	QsState    *s = sv;

	(void) cfg;
	if (node == CLIENT)
	{
		if (ev->kind == CMC_EV_CLIENT)
			qs_send(out, SERVER, M_WRITE, 1);
		else if (ev->kind == CMC_EV_RECV && ev->body[0] == M_ACK)
			cmc_out_push(out, CMC_OUT_REPLY)->arg = ev->body[1];
		return;
	}
	switch (ev->kind)
	{
		case CMC_EV_RECV:
			if (ev->body[0] == M_WRITE)
			{
				CmcOutput  *p = cmc_out_push(out, CMC_OUT_PERSIST);

				p->len = 1;
				p->body[0] = ev->body[1];
				s->writer = ev->src;
#ifdef QUICKSTART_BUG
				qs_send(out, ev->src, M_ACK, ev->body[1]);	/* not durable yet */
#endif
			}
			break;
		case CMC_EV_FLUSHED:
#ifndef QUICKSTART_BUG
			qs_send(out, s->writer, M_ACK, ev->body[0]);
#endif
			break;
		case CMC_EV_RESTART:
			s->restarted = 1;
			break;
		default:
			break;
	}
}

/* The engine calls this when a persist reaches disk: only it may change
 * the durable byte. */
static void
qs_apply_persist(const void *cfg, int node, void *durable, const uint8_t *body,
				 uint16_t len)
{
	(void) cfg;
	(void) node;
	(void) len;
	((QsState *) durable)->value = body[0];
}

Tested source: docs/_includes/snippets/quickstart.c

step() never writes the durable byte itself. The engine owns the durable part of the state: when a persist completes it calls apply_persist(), and it checks after every step that the durable bytes did not change. That is what lets it model a crash honestly: the volatile bytes are lost, and of the persists still pending, any prefix may have reached disk.

The core

The vtable ties it together. The engine calls cfg_set for each --cfg key=value; this core has no settings. clients says which nodes take client requests.


static void
qs_cfg_default(void *cfg)
{
	(void) cfg;
}

static int
qs_cfg_set(void *cfg, const char *key, const char *val)
{
	(void) cfg;
	(void) key;
	(void) val;
	return -1;					/* this core has no settings */
}

static int
qs_nnodes(const void *cfg)
{
	(void) cfg;
	return 2;
}

static void
qs_init(const void *cfg, int node, void *sv)
{
	(void) cfg;
	(void) node;
	memset(sv, 0, sizeof(QsState));
}

static int
qs_clients(const void *cfg, int node)
{
	(void) cfg;
	return node == CLIENT;		/* only the client takes CLIENT events */
}

static void
qs_describe(const void *cfg, int node, const void *sv, FILE *f)
{
	const QsState *s = sv;

	(void) cfg;
	if (node == SERVER)
		fprintf(f, "server value=%u restarted=%u", s->value, s->restarted);
	else
		fprintf(f, "client");
}

static void
qs_describe_msg(const void *cfg, const uint8_t *body, FILE *f)
{
	(void) cfg;
	fprintf(f, "%s(%u)", body[0] == M_WRITE ? "WRITE" : "ACK", body[1]);
}

static const CmcCore qs_core = {
	.name = "quickstart",
	.state_size = sizeof(QsState),
	.durable_size = 1,
	.cfg_default = qs_cfg_default,
	.cfg_set = qs_cfg_set,
	.nnodes = qs_nnodes,
	.init = qs_init,
	.step = qs_step,
	.apply_persist = qs_apply_persist,
	.describe = qs_describe,
	.describe_msg = qs_describe_msg,
	.clients = qs_clients,
};

Tested source: docs/_includes/snippets/quickstart.c

The properties

A property reads the world through accessors: cmc_node() for a node’s state, cmc_nreplies() and cmc_reply() for the ghost log of replies sent to clients.


/* After a restart, every acknowledged write is still on the server's disk. */
static bool
no_lost_ack(const CmcWorld *w, CmcWhy *why)
{
	const QsState *s = cmc_node(w, SERVER);

	for (int i = 0; i < cmc_nreplies(w); i++)
	{
		int			who;
		uint32_t	v;

		cmc_reply(w, i, &who, &v);
		if (s->restarted && s->value != v)
		{
			cmc_why(why, "write %u was acknowledged, but the server restarted with value %u",
					v, s->value);
			return false;
		}
	}
	return true;
}

/* Some run gets a write acknowledged at all (else NoLostAck holds vacuously). */
static bool
acked(const CmcWorld *w, CmcWhy *why)
{
	(void) why;
	return cmc_nreplies(w) > 0;
}

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

static const CmcModel qs_model = {
	.name = "quickstart",
	.core = &qs_core,
	.props = qs_props,
	.nprops = sizeof(qs_props) / sizeof(qs_props[0]),
};

Tested source: docs/_includes/snippets/quickstart.c

Acked is a witness: some reachable state must satisfy it. Without it, a model in which the client never gets an acknowledgement would pass NoLostAck trivially, and so would a model whose budgets are too small to reach the interesting states.

main() 


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

	return cmc_main(argc, argv, models, sizeof(models) / sizeof(models[0]));
}

Tested source: docs/_includes/snippets/quickstart.c

cmc_main() is the whole cmc(1) command line. Your program carries your models and is your checker.

Run it 

cc -std=c11 -Iinclude docs/_includes/snippets/quickstart.c \
    build/libcmc.a -o quickstart
./quickstart --model quickstart --all-props --crashes 1

cmc: model quickstart, cfg "", breadth-first search, world 488 bytes
Model checking completed. No error has been found.
  Estimated probability of a 128-bit fingerprint collision (n^2/2^129): 1.32e-36
Witness Acked: reached
  Acked first reached at depth 5
37 states generated, 30 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 7.
Finished in 0.00s

libcmc tried every order of the client request, the two messages, the disk write and one crash of either node, and found no state that breaks NoLostAck. The exit status is 0.

Plant the bug

Built with -DQUICKSTART_BUG, the server acknowledges as soon as it asks for the write, before the write is durable. Without a crash, nothing goes wrong:

cc -std=c11 -DQUICKSTART_BUG -Iinclude docs/_includes/snippets/quickstart.c \
    build/libcmc.a -o quickstart-bug
./quickstart-bug --model quickstart --all-props

Model checking completed. No error has been found.

Allow one crash, and libcmc finds it:

./quickstart-bug --model quickstart --all-props --crashes 1 --trace-out bug.replay

Error: Invariant NoLostAck is violated.
  write 1 was acknowledged, but the server restarted with value 0
Error: The behavior up to this point is:
State 1: <Initial predicate>
  node 0: server value=0 restarted=0
  node 1: client
  net:
  ...
State 2: <CLIENT node 1>
  node 0: server value=0 restarted=0
  node 1: client
  net: [1->0 x1 WRITE(1)]
  ...
State 3: <DELIVER 1->0 #0>
  node 0: server value=0 restarted=0
  node 1: client
  net: [0->1 x1 ACK(1)]
  env: ... | n0 ... persists=1 ...
State 4: <DELIVER 0->1 #0>
  ...
  replies: (n1,1)

State 5: <CRASH node 0>
  node 0: server value=0 restarted=1
  ...
  replies: (n1,1)
Replay file written to bug.replay (4 actions).

Four events: the client asks, the server receives the write and acknowledges it with the persist still pending, the client gets the acknowledgement, and the server crashes before the persist completes. Breadth-first search finds the shortest such sequence. The exit status is 1.

The replay file runs the same four events through the real step code, printing every state:

./quickstart-bug --replay bug.replay --all-props

Simulation finds it too, and prints the seed that reproduces it:

./quickstart-bug --model quickstart --all-props --crashes 1 --simulate --walks 1000

What to take from this

  • The bug needs a crash to show. A pass means “no violation within these budgets”; raise --crashes, --drops and --clients until your planted bugs are caught.
  • The witness guards against passing for the wrong reason.
  • The planted bug lives in the shipped source behind #ifdef. Your gate builds each variant and requires each one to be caught. That is the subject of the next page.