# Is this solution to the dining philosopher's problem entirely valid?

In a question on Stack Overflow, the answer by Patrick Trentin lists the following solution to the dining philosopher's problem:

A possible approach for avoiding deadlock without incurring starvation is to introduce the concept of altruistic philosopher, that is a philosopher which drops the fork that it holds when it realises that he can not eat because the other fork is already used.

Having just one altruistic philosopher is sufficient in order to avoid deadlock, and thus all other philosophers can continue being greedy and attempt to grab as many forks as possible.

However, if you never change who is the altruistic philosopher during your execution, then you might end up with that guy starving himself to death. Thus, the solution is to change the altruistic philosopher infinitely often. A fair strategy is to change it in a round robin fashion each time that one philosopher acts altruistically. In that way, no philosopher is penalised and you can actually verify that no philosopher starves under the fairness condition that the scheduler gives a chance to every philosopher to execute infinitely often.

I was intrigued by this solution because I hadn't heard it before. However, I can find no references to it anywhere in the existing literature.

• I did a quick check, and saw that it isn't listed on Wikipedia as a standard solution.
• Googling 'altruistic philosopher dining' yields only one result from Google Books that does not discuss the round robin strategy and only vaguely alludes to the altruistic philosopher to talk about the perils of starvation.
• I tried looking up altruistic philosopher on ArXiv, only to return no results.
• Trentin cites a book about nuXmv, a symbolic model checker, as his source but only provides a link to his own lab slides.

So my question: does this naive yet seemingly remarkable solution actually work? Or are there pitfalls that have been overlooked? I find it hard to believe that, if it works, it wouldn't have at least some mention somewhere - but at the same time I can't see why it wouldn't work, as it's a fairly naive solution.

If it does work, can I either a) have a reference to a proof, or b) an actual proof that this solves the dining philosopher's problem? If it doesn't, same standards apply, except for the negation of a proof. :)

• Coffman in 1971 wrote about four simultaneous conditions for deadlock - if you break at least one of them - it is like tie breaker. With alteuist there is no more circular wait and your system become preemptive. – Evil Jul 14 '16 at 5:27
• A formal proof can be quite tedious, see for example cs.stackexchange.com/questions/45763/… The techniques are similar here, try proving this yourself. If you are still stuck, i will try to add a proof later, but see the linked post to realize what you are asking (and don't be disappointed if the proof is full of indexes and doesn't give you any special insight, "formal" proofs for the correctness of even supposedly trivial concurrent protocols might surprise you). – Ariel Jul 14 '16 at 15:47
• The word formal appears in quotation since treating concurrent algorithms formally is an entire field, and one must define precisely all the basic notions (e.g. how is time represented). – Ariel Jul 14 '16 at 15:50
• @Ariel Then I will settle for knowledge that a proof or falsification of the validity of the solution exists. :) – Akshat Mahajan Jul 14 '16 at 16:25

The description of an altruistic philosopher given in this answer, that you quoted in your question, is slightly imprecise. What it really is going on is that:

A possible approach for avoiding deadlock without incurring in starvation is to introduce the concept of altruistic philosopher, that is a philosopher which drops the fork that it holds when it realizes that no one can eat because there is a deadlock situation.

So the actual condition for altruism is stronger than the one in your quote. Another important condition is that the fork that is put down by the altruistic philosopher is handed over to the philosopher waiting for it, e.g. by waking up the process that is waiting on the resource. (Otherwise the deadlock situation could actually reappear one instant later).

I apologize for the confusion I may have created in this regard. In my stackoverflow answer I simplified the actual model to convey the basic idea, but this left out some details that are important for "formally proving" the correctness of the solution.

Note: I don't have the time to write down a formal proof in this moment, so I will try to make a simple argument.

The pre-conditions are as follows:

• Ph_i is the altruistic philosopher
• Ph_i holds the left fork and the right fork is hold by its successor Ph_{i+1}
• There must be a deadlock: every Ph_k is holding the left fork

the actions performed are:

• Ph_i gives his left fork to its predecessor Ph_{i-1}

the post-conditions are as follows:

• Ph_{i+1} becomes the new altruistic philosopher
• Ph_{i-1} is now holding two forks and can eat
• After eating, Ph_{i-1} puts down both forks.

The important invariant is that the predecessor of the altruistic philosopher is guaranteed to eat after a deadlock situation.

Given N philosophers, the round robin policy guarantees that each philosopher becomes altruistic exactly once in a sequence of N deadlocks. Hence, each philosopher is guaranteed to eat (at least) once every N deadlocks (because it is the predecessor of an altruistic philosopher exactly once every N deadlocks).

This is, of course, the analysis of the worst-case possible outcome. Depending on the work-load, deadlocks may not arise so frequently and in this case each philosopher would have the chance to eat pretty much anytime it wants.

The naive solution to the dining philosophers presented in this answer is quite effective for the limited purposes of teaching Model Checking / Formal Verification techniques. However, I would not assume that it is the best engineering solution for practical situations because it requires one to detect a deadlock. Also, it may be hard to reduce practical problems to the simple scenario of the dining philosophers (e.g. there could be many more resources involved, the order in which resources are grabbed is not fixed, etc.).

• I'm not sure the stated set of actions is admissible. As far as I know, the admissible set of actions is: 1) try to pick up the left fork 2) put it down 3) try to pick up the right fork 4) put it down. A philosopher can do a lot of internal bookkeeping but cannot communicate with another philosopher other than through these four actions. – reinierpost Nov 21 '19 at 12:33
• @reinierpost that is quite a relevant observation about a potential limitation that may or may not apply depending on who you ask (e.g. Wikipedia lists an arbitrator solution which would not be much different from this). Anyway, that is also one of the reasons why I stated that the solution is probably only academically interesting for the purposes of teaching Model Checking / Formal Verification. There rarely are one-fit-all solutions, after all. – Patrick Trentin Nov 21 '19 at 12:37