Dining Philosoraptors

So a group of five philosoraptors get together for their weekly poker match and decide to order some Chinese food, however they unfortunately only have five chopsticks between them. Each chopstick is between two philosoraptors and they are around a round poker table.

When the Chinese food arrives they will each reach for chopsticks, if one next to them is taken they will hold on to whatever they have and wait for the other. If they get both, they can eat and put them both down again. The question is, are they guaranteed to eat, or may they deadlock.

SABR can be useful in finding concurrency issues such as this. For this example we model these rules to see if a deadlock state is possible.

source | solution

Then we can check if we can reach that state.

source | solution

Even if there was no way to reach that state, deadlock may still be possible and reachable in another state, so we combine our first and second examples to test for this. In this we utilize stage setting in Opt because the information that can be placed in End alone is not sufficient.

Opt(19:20) means option for the last stage since we are testing up to stage 20. Stage setting can also be useful for improving speed and can be used with Req, Opt, Trans, and TransSim. In this code we indicate no one has both chopsticks in the deadlock stage because they would then put them down, relieving deadlock.


source | solution

As we can see from the solution, deadlock is possible by the transitions indicated.