Skip to content

Commit 1311c92

Browse files
lemmylemmy
committed
*Refine* (not extend as in previous commit) the spec EWD998ChanID to add
shutdown functionality.
1 parent b010c54 commit 1311c92

File tree

1 file changed

+232
-0
lines changed

1 file changed

+232
-0
lines changed

‎specifications/ewd998/EWD998ChanIDTermination.tla

+232
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,232 @@
1+
---------------------- MODULE EWD998ChanIDTermination ----------------------
2+
(***************************************************************************)
3+
(* This spec has the following two notable differences: *)
4+
(* - Add SendTermination and RecvTermination actions that model how the *)
5+
(* Initiator notifies the ring about final termination. *)
6+
(* - Introduce a new message type TrmMsg that the initiator sends to *)
7+
(* notify the other nodes about termination. Here, the initiator *)
8+
(* sends N-1 messages (one to each node), but an implementation could *)
9+
(* e.g. use a broadcast or multicast (which would make for a nice *)
10+
(* example at the PlusPy level) *)
11+
(* *)
12+
(* Minor/Hack: *)
13+
(* - Hacks TypeOK to account for the set of Messages having changed *)
14+
(* without being included in the refinement mapping. *)
15+
(***************************************************************************)
16+
EXTENDS Integers, Sequences, FiniteSets, Naturals, Utils
17+
18+
19+
CONSTANT Nodes
20+
ASSUME IsFiniteSet(Nodes) /\ Nodes # {}
21+
22+
N == Cardinality(Nodes)
23+
24+
\* Choose a node to be the initiator of a fresh token. We don't care which one it
25+
\* is as long as it is always the same.
26+
Initiator == CHOOSE n \in Nodes : TRUE
27+
28+
\* Organize Nodes in a ring.
29+
RingOfNodes ==
30+
CHOOSE r \in [ Nodes -> Nodes ]: IsSimpleCycle(Nodes, r)
31+
32+
Color == {"white", "black"}
33+
34+
VARIABLES
35+
active,
36+
color,
37+
counter,
38+
inbox
39+
40+
vars == <<active, color, counter, inbox>>
41+
42+
EWD998ChanID == INSTANCE EWD998ChanID \* Straight forward refinement mapping
43+
\* because we only *add* functionality.
44+
45+
\* Define a new message type.
46+
TrmMsg == [type |-> "trm"]
47+
48+
\* Wow, this is ugly! It would be cleaner to declare a Message constant in
49+
\* EWD998, but that would mean that its definition has to happen in a TLC
50+
\* model for model checking. A TLC model cannot reference the definitions
51+
\* of TokenMsg and BasicMsg in EWD998.
52+
\*Message == {EWD998ChanID!EWD998Chan!TokenMsg,
53+
\* EWD998ChanID!EWD998Chan!BasicMsg,
54+
\* TrmMsg}
55+
\*
56+
\*\* Poor mans re-define of TypeOK here because we re-defined Message above.
57+
\*TypeOK ==
58+
\* /\ EWD998ChanID!EWD998Chan!TypeOK
59+
\* /\ inbox \in [Nodes -> Seq(Message)]
60+
\*
61+
\* Instead of the hacks above, I've used TLC's definition override to hack
62+
\* TrmMsg into Messages:
63+
\* Message[EWD998ChanId] <-
64+
\* {EWD998ChanID!EWD998Chan!TokenMsg, EWD998ChanID!EWD998Chan!BasicMsg, TrmMsg}
65+
\* This lets us check TypeOK and Inv.
66+
67+
------------------------------------------------------------------------------
68+
69+
Init ==
70+
(* Rule 0 *)
71+
/\ counter = [n \in Nodes |-> 0] \* c properly initialized
72+
/\ inbox = [n \in Nodes |-> IF n = Initiator
73+
THEN << [type |-> "tok", q |-> 0, color |-> "black" ] >>
74+
ELSE <<>>] \* with empty channels.
75+
(* EWD840 *)
76+
/\ active \in [Nodes -> BOOLEAN]
77+
/\ color \in [Nodes -> Color]
78+
79+
InitiateProbe ==
80+
/\ \A j \in 1..Len(inbox[Initiator]) :
81+
/\ inbox[Initiator][j].type # "trm"
82+
(* Rule 1 *)
83+
/\ \E j \in 1..Len(inbox[Initiator]):
84+
\* Token is at node the Initiator.
85+
/\ inbox[Initiator][j].type = "tok"
86+
/\ \* Previous round inconsistent, if:
87+
\/ inbox[Initiator][j].color = "black"
88+
\/ color[Initiator] = "black"
89+
\* Implicit stated in EWD998 as c0 + q > 0 means that termination has not
90+
\* been achieved: Initiate a probe if the token's color is white but the
91+
\* number of in-flight messages is not zero.
92+
\/ counter[Initiator] + inbox[Initiator][j].q # 0
93+
/\ inbox' = [inbox EXCEPT ![RingOfNodes[Initiator]] = Append(@,
94+
[type |-> "tok", q |-> 0,
95+
(* Rule 6 *)
96+
color |-> "white"]),
97+
![Initiator] = RemoveAt(@, j) ] \* consume token message from inbox[0].
98+
(* Rule 6 *)
99+
/\ color' = [ color EXCEPT ![Initiator] = "white" ]
100+
\* The state of the nodes remains unchanged by token-related actions.
101+
/\ UNCHANGED <<active, counter>>
102+
103+
PassToken(n) ==
104+
(* Rule 2 *)
105+
/\ ~ active[n] \* If machine i is active, keep the token.
106+
/\ \E j \in 1..Len(inbox[n]) :
107+
/\ inbox[n][j].type = "tok"
108+
\* the machine nr.i+1 transmits the token to machine nr.i under q := q + c[i+1]
109+
/\ LET tkn == inbox[n][j]
110+
IN inbox' = [inbox EXCEPT ![RingOfNodes[n]] =
111+
Append(@, [tkn EXCEPT !.q = tkn.q + counter[n],
112+
!.color = IF color[n] = "black"
113+
THEN "black"
114+
ELSE tkn.color]),
115+
![n] = RemoveAt(@, j) ] \* pass on the token.
116+
(* Rule 7 *)
117+
/\ color' = [ color EXCEPT ![n] = "white" ]
118+
\* The state of the nodes remains unchanged by token-related actions.
119+
/\ UNCHANGED <<active, counter>>
120+
121+
System(n) == \/ /\ n = Initiator
122+
/\ InitiateProbe
123+
\/ /\ n # Initiator
124+
/\ PassToken(n)
125+
126+
-----------------------------------------------------------------------------
127+
128+
SendMsg(n) ==
129+
\* Only allowed to send msgs if node i is active.
130+
/\ active[n]
131+
(* Rule 0 *)
132+
/\ counter' = [counter EXCEPT ![n] = @ + 1]
133+
\* Non-deterministically choose a receiver node.
134+
/\ \E j \in Nodes \ {n} :
135+
\* Send a message (not the token) to j.
136+
/\ inbox' = [inbox EXCEPT ![j] = Append(@, [type |-> "pl" ] ) ]
137+
\* Note that we don't blacken node i as in EWD840 if node i
138+
\* sends a message to node j with j > i
139+
/\ UNCHANGED <<active, color>>
140+
141+
\* RecvMsg could write the incoming message to a (Java) buffer from which the (Java) implementation consumes it.
142+
RecvMsg(n) ==
143+
(* Rule 0 *)
144+
/\ counter' = [counter EXCEPT ![n] = @ - 1]
145+
(* Rule 3 *)
146+
/\ color' = [ color EXCEPT ![n] = "black" ]
147+
\* Receipt of a message activates node n.
148+
/\ active' = [ active EXCEPT ![n] = TRUE ]
149+
\* Consume a message (not the token!).
150+
/\ \E j \in 1..Len(inbox[n]) :
151+
/\ inbox[n][j].type = "pl"
152+
/\ inbox' = [inbox EXCEPT ![n] = RemoveAt(@, j) ]
153+
/\ UNCHANGED <<>>
154+
155+
Deactivate(n) ==
156+
/\ active[n]
157+
/\ active' = [active EXCEPT ![n] = FALSE]
158+
/\ UNCHANGED <<color, inbox, counter>>
159+
160+
Environment(n) ==
161+
\/ SendMsg(n)
162+
\/ RecvMsg(n)
163+
\/ Deactivate(n)
164+
165+
-----------------------------------------------------------------------------
166+
167+
(* *)
168+
SendTermination ==
169+
\* Don't send termination message multiple times. If - due to a
170+
\* cosmic ray - the initiator doesn't correctly terminate, don't
171+
\* let it interfere with future systems...
172+
/\ \A j \in 1..Len(inbox[Initiator]) :
173+
/\ inbox[Initiator][j].type # "trm"
174+
\* Safra's termination conditions:
175+
/\ active[Initiator] = FALSE
176+
/\ color[Initiator] = "white"
177+
/\ \E j \in 1..Len(inbox[Initiator]) :
178+
/\ inbox[Initiator][j].type = "tok"
179+
/\ inbox[Initiator][j].color = "white"
180+
/\ counter[Initiator] + inbox[Initiator][j].q = 0
181+
\* Don't remove the token msg from inbox[Initiator]
182+
\* because it would mess up Inv, i.e. tpos.
183+
\* /\ inbox' = [inbox EXCEPT ![n] = RemoveAt(@, j) ]
184+
\* Send termination message to all nodes (including self).
185+
/\ inbox' = [ node \in Nodes |-> inbox[node] \o <<TrmMsg>>]
186+
\* TODO: Doesn't this re-enable the InitiateProbe action above?
187+
\* Account for the new messages sent.
188+
/\ counter' = [counter EXCEPT ![Initiator] = N]
189+
\* The state of the nodes remains unchanged by token-related actions.
190+
/\ UNCHANGED <<active, color>>
191+
192+
(* Override with Sys.exit in PlusPy to gracefully terminate the runtime. *)
193+
Terminate(n) == TRUE \*PrintT("sys.exit")
194+
195+
(* *)
196+
RecvTermination(n) ==
197+
/\ \E j \in 1..Len(inbox[n]) :
198+
/\ inbox[n][j].type = "trm"
199+
/\ Terminate(n)
200+
/\ UNCHANGED vars
201+
202+
Termination(n) ==
203+
\/ /\ n = Initiator
204+
/\ SendTermination
205+
\/ /\ n # Initiator
206+
/\ RecvTermination(n)
207+
208+
------------------------------------------------------------------------------
209+
210+
Next(n) ==
211+
\/ System(n)
212+
\/ Environment(n)
213+
\/ Termination(n)
214+
215+
Spec ==
216+
Init /\ [][\E n \in Nodes: Next(n)]_vars
217+
/\ \A n \in Nodes:
218+
/\ WF_vars(System(n))
219+
/\ WF_vars(Environment(n))
220+
/\ WF_vars(Termination(n))
221+
222+
------------------------------------------------------------------------------
223+
224+
\* Iff - from some point onward - none of the nodes send out
225+
\* payload messages, all nodes will eventually terminate.
226+
TerminationMessagesIfNoPayloadMessages ==
227+
<>[][\A n \in Nodes : ~ SendMsg(n)]_vars =>
228+
<>[][\A n \in Nodes : RecvTermination(n)]_vars
229+
230+
THEOREM Spec => TerminationMessagesIfNoPayloadMessages
231+
232+
=============================================================================

0 commit comments

Comments
 (0)