diff --git a/.github/workflows/run.sh b/.github/workflows/run.sh index c224f5cb..ce746754 100755 --- a/.github/workflows/run.sh +++ b/.github/workflows/run.sh @@ -39,8 +39,8 @@ echo Check MCDieHarder $TLC_COMMAND specifications/DieHard/MCDieHarder || (($? == 12)) ## Expect a safety violation echo Check DieHard $TLC_COMMAND specifications/DieHard/DieHard || (($? == 12)) ## Expect a safety violation -echo Check DiningPhilosophers -$TLC_COMMAND specifications/DiningPhilosophers/DiningPhilosophers +echo Check DiningPhilosophersPCal +$TLC_COMMAND specifications/DiningPhilosophers/DiningPhilosophersPCal echo Check TransitiveClosure $TLC_COMMAND specifications/TransitiveClosure/TransitiveClosure echo Check MCEcho diff --git a/README.md b/README.md index 0e4a22cb..e19baadc 100644 --- a/README.md +++ b/README.md @@ -33,7 +33,7 @@ Here is a list of specs included in this repository which are validated by the C | [Boyer-Moore Majority Vote](specifications/Majority) | Stephan Merz | ✔ | ✔ | | ✔ | | | [Proof x+x is Even](specifications/sums_even) | Martin Riener | ✔ | ✔ | | ✔ | | | [The N-Queens Puzzle](specifications/N-Queens) | Stephan Merz | ✔ | | ✔ | ✔ | | -| [The Dining Philosophers Problem](specifications/DiningPhilosophers) | Jeff Hemphill | ✔ | | ✔ | ✔ | ✔ | +| [The Dining Philosophers Problem](specifications/DiningPhilosophers) | Jeff Hemphill, Markus Kuppe | ✔ | ✔ | (✔) | ✔ | ✔ | | [The Car Talk Puzzle](specifications/CarTalkPuzzle) | Leslie Lamport | ✔ | | | ✔ | | | [The Die Hard Problem](specifications/DieHard) | Leslie Lamport | ✔ | ✔ | | ✔ | ✔ | | [The Prisoners & Switches Puzzle](specifications/Prisoners) | Leslie Lamport | ✔ | | | ✔ | | diff --git a/specifications/DiningPhilosophers/APDiningPhilosophers.tla b/specifications/DiningPhilosophers/APDiningPhilosophers.tla index 0f8ac5a7..43161f89 100644 --- a/specifications/DiningPhilosophers/APDiningPhilosophers.tla +++ b/specifications/DiningPhilosophers/APDiningPhilosophers.tla @@ -1,5 +1,5 @@ ---- MODULE APDiningPhilosophers ---- -(* Apalache type annotations for DiningPhilosophers.tla, applied via +(* Apalache type annotations for DiningPhilosophersPCal.tla, applied via INSTANCE so the original spec remains free of tool-specific idiosyncrasies. *) @@ -17,6 +17,6 @@ VARIABLES \* @type: Int -> Bool; hungry -INSTANCE DiningPhilosophers +INSTANCE DiningPhilosophersPCal ==== diff --git a/specifications/DiningPhilosophers/DiningPhilosophers.cfg b/specifications/DiningPhilosophers/DiningPhilosophers.cfg index 836605ab..c1a8d2d7 100644 --- a/specifications/DiningPhilosophers/DiningPhilosophers.cfg +++ b/specifications/DiningPhilosophers/DiningPhilosophers.cfg @@ -1,9 +1,4 @@ -\* Add statements after this line. +CONSTANTS N = 5 SPECIFICATION Spec -CONSTANT - NP = 5 -INVARIANT - TypeOK - ExclusiveAccess -PROPERTY - NobodyStarves +INVARIANT TypeOK NoDeadlock +PROPERTY NoLivelock NoStarvation diff --git a/specifications/DiningPhilosophers/DiningPhilosophers.tla b/specifications/DiningPhilosophers/DiningPhilosophers.tla index 2fbce81f..32bd01b3 100644 --- a/specifications/DiningPhilosophers/DiningPhilosophers.tla +++ b/specifications/DiningPhilosophers/DiningPhilosophers.tla @@ -1,232 +1,95 @@ ----- MODULE DiningPhilosophers ---- +---------------------------- MODULE DiningPhilosophers ---------------------------- -(* -TLA+ / PlusCal implementation of the Dining Philosophers problem. -Based on the exercise given in https://learntla.com/temporal-logic/operators/ +EXTENDS Naturals, FiniteSets -This is an implementation of the Chandy-Misra solution. -https://en.wikipedia.org/wiki/Dining_philosophers_problem#Chandy/Misra_solution +CONSTANT N \* Number of philosophers +ASSUME NIsPosNat == N \in Nat \ {0} -In Dijkstra's original formulation of the problem, philosophers may not speak -to each other and cannot hand forks to each other. +P == 1..N -In the Chandy-Misra formulation, philosophers may hand forks directly to each -other. - -I ran this with alygin's TLA+ extension for VSCode: - https://marketplace.visualstudio.com/items?itemName=alygin.vscode-tlaplus -"> TLA+: Parse module" updates the translated TLA+ to match the PlusCal - 'algorithm' above. -"> TLA+: Check model with TLC" checks the model's correctness. - -You can also use TLA+ Toolbox. You may need to "create a model" and -use the UI to add the invariants and properties at the bottom of this file. -*) - -EXTENDS Integers, TLC - -CONSTANTS - \* Number of philosophers - NP - -ASSUME - /\ NP \in Nat \ {0} +LeftFork(p) == p +RightFork(p) == (p % N) + 1 -(* --algorithm DiningPhilosophers +ASSUME ForksDistinct == \A p \in P : RightFork(p) \in P /\ RightFork(p) # LeftFork(p) +ASSUME ForksCovered == {RightFork(p) : p \in P} = P -variables - forks = [ - fork \in 1..NP |-> [ - \* We start with each fork held by the lowest-number philosopher - \* adjacent to the fork. - holder |-> IF fork = 2 THEN 1 ELSE fork, - \* Each fork starts out "dirty". Eating causes a fork to become - \* dirty, after which the philosopher must clean the fork and hand - \* it to their neighbor. - clean |-> FALSE - ] - ] +VARIABLES philosophers, forks +vars == <> -define - LeftFork(p) == p - RightFork(p) == IF p = NP THEN 1 ELSE p + 1 - - LeftPhilosopher(p) == IF p = 1 THEN NP ELSE p - 1 - RightPhilosopher(p) == IF p = NP THEN 1 ELSE p + 1 - - IsHoldingBothForks(p) == - forks[LeftFork(p)].holder = p /\ forks[RightFork(p)].holder = p - BothForksAreClean(p) == - forks[LeftFork(p)].clean /\ forks[RightFork(p)].clean - - CanEat(p) == IsHoldingBothForks(p) /\ BothForksAreClean(p) -end define; - -\* This spawns 'NP' parallel Philosopher processes. -\* -\* A process looks kind of like an object oriented class, but '\in 1..NP' means -\* it's really just an integer between 1 and NP. Use 'self' to access that -\* integer. -\* -\* If you remove the 'fair' in 'fair process', each process can stop at any -\* time and will never run again. Dining philosophers don't randomly die while -\* clenching forks in the original problem, so let's keep the processes fair. -fair process Philosopher \in 1..NP -\* This acts like a member variable and you can access it like one. But we're -\* actually creating an array with one element per process, and the "member -\* variable" we access is just the corresponding bucket in that array. -variables hungry = TRUE; -begin -Loop: - while TRUE do - \* Check if we're holding dirty forks that other philosophers might - \* want. - if - /\ forks[LeftFork(self)].holder = self - /\ ~forks[LeftFork(self)].clean - then - forks[LeftFork(self)] := [ - holder |-> LeftPhilosopher(self), - clean |-> TRUE - ]; - elsif - /\ forks[RightFork(self)].holder = self - /\ ~forks[RightFork(self)].clean - then - forks[RightFork(self)] := [ - holder |-> RightPhilosopher(self), - clean |-> TRUE - ]; - end if; - if hungry then - if CanEat(self) then -Eat: - hungry := FALSE; - forks[LeftFork(self)].clean := FALSE || - forks[RightFork(self)].clean := FALSE; - end if; - else -Think: - hungry := TRUE; - end if; - end while; -end process; - -end algorithm; *) -\* BEGIN TRANSLATION (chksum(pcal) = "ea877089" /\ chksum(tla) = "16352822") -VARIABLES forks, pc - -(* define statement *) -LeftFork(p) == p -RightFork(p) == IF p = NP THEN 1 ELSE p + 1 - -LeftPhilosopher(p) == IF p = 1 THEN NP ELSE p - 1 -RightPhilosopher(p) == IF p = NP THEN 1 ELSE p + 1 - -IsHoldingBothForks(p) == - forks[LeftFork(p)].holder = p /\ forks[RightFork(p)].holder = p -BothForksAreClean(p) == - forks[LeftFork(p)].clean /\ forks[RightFork(p)].clean - -CanEat(p) == IsHoldingBothForks(p) /\ BothForksAreClean(p) - -VARIABLE hungry - -vars == << forks, pc, hungry >> - -ProcSet == (1..NP) - -Init == (* Global variables *) - /\ forks = [ - fork \in 1..NP |-> [ - - - holder |-> IF fork = 2 THEN 1 ELSE fork, - - - - clean |-> FALSE - ] - ] - (* Process Philosopher *) - /\ hungry = [self \in 1..NP |-> TRUE] - /\ pc = [self \in ProcSet |-> "Loop"] - -Loop(self) == /\ pc[self] = "Loop" - /\ IF /\ forks[LeftFork(self)].holder = self - /\ ~forks[LeftFork(self)].clean - THEN /\ forks' = [forks EXCEPT ![LeftFork(self)] = [ - holder |-> LeftPhilosopher(self), - clean |-> TRUE - ]] - ELSE /\ IF /\ forks[RightFork(self)].holder = self - /\ ~forks[RightFork(self)].clean - THEN /\ forks' = [forks EXCEPT ![RightFork(self)] = [ - holder |-> RightPhilosopher(self), - clean |-> TRUE - ]] - ELSE /\ TRUE - /\ forks' = forks - /\ IF hungry[self] - THEN /\ IF CanEat(self) - THEN /\ pc' = [pc EXCEPT ![self] = "Eat"] - ELSE /\ pc' = [pc EXCEPT ![self] = "Loop"] - ELSE /\ pc' = [pc EXCEPT ![self] = "Think"] - /\ UNCHANGED hungry - -Think(self) == /\ pc[self] = "Think" - /\ hungry' = [hungry EXCEPT ![self] = TRUE] - /\ pc' = [pc EXCEPT ![self] = "Loop"] - /\ forks' = forks - -Eat(self) == /\ pc[self] = "Eat" - /\ hungry' = [hungry EXCEPT ![self] = FALSE] - /\ forks' = [forks EXCEPT ![LeftFork(self)].clean = FALSE, - ![RightFork(self)].clean = FALSE] - /\ pc' = [pc EXCEPT ![self] = "Loop"] - -Philosopher(self) == Loop(self) \/ Think(self) \/ Eat(self) - -Next == (\E self \in 1..NP: Philosopher(self)) - -Spec == /\ Init /\ [][Next]_vars - /\ \A self \in 1..NP : WF_vars(Philosopher(self)) - -\* END TRANSLATION - ----- -(* Invariant helpers *) ----- - -(* TRUE iff philosophers p and q share a fork between them. *) -ShareFork(p, q) == - {LeftFork(p), RightFork(p)} \cap {LeftFork(q), RightFork(q)} /= {} - ----- -(* Invariants *) ----- - -(* -TLA+ and PlusCal are dynamically-typed, but we can roll our own typechecking -with an invariant. -*) TypeOK == - /\ forks \in [1..NP -> [holder: 1..NP, clean: BOOLEAN]] - /\ hungry \in [1..NP -> BOOLEAN] - /\ pc \in [1..NP -> {"Loop", "Eat", "Think"}] - -(* If two philosophers share a fork, they cannot eat at the same time. *) -ExclusiveAccess == - \A p,q \in 1..NP: - p /= q /\ ShareFork(p, q) => ~(pc[p] = "Eat" /\ pc[q] = "Eat") + /\ philosophers \in [P -> SUBSET P] + /\ forks \in SUBSET P + +Init == + \* each philosopher starts with no forks + /\ philosophers = [ p \in P |-> {} ] + \* all forks are available + /\ forks = 1..N + +TakeLeft(p) == + \* Philosopher N grabs the right fork first. + /\ p = N => philosophers[p] = {RightFork(p)} + /\ LeftFork(p) \in forks + /\ forks' = forks \ {LeftFork(p)} + /\ philosophers' = + [philosophers EXCEPT ![p] = philosophers[p] \cup {LeftFork(p)}] + +TakeRight(p) == + \* All other philosophers grab the left fork first. + /\ p # N => philosophers[p] = {LeftFork(p)} + /\ RightFork(p) \in forks + /\ forks' = forks \ {RightFork(p)} + /\ philosophers' = + [philosophers EXCEPT ![p] = philosophers[p] \cup {RightFork(p)}] + +Release(p) == + /\ philosophers[p] = {LeftFork(p), RightFork(p)} + /\ forks' = forks \cup {LeftFork(p), RightFork(p)} + /\ philosophers' = [philosophers EXCEPT ![p] = {}] + +Next == + \E p \in P: + \/ TakeLeft(p) + \/ TakeRight(p) + \/ Release(p) + +Spec == + /\ Init + /\ [][Next]_vars + /\ \A p \in P : + SF_vars(TakeLeft(p) \/ TakeRight(p) \/ Release(p)) + +IsEating(p) == + Cardinality(philosophers[p]) = 2 + +NoDeadlock == + ENABLED Next + +NoLivelock == + []<>(\E p \in P: IsEating(p)) + +NoStarvation == + \A p \in P: []<>IsEating(p) + +\* Proved in DiningPhilosophers_proof. +THEOREM DeadlockFreedom == Spec => []NoDeadlock +THEOREM LivelockFreedom == Spec => NoLivelock +THEOREM StarvationFreedom == Spec => NoStarvation + +----- + +Alias == + LET ThinkHungryEat(p) == + IF IsEating(p) THEN "eating" + ELSE IF Cardinality(philosophers[p]) = 1 THEN "hungry" + ELSE "thinking" IN + [ + philosophers |-> philosophers, + forks |-> forks, + eating |-> [ p \in DOMAIN philosophers |-> ThinkHungryEat(p) ] + ] ----- -(* Properties *) ----- +----------------------------------------------------------------------------- -(* -Every philosopher will eventually get to eat again. -*) -NobodyStarves == \A p \in 1..NP: []<>(~hungry[p]) -==== +===== diff --git a/specifications/DiningPhilosophers/DiningPhilosophersPCal.cfg b/specifications/DiningPhilosophers/DiningPhilosophersPCal.cfg new file mode 100644 index 00000000..836605ab --- /dev/null +++ b/specifications/DiningPhilosophers/DiningPhilosophersPCal.cfg @@ -0,0 +1,9 @@ +\* Add statements after this line. +SPECIFICATION Spec +CONSTANT + NP = 5 +INVARIANT + TypeOK + ExclusiveAccess +PROPERTY + NobodyStarves diff --git a/specifications/DiningPhilosophers/DiningPhilosophersPCal.tla b/specifications/DiningPhilosophers/DiningPhilosophersPCal.tla new file mode 100644 index 00000000..d0caf75b --- /dev/null +++ b/specifications/DiningPhilosophers/DiningPhilosophersPCal.tla @@ -0,0 +1,232 @@ +---- MODULE DiningPhilosophersPCal ---- + +(* +TLA+ / PlusCal implementation of the Dining Philosophers problem. +Based on the exercise given in https://learntla.com/temporal-logic/operators/ + +This is an implementation of the Chandy-Misra solution. +https://en.wikipedia.org/wiki/Dining_philosophers_problem#Chandy/Misra_solution + +In Dijkstra's original formulation of the problem, philosophers may not speak +to each other and cannot hand forks to each other. + +In the Chandy-Misra formulation, philosophers may hand forks directly to each +other. + +I ran this with alygin's TLA+ extension for VSCode: + https://marketplace.visualstudio.com/items?itemName=tlaplus.vscode-ide +"> TLA+: Parse module" updates the translated TLA+ to match the PlusCal + 'algorithm' above. +"> TLA+: Check model with TLC" checks the model's correctness. + +You can also use TLA+ Toolbox. You may need to "create a model" and +use the UI to add the invariants and properties at the bottom of this file. +*) + +EXTENDS Integers, TLC + +CONSTANTS + \* Number of philosophers + NP + +ASSUME + /\ NP \in Nat \ {0} + +(* --algorithm DiningPhilosophers + +variables + forks = [ + fork \in 1..NP |-> [ + \* We start with each fork held by the lowest-number philosopher + \* adjacent to the fork. + holder |-> IF fork = 2 THEN 1 ELSE fork, + \* Each fork starts out "dirty". Eating causes a fork to become + \* dirty, after which the philosopher must clean the fork and hand + \* it to their neighbor. + clean |-> FALSE + ] + ] + +define + LeftFork(p) == p + RightFork(p) == IF p = NP THEN 1 ELSE p + 1 + + LeftPhilosopher(p) == IF p = 1 THEN NP ELSE p - 1 + RightPhilosopher(p) == IF p = NP THEN 1 ELSE p + 1 + + IsHoldingBothForks(p) == + forks[LeftFork(p)].holder = p /\ forks[RightFork(p)].holder = p + BothForksAreClean(p) == + forks[LeftFork(p)].clean /\ forks[RightFork(p)].clean + + CanEat(p) == IsHoldingBothForks(p) /\ BothForksAreClean(p) +end define; + +\* This spawns 'NP' parallel Philosopher processes. +\* +\* A process looks kind of like an object oriented class, but '\in 1..NP' means +\* it's really just an integer between 1 and NP. Use 'self' to access that +\* integer. +\* +\* If you remove the 'fair' in 'fair process', each process can stop at any +\* time and will never run again. Dining philosophers don't randomly die while +\* clenching forks in the original problem, so let's keep the processes fair. +fair process Philosopher \in 1..NP +\* This acts like a member variable and you can access it like one. But we're +\* actually creating an array with one element per process, and the "member +\* variable" we access is just the corresponding bucket in that array. +variables hungry = TRUE; +begin +Loop: + while TRUE do + \* Check if we're holding dirty forks that other philosophers might + \* want. + if + /\ forks[LeftFork(self)].holder = self + /\ ~forks[LeftFork(self)].clean + then + forks[LeftFork(self)] := [ + holder |-> LeftPhilosopher(self), + clean |-> TRUE + ]; + elsif + /\ forks[RightFork(self)].holder = self + /\ ~forks[RightFork(self)].clean + then + forks[RightFork(self)] := [ + holder |-> RightPhilosopher(self), + clean |-> TRUE + ]; + end if; + if hungry then + if CanEat(self) then +Eat: + hungry := FALSE; + forks[LeftFork(self)].clean := FALSE || + forks[RightFork(self)].clean := FALSE; + end if; + else +Think: + hungry := TRUE; + end if; + end while; +end process; + +end algorithm; *) +\* BEGIN TRANSLATION (chksum(pcal) = "ea877089" /\ chksum(tla) = "16352822") +VARIABLES forks, pc + +(* define statement *) +LeftFork(p) == p +RightFork(p) == IF p = NP THEN 1 ELSE p + 1 + +LeftPhilosopher(p) == IF p = 1 THEN NP ELSE p - 1 +RightPhilosopher(p) == IF p = NP THEN 1 ELSE p + 1 + +IsHoldingBothForks(p) == + forks[LeftFork(p)].holder = p /\ forks[RightFork(p)].holder = p +BothForksAreClean(p) == + forks[LeftFork(p)].clean /\ forks[RightFork(p)].clean + +CanEat(p) == IsHoldingBothForks(p) /\ BothForksAreClean(p) + +VARIABLE hungry + +vars == << forks, pc, hungry >> + +ProcSet == (1..NP) + +Init == (* Global variables *) + /\ forks = [ + fork \in 1..NP |-> [ + + + holder |-> IF fork = 2 THEN 1 ELSE fork, + + + + clean |-> FALSE + ] + ] + (* Process Philosopher *) + /\ hungry = [self \in 1..NP |-> TRUE] + /\ pc = [self \in ProcSet |-> "Loop"] + +Loop(self) == /\ pc[self] = "Loop" + /\ IF /\ forks[LeftFork(self)].holder = self + /\ ~forks[LeftFork(self)].clean + THEN /\ forks' = [forks EXCEPT ![LeftFork(self)] = [ + holder |-> LeftPhilosopher(self), + clean |-> TRUE + ]] + ELSE /\ IF /\ forks[RightFork(self)].holder = self + /\ ~forks[RightFork(self)].clean + THEN /\ forks' = [forks EXCEPT ![RightFork(self)] = [ + holder |-> RightPhilosopher(self), + clean |-> TRUE + ]] + ELSE /\ TRUE + /\ forks' = forks + /\ IF hungry[self] + THEN /\ IF CanEat(self) + THEN /\ pc' = [pc EXCEPT ![self] = "Eat"] + ELSE /\ pc' = [pc EXCEPT ![self] = "Loop"] + ELSE /\ pc' = [pc EXCEPT ![self] = "Think"] + /\ UNCHANGED hungry + +Think(self) == /\ pc[self] = "Think" + /\ hungry' = [hungry EXCEPT ![self] = TRUE] + /\ pc' = [pc EXCEPT ![self] = "Loop"] + /\ forks' = forks + +Eat(self) == /\ pc[self] = "Eat" + /\ hungry' = [hungry EXCEPT ![self] = FALSE] + /\ forks' = [forks EXCEPT ![LeftFork(self)].clean = FALSE, + ![RightFork(self)].clean = FALSE] + /\ pc' = [pc EXCEPT ![self] = "Loop"] + +Philosopher(self) == Loop(self) \/ Think(self) \/ Eat(self) + +Next == (\E self \in 1..NP: Philosopher(self)) + +Spec == /\ Init /\ [][Next]_vars + /\ \A self \in 1..NP : WF_vars(Philosopher(self)) + +\* END TRANSLATION + +---- +(* Invariant helpers *) +---- + +(* TRUE iff philosophers p and q share a fork between them. *) +ShareFork(p, q) == + {LeftFork(p), RightFork(p)} \cap {LeftFork(q), RightFork(q)} /= {} + +---- +(* Invariants *) +---- + +(* +TLA+ and PlusCal are dynamically-typed, but we can roll our own typechecking +with an invariant. +*) +TypeOK == + /\ forks \in [1..NP -> [holder: 1..NP, clean: BOOLEAN]] + /\ hungry \in [1..NP -> BOOLEAN] + /\ pc \in [1..NP -> {"Loop", "Eat", "Think"}] + +(* If two philosophers share a fork, they cannot eat at the same time. *) +ExclusiveAccess == + \A p,q \in 1..NP: + p /= q /\ ShareFork(p, q) => ~(pc[p] = "Eat" /\ pc[q] = "Eat") + +---- +(* Properties *) +---- + +(* +Every philosopher will eventually get to eat again. +*) +NobodyStarves == \A p \in 1..NP: []<>(~hungry[p]) + +==== diff --git a/specifications/DiningPhilosophers/DiningPhilosophers_anim.cfg b/specifications/DiningPhilosophers/DiningPhilosophers_anim.cfg new file mode 100644 index 00000000..1a23796b --- /dev/null +++ b/specifications/DiningPhilosophers/DiningPhilosophers_anim.cfg @@ -0,0 +1,6 @@ +CONSTANT + N = 5 +SPECIFICATION + Spec +ALIAS + AnimAlias \ No newline at end of file diff --git a/specifications/DiningPhilosophers/DiningPhilosophers_anim.gif b/specifications/DiningPhilosophers/DiningPhilosophers_anim.gif new file mode 100644 index 00000000..d88a0f83 Binary files /dev/null and b/specifications/DiningPhilosophers/DiningPhilosophers_anim.gif differ diff --git a/specifications/DiningPhilosophers/DiningPhilosophers_anim.tla b/specifications/DiningPhilosophers/DiningPhilosophers_anim.tla new file mode 100644 index 00000000..7dfb34c3 --- /dev/null +++ b/specifications/DiningPhilosophers/DiningPhilosophers_anim.tla @@ -0,0 +1,149 @@ +---- MODULE DiningPhilosophers_anim ---- +EXTENDS TLC, Integers, Sequences, SVG, DiningPhilosophers + +(***************************************************************************) +(* Every seat is drawn once, in the frame of the philosopher at the top of *) +(* the table, and then rotated about the table's center. Philosophers are *) +(* placed counter-clockwise so that, facing the table, LeftFork(p) is at *) +(* p's left hand and RightFork(p) at p's right hand. *) +(***************************************************************************) + +\* Table radius. Plates lie 25 inside the edge and need about 65 between +\* neighbors, so the table grows with N. +R == IF 25 + 11 * N > 80 THEN 25 + 11 * N ELSE 80 + +\* The table's top edge is at y = 70, which all seat coordinates rely on. +Cx == R + 70 +Cy == R + 70 + +\* Angles are in tenths of a degree, in 0..7200 to avoid negative numbers. +SeatAngle(p) == 3600 - (3600 * (p - 1)) \div N +ForkAngle(f) == SeatAngle(f) + 1800 \div N \* Fork f lies between seats f and f-1. + +Deg(t) == ToString(t \div 10) \o "." \o ToString(t % 10) + +RotateAboutCenter(t) == + "rotate(" \o Deg(t) \o " " \o ToString(Cx) \o " " \o ToString(Cy) \o ")" + +\* Undo the rotation of the enclosing seat so that labels stay upright. +Upright(t, x, y) == + "rotate(" \o Deg(7200 - t) \o " " \o ToString(x) \o " " \o ToString(y) \o ")" + +Show(cond, elem) == IF cond THEN <> ELSE <<>> + +Label(x, y, t, str, size, color) == + Text(x, y, str, + ("text-anchor" :> "middle" @@ "font-family" :> "sans-serif" @@ + "font-size" :> ToString(size) @@ "fill" :> color @@ + "transform" :> Upright(t, x, y - size \div 3))) + +ThinkingColor == "#9db4d0" +HungryColor == "#f2a541" +EatingColor == "#5cb85c" + +StateColor(p) == + CASE IsEating(p) -> EatingColor + [] Cardinality(philosophers[p]) = 1 -> HungryColor + [] OTHER -> ThinkingColor + +(***************************************************************************) +(* A fork centered at (x, y), rotated by a degrees. Unrotated, its tines *) +(* point up. *) +(***************************************************************************) +ForkGlyph(x, y, a) == + LET style(w) == ("stroke" :> "#5a5a5a" @@ "stroke-width" :> w @@ + "stroke-linecap" :> "round") + IN Group(<< + Line(0, 2, 0, 14, style("3")), + Line(-4, -2, 4, -2, style("1.5")), + Line(-4, -2, -4, -13, style("1.5")), + Line( 0, -2, 0, -13, style("1.5")), + Line( 4, -2, 4, -13, style("1.5")) + >>, + ("transform" :> "translate(" \o ToString(x) \o " " \o ToString(y) \o + ") rotate(" \o ToString(a) \o ")")) + +Table == + Circle(Cx, Cy, R, ("fill" :> "#deb887" @@ "stroke" :> "#a0764a" @@ + "stroke-width" :> "3")) + +\* A plate in front of philosopher p, with food on it while p eats. +Plate(p) == + Group(<< + Circle(Cx, 95, 15, [fill |-> "white", stroke |-> "#999"]), + Circle(Cx, 95, 10, [fill |-> "none", stroke |-> "#ddd"]) + >> \o + Show(IsEating(p), Circle(Cx, 95, 7, [fill |-> "#e07b39"])), + ("transform" :> RotateAboutCenter(SeatAngle(p)))) + +\* Philosopher p with an arm and a fork for each fork that p holds. +Philosopher(p) == + LET t == SeatAngle(p) + arm(x1, x2) == Line(x1, 52, x2, 62, + ("stroke" :> StateColor(p) @@ "stroke-width" :> "6" @@ + "stroke-linecap" :> "round")) + hand(x) == Circle(x, 61, 4, [fill |-> "#f6d7b0", stroke |-> "#555"]) + left == LeftFork(p) \in philosophers[p] + \* For N = 1, both hands would show the same, only, fork. + right == RightFork(p) \in philosophers[p] /\ RightFork(p) # LeftFork(p) + IN Group( + Show(left, arm(Cx + 10, Cx + 25)) \o + Show(right, arm(Cx - 10, Cx - 25)) \o + << + Rect(Cx - 18, 44, 36, 24, [rx |-> "12", fill |-> StateColor(p), stroke |-> "#555"]), + Circle(Cx, 32, 12, [fill |-> "#f6d7b0", stroke |-> "#555"]), + Label(Cx, 36, t, ToString(p), 12, "#333") + >> \o + \* Held forks point towards the plate. + Show(left, ForkGlyph(Cx + 22, 70, 200)) \o + Show(right, ForkGlyph(Cx - 22, 70, 160)) \o + Show(left, hand(Cx + 25)) \o + Show(right, hand(Cx - 25)), + ("transform" :> RotateAboutCenter(t))) + +\* Fork f on the table; only its number remains while someone holds it. +TableFork(f) == + Group( + Show(f \in forks, ForkGlyph(Cx, 92, 180)) \o + <>, + ("transform" :> RotateAboutCenter(ForkAngle(f)))) + +Legend == + LET x == 2 * Cx + 15 + entry(i, color, str) == + Group(<< + Rect(x, 20 + 22 * i, 14, 14, [rx |-> "4", fill |-> color, stroke |-> "#555"]), + Text(x + 20, 32 + 22 * i, str, + ("font-family" :> "sans-serif" @@ "font-size" :> "11" @@ "fill" :> "#333")) + >>, <<>>) + IN Group(<< + entry(0, ThinkingColor, "thinking"), + entry(1, HungryColor, "hungry (1 fork)"), + entry(2, EatingColor, "eating (2 forks)") + >>, <<>>) + +\* Scale the drawing, in hundredths, to 600 wide, which fits Spectacle's pane. +ViewWidth == 600 +Scale == (100 * ViewWidth) \div (2 * Cx + 130) +ViewHeight == (2 * Cy * Scale) \div 100 + +ScaleStr == + ToString(Scale \div 100) \o "." \o + (IF Scale % 100 < 10 THEN "0" ELSE "") \o ToString(Scale % 100) + +AnimView == + Group(<> \o + [p \in P |-> Plate(p)] \o + [f \in P |-> TableFork(f)] \o + [p \in P |-> Philosopher(p)] \o + <>, + ("transform" :> "scale(" \o ScaleStr \o " " \o ScaleStr \o ")")) + +\* Animation alias for generating SVG files with TLC. +AnimAlias == + [ + philosophers |-> philosophers, forks |-> forks + ] @@ + [ _anim |-> SVGSerialize(SVGDoc(AnimView, 0, 0, ViewWidth, ViewHeight, <<>>), "DiningPhilosophers_anim_", TLCGet("level")) ] + +==== diff --git a/specifications/DiningPhilosophers/DiningPhilosophers_proof.tla b/specifications/DiningPhilosophers/DiningPhilosophers_proof.tla new file mode 100644 index 00000000..0286b8ec --- /dev/null +++ b/specifications/DiningPhilosophers/DiningPhilosophers_proof.tla @@ -0,0 +1,705 @@ +------------------------- MODULE DiningPhilosophers_proof ------------------------- +(***************************************************************************) +(* Proof that the solution in DiningPhilosophers is starvation free: every *) +(* philosopher eats infinitely often. *) +(* *) +(* All philosophers but N take their left fork first, and N takes its *) +(* right fork first. Either way, each philosopher first takes the lower- *) +(* numbered of its two forks (Dijkstra's resource hierarchy). *) +(* *) +(* A philosopher who holds fork f either eats, and then releases f, or *) +(* holds f as its low fork and waits for its high fork, whose number is *) +(* larger. By induction from the largest fork down, every fork is free *) +(* infinitely often, so strong fairness lets every philosopher take its *) +(* low fork, then its high fork, and eat. *) +(***************************************************************************) +EXTENDS DiningPhilosophers, TLAPS, NaturalsInduction, FiniteSetTheorems + +----------------------------------------------------------------------------- +(***************************************************************************) +(* Fork numbering. *) +(***************************************************************************) + +LEMMA NAtLeastTwo == N \in Nat /\ N >= 2 +<1>1. N \in Nat /\ N # 0 + BY NIsPosNat +<1>2. N # 1 + <2>. SUFFICES ASSUME N = 1 PROVE FALSE + OBVIOUS + <2>1. 1 \in P + BY <1>1 DEF P + <2>2. RightFork(1) # LeftFork(1) + BY <2>1, ForksDistinct + <2>. QED + BY <2>2 DEF RightFork, LeftFork +<1>. QED + BY <1>1, <1>2 + +LEMMA RightForkDef == + \A q \in P : RightFork(q) = IF q = N THEN 1 ELSE q + 1 +BY NAtLeastTwo DEF P, RightFork + +\* The fork that a philosopher takes first, and the one it takes second. +LowFork(p) == IF p = N THEN RightFork(p) ELSE LeftFork(p) +HighFork(p) == IF p = N THEN LeftFork(p) ELSE RightFork(p) + +LEMMA ForkFacts == + \A q \in P : + /\ LowFork(q) \in P + /\ HighFork(q) \in P + /\ LowFork(q) < HighFork(q) + /\ {LowFork(q), HighFork(q)} = {LeftFork(q), RightFork(q)} +BY NAtLeastTwo, RightForkDef DEF P, LowFork, HighFork, LeftFork + +\* The philosopher whose right fork is f. +Pred(f) == IF f = 1 THEN N ELSE f - 1 + +LEMMA PredInP == \A f \in P : Pred(f) \in P +BY NAtLeastTwo DEF P, Pred + +\* Fork f is only ever held by philosopher f or philosopher Pred(f). +LEMMA Holders == + \A f, q \in P : f \in {LowFork(q), HighFork(q)} => q = f \/ q = Pred(f) +BY NAtLeastTwo, ForkFacts, RightForkDef DEF P, LeftFork, Pred + +----------------------------------------------------------------------------- +(***************************************************************************) +(* Inductive invariant. *) +(***************************************************************************) + +Idle(p) == philosophers[p] = {} +Hungry(p) == philosophers[p] = {LowFork(p)} +Eating(p) == philosophers[p] = {LowFork(p), HighFork(p)} + +Phases == \A p \in P : Idle(p) \/ Hungry(p) \/ Eating(p) + +\* A fork lies on the table iff no one holds it ... +OnTable == \A f \in P : f \in forks <=> \A p \in P : f \notin philosophers[p] + +\* ... and no two philosophers hold the same fork. +Exclusive == \A p, q \in P : p # q => philosophers[p] \cap philosophers[q] = {} + +Inv == TypeOK /\ Phases /\ OnTable /\ Exclusive + +\* TakeLeft and TakeRight, seen as taking the low fork, then the high one. +TakeLow(p) == + /\ philosophers[p] = {} + /\ LowFork(p) \in forks + /\ forks' = forks \ {LowFork(p)} + /\ philosophers' = [philosophers EXCEPT ![p] = {LowFork(p)}] + +TakeHigh(p) == + /\ philosophers[p] = {LowFork(p)} + /\ HighFork(p) \in forks + /\ forks' = forks \ {HighFork(p)} + /\ philosophers' = [philosophers EXCEPT ![p] = {LowFork(p), HighFork(p)}] + +NextLH == \E p \in P : TakeLow(p) \/ TakeHigh(p) \/ Release(p) + +LEMMA TakeAgree == + ASSUME Inv, NEW p \in P, TakeLeft(p) \/ TakeRight(p) + PROVE TakeLow(p) \/ TakeHigh(p) +<1>. USE DEF Inv, TypeOK, LowFork, HighFork +<1>1. CASE TakeLeft(p) /\ p # N + <2>1. LeftFork(p) \in P /\ LeftFork(p) \notin philosophers[p] + BY <1>1 DEF TakeLeft, OnTable, LeftFork + <2>2. philosophers[p] = {} + BY <2>1, <1>1 DEF Phases, Idle, Hungry, Eating + <2>. QED + BY <1>1, <2>2 DEF TakeLeft, TakeLow +<1>2. CASE TakeLeft(p) /\ p = N + BY <1>2 DEF TakeLeft, TakeHigh +<1>3. CASE TakeRight(p) /\ p # N + BY <1>3 DEF TakeRight, TakeHigh +<1>4. CASE TakeRight(p) /\ p = N + <2>1. RightFork(p) \in P /\ RightFork(p) \notin philosophers[p] + BY <1>4, ForksDistinct DEF TakeRight, OnTable + <2>2. philosophers[p] = {} + BY <2>1, <1>4 DEF Phases, Idle, Hungry, Eating + <2>. QED + BY <1>4, <2>2 DEF TakeRight, TakeLow +<1>. QED + BY <1>1, <1>2, <1>3, <1>4 + +LEMMA NextAgree == ASSUME Inv, Next PROVE NextLH +BY TakeAgree DEF Next, NextLH + +\* What each action does, stated pointwise. +LEMMA TakeLowFrame == + ASSUME TypeOK, NEW p \in P, TakeLow(p) + PROVE /\ philosophers[p] = {} /\ LowFork(p) \in forks + /\ forks' = forks \ {LowFork(p)} + /\ philosophers'[p] = {LowFork(p)} + /\ \A r \in P : r # p => philosophers'[r] = philosophers[r] +BY DEF TypeOK, TakeLow + +LEMMA TakeHighFrame == + ASSUME TypeOK, NEW p \in P, TakeHigh(p) + PROVE /\ philosophers[p] = {LowFork(p)} /\ HighFork(p) \in forks + /\ forks' = forks \ {HighFork(p)} + /\ philosophers'[p] = {LowFork(p), HighFork(p)} + /\ \A r \in P : r # p => philosophers'[r] = philosophers[r] +BY DEF TypeOK, TakeHigh + +LEMMA ReleaseFrame == + ASSUME TypeOK, NEW p \in P, Release(p) + PROVE /\ philosophers[p] = {LowFork(p), HighFork(p)} + /\ forks' = forks \cup {LowFork(p), HighFork(p)} + /\ philosophers'[p] = {} + /\ \A r \in P : r # p => philosophers'[r] = philosophers[r] +BY ForkFacts DEF TypeOK, Release + +THEOREM TypeOKInit == Init => TypeOK +BY DEF Init, TypeOK, P + +THEOREM TypeOKNext == TypeOK /\ [Next]_vars => TypeOK' +<1>. SUFFICES ASSUME TypeOK, [Next]_vars PROVE TypeOK' + OBVIOUS +<1>. USE ForkFacts DEF TypeOK +<1>1. ASSUME NEW p \in P, TakeLeft(p) PROVE TypeOK' + BY <1>1 DEF TakeLeft, LeftFork +<1>2. ASSUME NEW p \in P, TakeRight(p) PROVE TypeOK' + BY <1>2, ForksDistinct DEF TakeRight +<1>3. ASSUME NEW p \in P, Release(p) PROVE TypeOK' + BY <1>3, ReleaseFrame DEF Release +<1>4. CASE UNCHANGED vars + BY <1>4 DEF vars +<1>. QED + BY <1>1, <1>2, <1>3, <1>4 DEF Next + +THEOREM PhasesNext == Inv /\ [Next]_vars => Phases' +<1>. SUFFICES ASSUME Inv, [Next]_vars PROVE Phases' + OBVIOUS +<1>. USE DEF Inv, Phases, Idle, Hungry, Eating +<1>1. ASSUME NEW p \in P, TakeLow(p) PROVE Phases' + BY <1>1, TakeLowFrame +<1>2. ASSUME NEW p \in P, TakeHigh(p) PROVE Phases' + BY <1>2, TakeHighFrame +<1>3. ASSUME NEW p \in P, Release(p) PROVE Phases' + BY <1>3, ReleaseFrame +<1>4. CASE UNCHANGED vars + BY <1>4 DEF vars +<1>. QED + BY <1>1, <1>2, <1>3, <1>4, NextAgree DEF NextLH + +THEOREM OnTableNext == Inv /\ [Next]_vars => OnTable' +<1>. SUFFICES ASSUME Inv, [Next]_vars, NEW g \in P + PROVE g \in forks' <=> \A r \in P : g \notin philosophers'[r] + BY DEF OnTable +<1>. USE ForkFacts DEF Inv, TypeOK, OnTable +<1>1. ASSUME NEW p \in P, TakeLow(p) + PROVE g \in forks' <=> \A r \in P : g \notin philosophers'[r] + <2>1. CASE g = LowFork(p) + BY <1>1, <2>1, TakeLowFrame + <2>2. CASE g # LowFork(p) + <3>1. \A r \in P : g \in philosophers'[r] <=> g \in philosophers[r] + BY <1>1, <2>2, TakeLowFrame + <3>. QED + BY <1>1, <2>2, <3>1, TakeLowFrame + <2>. QED + BY <2>1, <2>2 +<1>2. ASSUME NEW p \in P, TakeHigh(p) + PROVE g \in forks' <=> \A r \in P : g \notin philosophers'[r] + <2>1. CASE g = HighFork(p) + BY <1>2, <2>1, TakeHighFrame + <2>2. CASE g # HighFork(p) + <3>1. \A r \in P : g \in philosophers'[r] <=> g \in philosophers[r] + BY <1>2, <2>2, TakeHighFrame + <3>. QED + BY <1>2, <2>2, <3>1, TakeHighFrame + <2>. QED + BY <2>1, <2>2 +<1>3. ASSUME NEW p \in P, Release(p) + PROVE g \in forks' <=> \A r \in P : g \notin philosophers'[r] + <2>1. CASE g \in {LowFork(p), HighFork(p)} + BY <1>3, <2>1, ReleaseFrame DEF Exclusive + <2>2. CASE g \notin {LowFork(p), HighFork(p)} + <3>1. \A r \in P : g \in philosophers'[r] <=> g \in philosophers[r] + BY <1>3, <2>2, ReleaseFrame + <3>. QED + BY <1>3, <2>2, <3>1, ReleaseFrame + <2>. QED + BY <2>1, <2>2 +<1>4. CASE UNCHANGED vars + BY <1>4 DEF vars +<1>. QED + BY <1>1, <1>2, <1>3, <1>4, NextAgree DEF NextLH + +THEOREM ExclusiveNext == Inv /\ [Next]_vars => Exclusive' +<1>. SUFFICES ASSUME Inv, [Next]_vars, + NEW r1 \in P, NEW r2 \in P, r1 # r2 + PROVE philosophers'[r1] \cap philosophers'[r2] = {} + BY DEF Exclusive +<1>. USE DEF Inv, TypeOK +<1>1. ASSUME NEW p \in P, TakeLow(p) + PROVE philosophers'[r1] \cap philosophers'[r2] = {} + <2>1. \A r \in P : LowFork(p) \notin philosophers[r] + BY <1>1, TakeLowFrame DEF OnTable + <2>. QED + BY <1>1, <2>1, TakeLowFrame DEF Exclusive +<1>2. ASSUME NEW p \in P, TakeHigh(p) + PROVE philosophers'[r1] \cap philosophers'[r2] = {} + <2>1. \A r \in P : HighFork(p) \notin philosophers[r] + BY <1>2, TakeHighFrame DEF OnTable + <2>2. \A r \in P : r # p => LowFork(p) \notin philosophers[r] + <3>. SUFFICES ASSUME NEW r \in P, r # p PROVE LowFork(p) \notin philosophers[r] + OBVIOUS + <3>1. philosophers[p] \cap philosophers[r] = {} + BY DEF Exclusive + <3>. QED + BY <1>2, <3>1, TakeHighFrame + <2>. QED + BY <1>2, <2>1, <2>2, TakeHighFrame DEF Exclusive +<1>3. ASSUME NEW p \in P, Release(p) + PROVE philosophers'[r1] \cap philosophers'[r2] = {} + BY <1>3, ReleaseFrame DEF Exclusive +<1>4. CASE UNCHANGED vars + BY <1>4 DEF vars, Exclusive +<1>. QED + BY <1>1, <1>2, <1>3, <1>4, NextAgree DEF NextLH + +THEOREM InvInit == Init => Inv +BY ForkFacts, TypeOKInit DEF Init, Inv, Phases, OnTable, Exclusive, Idle, P + +THEOREM InvNext == Inv /\ [Next]_vars => Inv' +BY TypeOKNext, PhasesNext, OnTableNext, ExclusiveNext DEF Inv + +THEOREM InvSpec == Spec => []Inv +BY InvInit, InvNext, PTL DEF Spec + +----------------------------------------------------------------------------- +(***************************************************************************) +(* The steps of a single philosopher. *) +(***************************************************************************) + +Act(p) == TakeLeft(p) \/ TakeRight(p) \/ Release(p) + +LEMMA SpecNext == Spec => [][Next]_vars +BY DEF Spec + +LEMMA SpecFair == \A q \in P : Spec => SF_vars(Act(q)) +BY DEF Spec, Act + +\* A step either is a step of q or leaves q's forks alone. +LEMMA NextSplit == + ASSUME Inv, [Next]_vars, NEW q \in P + PROVE <>_vars \/ philosophers'[q] = philosophers[q] +<1>1. CASE UNCHANGED vars + BY <1>1 DEF vars +<1>2. ASSUME NEW p \in P, p # q, Act(p) + PROVE philosophers'[q] = philosophers[q] + BY <1>2 DEF Act, TakeLeft, TakeRight, Release, Inv, TypeOK +<1>3. CASE Act(q) + BY <1>3 DEF vars +<1>. QED + BY <1>1, <1>2, <1>3 DEF Next, Act + +\* A step of q is a step of TakeLow, TakeHigh, or Release. +LEMMA ActAgree == + ASSUME Inv, NEW q \in P, Act(q) + PROVE TakeLow(q) \/ TakeHigh(q) \/ Release(q) +BY TakeAgree DEF Act + +LEMMA IdleStep == + ASSUME Inv, NEW q \in P, Idle(q), <>_vars + PROVE Hungry(q)' +BY ActAgree, ForkFacts DEF Inv, TypeOK, Idle, Hungry, TakeLow, TakeHigh, Release + +LEMMA HungryStep == + ASSUME Inv, NEW q \in P, Hungry(q), <>_vars + PROVE Eating(q)' +BY ActAgree, ForkFacts DEF Inv, TypeOK, Hungry, Eating, TakeLow, TakeHigh, Release + +LEMMA EatingStep == + ASSUME Inv, NEW q \in P, Eating(q), <>_vars + PROVE \A f \in philosophers[q] : f \in forks' +BY ActAgree, ForkFacts DEF Inv, TypeOK, Eating, TakeLow, TakeHigh, Release + +LEMMA IdleEnabled == + ASSUME NEW q \in P + PROVE Inv /\ Idle(q) /\ LowFork(q) \in forks => ENABLED <>_vars +<1>. SUFFICES ASSUME Inv, Idle(q), LowFork(q) \in forks + PROVE ENABLED <>_vars + OBVIOUS +<1>1. philosophers \in [P -> SUBSET P] /\ philosophers[q] = {} + BY DEF Inv, TypeOK, Idle +<1>2. CASE q # N + <2>1. LeftFork(q) \in forks + BY <1>2 DEF LowFork + <2>2. <<[philosophers EXCEPT ![q] = philosophers[q] \cup {LeftFork(q)}], + forks \ {LeftFork(q)}>> # <> + BY <1>1 + <2>3. ENABLED <>_vars + BY <1>1, <1>2, <2>1, <2>2, ExpandENABLED DEF TakeLeft, vars + <2>. QED + BY <2>3, ExpandENABLED DEF Act, TakeLeft, TakeRight, Release, vars +<1>3. CASE q = N + <2>1. RightFork(q) \in forks + BY <1>3 DEF LowFork + <2>2. <<[philosophers EXCEPT ![q] = philosophers[q] \cup {RightFork(q)}], + forks \ {RightFork(q)}>> # <> + BY <1>1 + <2>3. ENABLED <>_vars + BY <1>1, <1>3, <2>1, <2>2, ExpandENABLED DEF TakeRight, vars + <2>. QED + BY <2>3, ExpandENABLED DEF Act, TakeLeft, TakeRight, Release, vars +<1>. QED + BY <1>2, <1>3 + +LEMMA HungryEnabled == + ASSUME NEW q \in P + PROVE Inv /\ Hungry(q) /\ HighFork(q) \in forks => ENABLED <>_vars +<1>. SUFFICES ASSUME Inv, Hungry(q), HighFork(q) \in forks + PROVE ENABLED <>_vars + OBVIOUS +<1>1. philosophers \in [P -> SUBSET P] /\ philosophers[q] = {LowFork(q)} + BY DEF Inv, TypeOK, Hungry +<1>2. LeftFork(q) # RightFork(q) + BY ForksDistinct +<1>3. CASE q # N + <2>1. philosophers[q] = {LeftFork(q)} /\ RightFork(q) \in forks + BY <1>1, <1>3 DEF LowFork, HighFork + <2>2. <<[philosophers EXCEPT ![q] = philosophers[q] \cup {RightFork(q)}], + forks \ {RightFork(q)}>> # <> + BY <1>1, <1>2, <2>1 + <2>3. (q # N => philosophers[q] = {LeftFork(q)}) /\ RightFork(q) \in forks + BY <2>1 + <2>4. ENABLED <>_vars + BY <2>2, <2>3, ExpandENABLED DEF TakeRight, vars + <2>. QED + BY <2>4, ExpandENABLED DEF Act, TakeLeft, TakeRight, Release, vars +<1>4. CASE q = N + <2>1. philosophers[q] = {RightFork(q)} /\ LeftFork(q) \in forks + BY <1>1, <1>4 DEF LowFork, HighFork + <2>2. <<[philosophers EXCEPT ![q] = philosophers[q] \cup {LeftFork(q)}], + forks \ {LeftFork(q)}>> # <> + BY <1>1, <1>2, <2>1 + <2>3. (q = N => philosophers[q] = {RightFork(q)}) /\ LeftFork(q) \in forks + BY <2>1 + <2>4. ENABLED <>_vars + BY <2>2, <2>3, ExpandENABLED DEF TakeLeft, vars + <2>. QED + BY <2>4, ExpandENABLED DEF Act, TakeLeft, TakeRight, Release, vars +<1>. QED + BY <1>3, <1>4 + +LEMMA EatingEnabled == + ASSUME NEW q \in P + PROVE Inv /\ Eating(q) => ENABLED <>_vars +<1>. SUFFICES ASSUME Inv, Eating(q) + PROVE ENABLED <>_vars + OBVIOUS +<1>1. philosophers \in [P -> SUBSET P] + /\ philosophers[q] = {LeftFork(q), RightFork(q)} + BY ForkFacts DEF Inv, TypeOK, Eating +<1>2. {LeftFork(q), RightFork(q)} # {} + OBVIOUS +<1>3. <<[philosophers EXCEPT ![q] = {}], forks \cup {LeftFork(q), RightFork(q)}>> + # <> + BY <1>1, <1>2 +<1>4. ENABLED <>_vars + BY <1>1, <1>3, ExpandENABLED DEF Release, vars +<1>. QED + BY <1>4, ExpandENABLED DEF Act, TakeLeft, TakeRight, Release, vars + +----------------------------------------------------------------------------- +(***************************************************************************) +(* Progress of a single philosopher. *) +(***************************************************************************) + +FreeIO(f) == []<>(f \in forks) + +HeldEat(f, q) == Eating(q) /\ f \in philosophers[q] + +\* Named so that the lemmas below can be instantiated: backends other than +\* PTL only see temporal formulas through opaque operators. +IdleToHungry(q) == Idle(q) ~> Hungry(q) +HungryToEating(q) == Hungry(q) ~> Eating(q) +EatingFrees(f, q) == HeldEat(f, q) ~> (f \in forks) +HungryFrees(f, q) == (Hungry(q) /\ f = LowFork(q)) ~> (f \in forks) + +LEMMA IdleHungry == + ASSUME NEW q \in P + PROVE Spec /\ FreeIO(LowFork(q)) => IdleToHungry(q) +<1>1. Inv /\ Idle(q) /\ [Next]_vars => Idle(q)' \/ Hungry(q)' + <2>. SUFFICES ASSUME Inv, Idle(q), [Next]_vars PROVE Idle(q)' \/ Hungry(q)' + OBVIOUS + <2>1. CASE philosophers'[q] = philosophers[q] + BY <2>1 DEF Idle + <2>2. CASE <>_vars + BY <2>2, IdleStep + <2>. QED + BY <2>1, <2>2, NextSplit +<1>2. Inv /\ Idle(q) /\ <>_vars => Hungry(q)' + BY IdleStep +<1>3. Inv /\ Idle(q) /\ LowFork(q) \in forks => ENABLED <>_vars + BY IdleEnabled +<1>4. Spec => SF_vars(Act(q)) + BY SpecFair +<1>. QED + BY <1>1, <1>2, <1>3, <1>4, InvSpec, SpecNext, PTL DEF FreeIO, IdleToHungry + +LEMMA HungryEat == + ASSUME NEW q \in P + PROVE Spec /\ FreeIO(HighFork(q)) => HungryToEating(q) +<1>1. Inv /\ Hungry(q) /\ [Next]_vars => Hungry(q)' \/ Eating(q)' + <2>. SUFFICES ASSUME Inv, Hungry(q), [Next]_vars PROVE Hungry(q)' \/ Eating(q)' + OBVIOUS + <2>1. CASE philosophers'[q] = philosophers[q] + BY <2>1 DEF Hungry + <2>2. CASE <>_vars + BY <2>2, HungryStep + <2>. QED + BY <2>1, <2>2, NextSplit +<1>2. Inv /\ Hungry(q) /\ <>_vars => Eating(q)' + BY HungryStep +<1>3. Inv /\ Hungry(q) /\ HighFork(q) \in forks => ENABLED <>_vars + BY HungryEnabled +<1>4. Spec => SF_vars(Act(q)) + BY SpecFair +<1>. QED + BY <1>1, <1>2, <1>3, <1>4, InvSpec, SpecNext, PTL DEF FreeIO, HungryToEating + +LEMMA EatRelease == + ASSUME NEW f \in P, NEW q \in P + PROVE Spec => EatingFrees(f, q) +<1>1. Inv /\ HeldEat(f, q) /\ [Next]_vars => HeldEat(f, q)' \/ (f \in forks)' + <2>. SUFFICES ASSUME Inv, HeldEat(f, q), [Next]_vars + PROVE HeldEat(f, q)' \/ (f \in forks)' + OBVIOUS + <2>1. CASE philosophers'[q] = philosophers[q] + BY <2>1 DEF HeldEat, Eating + <2>2. CASE <>_vars + BY <2>2, EatingStep DEF HeldEat + <2>. QED + BY <2>1, <2>2, NextSplit +<1>2. Inv /\ HeldEat(f, q) /\ <>_vars => (f \in forks)' + BY EatingStep DEF HeldEat +<1>3. Inv /\ HeldEat(f, q) => ENABLED <>_vars + BY EatingEnabled DEF HeldEat +<1>4. Spec => SF_vars(Act(q)) + BY SpecFair +<1>. QED + BY <1>1, <1>2, <1>3, <1>4, InvSpec, SpecNext, PTL DEF EatingFrees + +\* A hungry philosopher who holds f as its low fork eventually frees f, +\* provided that all forks larger than f are free infinitely often. +LEMMA HungryRelease == + ASSUME NEW f \in P, NEW q \in P + PROVE Spec /\ (\A g \in P : g > f => FreeIO(g)) => HungryFrees(f, q) +<1>1. CASE f = LowFork(q) + <2>1. HighFork(q) \in P /\ HighFork(q) > f + BY <1>1, ForkFacts + <2>2. (\A g \in P : g > f => FreeIO(g)) => FreeIO(HighFork(q)) + BY <2>1 + <2>3. Spec /\ FreeIO(HighFork(q)) => HungryToEating(q) + BY HungryEat + <2>4. Spec => EatingFrees(f, q) + BY EatRelease + <2>5. Eating(q) => HeldEat(f, q) + BY <1>1 DEF HeldEat, Eating + <2>6. (Hungry(q) /\ f = LowFork(q)) => Hungry(q) + OBVIOUS + <2>. QED + BY <2>2, <2>3, <2>4, <2>5, <2>6, PTL + DEF HungryToEating, EatingFrees, HungryFrees +<1>2. CASE f # LowFork(q) + <2>1. ~(Hungry(q) /\ f = LowFork(q)) + BY <1>2 + <2>. QED + BY <2>1, PTL DEF HungryFrees +<1>. QED + BY <1>1, <1>2 + +----------------------------------------------------------------------------- +(***************************************************************************) +(* Every fork is free infinitely often. *) +(***************************************************************************) + +LEMMA HeldBy == + ASSUME NEW f \in P + PROVE Inv /\ ~(f \in forks) => + \/ HeldEat(f, f) \/ HeldEat(f, Pred(f)) + \/ Hungry(f) /\ f = LowFork(f) + \/ Hungry(Pred(f)) /\ f = LowFork(Pred(f)) +<1>. SUFFICES ASSUME Inv, ~(f \in forks) + PROVE \/ HeldEat(f, f) \/ HeldEat(f, Pred(f)) + \/ Hungry(f) /\ f = LowFork(f) + \/ Hungry(Pred(f)) /\ f = LowFork(Pred(f)) + OBVIOUS +<1>1. PICK q \in P : f \in philosophers[q] + BY DEF Inv, OnTable +<1>2. f \in {LowFork(q), HighFork(q)} + BY <1>1 DEF Inv, Phases, Idle, Hungry, Eating +<1>3. q = f \/ q = Pred(f) + BY <1>2, Holders +<1>4. HeldEat(f, q) \/ (Hungry(q) /\ f = LowFork(q)) + BY <1>1 DEF Inv, Phases, Idle, Hungry, Eating, HeldEat +<1>. QED + BY <1>3, <1>4 + +LEMMA FreeStep == + ASSUME NEW f \in P + PROVE Spec /\ (\A g \in P : g > f => FreeIO(g)) => FreeIO(f) +<1>1. Pred(f) \in P + BY PredInP +<1>2. Inv /\ ~(f \in forks) => + \/ HeldEat(f, f) \/ HeldEat(f, Pred(f)) + \/ Hungry(f) /\ f = LowFork(f) + \/ Hungry(Pred(f)) /\ f = LowFork(Pred(f)) + BY HeldBy +<1>3. Spec => EatingFrees(f, f) + BY EatRelease +<1>4. Spec => EatingFrees(f, Pred(f)) + BY <1>1, EatRelease +<1>5. Spec /\ (\A g \in P : g > f => FreeIO(g)) => HungryFrees(f, f) + BY HungryRelease +<1>6. Spec /\ (\A g \in P : g > f => FreeIO(g)) => HungryFrees(f, Pred(f)) + BY <1>1, HungryRelease +<1>. QED + BY <1>2, <1>3, <1>4, <1>5, <1>6, InvSpec, PTL + DEF FreeIO, EatingFrees, HungryFrees + +THEOREM AllFree == \A f \in P : Spec => FreeIO(f) +<1>. DEFINE Q(m) == Spec => \A g \in P : g + m > N => FreeIO(g) +<1>1. Q(0) + BY NAtLeastTwo DEF P +<1>2. \A m \in Nat : Q(m) => Q(m + 1) + <2>. SUFFICES ASSUME NEW m \in Nat, Q(m) + PROVE Q(m + 1) + OBVIOUS + <2>1. ASSUME NEW g \in P, g + (m + 1) > N + PROVE Spec => FreeIO(g) + <3>1. CASE g + m > N + BY <3>1 + <3>2. CASE ~(g + m > N) + <4>1. \A h \in P : h > g => h + m > N + BY <2>1, <3>2, NAtLeastTwo DEF P + <4>2. Spec => \A h \in P : h > g => FreeIO(h) + BY <4>1 + <4>. QED + BY <4>2, FreeStep + <3>. QED + BY <3>1, <3>2 + <2>. QED + BY <2>1 +<1>. HIDE DEF Q +<1>3. \A m \in Nat : Q(m) + BY <1>1, <1>2, NatInduction +<1>4. Q(N) + BY <1>3, NAtLeastTwo +<1>. QED + BY <1>4, NAtLeastTwo DEF Q, P + +----------------------------------------------------------------------------- +(***************************************************************************) +(* Starvation freedom. *) +(***************************************************************************) + +LEMMA EatingIsEating == \A p \in P : Eating(p) => IsEating(p) +<1>. SUFFICES ASSUME NEW p \in P, Eating(p) PROVE IsEating(p) + OBVIOUS +<1>1. LowFork(p) # HighFork(p) + BY ForkFacts +<1>2. IsFiniteSet({LowFork(p)}) /\ Cardinality({LowFork(p)}) = 1 + BY FS_Singleton +<1>3. Cardinality({LowFork(p)} \cup {HighFork(p)}) = 2 + BY <1>1, <1>2, FS_AddElement +<1>. QED + BY <1>3 DEF Eating, IsEating + +THEOREM StarvationFreedom +<1>. SUFFICES ASSUME NEW p \in P PROVE Spec => []<>IsEating(p) + BY DEF NoStarvation +<1>1. Spec => FreeIO(LowFork(p)) + BY AllFree, ForkFacts +<1>2. Spec => FreeIO(HighFork(p)) + BY AllFree, ForkFacts +<1>3. Spec /\ FreeIO(LowFork(p)) => IdleToHungry(p) + BY IdleHungry +<1>4. Spec /\ FreeIO(HighFork(p)) => HungryToEating(p) + BY HungryEat +<1>5. Inv => Idle(p) \/ Hungry(p) \/ Eating(p) + BY DEF Inv, Phases +<1>6. Eating(p) => IsEating(p) + BY EatingIsEating +<1>. QED + BY <1>1, <1>2, <1>3, <1>4, <1>5, <1>6, InvSpec, PTL + DEF IdleToHungry, HungryToEating + +EatsIO(p) == []<>IsEating(p) + +THEOREM StarvationImpliesNoLivelock == NoStarvation => NoLivelock +<1>1. 1 \in P + BY NIsPosNat DEF P +<1>2. NoStarvation => \A p \in P : EatsIO(p) + BY DEF NoStarvation, EatsIO +<1>3. NoStarvation => EatsIO(1) + BY <1>1, <1>2 +<1>4. IsEating(1) => \E p \in P : IsEating(p) + BY <1>1 +<1>. QED + BY <1>3, <1>4, PTL DEF EatsIO, NoLivelock + +THEOREM LivelockFreedom +BY StarvationFreedom, StarvationImpliesNoLivelock + +----------------------------------------------------------------------------- +(***************************************************************************) +(* Deadlock freedom. If no one eats, fork N is free, because it is the *) +(* high fork of both philosophers who can hold it. So philosopher N-1 or *) +(* N can take it if hungry; if both are idle, fork N-1 is free too. *) +(***************************************************************************) + +LEMMA ActEnabledNext == + ASSUME NEW q \in P + PROVE (ENABLED <>_vars) => ENABLED Next +BY ExpandENABLED DEF Act, Next, TakeLeft, TakeRight, Release, vars + +LEMMA TopForks == + /\ N - 1 \in P /\ N \in P + /\ LowFork(N - 1) = N - 1 /\ HighFork(N - 1) = N + /\ LowFork(N) = 1 /\ HighFork(N) = N + /\ Pred(N) = N - 1 /\ 1 # N /\ N - 1 # N + /\ Pred(N - 1) = N \/ LowFork(Pred(N - 1)) # N - 1 +BY NAtLeastTwo, RightForkDef DEF P, LowFork, HighFork, LeftFork, Pred + +THEOREM InvNoDeadlock == Inv => NoDeadlock +<1>. SUFFICES ASSUME Inv PROVE ENABLED Next + BY DEF NoDeadlock +<1>. DEFINE M == N - 1 +<1>0. TopForks + BY TopForks +<1>1. CASE \E q \in P : Eating(q) + BY <1>1, EatingEnabled, ActEnabledNext +<1>2. CASE \A q \in P : ~Eating(q) + <2>1. ~HeldEat(N, N) /\ ~HeldEat(N, Pred(N)) + /\ ~HeldEat(M, M) /\ ~HeldEat(M, Pred(M)) + BY <1>0, <1>2, PredInP DEF HeldEat + <2>2. N \in forks + <3>1. N # LowFork(N) /\ N # LowFork(Pred(N)) + BY <1>0 + <3>. QED + BY <1>0, <2>1, <3>1, HeldBy + <2>3. CASE Hungry(M) + BY <1>0, <2>2, <2>3, HungryEnabled, ActEnabledNext + <2>4. CASE Hungry(N) + BY <1>0, <2>2, <2>4, HungryEnabled, ActEnabledNext + <2>5. CASE ~Hungry(M) /\ ~Hungry(N) + <3>1. Idle(M) /\ Idle(N) + BY <1>0, <1>2, <2>5 DEF Inv, Phases + <3>2. ~Hungry(Pred(M)) \/ LowFork(Pred(M)) # M + BY <1>0, <2>5 + <3>3. M \in forks + BY <1>0, <2>1, <2>5, <3>2, HeldBy + <3>. QED + BY <1>0, <3>1, <3>3, IdleEnabled, ActEnabledNext + <2>. QED + BY <2>3, <2>4, <2>5 +<1>. QED + BY <1>1, <1>2 + +THEOREM DeadlockFreedom +BY InvNoDeadlock, InvSpec, PTL + +============================================================================= diff --git a/specifications/DiningPhilosophers/manifest.json b/specifications/DiningPhilosophers/manifest.json index f71b9010..7491e783 100644 --- a/specifications/DiningPhilosophers/manifest.json +++ b/specifications/DiningPhilosophers/manifest.json @@ -1,7 +1,8 @@ { "sources": [], "authors": [ - "Jeff Hemphill" + "Jeff Hemphill", + "Markus Kuppe" ], "tags": [ "beginner" @@ -21,12 +22,27 @@ }, { "path": "specifications/DiningPhilosophers/DiningPhilosophers.tla", + "features": [], + "models": [ + { + "path": "specifications/DiningPhilosophers/DiningPhilosophers.cfg", + "runtime": "00:00:01", + "mode": "exhaustive search", + "result": "success", + "distinctStates": 70, + "totalStates": 220, + "stateDepth": 6 + } + ] + }, + { + "path": "specifications/DiningPhilosophers/DiningPhilosophersPCal.tla", "features": [ "pluscal" ], "models": [ { - "path": "specifications/DiningPhilosophers/DiningPhilosophers.cfg", + "path": "specifications/DiningPhilosophers/DiningPhilosophersPCal.cfg", "runtime": "00:00:01", "mode": "exhaustive search", "result": "success", @@ -35,6 +51,29 @@ "stateDepth": 29 } ] + }, + { + "path": "specifications/DiningPhilosophers/DiningPhilosophers_anim.tla", + "features": [], + "models": [ + { + "path": "specifications/DiningPhilosophers/DiningPhilosophers_anim.cfg", + "runtime": "00:00:01", + "mode": "exhaustive search", + "result": "success", + "distinctStates": 70, + "totalStates": 220, + "stateDepth": 6 + } + ] + }, + { + "path": "specifications/DiningPhilosophers/DiningPhilosophers_proof.tla", + "features": [], + "models": [], + "proof": { + "maxRuntimeMinutes": 3 + } } ] } \ No newline at end of file