git:20261018.d554b10 to git:20261018.662aa2d
31 added, 10 removed. Audit A to A.
# statem_parallel
## Purpose
Parallel model-based testing on `statem` and qcheck: does a concurrent system
behave like its sequential model when several callers use it at once? A
`Spec` describes the model and the system; `check` generates a `Case` (a
sequential prefix and two or three branches), runs the branches at the same
moment, and asks `statem/linearize` whether the histories have an order the
model agrees with. A failure is shrunk to a small case and reported with the
failing history and where the search for an order got stuck. Testing library:
consumers take it as a dev dependency. BEAM-only (`gleam_erlang`,
`gleam_otp`, `weft`), so it is deliberately NOT in `lint/policy.
portable_packages`; the pure checker lives in `packages/statem` for that
reason.
## Key types
- `Spec(model, cmd, sut, response)`: `initial`, `command`, `precondition`
(`statem.Admission`), pure `next_model`, `new_sut`, `run(sut, cmd) ->
response`, `postcondition(model, cmd, response) -> Result(Nil,
- statem.Violation)`, `teardown`. `run` is called from several processes at
- once and must be safe for that; `sut` is a shared handle (subject, pid
- client), never a value. `new_sut`, `run`, `postcondition`, `next_model`
- and `teardown` are rescued: a crash is a `statem.crash` violation
- (teardown's is dropped), so teardown runs on every path.
+ statem.Violation)`, `finish(sut) -> Result(Nil, statem.Violation)`,
+ `teardown`. `run` is called from several processes at once and must be
+ safe for that; `sut` is a shared handle (subject, pid client), never a
+ value. `finish` runs once per execution, on the test process, only after
+ a race judged linearizable and before teardown (never after a prefix
+ failure, crash, timeout or non-linearizable verdict); it is where
+ end-state invariants live (an audit read-back, a quiet pool). `new_sut`,
+ `run`, `postcondition`, `next_model`, `finish` and `teardown` are
+ rescued: a crash is a `statem.crash` violation (teardown's is dropped),
+ so teardown runs on every path.
- `Case(cmd)(prefix, branches)`.
- `Config` via `default_config(seed:)` and `with_*`: `test_count` (100),
`branches` (2, clamped 2..3), `max_prefix` (6), `max_branch` (4, clamped
1..6), `max_shrinks` (500), `shrink_retries` (10), `repeat` (3),
`shrink_stop`, `deadline` (10 s, the parallel phase only), `search_budget`
(checker nodes, 100_000). No random default seed.
- `Failure(cmd, response)`: seed, run, violation, original and shrunk
`Case`, `Evidence` (`InPrefix(step)`, `Raced(histories, explanation)`,
- `Unrecorded`), shrinks accepted, executions, `statem.ShrinkEnd`.
+ `AfterRace(histories)` for a `finish` failure, `Unrecorded`, `NoRace`),
+ shrinks accepted, executions, `statem.ShrinkEnd`.
- `check`, `check_run`, `generate_case` (a case from `(seed, run)` alone),
`report(failure, describe)`.
- Violation tags: the spec's own for a prefix failure; fixed ones for the
- rest, so a shrink stays on the failure it found: `statem.not_linearizable`,
- `statem.undecided`, `statem.timeout`, `statem.crash`.
+ Violation tags: the spec's own for a prefix or `finish` failure; fixed ones
+ for the rest, so a shrink stays on the failure it found:
+ `statem.not_linearizable`, `statem.undecided`, `statem.timeout`,
+ `statem.crash`, `statem.no_race`. All race failures share
+ `statem.not_linearizable`, so a shrink can move from one concurrency bug to
+ another (a lost update to an underflow); the shrunk case is still a real
+ failure, not necessarily the original bug.
## How it works
Run `i` takes the same per-run seed as `statem` (`statem.run_seed`). The
prefix is drawn with `statem.grow`; each branch is drawn from the model after
the prefix, as if alone. A case is admissible only if every command's
precondition holds in every interleaving of the branches
(`internal/interleave` enumerates them while there are at most 10_000;
past that the longest branch is trimmed). An inadmissible draw, or one that
left fewer than two branches, is redrawn up to eight times, then trimmed
- command by command, so generation always ends with an admissible case.
+ command by command, so generation always ends with an admissible case. A
+ case that ends with fewer than two non-empty branches races nothing: the run
+ fails at once, unexecuted and unshrunk, as `statem.no_race` with `NoRace`
+ evidence, so preconditions that admit no concurrent pair are reported
+ instead of passing green.
An execution builds one system, runs the prefix call by call checking each
response against the model (a prefix failure races nothing), then
`internal/runner.race`: one weft task per branch, `limit` set to the branch
count (weft's default is the scheduler count, and a barrier between more
branches than slots deadlocks), each task parks on a go subject until the
coordinator has all of them, then calls in order reading weft's monotonic
clock (milliseconds) around each call. The weft deadline kills and joins
what has not finished; an unfinished branch is `statem.timeout`, a crash
outranks it. The prefix is NOT deadline-bounded. The histories go to
`linearize.check` with the post-prefix model.
The seed fixes the case, never the interleaving. `repeat` runs a generated
case several times before it counts as passing; `shrink_retries` accepts a
candidate if any attempt fails with the original tag (`statem.first_failure`).
Shrink candidates, in order: drop a branch (while more than two), merge two
branches, delete one command from a branch, delete from the prefix, move a
branch's first command to the end of the prefix. Each must be admissible.
+ A candidate may race fewer than two branches (only generation refuses
+ that, as `statem.no_race`): it is kept only while it still fails under the
+ original tag, so a prefix failure shrinks to the prefix alone.
+
+ After the race, a linearizable verdict hands the system to `finish`; its
+ violation keeps the spec's tag, its crash is `statem.crash` naming
+ `finish`, and its evidence is `AfterRace(histories)`.
## Invariants that break things
- `run` shared across processes: a `sut` that is a plain value is copied
into each branch process and nothing races.
- Millisecond instants: calls that fit in one millisecond are treated as
overlapping, which hides ordering constraints but cannot invent a failure.
- A racy bug may need `repeat` and `shrink_retries` above one; tests that
make a race near-certain (a two millisecond pause between a read and a
write) still keep both.
- A crash that kills the system's own linked process kills the test
process; crash `run`, not the actor, in tests.
- Not built, deliberately: symbolic result variables, coverage labels,
scheduler instrumentation beyond the start barrier, a deadline on the
prefix.