1 /* Peterson's algorithm for N processes - see Lynch's book, p. 284 */
4 #define N 3 /* nr of processes */
9 byte ncrit; /* auxiliary var to check mutual exclusion */
11 active [N] proctype user()
13 /* without never claims, _pid's are: 0 .. N-1 */
15 k = 0; /* count max N-1 rounds of competition */
21 j = 0; /* for all j != _pid */
28 (flag[j] < k || turn[k] != _pid);
35 :: else -> /* survived all N-1 rounds */
40 assert(ncrit == 1); /* critical section */