Dining Philosophers

We consider the classical problem of dining philosophers. The goal is to model this problem in PlusCal, formalize the requirements below in TLA+, and check under which fairness conditions these requirements hold.

Requirements

We consider the following requirements:

  1. Each philosopher thinks infinitely often
  2. Two neighbours never eat at the same time
  3. When a philosopher is hungry, he eventually have a meal
  4. When a philosopher eats, he will think some time later
  5. When a philosopher eats, he has been thinking before
  6. Between two meals of philosopher i, Philosopher i+1 gets to eat to (for each i)

Formalize the 6 requirements above as LTL formulas. Define the atomic propositions that are needed for your formulas.

Anarchic access to the forks

A philosopher does the following sequence of actions repeatedly:

Write a PlusCal model where each philosopher runs the algorithm above. Explain why your model has deadlocks.

A semaphore to rule them all

A solution is to use a semaphore (mutex) to solve the deadlock issue. Now, the philosophers do the following sequence of actions repeatedly:

Write a PlusCal model where each philosopher runs the algorithm above. The mutex semaphore is implemented as an integer variable.

Formalize the first 4 requirements above in TLA+. For each requirement (1, 2, 3 and 4) and each fairness condition (no, -wfNext, -wf and -sf), fill the following table indicating (YES/NO) whether the requirement holds under the fairness condition or not.

no -wfNext -wf -sf
1
2
3
4

Comment each result in the table: either by explaining why the requirement holds under the fairness constraint, or by explaining why the counter-example satisfies the fairness constraint and falsifies the requirement.

Fair ruling

We consider some potential solutions to the cases where fairness conditions do not guarantee satisfaction of the requirements.