Skip to content

Commit fd5382a

Browse files
muenchnerkindlmuenchnerkindl
committed
added Chang-Roberts algorithm
1 parent 9247d2d commit fd5382a

File tree

2 files changed

+175
-0
lines changed

2 files changed

+175
-0
lines changed

‎specifications/chang_roberts/ChangRoberts.tla

+154
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,154 @@
1+
---------------------------- MODULE ChangRoberts ----------------------------
2+
(***************************************************************************)
3+
(* Algorithm by Chang and Roberts for electing a leader on a *)
4+
(* unidirectional ring. The algorithm originally appeared as *)
5+
(* E. Chang, R. Roberts: An improved algorithm for decentralized *)
6+
(* extrema-finding in circular configurations of processes, *)
7+
(* CACM 22(5): 281-283, 1979. *)
8+
(***************************************************************************)
9+
EXTENDS Naturals
10+
11+
(***************************************************************************)
12+
(* Constant parameters: *)
13+
(* - N is the number of nodes *)
14+
(* - Id(i) denotes the identity of node i *)
15+
(* The algorithm can be initiated by several nodes, and the node with *)
16+
(* the smallest identity will be elected as the leader. *)
17+
(***************************************************************************)
18+
CONSTANTS N, Id(_)
19+
20+
Node == 1 .. N
21+
22+
ASSUME
23+
/\ N \in Nat \ {0}
24+
/\ \A n \in Node : Id(n) \in Nat
25+
/\ \A m,n \in Node : Id(m) = Id(n) => m = n \* IDs are unique
26+
27+
next(n) == IF n=N THEN 1 ELSE n+1 \* successor along the ring
28+
29+
(** Chang-Roberts algorithm written in PlusCal
30+
--algorithm ChangRoberts {
31+
(* msgs[n]: messages waiting to be received by node n *)
32+
variable msgs = [n \in Node |-> {}];
33+
fair process (node \in Node)
34+
variables
35+
(* is this node an initiator: assigned non-deterministically *)
36+
initiator \in BOOLEAN,
37+
state = IF initiator THEN "cand" ELSE "lost"; {
38+
n0: if (initiator) {
39+
\* send own ID to neighbor
40+
msgs[next(self)] := @ \cup {Id(self)};
41+
n1: while (state # "won") {
42+
\* handle some waiting message
43+
with (q \in msgs[self]) {
44+
if (q < Id(self)) { \* received message for smalled ID: pass it on, record loss
45+
state := "lost";
46+
msgs := [msgs EXCEPT ![self] = @ \ {q},
47+
![next(self)] = @ \cup {q}];
48+
}
49+
else { \* don't pass on other messages
50+
msgs := [msgs EXCEPT ![self] = @ \ {q}];
51+
\* the process wins the election if it receives its own ID
52+
if (q = Id(self)) { state := "won"; }
53+
}
54+
} \* end with
55+
} \* end while
56+
} else { \* non-initiator: pass all messages to the neighbor
57+
n2: while (TRUE) {
58+
with (q \in msgs[self]) {
59+
msgs := [msgs EXCEPT ![self] = @ \ {q},
60+
![next(self)] = @ \cup {q}];
61+
} \* end with
62+
} \* end while
63+
} \* end if
64+
} \* end process
65+
} \* end algorithm
66+
**)
67+
\* BEGIN TRANSLATION
68+
VARIABLES msgs, pc, initiator, state
69+
70+
vars == << msgs, pc, initiator, state >>
71+
72+
ProcSet == (Node)
73+
74+
Init == (* Global variables *)
75+
/\ msgs = [n \in Node |-> {}]
76+
(* Process node *)
77+
/\ initiator \in [Node -> BOOLEAN]
78+
/\ state = [self \in Node |-> IF initiator[self] THEN "cand" ELSE "lost"]
79+
/\ pc = [self \in ProcSet |-> "n0"]
80+
81+
n0(self) == /\ pc[self] = "n0"
82+
/\ IF initiator[self]
83+
THEN /\ msgs' = [msgs EXCEPT ![next(self)] = @ \cup {Id(self)}]
84+
/\ pc' = [pc EXCEPT ![self] = "n1"]
85+
ELSE /\ pc' = [pc EXCEPT ![self] = "n2"]
86+
/\ msgs' = msgs
87+
/\ UNCHANGED << initiator, state >>
88+
89+
n1(self) == /\ pc[self] = "n1"
90+
/\ IF state[self] # "won"
91+
THEN /\ \E q \in msgs[self]:
92+
IF q < Id(self)
93+
THEN /\ state' = [state EXCEPT ![self] = "lost"]
94+
/\ msgs' = [msgs EXCEPT ![self] = @ \ {q},
95+
![next(self)] = @ \cup {q}]
96+
ELSE /\ msgs' = [msgs EXCEPT ![self] = @ \ {q}]
97+
/\ IF q = Id(self)
98+
THEN /\ state' = [state EXCEPT ![self] = "won"]
99+
ELSE /\ TRUE
100+
/\ state' = state
101+
/\ pc' = [pc EXCEPT ![self] = "n1"]
102+
ELSE /\ pc' = [pc EXCEPT ![self] = "Done"]
103+
/\ UNCHANGED << msgs, state >>
104+
/\ UNCHANGED initiator
105+
106+
n2(self) == /\ pc[self] = "n2"
107+
/\ \E q \in msgs[self]:
108+
msgs' = [msgs EXCEPT ![self] = @ \ {q},
109+
![next(self)] = @ \cup {q}]
110+
/\ pc' = [pc EXCEPT ![self] = "n2"]
111+
/\ UNCHANGED << initiator, state >>
112+
113+
node(self) == n0(self) \/ n1(self) \/ n2(self)
114+
115+
Next == (\E self \in Node: node(self))
116+
\/ (* Disjunct to prevent deadlock on termination *)
117+
((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)
118+
119+
Spec == /\ Init /\ [][Next]_vars
120+
/\ \A self \in Node : WF_vars(node(self))
121+
122+
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
123+
124+
\* END TRANSLATION
125+
-----------------------------------------------------------------------------
126+
(* type correctness *)
127+
TypeOK ==
128+
/\ pc \in [Node -> {"n0", "n1", "n2", "Done"}]
129+
/\ msgs \in [Node -> SUBSET {Id(n) : n \in Node}]
130+
/\ initiator \in [Node -> BOOLEAN]
131+
/\ state \in [Node -> {"cand", "lost", "won"}]
132+
133+
(***************************************************************************)
134+
(* Safety property: when node n wins the election, it is the initiator *)
135+
(* with the smallest ID, and all other nodes know that they lost. *)
136+
(***************************************************************************)
137+
Correctness ==
138+
\A n \in Node : state[n] = "won" =>
139+
/\ initiator[n]
140+
/\ \A m \in Node \ {n} :
141+
/\ state[m] = "lost"
142+
/\ initiator[m] => Id(m) > Id(n)
143+
144+
(***************************************************************************)
145+
(* Liveness property: if there is an initiator then eventually there *)
146+
(* will be a winner. *)
147+
(***************************************************************************)
148+
Liveness ==
149+
(\E n \in Node : initiator[n]) ~> (\E n \in Node : state[n] = "won")
150+
151+
=============================================================================
152+
\* Modification History
153+
\* Last modified Sun Jun 12 18:33:42 CEST 2016 by merz
154+
\* Created Sat Apr 23 14:05:31 CEST 2016 by merz

‎specifications/chang_roberts/README.md

+21
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
# Chang-Roberts algorithm for leader election in a ring
2+
An early algorithm for electing a leader in a unidirectional ring
3+
appeared as
4+
5+
E. Chang, R. Roberts: An improved algorithm for decentralized extrema-finding
6+
in circular configurations of processes. CACM 22(5): 281-283, 1979.
7+
8+
The module contains a PlusCal version of that algorithm. For verifying it,
9+
create an instance, e.g.
10+
11+
N <- 6
12+
Id(n) <- IF n=1 THEN 12
13+
ELSE IF n=2 THEN 27
14+
ELSE IF n=3 THEN 63
15+
ELSE IF n=4 THEN 3
16+
ELSE IF n=5 THEN 45
17+
ELSE IF n=6 THEN 9
18+
ELSE "error"
19+
20+
and check the invariants TypeOK and Correctness and the temporal logic
21+
property Liveness.

0 commit comments

Comments
 (0)