From 0e802b4a01f24a8c587ca942a91d64b5a0105e3e Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 28 Oct 2026 21:05:41 -0700 Subject: [PATCH] Add Hillel Wayne's two-thread counter as a first refinement example. The refinement examples in this repository are too large to show what a refinement mapping is in a few minutes. Hillel Wayne's two-thread counter from his blog post fits on a page. TLC finds the lost update when bad.tla splits the increment into a read and a write, and verifies that good.tla, which adds a lock, refines both abstract.tla and bad.tla. good_proof.tla proves both refinements with TLAPS. https://www.hillelwayne.com/post/refinement/ Co-authored-by: Hillel Wayne <2660212+hwayne@users.noreply.github.com> Co-authored-by: Claude Opus 5.5 Signed-off-by: Markus Alexander Kuppe --- README.md | 1 + .../SpecificationRefinement/README.md | 8 +++ .../SpecificationRefinement/abstract.cfg | 3 + .../SpecificationRefinement/abstract.tla | 30 +++++++++ .../SpecificationRefinement/bad.cfg | 5 ++ .../SpecificationRefinement/bad.tla | 49 +++++++++++++++ .../SpecificationRefinement/good.cfg | 7 +++ .../SpecificationRefinement/good.tla | 63 +++++++++++++++++++ .../SpecificationRefinement/good_proof.tla | 45 +++++++++++++ .../SpecificationRefinement/manifest.json | 63 +++++++++++++++++++ 10 files changed, 274 insertions(+) create mode 100644 specifications/SpecificationRefinement/README.md create mode 100644 specifications/SpecificationRefinement/abstract.cfg create mode 100644 specifications/SpecificationRefinement/abstract.tla create mode 100644 specifications/SpecificationRefinement/bad.cfg create mode 100644 specifications/SpecificationRefinement/bad.tla create mode 100644 specifications/SpecificationRefinement/good.cfg create mode 100644 specifications/SpecificationRefinement/good.tla create mode 100644 specifications/SpecificationRefinement/good_proof.tla create mode 100644 specifications/SpecificationRefinement/manifest.json diff --git a/README.md b/README.md index 67a492cb..684b3fef 100644 --- a/README.md +++ b/README.md @@ -45,6 +45,7 @@ Here is a list of specs included in this repository which are validated by the C | [The Coffee Can Bean Problem](specifications/CoffeeCan) | Andrew Helwer | ✔ | ✔ | | ✔ | ✔ | | [EWD687a: Detecting Termination in Distributed Computations](specifications/ewd687a) | Stephan Merz, Leslie Lamport, Markus Kuppe | ✔ | ✔ | (✔) | ✔ | | | [The Moving Cat Puzzle](specifications/Moving_Cat_Puzzle) | Florian Schanda | ✔ | | | ✔ | ✔ | +| [Specification Refinement](specifications/SpecificationRefinement) | Hillel Wayne | ✔ | ✔ | | ✔ | | | [The Boulangerie Algorithm](specifications/Bakery-Boulangerie) | Leslie Lamport, Stephan Merz | | ✔ | ✔ | ✔ | | | [Misra Reachability Algorithm](specifications/MisraReachability) | Leslie Lamport | | ✔ | ✔ | ✔ | ✔ | | [Byzantizing Paxos by Refinement](specifications/byzpaxos) | Leslie Lamport | | ✔ | ✔ | ✔ | | diff --git a/specifications/SpecificationRefinement/README.md b/specifications/SpecificationRefinement/README.md new file mode 100644 index 00000000..93e099d0 --- /dev/null +++ b/specifications/SpecificationRefinement/README.md @@ -0,0 +1,8 @@ +# Specification Refinement + +This example accompanies Hillel Wayne's blog post [*Specification Refinement*](https://www.hillelwayne.com/post/refinement/), which introduces refinement mappings in TLA⁺ using a two-thread counter: + +- [`abstract.tla`](abstract.tla) (`abstract.cfg`): The high-level specification where two threads atomically increment a shared `counter` and transition from `"start"` to `"done"`. +- [`bad.tla`](bad.tla) (`bad.cfg`): A lower-level specification that splits the increment into two non-atomic steps (`GetCounter` and `IncCounter`) using a thread-local variable `tmp` and an intermediate state `"inc"`. Checking `PROPERTY Refinement` with TLC fails with a liveness/temporal property violation, exhibiting the race condition where both threads read `0` and both write `1`. +- [`good.tla`](good.tla) (`good.cfg`): Adds a `lock` variable to make the read-modify-write critical section mutually exclusive. TLC verifies that `good` refines both `abstract` (`Refinement`) and `bad` (`RefinesBad`). +- [`good_proof.tla`](good_proof.tla): TLAPS machine-checked proofs that `good` refines both `abstract` (`THEOREM ImplementsAbstract == Spec => Refinement`) and `bad` (`THEOREM ImplementsBad == Spec => RefinesBad`). diff --git a/specifications/SpecificationRefinement/abstract.cfg b/specifications/SpecificationRefinement/abstract.cfg new file mode 100644 index 00000000..8f0db86b --- /dev/null +++ b/specifications/SpecificationRefinement/abstract.cfg @@ -0,0 +1,3 @@ +SPECIFICATION Spec + +CHECK_DEADLOCK FALSE diff --git a/specifications/SpecificationRefinement/abstract.tla b/specifications/SpecificationRefinement/abstract.tla new file mode 100644 index 00000000..45b18ac3 --- /dev/null +++ b/specifications/SpecificationRefinement/abstract.tla @@ -0,0 +1,30 @@ +---- MODULE abstract ---- +EXTENDS Integers, Sequences + +VARIABLES pc, counter +vars == <> + +\* Two threads +Threads == 1..2 + +\* State transition action +Trans(thread, from, to) == + /\ pc[thread] = from + /\ pc' = [pc EXCEPT ![thread] = to] + +\* Both threads start in the `start` state +Init == + /\ pc = [t \in Threads |-> "start"] + /\ counter = 0 + +Next == + \* Pick one thread + \/ \E t \in Threads: + \* Move it to `done` + /\ Trans(t, "start", "done") + \* Increment counter + /\ counter' = counter + 1 + +Spec == Init /\ [][Next]_vars + +==== diff --git a/specifications/SpecificationRefinement/bad.cfg b/specifications/SpecificationRefinement/bad.cfg new file mode 100644 index 00000000..8e1c5e4e --- /dev/null +++ b/specifications/SpecificationRefinement/bad.cfg @@ -0,0 +1,5 @@ +SPECIFICATION Spec + +PROPERTY Refinement + +CHECK_DEADLOCK FALSE diff --git a/specifications/SpecificationRefinement/bad.tla b/specifications/SpecificationRefinement/bad.tla new file mode 100644 index 00000000..109952c3 --- /dev/null +++ b/specifications/SpecificationRefinement/bad.tla @@ -0,0 +1,49 @@ +---- MODULE bad ---- +EXTENDS Integers, Sequences + +VARIABLES pc, counter, tmp +vars == <> + +Threads == 1..2 + +States == {"start", "inc", "done"} + +Trans(thread, from, to) == + /\ pc[thread] = from + /\ pc' = [pc EXCEPT ![thread] = to] + +Init == + /\ pc = [t \in Threads |-> "start"] + /\ counter = 0 + /\ tmp = [t \in Threads |-> 0] + +GetCounter(t) == + /\ tmp' = [tmp EXCEPT ![t] = counter] + /\ UNCHANGED counter + +IncCounter(t) == + /\ counter' = tmp[t] + 1 + /\ UNCHANGED tmp + +Next == + \/ \E t \in Threads: + \* Step to get the counter value + \/ /\ Trans(t, "start", "inc") + /\ GetCounter(t) + \* Step to increment the counter + \/ /\ Trans(t, "inc", "done") + /\ IncCounter(t) + +Spec == Init /\ [][Next]_vars + +Mapping == + INSTANCE abstract WITH + counter <- counter, + pc <- [t \in Threads |-> + IF pc[t] = "inc" THEN "start" + ELSE pc[t] + ] + +Refinement == Mapping!Spec + +==== diff --git a/specifications/SpecificationRefinement/good.cfg b/specifications/SpecificationRefinement/good.cfg new file mode 100644 index 00000000..8a561355 --- /dev/null +++ b/specifications/SpecificationRefinement/good.cfg @@ -0,0 +1,7 @@ +SPECIFICATION Spec + +PROPERTIES + Refinement + RefinesBad + +CHECK_DEADLOCK FALSE diff --git a/specifications/SpecificationRefinement/good.tla b/specifications/SpecificationRefinement/good.tla new file mode 100644 index 00000000..aaf758ca --- /dev/null +++ b/specifications/SpecificationRefinement/good.tla @@ -0,0 +1,63 @@ +---- MODULE good ---- +EXTENDS Integers, Sequences + +VARIABLES pc, counter, tmp, lock +vars == <> + +Threads == 1..2 + +States == {"start", "inc", "done"} + +Trans(thread, from, to) == + /\ pc[thread] = from + /\ pc' = [pc EXCEPT ![thread] = to] + +Init == + /\ pc = [t \in Threads |-> "start"] + /\ counter = 0 + /\ tmp = <<0, 0>> + /\ lock = 0 + +AcquireLock(t) == + /\ lock = 0 + /\ lock' = t + +ReleaseLock(t) == + /\ lock = t + /\ lock' = 0 + +GetCounter(t) == + /\ tmp' = [tmp EXCEPT ![t] = counter] + /\ UNCHANGED counter + +IncCounter(t) == + /\ counter' = tmp[t] + 1 + /\ UNCHANGED tmp + +Next == + \/ \E t \in Threads: + \/ /\ Trans(t, "start", "inc") + /\ GetCounter(t) + /\ AcquireLock(t) + \/ /\ Trans(t, "inc", "done") + /\ IncCounter(t) + /\ ReleaseLock(t) + +Spec == Init /\ [][Next]_vars + +Mapping == + INSTANCE abstract WITH + counter <- counter, + pc <- [t \in Threads |-> + IF pc[t] = "inc" THEN "start" + ELSE pc[t] + ] + +Refinement == Mapping!Spec + +BadMapping == + INSTANCE bad + +RefinesBad == BadMapping!Spec + +==== diff --git a/specifications/SpecificationRefinement/good_proof.tla b/specifications/SpecificationRefinement/good_proof.tla new file mode 100644 index 00000000..bbf82df4 --- /dev/null +++ b/specifications/SpecificationRefinement/good_proof.tla @@ -0,0 +1,45 @@ +---- MODULE good_proof ---- +EXTENDS good, TLAPS + +TypeOK == + /\ pc \in [Threads -> States] + /\ counter \in Int + /\ tmp \in [Threads -> Int] + /\ lock \in Threads \cup {0} + +Inv == + /\ TypeOK + /\ \A t \in Threads : + /\ (pc[t] = "inc") <=> (lock = t) + /\ (pc[t] = "inc") => (tmp[t] = counter) + +LEMMA TypeAndInv == Spec => []Inv +<1>1. Init => Inv + BY DEF Init, Inv, TypeOK, Threads, States +<1>2. Inv /\ [Next]_vars => Inv' + BY DEF Inv, TypeOK, Next, vars, Threads, States, + Trans, GetCounter, IncCounter, AcquireLock, ReleaseLock +<1>3. QED + BY <1>1, <1>2, PTL DEF Spec + +THEOREM ImplementsAbstract == Spec => Refinement +<1>1. Init => Mapping!Init + BY DEF Init, Mapping!Init, Threads, Mapping!Threads +<1>2. Inv /\ [Next]_vars => [Mapping!Next]_Mapping!vars + BY DEF Inv, TypeOK, Next, vars, Threads, States, + Trans, GetCounter, IncCounter, AcquireLock, ReleaseLock, + Mapping!Next, Mapping!vars, Mapping!Trans, Mapping!Threads +<1>3. QED + BY <1>1, <1>2, TypeAndInv, PTL DEF Spec, Refinement, Mapping!Spec + +THEOREM ImplementsBad == Spec => RefinesBad +<1>1. Init => BadMapping!Init + BY DEF Init, BadMapping!Init, Threads, BadMapping!Threads +<1>2. [Next]_vars => [BadMapping!Next]_BadMapping!vars + BY DEF Next, vars, Threads, Trans, GetCounter, IncCounter, AcquireLock, ReleaseLock, + BadMapping!Next, BadMapping!vars, BadMapping!Threads, + BadMapping!Trans, BadMapping!GetCounter, BadMapping!IncCounter +<1>3. QED + BY <1>1, <1>2, PTL DEF Spec, RefinesBad, BadMapping!Spec + +==== diff --git a/specifications/SpecificationRefinement/manifest.json b/specifications/SpecificationRefinement/manifest.json new file mode 100644 index 00000000..b21e0f28 --- /dev/null +++ b/specifications/SpecificationRefinement/manifest.json @@ -0,0 +1,63 @@ +{ + "sources": [ + "https://www.hillelwayne.com/post/refinement/" + ], + "authors": [ + "Hillel Wayne" + ], + "tags": [ + "beginner" + ], + "modules": [ + { + "path": "specifications/SpecificationRefinement/abstract.tla", + "features": [], + "models": [ + { + "path": "specifications/SpecificationRefinement/abstract.cfg", + "runtime": "00:00:01", + "mode": "exhaustive search", + "result": "success", + "distinctStates": 4, + "totalStates": 5, + "stateDepth": 3 + } + ] + }, + { + "path": "specifications/SpecificationRefinement/bad.tla", + "features": [], + "models": [ + { + "path": "specifications/SpecificationRefinement/bad.cfg", + "runtime": "00:00:01", + "mode": "exhaustive search", + "result": "liveness failure" + } + ] + }, + { + "path": "specifications/SpecificationRefinement/good.tla", + "features": [], + "models": [ + { + "path": "specifications/SpecificationRefinement/good.cfg", + "runtime": "00:00:01", + "mode": "exhaustive search", + "result": "success", + "distinctStates": 9, + "totalStates": 9, + "stateDepth": 5 + } + ] + }, + { + "path": "specifications/SpecificationRefinement/good_proof.tla", + "features": [], + "models": [], + "proof": { + "maxRuntimeMinutes": 1 + } + } + ] +}