0.4 Modeling concurrent processes: homework exercises

To keep the problem small, let's assume we have three philosophers.As a slight simplication of some of the following problems, we'll ignore maxims about code reuse, and choose to useseparate procedures for each philsopher's strategy.

• Here is one attempted solution. Repeatedly, each philosopher tries to pick up the left fork,then tries to pick up the right fork, and then eats and drops the forks.A problem with this solution is that it has a race condition -- two philosophers can have the same fork at the same time.
  • Run this code in SPIN. Provide some output from a sample run.
  • Add appropriate assert statements to the code to test for a race condition. If necessary, you may add other codeto keep track of information to use in these assertions.
  • Use SPIN to find a shortest trace illustrating a race condition.
• Here is another attempted solution. It uses the same strategy, except that each fork has a lock.A problem with this solution is that it can deadlock.
  • Use SPIN to show that the previous race conditions cannot happen.
  • Use SPIN to find a shortest trace illustrating deadlock.
  • Recode this version so it uses multiple copies of only a single proctype .
• Informally, deadlock is often viewed in the more restrictive sense of deadlocking on the acquisition of locks.This is equivalent to considering the case where the only guard conditions are those testing boolean locks.In this sense, deadlock can only happen where there are at least two locks involved. The following problems are instances oftwo general strategies for avoiding this: using fewer locks or being careful with locks.In the following, code reuse will not matter -- you may write code using either a single or multiple proctype s.One attempt is to only have a lock for only every other fork.The idea is that each philosopher only needs to grab one lock.
  • Modify the code to do this with an even number of philosophers and forks, say four of each.
  • Does this code have the race condition or deadlock? Use SPIN to determine this.If no, show SPIN's successful output. If yes, find a shortest trace illustrating the problem.
• A well-known solution is to number the forks somehow and ensurethat locks are always obtained in numerical order (instead of always left-then-right).Note: Maintain the provided lock-based code's lock convention of first-acquired last-released.
  • Modify the code to do this.
  • Use SPIN to show that this does not have race conditions or deadlock.
  • Use SPIN to determine whether using a first-acquired first-released protocol has race conditionsor deadlock.
• Assume that philosophers always try to pick up both forks,eat, and then drop both forks, all philsophers use the same strategy, but we have not chosen a particular strategy yet.If we assume weak fairness is enforced and deadlock is avoided, does each philosopher eat repeatedly? What if we assumestrong fairness?