Decide whether a Lockstep.History is sequentially consistent
with respect to a Lockstep.Model.
Sequential consistency (Lamport, 1979) is weaker than linearizability: it requires a total order of operations such that
- Each process's ops appear in the order that process issued them (program order).
- The order is consistent with the model.
Crucially, the order does NOT have to respect real-time across processes. So an operation P1 finished and an operation P2 invoked after, can still appear with P2 before P1 in the legal order — as long as P1's process's own operations stay in their program order.
Useful for checking implementations that don't claim linearizability but do claim per-process ordering (some eventually-consistent registers, certain caching layers).
Returns the same shape as Lockstep.Checker.Linearizable.check/2.
Algorithm
Backtracking similar to the linearizability checker, but the "minimal" predicate is process-order-only: an op O is a valid next-pick iff there's no earlier-issued op (smaller invoke index) on the same process still pending.
Summary
Functions
Check events against model for sequential consistency. See
module doc for return shape.
Functions
@spec check([Lockstep.History.Event.t()], module()) :: {:ok, %{linearized_order: [Lockstep.Checker.Linearizable.Op.t()]}} | {:error, %{ reason: atom() | String.t(), remaining: [Lockstep.Checker.Linearizable.Op.t()] }}
Check events against model for sequential consistency. See
module doc for return shape.