Is this solution to the dining philosopher's problem entirely valid?
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.).