Lockstep.Checker.Linearizable (Lockstep v0.1.0)

Copy Markdown View Source

Decide whether a Lockstep.History is linearizable with respect to a given Lockstep.Model.

A history is linearizable iff there exists a total order of its operations such that:

  1. The order respects real-time: if op A's :ok/:fail/:info happens before op B's :invoke, then A precedes B.
  2. Each operation is consistent with the model when applied in that order.

Pending ops (an :invoke with no matching completion) are ignored — equivalent to assuming they didn't apply. (:info completions are similarly treated as no-apply by default. A more sophisticated checker would branch.)

Algorithm

Wing-Gong-style backtracking: at each step, find the set of ops whose :invoke is real-time-minimal (no completed op finished before this op started). Try each as the next-linearized op; if it's consistent with the model, recurse on the remainder. If all candidates fail, backtrack.

Worst-case O(n!) — fine for small histories (~30 ops). For large histories you'd want a smarter algorithm (Knossos-style SAT, or the linear-time check that exists for some special cases).

Returns

  • {:ok, %{linearized_order: [Op.t()]}} — found a valid serial order. Useful for debugging: shows which order matches.
  • {:error, %{reason: ..., ...}} — no valid order exists. The history violates the model.

Summary

Functions

check(events, model)

Check the history against the model. See module doc for return shape.

format_violation(info)

Render an :error info map from check/2 as a human-readable multi-line string. Useful in test failure messages so you can see at a glance which ops linearized and which couldn't fit.

Functions

check(events, model)

@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 the history against the model. See module doc for return shape.

format_violation(info)

@spec format_violation(map()) :: String.t()

Render an :error info map from check/2 as a human-readable multi-line string. Useful in test failure messages so you can see at a glance which ops linearized and which couldn't fit.

case Lockstep.Checker.Linearizable.check(events, Register) do
  {:ok, _} -> :ok
  {:error, info} -> raise Lockstep.Checker.Linearizable.format_violation(info)
end