A specification of correct sequential behavior for a system under test. Consistency checkers (Lockstep.Checker.Linearizable, Lockstep.Checker.SequentialConsistency) consult a Model to decide whether a candidate serial order of operations is valid.

A Model has two callbacks:

• init/0 — initial state.
• step/3 — apply an (invoke, complete) operation pair to state. Return {:ok, new_state} if the completion is consistent with the state, or {:error, reason} if it isn't (e.g. a :read returned a value that the model says shouldn't be visible).

Models are pure functions of state — no message passing, no IO. The checker runs them many times under different orderings.

Built-in models

• Lockstep.Model.Register — read/write/cas register.

Writing a model

defmodule Counter do
  @behaviour Lockstep.Model

  def init, do: 0

  def step(n, %{f: :inc}, %{type: :ok, value: result}) do
    if result == n + 1, do: {:ok, n + 1}, else: {:error, :unexpected_inc}
  end

  def step(n, %{f: :read}, %{type: :ok, value: v}) do
    if v == n, do: {:ok, n}, else: {:error, :stale_read}
  end

  # Generic completion handlers
  def step(n, _invoke, %{type: :fail}), do: {:ok, n}
  def step(n, _invoke, %{type: :info}), do: {:ok, n}
end