Awesome Reviewers

Verification · Formal

Concurrency model checking

Explores thread interleavings systematically to find races and orderings that fail only rarely.

Sub-techniques

  • Exhaustive interleaving V1029.001

    Enumerate all interleavings of a small test (loom).

  • Randomized scheduling V1029.002

    Sample schedules with a controlled scheduler (shuttle).

How to build it

  1. Isolate the concurrent primitive behind an interface the checker can swap.
  2. Write small tests with two or three threads.
  3. Run them in a dedicated CI job with the checker's cfg flag.

Signals in a repository

  • --cfg loom in RUSTFLAGS or loom::model in tests.
  • ThreadSanitizer builds in CI.