G52CON: Exercise 5, Proving Correctness

Questions:

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