Layer 3 — does the implementation conform?

ExTLA tutorial. Previous: Layer 1 — invariants on a running GenServer.

A specification describes abstract states and the steps between them. An implementation has concrete state — a map with holder and waiting in it — and messages. Conformance means that every step the implementation takes, seen through a mapping to the abstract state, is a step the specification allows. The mapping is a refinement:

defmodule Tutorial.Refinement do
  use ExTLA.Refinement

  def abstract(%{holder: holder, waiting: waiting}) do
    pc =
      Map.new([:alice, :bob, :carol], fn c ->
        {c,
         cond do
           holder == c -> :holding
           c in waiting -> :waiting
           true -> :idle
         end}
      end)

    %{free: holder == nil, pc: pc}
  end

  def abstract_action({:request, c}), do: {:request, %{c: c}}
  def abstract_action({:acquire, c}), do: {:acquire, %{c: c}}
  def abstract_action({:release, c}), do: {:release, %{c: c}}
  def abstract_action(_), do: :unmapped

  def concrete_message(:request, %{c: c}), do: {:request, c}
  def concrete_message(:acquire, %{c: c}), do: {:acquire, c}
  def concrete_message(:release, %{c: c}), do: {:release, c}
end

abstract/1 maps a concrete state to the spec's variables — exactly the spec's variables, same keys, same shapes. abstract_action/1 maps a message to the spec action it performs, with its params; :unmapped is not a shrug but a claim, that the message does not move the abstract state, and it is checked as one. concrete_message/2 is the inverse, and it is what lets the spec drive the implementation. The mapping is validated when the server compiles: one that forgets a variable or an action fails the build.

Now the server, with the mapping attached:

defmodule Tutorial.CheckedLockServer do
  use GenServer
  use ExTLA.GenServer, spec: Tutorial.Lock, refinement: Tutorial.Refinement

  def start_link(opts \\ []), do: GenServer.start_link(__MODULE__, opts)

  @impl true
  def init(_opts), do: {:ok, %{holder: nil, waiting: []}}

  @impl true
  def handle_call({:request, c}, _from, s), do: {:reply, :ok, %{s | waiting: s.waiting ++ [c]}}

  def handle_call({:acquire, c}, _from, %{holder: nil} = s),
    do: {:reply, :ok, %{s | holder: c, waiting: List.delete(s.waiting, c)}}

  def handle_call({:release, c}, _from, %{holder: c} = s), do: {:reply, :ok, %{s | holder: nil}}
end

use ExTLA.GenServer wraps every callback (Layer 1 is built in). After each one, the pre- and post-states go through abstract/1, the message through abstract_action/1, and the step is checked for legality: the named action's guard must have held in the abstract pre-state, and the spec's transition from that state must produce exactly the abstract post-state. That second half is the refinement check, and it is what makes this conformance rather than a projection with some predicates on it (§What conformance checks). Acquire without having requested, which the code is perfectly willing to do and the spec is not:

{:ok, pid} = Tutorial.CheckedLockServer.start_link()
GenServer.call(pid, {:acquire, :alice})

** (ExTLA.GenServer.Violation) ═══ CONFORMANCE: NOT ENABLED ═════════════════════════════════════════════════

  The implementation took :acquire, which the spec does not permit here.

  The guard is false in this state for every binding the mapping admits.

  abstract pre-state:
        free = true
        pc = %{alice: :idle, bob: :idle, carol: :idle}


  spec:   Tutorial.Lock

Simulation: random traces, every step checked

Driving the server by hand finds what you thought to try. mix extla.simulate generates messages from the spec — those whose action is enabled in the current abstract state, via concrete_message/2 — and runs them against the live server, checking every step as above:

mix extla.simulate Tutorial.CheckedLockServer --seed 1

Tutorial.CheckedLockServer — NO FINDING
  100 traces, 2500 steps, 0 restarts, 179ms, seed 1
  covered 100% of the spec's actions: acquire x800, release x738, request x962
  20 distinct abstract states

A run like this has checked the traces it drew and nothing else, and the report says which actions those were: all three, and all twenty of the abstract states the DSL page counted. The seed is always printed so that a finding can be run again.

Here is a server with a bug in it. On release it puts the client back on the waiting list — an off-by-one in somebody's idea of a queue:

defmodule Tutorial.LeakyLockServer do
  use GenServer
  use ExTLA.GenServer, spec: Tutorial.Lock, refinement: Tutorial.Refinement

  def start_link(opts \\ []), do: GenServer.start_link(__MODULE__, opts)

  @impl true
  def init(_opts), do: {:ok, %{holder: nil, waiting: []}}

  @impl true
  def handle_call({:request, c}, _from, s), do: {:reply, :ok, %{s | waiting: s.waiting ++ [c]}}

  def handle_call({:acquire, c}, _from, %{holder: nil} = s),
    do: {:reply, :ok, %{s | holder: c, waiting: List.delete(s.waiting, c)}}

  def handle_call({:release, c}, _from, %{holder: c} = s),
    do: {:reply, :ok, %{s | holder: nil, waiting: s.waiting ++ [c]}}
end

mix extla.simulate Tutorial.LeakyLockServer --seed 1

Tutorial.LeakyLockServer — CONFORMANCE VIOLATION: diverged
  1 traces, 5 steps, 0 restarts, 0ms, seed 1
  covered 100% of the spec's actions: acquire x1, release x1, request x3
  6 distinct abstract states

═══ CONFORMANCE: DIVERGED ════════════════════════════════════════════════════

  :release is enabled, but the spec's transition does not produce what the
  implementation produced. Closest candidate binding: %{c: :alice}

  variables that differ:
        pc:
          spec:           %{alice: :idle, bob: :waiting, carol: :waiting}
          implementation: %{alice: :waiting, bob: :waiting, carol: :waiting}

  abstract pre-state:
        free = false
        pc = %{alice: :holding, bob: :waiting, carol: :waiting}


  spec:   Tutorial.Lock

═══ VIOLATION: diverged ════════════════════════════════════════════
═══ CONFORMANCE: DIVERGED ════════════════════════════════════════════════════

  :release is enabled, but the spec's transition does not produce what the
  implementation produced. Closest candidate binding: %{c: :alice}

  variables that differ:
        pc:
          spec:           %{alice: :idle, bob: :waiting, carol: :waiting}
          implementation: %{alice: :waiting, bob: :waiting, carol: :waiting}

  abstract pre-state:
        free = false
        pc = %{alice: :holding, bob: :waiting, carol: :waiting}


  spec:   Tutorial.Lock

State 1 (Init):
  free = true
  pc   = %{alice: :idle, bob: :idle, carol: :idle}

── request(c: :alice) ────────────────────

State 2:
  free = true
  pc   = %{alice: :waiting, bob: :idle, carol: :idle}   ← changed

── request(c: :bob) ────────────────────

State 3:
  free = true
  pc   = %{alice: :waiting, bob: :waiting, carol: :idle}   ← changed

── acquire(c: :alice) ────────────────────

State 4:
  free = false   ← changed
  pc   = %{alice: :holding, bob: :waiting, carol: :idle}   ← changed

── request(c: :carol) ────────────────────

State 5:
  free = false
  pc   = %{alice: :holding, bob: :waiting, carol: :waiting}   ← changed

── release(c: :alice) ────────────────────

State 6 [VIOLATION]:
  free = true   ← changed
  pc   = %{alice: :waiting, bob: :waiting, carol: :waiting}   ← changed

════════════════════════════════════════════════════════════════════

Every invariant of Tutorial.Lock holds in that post-state. Alice is waiting, nobody holds, the lock is free — a state the spec has. What the spec does not have is a release step that lands there, and that is why the step is what gets checked. The finding is a ExTLA.Trace, the same shape the model checker produces, and the report shows the whole behaviour that led to it.

Replay: the counterexample, run against the code

The loop that makes the three layers one tool. Symmetry's Tutorial.NamedLock has a counterexample — Carol requests, Carol acquires — found by the checker before any code existed. ExTLA.Replay drives a server through that exact sequence, via concrete_message/2, and checks each state it reaches against the trace's:

result = ExTLA.ModelChecker.run(Tutorial.NamedLock, %{constants: %{clients: MapSet.new([:alice, :bob, :carol])}})
%{status: :violation} = result

report = ExTLA.Replay.counterexample(Tutorial.CheckedLockServer, result.violation)
%{status: :ok, steps_checked: 2} = report

:ok here means reproduced: the running server performed both steps and arrived, state for state, where the checker said it would. The abstract finding is a fact about the code. And a Layer 3 finding replays the same way — the leaky server's trace, run against the leaky server, diverges at the same step:

simulation = ExTLA.Simulation.run(Tutorial.LeakyLockServer, %{traces: 100, max_steps: 25, seed: 1})
%{status: :violation} = simulation

report = ExTLA.Replay.counterexample(Tutorial.LeakyLockServer, simulation.violation)
%{status: :violation, violation: %{kind: :diverged}} = report

From the shell the counterexample travels as JSON — mix extla.check --format json writes it, and mix extla.replay reads it:

mix extla.check Tutorial.NamedLock --format json > counterexample.json
mix extla.replay Tutorial.CheckedLockServer --trace counterexample.json

With --trace the task starts the server itself, with [] as its init argument. --init-arg passes a different one (a literal term such as [start: 0]; an expression is refused, never run), --server drives a process that is already running and registered (MyApp.Server or :name) instead of starting one, and --timeout sets how many milliseconds to wait for each reply (default 5000). They are ExTLA.Replay.counterexample/3's :init_arg, :server and :timeout. All three are refused with --captured, which checks a recorded trace and drives nothing.

mix extla.replay exits 0 when the behaviour was reproduced, 1 on a conformance violation, and 2 when the implementation could not follow the trace — which is not a conformance failure: the spec permits a behaviour the code does not take, and which of the two is wrong is not something the tool can decide. It says so, rather than guessing. It exits 3 when the trace names a step it cannot reproduce: a :restart (a crash injected by mix extla.simulate --inject-failures) against a server it was handed with --server, which it does not own and will not kill. That is a limit of the replay, not a claim about the implementation.

That is the whole pipeline (§The verification pipeline): model check the spec, so design bugs are found before the code exists; simulate the implementation against it, so the code is held to the design; replay any counterexample against the code, so a finding at either level is a fact about both. Running all of that from your own suite, and keeping it running, is Putting a specification in your project.

Where to next

• The DSL reference — the DSL, normatively. Every rule this page leaned on is stated there with its reason.
• The reference — the checker's options and what each costs, the JSON result schema, state constraints, symmetry, parallel exploration, and what conformance checks.
• ExTLA.GenServer, ExTLA.Refinement, ExTLA.Simulation and ExTLA.Replay — the conformance layer, module by module, and mix help extla.simulate for --against-graph, which checks Layers 2 and 3 against each other.
• The examples — whole specifications with implementations, including the distributed lock this tutorial's is a small cousin of.
• Design decisions — why the tool is shaped the way it is, decision by decision.

The pages above are where to go when this tutorial has stopped answering a question. The tutorial itself continues: the next three pages are the ones about using this on a system you did not write for it.

Next: From a system you have to a specification you can check.