From dd2270d97d487d753e9524e5a8c28faed5bc1569 Mon Sep 17 00:00:00 2001 From: Andrew Helwer <2n8rn1w1f@mozmail.com> Date: Fri, 19 Jan 2024 10:22:10 -0500 Subject: [PATCH] Added model for LoopInvariance, tagged it as Beginner Reverted CRLF newline normalizations Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com> --- README.md | 2 +- manifest.json | 40 +- .../Bakery-Boulangerie/Boulanger.tla | 1070 ++++++++--------- .../Bakery-Boulangerie/MCBakery.tla | 2 + .../Bakery-Boulangerie/MCBoulanger.tla | 1 + .../LoopInvariance/MCBinarySearch.cfg | 8 + .../LoopInvariance/MCBinarySearch.tla | 7 + specifications/LoopInvariance/MCQuicksort.cfg | 8 + specifications/LoopInvariance/MCQuicksort.tla | 7 + .../MisraReachability/Reachable.tla | 479 ++++---- specifications/Stones/Stones.tla | 1 - specifications/TeachingConcurrency/Simple.tla | 297 +++-- 12 files changed, 996 insertions(+), 926 deletions(-) create mode 100644 specifications/LoopInvariance/MCBinarySearch.cfg create mode 100644 specifications/LoopInvariance/MCBinarySearch.tla create mode 100644 specifications/LoopInvariance/MCQuicksort.cfg create mode 100644 specifications/LoopInvariance/MCQuicksort.tla diff --git a/README.md b/README.md index 9fa51302..a506229e 100644 --- a/README.md +++ b/README.md @@ -19,6 +19,7 @@ Here is a list of specs included in this repository, with links to the relevant | Name | Author(s) | Beginner | TLAPS Proof | PlusCal | TLC Model | Apalache | | --------------------------------------------------------------------------------------------------- | ------------------------------------------ | :------: | :---------: | :-----: | :-------: | :------: | | [Teaching Concurrency](specifications/TeachingConcurrency) | Leslie Lamport | ✔ | ✔ | ✔ | ✔ | | +| [Loop Invariance](specifications/LoopInvariance) | Leslie Lamport | ✔ | ✔ | ✔ | ✔ | | | [Learn TLA⁺ Proofs](specifications/LearnProofs) | Andrew Helwer | ✔ | ✔ | ✔ | ✔ | | | [Boyer-Moore Majority Vote](specifications/Majority) | Stephan Merz | ✔ | ✔ | | ✔ | | | [Proof x+x is Even](specifications/sums_even) | Stephan Merz | ✔ | ✔ | | | | @@ -34,7 +35,6 @@ Here is a list of specs included in this repository, with links to the relevant | [Stone Scale Puzzle](specifications/Stones) | Leslie Lamport | ✔ | | | ✔ | | | [The Boulangerie Algorithm](specifications/Bakery-Boulangerie) | Leslie Lamport, Stephan Merz | | ✔ | ✔ | ✔ | | | [Misra Reachability Algorithm](specifications/MisraReachability) | Leslie Lamport | | ✔ | ✔ | | | -| [Loop Invariance](specifications/LoopInvariance) | Leslie Lamport | | ✔ | ✔ | | | | [EWD840: Termination Detection in a Ring](specifications/ewd840) | Stephan Merz | | ✔ | | ✔ | | | [EWD998: Termination Detection in a Ring with Asynchronous Message Delivery](specifications/ewd998) | Stephan Merz, Markus Kuppe | | ✔ | | ✔ | | | [The Paxos Protocol](specifications/Paxos) | Leslie Lamport | | ✔ | | ✔ | | diff --git a/manifest.json b/manifest.json index af18a36e..f2de77fa 100644 --- a/manifest.json +++ b/manifest.json @@ -836,7 +836,9 @@ "authors": [ "Leslie Lamport" ], - "tags": [], + "tags": [ + "beginner" + ], "modules": [ { "path": "specifications/LoopInvariance/BinarySearch.tla", @@ -848,6 +850,42 @@ ], "models": [] }, + { + "path": "specifications/LoopInvariance/MCBinarySearch.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/LoopInvariance/MCBinarySearch.cfg", + "runtime": "small", + "size": "00:00:05", + "mode": "exhaustive search", + "features": [ + "liveness" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/LoopInvariance/MCQuicksort.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/LoopInvariance/MCQuicksort.cfg", + "runtime": "00:00:05", + "size": "small", + "mode": "exhaustive search", + "features": [ + "liveness" + ], + "result": "success" + } + ] + }, { "path": "specifications/LoopInvariance/Quicksort.tla", "communityDependencies": [], diff --git a/specifications/Bakery-Boulangerie/Boulanger.tla b/specifications/Bakery-Boulangerie/Boulanger.tla index 5aa0e89d..c1e87a3a 100644 --- a/specifications/Bakery-Boulangerie/Boulanger.tla +++ b/specifications/Bakery-Boulangerie/Boulanger.tla @@ -1,538 +1,538 @@ ------------------------------- MODULE Boulanger ---------------------------- -(***************************************************************************) -(* This is a PlusCal encoding of the Boulangerie Algorithm of Yoram Moses *) -(* and Katia Patkin--a variant of the Bakery Algorithm--and a proof that *) -(* it implements mutual exclusion. The bakery algorithm appeared in *) -(* *) -(* Leslie Lamport *) -(* A New Solution of Dijkstra's Concurrent Programming Problem *) -(* Communications of the ACM 17, 8 (August 1974), 453-455 *) -(* *) -(* The PlusCal encoding differs from the Moses-Patkin algorithm in one *) -(* respect. To enter the critical section, the PlusCal version examines *) -(* other processes one at a time--in the while loop at label w1. The *) -(* Moses-Patkin algorithm performs those examinations in parallel. *) -(* Because PlusCal does not allow sub-processes, it would be difficult *) -(* (but not impossible) to express that algorithm in PlusCal. It would be *) -(* easy to express their version in TLA+ (for example, by modifying the *) -(* TLA+ translation of the PlusCal code), and it should be straightforward *) -(* to convert the invariance proof presented here to a proof of the more *) -(* general version. I will leave that as an exercise for others. *) -(* *) -(* I started with a PlusCal encoding and invariance proof of the Bakery *) -(* Algorithm. The only non-obvious part of that encoding is how it *) -(* represented the safe registers assumed by the algorithm, which are *) -(* registers in which reads and writes are not atomic. A safe register is *) -(* represented by a variable r whose value is written by performing some *) -(* number of atomic writes of non-deterministically chosen "legal" values *) -(* to r followed by a single write of the desired value. A read of the *) -(* register is performed by a single atomic read of r. It can be shown *) -(* that this captures the semantics of a safe register. *) -(* *) -(* Starting from the PlusCal version of the Bakery Algorithm, it was easy *) -(* to modify it to the Boulangerie Algorithm (with the simplification *) -(* described above). I model checked the algorithm on some small models *) -(* to convince myself that there were no trivial errors that would be *) -(* likely to arise from an error in the encoding. I then modified the *) -(* invariant by a combination of a bit of thinking and a fair amount of *) -(* trial and error, finding errors in the invariant by model checking very *) -(* small models. (I checked it on two processes with chosen numbers *) -(* restricted to be at most 3.) *) -(* *) -(* When checking on a small model revealed no error in the invariant, I *) -(* checked the proof with TLAPS (the TLA+ proof system). The high level *) -(* proof, consisting of steps <1>1 - <1>4, are standard and are the same *) -(* as for the Bakery Algorithm. TLAPS checks this simple four-step proof *) -(* for the Bakery Algorithm with terminal BY proofs that just tell it to *) -(* use the necessary assumptions and to expand all definitions. This *) -(* didn't work for the hard part of the Boulangerie Algorithm--step <1>2 *) -(* that checks inductive invariance. *) -(* *) -(* When a proof doesn't go through, one keeps decomposing the proof of the *) -(* steps that aren't proved until one sees what the problem is. This *) -(* decomposition is done with little thinking and no typing using the *) -(* Toolbox's Decompose Proof command. (The Toolbox is the IDE for the *) -(* TLA+ tools.) Step <1>2 has the form A /\ B => C, where B is a *) -(* disjunction, and the Decompose Proof command produces a level-<2> proof *) -(* consisting of subgoals essentially of the form A /\ Bi => C for the *) -(* disjuncts Bi of B. Two of those subgoals weren't proved. I decomposed *) -(* them both for several levels until I saw that in one of them, some step *) -(* wasn't preserving the part of the invariant that asserts *) -(* type-correctness. I then quickly found the culprit: a silly error in *) -(* the type invariant in which I had in one place written the set Proc of *) -(* process numbers instead of the set Nat of natural numbers. After *) -(* correcting that error, only one of the level-<2> subgoals remained *) -(* unproved: step <2>5. Using the Decompose Proof command as far as I *) -(* could on that step, one substep remained unproved. (I think it was at *) -(* level <5>.) Looking at what the proof obligations were, the obvious *) -(* decomposition was a two-way case split, which I did by manually *) -(* entering another level of subproof. One of those cases weren't proved, *) -(* so I tried another two-way case split on it. That worked. I then made *) -(* that substep to the first step of the (level <3>) proof of <2>5, moving *) -(* its proof with it. With that additional fact, TLAPS was able to prove *) -(* <2>5 in one more step (the QED step). *) -(* *) -(* The entire proof now is about 70 lines. I only typed 20 of those 70 *) -(* lines. The rest either came from the original Bakery Algorithm *) -(* (8-line) proof or were generated by the Decompose Proof Command. *) -(* *) -(* I don't know how much time I actually spent writing the algorithm and *) -(* its proof. Except for the final compaction of the (correct) proof of *) -(* <2>5, the entire exercise took me two days. However, most of that was *) -(* spent tracking down bugs in the Toolbox. We are in the process of *) -(* moving the Toolbox to a new version of Eclipse, and there are many bugs *) -(* that must be fixed before it's ready to be released. I would estimate *) -(* that it would have taken me less than 4 hours without Toolbox bugs. I *) -(* find it remarkable how little thinking the whole thing took. *) -(* *) -(* This whole process was a lot easier than trying to write a convincing *) -(* hand proof--a proof that I would regard as adequate to justify *) -(* publication of the proof. *) -(***************************************************************************) - -EXTENDS Integers, TLAPS - -(***************************************************************************) -(* We first declare N to be the number of processes, and we assume that N *) -(* is a natural number. *) -(***************************************************************************) -CONSTANT N -ASSUME N \in Nat - -(***************************************************************************) -(* We define Procs to be the set {1, 2, ... , N} of processes. *) -(***************************************************************************) -Procs == 1..N - -(***************************************************************************) -(* \prec is defined to be the lexicographical less-than relation on pairs *) -(* of numbers. *) -(***************************************************************************) -a \prec b == \/ a[1] < b[1] - \/ (a[1] = b[1]) /\ (a[2] < b[2]) - -(*** this is a comment containing the PlusCal code * - ---algorithm Boulanger -{ variable num = [i \in Procs |-> 0], flag = [i \in Procs |-> FALSE]; - fair process (p \in Procs) - variables unchecked = {}, max = 0, nxt = 1, previous = -1 ; - { ncs:- while (TRUE) - { e1: either { flag[self] := ~ flag[self] ; - goto e1 } - or { flag[self] := TRUE; - unchecked := Procs \ {self} ; - max := 0 - } ; - e2: while (unchecked # {}) - { with (i \in unchecked) - { unchecked := unchecked \ {i}; - if (num[i] > max) { max := num[i] } - } - }; - e3: either { with (k \in Nat) { num[self] := k } ; - goto e3 } - or { num[self] := max + 1 } ; - e4: either { flag[self] := ~ flag[self] ; - goto e4 } - or { flag[self] := FALSE; - unchecked := IF num[self] = 1 - THEN 1..(self-1) - ELSE Procs \ {self} - } ; - w1: while (unchecked # {}) - { with (i \in unchecked) { nxt := i }; - await ~ flag[nxt]; - previous := -1 ; - w2: if ( \/ num[nxt] = 0 - \/ <> \prec <> - \/ /\ previous # -1 - /\ num[nxt] # previous) - { unchecked := unchecked \ {nxt}; - if (unchecked = {}) {goto cs} - else {goto w1} - } - else { previous := num[nxt] ; - goto w2 } - - } ; - cs: skip ; \* the critical section; - exit: either { with (k \in Nat) { num[self] := k } ; - goto exit } - or { num[self] := 0 } - } - } -} - - this ends the comment containing the PlusCal code -*************) - -\* BEGIN TRANSLATION (this begins the translation of the PlusCal code) -VARIABLES num, flag, pc, unchecked, max, nxt, previous - -vars == << num, flag, pc, unchecked, max, nxt, previous >> - -ProcSet == (Procs) - -Init == (* Global variables *) - /\ num = [i \in Procs |-> 0] - /\ flag = [i \in Procs |-> FALSE] - (* Process p *) - /\ unchecked = [self \in Procs |-> {}] - /\ max = [self \in Procs |-> 0] - /\ nxt = [self \in Procs |-> 1] - /\ previous = [self \in Procs |-> -1] - /\ pc = [self \in ProcSet |-> "ncs"] - -ncs(self) == /\ pc[self] = "ncs" - /\ pc' = [pc EXCEPT ![self] = "e1"] - /\ UNCHANGED << num, flag, unchecked, max, nxt, previous >> - -e1(self) == /\ pc[self] = "e1" - /\ \/ /\ flag' = [flag EXCEPT ![self] = ~ flag[self]] - /\ pc' = [pc EXCEPT ![self] = "e1"] - /\ UNCHANGED <> - \/ /\ flag' = [flag EXCEPT ![self] = TRUE] - /\ unchecked' = [unchecked EXCEPT ![self] = Procs \ {self}] - /\ max' = [max EXCEPT ![self] = 0] - /\ pc' = [pc EXCEPT ![self] = "e2"] - /\ UNCHANGED << num, nxt, previous >> - -e2(self) == /\ pc[self] = "e2" - /\ IF unchecked[self] # {} - THEN /\ \E i \in unchecked[self]: - /\ unchecked' = [unchecked EXCEPT ![self] = unchecked[self] \ {i}] - /\ IF num[i] > max[self] - THEN /\ max' = [max EXCEPT ![self] = num[i]] - ELSE /\ TRUE - /\ max' = max - /\ pc' = [pc EXCEPT ![self] = "e2"] - ELSE /\ pc' = [pc EXCEPT ![self] = "e3"] - /\ UNCHANGED << unchecked, max >> - /\ UNCHANGED << num, flag, nxt, previous >> - -e3(self) == /\ pc[self] = "e3" - /\ \/ /\ \E k \in Nat: - num' = [num EXCEPT ![self] = k] - /\ pc' = [pc EXCEPT ![self] = "e3"] - \/ /\ num' = [num EXCEPT ![self] = max[self] + 1] - /\ pc' = [pc EXCEPT ![self] = "e4"] - /\ UNCHANGED << flag, unchecked, max, nxt, previous >> - -e4(self) == /\ pc[self] = "e4" - /\ \/ /\ flag' = [flag EXCEPT ![self] = ~ flag[self]] - /\ pc' = [pc EXCEPT ![self] = "e4"] - /\ UNCHANGED unchecked - \/ /\ flag' = [flag EXCEPT ![self] = FALSE] - /\ unchecked' = [unchecked EXCEPT ![self] = IF num[self] = 1 - THEN 1..(self-1) - ELSE Procs \ {self}] - /\ pc' = [pc EXCEPT ![self] = "w1"] - /\ UNCHANGED << num, max, nxt, previous >> - -w1(self) == /\ pc[self] = "w1" - /\ IF unchecked[self] # {} - THEN /\ \E i \in unchecked[self]: - nxt' = [nxt EXCEPT ![self] = i] - /\ ~ flag[nxt'[self]] - /\ previous' = [previous EXCEPT ![self] = -1] - /\ pc' = [pc EXCEPT ![self] = "w2"] - ELSE /\ pc' = [pc EXCEPT ![self] = "cs"] - /\ UNCHANGED << nxt, previous >> - /\ UNCHANGED << num, flag, unchecked, max >> - -w2(self) == /\ pc[self] = "w2" - /\ IF \/ num[nxt[self]] = 0 - \/ <> \prec <> - \/ /\ previous[self] # -1 - /\ num[nxt[self]] # previous[self] - THEN /\ unchecked' = [unchecked EXCEPT ![self] = unchecked[self] \ {nxt[self]}] - /\ IF unchecked'[self] = {} - THEN /\ pc' = [pc EXCEPT ![self] = "cs"] - ELSE /\ pc' = [pc EXCEPT ![self] = "w1"] - /\ UNCHANGED previous - ELSE /\ previous' = [previous EXCEPT ![self] = num[nxt[self]]] - /\ pc' = [pc EXCEPT ![self] = "w2"] - /\ UNCHANGED unchecked - /\ UNCHANGED << num, flag, max, nxt >> - -cs(self) == /\ pc[self] = "cs" - /\ TRUE - /\ pc' = [pc EXCEPT ![self] = "exit"] - /\ UNCHANGED << num, flag, unchecked, max, nxt, previous >> - -exit(self) == /\ pc[self] = "exit" - /\ \/ /\ \E k \in Nat: - num' = [num EXCEPT ![self] = k] - /\ pc' = [pc EXCEPT ![self] = "exit"] - \/ /\ num' = [num EXCEPT ![self] = 0] - /\ pc' = [pc EXCEPT ![self] = "ncs"] - /\ UNCHANGED << flag, unchecked, max, nxt, previous >> - -p(self) == ncs(self) \/ e1(self) \/ e2(self) \/ e3(self) \/ e4(self) - \/ w1(self) \/ w2(self) \/ cs(self) \/ exit(self) - -Next == (\E self \in Procs: p(self)) - -Spec == /\ Init /\ [][Next]_vars - /\ \A self \in Procs : WF_vars((pc[self] # "ncs") /\ p(self)) - -\* END TRANSLATION (this ends the translation of the PlusCal code) - -(***************************************************************************) -(* MutualExclusion asserts that two distinct processes are in their *) -(* critical sections. *) -(***************************************************************************) -MutualExclusion == \A i,j \in Procs : (i # j) => ~ /\ pc[i] = "cs" - /\ pc[j] = "cs" ------------------------------------------------------------------------------ -(***************************************************************************) -(* The Inductive Invariant *) -(* *) -(* TypeOK is the type-correctness invariant. *) -(***************************************************************************) -TypeOK == /\ num \in [Procs -> Nat] - /\ flag \in [Procs -> BOOLEAN] - /\ unchecked \in [Procs -> SUBSET Procs] - /\ max \in [Procs -> Nat] - /\ nxt \in [Procs -> Procs] - /\ pc \in [Procs -> {"ncs", "e1", "e2", "e3", - "e4", "w1", "w2", "cs", "exit"}] - /\ previous \in [Procs -> Nat \cup {-1}] - -(***************************************************************************) -(* Before(i, j) is a condition that implies that num[i] > 0 and, if j is *) -(* trying to enter its critical section and i does not change num[i], then *) -(* j either has or will choose a value of num[j] for which *) -(* *) -(* <> \prec <> *) -(* *) -(* is true. *) -(***************************************************************************) -Before(i,j) == /\ num[i] > 0 - /\ \/ pc[j] \in {"ncs", "e1", "exit"} - \/ /\ pc[j] = "e2" - /\ \/ i \in unchecked[j] - \/ max[j] >= num[i] - \/ (j > i) /\ (max[j] + 1 = num[i]) - \/ /\ pc[j] = "e3" - /\ \/ max[j] >= num[i] - \/ (j > i) /\ (max[j] + 1 = num[i]) - \/ /\ pc[j] \in {"e4", "w1", "w2"} - /\ <> \prec <> - /\ (pc[j] \in {"w1", "w2"}) => (i \in unchecked[j]) - \/ /\ num[i] = 1 - /\ i < j - -(***************************************************************************) -(* Inv is the complete inductive invariant. *) -(***************************************************************************) -Inv == /\ TypeOK - /\ \A i \in Procs : - /\ (pc[i] \in {"ncs", "e1", "e2"}) => (num[i] = 0) - /\ (pc[i] \in {"e4", "w1", "w2", "cs"}) => (num[i] # 0) - /\ (pc[i] \in {"e2", "e3"}) => flag[i] - /\ (pc[i] = "w2") => (nxt[i] # i) - /\ (pc[i] \in {"e2", "w1", "w2"}) => i \notin unchecked[i] - /\ (pc[i] \in {"w1", "w2"}) => - \A j \in (Procs \ unchecked[i]) \ {i} : Before(i, j) - /\ /\ pc[i] = "w2" - /\ \/ (pc[nxt[i]] = "e2") /\ (i \notin unchecked[nxt[i]]) - \/ pc[nxt[i]] = "e3" - => max[nxt[i]] >= num[i] - /\ /\ pc[i] = "w2" - /\ previous[i] # -1 - /\ previous[i] # num[nxt[i]] - /\ pc[nxt[i]] \in {"e4", "w1", "w2", "cs"} - => Before(i, nxt[i]) - /\ (pc[i] = "cs") => \A j \in Procs \ {i} : Before(i, j) ------------------------------------------------------------------------------ -(***************************************************************************) -(* Proof of Mutual Exclusion *) -(* *) -(* This is a standard invariance proof, where <1>2 asserts that any step *) -(* of the algorithm (including a stuttering step) starting in a state in *) -(* which Inv is true leaves Inv true. Step <1>4 follows easily from *) -(* <1>1-<1>3 by simple temporal reasoning, checked by the PTL *) -(* (Propositional Temporal Logic) backend prover. *) -(***************************************************************************) -THEOREM Spec => []MutualExclusion -<1> USE N \in Nat DEFS Procs, TypeOK, Before, \prec, ProcSet - -<1>1. Init => Inv - BY SMT DEF Init, Inv - -<1>2. Inv /\ [Next]_vars => Inv' - <2> SUFFICES ASSUME Inv, - [Next]_vars - PROVE Inv' - OBVIOUS - <2>1. ASSUME NEW self \in Procs, - ncs(self) - PROVE Inv' - BY <2>1, Z3 DEF ncs, Inv - <2>2. ASSUME NEW self \in Procs, - e1(self) - PROVE Inv' - <3>. /\ pc[self] = "e1" - /\ UNCHANGED << num, nxt, previous >> - BY <2>2 DEF e1 - <3>1. CASE /\ flag' = [flag EXCEPT ![self] = ~ flag[self]] - /\ pc' = [pc EXCEPT ![self] = "e1"] - /\ UNCHANGED <> - BY <3>1 DEF Inv - <3>2. CASE /\ flag' = [flag EXCEPT ![self] = TRUE] - /\ unchecked' = [unchecked EXCEPT ![self] = Procs \ {self}] - /\ max' = [max EXCEPT ![self] = 0] - /\ pc' = [pc EXCEPT ![self] = "e2"] - BY <3>2 DEF Inv - <3>. QED BY <3>1, <3>2, <2>2 DEF e1 - <2>3. ASSUME NEW self \in Procs, - e2(self) - PROVE Inv' - <3>. /\ pc[self] = "e2" - /\ UNCHANGED << num, flag, nxt, previous >> - BY <2>3 DEF e2 - <3>1. ASSUME NEW i \in unchecked[self], - unchecked' = [unchecked EXCEPT ![self] = unchecked[self] \ {i}], - num[i] > max[self], - max' = [max EXCEPT ![self] = num[i]], - pc' = [pc EXCEPT ![self] = "e2"] - PROVE Inv' - BY <3>1, Z3 DEF Inv - <3>2. ASSUME NEW i \in unchecked[self], - unchecked' = [unchecked EXCEPT ![self] = unchecked[self] \ {i}], - ~(num[i] > max[self]), - max' = max, - pc' = [pc EXCEPT ![self] = "e2"] - PROVE Inv' - BY <3>2, Z3 DEF Inv - <3>3. CASE /\ unchecked[self] = {} - /\ pc' = [pc EXCEPT ![self] = "e3"] - /\ UNCHANGED << unchecked, max >> - BY <3>3, Z3 DEF Inv - <3>. QED BY <3>1, <3>2, <3>3, <2>3 DEF e2 - <2>4. ASSUME NEW self \in Procs, - e3(self) - PROVE Inv' - <3>. /\ pc[self] = "e3" - /\ UNCHANGED << flag, unchecked, max, nxt, previous >> - BY <2>4 DEF e3 - <3>1. CASE /\ \E k \in Nat: num' = [num EXCEPT ![self] = k] - /\ pc' = [pc EXCEPT ![self] = "e3"] - BY <3>1, Z3 DEF Inv - <3>2. CASE /\ num' = [num EXCEPT ![self] = max[self] + 1] - /\ pc' = [pc EXCEPT ![self] = "e4"] - BY <3>2, Z3 DEF Inv - <3>. QED BY <3>1, <3>2, <2>4 DEF e3 - <2>5. ASSUME NEW self \in Procs, - e4(self) - PROVE Inv' - <3>. /\ pc[self] = "e4" - /\ UNCHANGED << num, max, nxt, previous >> - BY <2>5 DEF e4 - <3>1. CASE /\ flag' = [flag EXCEPT ![self] = ~ flag[self]] - /\ pc' = [pc EXCEPT ![self] = "e4"] - /\ UNCHANGED unchecked - BY <3>1, Z3 DEF Inv - <3>2. CASE /\ flag' = [flag EXCEPT ![self] = FALSE] - /\ num[self] = 1 - /\ unchecked' = [unchecked EXCEPT ![self] = 1..(self-1)] - /\ pc' = [pc EXCEPT ![self] = "w1"] - BY <3>2, Z3 DEF Inv - <3>3. CASE /\ flag' = [flag EXCEPT ![self] = FALSE] - /\ num[self] # 1 - /\ unchecked' = [unchecked EXCEPT ![self] = Procs \ {self}] - /\ pc' = [pc EXCEPT ![self] = "w1"] - BY <3>3, Z3 DEF Inv - <3>. QED BY <3>1, <3>2, <3>3, <2>5 DEF e4 - <2>6. ASSUME NEW self \in Procs, - w1(self) - PROVE Inv' - <3>. /\ pc[self] = "w1" - /\ UNCHANGED << num, flag, unchecked, max >> - BY <2>6 DEF w1 - <3>1. CASE /\ unchecked[self] # {} - /\ \E i \in unchecked[self]: - nxt' = [nxt EXCEPT ![self] = i] - /\ ~ flag[nxt'[self]] - /\ previous' = [previous EXCEPT ![self] = -1] - /\ pc' = [pc EXCEPT ![self] = "w2"] - BY <3>1, Z3 DEF Inv - <3>2. CASE /\ unchecked[self] = {} - /\ pc' = [pc EXCEPT ![self] = "cs"] - /\ UNCHANGED << nxt, previous >> - BY <3>2, Z3 DEF Inv - <3>. QED BY <3>1, <3>2, <2>6 DEF w1 - <2>7. ASSUME NEW self \in Procs, - w2(self) - PROVE Inv' - <3>. /\ pc[self] = "w2" - /\ UNCHANGED << num, flag, max, nxt >> - BY <2>7 DEF w2 - <3>1. CASE /\ \/ num[nxt[self]] = 0 - \/ <> \prec <> - \/ /\ previous[self] # -1 - /\ num[nxt[self]] # previous[self] - /\ unchecked' = [unchecked EXCEPT ![self] = unchecked[self] \ {nxt[self]}] - /\ unchecked'[self] = {} - /\ pc' = [pc EXCEPT ![self] = "cs"] - /\ UNCHANGED previous - BY <3>1, Z3 DEF Inv - <3>2. CASE /\ \/ num[nxt[self]] = 0 - \/ <> \prec <> - \/ /\ previous[self] # -1 - /\ num[nxt[self]] # previous[self] - /\ unchecked' = [unchecked EXCEPT ![self] = unchecked[self] \ {nxt[self]}] - /\ unchecked'[self] # {} - /\ pc' = [pc EXCEPT ![self] = "w1"] - /\ UNCHANGED previous - BY <3>2, Z3 DEF Inv - <3>3. CASE /\ ~ \/ num[nxt[self]] = 0 - \/ <> \prec <> - \/ /\ previous[self] # -1 - /\ num[nxt[self]] # previous[self] - /\ previous' = [previous EXCEPT ![self] = num[nxt[self]]] - /\ pc' = [pc EXCEPT ![self] = "w2"] - /\ UNCHANGED unchecked - BY <3>3, Z3 DEF Inv - <3>. QED BY <3>1, <3>2, <3>3, <2>7 DEF w2 - <2>8. ASSUME NEW self \in Procs, - cs(self) - PROVE Inv' - BY <2>8, Z3 DEF cs, Inv - <2>9. ASSUME NEW self \in Procs, - exit(self) - PROVE Inv' - <3>. /\ pc[self] = "exit" - /\ UNCHANGED << flag, unchecked, max, nxt, previous >> - BY <2>9 DEF exit - <3>1. CASE /\ \E k \in Nat: num' = [num EXCEPT ![self] = k] - /\ pc' = [pc EXCEPT ![self] = "exit"] - BY <3>1, Z3 DEF Inv - <3>2. CASE /\ num' = [num EXCEPT ![self] = 0] - /\ pc' = [pc EXCEPT ![self] = "ncs"] - BY <3>2, Z3 DEF Inv - <3>. QED BY <3>1, <3>2, <2>9 DEF exit - <2>10. CASE UNCHANGED vars - BY <2>10, Z3 DEF vars, Inv - <2>11. QED - BY <2>1, <2>10, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7, <2>8, <2>9 DEF Next, p - -<1>3. Inv => MutualExclusion - BY SMT DEF Inv, MutualExclusion - -<1>4. QED - BY <1>1, <1>2, <1>3, PTL DEF Spec ------------------------------------------------------------------------------- -Trying(i) == pc[i] = "e1" -InCS(i) == pc[i] = "cs" -DeadlockFree == (\E i \in Procs : Trying(i)) ~> (\E i \in Procs : InCS(i)) -StarvationFree == \A i \in Procs : Trying(i) ~> InCS(i) -============================================================================= +------------------------------ MODULE Boulanger ---------------------------- +(***************************************************************************) +(* This is a PlusCal encoding of the Boulangerie Algorithm of Yoram Moses *) +(* and Katia Patkin--a variant of the Bakery Algorithm--and a proof that *) +(* it implements mutual exclusion. The bakery algorithm appeared in *) +(* *) +(* Leslie Lamport *) +(* A New Solution of Dijkstra's Concurrent Programming Problem *) +(* Communications of the ACM 17, 8 (August 1974), 453-455 *) +(* *) +(* The PlusCal encoding differs from the Moses-Patkin algorithm in one *) +(* respect. To enter the critical section, the PlusCal version examines *) +(* other processes one at a time--in the while loop at label w1. The *) +(* Moses-Patkin algorithm performs those examinations in parallel. *) +(* Because PlusCal does not allow sub-processes, it would be difficult *) +(* (but not impossible) to express that algorithm in PlusCal. It would be *) +(* easy to express their version in TLA+ (for example, by modifying the *) +(* TLA+ translation of the PlusCal code), and it should be straightforward *) +(* to convert the invariance proof presented here to a proof of the more *) +(* general version. I will leave that as an exercise for others. *) +(* *) +(* I started with a PlusCal encoding and invariance proof of the Bakery *) +(* Algorithm. The only non-obvious part of that encoding is how it *) +(* represented the safe registers assumed by the algorithm, which are *) +(* registers in which reads and writes are not atomic. A safe register is *) +(* represented by a variable r whose value is written by performing some *) +(* number of atomic writes of non-deterministically chosen "legal" values *) +(* to r followed by a single write of the desired value. A read of the *) +(* register is performed by a single atomic read of r. It can be shown *) +(* that this captures the semantics of a safe register. *) +(* *) +(* Starting from the PlusCal version of the Bakery Algorithm, it was easy *) +(* to modify it to the Boulangerie Algorithm (with the simplification *) +(* described above). I model checked the algorithm on some small models *) +(* to convince myself that there were no trivial errors that would be *) +(* likely to arise from an error in the encoding. I then modified the *) +(* invariant by a combination of a bit of thinking and a fair amount of *) +(* trial and error, finding errors in the invariant by model checking very *) +(* small models. (I checked it on two processes with chosen numbers *) +(* restricted to be at most 3.) *) +(* *) +(* When checking on a small model revealed no error in the invariant, I *) +(* checked the proof with TLAPS (the TLA+ proof system). The high level *) +(* proof, consisting of steps <1>1 - <1>4, are standard and are the same *) +(* as for the Bakery Algorithm. TLAPS checks this simple four-step proof *) +(* for the Bakery Algorithm with terminal BY proofs that just tell it to *) +(* use the necessary assumptions and to expand all definitions. This *) +(* didn't work for the hard part of the Boulangerie Algorithm--step <1>2 *) +(* that checks inductive invariance. *) +(* *) +(* When a proof doesn't go through, one keeps decomposing the proof of the *) +(* steps that aren't proved until one sees what the problem is. This *) +(* decomposition is done with little thinking and no typing using the *) +(* Toolbox's Decompose Proof command. (The Toolbox is the IDE for the *) +(* TLA+ tools.) Step <1>2 has the form A /\ B => C, where B is a *) +(* disjunction, and the Decompose Proof command produces a level-<2> proof *) +(* consisting of subgoals essentially of the form A /\ Bi => C for the *) +(* disjuncts Bi of B. Two of those subgoals weren't proved. I decomposed *) +(* them both for several levels until I saw that in one of them, some step *) +(* wasn't preserving the part of the invariant that asserts *) +(* type-correctness. I then quickly found the culprit: a silly error in *) +(* the type invariant in which I had in one place written the set Proc of *) +(* process numbers instead of the set Nat of natural numbers. After *) +(* correcting that error, only one of the level-<2> subgoals remained *) +(* unproved: step <2>5. Using the Decompose Proof command as far as I *) +(* could on that step, one substep remained unproved. (I think it was at *) +(* level <5>.) Looking at what the proof obligations were, the obvious *) +(* decomposition was a two-way case split, which I did by manually *) +(* entering another level of subproof. One of those cases weren't proved, *) +(* so I tried another two-way case split on it. That worked. I then made *) +(* that substep to the first step of the (level <3>) proof of <2>5, moving *) +(* its proof with it. With that additional fact, TLAPS was able to prove *) +(* <2>5 in one more step (the QED step). *) +(* *) +(* The entire proof now is about 70 lines. I only typed 20 of those 70 *) +(* lines. The rest either came from the original Bakery Algorithm *) +(* (8-line) proof or were generated by the Decompose Proof Command. *) +(* *) +(* I don't know how much time I actually spent writing the algorithm and *) +(* its proof. Except for the final compaction of the (correct) proof of *) +(* <2>5, the entire exercise took me two days. However, most of that was *) +(* spent tracking down bugs in the Toolbox. We are in the process of *) +(* moving the Toolbox to a new version of Eclipse, and there are many bugs *) +(* that must be fixed before it's ready to be released. I would estimate *) +(* that it would have taken me less than 4 hours without Toolbox bugs. I *) +(* find it remarkable how little thinking the whole thing took. *) +(* *) +(* This whole process was a lot easier than trying to write a convincing *) +(* hand proof--a proof that I would regard as adequate to justify *) +(* publication of the proof. *) +(***************************************************************************) + +EXTENDS Integers, TLAPS + +(***************************************************************************) +(* We first declare N to be the number of processes, and we assume that N *) +(* is a natural number. *) +(***************************************************************************) +CONSTANT N +ASSUME N \in Nat + +(***************************************************************************) +(* We define Procs to be the set {1, 2, ... , N} of processes. *) +(***************************************************************************) +Procs == 1..N + +(***************************************************************************) +(* \prec is defined to be the lexicographical less-than relation on pairs *) +(* of numbers. *) +(***************************************************************************) +a \prec b == \/ a[1] < b[1] + \/ (a[1] = b[1]) /\ (a[2] < b[2]) + +(*** this is a comment containing the PlusCal code * + +--algorithm Boulanger +{ variable num = [i \in Procs |-> 0], flag = [i \in Procs |-> FALSE]; + fair process (p \in Procs) + variables unchecked = {}, max = 0, nxt = 1, previous = -1 ; + { ncs:- while (TRUE) + { e1: either { flag[self] := ~ flag[self] ; + goto e1 } + or { flag[self] := TRUE; + unchecked := Procs \ {self} ; + max := 0 + } ; + e2: while (unchecked # {}) + { with (i \in unchecked) + { unchecked := unchecked \ {i}; + if (num[i] > max) { max := num[i] } + } + }; + e3: either { with (k \in Nat) { num[self] := k } ; + goto e3 } + or { num[self] := max + 1 } ; + e4: either { flag[self] := ~ flag[self] ; + goto e4 } + or { flag[self] := FALSE; + unchecked := IF num[self] = 1 + THEN 1..(self-1) + ELSE Procs \ {self} + } ; + w1: while (unchecked # {}) + { with (i \in unchecked) { nxt := i }; + await ~ flag[nxt]; + previous := -1 ; + w2: if ( \/ num[nxt] = 0 + \/ <> \prec <> + \/ /\ previous # -1 + /\ num[nxt] # previous) + { unchecked := unchecked \ {nxt}; + if (unchecked = {}) {goto cs} + else {goto w1} + } + else { previous := num[nxt] ; + goto w2 } + + } ; + cs: skip ; \* the critical section; + exit: either { with (k \in Nat) { num[self] := k } ; + goto exit } + or { num[self] := 0 } + } + } +} + + this ends the comment containing the PlusCal code +*************) + +\* BEGIN TRANSLATION (this begins the translation of the PlusCal code) +VARIABLES num, flag, pc, unchecked, max, nxt, previous + +vars == << num, flag, pc, unchecked, max, nxt, previous >> + +ProcSet == (Procs) + +Init == (* Global variables *) + /\ num = [i \in Procs |-> 0] + /\ flag = [i \in Procs |-> FALSE] + (* Process p *) + /\ unchecked = [self \in Procs |-> {}] + /\ max = [self \in Procs |-> 0] + /\ nxt = [self \in Procs |-> 1] + /\ previous = [self \in Procs |-> -1] + /\ pc = [self \in ProcSet |-> "ncs"] + +ncs(self) == /\ pc[self] = "ncs" + /\ pc' = [pc EXCEPT ![self] = "e1"] + /\ UNCHANGED << num, flag, unchecked, max, nxt, previous >> + +e1(self) == /\ pc[self] = "e1" + /\ \/ /\ flag' = [flag EXCEPT ![self] = ~ flag[self]] + /\ pc' = [pc EXCEPT ![self] = "e1"] + /\ UNCHANGED <> + \/ /\ flag' = [flag EXCEPT ![self] = TRUE] + /\ unchecked' = [unchecked EXCEPT ![self] = Procs \ {self}] + /\ max' = [max EXCEPT ![self] = 0] + /\ pc' = [pc EXCEPT ![self] = "e2"] + /\ UNCHANGED << num, nxt, previous >> + +e2(self) == /\ pc[self] = "e2" + /\ IF unchecked[self] # {} + THEN /\ \E i \in unchecked[self]: + /\ unchecked' = [unchecked EXCEPT ![self] = unchecked[self] \ {i}] + /\ IF num[i] > max[self] + THEN /\ max' = [max EXCEPT ![self] = num[i]] + ELSE /\ TRUE + /\ max' = max + /\ pc' = [pc EXCEPT ![self] = "e2"] + ELSE /\ pc' = [pc EXCEPT ![self] = "e3"] + /\ UNCHANGED << unchecked, max >> + /\ UNCHANGED << num, flag, nxt, previous >> + +e3(self) == /\ pc[self] = "e3" + /\ \/ /\ \E k \in Nat: + num' = [num EXCEPT ![self] = k] + /\ pc' = [pc EXCEPT ![self] = "e3"] + \/ /\ num' = [num EXCEPT ![self] = max[self] + 1] + /\ pc' = [pc EXCEPT ![self] = "e4"] + /\ UNCHANGED << flag, unchecked, max, nxt, previous >> + +e4(self) == /\ pc[self] = "e4" + /\ \/ /\ flag' = [flag EXCEPT ![self] = ~ flag[self]] + /\ pc' = [pc EXCEPT ![self] = "e4"] + /\ UNCHANGED unchecked + \/ /\ flag' = [flag EXCEPT ![self] = FALSE] + /\ unchecked' = [unchecked EXCEPT ![self] = IF num[self] = 1 + THEN 1..(self-1) + ELSE Procs \ {self}] + /\ pc' = [pc EXCEPT ![self] = "w1"] + /\ UNCHANGED << num, max, nxt, previous >> + +w1(self) == /\ pc[self] = "w1" + /\ IF unchecked[self] # {} + THEN /\ \E i \in unchecked[self]: + nxt' = [nxt EXCEPT ![self] = i] + /\ ~ flag[nxt'[self]] + /\ previous' = [previous EXCEPT ![self] = -1] + /\ pc' = [pc EXCEPT ![self] = "w2"] + ELSE /\ pc' = [pc EXCEPT ![self] = "cs"] + /\ UNCHANGED << nxt, previous >> + /\ UNCHANGED << num, flag, unchecked, max >> + +w2(self) == /\ pc[self] = "w2" + /\ IF \/ num[nxt[self]] = 0 + \/ <> \prec <> + \/ /\ previous[self] # -1 + /\ num[nxt[self]] # previous[self] + THEN /\ unchecked' = [unchecked EXCEPT ![self] = unchecked[self] \ {nxt[self]}] + /\ IF unchecked'[self] = {} + THEN /\ pc' = [pc EXCEPT ![self] = "cs"] + ELSE /\ pc' = [pc EXCEPT ![self] = "w1"] + /\ UNCHANGED previous + ELSE /\ previous' = [previous EXCEPT ![self] = num[nxt[self]]] + /\ pc' = [pc EXCEPT ![self] = "w2"] + /\ UNCHANGED unchecked + /\ UNCHANGED << num, flag, max, nxt >> + +cs(self) == /\ pc[self] = "cs" + /\ TRUE + /\ pc' = [pc EXCEPT ![self] = "exit"] + /\ UNCHANGED << num, flag, unchecked, max, nxt, previous >> + +exit(self) == /\ pc[self] = "exit" + /\ \/ /\ \E k \in Nat: + num' = [num EXCEPT ![self] = k] + /\ pc' = [pc EXCEPT ![self] = "exit"] + \/ /\ num' = [num EXCEPT ![self] = 0] + /\ pc' = [pc EXCEPT ![self] = "ncs"] + /\ UNCHANGED << flag, unchecked, max, nxt, previous >> + +p(self) == ncs(self) \/ e1(self) \/ e2(self) \/ e3(self) \/ e4(self) + \/ w1(self) \/ w2(self) \/ cs(self) \/ exit(self) + +Next == (\E self \in Procs: p(self)) + +Spec == /\ Init /\ [][Next]_vars + /\ \A self \in Procs : WF_vars((pc[self] # "ncs") /\ p(self)) + +\* END TRANSLATION (this ends the translation of the PlusCal code) + +(***************************************************************************) +(* MutualExclusion asserts that two distinct processes are in their *) +(* critical sections. *) +(***************************************************************************) +MutualExclusion == \A i,j \in Procs : (i # j) => ~ /\ pc[i] = "cs" + /\ pc[j] = "cs" +----------------------------------------------------------------------------- +(***************************************************************************) +(* The Inductive Invariant *) +(* *) +(* TypeOK is the type-correctness invariant. *) +(***************************************************************************) +TypeOK == /\ num \in [Procs -> Nat] + /\ flag \in [Procs -> BOOLEAN] + /\ unchecked \in [Procs -> SUBSET Procs] + /\ max \in [Procs -> Nat] + /\ nxt \in [Procs -> Procs] + /\ pc \in [Procs -> {"ncs", "e1", "e2", "e3", + "e4", "w1", "w2", "cs", "exit"}] + /\ previous \in [Procs -> Nat \cup {-1}] + +(***************************************************************************) +(* Before(i, j) is a condition that implies that num[i] > 0 and, if j is *) +(* trying to enter its critical section and i does not change num[i], then *) +(* j either has or will choose a value of num[j] for which *) +(* *) +(* <> \prec <> *) +(* *) +(* is true. *) +(***************************************************************************) +Before(i,j) == /\ num[i] > 0 + /\ \/ pc[j] \in {"ncs", "e1", "exit"} + \/ /\ pc[j] = "e2" + /\ \/ i \in unchecked[j] + \/ max[j] >= num[i] + \/ (j > i) /\ (max[j] + 1 = num[i]) + \/ /\ pc[j] = "e3" + /\ \/ max[j] >= num[i] + \/ (j > i) /\ (max[j] + 1 = num[i]) + \/ /\ pc[j] \in {"e4", "w1", "w2"} + /\ <> \prec <> + /\ (pc[j] \in {"w1", "w2"}) => (i \in unchecked[j]) + \/ /\ num[i] = 1 + /\ i < j + +(***************************************************************************) +(* Inv is the complete inductive invariant. *) +(***************************************************************************) +Inv == /\ TypeOK + /\ \A i \in Procs : + /\ (pc[i] \in {"ncs", "e1", "e2"}) => (num[i] = 0) + /\ (pc[i] \in {"e4", "w1", "w2", "cs"}) => (num[i] # 0) + /\ (pc[i] \in {"e2", "e3"}) => flag[i] + /\ (pc[i] = "w2") => (nxt[i] # i) + /\ (pc[i] \in {"e2", "w1", "w2"}) => i \notin unchecked[i] + /\ (pc[i] \in {"w1", "w2"}) => + \A j \in (Procs \ unchecked[i]) \ {i} : Before(i, j) + /\ /\ pc[i] = "w2" + /\ \/ (pc[nxt[i]] = "e2") /\ (i \notin unchecked[nxt[i]]) + \/ pc[nxt[i]] = "e3" + => max[nxt[i]] >= num[i] + /\ /\ pc[i] = "w2" + /\ previous[i] # -1 + /\ previous[i] # num[nxt[i]] + /\ pc[nxt[i]] \in {"e4", "w1", "w2", "cs"} + => Before(i, nxt[i]) + /\ (pc[i] = "cs") => \A j \in Procs \ {i} : Before(i, j) +----------------------------------------------------------------------------- +(***************************************************************************) +(* Proof of Mutual Exclusion *) +(* *) +(* This is a standard invariance proof, where <1>2 asserts that any step *) +(* of the algorithm (including a stuttering step) starting in a state in *) +(* which Inv is true leaves Inv true. Step <1>4 follows easily from *) +(* <1>1-<1>3 by simple temporal reasoning, checked by the PTL *) +(* (Propositional Temporal Logic) backend prover. *) +(***************************************************************************) +THEOREM Spec => []MutualExclusion +<1> USE N \in Nat DEFS Procs, TypeOK, Before, \prec, ProcSet + +<1>1. Init => Inv + BY SMT DEF Init, Inv + +<1>2. Inv /\ [Next]_vars => Inv' + <2> SUFFICES ASSUME Inv, + [Next]_vars + PROVE Inv' + OBVIOUS + <2>1. ASSUME NEW self \in Procs, + ncs(self) + PROVE Inv' + BY <2>1, Z3 DEF ncs, Inv + <2>2. ASSUME NEW self \in Procs, + e1(self) + PROVE Inv' + <3>. /\ pc[self] = "e1" + /\ UNCHANGED << num, nxt, previous >> + BY <2>2 DEF e1 + <3>1. CASE /\ flag' = [flag EXCEPT ![self] = ~ flag[self]] + /\ pc' = [pc EXCEPT ![self] = "e1"] + /\ UNCHANGED <> + BY <3>1 DEF Inv + <3>2. CASE /\ flag' = [flag EXCEPT ![self] = TRUE] + /\ unchecked' = [unchecked EXCEPT ![self] = Procs \ {self}] + /\ max' = [max EXCEPT ![self] = 0] + /\ pc' = [pc EXCEPT ![self] = "e2"] + BY <3>2 DEF Inv + <3>. QED BY <3>1, <3>2, <2>2 DEF e1 + <2>3. ASSUME NEW self \in Procs, + e2(self) + PROVE Inv' + <3>. /\ pc[self] = "e2" + /\ UNCHANGED << num, flag, nxt, previous >> + BY <2>3 DEF e2 + <3>1. ASSUME NEW i \in unchecked[self], + unchecked' = [unchecked EXCEPT ![self] = unchecked[self] \ {i}], + num[i] > max[self], + max' = [max EXCEPT ![self] = num[i]], + pc' = [pc EXCEPT ![self] = "e2"] + PROVE Inv' + BY <3>1, Z3 DEF Inv + <3>2. ASSUME NEW i \in unchecked[self], + unchecked' = [unchecked EXCEPT ![self] = unchecked[self] \ {i}], + ~(num[i] > max[self]), + max' = max, + pc' = [pc EXCEPT ![self] = "e2"] + PROVE Inv' + BY <3>2, Z3 DEF Inv + <3>3. CASE /\ unchecked[self] = {} + /\ pc' = [pc EXCEPT ![self] = "e3"] + /\ UNCHANGED << unchecked, max >> + BY <3>3, Z3 DEF Inv + <3>. QED BY <3>1, <3>2, <3>3, <2>3 DEF e2 + <2>4. ASSUME NEW self \in Procs, + e3(self) + PROVE Inv' + <3>. /\ pc[self] = "e3" + /\ UNCHANGED << flag, unchecked, max, nxt, previous >> + BY <2>4 DEF e3 + <3>1. CASE /\ \E k \in Nat: num' = [num EXCEPT ![self] = k] + /\ pc' = [pc EXCEPT ![self] = "e3"] + BY <3>1, Z3 DEF Inv + <3>2. CASE /\ num' = [num EXCEPT ![self] = max[self] + 1] + /\ pc' = [pc EXCEPT ![self] = "e4"] + BY <3>2, Z3 DEF Inv + <3>. QED BY <3>1, <3>2, <2>4 DEF e3 + <2>5. ASSUME NEW self \in Procs, + e4(self) + PROVE Inv' + <3>. /\ pc[self] = "e4" + /\ UNCHANGED << num, max, nxt, previous >> + BY <2>5 DEF e4 + <3>1. CASE /\ flag' = [flag EXCEPT ![self] = ~ flag[self]] + /\ pc' = [pc EXCEPT ![self] = "e4"] + /\ UNCHANGED unchecked + BY <3>1, Z3 DEF Inv + <3>2. CASE /\ flag' = [flag EXCEPT ![self] = FALSE] + /\ num[self] = 1 + /\ unchecked' = [unchecked EXCEPT ![self] = 1..(self-1)] + /\ pc' = [pc EXCEPT ![self] = "w1"] + BY <3>2, Z3 DEF Inv + <3>3. CASE /\ flag' = [flag EXCEPT ![self] = FALSE] + /\ num[self] # 1 + /\ unchecked' = [unchecked EXCEPT ![self] = Procs \ {self}] + /\ pc' = [pc EXCEPT ![self] = "w1"] + BY <3>3, Z3 DEF Inv + <3>. QED BY <3>1, <3>2, <3>3, <2>5 DEF e4 + <2>6. ASSUME NEW self \in Procs, + w1(self) + PROVE Inv' + <3>. /\ pc[self] = "w1" + /\ UNCHANGED << num, flag, unchecked, max >> + BY <2>6 DEF w1 + <3>1. CASE /\ unchecked[self] # {} + /\ \E i \in unchecked[self]: + nxt' = [nxt EXCEPT ![self] = i] + /\ ~ flag[nxt'[self]] + /\ previous' = [previous EXCEPT ![self] = -1] + /\ pc' = [pc EXCEPT ![self] = "w2"] + BY <3>1, Z3 DEF Inv + <3>2. CASE /\ unchecked[self] = {} + /\ pc' = [pc EXCEPT ![self] = "cs"] + /\ UNCHANGED << nxt, previous >> + BY <3>2, Z3 DEF Inv + <3>. QED BY <3>1, <3>2, <2>6 DEF w1 + <2>7. ASSUME NEW self \in Procs, + w2(self) + PROVE Inv' + <3>. /\ pc[self] = "w2" + /\ UNCHANGED << num, flag, max, nxt >> + BY <2>7 DEF w2 + <3>1. CASE /\ \/ num[nxt[self]] = 0 + \/ <> \prec <> + \/ /\ previous[self] # -1 + /\ num[nxt[self]] # previous[self] + /\ unchecked' = [unchecked EXCEPT ![self] = unchecked[self] \ {nxt[self]}] + /\ unchecked'[self] = {} + /\ pc' = [pc EXCEPT ![self] = "cs"] + /\ UNCHANGED previous + BY <3>1, Z3 DEF Inv + <3>2. CASE /\ \/ num[nxt[self]] = 0 + \/ <> \prec <> + \/ /\ previous[self] # -1 + /\ num[nxt[self]] # previous[self] + /\ unchecked' = [unchecked EXCEPT ![self] = unchecked[self] \ {nxt[self]}] + /\ unchecked'[self] # {} + /\ pc' = [pc EXCEPT ![self] = "w1"] + /\ UNCHANGED previous + BY <3>2, Z3 DEF Inv + <3>3. CASE /\ ~ \/ num[nxt[self]] = 0 + \/ <> \prec <> + \/ /\ previous[self] # -1 + /\ num[nxt[self]] # previous[self] + /\ previous' = [previous EXCEPT ![self] = num[nxt[self]]] + /\ pc' = [pc EXCEPT ![self] = "w2"] + /\ UNCHANGED unchecked + BY <3>3, Z3 DEF Inv + <3>. QED BY <3>1, <3>2, <3>3, <2>7 DEF w2 + <2>8. ASSUME NEW self \in Procs, + cs(self) + PROVE Inv' + BY <2>8, Z3 DEF cs, Inv + <2>9. ASSUME NEW self \in Procs, + exit(self) + PROVE Inv' + <3>. /\ pc[self] = "exit" + /\ UNCHANGED << flag, unchecked, max, nxt, previous >> + BY <2>9 DEF exit + <3>1. CASE /\ \E k \in Nat: num' = [num EXCEPT ![self] = k] + /\ pc' = [pc EXCEPT ![self] = "exit"] + BY <3>1, Z3 DEF Inv + <3>2. CASE /\ num' = [num EXCEPT ![self] = 0] + /\ pc' = [pc EXCEPT ![self] = "ncs"] + BY <3>2, Z3 DEF Inv + <3>. QED BY <3>1, <3>2, <2>9 DEF exit + <2>10. CASE UNCHANGED vars + BY <2>10, Z3 DEF vars, Inv + <2>11. QED + BY <2>1, <2>10, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7, <2>8, <2>9 DEF Next, p + +<1>3. Inv => MutualExclusion + BY SMT DEF Inv, MutualExclusion + +<1>4. QED + BY <1>1, <1>2, <1>3, PTL DEF Spec +------------------------------------------------------------------------------ +Trying(i) == pc[i] = "e1" +InCS(i) == pc[i] = "cs" +DeadlockFree == (\E i \in Procs : Trying(i)) ~> (\E i \in Procs : InCS(i)) +StarvationFree == \A i \in Procs : Trying(i) ~> InCS(i) +============================================================================= \* Modification History \* Last modified Tue Aug 27 12:22:38 PDT 2019 by loki \* Last modified Thu May 24 20:03:58 CEST 2018 by merz -\* Last modified Thu May 24 13:49:22 CEST 2018 by merz -\* Last modified Tue Jul 21 17:55:23 PDT 2015 by lamport -\* Created Thu Nov 21 15:54:32 PST 2013 by lamport +\* Last modified Thu May 24 13:49:22 CEST 2018 by merz +\* Last modified Tue Jul 21 17:55:23 PDT 2015 by lamport +\* Created Thu Nov 21 15:54:32 PST 2013 by lamport diff --git a/specifications/Bakery-Boulangerie/MCBakery.tla b/specifications/Bakery-Boulangerie/MCBakery.tla index e0dc8d30..d9f40ecf 100644 --- a/specifications/Bakery-Boulangerie/MCBakery.tla +++ b/specifications/Bakery-Boulangerie/MCBakery.tla @@ -1,5 +1,7 @@ ---------------------------- MODULE MCBakery -------------------------------- EXTENDS Bakery CONSTANT MaxNat +ASSUME MaxNat \in Nat NatOverride == 0 .. MaxNat ============================================================================= + diff --git a/specifications/Bakery-Boulangerie/MCBoulanger.tla b/specifications/Bakery-Boulangerie/MCBoulanger.tla index c2c7e7db..a3c6142d 100644 --- a/specifications/Bakery-Boulangerie/MCBoulanger.tla +++ b/specifications/Bakery-Boulangerie/MCBoulanger.tla @@ -1,6 +1,7 @@ --------------------------- MODULE MCBoulanger ------------------------------ EXTENDS Boulanger CONSTANT MaxNat +ASSUME MaxNat \in Nat NatOverride == 0 .. MaxNat StateConstraint == \A process \in Procs : num[process] < MaxNat ============================================================================= diff --git a/specifications/LoopInvariance/MCBinarySearch.cfg b/specifications/LoopInvariance/MCBinarySearch.cfg new file mode 100644 index 00000000..5b46fac3 --- /dev/null +++ b/specifications/LoopInvariance/MCBinarySearch.cfg @@ -0,0 +1,8 @@ +CONSTANTS + Values = {1,2,3,4,5} + MaxSeqLen = 8 + Seq <- LimitedSeq +INVARIANTS resultCorrect TypeOK Inv +PROPERTY Termination +SPECIFICATION Spec + diff --git a/specifications/LoopInvariance/MCBinarySearch.tla b/specifications/LoopInvariance/MCBinarySearch.tla new file mode 100644 index 00000000..1a1b63dd --- /dev/null +++ b/specifications/LoopInvariance/MCBinarySearch.tla @@ -0,0 +1,7 @@ +--------------------------- MODULE MCBinarySearch --------------------------- +EXTENDS BinarySearch +CONSTANT MaxSeqLen +ASSUME MaxSeqLen \in Nat +LimitedSeq(S) == UNION {[1 .. n -> S] : n \in 1 .. MaxSeqLen} +============================================================================= + diff --git a/specifications/LoopInvariance/MCQuicksort.cfg b/specifications/LoopInvariance/MCQuicksort.cfg new file mode 100644 index 00000000..bd23c2be --- /dev/null +++ b/specifications/LoopInvariance/MCQuicksort.cfg @@ -0,0 +1,8 @@ +CONSTANTS + Values = {1,2,3} + MaxSeqLen = 4 + Seq <- LimitedSeq +INVARIANTS PCorrect TypeOK Inv +PROPERTY Termination +SPECIFICATION Spec + diff --git a/specifications/LoopInvariance/MCQuicksort.tla b/specifications/LoopInvariance/MCQuicksort.tla new file mode 100644 index 00000000..e3f5d31f --- /dev/null +++ b/specifications/LoopInvariance/MCQuicksort.tla @@ -0,0 +1,7 @@ +---------------------------- MODULE MCQuicksort ----------------------------- +EXTENDS Quicksort +CONSTANT MaxSeqLen +ASSUME MaxSeqLen \in Nat +LimitedSeq(S) == UNION {[1 .. n -> S] : n \in 1 .. MaxSeqLen} +============================================================================= + diff --git a/specifications/MisraReachability/Reachable.tla b/specifications/MisraReachability/Reachable.tla index 081cf724..eeeb697e 100644 --- a/specifications/MisraReachability/Reachable.tla +++ b/specifications/MisraReachability/Reachable.tla @@ -1,240 +1,241 @@ ------------------------------ MODULE Reachable ----------------------------- -(***************************************************************************) -(* This module specifies an algorithm for computing the set of nodes in a *) -(* directed graph that are reachable from a given node called Root. The *) -(* algorithm is due to Jayadev Misra. It is, to my knowledge, a new *) -(* variant of a fairly obvious breadth-first search for reachable nodes. *) -(* I find this algorithm interesting because it is easier to implement *) -(* using multiple processors than the obvious algorithm. Module ParReach *) -(* describes such an implementation. You may want to read it after *) -(* reading this module. *) -(* *) -(* Module ReachableProofs contains a TLA+ proof of the algorithm's safety *) -(* property--that is, partial correctness, which means that if the *) -(* algorithm terminates then it produces the correct answer. That proof *) -(* has been checked by TLAPS, the TLA+ proof system. The proof is based *) -(* on ideas from an informal correctness proof by Misra. *) -(* *) -(* In this module, reachability is expressed in terms of the operator *) -(* ReachableFrom, where ReachableFrom(S) is the set of nodes reachable *) -(* from the nodes in the set S of nodes. This operator is defined in *) -(* module Reachability. That module describes a directed graph in terms *) -(* of the constants Nodes and Succ, where Nodes is the set of nodes and *) -(* Succ is a function with domain Nodes such that Succ[m] is the set of *) -(* all nodes n such that there is an edge from m to n. If you are not *) -(* familiar with directed graphs, you should read at least the opening *) -(* comments in module Reachability. *) -(***************************************************************************) -EXTENDS Reachability, Integers, FiniteSets - -CONSTANT Root -ASSUME RootAssump == Root \in Nodes - -(***************************************************************************) -(* Reachable is defined to be the set of notes reachable from Root. The *) -(* purpose of the algorithm is to compute Reachable. *) -(***************************************************************************) -Reachable == ReachableFrom({Root}) ---------------------------------------------------------------------------- -(*************************************************************************** -The obvious algorithm for computing Reachable({Root}) is as follows. -There are two variables which, following Misra, we call `marked' and -vroot. Each variable holds a set of nodes that are reachable from -Root. Initially, marked = {} and vroot = {Root}. While vroot is -non-empty, the obvious algorithm removed an arbitrary node v from -vroot, adds v to `marked', and adds to vroot all nodes in Succ[v] that -are not in `marked'. The algorithm terminates when vroot is empty, -which will eventually be the case if and only if Reachable({Root}) is a -finite set. When it terminates, `marked' equals Reachable({Root}). - -In the obvious algorithm, `marked' and vroot are always disjoint sets of -nodes. Misra's variant differs in that `marked' and vroot are not -necessarily disjoint. While vroot is nonempty, it chooses an arbitrary -node and does the following: - - IF v is not in in `marked' - THEN it performs the same action as the obvious algorithm except: - (1) it doesn't remove v from vroot, and - (2) it adds all nodes in Succ[v] to vroot, not just the ones - not in `marked'. - ELSE it removes v from vroot - - Here is the algorithm's PlusCal code. - - ---fair algorithm Reachable { - variables marked = {}, vroot = {Root}; - { a: while (vroot /= {}) - { with (v \in vroot) - { if (v \notin marked) - { marked := marked \cup {v}; - vroot := vroot \cup Succ[v] } - else { vroot := vroot \ {v} } - } - } - } -} - - -***************************************************************************) - -\* BEGIN TRANSLATION Here is the TLA+ translation of the PlusCal code. -VARIABLES marked, vroot, pc - -\*Reachable == ReachableFrom(marked) (* added for a test *) -vars == << marked, vroot, pc >> - -Init == (* Global variables *) - /\ marked = {} - /\ vroot = {Root} - /\ pc = "a" - -a == /\ pc = "a" - /\ IF vroot /= {} - THEN /\ \E v \in vroot: - IF v \notin marked - THEN /\ marked' = (marked \cup {v}) - /\ vroot' = (vroot \cup Succ[v]) - ELSE /\ vroot' = vroot \ {v} - /\ UNCHANGED marked - /\ pc' = "a" - ELSE /\ pc' = "Done" - /\ UNCHANGED << marked, vroot >> - -Next == a - \/ (* Disjunct to prevent deadlock on termination *) - (pc = "Done" /\ UNCHANGED vars) - -Spec == /\ Init /\ [][Next]_vars - /\ WF_vars(Next) - -Termination == <>(pc = "Done") - -\* END TRANSLATION ----------------------------------------------------------------------------- -(***************************************************************************) -(* Partial correctness is based on the invariance of the following four *) -(* state predicates. I have sketched very informal proofs of their *) -(* invariance, as well of proofs of the the two theorems that assert *) -(* correctness of the algorithm. The module ReachableProofs contains *) -(* rigorous, TLAPS checked TLA+ proofs of all except the last theorem. *) -(* The last theorem asserts termination, which is a liveness property, and *) -(* TLAPS is not yet capable of proving liveness properties. *) -(***************************************************************************) -TypeOK == /\ marked \in SUBSET Nodes - /\ vroot \in SUBSET Nodes - /\ pc \in {"a", "Done"} - /\ (pc = "Done") => (vroot = {}) - (*************************************************************************) - (* The invariance of TypeOK is obvious. (I decided to make the obvious *) - (* fact that pc equals "Done" only if vroot is empty part of the *) - (* type-correctness invariant.) *) - (*************************************************************************) - -Inv1 == /\ TypeOK - /\ \A n \in marked : Succ[n] \subseteq (marked \cup vroot) - (*************************************************************************) - (* The second conjunct of Inv1 is invariant because each element of *) - (* Succ[n] is added to vroot when n is added to `marked', and it remains *) - (* in vroot at least until it's added to `marked'. I made TypeOK a *) - (* conjunct of Inv1 to make Inv1 an inductive invariant, which made the *) - (* TLA+ proof of its invariance a tiny bit easier to read. *) - (*************************************************************************) - -Inv2 == (marked \cup ReachableFrom(vroot)) = ReachableFrom(marked \cup vroot) - (*************************************************************************) - (* Since ReachableFrom(marked \cup vroot) is the union of *) - (* ReachableFrom(marked) and ReachableFrom(vroot), to prove that Inv2 is *) - (* invariant we must show ReachableFrom(marked) is a subset of *) - (* marked \cup ReachabledFrom(vroot). For this, we assume that m is in *) - (* ReachableFrom(marked) and show that it either is in `marked' or is *) - (* reachable from a node in vroot. *) - (* *) - (* Since m is in ReachableFrom(marked), there is a path with nodes *) - (* p_1, p_2, ... , p_j such that p_1 is in `marked' and p_j = m. If *) - (* all the p_i are in `marked', then m is in `marked' and we're done. *) - (* Otherwise, choose i such that p_1, ... , p_i are in `marked', but *) - (* p_(i+1) isn't in `marked'. Then p_(i+1) is in succ[p_i], which by *) - (* Inv1 implies that it's in marked \cup vroot. Since it isn't in *) - (* `marked', it must be in vroot. The path with nodes *) - (* p_(i+1), ... , p_j shows that p_j, which equals m, is in *) - (* ReachableFrom(vroot). This completes the proof that m is in `marked' *) - (* or ReachableFrom(vroot). *) - (*************************************************************************) - -Inv3 == Reachable = marked \cup ReachableFrom(vroot) - (*************************************************************************) - (* For convenience, let R equal marked \cup ReachableFrom(vroot). In *) - (* the initial state, marked = {} and vroot = {Root}, so R equals *) - (* Reachable and Inv3 is true. We have to show that each action `a' *) - (* step leaves R unchanged. There are two cases: *) - (* *) - (* Case1: The `a' step adds an element v of vroot to `marked' and adds *) - (* to vroot the nodes in Succ[v], which are all in ReachableFrom(vroot). *) - (* Since v itself is also in ReachableFrom(vroot), the step leaves R *) - (* unchanged. *) - (* *) - (* Case 2: The `a' step removes from vroot an element v of `marked'. *) - (* Since Inv1 implies that every node in Succ[v] is in vroot, the only *) - (* element that this step removes from ReachableFrom(vroot) is v, which *) - (* the step adds to `marked'. Hence R is unchanged. *) - (*************************************************************************) - -(***************************************************************************) -(* It is straightforward to use TLC to check that Inv1-Inv3 are invariants *) -(* of the algorithm for small graphs. *) -(***************************************************************************) - -(***************************************************************************) -(* Partial correctness of the algorithm means that if it has terminated, *) -(* then `marked' equals Reachable. The algorithm has terminated when pc *) -(* equals "Done", so this theorem asserts partial correctness. *) -(***************************************************************************) -THEOREM Spec => []((pc = "Done") => (marked = Reachable)) - (*************************************************************************) - (* TypeOK implies (pc = "Done") => (vroot = {}). Since, *) - (* ReachableFrom({}) equals {}, Inv3 implies *) - (* (vroot = {}) => (marked = Reachable). Hence the theorem follows from *) - (* the invariance of TypeOK and Inv3. *) - (*************************************************************************) - -(***************************************************************************) -(* The following theorem asserts that if the set of nodes reachable from *) -(* Root is finite, then the algorithm eventually terminates. Of course, *) -(* this liveness property can be true only because Spec implies weak *) -(* fairness of Next, which equals action `a'. *) -(***************************************************************************) -THEOREM ASSUME IsFiniteSet(Reachable) - PROVE Spec => <>(pc = "Done") - (*************************************************************************) - (* To prove the theorem, we assume a behavior satisfies Spec and prove *) - (* that it satisfies <>(pc = "Done"). If pc = "a" and vroot = {}, then *) - (* an `a' step sets pc to "Done". Since invariance of TypeOK implies *) - (* [](pc \in {"a", "Done"}), weak fairness of `a' implies that to prove *) - (* <>(pc = "Done"), it suffices to prove <>(vroot = {}). *) - (* *) - (* We prove <>(root = {}) by contradiction. We assume it's false, which *) - (* means that [](root /= {}) is true, and obtain a contradiction. From *) - (* []TypeOK, we infer that [](root /= {}) implies [](pc = "a"). By weak *) - (* fairness of action `a', [](root /= {}) implies that there are an *) - (* infinite number of `a' steps. The assumption that Reachable is *) - (* finite and []Inv3 imply that `marked' and vroot are always finite. *) - (* Since vroot is always finite and nonempty, from any state there can *) - (* be only a finite number of `a' steps that remove an element from *) - (* vroot until there is an `a' step that adds a new element to `marked'. *) - (* Since there are an infinite number of `a' steps, there must be an *) - (* infinite number of steps that add new elements to `marked'. This is *) - (* impossible because `marked' is a finite set. Hence, we have the *) - (* required contradiction. *) - (*************************************************************************) - - (**************************************************************************) - (* TLC can quickly check these two theorems on models containing a half *) - (* dozen nodes. *) - (**************************************************************************) -============================================================================= +----------------------------- MODULE Reachable ----------------------------- +(***************************************************************************) +(* This module specifies an algorithm for computing the set of nodes in a *) +(* directed graph that are reachable from a given node called Root. The *) +(* algorithm is due to Jayadev Misra. It is, to my knowledge, a new *) +(* variant of a fairly obvious breadth-first search for reachable nodes. *) +(* I find this algorithm interesting because it is easier to implement *) +(* using multiple processors than the obvious algorithm. Module ParReach *) +(* describes such an implementation. You may want to read it after *) +(* reading this module. *) +(* *) +(* Module ReachableProofs contains a TLA+ proof of the algorithm's safety *) +(* property--that is, partial correctness, which means that if the *) +(* algorithm terminates then it produces the correct answer. That proof *) +(* has been checked by TLAPS, the TLA+ proof system. The proof is based *) +(* on ideas from an informal correctness proof by Misra. *) +(* *) +(* In this module, reachability is expressed in terms of the operator *) +(* ReachableFrom, where ReachableFrom(S) is the set of nodes reachable *) +(* from the nodes in the set S of nodes. This operator is defined in *) +(* module Reachability. That module describes a directed graph in terms *) +(* of the constants Nodes and Succ, where Nodes is the set of nodes and *) +(* Succ is a function with domain Nodes such that Succ[m] is the set of *) +(* all nodes n such that there is an edge from m to n. If you are not *) +(* familiar with directed graphs, you should read at least the opening *) +(* comments in module Reachability. *) +(***************************************************************************) +EXTENDS Reachability, Integers, FiniteSets + +CONSTANT Root +ASSUME RootAssump == Root \in Nodes + +(***************************************************************************) +(* Reachable is defined to be the set of notes reachable from Root. The *) +(* purpose of the algorithm is to compute Reachable. *) +(***************************************************************************) +Reachable == ReachableFrom({Root}) +--------------------------------------------------------------------------- +(*************************************************************************** +The obvious algorithm for computing Reachable({Root}) is as follows. +There are two variables which, following Misra, we call `marked' and +vroot. Each variable holds a set of nodes that are reachable from +Root. Initially, marked = {} and vroot = {Root}. While vroot is +non-empty, the obvious algorithm removed an arbitrary node v from +vroot, adds v to `marked', and adds to vroot all nodes in Succ[v] that +are not in `marked'. The algorithm terminates when vroot is empty, +which will eventually be the case if and only if Reachable({Root}) is a +finite set. When it terminates, `marked' equals Reachable({Root}). + +In the obvious algorithm, `marked' and vroot are always disjoint sets of +nodes. Misra's variant differs in that `marked' and vroot are not +necessarily disjoint. While vroot is nonempty, it chooses an arbitrary +node and does the following: + + IF v is not in in `marked' + THEN it performs the same action as the obvious algorithm except: + (1) it doesn't remove v from vroot, and + (2) it adds all nodes in Succ[v] to vroot, not just the ones + not in `marked'. + ELSE it removes v from vroot + + Here is the algorithm's PlusCal code. + + +--fair algorithm Reachable { + variables marked = {}, vroot = {Root}; + { a: while (vroot /= {}) + { with (v \in vroot) + { if (v \notin marked) + { marked := marked \cup {v}; + vroot := vroot \cup Succ[v] } + else { vroot := vroot \ {v} } + } + } + } +} + + +***************************************************************************) + +\* BEGIN TRANSLATION Here is the TLA+ translation of the PlusCal code. +VARIABLES marked, vroot, pc + +\*Reachable == ReachableFrom(marked) (* added for a test *) +vars == << marked, vroot, pc >> + +Init == (* Global variables *) + /\ marked = {} + /\ vroot = {Root} + /\ pc = "a" + +a == /\ pc = "a" + /\ IF vroot /= {} + THEN /\ \E v \in vroot: + IF v \notin marked + THEN /\ marked' = (marked \cup {v}) + /\ vroot' = (vroot \cup Succ[v]) + ELSE /\ vroot' = vroot \ {v} + /\ UNCHANGED marked + /\ pc' = "a" + ELSE /\ pc' = "Done" + /\ UNCHANGED << marked, vroot >> + +Next == a + \/ (* Disjunct to prevent deadlock on termination *) + (pc = "Done" /\ UNCHANGED vars) + +Spec == /\ Init /\ [][Next]_vars + /\ WF_vars(Next) + +Termination == <>(pc = "Done") + +\* END TRANSLATION +---------------------------------------------------------------------------- +(***************************************************************************) +(* Partial correctness is based on the invariance of the following four *) +(* state predicates. I have sketched very informal proofs of their *) +(* invariance, as well of proofs of the the two theorems that assert *) +(* correctness of the algorithm. The module ReachableProofs contains *) +(* rigorous, TLAPS checked TLA+ proofs of all except the last theorem. *) +(* The last theorem asserts termination, which is a liveness property, and *) +(* TLAPS is not yet capable of proving liveness properties. *) +(***************************************************************************) +TypeOK == /\ marked \in SUBSET Nodes + /\ vroot \in SUBSET Nodes + /\ pc \in {"a", "Done"} + /\ (pc = "Done") => (vroot = {}) + (*************************************************************************) + (* The invariance of TypeOK is obvious. (I decided to make the obvious *) + (* fact that pc equals "Done" only if vroot is empty part of the *) + (* type-correctness invariant.) *) + (*************************************************************************) + +Inv1 == /\ TypeOK + /\ \A n \in marked : Succ[n] \subseteq (marked \cup vroot) + (*************************************************************************) + (* The second conjunct of Inv1 is invariant because each element of *) + (* Succ[n] is added to vroot when n is added to `marked', and it remains *) + (* in vroot at least until it's added to `marked'. I made TypeOK a *) + (* conjunct of Inv1 to make Inv1 an inductive invariant, which made the *) + (* TLA+ proof of its invariance a tiny bit easier to read. *) + (*************************************************************************) + +Inv2 == (marked \cup ReachableFrom(vroot)) = ReachableFrom(marked \cup vroot) + (*************************************************************************) + (* Since ReachableFrom(marked \cup vroot) is the union of *) + (* ReachableFrom(marked) and ReachableFrom(vroot), to prove that Inv2 is *) + (* invariant we must show ReachableFrom(marked) is a subset of *) + (* marked \cup ReachabledFrom(vroot). For this, we assume that m is in *) + (* ReachableFrom(marked) and show that it either is in `marked' or is *) + (* reachable from a node in vroot. *) + (* *) + (* Since m is in ReachableFrom(marked), there is a path with nodes *) + (* p_1, p_2, ... , p_j such that p_1 is in `marked' and p_j = m. If *) + (* all the p_i are in `marked', then m is in `marked' and we're done. *) + (* Otherwise, choose i such that p_1, ... , p_i are in `marked', but *) + (* p_(i+1) isn't in `marked'. Then p_(i+1) is in succ[p_i], which by *) + (* Inv1 implies that it's in marked \cup vroot. Since it isn't in *) + (* `marked', it must be in vroot. The path with nodes *) + (* p_(i+1), ... , p_j shows that p_j, which equals m, is in *) + (* ReachableFrom(vroot). This completes the proof that m is in `marked' *) + (* or ReachableFrom(vroot). *) + (*************************************************************************) + +Inv3 == Reachable = marked \cup ReachableFrom(vroot) + (*************************************************************************) + (* For convenience, let R equal marked \cup ReachableFrom(vroot). In *) + (* the initial state, marked = {} and vroot = {Root}, so R equals *) + (* Reachable and Inv3 is true. We have to show that each action `a' *) + (* step leaves R unchanged. There are two cases: *) + (* *) + (* Case1: The `a' step adds an element v of vroot to `marked' and adds *) + (* to vroot the nodes in Succ[v], which are all in ReachableFrom(vroot). *) + (* Since v itself is also in ReachableFrom(vroot), the step leaves R *) + (* unchanged. *) + (* *) + (* Case 2: The `a' step removes from vroot an element v of `marked'. *) + (* Since Inv1 implies that every node in Succ[v] is in vroot, the only *) + (* element that this step removes from ReachableFrom(vroot) is v, which *) + (* the step adds to `marked'. Hence R is unchanged. *) + (*************************************************************************) + +(***************************************************************************) +(* It is straightforward to use TLC to check that Inv1-Inv3 are invariants *) +(* of the algorithm for small graphs. *) +(***************************************************************************) + +(***************************************************************************) +(* Partial correctness of the algorithm means that if it has terminated, *) +(* then `marked' equals Reachable. The algorithm has terminated when pc *) +(* equals "Done", so this theorem asserts partial correctness. *) +(***************************************************************************) +THEOREM Spec => []((pc = "Done") => (marked = Reachable)) + (*************************************************************************) + (* TypeOK implies (pc = "Done") => (vroot = {}). Since, *) + (* ReachableFrom({}) equals {}, Inv3 implies *) + (* (vroot = {}) => (marked = Reachable). Hence the theorem follows from *) + (* the invariance of TypeOK and Inv3. *) + (*************************************************************************) + +(***************************************************************************) +(* The following theorem asserts that if the set of nodes reachable from *) +(* Root is finite, then the algorithm eventually terminates. Of course, *) +(* this liveness property can be true only because Spec implies weak *) +(* fairness of Next, which equals action `a'. *) +(***************************************************************************) +THEOREM ASSUME IsFiniteSet(Reachable) + PROVE Spec => <>(pc = "Done") + (*************************************************************************) + (* To prove the theorem, we assume a behavior satisfies Spec and prove *) + (* that it satisfies <>(pc = "Done"). If pc = "a" and vroot = {}, then *) + (* an `a' step sets pc to "Done". Since invariance of TypeOK implies *) + (* [](pc \in {"a", "Done"}), weak fairness of `a' implies that to prove *) + (* <>(pc = "Done"), it suffices to prove <>(vroot = {}). *) + (* *) + (* We prove <>(root = {}) by contradiction. We assume it's false, which *) + (* means that [](root /= {}) is true, and obtain a contradiction. From *) + (* []TypeOK, we infer that [](root /= {}) implies [](pc = "a"). By weak *) + (* fairness of action `a', [](root /= {}) implies that there are an *) + (* infinite number of `a' steps. The assumption that Reachable is *) + (* finite and []Inv3 imply that `marked' and vroot are always finite. *) + (* Since vroot is always finite and nonempty, from any state there can *) + (* be only a finite number of `a' steps that remove an element from *) + (* vroot until there is an `a' step that adds a new element to `marked'. *) + (* Since there are an infinite number of `a' steps, there must be an *) + (* infinite number of steps that add new elements to `marked'. This is *) + (* impossible because `marked' is a finite set. Hence, we have the *) + (* required contradiction. *) + (*************************************************************************) + + (**************************************************************************) + (* TLC can quickly check these two theorems on models containing a half *) + (* dozen nodes. *) + (**************************************************************************) +============================================================================= \* Modification History -\* Last modified Tue Aug 27 14:46:36 PDT 2019 by loki -\* Last modified Wed Apr 17 12:21:22 PDT 2019 by lamport -\* Created Thu Apr 04 10:11:51 PDT 2019 by lamport - +\* Last modified Tue Aug 27 14:46:36 PDT 2019 by loki +\* Last modified Wed Apr 17 12:21:22 PDT 2019 by lamport +\* Created Thu Apr 04 10:11:51 PDT 2019 by lamport + + diff --git a/specifications/Stones/Stones.tla b/specifications/Stones/Stones.tla index a062951f..2036c26b 100644 --- a/specifications/Stones/Stones.tla +++ b/specifications/Stones/Stones.tla @@ -102,4 +102,3 @@ ASSUME \/ \E p \in Partitions(<< >>, W) : \* Modification History \* Last modified Wed Feb 04 16:44:37 PST 2015 by lamport \* Created Wed Feb 04 13:33:09 PST 2015 by lamport - diff --git a/specifications/TeachingConcurrency/Simple.tla b/specifications/TeachingConcurrency/Simple.tla index 2904da2a..77361ee6 100644 --- a/specifications/TeachingConcurrency/Simple.tla +++ b/specifications/TeachingConcurrency/Simple.tla @@ -1,160 +1,159 @@ ------------------------------- MODULE Simple ------------------------------ -(***************************************************************************) -(* This is a trivial example from the document "Teaching Conccurrency" *) -(* that appeared in *) -(* *) -(* ACM SIGACT News Volume 40, Issue 1 (March 2009), 58-62 *) -(* *) -(* A copy of that article is at *) -(* *) -(* http://lamport.azurewebsites.net/pubs/teaching-concurrency.pdf *) -(* *) -(* It is also the example in Section 7.2 of "Proving Safety Properties", *) -(* which is at *) -(* *) -(* http://lamport.azurewebsites.net/tla/proving-safety.pdf *) -(***************************************************************************) -EXTENDS Integers, TLAPS - -CONSTANT N -ASSUME NAssump == (N \in Nat) /\ (N > 0) - -(**************************************************************************** -Here is the algorithm in PlusCal. It's easy to understand if you think -of the N processes, numbered from 0 through N-1, as arranged in a -circle, with processes (i-1) % N and (i+1) % N being the processes on -either side of process i. - ---algorithm Simple { - variables x = [i \in 0..(N-1) |-> 0], y = [i \in 0..(N-1) |-> 0] ; - process (proc \in 0..N-1) { - a: x[self] := 1 ; - b: y[self] := x[(self-1) % N] - } -} -****************************************************************************) -\* BEGIN TRANSLATION This is the TLA+ translation of the PlusCal code. -VARIABLES x, y, pc - -vars == << x, y, pc >> - -ProcSet == (0..N-1) - -Init == (* Global variables *) - /\ x = [i \in 0..(N-1) |-> 0] - /\ y = [i \in 0..(N-1) |-> 0] - /\ pc = [self \in ProcSet |-> "a"] - -a(self) == /\ pc[self] = "a" - /\ x' = [x EXCEPT ![self] = 1] - /\ pc' = [pc EXCEPT ![self] = "b"] - /\ y' = y - -b(self) == /\ pc[self] = "b" - /\ y' = [y EXCEPT ![self] = x[(self-1) % N]] - /\ pc' = [pc EXCEPT ![self] = "Done"] - /\ x' = x - -proc(self) == a(self) \/ b(self) - -Next == (\E self \in 0..N-1: proc(self)) - \/ (* Disjunct to prevent deadlock on termination *) - ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars) - -Spec == Init /\ [][Next]_vars - -Termination == <>(\A self \in ProcSet: pc[self] = "Done") - -\* END TRANSLATION ----------------------------------------------------------------------------- -(***************************************************************************) -(* The property of this algorithm we want to prove is that, when all the *) -(* processes have terminated, y[i] equals 1 for at least one process i. *) -(* This property is express by the invariance of the following formula *) -(* PCorrect. In other words, we have to prove the theorem *) -(* *) -(* Spec => []PCorrect *) -(***************************************************************************) -PCorrect == (\A i \in 0..(N-1) : pc[i] = "Done") => - (\E i \in 0..(N-1) : y[i] = 1) - -(***************************************************************************) -(* Proving the invariance of PCorrect requires finding an inductive *) -(* invariant Inv that implies it. As usual, the inductive invariant *) -(* includes a type-correctness invariant, which is the following formula *) -(* TypeOK. *) -(***************************************************************************) -TypeOK == /\ x \in [0..(N-1) -> {0,1}] - /\ y \in [0..(N-1) -> {0,1}] - /\ pc \in [0..(N-1) -> {"a", "b", "Done"}] - -(***************************************************************************) -(* It's easy to use TLC to check that the following formula Inv is an *) -(* inductive invariant of the algorithm. You should also be able check *) -(* that the propositional logic tautology *) -(* *) -(* (A => B) = ((~A) \/ B) *) -(* *) -(* and the predicate logic tautology *) -(* *) -(* (~ \A i \in S : P(i)) = \E i \in S : ~P(i) *) -(* *) -(* imply that the last conjunct of Inv is equivalet to PCorrect. When I *) -(* wrote the definition, I knew that this conjunct of Inv implied *) -(* PCorrect, but I didn't realize that the two were equivalent until I saw *) -(* the invariant written in terms of PCorrect in a paper by Yuri Abraham. *) -(* That's why I originally didn't define Inv in terms of PCorrect. I'm *) -(* not sure why, but I find the implication to be a more natural way to *) -(* write the postcondition PCorrect and the disjunction to be a more *) -(* natural way to think about the inductive invariant. *) -(***************************************************************************) -Inv == /\ TypeOK - /\ \A i \in 0..(N-1) : (pc[i] \in {"b", "Done"}) => (x[i] = 1) - /\ \/ \E i \in 0..(N-1) : pc[i] /= "Done" - \/ \E i \in 0..(N-1) : y[i] = 1 - - -(***************************************************************************) -(* Here is the proof of correctness. The top-level steps <1>1 - <1>4 are *) -(* the standard ones for an invariance proof, and the decomposition of the *) -(* proof of <1>2 was done with the Toolbox's Decompose Proof command. It *) -(* was trivial to get TLAPS to check the proof, except for the proof of *) -(* <2>2. A comment explains the problem I had with that step. *) -(***************************************************************************) -THEOREM Spec => []PCorrect -<1> USE NAssump -<1>1. Init => Inv - BY DEF Init, Inv, TypeOK, ProcSet -<1>2. Inv /\ [Next]_vars => Inv' +------------------------------ MODULE Simple ------------------------------ +(***************************************************************************) +(* This is a trivial example from the document "Teaching Conccurrency" *) +(* that appeared in *) +(* *) +(* ACM SIGACT News Volume 40, Issue 1 (March 2009), 58-62 *) +(* *) +(* A copy of that article is at *) +(* *) +(* http://lamport.azurewebsites.net/pubs/teaching-concurrency.pdf *) +(* *) +(* It is also the example in Section 7.2 of "Proving Safety Properties", *) +(* which is at *) +(* *) +(* http://lamport.azurewebsites.net/tla/proving-safety.pdf *) +(***************************************************************************) +EXTENDS Integers, TLAPS + +CONSTANT N +ASSUME NAssump == (N \in Nat) /\ (N > 0) + +(**************************************************************************** +Here is the algorithm in PlusCal. It's easy to understand if you think +of the N processes, numbered from 0 through N-1, as arranged in a +circle, with processes (i-1) % N and (i+1) % N being the processes on +either side of process i. + +--algorithm Simple { + variables x = [i \in 0..(N-1) |-> 0], y = [i \in 0..(N-1) |-> 0] ; + process (proc \in 0..N-1) { + a: x[self] := 1 ; + b: y[self] := x[(self-1) % N] + } +} +****************************************************************************) +\* BEGIN TRANSLATION This is the TLA+ translation of the PlusCal code. +VARIABLES x, y, pc + +vars == << x, y, pc >> + +ProcSet == (0..N-1) + +Init == (* Global variables *) + /\ x = [i \in 0..(N-1) |-> 0] + /\ y = [i \in 0..(N-1) |-> 0] + /\ pc = [self \in ProcSet |-> "a"] + +a(self) == /\ pc[self] = "a" + /\ x' = [x EXCEPT ![self] = 1] + /\ pc' = [pc EXCEPT ![self] = "b"] + /\ y' = y + +b(self) == /\ pc[self] = "b" + /\ y' = [y EXCEPT ![self] = x[(self-1) % N]] + /\ pc' = [pc EXCEPT ![self] = "Done"] + /\ x' = x + +proc(self) == a(self) \/ b(self) + +Next == (\E self \in 0..N-1: proc(self)) + \/ (* Disjunct to prevent deadlock on termination *) + ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars) + +Spec == Init /\ [][Next]_vars + +Termination == <>(\A self \in ProcSet: pc[self] = "Done") + +\* END TRANSLATION +---------------------------------------------------------------------------- +(***************************************************************************) +(* The property of this algorithm we want to prove is that, when all the *) +(* processes have terminated, y[i] equals 1 for at least one process i. *) +(* This property is express by the invariance of the following formula *) +(* PCorrect. In other words, we have to prove the theorem *) +(* *) +(* Spec => []PCorrect *) +(***************************************************************************) +PCorrect == (\A i \in 0..(N-1) : pc[i] = "Done") => + (\E i \in 0..(N-1) : y[i] = 1) + +(***************************************************************************) +(* Proving the invariance of PCorrect requires finding an inductive *) +(* invariant Inv that implies it. As usual, the inductive invariant *) +(* includes a type-correctness invariant, which is the following formula *) +(* TypeOK. *) +(***************************************************************************) +TypeOK == /\ x \in [0..(N-1) -> {0,1}] + /\ y \in [0..(N-1) -> {0,1}] + /\ pc \in [0..(N-1) -> {"a", "b", "Done"}] + +(***************************************************************************) +(* It's easy to use TLC to check that the following formula Inv is an *) +(* inductive invariant of the algorithm. You should also be able check *) +(* that the propositional logic tautology *) +(* *) +(* (A => B) = ((~A) \/ B) *) +(* *) +(* and the predicate logic tautology *) +(* *) +(* (~ \A i \in S : P(i)) = \E i \in S : ~P(i) *) +(* *) +(* imply that the last conjunct of Inv is equivalet to PCorrect. When I *) +(* wrote the definition, I knew that this conjunct of Inv implied *) +(* PCorrect, but I didn't realize that the two were equivalent until I saw *) +(* the invariant written in terms of PCorrect in a paper by Yuri Abraham. *) +(* That's why I originally didn't define Inv in terms of PCorrect. I'm *) +(* not sure why, but I find the implication to be a more natural way to *) +(* write the postcondition PCorrect and the disjunction to be a more *) +(* natural way to think about the inductive invariant. *) +(***************************************************************************) +Inv == /\ TypeOK + /\ \A i \in 0..(N-1) : (pc[i] \in {"b", "Done"}) => (x[i] = 1) + /\ \/ \E i \in 0..(N-1) : pc[i] /= "Done" + \/ \E i \in 0..(N-1) : y[i] = 1 + + +(***************************************************************************) +(* Here is the proof of correctness. The top-level steps <1>1 - <1>4 are *) +(* the standard ones for an invariance proof, and the decomposition of the *) +(* proof of <1>2 was done with the Toolbox's Decompose Proof command. It *) +(* was trivial to get TLAPS to check the proof, except for the proof of *) +(* <2>2. A comment explains the problem I had with that step. *) +(***************************************************************************) +THEOREM Spec => []PCorrect +<1> USE NAssump +<1>1. Init => Inv + BY DEF Init, Inv, TypeOK, ProcSet +<1>2. Inv /\ [Next]_vars => Inv' <2> SUFFICES ASSUME Inv, [Next]_vars PROVE Inv' OBVIOUS <2>1. ASSUME NEW self \in 0..(N-1), a(self) - PROVE Inv' - BY <2>1 DEF a, Inv, TypeOK + PROVE Inv' + BY <2>1 DEF a, Inv, TypeOK <2>2. ASSUME NEW self \in 0..(N-1), b(self) - PROVE Inv' - (***********************************************************************) - (* I spent a lot of time decomposing this step down to about level <5> *) - (* until I realized that the problem was that the default SMT solver *) - (* in the version of TLAPS I was using was CVC3, which seems to know *) - (* nothing about the % operator. When I used Z3, no further *) - (* decomposition was needed. *) - (***********************************************************************) - BY <2>2, Z3 DEF b, Inv, TypeOK - <2>3. CASE UNCHANGED vars + PROVE Inv' + (***********************************************************************) + (* I spent a lot of time decomposing this step down to about level <5> *) + (* until I realized that the problem was that the default SMT solver *) + (* in the version of TLAPS I was using was CVC3, which seems to know *) + (* nothing about the % operator. When I used Z3, no further *) + (* decomposition was needed. *) + (***********************************************************************) + BY <2>2, Z3 DEF b, Inv, TypeOK + <2>3. CASE UNCHANGED vars BY <2>3 DEF TypeOK, Inv, vars <2>4. QED BY <2>1, <2>2, <2>3 DEF Next, proc -<1>3. Inv => PCorrect - BY DEF Inv, TypeOK, PCorrect -<1>4. QED - BY <1>1, <1>2, <1>3, PTL DEF Spec -============================================================================= -\* Modification History -\* Last modified Wed May 15 02:33:18 PDT 2019 by lamport -\* Created Mon Apr 15 16:25:14 PDT 2019 by lamport - +<1>3. Inv => PCorrect + BY DEF Inv, TypeOK, PCorrect +<1>4. QED + BY <1>1, <1>2, <1>3, PTL DEF Spec +============================================================================= +\* Modification History +\* Last modified Wed May 15 02:33:18 PDT 2019 by lamport +\* Created Mon Apr 15 16:25:14 PDT 2019 by lamport