Skip to content

Commit 6004e82

Browse files
ywelschywelsch
authored
Zen with terms (#30)
This is an alternative specification to https://github.com/elastic/elasticsearch-formal-models/blob/master/cluster/tla/consensus.tla that resembles existing Zen more closely in that it does not require force-publishing the last accepted value upon election, but limits this only to the configuration.
1 parent 4e12262 commit 6004e82

File tree

5 files changed

+397
-0
lines changed

5 files changed

+397
-0
lines changed

‎.gitignore

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,11 @@
44
**/tla/*.toolbox/*.log
55
**/tla/*.toolbox/*.pdf
66
**/tla/*.toolbox/*.tex
7+
**/tla/*.toolbox/*___model_SnapShot*.launch
8+
**/tla/*.toolbox/**/*.tla
9+
**/tla/*.toolbox/**/*.out
10+
**/tla/*.toolbox/**/MC.cfg
711
**/tla/*.pdf
12+
**/tla/*.old
813
**/*~
914
cluster/isabelle/output

‎ZenWithTerms/tla/ZenWithTerms.tla

Lines changed: 301 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,301 @@
1+
-------------------------------------------------------------------------------------
2+
3+
-------------------------------- MODULE ZenWithTerms --------------------------------
4+
\* Imported modules used in this specification
5+
EXTENDS Naturals, FiniteSets, Sequences, TLC
6+
7+
----
8+
9+
CONSTANTS Values
10+
11+
\* Set of node ids (all master-eligible nodes)
12+
CONSTANTS Nodes
13+
14+
\* RPC message types
15+
CONSTANTS
16+
Join,
17+
PublishRequest,
18+
PublishResponse,
19+
Commit
20+
21+
----
22+
23+
\* Set of requests and responses sent between nodes.
24+
VARIABLE messages
25+
\* Transitive closure of value updates as done by leaders
26+
VARIABLE descendant
27+
28+
\* node state (map from node id to state)
29+
VARIABLE currentTerm
30+
VARIABLE lastCommittedConfiguration
31+
VARIABLE lastAcceptedTerm
32+
VARIABLE lastAcceptedVersion
33+
VARIABLE lastAcceptedValue
34+
VARIABLE lastAcceptedConfiguration
35+
VARIABLE joinVotes
36+
VARIABLE startedJoinSinceLastReboot
37+
VARIABLE electionWon
38+
VARIABLE lastPublishedVersion
39+
VARIABLE lastPublishedConfiguration
40+
VARIABLE publishVotes
41+
42+
----
43+
44+
Terms == Nat
45+
46+
\* set of valid configurations (i.e. the set of all non-empty subsets of Nodes)
47+
ValidConfigs == SUBSET(Nodes) \ {{}}
48+
49+
\* quorums correspond to majority of votes in a config
50+
IsQuorum(votes, config) == Cardinality(votes \cap config) * 2 > Cardinality(config)
51+
52+
ElectionWon(n, votes) ==
53+
/\ IsQuorum(votes, lastCommittedConfiguration[n])
54+
/\ IsQuorum(votes, lastAcceptedConfiguration[n])
55+
56+
\* initial model state
57+
Init == /\ messages = {}
58+
/\ descendant = {}
59+
/\ currentTerm = [n \in Nodes |-> 0]
60+
/\ lastCommittedConfiguration \in {[n \in Nodes |-> vc] : vc \in ValidConfigs} \* all agree on initial config
61+
/\ lastAcceptedTerm = [n \in Nodes |-> 0]
62+
/\ lastAcceptedVersion = [n \in Nodes |-> 0]
63+
/\ lastAcceptedValue \in {[n \in Nodes |-> v] : v \in Values} \* all agree on initial value
64+
/\ lastAcceptedConfiguration = [n \in Nodes |-> lastCommittedConfiguration[n]]
65+
/\ joinVotes = [n \in Nodes |-> {}]
66+
/\ startedJoinSinceLastReboot = [n \in Nodes |-> FALSE]
67+
/\ electionWon = [n \in Nodes |-> FALSE]
68+
/\ lastPublishedVersion = [n \in Nodes |-> 0]
69+
/\ lastPublishedConfiguration = [n \in Nodes |-> lastCommittedConfiguration[n]]
70+
/\ publishVotes = [n \in Nodes |-> {}]
71+
72+
\* Send join request from node n to node nm for term t
73+
HandleStartJoin(n, nm, t) ==
74+
/\ t > currentTerm[n]
75+
/\ LET
76+
joinRequest == [method |-> Join,
77+
source |-> n,
78+
dest |-> nm,
79+
term |-> t,
80+
laTerm |-> lastAcceptedTerm[n],
81+
laVersion |-> lastAcceptedVersion[n]]
82+
IN
83+
/\ currentTerm' = [currentTerm EXCEPT ![n] = t]
84+
/\ lastPublishedVersion' = [lastPublishedVersion EXCEPT ![n] = 0]
85+
/\ lastPublishedConfiguration' = [lastPublishedConfiguration EXCEPT ![n] = lastAcceptedConfiguration[n]]
86+
/\ startedJoinSinceLastReboot' = [startedJoinSinceLastReboot EXCEPT ![n] = TRUE]
87+
/\ electionWon' = [electionWon EXCEPT ![n] = FALSE]
88+
/\ joinVotes' = [joinVotes EXCEPT ![n] = {}]
89+
/\ publishVotes' = [publishVotes EXCEPT ![n] = {}]
90+
/\ messages' = messages \cup { joinRequest }
91+
/\ UNCHANGED <<lastCommittedConfiguration, lastAcceptedConfiguration, lastAcceptedVersion,
92+
lastAcceptedValue, lastAcceptedTerm, descendant>>
93+
94+
\* node n handles a join request and checks if it has received enough joins (= votes)
95+
\* for its term to be elected as master
96+
HandleJoinRequest(n, m) ==
97+
/\ m.method = Join
98+
/\ m.term = currentTerm[n]
99+
/\ startedJoinSinceLastReboot[n]
100+
/\ \/ m.laTerm < lastAcceptedTerm[n]
101+
\/ /\ m.laTerm = lastAcceptedTerm[n]
102+
/\ m.laVersion <= lastAcceptedVersion[n]
103+
/\ joinVotes' = [joinVotes EXCEPT ![n] = @ \cup { m.source }]
104+
/\ electionWon' = [electionWon EXCEPT ![n] = ElectionWon(n, joinVotes'[n])]
105+
/\ IF electionWon[n] = FALSE /\ electionWon'[n]
106+
THEN
107+
\* initiating publish version with last accepted version to enable client requests
108+
/\ lastPublishedVersion' = [lastPublishedVersion EXCEPT ![n] = lastAcceptedVersion[n]]
109+
ELSE
110+
UNCHANGED <<lastPublishedVersion>>
111+
/\ UNCHANGED <<lastCommittedConfiguration, currentTerm, publishVotes, messages, descendant,
112+
lastAcceptedVersion, lastAcceptedValue, lastAcceptedConfiguration,
113+
lastAcceptedTerm, startedJoinSinceLastReboot, lastPublishedConfiguration>>
114+
115+
\* client causes a cluster state change v with configuration vs
116+
ClientRequest(n, v, vs) ==
117+
/\ electionWon[n]
118+
/\ lastPublishedVersion[n] = lastAcceptedVersion[n] \* means we have the last published value / config (useful for CAS operations, where we need to read the previous value first)
119+
/\ vs /= lastAcceptedConfiguration[n] => lastCommittedConfiguration[n] = lastAcceptedConfiguration[n] \* only allow reconfiguration if there is not already a reconfiguration in progress
120+
/\ IsQuorum(joinVotes[n], vs) \* only allow reconfiguration if we have a quorum of (join) votes for the new config
121+
/\ LET
122+
newPublishVersion == lastPublishedVersion[n] + 1
123+
publishRequests == { [method |-> PublishRequest,
124+
source |-> n,
125+
dest |-> ns,
126+
term |-> currentTerm[n],
127+
version |-> newPublishVersion,
128+
value |-> v,
129+
config |-> vs,
130+
commConf |-> lastCommittedConfiguration[n]] : ns \in Nodes }
131+
newEntry == [prevT |-> lastAcceptedTerm[n],
132+
prevV |-> lastAcceptedVersion[n],
133+
nextT |-> currentTerm[n],
134+
nextV |-> newPublishVersion]
135+
matchingElems == { e \in descendant :
136+
/\ e.nextT = newEntry.prevT
137+
/\ e.nextV = newEntry.prevV }
138+
newTransitiveElems == { [prevT |-> e.prevT,
139+
prevV |-> e.prevV,
140+
nextT |-> newEntry.nextT,
141+
nextV |-> newEntry.nextV] : e \in matchingElems }
142+
IN
143+
/\ descendant' = descendant \cup {newEntry} \cup newTransitiveElems
144+
/\ lastPublishedVersion' = [lastPublishedVersion EXCEPT ![n] = newPublishVersion]
145+
/\ lastPublishedConfiguration' = [lastPublishedConfiguration EXCEPT ![n] = vs]
146+
/\ publishVotes' = [publishVotes EXCEPT ![n] = {}] \* publishVotes are only counted per publish version
147+
/\ messages' = messages \cup publishRequests
148+
/\ UNCHANGED <<startedJoinSinceLastReboot, lastCommittedConfiguration, currentTerm, electionWon,
149+
lastAcceptedVersion, lastAcceptedValue, lastAcceptedTerm, lastAcceptedConfiguration, joinVotes>>
150+
151+
\* handle publish request m on node n
152+
HandlePublishRequest(n, m) ==
153+
/\ m.method = PublishRequest
154+
/\ m.term = currentTerm[n]
155+
/\ (m.term = lastAcceptedTerm[n]) => (m.version > lastAcceptedVersion[n])
156+
/\ lastAcceptedTerm' = [lastAcceptedTerm EXCEPT ![n] = m.term]
157+
/\ lastAcceptedVersion' = [lastAcceptedVersion EXCEPT ![n] = m.version]
158+
/\ lastAcceptedValue' = [lastAcceptedValue EXCEPT ![n] = m.value]
159+
/\ lastAcceptedConfiguration' = [lastAcceptedConfiguration EXCEPT ![n] = m.config]
160+
/\ lastCommittedConfiguration' = [lastCommittedConfiguration EXCEPT ![n] = m.commConf]
161+
/\ LET
162+
response == [method |-> PublishResponse,
163+
source |-> n,
164+
dest |-> m.source,
165+
term |-> m.term,
166+
version |-> m.version]
167+
IN
168+
/\ messages' = messages \cup {response}
169+
/\ UNCHANGED <<startedJoinSinceLastReboot, currentTerm, descendant, lastPublishedConfiguration,
170+
electionWon, lastPublishedVersion, joinVotes, publishVotes>>
171+
172+
\* node n commits a change
173+
HandlePublishResponse(n, m) ==
174+
/\ m.method = PublishResponse
175+
/\ m.term = currentTerm[n]
176+
/\ m.version = lastPublishedVersion[n]
177+
/\ publishVotes' = [publishVotes EXCEPT ![n] = @ \cup {m.source}]
178+
/\ IF
179+
/\ IsQuorum(publishVotes'[n], lastCommittedConfiguration[n])
180+
/\ IsQuorum(publishVotes'[n], lastPublishedConfiguration[n])
181+
THEN
182+
LET
183+
commitRequests == { [method |-> Commit,
184+
source |-> n,
185+
dest |-> ns,
186+
term |-> currentTerm[n],
187+
version |-> lastPublishedVersion[n]] : ns \in Nodes }
188+
IN
189+
/\ messages' = messages \cup commitRequests
190+
ELSE
191+
UNCHANGED <<messages>>
192+
/\ UNCHANGED <<startedJoinSinceLastReboot, lastCommittedConfiguration, currentTerm, electionWon, descendant,
193+
lastAcceptedVersion, lastAcceptedValue, lastAcceptedTerm, lastAcceptedConfiguration,
194+
lastPublishedVersion, lastPublishedConfiguration, joinVotes>>
195+
196+
\* apply committed configuration to node n
197+
HandleCommitRequest(n, m) ==
198+
/\ m.method = Commit
199+
/\ m.term = currentTerm[n]
200+
/\ m.term = lastAcceptedTerm[n]
201+
/\ m.version = lastAcceptedVersion[n]
202+
/\ lastCommittedConfiguration' = [lastCommittedConfiguration EXCEPT ![n] = lastAcceptedConfiguration[n]]
203+
/\ UNCHANGED <<currentTerm, joinVotes, messages, lastAcceptedTerm, lastAcceptedValue, startedJoinSinceLastReboot, descendant,
204+
electionWon, lastAcceptedConfiguration, lastAcceptedVersion, lastPublishedVersion, publishVotes,
205+
lastPublishedConfiguration>>
206+
207+
\* crash/restart node n (loses ephemeral state)
208+
RestartNode(n) ==
209+
/\ electionWon' = [electionWon EXCEPT ![n] = FALSE]
210+
/\ startedJoinSinceLastReboot' = [startedJoinSinceLastReboot EXCEPT ![n] = FALSE]
211+
/\ joinVotes' = [joinVotes EXCEPT ![n] = {}]
212+
/\ lastPublishedVersion' = [lastPublishedVersion EXCEPT ![n] = 0]
213+
/\ lastPublishedConfiguration' = [lastPublishedConfiguration EXCEPT ![n] = lastAcceptedConfiguration[n]]
214+
/\ publishVotes' = [publishVotes EXCEPT ![n] = {}]
215+
/\ UNCHANGED <<messages, lastAcceptedVersion, currentTerm, lastCommittedConfiguration, descendant,
216+
lastAcceptedTerm, lastAcceptedValue, lastAcceptedConfiguration>>
217+
218+
\* next-step relation
219+
Next ==
220+
\/ \E n, nm \in Nodes : \E t \in Terms : HandleStartJoin(n, nm, t)
221+
\/ \E m \in messages : HandleJoinRequest(m.dest, m)
222+
\/ \E n \in Nodes : \E v \in Values : \E vs \in ValidConfigs : ClientRequest(n, v, vs)
223+
\/ \E m \in messages : HandlePublishRequest(m.dest, m)
224+
\/ \E m \in messages : HandlePublishResponse(m.dest, m)
225+
\/ \E m \in messages : HandleCommitRequest(m.dest, m)
226+
\/ \E n \in Nodes : RestartNode(n)
227+
228+
----
229+
230+
\* Invariants
231+
232+
SingleNodeInvariant ==
233+
\A n \in Nodes :
234+
/\ lastAcceptedTerm[n] <= currentTerm[n]
235+
/\ electionWon[n] = ElectionWon(n, joinVotes[n]) \* cached value is consistent
236+
/\ IF electionWon[n] THEN lastPublishedVersion[n] >= lastAcceptedVersion[n] ELSE lastPublishedVersion[n] = 0
237+
/\ electionWon[n] => startedJoinSinceLastReboot[n]
238+
/\ publishVotes[n] /= {} => electionWon[n]
239+
240+
OneMasterPerTerm ==
241+
\A m1, m2 \in messages:
242+
/\ m1.method = PublishRequest
243+
/\ m2.method = PublishRequest
244+
/\ m1.term = m2.term
245+
=> m1.source = m2.source
246+
247+
LogMatching ==
248+
\A m1, m2 \in messages:
249+
/\ m1.method = PublishRequest
250+
/\ m2.method = PublishRequest
251+
/\ m1.term = m2.term
252+
/\ m1.version = m2.version
253+
=> m1.value = m2.value
254+
255+
CommittedPublishRequest(mp) ==
256+
/\ mp.method = PublishRequest
257+
/\ \E mc \in messages:
258+
/\ mc.method = Commit
259+
/\ mp.term = mc.term
260+
/\ mp.version = mc.version
261+
262+
DescendantRelationIsStrictlyOrdered ==
263+
/\ \A d \in descendant:
264+
/\ d.prevT <= d.nextT
265+
/\ d.prevV < d.nextV
266+
\* relation is transitive
267+
/\ \A d1, d2 \in descendant:
268+
d1.nextT = d2.prevT /\ d1.nextV = d2.prevV
269+
=> [prevT |-> d1.prevT, prevV |-> d1.prevV, nextT |-> d2.nextT, nextV |-> d2.nextV] \in descendant
270+
271+
NewerOpsBasedOnOlderCommittedOps ==
272+
\A m1, m2 \in messages :
273+
/\ CommittedPublishRequest(m1)
274+
/\ m2.method = PublishRequest
275+
/\ m2.term >= m1.term
276+
/\ m2.version > m1.version
277+
=> [prevT |-> m1.term, prevV |-> m1.version, nextT |-> m2.term, nextV |-> m2.version] \in descendant
278+
279+
\* main invariant (follows from NewerOpsBasedOnOlderCommittedOps):
280+
CommittedValuesDescendantsFromCommittedValues ==
281+
\A m1, m2 \in messages :
282+
/\ CommittedPublishRequest(m1)
283+
/\ CommittedPublishRequest(m2)
284+
/\ \/ m1.term /= m2.term
285+
\/ m1.version /= m2.version
286+
=>
287+
\/ [prevT |-> m1.term, prevV |-> m1.version, nextT |-> m2.term, nextV |-> m2.version] \in descendant
288+
\/ [prevT |-> m2.term, prevV |-> m2.version, nextT |-> m1.term, nextV |-> m1.version] \in descendant
289+
290+
CommittedValuesDescendantsFromInitialValue ==
291+
\A m \in messages :
292+
CommittedPublishRequest(m)
293+
=>
294+
[prevT |-> 0, prevV |-> 0, nextT |-> m.term, nextV |-> m.version] \in descendant
295+
296+
\* State-exploration limits
297+
StateConstraint ==
298+
/\ \A n \in Nodes: IF currentTerm[n] <= 1 THEN lastPublishedVersion[n] <= 2 ELSE lastPublishedVersion[n] <= 3
299+
/\ Cardinality(messages) <= 15
300+
301+
====================================================================================================

‎ZenWithTerms/tla/ZenWithTerms.toolbox/.project

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<projectDescription>
3+
<name>ZenWithTerms</name>
4+
<comment></comment>
5+
<projects>
6+
</projects>
7+
<buildSpec>
8+
<buildCommand>
9+
<name>toolbox.builder.TLAParserBuilder</name>
10+
<arguments>
11+
</arguments>
12+
</buildCommand>
13+
<buildCommand>
14+
<name>toolbox.builder.PCalAlgorithmSearchingBuilder</name>
15+
<arguments>
16+
</arguments>
17+
</buildCommand>
18+
</buildSpec>
19+
<natures>
20+
<nature>toolbox.natures.TLANature</nature>
21+
</natures>
22+
<linkedResources>
23+
<link>
24+
<name>ZenWithTerms.tla</name>
25+
<type>1</type>
26+
<locationURI>PARENT-1-PROJECT_LOC/ZenWithTerms.tla</locationURI>
27+
</link>
28+
</linkedResources>
29+
</projectDescription>

‎ZenWithTerms/tla/ZenWithTerms.toolbox/.settings/org.lamport.tla.toolbox.prefs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
ProjectRootFile=PARENT-1-PROJECT_LOC/ZenWithTerms.tla
2+
eclipse.preferences.version=1

0 commit comments

Comments
 (0)