Skip to content

Commit 97e0673

Browse files
muenchnerkindlmuenchnerkindl
committed
added EWD 840 and moved sums_even to a subdirectory
1 parent a56ec47 commit 97e0673

File tree

4 files changed

+254
-0
lines changed

4 files changed

+254
-0
lines changed

‎specifications/ewd840/EWD840.tla

+244
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,244 @@
1+
------------------------------- MODULE EWD840 -------------------------------
2+
(***************************************************************************)
3+
(* TLA+ specification of an algorithm for distributed termination *)
4+
(* detection on a ring, due to Dijkstra, published as EWD 840: *)
5+
(* Derivation of a termination detection algorithm for distributed *)
6+
(* computations (with W.H.J.Feijen and A.J.M. van Gasteren). *)
7+
(***************************************************************************)
8+
EXTENDS Naturals, TLAPS
9+
10+
CONSTANT N
11+
ASSUME NAssumption == N \in Nat \ {0}
12+
13+
VARIABLES active, color, tpos, tcolor
14+
15+
Nodes == 0 .. N-1
16+
Color == {"white", "black"}
17+
18+
TypeOK ==
19+
/\ active \in [Nodes -> BOOLEAN] \* status of nodes (active or passive)
20+
/\ color \in [Nodes -> Color] \* color of nodes
21+
/\ tpos \in Nodes \* token position
22+
/\ tcolor \in Color \* token color
23+
24+
(* Initially the token is black. The other variables may take
25+
any "type-correct" values. *)
26+
Init ==
27+
/\ active \in [Nodes -> BOOLEAN]
28+
/\ color \in [Nodes -> Color]
29+
/\ tpos \in Nodes
30+
/\ tcolor = "black"
31+
32+
(* Node 0 may initiate a probe when it has the token and
33+
when either it is black or the token is black. It passes
34+
a white token to node N-1 and paints itself white. *)
35+
InitiateProbe ==
36+
/\ tpos = 0
37+
/\ tcolor = "black" \/ color[0] = "black"
38+
/\ tpos' = N-1
39+
/\ tcolor' = "white"
40+
/\ active' = active
41+
/\ color' = [color EXCEPT ![0] = "white"]
42+
43+
(* A node i different from 0 that possesses the token may pass
44+
it to node i-1 under the following circumstances:
45+
- node i is inactive or
46+
- node i is colored black or
47+
- the token is black.
48+
Note that the last two conditions will result in an
49+
inconclusive round, since the token will be black.
50+
The token will be stained if node i is black, otherwise
51+
its color is unchanged. Node i will be made white. *)
52+
PassToken(i) ==
53+
/\ tpos = i
54+
/\ ~ active[i] \/ color[i] = "black" \/ tcolor = "black"
55+
/\ tpos' = i-1
56+
/\ tcolor' = IF color[i] = "black" THEN "black" ELSE tcolor
57+
/\ active' = active
58+
/\ color' = [color EXCEPT ![i] = "white"]
59+
60+
(* token passing actions controlled by the termination detection algorithm *)
61+
System == InitiateProbe \/ \E i \in Nodes \ {0} : PassToken(i)
62+
63+
(* An active node i may activate another node j by sending it
64+
a message. If j>i (hence activation goes against the direction
65+
of the token being passed), then node i becomes black. *)
66+
SendMsg(i) ==
67+
/\ active[i]
68+
/\ \E j \in Nodes \ {i} :
69+
/\ active' = [active EXCEPT ![j] = TRUE]
70+
/\ color' = [color EXCEPT ![i] = IF j>i THEN "black" ELSE @]
71+
/\ UNCHANGED <<tpos, tcolor>>
72+
73+
(* Any active node may become inactive at any moment. *)
74+
Deactivate(i) ==
75+
/\ active[i]
76+
/\ active' = [active EXCEPT ![i] = FALSE]
77+
/\ UNCHANGED <<color, tpos, tcolor>>
78+
79+
(* actions performed by the underlying algorithm *)
80+
Environment == \E i \in Nodes : SendMsg(i) \/ Deactivate(i)
81+
82+
(* next-state relation: disjunction of above actions *)
83+
Next == System \/ Environment
84+
85+
vars == <<active, color, tpos, tcolor>>
86+
87+
Spec == Init /\ [][Next]_vars /\ WF_vars(System)
88+
89+
-----------------------------------------------------------------------------
90+
91+
(***************************************************************************)
92+
(* Non-properties, useful for validating the specification with TLC. *)
93+
(***************************************************************************)
94+
TokenAlwaysBlack == tcolor = "black"
95+
96+
NeverChangeColor == [][ UNCHANGED color ]_vars
97+
98+
(***************************************************************************)
99+
(* Main safety property: if there is a white token at node 0 then every *)
100+
(* node is inactive. *)
101+
(***************************************************************************)
102+
terminationDetected ==
103+
/\ tpos = 0 /\ tcolor = "white"
104+
/\ color[0] = "white" /\ ~ active[0]
105+
106+
TerminationDetection ==
107+
terminationDetected => \A i \in Nodes : ~ active[i]
108+
109+
(***************************************************************************)
110+
(* Liveness property: termination is eventually detected. *)
111+
(***************************************************************************)
112+
Liveness ==
113+
(\A i \in Nodes : ~ active[i]) ~> terminationDetected
114+
115+
(***************************************************************************)
116+
(* The following property asserts that when every process always *)
117+
(* eventually terminates then eventually termination will be detected. *)
118+
(* It does not hold since processes can wake up each other. *)
119+
(***************************************************************************)
120+
FalseLiveness ==
121+
(\A i \in Nodes : []<> ~ active[i]) ~> terminationDetected
122+
123+
(***************************************************************************)
124+
(* The following property says that eventually all nodes will terminate *)
125+
(* assuming that from some point onwards no messages are sent. It is *)
126+
(* not supposed to hold: any node may indefinitely perform local *)
127+
(* computations. However, this property is verified if the fairness *)
128+
(* condition WF_vars(Next) is used instead of only WF_vars(System) that *)
129+
(* requires fairness of the actions controlled by termination detection. *)
130+
(***************************************************************************)
131+
SpecWFNext == Init /\ [][Next]_vars /\ WF_vars(Next)
132+
AllNodesTerminateIfNoMessages ==
133+
<>[][\A i \in Nodes : ~ SendMsg(i)]_vars => <>(\A i \in Nodes : ~ active[i])
134+
135+
(***************************************************************************)
136+
(* Dijkstra's inductive invariant *)
137+
(***************************************************************************)
138+
Inv ==
139+
\/ P0:: \A i \in Nodes : tpos < i => ~ active[i]
140+
\/ P1:: \E j \in 0 .. tpos : color[j] = "black"
141+
\/ P2:: tcolor = "black"
142+
143+
(***************************************************************************)
144+
(* Use the following specification to check that the predicate *)
145+
(* TypeOK /\ Inv is inductive for EWD 840: verify that it is an *)
146+
(* (ordinary) invariant of a specification obtained by replacing the *)
147+
(* initial condition by that conjunction. *)
148+
(***************************************************************************)
149+
CheckInductiveSpec == TypeOK /\ Inv /\ [][Next]_vars
150+
-----------------------------------------------------------------------------
151+
(***************************************************************************)
152+
(* Interactive proof of safety using TLAPS. *)
153+
(***************************************************************************)
154+
155+
(***************************************************************************)
156+
(* The algorithm is type-correct: TypeOK is an inductive invariant. *)
157+
(***************************************************************************)
158+
LEMMA TypeCorrect == Spec => []TypeOK
159+
<1>1. Init => TypeOK
160+
BY DEF Init, TypeOK, Color
161+
<1>2. TypeOK /\ [Next]_vars => TypeOK'
162+
BY NAssumption DEF TypeOK, Color, Nodes, vars, Next, System, Environment,
163+
InitiateProbe, PassToken, SendMsg, Deactivate
164+
<1>. QED BY <1>1, <1>2, PTL DEF Spec
165+
166+
167+
(***************************************************************************)
168+
(* Follows a more detailed proof of the same lemma. It illustrates how *)
169+
(* proofs can be decomposed hierarchically. Use the "Decompose Proof" *)
170+
(* command (C-G C-D) to prepare the skeleton of the level-2 steps. *)
171+
(***************************************************************************)
172+
LEMMA Spec => []TypeOK
173+
<1>1. Init => TypeOK
174+
BY DEF Init, TypeOK, Color
175+
<1>2. TypeOK /\ [Next]_vars => TypeOK'
176+
<2> SUFFICES ASSUME TypeOK,
177+
[Next]_vars
178+
PROVE TypeOK'
179+
OBVIOUS
180+
<2>. USE NAssumption DEF TypeOK, Nodes, Color
181+
<2>1. CASE InitiateProbe
182+
BY <2>1 DEF InitiateProbe
183+
<2>2. ASSUME NEW i \in Nodes \ {0},
184+
PassToken(i)
185+
PROVE TypeOK'
186+
BY <2>2 DEF PassToken
187+
<2>3. ASSUME NEW i \in Nodes,
188+
SendMsg(i)
189+
PROVE TypeOK'
190+
BY <2>3 DEF SendMsg
191+
<2>4. ASSUME NEW i \in Nodes,
192+
Deactivate(i)
193+
PROVE TypeOK'
194+
BY <2>4 DEF Deactivate
195+
<2>5. CASE UNCHANGED vars
196+
BY <2>5 DEF vars
197+
<2>. QED
198+
BY <2>1, <2>2, <2>3, <2>4, <2>5 DEF Environment, Next, System
199+
<1>. QED BY <1>1, <1>2, PTL DEF Spec
200+
201+
(***************************************************************************)
202+
(* Prove the main soundness property of the algorithm by (1) proving that *)
203+
(* Inv is an inductive invariant and (2) that it implies correctness. *)
204+
(***************************************************************************)
205+
THEOREM Safety == Spec => []TerminationDetection
206+
<1>1. Init => Inv
207+
BY NAssumption DEF Init, Inv, Nodes
208+
<1>2. TypeOK /\ Inv /\ [Next]_vars => Inv'
209+
BY NAssumption
210+
DEF TypeOK, Inv, Next, vars, Nodes, Color,
211+
System, Environment, InitiateProbe, PassToken, SendMsg, Deactivate
212+
<1>3. Inv => TerminationDetection
213+
BY NAssumption DEF Inv, TerminationDetection, terminationDetected, Nodes
214+
<1>. QED
215+
BY <1>1, <1>2, <1>3, TypeCorrect, PTL DEF Spec
216+
217+
218+
(***************************************************************************)
219+
(* Step <1>3 of the above proof shows that Dijkstra's invariant implies *)
220+
(* TerminationDetection. If you find that one-line proof too obscure, here *)
221+
(* is a more detailed, hierarchical proof of that same implication. *)
222+
(***************************************************************************)
223+
LEMMA Inv => TerminationDetection
224+
<1>1. SUFFICES ASSUME tpos = 0, tcolor = "white",
225+
color[0] = "white", ~ active[0],
226+
Inv
227+
PROVE \A i \in Nodes : ~ active[i]
228+
BY <1>1 DEF TerminationDetection, terminationDetected
229+
<1>2. ~ Inv!P2 BY tcolor = "white" DEF Inv
230+
<1>3. ~ Inv!P1 BY <1>1 DEF Inv
231+
<1>. QED
232+
<2>1. Inv!P0 BY Inv, <1>2, <1>3 DEF Inv
233+
<2>. TAKE i \in Nodes
234+
<2>3. CASE i = 0 BY <2>1, <1>1, <2>3
235+
<2>4. CASE i \in 1 .. N-1
236+
<3>1. tpos < i BY tpos=0, <2>4, NAssumption
237+
<3>2. i < N BY NAssumption, <2>4
238+
<3>. QED BY <3>1, <3>2, <2>1
239+
<2>. QED BY <2>3, <2>4 DEF Nodes
240+
241+
=============================================================================
242+
\* Modification History
243+
\* Last modified Mon May 30 20:40:46 CEST 2016 by merz
244+
\* Created Mon Sep 09 11:33:10 CEST 2013 by merz

‎specifications/ewd840/README.md

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
# Termination detection in a ring
2+
A specification of Dijkstra's algorithm for termination detection
3+
in a ring. The algorithm was published as
4+
Edsger W. Dijkstra: Derivation of a termination detection algorithm for distributed computations. Inf. Proc. Letters 16:217-219 (1983).
5+
It appears as [EWD 840](https://www.cs.utexas.edu/users/EWD/ewd08xx/EWD840.PDF).
6+
7+
TLC can be used to verify safety and liveness properties. The TLA+ module also
8+
contains a hierarchical proof of the safety property that is checked by TLAPS.

‎specifications/sums_even/README.md

+2
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
# The double of any number is even
2+
Two proofs of the fact that x+x is even, for any natural number x.

‎specifications/sums_even.tla renamed to ‎specifications/sums_even/sums_even.tla

File renamed without changes.

0 commit comments

Comments
 (0)