Dining Philosophers
Step through individual fork acquisitions and inspect ownership, waiting and completed meals.
About this tool
Explore how five philosophers share five forks when every philosopher acquires the lower-numbered fork first. Follow individual actions, including unsuccessful attempts, and inspect exactly who owns each resource.
Prepare and step
Prepare creates the initial state: everyone is thinking, all forks are free, and all counters are zero. Step performs one action for the selected philosopher. Automatic performs one action at a time at the chosen pace of 0.25–4 actions per second. This pace affects only presentation; the model counts actions, not physical time.
Round robin selects the philosopher after the one who just acted. Manual lets you choose any philosopher, including the same one repeatedly. Changing scheduling, philosopher selection or pace pauses the run and preserves its current state. Reset returns a prepared experiment to the initial state while keeping these settings.
Pause, hiding the tool and navigating away stop automatic actions. Missed background time is not replayed. Returning within the app preserves the paused state; reloading restores settings only and waits for Prepare.
Neighbors and fork order
The visible philosopher names are P1–P5, while forks are numbered F0–F4. P1 needs F0 and F1; P2 needs F1 and F2; P3 needs F2 and F3; P4 needs F3 and F4; P5 needs F4 and F0. Each fork sits between exactly the two philosophers who can use it.
Every philosopher takes the smaller fork number before the larger one. Thus P5 takes F0 before F4. Ownership lines and colors connect a held fork to its philosopher. The table and fork-owner list provide the same information as text.
One atomic action
- A thinking philosopher becomes hungry, holding no fork.
- A philosopher needing the first fork tries to acquire the lower-numbered fork. If it is free, the philosopher takes it and still holds only one fork. Otherwise the attempt waits without changing ownership.
- A philosopher needing the second fork tries the higher-numbered fork while retaining the first. Successful acquisition starts eating; an unsuccessful attempt keeps the existing fork.
- An eating philosopher releases both forks in one action, completes exactly one meal and returns to thinking.
The action counter includes unsuccessful acquisition attempts. Hungry counts both phases before eating. Blocked counts hungry philosophers whose currently wanted fork has an owner; it does not mean that the entire system is deadlocked.
Try an interleaving
Choose Manual and P1. Two steps make P1 hungry and acquire F0. Choose P5 and step twice: P5 becomes hungry, then waits for F0 while holding nothing. Return to P1: one step acquires F1 and starts eating; the next releases both forks and completes a meal. P5 can then acquire F0 on its next action.
Deadlock and fairness
The resource hierarchy removes circular waiting: a philosopher holding one fork can request only a higher-numbered fork. A cycle of strictly increasing fork numbers cannot close. The exclusive-owner rule also prevents neighboring philosophers from eating at the same time.
Deadlock avoidance is not a general fairness guarantee. An unfair manual schedule can repeatedly select a waiting philosopher and never select an owner who could release the needed fork. That stalled selection sequence is not proof of a global resource deadlock. The displayed progress and meal counts describe only the chosen sequence; this tool promises neither FIFO service nor bounded waiting for every philosopher.
Scope and source
This is a deterministic interleaving model, not a simulation of actual threads or random thinking and eating durations.
Dijkstra and Scholten, Distributed Arbitration (EWD752) discusses neighboring fork resources, acquisition and blocking states, and resource ranking in §4. Its statements about individual freedom from starvation rely on the stronger binary-arbitration assumptions P0/C0. Those guarantees are not transferred to this freely selectable scheduler.