[lemmy]

Dijkstra's resource hierarchy (TLA+)

DiningPhilosophers.tla models the forks directly. Odd philosophers take their left fork first, and even philosophers take their right fork first, which breaks the circular wait. Strong fairness makes the spec free of deadlock, livelock, and starvation.

The git history shows how the spec got there. The table lists, for each commit, the properties for which TLC finds a counterexample:

Step	Solution	Known as	Deadlock	Livelock	Starvation
1	Take the forks in any order	Unordered fork acquisition	yes	yes	yes
2	Take the left fork before the right fork	Naive (symmetric) solution	yes	yes	yes
3	Put the left fork back if the right fork is taken	Back-off and retry	no	yes	yes
4	Take both forks at once	Dijkstra's semaphore solution (Tanenbaum's monitor)	no	no	yes
5	Let a philosopher who ate wait for its neighbors	Priority to waiting neighbors	no	no	no
6	Let a waiter serve philosophers in order	Waiter (arbitrator) with a queue	no	no	no
7	Let a footman seat at most N-1 philosophers	Footman (butler) solution	no	no	no
8	Let philosopher N take its right fork first	Resource hierarchy (asymmetric) solution	no	no	no
9	Let even philosophers take their right fork first	Odd/even (alternating) solution	no	no	no

In steps 1 and 2, every philosopher can end up holding one fork. In step 4, two neighbors can take turns eating and starve the philosopher between them. Steps 5 and 6 fix that: in step 5 a philosopher who ate waits for its neighbors, and in step 6 a waiter serves neighbors in the order in which they asked. Both still take two forks in one step, which no lock on a single fork provides. Step 7 goes back to one fork at a time, with a footman whose guard reads the
state of every philosopher. Steps 8 and 9 replace the footman with a fork order that each philosopher follows on its own.

This repository has specs of two other solutions:

• Chandy-Misra: philosophers hand clean forks to their neighbors on
  request. See DiningPhilosophersPCal.tla
  below.
• Bakery: hungry philosophers take a ticket, and the lowest ticket eats
  first. The ticket order gives a fair, first-come-first-served solution.
  Lamport's Bakery algorithm and its Boulangerie variant are in
  Bakery-Boulangerie. They solve mutual exclusion,
  not dining, but the ticket idea carries over.

TLC checks the spec only for N = 5. DiningPhilosophers_proof.tla proves with
TLAPS that the spec is free of deadlock, livelock, and starvation for every N:

tlapm --strict DiningPhilosophers_proof.tla

DiningPhilosophers_anim.tla draws the table, forks, and philosophers for any N and writes one SVG per state. The animation comes from Spectacle.