Install and build
A C11 compiler, make and libc. Nothing else.
---Get the source
git clone https://codeberg.org/gregburd/libcmc.git
cd libcmc
The GitHub mirror, https://github.com/gburd/libcmc, has the same
history.
Build and test
make # build/libcmc.a, build/cmc, build/test_cmc
make check # about a minute
make check runs the engine tests, the toy core’s planted-bug gate,
the purity gate and its own teeth, the documentation gate, and the
calibration rows against TLC that finish in about 30 seconds. It
should end with:
check-calibration: every row matches TLC
gcc and clang must both build the tree with -Wall -Wextra -Werror:
make CC=clang check
The longer gates:
| target | what | time |
|---|---|---|
make check-msan |
the engine tests under clang’s MemorySanitizer | 10 s |
make check-calibration |
all 22 calibration rows against TLC; about 7 GB of RAM | 8 min |
make check-hc-bugs |
planted bugs in the calibration core must break calibration | 30 s |
make check-all |
all of the above | 10 min |
The times are from a 48-core Xeon; every gate is single-threaded.
Build output goes to build/, and logs and replay files to
$CMC_SCRATCH (default ~/tmp/cmc-build).
Install
make install PREFIX=/usr/local
This installs lib/libcmc.a, include/cmc.h, and the man pages
cmc(1), libcmc(3) and cmc(7). DESTDIR works as usual.
With Nix
The repository is a flake:
nix build # result/lib/libcmc.a, result/include/cmc.h, man pages
nix flake check # builds, then runs make check (gcc and clang)
nix develop # gcc, clang, mandoc, ruby for the docs site
Try it
The cmc binary built here carries the toy lock server, three copies
of it with planted bugs, and the calibration core.
build/cmc --model toy --all-props
build/cmc --model toy-bug1 --inv Mutex
The first passes, with 34 distinct states. The second prints the six events after which two clients hold the lock at once. The next page builds a model from nothing.