CSCI P415/515 Fri Jan 6 15:18:04 EST 2012 [SDJ]

Homework Assignment

The examples [below] in this assignment are taken from H. M. Deitel's textbook, Operating Systems (Addison Wesley, 2nd ed., 1990). They illustrate various aspects of the two-process mutual exclusion problem through a sequence of not-quite-correct solution attempts. You are to model these examples in SMV and use model checking to verify their properties—both good and bad.

Instructions

  1. Model the six two-process mutual exclusion protocols [below] in SMV, naming the source files me1.smv, me2.smv,  ...  me6.smv.
  2. Formulate and check whether each model satisfies properties of:
    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 do so.
  3. Submit a report, report.pdf, presenting your findings.

    If a protocol fails to satisfy a property, analyze failure scenarios and clearly explain why. Statements like, "Version 2 isn't safe," are not adequate.

    Clarity counts. you may (but are not required to) use sequence diagrams, vw screenshots, or other means to help clarify your explanations. Consult man vw learn how to manage trace information.

Notes and Hints

  1. Your first task is to translate the pseudo-C protocol descriptions into SMV models. This requires you to have a semantic interpretation in mind. Processes p[0] and p[1] are assumed to execute concurrently (in parallel or as time-sharing processes). For these models, an atomic action involves one transaction with a shared variable. Translating Pseudocode to SMV [PDF] describes a general (automatable) technique for synthesizing SMV models from sequential process descriptions at this level of atomicity.
    However,   I do not recommend using a "mechanical" translation in this assignment. For one thing, such a brute-force translation will result in unnecessarily ``noisy'' models, making the analysis and explanation harder. For another, the whole purpose of this assignment is to learn how to identify salient (relevant to the problem) features of system. The example [PDF] (to be discussed in lecture) illustrates ad hoc model synthesis for problems of the kind used in this assignment. It will be discussed in lecture.
  2. Formulate CTL* properties (SPEC formulas) for the safety, liveness, and independence properties described above. These specifications should be the same for every model.
  3. Run vw to analyze the properties.
  4. Write a report named report.pdf. presenting your results.
    Note:   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 may but are not required to use diagrams or other means to more clearly present failure scenarios. It is acceptable to use screen shots of vw panels, but consult the man page to learn how to supress irrelevant traces.

Mutual Exclusion Protocols

 In all of his examples, Deitel specifies a process as a procedure P[i], where boolean value i (0 or 1). The expression "(-i) inverts i, from 0 to 1 or from 1 to 0. An assignment like  turn := (-i)  says, "set turn to the value of the other process's index. [Note 1].

In each version, the statements NONCRITICAL and CRITICAL represent arbitrary regions code. A process in its NONCRITICAL region runs for an indefinite, possibly infinite, period of time. A process in its CRITICAL region runs for an indefinite, but finite, period of time. The portion of the protocol just before the CRITICAL region is often called the entry protool; and the portion just after the exit protocol.

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

bool turn;      /* unspecified no initial value in {0, 1}. */

procedure p[i]  /* i: {0, 1} */
  {
   while (1) do 
     { 
       NONCRITCIAL;
       while (turn == (-i)) do {/* nothing */};
       CRITICAL;
       turn = (-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[-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[-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). Even though it is not correct in a absolute sense, it is "statistically valid." Be sure to explain in your report how you model RANDOM_DELAY, the idea that the process pauses for an 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[-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. 

bool 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[-i] do
     {
       if (turn = (-i)) then
        {
         T[i] = 0;
         while (turn = (-i)) do {/* nothing */};
         T[i] = 1;
        }
      }
    CRITICAL;
    turn = (-i);
    T[i] = 0;
   }
 }

Version 6 (Peterson's algorithm). Deitel claims this protocol, due to G. L. Peterson, is a simpler solution. 

bool 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 = -i;
    while (T[-i] && turn = (-i)) do {/* nothing */;}
    CRITICAL;
    T[i] = 0;
   }
 }

Notes

    [Note 1]. From a formal perspective, it's even worse in the original textbook. Dietel declares the variables as integers, turn: int, and "inverts" them with subtraction, turn := 1 - turn. Fortunately, since inversion is the only operation these variables remain in the range {0, 1}. In the tradition of C programming, he also uses these integers for truth values in while loops and if statements. [BACK]