Modeling in SMV, the Mutual Exclusion Problem

Translate these examples into SMV and check whether each satisfies properties of safety and liveness properties. For some suggestions about modeling Deitel's pseudocode in SMV, see Translating pseudocode to SMV. However, I do not recommend using a "mechanical" translation. For one thing, the purpose of this assignment is to learn how to model relevant system details; for another, a brute-force translation will make it harder to explain the results. The properties to check include:

Safety: The two processes are never in their critical phases at the same time.

Liveness: Should a process attempt to move into its critical phase, it will eventually get to do so.

Nonalternation: There is not a fixed priority. That is, a process may become critical repeatedly if the other process remains nonactive. Another way of saying this is that, should one process die, the other is still able to "go critical."

Your first task is to translate these pseudo-C expressions into SMV models. This requires you to have a semantic interpretation in mind. In all cases, processes p[1] and p[0] are assumed to execute concurrently (either in parallel or as time sharing processes) at an appropriate level of atomicity. This means that, considered as software, a process's basic step involves at most one primitive transaction with a shared variable.

I recommend that you use asynchronous interleaving in your models, but this is not a requirement.

What to turn in

1. In a subdirectory Develop SMV models for the six examples that follow, using names me1.smv, me2.smv ..., me6.smv. For each of these source files, generate SMV outputs using the graphic interface vw.

2. Write a report explaining your results.

   I am not looking for short statements, like "Version 2 isn't safe." If a property fails, study the counterexample to discover how it fails, and then explain it. You are encouraged but not required to use diagrams or other means to present failure scenarios. Nor should you simply copy the SMV outputs (?.out) into your report. It is acceptable to use screen shots of vw panels, but consult the man page to learn how to supress irrelevant traces.

   ---

   In all of his examples, Deitel specifies a process as a procedure P[i], where i is understood to be either 0 or 1. He uses the "trick" of logically negating i with the expression 1-i.

   Version 1

   According to Deitel, this version is safe but not live in the most general sense, because processes are forced to alternate.

   int turn;      /* turn: {0, 1} */
   
   procedure p[i] /* i: {0, 1} */
     {
      while (1) do 
        { 
          NONCRITCIAL;
          while (turn == (1-i)) do {/* nothing */};
          CRITICAL;
          turn = (1-i);
        }
     }
   

   Version 2

   According to Deitel, this version is not safe.

   bool T[2] = {0, 0};       /* Who's trying */
   
   procedure p[i]            /* i: {0, 1} */
     {
      while (1) do
        { 
          NONCRITCIAL;
          while T[1-i] do {/* nothing */;}
          T[i] = 1;
          CRITICAL;
          T[i] = 0;
        }
     }
   

   Version 3

   I leave it to you to figure out what the problem is with this version.

   bool T[2] = {0, 0};       /* Who's trying */
   
   procedure p[i]            /* i: {1, 0} */
    {
     while (1) do
      {
       NONCRITICAL;
       T[i] = 1;
       while T[1-i] do {/* nothing */;}
       CRITICAL;
       T[i] = 0;
      }
    }
   

   Version 4

   This example is interesting because it is close to a basic protocol used in hardware and communications (Ethernet, for example). In other words, it has practical applications even though it is not correct in a strict sense. Be sure to explain in your report how you model RANDOM_DELAY, the idea that the process just waits for a while.

   bool T[2] = {0, 0};       /* Who's trying */
   
   procedure p[i]            /* i: {1, 0} */
    {
     while (1) do
      {
       NONCRITICAL;
       T[i] = 1;
       while T[1-i] do
         {
           T[i] = 0;
           RANDOM_DELAY;
           T[i] = 1;
         }
       CRITICAL
       T[i] = 0;
      }
    }
   

   Version 5 (Dekker's algorithm)

   Deitel claims this protocol, published by E. Dijkstra who attributes it to Dekker, is a solution to two-process mutual exclusion.

   int turn;                 /* turn: {0, 1} */
   bool T[2] = {0, 0};       /* Who's trying */
   
   procedure p[i]            /* i: {1, 0} */
    {
     while (1) do
      {
       NONCRITICAL;
       T[i] = 1;
       while T[1-i] do
        {
          if (turn = (1-i)) then
           {
            T[i] = 0;
            while (turn = (1-i)) do {/* nothing */};
            T[i] = 1;
           }
         }
       CRITICAL;
       turn = 1-i;
       T[i] = 0;
      }
    }
   

   Version 6 (Peterson's algorithm)

   Deitel claims this protocol, due to G. L. Peterson, is a simpler solution.

   int turn;                 /* turn: {0, 1} */
   bool T[2] = {0, 0};       /* Who's trying */
   
   procedure p[i]            /* i: {1, 0} */
    {
     while (1) do
      {
       NONCRITICAL;
       T[i] = 1;
       turn = 1-i;
       while (T[1-i] && turn = (1-i)) do {/* nothing */;}
       CRITICAL;
       T[i] = 0;
      }
    }