G52CON 2008-2009: Solution to Exercise 5, Proving Correctness

    
    // Process 1                           // Process 2
    
    init1;                                 init2;
    while(true) {                          while(true) {
        c1 = true;  // entry protocol          c2 = true;   // entry protocol
        turn = 2;                              turn = 1;
        while (c2 && turn == 2) {};            while (c1 && turn == 1) {};
        crit1;                                 crit2;
        c1 = false; // exit protocol           c2 = false;  // exit protocol
        rem1;                                  rem2;
    }                                      }
    
    
                           // Shared variables
                           boolean c1 = false, c2 = false;
                           integer turn = 1;
    

    Figure 1

  1. Prove that the critical section protocol for 2 processes based on Petersen's Algorithm shown in Figure 1 above satisfies the Mutual Exclusion property.

We need to show that P1 in crit1 implies that P2 is not in crit2.

Proof by contradiction:

  1. when P1 entered crit1, c1 was true and the loop condition evaluated to false, i.e.:
    1. c2 == false and turn == 1 or
    2. c2 == false and turn == 2 or
    3. c2 == false and turn == 1
  2. for P2 to enter its critical section while P1 is in crit1, turn must be equal to 2
  3. turn must have been 2 when P1 entered crit1
  4. c2 must have been false when P1 entered crit1
  5. when P1 entered crit1, P2 had not executed its entry protocol
  6. when P2 enters crit2, turn must be 1
  7. contradiction

Notes

  1. c1 is set in the entry protocol and is not reset until P1 exits its critical section. For the loop condition in the entry protocol to evaluate to false, either c2 must be false or turn must be 1 or both.
  2. Since c1 is true when P1 enters its critical section and is not reset, the only way P2 can complete its entry protocol is if turn == 2, otherwise P2 would spin in the loop in its entry protocol.
  3. P2 can't set turn to 2 and P1 can't change the value of turn when it is in its critical section.
  4. From case 1(b) above: if turn was 2 when P1 entered crit1, c2 must have been false for the loop condition in its entry protocol to evaluate to false.
  5. c2 is only false outside P2's entry and exit protocols. If P2 had executed its entry protocol it would have set c2 to true.
  6. When P2 does execute its entry protocol, it must set turn to 1.
  7. This contradicts the assumption in step 2.