# 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.

A philosopher does the following sequence of actions repeatedly:

• Think
• Wait for the left fork to be available, then take it
• Wait for the right fork to be available, then take it
• Eat
• Release the left fork
• Realease the right fork

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:

• Think
• P(mutex)
• Take the left and right forks if they are available, then V(mutex)
• Otherwise, V(mutex) and go back thinking
• Eat
• Release the left fork
• Realease the right fork

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.
• Suppose that a fair implementation of the semaphore is used instead. What would be the impact on the previous results?
• What is the impact of replacing await(mutex > 0) (i.e. P(mutex)) by a condition await(mutex > 0 /\ left_fork_is_free /\ right_fork_is_free) on the previous results? (where left_fork_is_free should be replaced by a condition stating that the left fork is free, and similarly for the right fork. The exact definitions depend on your model)
• What should be done to get a model that satisfies the 4 requirements above?