How do I prove whether or not a dining philosophers suffers from deadlock or starvation possibilities? Where to start?

I have a homework task to prove whether or not a particular variation on the dining philosophers problem suffers from deadlock or starvation. I suspect that the situation does not suffer at all from either but I'm finding this tricky to prove and I 开发者_开发百科don't really know where to start. Is there a general strategy for attacking this sort of problem?

---

You can read about Wait-for graphs (more details here) which are DAGs (Directed Acyclic Graphs) and are used to detect deadlocks.

cheers

---

For a start, I would be very surprised to hear there is a general strategy to solve the problem which is not so abstract as to be useless.

Now, showing the variation is safe is much, much easier than proving it: your task is to prove the variation is safe? If so, you might minimize the number of parts (reduce the number of philosophers to two or maybe three) and try ta apply one or more formal verification methods.

In practice, formal verification is so rare that I might illustrate it best with an example: I've talked with people working on software used in nuclear facilities (haven't gone into the details) and when I asked if they use formal verification, I got "well, yes, we should [be using it]..."