0b55f123 |
1 | /* Peterson's algorithm for N processes - see Lynch's book, p. 284 */ |
2 | |
3 | #ifndef N |
4 | #define N 3 /* nr of processes */ |
5 | #endif |
6 | |
7 | byte turn[N], flag[N]; |
8 | |
9 | byte ncrit; /* auxiliary var to check mutual exclusion */ |
10 | |
11 | active [N] proctype user() |
12 | { byte j, k; |
13 | /* without never claims, _pid's are: 0 .. N-1 */ |
14 | again: |
15 | k = 0; /* count max N-1 rounds of competition */ |
16 | do |
17 | :: k < N-1 -> |
18 | flag[_pid] = k; |
19 | turn[k] = _pid; |
20 | |
21 | j = 0; /* for all j != _pid */ |
22 | do |
23 | :: j == _pid -> |
24 | j++ |
25 | :: j != _pid -> |
26 | if |
27 | :: j < N -> |
28 | (flag[j] < k || turn[k] != _pid); |
29 | j++ |
30 | :: j >= N -> |
31 | break |
32 | fi |
33 | od; |
34 | k++ |
35 | :: else -> /* survived all N-1 rounds */ |
36 | break |
37 | od; |
38 | |
39 | ncrit++; |
40 | assert(ncrit == 1); /* critical section */ |
41 | ncrit--; |
42 | |
43 | flag[_pid] = 0; |
44 | goto again |
45 | } |