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
TRUE. In addition,
FALSE, meaning that
Thread B has left its critical section,
0, meaning that
Thread B is just now trying to enter its critical section, but graciously waiting,
Thread B is right before the line
turn = 0, trying to enter its critical section, after setting
TRUE but before setting
0 and busy waiting.
So if both threads are in their critical sections, then we conclude that the state must satisfy
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.)