G52CON: Solution to Exercise 5, Proving Correctness

// Process 1                           // Process 2

init1;                                 init2;
while(true) {                          while(true) {
    c1 = 0;  // entry protocol             c2 = 0;   // entry protocol
    while (c2 == 0) {};                    while (c1 == 0) {};
    crit1;                                 crit2;
    c1 = 1; // exit protocol               c2 = 1;  // exit protocol
    rem1;                                  rem2;
}                                      }


                       // Shared variables
                       boolean c1 = 1, c2 = 1;

Figure 1
1. Prove that the critical section protocol for 2 processes 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 (and vice versa).

1. when P1 enters its critical section, c1 is 0 and the loop condition in its entry protocol evaluates to false, i.e., c2 is 1
2. c2 only has the value 1 when P2 is not in its critical section (by inspection: c2 is initially 1, and P2 sets it to 0 in its entry protocol and back to 1 in its exit protocol)
3. P2 is therefore not in its critical section when P1 enters crit1
4. for P2 to enter its critical section while P1 is in its critical section, c1 must become 1
5. since P2 can't set c1 to 1, this can only happen when P1 leaves its critical section and sets c1 to 1 in its exit protocol
6. P2 therefore can't enter its critical section while P1 is in its critical section.