Linearization checking for parallel execution results.

When commands execute in parallel branches, the Linearization module verifies that the observed results can be explained by some sequential (linear) ordering of the commands.

What is Linearizability?

A parallel execution is linearizable if there exists a sequential ordering of the commands such that:

1. The ordering respects the happens-before relationship within each branch
2. Each command's observed events are consistent with what the model predicts for the state at that command's position in the ordering

If no such ordering exists, the system has exhibited non-linearizable behavior, which typically indicates a race condition or consistency bug.

Algorithm

Given branch execution results:

1. Generate interleavings (orderings that preserve intra-branch order)
2. For each interleaving, walk the commands in order, asking the model's simulator what events each command SHOULD produce given the model state at that point, and compare against the events the SUT actually produced for that command
3. Advance the model state with the OBSERVED events and, at that same position, run the model's synchronous (@trigger) assertions against the advanced state
4. Advance and continue
5. If any interleaving is fully consistent (events compatible AND all triggered assertions hold at every position), the execution is linearizable

Soundness invariant (why this module exists)

A concurrent/branching execution is a failure ONLY if NO single ordering of the branches can simultaneously (a) reproduce every command's observed events and (b) satisfy every triggered synchronous assertion at that command's position. The observed events and the model-state prediction an assertion runs against MUST come from the SAME candidate ordering.

This invariant is the antidote to a soundness bug that over-reported races: the executor used to run each branch's synchronous assertions against that branch's forked projection state. A fork is a partial view: it sees the prefix plus its own branch, never the concurrently-executing sibling branches' effects. So a read in one branch could observe a value written by a sibling's write (the real interleaving) while the reader's model state never recorded that write, firing a spurious assertion. Put k v ∥ Get k was flagged even though Put-then-Get is a perfectly legal serialization. The fix: the executor disables those unsound per-branch assertions, and assertion checking moves HERE, where it is evaluated against observed events and the model prediction drawn from one consistent ordering. check/5 therefore refutes an execution only when every ordering fails, and its refutation carries the specific assertion (when one is the cause) so the report is as precise as the old per-branch path was, without its false positives.

Verification strength

The check is exactly as strong as the model's simulator: predicted event fields that are nil, unresolved refs, or external markers are treated as wildcards, and commands the simulator does not predict (returns []) are unconstrained. A model without a simulator/0 cannot be verified at all; check/5 then returns {:indeterminate, 0} rather than fabricating a verdict.

Complexity

The number of interleavings grows multinomially with branch count/length (see linearization_count/1). check/5 examines at most :max_candidates interleavings (default 1000); if none is consistent but the candidate space was not exhausted, it returns {:indeterminate, checked} instead of claiming a race.

Usage

case Linearization.check(branches, branch_events, projections, model,
       start_index: 3) do
  {:ok, linearization} -> # consistent ordering found
  :no_linearization    -> # exhaustively refuted: race condition
  {:indeterminate, n}  -> # cannot verify (no simulator / cap reached)
end