-
Notifications
You must be signed in to change notification settings - Fork 200
/
EWD998Chan.tla
194 lines (165 loc) · 8.07 KB
/
EWD998Chan.tla
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
----------------------------- MODULE EWD998Chan -----------------------------
(***************************************************************************)
(* TLA+ specification of an algorithm for distributed termination *)
(* detection on a ring, due to Shmuel Safra, published as EWD 998: *)
(* Shmuel Safra's version of termination detection. *)
(* Contrary to EWD998, this variant models message channels as sequences. *)
(***************************************************************************)
EXTENDS Integers, Sequences, FiniteSets, Utils
CONSTANT N
ASSUME NAssumption == N \in Nat \ {0} \* At least one node.
Node == 0 .. N-1
Color == {"white", "black"}
VARIABLES
active,
color,
counter,
inbox
vars == <<active, color, counter, inbox>>
TokenMsg == [type : {"tok"}, q : Int, color : Color]
BasicMsg == [type : {"pl"}]
Message == TokenMsg \cup BasicMsg
TypeOK ==
/\ counter \in [Node -> Int]
/\ active \in [Node -> BOOLEAN]
/\ color \in [Node -> Color]
/\ inbox \in [Node -> Seq(Message)]
\* There is always exactly one token (singleton-type).
/\ \E i \in Node : \E j \in 1..Len(inbox[i]): inbox[i][j].type = "tok"
/\ \A i,j \in Node : \A k \in 1 .. Len(inbox[i]) : \A l \in 1 .. Len(inbox[j]) :
inbox[i][k].type = "tok" /\ inbox[j][l].type = "tok"
=> i = j /\ k = l
------------------------------------------------------------------------------
Init ==
(* Rule 0 *)
/\ counter = [i \in Node |-> 0] \* c properly initialized
\* /\ inbox = [i \in Node |-> IF i = 0
\* THEN << [type |-> "tok", q |-> 0, color |-> "black" ] >>
\* ELSE <<>>] \* with empty channels.
\* The token may be at any node of the ring initially.
/\ inbox \in { f \in
[ Node -> {<<>>, <<[type |-> "tok", q |-> 0, color |-> "black" ]>> } ] :
Cardinality({ i \in DOMAIN f: f[i] # <<>> }) = 1 }
(* EWD840 *)
/\ active \in [Node -> BOOLEAN]
/\ color \in [Node -> Color]
InitiateProbe ==
(* Rule 1 *)
/\ \E j \in 1..Len(inbox[0]):
\* Token is at node 0.
/\ inbox[0][j].type = "tok"
/\ \* Previous round inconsistent, if:
\/ inbox[0][j].color = "black"
\/ color[0] = "black"
\* Implicit stated in EWD998 as c0 + q > 0 means that termination has not
\* been achieved: Initiate a probe if the token's color is white but the
\* number of in-flight messages is not zero.
\/ counter[0] + inbox[0][j].q # 0
/\ inbox' = [inbox EXCEPT ![N-1] = Append(@,
[type |-> "tok", q |-> 0,
(* Rule 6 *)
color |-> "white"]),
![0] = RemoveAt(@, j) ] \* consume token message from inbox[0].
(* Rule 6 *)
/\ color' = [ color EXCEPT ![0] = "white" ]
\* The state of the nodes remains unchanged by token-related actions.
/\ UNCHANGED <<active, counter>>
PassToken(i) ==
(* Rule 2 *)
/\ ~ active[i] \* If machine i is active, keep the token.
/\ \E j \in 1..Len(inbox[i]) :
/\ inbox[i][j].type = "tok"
\* the machine nr.i+1 transmits the token to machine nr.i under q := q + c[i+1]
/\ LET tkn == inbox[i][j]
IN inbox' = [inbox EXCEPT ![i-1] =
Append(@, [tkn EXCEPT !.q = tkn.q + counter[i],
!.color = IF color[i] = "black"
THEN "black"
ELSE tkn.color]),
![i] = RemoveAt(@, j) ] \* pass on the token.
(* Rule 7 *)
/\ color' = [ color EXCEPT ![i] = "white" ]
\* The state of the nodes remains unchanged by token-related actions.
/\ UNCHANGED <<active, counter>>
System == \/ InitiateProbe
\/ \E i \in Node \ {0} : PassToken(i)
-----------------------------------------------------------------------------
SendMsg(i) ==
\* Only allowed to send msgs if node i is active.
/\ active[i]
(* Rule 0 *)
/\ counter' = [counter EXCEPT ![i] = @ + 1]
\* Non-deterministically choose a receiver node.
/\ \E j \in Node \ {i} :
\* Send a message (not the token) to j.
/\ inbox' = [inbox EXCEPT ![j] = Append(@, [type |-> "pl" ] ) ]
\* Note that we don't blacken node i as in EWD840 if node i
\* sends a message to node j with j > i
/\ UNCHANGED <<active, color>>
RecvMsg(i) ==
(* Rule 0 *)
/\ counter' = [counter EXCEPT ![i] = @ - 1]
(* Rule 3 *)
/\ color' = [ color EXCEPT ![i] = "black" ]
\* Receipt of a message activates i.
/\ active' = [ active EXCEPT ![i] = TRUE ]
\* Consume a message (not the token!).
/\ \E j \in 1..Len(inbox[i]) :
/\ inbox[i][j].type = "pl"
/\ inbox' = [inbox EXCEPT ![i] = RemoveAt(@, j) ]
/\ UNCHANGED <<>>
Deactivate(i) ==
/\ active[i]
/\ active' = [active EXCEPT ![i] = FALSE]
/\ UNCHANGED <<color, inbox, counter>>
Environment == \E i \in Node : SendMsg(i) \/ RecvMsg(i) \/ Deactivate(i)
-----------------------------------------------------------------------------
Next ==
System \/ Environment
Spec == Init /\ [][Next]_vars /\ WF_vars(System)
-----------------------------------------------------------------------------
(***************************************************************************)
(* The number of incoming messages of a node's given inbox. *)
(***************************************************************************)
NumberOfMsg(ibx) ==
Len(SelectSeq(ibx, LAMBDA msg: msg.type = "pl"))
(***************************************************************************)
(* Bound the otherwise infinite state space that TLC has to check. *)
(***************************************************************************)
StateConstraint ==
/\ \A i \in DOMAIN inbox : NumberOfMsg(inbox[i]) < 3
\* /\ \A i \in DOMAIN inbox : Len(inbox[i]) < 3
\* Even with the number of in-flight messages restricted, we need a bound
\* on the number of messages ever sent to exclude behaviors where two or
\* more nodes forever alternate between send, receive, send, ...
/\ \A i \in DOMAIN counter : counter[i] <= 3
-----------------------------------------------------------------------------
(***************************************************************************)
(* tpos \in Node s.t. the node's inbox contains the token. *)
(***************************************************************************)
tpos ==
CHOOSE i \in Node : \E j \in 1..Len(inbox[i]) : inbox[i][j].type = "tok"
token ==
LET idx == CHOOSE i \in 1 .. Len(inbox[tpos]): inbox[tpos][i].type = "tok"
IN inbox[tpos][idx]
(***************************************************************************)
(* EWD998 with channels refines EWD998 that models channels as sets. *)
(***************************************************************************)
EWD998 == INSTANCE EWD998 WITH token <-
[pos |-> tpos,
q |-> token.q,
color |-> token.color],
pending <-
\* Count the in-flight "pl" messages. The
\* inbox variable represents a node's network
\* interface that receives arbitrary messages.
\* However, EWD998 only "tracks" payload (pl)
\* messages.
[n \in Node |->
Len(SelectSeq(inbox[n],
LAMBDA msg: msg.type = "pl")) ]
\* TLC config doesn't accept the expression EWD998!Spec for PROPERTY.
\* Model-checked for N=3 and StateConstraint above on a laptop in ~15min.
EWD998Spec == EWD998!Spec
THEOREM Spec => EWD998Spec
=============================================================================