ExTLA tutorial. Previous: Invariants.
Nothing so far says the lock ever does anything. A spec in which every client waits forever
satisfies mutual_exclusion perfectly. Liveness is the other half: what must eventually happen.
temporal :no_starvation do
Enum.all?(^clients, fn c -> (pc[c] == :waiting) ~> (pc[c] == :holding) end)
endp ~> q is leads-to: whenever p holds, q holds at that point or later. The Enum.all? over
a constant is TLA+'s \A c \in Clients, one property per client. always, eventually and ~>
are the operators, and the fragment they may form is bounded and stated
(§5.1); a
formula outside it is a compile error, never a silently weaker check.
mix extla.check checks a temporal property whenever the spec declares one; --safety-only
turns it off, and under symmetry or --workers above 1 it is skipped with a warning. From code it
is the other way round: ExTLA.ModelChecker.run/2 and assert_spec/2 check liveness only when
the config says check_liveness: true. And the first thing you learn on checking one is that a
leads-to is refuted by a system that is merely allowed to stop — so a spec with a temporal
property needs to say which actions the system can be relied on to take. That is fairness, and there are two strengths of it.
Weak fairness, refuted
Weak fairness on an action says: if the action stays enabled from some point on, it is
eventually taken. Declared per client — acquire: [:c] is one constraint for each value of c,
and 02-dsl-semantics.md §5.2 says why the whole-action form would not do:
defmodule Tutorial.WeakLock do
use ExTLA.Spec
constant :clients, default: set([:alice, :bob, :carol])
variable :free, type: [true, false]
variable :pc, type: [^clients ~> [:idle, :waiting, :holding]]
init do
free = true
pc = for_each(^clients, fn _ -> :idle end)
end
action :request, params: [c: ^clients] do
require pc[c] == :idle
pc = update(pc, c, fn _ -> :waiting end)
end
action :acquire, params: [c: ^clients] do
require pc[c] == :waiting
require free
free = false
pc = update(pc, c, fn _ -> :holding end)
end
action :release, params: [c: ^clients] do
require pc[c] == :holding
free = true
pc = update(pc, c, fn _ -> :idle end)
end
invariant :mutual_exclusion do
Enum.count(^clients, fn c -> pc[c] == :holding end) <= 1
end
invariant :holding_means_taken do
Enum.all?(^clients, fn c -> pc[c] != :holding end) or free == false
end
temporal :no_starvation do
Enum.all?(^clients, fn c -> (pc[c] == :waiting) ~> (pc[c] == :holding) end)
end
fairness :weak, acquire: [:c], release: [:c]
endmix extla.check Tutorial.WeakLock
Tutorial.WeakLock — LIVENESS: no_starvation
20 distinct states, 48 transitions, depth 5, 1ms
═══ LIVENESS: no_starvation ════════════════════════════════════════
temporal property :no_starvation, at :alice, is refuted by this behaviour
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: :bob) ────────────────────
State 4:
free = false ← changed
pc = %{alice: :waiting, bob: :holding, carol: :idle} ← changed
── release(c: :bob) ────────────────────
State 5 (= state 2, the cycle head):
free = true ← changed
pc = %{alice: :waiting, bob: :idle, carol: :idle} ← changed
════════════════════════════════════════════════════════════════════
↺ back to state 2 — states 2-4 repeat forever.
--- COVERAGE: Tutorial.WeakLock ------------------------------------
Actions enabled in states distinct
acquire 7 12 12
release 12 12 0
request 16 24 7
Invariants evaluated near-miss
holding_means_taken 20 12
mutual_exclusion 20 -
type_ok 20 -
--------------------------------------------------------------------A liveness counterexample is not a trace that ends in a bad state; it is a lasso — a prefix,
then a cycle the system can repeat forever, along which the property never comes true. The
header says which instance of the Enum.all? it refutes — at :alice. Then read the end: state 5
is marked (= state 2, the cycle head), so the system is back where the cycle began, and the line
under the trace says states 2 to 4 repeat forever. Alice asks for the lock in state 2 and is still
waiting when the cycle closes. Bob requests, acquires and releases, forever, and every step of
that is one the fairness constraints permit — because acquire(c: :alice) is not continuously
enabled. It is disabled every time Bob holds the lock.
Weak fairness obliges nothing about an action that keeps being switched off, and this is exactly
the behaviour it does not rule out.
Strong fairness, holding
Strong fairness says: if the action is enabled infinitely often — even intermittently — it is eventually taken. That is the guarantee a lock needs, since a lock is by nature free only now and then:
defmodule Tutorial.StrongLock do
use ExTLA.Spec
constant :clients, default: set([:alice, :bob, :carol])
variable :free, type: [true, false]
variable :pc, type: [^clients ~> [:idle, :waiting, :holding]]
init do
free = true
pc = for_each(^clients, fn _ -> :idle end)
end
action :request, params: [c: ^clients] do
require pc[c] == :idle
pc = update(pc, c, fn _ -> :waiting end)
end
action :acquire, params: [c: ^clients] do
require pc[c] == :waiting
require free
free = false
pc = update(pc, c, fn _ -> :holding end)
end
action :release, params: [c: ^clients] do
require pc[c] == :holding
free = true
pc = update(pc, c, fn _ -> :idle end)
end
invariant :mutual_exclusion do
Enum.count(^clients, fn c -> pc[c] == :holding end) <= 1
end
invariant :holding_means_taken do
Enum.all?(^clients, fn c -> pc[c] != :holding end) or free == false
end
temporal :no_starvation do
Enum.all?(^clients, fn c -> (pc[c] == :waiting) ~> (pc[c] == :holding) end)
end
fairness :strong, acquire: [:c]
fairness :weak, release: [:c]
endmix extla.check Tutorial.StrongLock
Tutorial.StrongLock — verified
20 distinct states, 48 transitions, depth 5, 2msThe same twenty states, the same transitions, the same property — and it holds. Nothing changed
but the assumption about how the system is scheduled, which is what fairness is: a claim about the
implementation, that it will not starve an intermittently-enabled step. release keeps weak
fairness, because a holder's release stays enabled until it is taken, and weak is enough.
Per client, not per action
One more version, because it is the mistake 02-dsl-semantics.md §5.2 exists to name. fairness :strong, [:acquire]
without the [:c] is strong fairness on the action as a whole: if some client's acquire is
enabled infinitely often, some client eventually acquires. Bob acquiring satisfies that. Alice
waits forever anyway:
defmodule Tutorial.WholeActionLock do
use ExTLA.Spec
constant :clients, default: set([:alice, :bob, :carol])
variable :free, type: [true, false]
variable :pc, type: [^clients ~> [:idle, :waiting, :holding]]
init do
free = true
pc = for_each(^clients, fn _ -> :idle end)
end
action :request, params: [c: ^clients] do
require pc[c] == :idle
pc = update(pc, c, fn _ -> :waiting end)
end
action :acquire, params: [c: ^clients] do
require pc[c] == :waiting
require free
free = false
pc = update(pc, c, fn _ -> :holding end)
end
action :release, params: [c: ^clients] do
require pc[c] == :holding
free = true
pc = update(pc, c, fn _ -> :idle end)
end
invariant :mutual_exclusion do
Enum.count(^clients, fn c -> pc[c] == :holding end) <= 1
end
invariant :holding_means_taken do
Enum.all?(^clients, fn c -> pc[c] != :holding end) or free == false
end
temporal :no_starvation do
Enum.all?(^clients, fn c -> (pc[c] == :waiting) ~> (pc[c] == :holding) end)
end
fairness :strong, [:acquire]
fairness :weak, release: [:c]
endTutorial.WholeActionLock — LIVENESS: no_starvation
20 distinct states, 48 transitions, depth 5, 1ms
═══ LIVENESS: no_starvation ════════════════════════════════════════
temporal property :no_starvation, at :alice, is refuted by this behaviour
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: :bob) ────────────────────
State 4:
free = false ← changed
pc = %{alice: :waiting, bob: :holding, carol: :idle} ← changed
── release(c: :bob) ────────────────────
State 5 (= state 2, the cycle head):
free = true ← changed
pc = %{alice: :waiting, bob: :idle, carol: :idle} ← changed
════════════════════════════════════════════════════════════════════
↺ back to state 2 — states 2-4 repeat forever.
--- COVERAGE: Tutorial.WholeActionLock -----------------------------
Actions enabled in states distinct
acquire 7 12 12
release 12 12 0
request 16 24 7
Invariants evaluated near-miss
holding_means_taken 20 12
mutual_exclusion 20 -
type_ok 20 -
--------------------------------------------------------------------Same lasso as the weak one. TLA+ writes \A c \in Clients : SF_vars(Acquire(c)), and so does
ExTLA — acquire: [:c]. The named params must draw from a constant, for the reason the compiler
gives if you try otherwise: a state-drawn param has no fixed set of bindings to attach a
constraint to (§5.2).