# 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.

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