Skip to content

Commit bd65c02

Browse files
nolouchnolouch
committed
fix
1 parent d61bdaf commit bd65c02

File tree

2 files changed

+71
-64
lines changed

2 files changed

+71
-64
lines changed

‎JointConsensus/JointConsensus.tla

Lines changed: 70 additions & 62 deletions
Original file line numberDiff line numberDiff line change
@@ -45,9 +45,9 @@ VARIABLE elections
4545
VARIABLE allServers
4646

4747
\* The members of the server at that time.
48-
VARIABLE votersOfServer
49-
50-
nodeVars == <<allServers, votersOfServer>>
48+
VARIABLE voters
49+
VARIABLE nextVoters
50+
nodeVars == <<allServers, voters, nextVoters>>
5151
----
5252
\* The following variables are all per server (functions with domain Servers).
5353

@@ -58,7 +58,7 @@ VARIABLE state
5858
\* The candidate the server voted for in its current term, or
5959
\* Nil if it hasn't voted for any.
6060
VARIABLE votedFor
61-
serverVars == <<currentTerm, state, votedFor, allServers, votersOfServer>>
61+
serverVars == <<currentTerm, state, votedFor,allServers, voters,nextVoters>>
6262

6363
\* The set of requests that can go into the log
6464
VARIABLE clientRequests
@@ -95,6 +95,7 @@ VARIABLE nextIndex
9595
\* The latest entry that each follower has acknowledged is the same as the
9696
\* leader's. This is used to calculate commitIndex on the leader.
9797
VARIABLE matchIndex
98+
9899
leaderVars == <<nextIndex, matchIndex, elections>>
99100

100101
\* End of per server variables.
@@ -110,6 +111,13 @@ vars == <<messages, serverVars, candidateVars, leaderVars, logVars>>
110111
\* important property is that every quorum overlaps with every other.
111112
Quorum(Server) == {i \in SUBSET(Server) : Cardinality(i) * 2 > Cardinality(Server)}
112113

114+
BothQuorum(old, new) == IF old /= {} /\ new /= {} THEN
115+
{x[1] \cup x[2]: x \in (Quorum(old) \X Quorum(new))}
116+
ELSE IF new = {} THEN
117+
Quorum(old)
118+
ELSE IF old = {} THEN
119+
Quorum(new)
120+
ELSE {}
113121
\* The term of the last entry in a log, or 0 if the log is empty.
114122
LastTerm(xlog) == IF Len(xlog) = 0 THEN 0 ELSE xlog[Len(xlog)].term
115123

@@ -138,13 +146,13 @@ GetLatestConfig(i) ==
138146
LET length == Len(log[i])
139147
maxIndex == GetMaxConfigIndex(i, length)
140148
IN IF maxIndex = 0 THEN InitialServers
141-
ELSE log[i][maxIndex].value
149+
ELSE log[i][maxIndex]
142150
\* Get the latest commit config of server i.
143151
GetLatestCommitConfig(i) ==
144152
LET length == commitIndex[i]
145153
maxIndex == GetMaxConfigIndex(i, length)
146154
IN IF maxIndex = 0 THEN InitialServers
147-
ELSE log[i][maxIndex].value
155+
ELSE log[i][maxIndex]
148156

149157
----
150158
\* Define initial values for all variables
@@ -155,10 +163,11 @@ InitServerVars == /\ allServers = InitialServers \cup NewServers
155163
/\ currentTerm = [i \in allServers |-> 1]
156164
/\ state = [i \in allServers |-> Follower]
157165
/\ votedFor = [i \in allServers |-> Nil]
158-
/\ votersOfServer =
166+
/\ voters =
159167
LET initalVoters == InitialServers
160168
newVoters == (InitialServers \cup NewServers) \ InitialServers
161169
IN [i \in initalVoters |-> initalVoters] @@ [i \in newVoters |-> {}]
170+
/\ nextVoters = [i \in allServers |-> {}]
162171

163172
InitCandidateVars == /\ votesResponded = [i \in allServers |-> {}]
164173
/\ votesGranted = [i \in allServers |-> {}]
@@ -195,7 +204,7 @@ Timeout(i) == /\ state[i] \in {Follower, Candidate}
195204

196205
\* Candidate i sends j a RequestVote request.
197206
RequestVote(i, j) ==
198-
/\ j \in votersOfServer[i]
207+
/\ j \in (voters[i] \cup nextVoters[i])
199208
/\ state[i] = Candidate
200209
/\ j \notin votesResponded[i]
201210
/\ Send([mtype |-> RequestVoteRequest,
@@ -212,7 +221,7 @@ RequestVote(i, j) ==
212221
AppendEntries(i, j) ==
213222
/\ i /= j
214223
/\ state[i] = Leader
215-
/\ j \in votersOfServer[i]
224+
/\ j \in (voters[i] \cup nextVoters[i])
216225
/\ LET prevLogIndex == nextIndex[i][j] - 1
217226
prevLogTerm == IF prevLogIndex > 0 THEN
218227
log[i][prevLogIndex].term
@@ -221,7 +230,7 @@ AppendEntries(i, j) ==
221230
\* Send up to 1 entry, constrained by the end of the log.
222231
lastEntry == Min({Len(log[i]), nextIndex[i][j]})
223232
entries == SubSeq(log[i], nextIndex[i][j], lastEntry)
224-
IN /\ Len(entries) > 0 /\ matchIndex[i][j] < Len(log[i])
233+
IN /\ Len(entries) > 0 /\ matchIndex[i][j] < lastEntry
225234
/\ Send([mtype |-> AppendEntriesRequest,
226235
mterm |-> currentTerm[i],
227236
mprevLogIndex |-> prevLogIndex,
@@ -235,8 +244,9 @@ AppendEntries(i, j) ==
235244
\* Candidate i transitions to leader.
236245
BecomeLeader(i) ==
237246
/\ state[i] = Candidate
238-
/\ votesGranted[i] \in Quorum(votersOfServer[i])
247+
/\ votesGranted[i] \in BothQuorum(voters[i], nextVoters[i])
239248
/\ state' = [state EXCEPT ![i] = Leader]
249+
\*/\ PrintT(i \cup "became leader")
240250
/\ nextIndex' = [nextIndex EXCEPT ![i] =
241251
[j \in allServers |-> Len(log[i]) + 1]]
242252
/\ matchIndex' = [matchIndex EXCEPT ![i] =
@@ -249,31 +259,18 @@ BecomeLeader(i) ==
249259
evoterLog |-> voterLog[i]]}
250260
/\ UNCHANGED <<messages, currentTerm, votedFor, candidateVars, logVars, nodeVars>>
251261

252-
\* Leader i receives a client request to add v to the log.
253-
ClientRequest(i) ==
254-
/\ state[i] = Leader
255-
/\ clientRequests < MaxClientRequests
256-
/\ LET entry == [term |-> currentTerm[i],
257-
type |-> ValueEntry,
258-
value |-> clientRequests]
259-
newLog == Append(log[i], entry)
260-
IN /\ log' = [log EXCEPT ![i] = newLog]
261-
/\ clientRequests' = clientRequests + 1
262-
/\ UNCHANGED <<messages, serverVars, candidateVars,
263-
leaderVars, commitIndex, committedLog, committedLogDecrease, nodeVars>>
264-
265262
\* Leader i advances its commitIndex.
266263
\* This is done as a separate step from handling AppendEntries responses,
267264
\* in part to minimize atomic regions, and in part so that leaders of
268265
\* single-server clusters are able to mark entries committed.
269266
AdvanceCommitIndex(i) ==
270267
/\ state[i] = Leader
271268
/\ LET \* The set of servers that agree up through index.
272-
Agree(index) == {i} \cup {k \in allServers :
269+
Agree(index) == {i} \cup {k \in (voters[i] \cup nextVoters[i]) :
273270
matchIndex[i][k] >= index}
274271
\* The maximum indexes for which a quorum agrees
275272
agreeIndexes == {index \in 1..Len(log[i]) :
276-
Agree(index) \in Quorum(votersOfServer[i])}
273+
Agree(index) \in BothQuorum(voters[i] ,nextVoters[i])}
277274
\* New value for commitIndex'[i]
278275
newCommitIndex ==
279276
IF /\ agreeIndexes /= {}
@@ -283,49 +280,64 @@ AdvanceCommitIndex(i) ==
283280
ELSE
284281
commitIndex[i]
285282
newCommittedLog ==
286-
IF newCommitIndex > 1
283+
IF newCommitIndex >= 1
287284
THEN
288285
[j \in 1..newCommitIndex |-> log[i][j]]
289286
ELSE
290287
<<>>
291-
IN /\ commitIndex' = [commitIndex EXCEPT ![i] = newCommitIndex]
288+
IN /\ commitIndex[i] /= newCommitIndex
289+
/\ commitIndex' = [commitIndex EXCEPT ![i] = newCommitIndex]
292290
/\ committedLogDecrease' = \/ ( newCommitIndex < Len(committedLog))
293291
\/ \E j \in 1..Len(committedLog) : committedLog[j] /= newCommittedLog[j]
294292
/\ committedLog' = newCommittedLog
295-
/\ UNCHANGED <<messages, serverVars, candidateVars, leaderVars, log, clientRequests>>
293+
\*/\ PrintT(Len(log[i])\cup newCommitIndex)
294+
/\ UNCHANGED <<messages, serverVars, candidateVars, leaderVars, log, clientRequests, nodeVars>>
296295

297296
AdvanceCommitConfig(i) ==
298297
/\ GetMaxConfigIndex(i,commitIndex[i]) > 0
299298
/\ LET config == GetLatestCommitConfig(i)
300-
IN IF votersOfServer[i] /= config.newConf
299+
IN IF voters[i] /= config.newConf
301300
THEN /\ \/ \* leader not in the new configuration.
302301
\* switch to Follwer.
303302
/\ i \notin config.newConf
304303
/\ state[i] = Leader
305304
/\ state' = [state EXCEPT ![i] = Follower]
306305
\/ /\ i \in config.newConf
307306
/\ UNCHANGED <<state>>
308-
/\ votersOfServer' = [ votersOfServer EXCEPT ![i] = config.newConf]
309-
ELSE UNCHANGED <<votersOfServer>>
310-
/\ UNCHANGED <<currentTerm, votedFor, candidateVars, leaderVars, logVars, nodeVars>>
307+
/\ voters' = [ voters EXCEPT ![i] = config.newConf]
308+
/\ nextVoters' = [nextVoters EXCEPT ![i] = {}]
309+
ELSE UNCHANGED <<voters, state, nextVoters>>
310+
/\ UNCHANGED <<messages, currentTerm, votedFor, candidateVars, leaderVars, logVars, allServers>>
311311

312312

313313
\* Leader i add a group servers to cluster.
314314
SetNodes(i, newNodes) ==
315315
/\ state[i] = Leader
316316
/\ \* for reducing the state space, just verify once.
317317
Len(SelectSeq(log[i], LAMBDA logEntry : logEntry.type = ConfigEntry)) = 0
318-
/\ LET oldConfig == votersOfServer[i]
318+
/\ LET oldConfig == voters[i]
319319
entry == [term |-> currentTerm[i],
320320
type |-> ConfigEntry,
321321
newConf |-> newNodes,
322322
oldConf |-> oldConfig]
323-
transitionConfig == oldConfig \cup newNodes
324323
newLog == Append(log[i], entry)
325-
IN /\ log' = [log EXCEPT ![i] = newLog]
326-
/\ votersOfServer = [votersOfServer EXCEPT ![i] = transitionConfig]
327-
/\ UNCHANGED <<state, leaderVars, logVars, candidateVars, allServers>>
324+
IN /\ log' = [log EXCEPT ![i] = Append(@,entry)]
325+
/\ nextVoters' = [nextVoters EXCEPT ![i] = newNodes]
326+
/\ UNCHANGED <<messages, state, votedFor, currentTerm, candidateVars,
327+
leaderVars, commitIndex, committedLog, committedLogDecrease, allServers, voters, clientRequests>>
328328

329+
\* Leader i receives a client request to add v to the log.
330+
ClientRequest(i) ==
331+
/\ state[i] = Leader
332+
/\ clientRequests < MaxClientRequests
333+
/\ LET entry == [term |-> currentTerm[i],
334+
type |-> ValueEntry,
335+
value |-> clientRequests]
336+
newLog == Append(log[i], entry)
337+
IN /\ log' = [log EXCEPT ![i] = newLog]
338+
/\ clientRequests' = clientRequests + 1
339+
/\ UNCHANGED <<messages, serverVars, candidateVars,
340+
leaderVars, commitIndex, committedLog, committedLogDecrease, nodeVars>>
329341
----
330342
\* Message handlers
331343
\* i = recipient, j = sender, m = message
@@ -393,12 +405,12 @@ HandleAppendEntriesRequest(i, j, m) ==
393405
msource |-> i,
394406
mdest |-> j],
395407
m)
396-
/\ UNCHANGED <<serverVars, logVars>>
408+
/\ UNCHANGED <<serverVars, logVars, nodeVars>>
397409
\/ \* return to follower state
398410
/\ m.mterm = currentTerm[i]
399411
/\ state[i] = Candidate
400412
/\ state' = [state EXCEPT ![i] = Follower]
401-
/\ UNCHANGED <<currentTerm, votedFor, logVars, messages>>
413+
/\ UNCHANGED <<currentTerm, votedFor, logVars, messages, nodeVars>>
402414
\/ \* accept request
403415
/\ m.mterm = currentTerm[i]
404416
/\ state[i] = Follower
@@ -422,22 +434,22 @@ HandleAppendEntriesRequest(i, j, m) ==
422434
msource |-> i,
423435
mdest |-> j],
424436
m)
425-
/\ UNCHANGED <<serverVars, log, clientRequests, committedLog, committedLogDecrease>>
437+
/\ UNCHANGED <<serverVars, log, clientRequests, committedLog, committedLogDecrease, nodeVars>>
426438
\/ \* conflict: remove 1 entry
427439
/\ m.mentries /= << >>
428440
/\ Len(log[i]) >= index
429441
/\ log[i][index].term /= m.mentries[1].term
430442
/\ LET new == [index2 \in 1..(Len(log[i]) - 1) |->
431443
log[i][index2]]
432444
IN log' = [log EXCEPT ![i] = new]
433-
/\ UNCHANGED <<serverVars, commitIndex, messages,clientRequests, committedLog, committedLogDecrease>>
445+
/\ UNCHANGED <<serverVars, commitIndex, messages,clientRequests, committedLog, committedLogDecrease, nodeVars>>
434446
\/ \* no conflict: append entry
435447
/\ m.mentries /= << >>
436448
/\ Len(log[i]) = m.mprevLogIndex
437449
/\ log' = [log EXCEPT ![i] =
438450
Append(log[i], m.mentries[1])]
439-
/\ UNCHANGED <<serverVars, commitIndex, messages, clientRequests, committedLog, committedLogDecrease>>
440-
/\ UNCHANGED <<candidateVars, leaderVars, nodeVars>>
451+
/\ UNCHANGED <<serverVars, commitIndex, messages, clientRequests, committedLog, committedLogDecrease, nodeVars>>
452+
/\ UNCHANGED <<candidateVars, leaderVars>>
441453

442454
\* Servers i receives an AppendEntries response from server j with
443455
\* m.mterm = currentTerm[i].
@@ -493,20 +505,21 @@ Next ==
493505
\* Leader election
494506
\/ \E i,j \in allServers : RequestVote(i, j)
495507
\/ \E i \in allServers : BecomeLeader(i)
508+
\* Network
509+
\/ \E m \in messages : Receive(m)
510+
\/ \/ /\ \A i \in allServers : state[i] = Follower
511+
/\ \E i \in allServers : Timeout(i)
512+
\/ /\ \E i \in allServers : state[i] /= Follower
513+
/\ UNCHANGED <<serverVars, candidateVars, messages, logVars, leaderVars, nodeVars>>
496514
\* Client request
497515
\/ \E i \in allServers : ClientRequest(i)
498516
\* Config changed with joint consensus
499-
\/ \E i \in InitialServers: SetNodes(i, NewServers)
517+
\/ \E i \in allServers: SetNodes(i, NewServers)
500518
\* Log replica
501519
\/ \E i \in allServers : AdvanceCommitIndex(i)
502520
\/ \E i \in allServers : AdvanceCommitConfig(i)
503521
\/ \E i,j \in allServers : AppendEntries(i, j)
504-
\* Network
505-
\/ \E m \in messages : Receive(m)
506-
\/ \/ /\ \A i \in allServers : state[i] = Follower
507-
/\ \E i \in allServers : Timeout(i)
508-
\/ /\ \E i \in allServers : state[i] /= Follower
509-
/\ UNCHANGED <<serverVars, candidateVars, messages, leaderVars, logVars, nodeVars>>
522+
510523

511524

512525
\* The specification must start with the initial state and transition according
@@ -518,23 +531,18 @@ Spec == Init /\ [][Next]_vars
518531

519532
MoreThanOneLeader ==
520533
Cardinality({i \in allServers: state[i]=Leader}) > 1
534+
521535

522536
TransitionPhaseChecker ==
523-
\A i \in allServers: LET inTransition == /\ commitIndex[i] < GetMaxConfigIndex(i,Len(log[i]))
537+
\A i \in allServers: LET inTransition == /\ commitIndex[i] > 1
538+
/\ commitIndex[i] < GetMaxConfigIndex(i,Len(log[i]))
524539
/\ GetMaxConfigIndex(i,Len(log[i])) > 0
525540
configEntry == GetLatestConfig(i)
526541
IN IF inTransition THEN
527542
IF state[i] = Leader THEN
528-
votersOfServer[i] = configEntry.oldConf \cup configEntry.newConf
529-
ELSE votersOfServer[i] = configEntry.oldConf
530-
ELSE TRUE
531-
CommittedPhaseChecker ==
532-
\A i \in allServers: LET committed == /\ commitIndex[i] > 0
533-
/\ GetMaxConfigIndex(i,commitIndex[i]) > 0
534-
/\ commitIndex[i] > GetMaxConfigIndex(i,commitIndex[i])
535-
configEntry == GetLatestCommitConfig(i)
536-
IN IF committed THEN
537-
votersOfServer[i] = configEntry.newConf
543+
/\ voters[i] = configEntry.oldConf
544+
/\ nextVoters[i] = configEntry.newConf
545+
ELSE /\ voters[i] = configEntry.oldConf
538546
ELSE TRUE
539547

540548
===============================================================================

‎JointConsensus/JointConsensus.toolbox/JointConsensus___ConfigCheck.launch

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,13 +19,12 @@
1919
<stringAttribute key="modelBehaviorNext" value=""/>
2020
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
2121
<intAttribute key="modelBehaviorSpecType" value="1"/>
22-
<stringAttribute key="modelBehaviorVars" value="elections, committedLogDecrease, allServers, messages, clientRequests, matchIndex, log, votersOfServer, state, commitIndex, currentTerm, votesResponded, committedLog, nextIndex, votesGranted, voterLog, votedFor"/>
22+
<stringAttribute key="modelBehaviorVars" value="elections, committedLogDecrease, allServers, messages, clientRequests, matchIndex, log, state, commitIndex, nextVoters, currentTerm, votesResponded, voters, committedLog, nextIndex, votesGranted, voterLog, votedFor"/>
2323
<stringAttribute key="modelComments" value=""/>
2424
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
2525
<listAttribute key="modelCorrectnessInvariants">
2626
<listEntry value="1\lnot MoreThanOneLeader"/>
2727
<listEntry value="1TransitionPhaseChecker"/>
28-
<listEntry value="1CommittedPhaseChecker"/>
2928
</listAttribute>
3029
<listAttribute key="modelCorrectnessProperties"/>
3130
<stringAttribute key="modelExpressionEval" value=""/>

0 commit comments

Comments
 (0)