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.

© 2024-2026 db7 — licensed under CC BY 4.0.