Race condition, my doubt on Peterson's algorithm vs. C

Question

I have seen this C code showing an implentation of Peterson's Critical Section algorithm. It is obviously skeletal and hardwired for two threads but the logic is supposed to be correct in detail.

Despite reading and talking I remain with a grain of doubt about the following line (and the similar line for Thread B):

`while (turn == 1 && flag1) skip;

When it is compiled, the while clause will generate multiple instructions which it seems to me can lead to a race condition in a pre-emptive scheduling model.

While I trust the proofs etc. I have not seen a good way to refute my concern.

(I know this is an oldie but goodie so feel free to respond with a link.)

Answer 1

When it is compiled, the while clause will generate multiple instructions which it seems to me can lead to a race condition in a pre-emptive scheduling model.

This is the technical beauty of Peterson's algorithm. Even though there could be many possible execution paths for this short and simple-looking code, it guarantees mutual exclusion, progress and bounded waiting. (Bounded waiting is not guaranteed for more than two participating threads, though).

On first sight, it looks there is a race condition on which thread will set the value of "turn", especially in a pre-emptive scheduling model. However, a close analysis will show neither does this race condition corrupt the mutual exclusion nor does it prevent progress. Here is the basic analysis on mutual exclusion by Wikipedia, adapted for the variable names here.

Thread A and Thread B can never be in their critical sections at the same time. If Thread A is in its critical section, then flag0 is TRUE. In addition,

• either flag1 is FALSE, meaning that Thread B has left its critical section,
• or turn is 0, meaning that Thread B is just now trying to enter its critical section, but graciously waiting,
• or Thread B is right before the line turn = 0, trying to enter its critical section, after setting flag1 to TRUE but before setting turn to 0 and busy waiting.

So if both threads are in their critical sections, then we conclude that the state must satisfy flag0 and flag1 and turn = 0 and turn = 1. No state can satisfy both turn = 0 and turn = 1, so there can be no state where both threads are in their critical sections.

Note that the analysis above is programming-language independent. It does not matter you use C, Java, Python, assembly, etc.

Note that the analysis above only assumes that the code/instruction in each thread is executed/implemented serially. Whether there is a race condition to set turn or whether the scheduling model is pre-emptive does not matter.

As you could have insisted, it is not convincing enough with the explanation above, nor with many similar high-level arguments in textbooks. Currency is too subtle, delicate and illusive for involving propositions to be proved easily, usually.

People have spent great efforts proving propositions involving concurrency (in a pre-emptive scheduling model). For example, Uri Abraham's paper The assertional versus Tarskian methods presents two formal proofs on the correctness of the Peterson's algorithm, together with an enlightening and convincing clarification on what is a formal proof. You will be convinced beyond any doubt if you have finished reading it or just half of it. (I do not remember whether I have finished reading that paper, though.)

Answer 2

For starters, one could model this in one's favourite model-checking language such as Promela and explore the model with spin.

With the basic atomic awaits, the code could look like this

#include "critical3.h"

bool wantp = false, wantq = false, last = 1

active proctype p()
{
  do
    :: non_critical_section('p');
wap:   wantp = true;
       last = 1;
       (!wantq || last == 0);
csp:   critical_section('p');
       wantp = false
  od
}

active proctype q()
{
  do
    :: non_critical_section('q');
waq:   wantq = true;
       last = 0;
       (!wantp || last == 1);
csq:   critical_section('q');
       wantq = false
  od
}

ltl mutex { !<>(p@csp && q@csq) }
ltl dlf   { [](p@wap && q@waq -> <>(p@csp || q@csq)) }
ltl aud   { [](p@wap && ([](!q@waq)) -> <>p@csp) }
ltl ee    { [](p@wap -> <>p@csp) }

where the included critical3.h is

/* 
  Definitions for 2 process critical sections; derived from Ben-Ari's.
*/

inline critical_section(proc) {
     printf("MSC: %c in CS\n", proc);
}

inline non_critical_section(proc) {
  printf("MSC: %c in non-CS\n", proc);
  do                            /* non-deterministically choose how
                                   long to stay, even forever */
    :: true ->
         skip
    :: true ->
         break
  od
}

Here's a version with explicit non-atomic awaits.

#include "critical3.h"

bool wantp = false, wantq = false, last = 1

active proctype p()
{
  do
    :: non_critical_section('p');
wap:   wantp = true;
       last = 1;
tp:    if
         :: !wantq -> goto csp
         :: else
       fi
       if
         :: last == 0 -> goto csp
         :: else -> goto tp
       fi
csp:   critical_section('p');
       wantp = false
  od
}

active proctype q()
{
  do
    :: non_critical_section('q');
waq:   wantq = true;
       last = 0;
tq:    if
         :: !wantp -> goto csq
         :: else -> skip
       fi
       if
         :: last == 1 -> goto csq
         :: else -> goto tq
       fi
csq:   critical_section('q');
       wantq = false
  od
}

ltl mutex { !<>(p@csp && q@csq) }
ltl dlf   { [](p@wap && q@waq -> <>(p@csp || q@csq)) }
ltl aud   { [](p@wap && ([](!q@waq)) -> <>p@csp) }
ltl ee    { [](p@wap -> <>p@csp) }

Exploring these models with spin reveals that both have the 4 claimed properties of a mutual exclusion algorithm, mutual exclusion (formalised as LTL property mutex), _deadlock-freedom (dlf), absence of unnecessary delay (aud), and eventual entry (ee). The last 3 require weak fairness, otherwise the execution could end with the other process doing infinitely many steps in its non-critical section.

Crucially, this model is faithful only for sequentially consistent hardware. Modern multi-core CPUs do not satisfy that assumption. One could use fence instructions to salvage correctness Peterson on architectures with weaker memory models (such as ARM's PSO and Intel's TSO).