AGENTS.md@packages/statem_parallel git:20261018.662aa2dA

Immutable. This exact content never changes and is served at /api/v1/blob/c2ea8dd98dfc29b8.

# 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)`, `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)`,
  `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 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. 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.