0b55f123 |
1 | /* Dolev, Klawe & Rodeh for leader election in unidirectional ring |
2 | * `An O(n log n) unidirectional distributed algorithm for extrema |
3 | * finding in a circle,' J. of Algs, Vol 3. (1982), pp. 245-260 |
4 | */ |
5 | |
6 | #define N 5 /* nr of processes (use 5 for demos) */ |
7 | #define I 3 /* node given the smallest number */ |
8 | #define L 10 /* size of buffer (>= 2*N) */ |
9 | |
10 | mtype = { one, two, winner }; |
11 | chan q[N] = [L] of { mtype, byte}; |
12 | |
13 | byte nr_leaders = 0; |
14 | |
15 | notrace { |
16 | do |
17 | :: q[0]?one,_ |
18 | :: q[0]?two,_ -> break |
19 | od; |
20 | do |
21 | :: q[0]?two,_ |
22 | :: q[0]?winner,_ -> break |
23 | od |
24 | } |
25 | |
26 | proctype node (chan in, out; byte mynumber) |
27 | { bit Active = 1, know_winner = 0; |
28 | byte nr, maximum = mynumber, neighbourR; |
29 | |
30 | xr in; |
31 | xs out; |
32 | |
33 | printf("MSC: %d\n", mynumber); |
34 | out!one(mynumber); |
35 | end: do |
36 | :: in?one(nr) -> |
37 | if |
38 | :: Active -> |
39 | if |
40 | :: nr != maximum -> |
41 | out!two(nr); |
42 | neighbourR = nr |
43 | :: else -> |
44 | /* Raynal p.39: max is greatest number */ |
45 | assert(nr == N); |
46 | know_winner = 1; |
47 | out!winner,nr; |
48 | fi |
49 | :: else -> |
50 | out!one(nr) |
51 | fi |
52 | |
53 | :: in?two(nr) -> |
54 | if |
55 | :: Active -> |
56 | if |
57 | :: neighbourR > nr && neighbourR > maximum -> |
58 | maximum = neighbourR; |
59 | out!one(neighbourR) |
60 | :: else -> |
61 | Active = 0 |
62 | fi |
63 | :: else -> |
64 | out!two(nr) |
65 | fi |
66 | :: in?winner,nr -> |
67 | if |
68 | :: nr != mynumber -> |
69 | printf("MSC: LOST\n"); |
70 | :: else -> |
71 | printf("MSC: LEADER\n"); |
72 | nr_leaders++; |
73 | assert(nr_leaders == 1) |
74 | fi; |
75 | if |
76 | :: know_winner |
77 | :: else -> out!winner,nr |
78 | fi; |
79 | break |
80 | od |
81 | } |
82 | |
83 | init { |
84 | byte proc; |
85 | atomic { |
86 | proc = 1; |
87 | do |
88 | :: proc <= N -> |
89 | run node (q[proc-1], q[proc%N], (N+I-proc)%N+1); |
90 | proc++ |
91 | :: proc > N -> |
92 | break |
93 | od |
94 | } |
95 | } |
96 | |