-
Notifications
You must be signed in to change notification settings - Fork 200
/
EWD998PCal.tla
170 lines (139 loc) · 7.04 KB
/
EWD998PCal.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
------------------------------- MODULE EWD998PCal -------------------------------
(***************************************************************************)
(* 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. *)
(* https://www.cs.utexas.edu/users/EWD/ewd09xx/EWD998.PDF *)
(***************************************************************************)
EXTENDS Integers, Bags, BagsExt
CONSTANT N
ASSUME NAssumption == N \in Nat \ {0} \* At least one node.
Node == 0 .. N-1
Initiator == 0 \* Any node can be the initiator; 0 has just been conveniently choosen to simplify the definition of token initiation.
(********
--algorithm ewd998 {
variables
(*
Although we know the relationship between the counter and network, modeling network as a set of messages would be too cumbersome.
We have two alternatives for modeling the network: as a bag of messages or as a sequence of messages. Although modeling it as a
sequence may seem more intuitive, we do not require its ordering properties for our purposes. Therefore, we have decided to use a
bag to represent the network. It's worth noting that Distributed Plucal refers to this concept as a "channel".
*)
network = [n \in Node |-> IF n = Initiator THEN SetToBag({[type|-> "tok", q |-> 0, color |-> "black"]}) ELSE EmptyBag];
define {
(*
The passMsg operator is not implementable -at least not without using extra synchronization- because it atomically reads a message
from the nic's in-buffer and writes to its out-buffer!
*)
passMsg(net, from, oldMsg, to, newMsg) == [ net EXCEPT ![from] = BagRemove(@, oldMsg), ![to] = BagAdd(@, newMsg) ]
sendMsg(net, to, msg) == [ net EXCEPT ![to] = BagAdd(@, msg) ]
dropMsg(net, to, msg) == [ net EXCEPT ![to] = BagRemove(@, msg) ]
pendingMsgs(net, rcv) == DOMAIN net[rcv]
}
fair process (node \in Node)
variables active \in BOOLEAN, color = "black", counter = 0;
{
l: while (TRUE) {
either { \* send some payload message to some other node.
when active;
with (to \in Node \ {self}) {
network := sendMsg(network, to, [type|-> "pl"]);
};
counter := counter + 1
} or { \* receive a payload message. Reactivates the node.
with (msg \in pendingMsgs(network, self)) {
when msg.type = "pl";
counter := counter - 1;
active := TRUE;
color := "black";
network := dropMsg(network, self, msg)
}
} or { \* terminate the current node.
active := FALSE
} or { \* pass the token to the next node.
when self # Initiator;
with (tok \in pendingMsgs(network, self)) {
when tok.type = "tok" /\ ~active;
network := passMsg(network, self, tok, self-1, [type|-> "tok", q |-> tok.q + counter, color |-> (IF color = "black" THEN "black" ELSE tok.color)]);
color := "white";
}
} or { \* Initiate token.
when self = Initiator;
with (tok \in pendingMsgs(network, self)) {
when tok.type = "tok" /\ (color = "black" \/ tok.q + counter # 0 \/ tok.color = "black");
network := passMsg(network, self, tok, N-1, [type|-> "tok", q |-> 0, color |-> "white"]);
color := "white";
}
}
}
}
}
********)
\* BEGIN TRANSLATION (chksum(pcal) = "4d658e04" /\ chksum(tla) = "530581e3")
VARIABLE network
(* define statement *)
passMsg(net, from, oldMsg, to, newMsg) == [ net EXCEPT ![from] = BagRemove(@, oldMsg), ![to] = BagAdd(@, newMsg) ]
sendMsg(net, to, msg) == [ net EXCEPT ![to] = BagAdd(@, msg) ]
dropMsg(net, to, msg) == [ net EXCEPT ![to] = BagRemove(@, msg) ]
pendingMsgs(net, rcv) == DOMAIN net[rcv]
VARIABLES active, color, counter
vars == << network, active, color, counter >>
ProcSet == (Node)
Init == (* Global variables *)
/\ network = [n \in Node |-> IF n = Initiator THEN SetToBag({[type|-> "tok", q |-> 0, color |-> "black"]}) ELSE EmptyBag]
(* Process node *)
/\ active \in [Node -> BOOLEAN]
/\ color = [self \in Node |-> "black"]
/\ counter = [self \in Node |-> 0]
node(self) == \/ /\ active[self]
/\ \E to \in Node \ {self}:
network' = sendMsg(network, to, [type|-> "pl"])
/\ counter' = [counter EXCEPT ![self] = counter[self] + 1]
/\ UNCHANGED <<active, color>>
\/ /\ \E msg \in pendingMsgs(network, self):
/\ msg.type = "pl"
/\ counter' = [counter EXCEPT ![self] = counter[self] - 1]
/\ active' = [active EXCEPT ![self] = TRUE]
/\ color' = [color EXCEPT ![self] = "black"]
/\ network' = dropMsg(network, self, msg)
\/ /\ active' = [active EXCEPT ![self] = FALSE]
/\ UNCHANGED <<network, color, counter>>
\/ /\ self # Initiator
/\ \E tok \in pendingMsgs(network, self):
/\ tok.type = "tok" /\ ~active[self]
/\ network' = passMsg(network, self, tok, self-1, [type|-> "tok", q |-> tok.q + counter[self], color |-> (IF color[self] = "black" THEN "black" ELSE tok.color)])
/\ color' = [color EXCEPT ![self] = "white"]
/\ UNCHANGED <<active, counter>>
\/ /\ self = Initiator
/\ \E tok \in pendingMsgs(network, self):
/\ tok.type = "tok" /\ (color[self] = "black" \/ tok.q + counter[self] # 0 \/ tok.color = "black")
/\ network' = passMsg(network, self, tok, N-1, [type|-> "tok", q |-> 0, color |-> "white"])
/\ color' = [color EXCEPT ![self] = "white"]
/\ UNCHANGED <<active, counter>>
Next == (\E self \in Node: node(self))
Spec == /\ Init /\ [][Next]_vars
/\ \A self \in Node : WF_vars(node(self))
\* END TRANSLATION
-----------------------------------------------------------------------------
token ==
LET tpos == CHOOSE i \in Node : \E m \in DOMAIN network[i]: m.type = "tok"
tok == CHOOSE m \in DOMAIN network[tpos] : m.type = "tok"
IN [pos |-> tpos, q |-> tok.q, color |-> tok.color]
pending ==
[n \in Node |-> IF [type|->"pl"] \in DOMAIN network[n] THEN network[n][[type|->"pl"]] ELSE 0]
EWD998 == INSTANCE EWD998
EWD998Spec == EWD998!Init /\ [][EWD998!Next]_EWD998!vars \* Not checking liveness because we cannot easily define fairness for what ewd998 calls system actions.
THEOREM Spec => EWD998Spec
-----------------------------------------------------------------------------
Alias ==
[
network |-> network,
active |-> active,
color |-> color,
counter |-> counter,
token |-> token,
pending |-> pending
]
StateConstraint ==
\A i \in DOMAIN counter : counter[i] < 3
=============================================================================