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

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

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

StackExchange Computer Science Q#158836, answer score: 2