Repository navigation
DiningPhilosophers: add a pure TLA+ spec that walks from broken solutions to a proved one - #237
Merged
Merged
Conversation
This makes room for a pure TLA+ version under the name DiningPhilosophers. The PCal suffix matches EWD998PCal and show521677PCal. APDiningPhilosophers now instantiates DiningPhilosophersPCal. The state space is unchanged. Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
The alygin.vscode-tlaplus extension has moved to the tlaplus organization and is now published as tlaplus.vscode-ide. Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
The PlusCal spec fixes one solution in code, so it cannot show why the naive solutions fail. DiningPhilosophers models the forks directly: philosophers take their left and right forks in any order and release both after eating. Strong fairness of each philosopher makes NoStarvation counterexamples show actual starvation. NoDeadlock and NoLivelock tell whether the table as a whole makes progress. The ASSUMEs reject fork layouts in which a fork is outside 1..N, a philosopher's two forks are the same, or a fork is no one's right fork. TLC finds the deadlock where every philosopher holds one fork. DiningPhilosophers_anim draws the table, plates, forks, and philosophers for any N, colored by state, and writes one SVG per state with SVGSerialize. The spec and animation come from Spectacle: https://github.com/will62794/spectacle Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
TakeRight had no ordering guard, so philosophers could grab either fork first. Require the left fork to be held before taking the right one, which models the naive left-then-right algorithm. TLC finds the classic deadlock where every philosopher holds only the left fork. Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
The naive left-then-right algorithm deadlocks once every philosopher holds a left fork. Let a philosopher who cannot get the right fork put the left fork back and retry. This removes the deadlock, but TLC still finds NoStarvation violations: philosophers can livelock by taking and returning their left forks, or starve while a neighbor keeps eating. Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Philosophers who put the left fork back can livelock. Replace TakeLeft, TakeRight, and PutBack with TakeBoth, which takes both forks in one step and only when both are free (Dijkstra's solution, as in Tanenbaum's monitor version). No philosopher ever holds a single fork, so there is no deadlock or livelock. TLC still finds a NoStarvation violation: a philosopher's two neighbors can eat in overlapping turns, so the philosopher's forks are never both free, and not even strong fairness forces it to eat. Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Taking both forks at once lets a philosopher's neighbors starve it. Go back to TakeLeft and TakeRight and fix the order in which a philosopher takes its forks: all but philosopher N take the left fork first, and N takes the right fork first. Each philosopher thus takes the lower-numbered of its two forks first (Dijkstra's resource hierarchy), which breaks the circular wait. TLC finds no violation of NoDeadlock, NoLivelock, or NoStarvation: under strong fairness, a philosopher who holds its first fork eventually gets the second, because that fork becomes free again and again. Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
TLC checks NoStarvation only for N = 5. The proof shows Spec => NoStarvation for every N. Forks are freed infinitely often, by induction from the highest fork down: a hungry philosopher holds its low fork and waits only for a higher one. Strong fairness then lets each philosopher take both forks. Check with: tlapm --strict DiningPhilosophers_proof.tla Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The PlusCal spec encodes one solution, so it cannot show why the naive solutions fail. DiningPhilosophers models the forks directly and checks NoDeadlock, NoLivelock, and NoStarvation under strong fairness of each philosopher. Each commit is one step, and TLC shows how each broken solution fails: