Reading the book on Principles of Model Checking by Christel Baier and Joost-Pieter Katoen, on page 43-45, I was reminded about a particular property of Peterson's mutual exclusion algorithm that I forgot from my undergraduate operating systems class, and therefore, I had pondered till I read the book. In particular, I was wondering why the need for the turn variable. Peterson's mutual exclusion algorithm is special in the way that it has the inclusion of a scheduling strategy to ensure the progress of the competing processes. Ha, I really forgot the obvious!

The book first gives an example of mutual exclusion using a semaphore with a notation called Program Graph, which is nice to abstract implementation details, as depicted below:

           |                                     |
           V                                     V
          +---------------+                     +---------------+
          | noncritical_1 |                     | noncritical_2 |
          +---------------+                     +---------------+
           ^    |                                ^    |
           |    |                                |    |
           |    V                                |    V
           |  +-----------+                      |  +-----------+
y := y + 1 |  | wait_1    |           y := y + 1 |  | wait_2    |
           |  +-----------+                      |  +-----------+
           |    |                                |    |
           |    | y > 0 : y := y - 1             |    | y > 0 : y := y - 1
           |    V                                |    V
          +---------------+                     +---------------+
          | critical_1    |                     | critical_2    |
          +---------------+                     +---------------+

Note: S1 ---- g : x ----> S2 means that the state can change from S1 to S2 provided that condition g is satisfied, and if action x exists, the action is carried out atomically along with the test of g.

Initializing y to 1, the above method is sufficient to guarantee mutual exclusion over a critical section for the two competing processes. However, as the book explains, it might be the case that the first process is always given a turn while the second process is kept waiting indefinitely.

The book then provides the solution by illustrating Peterson's mutual exclusion algorithm as the next example in which it is clearly stated that Peterson's algorithm has a built-in scheduling strategy. The program graph of Peterson's algorithm is given as follows:

            |                                      |
            V                                      V
           +---------------+                      +---------------+
           | noncritical_1 |                      | noncritical_2 |
           +---------------+                      +---------------+
            ^    |                                 ^    |
            |    | b1 := true; x := 2              |    | b2 := true; x := 1
            |    V                                 |    V
            |  +-----------+                       |  +-----------+
b1 := false |  | wait_1    |           b2 := false |  | wait_2    |
            |  +-----------+                       |  +-----------+
            |    |                                 |    |
            |    | x = 1 V ~b2                     |    | x = 2 V ~b1
            |    V                                 |    V
           +---------------+                      +---------------+
           | critical_1    |                      | critical_2    |
           +---------------+                      +---------------+

Specifically, b1 indicates that process 1 would like or is in the critical section, b2 indicates that process 2 would like or is in the critical section, and x indicates that whose turn it is now. In this way, process 1 cannot run indefinitely since it is forced to give process 2 a go.

To conclude, I failed to appreciate the beauty of Peterson's mutual exclusion algorithm during my undergraduate OS class. And, I forgot that a critical section cannot only be solved using mutual exclusion alone. Instead, two additional criteria need to be satisfied: progress and bounded waiting. Lastly I find the systematic automatic method by which I can be sure that a section of code is free from race condition: model checking.