Tiny Model Checker

Systematic concurrency exploration in a few lines of Scheme.

This page collects a series of posts documenting the design and implementation of a tiny, executable model checker for concurrent programs. The goal is not performance or completeness, but clarity: each post builds a minimal, correct foundation for reasoning about concurrency.

Building a Tiny Model Checker

• Part 1 — A cooperative scheduler Enumerating interleavings with a minimal execution core.

• Part 2 — Shared state and safety properties Adding shared memory and checking real correctness conditions.

• Part 3 — Blocking and waiting Modeling busy-waiting, deadlock, and AWAIT.

• Part 4 — Sleep sets and partial-order reduction Reducing redundant executions and exploring behaviors instead of schedules.

Future posts may extend this checker with more advanced reduction techniques (such as TruSt), alternative semantics, or experimental features. Those will live alongside this series rather than replacing it.