Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Swapping nextIndex for sentIndex #5897

Merged
merged 9 commits into from
Jan 9, 2024
Merged
Changes from 6 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion tla/consensus/MCccfraftAtomicReconfig.cfg
Original file line number Diff line number Diff line change
@@ -77,6 +77,5 @@ INVARIANTS
MonoLogInv
LogConfigurationConsistentInv
NoLeaderBeforeInitialTerm
MatchIndexLowerBoundNextIndexInv
CommitCommittableIndices
CommittableIndicesAreKnownSignaturesInv
8 changes: 4 additions & 4 deletions tla/consensus/Traceccfraft.tla
Original file line number Diff line number Diff line change
@@ -80,7 +80,7 @@ ASSUME TraceServers \subseteq Servers

TraceAppendEntriesBatchsize(i, j) ==
\* -1) .. to explicitly model heartbeats, i.e. a message with zero entries.
(nextIndex[i][j] - 1) .. Len(log[i])
sentIndex[i][j] .. Len(log[i])

TraceInitReconfigurationVars ==
/\ reconfigurationCount = 0
@@ -176,7 +176,7 @@ IsSendAppendEntries ==
/\ IsAppendEntriesRequest(msg, j, i, logline)
\* There is now one more message of this type.
/\ Network!OneMoreMessage(msg)
/\ logline.msg.sent_idx + 1 = nextIndex[i][j]
/\ logline.msg.sent_idx = sentIndex[i][j]
/\ logline.msg.match_idx = matchIndex[i][j]
/\ committableIndices[logline.msg.state.node_id] = Range(logline.msg.state.committable_indices)

@@ -243,7 +243,7 @@ IsRcvAppendEntriesResponse ==
/\ IsEvent("recv_append_entries_response")
/\ LET i == logline.msg.state.node_id
j == logline.msg.from_node_id
IN /\ logline.msg.sent_idx + 1 = nextIndex[i][j]
IN /\ logline.msg.sent_idx = sentIndex[i][j]
/\ logline.msg.match_idx = matchIndex[i][j]
/\ \E m \in Network!MessagesTo(i, j):
/\ m.type = AppendEntriesResponse
@@ -435,7 +435,7 @@ TraceDifferentialInv ==
\* /\ d.clientRequests = clientRequests
\* /\ d.votesGranted = votesGranted
\* /\ d.votesRequested = votesRequested
\* /\ d.nextIndex = nextIndex
\* /\ d.sentIndex = sentIndex
\* /\ d.matchIndex = matchIndex

-------------------------------------------------------------------------------------
48 changes: 24 additions & 24 deletions tla/consensus/ccfraft.tla
Original file line number Diff line number Diff line change
@@ -274,16 +274,15 @@ CandidateVarsTypeInv ==

\* The following variables are used only on leaders:

\* The next entry to send to each follower, called sent_idx in raft.h
\* The last entry sent to each follower.
\* In CCF, the leader updates nextIndex optimically when an AE message is dispatched
\* In contrast, in Raft the leader only updates nextIndex when an AE response is received
VARIABLE nextIndex
VARIABLE sentIndex

\* nextIndex cannot be zero as its the index of the first log
\* entry in the AE message (recalling that TLA+ is 1-indexed).
NextIndexTypeInv ==

SentIndexTypeInv ==
\A i, j \in Servers : i /= j =>
/\ nextIndex[i][j] \in Nat \ {0}
/\ sentIndex[i][j] \in Nat

\* The latest entry that each follower has acknowledged is the same as the
\* leader's. This is used to calculate commitIndex on the leader.
@@ -293,10 +292,10 @@ MatchIndexTypeInv ==
\A i, j \in Servers : i /= j =>
matchIndex[i][j] \in Nat

leaderVars == <<nextIndex, matchIndex>>
leaderVars == <<sentIndex, matchIndex>>

LeaderVarsTypeInv ==
/\ NextIndexTypeInv
/\ SentIndexTypeInv
/\ MatchIndexTypeInv

\* End of per server variables.
@@ -452,7 +451,7 @@ CommittedTermPrefix(i, x) ==
AppendEntriesBatchsize(i, j) ==
\* The Leader is modeled to send zero to one entries per AppendEntriesRequest.
\* This can be redefined to send bigger batches of entries.
{nextIndex[i][j]}
{sentIndex[i][j]}


PlausibleSucessorNodes(i) ==
@@ -496,11 +495,11 @@ InitMessagesVars ==
InitCandidateVars ==
/\ votesGranted = [i \in Servers |-> {}]

\* The values nextIndex[i][i] and matchIndex[i][i] are never read, since the
\* The values sentIndex[i][i] and matchIndex[i][i] are never read, since the
\* leader does not send itself messages. It's still easier to include these
\* in the functions.
InitLeaderVars ==
/\ nextIndex = [i \in Servers |-> [j \in Servers |-> 1]]
/\ sentIndex = [i \in Servers |-> [j \in Servers |-> 0]]
/\ matchIndex = [i \in Servers |-> [j \in Servers |-> 0]]

Init ==
@@ -557,15 +556,15 @@ AppendEntries(i, j) ==
\* AppendEntries must be sent for historical entries, unless
\* snapshots are used. Whether the node is in configuration at
\* that index makes no difference.
\* /\ IsInServerSetForIndex(j, i, nextIndex[i][j])
/\ LET prevLogIndex == nextIndex[i][j] - 1
\* /\ IsInServerSetForIndex(j, i, sentIndex[i][j])
/\ LET prevLogIndex == sentIndex[i][j]
prevLogTerm == IF prevLogIndex \in DOMAIN log[i] THEN
log[i][prevLogIndex].term
ELSE
StartTerm
\* Send a number of entries (constrained by the end of the log).
lastEntry(idx) == min(Len(log[i]), idx)
index == nextIndex[i][j]
index == sentIndex[i][j] + 1
msg(idx) ==
[type |-> AppendEntriesRequest,
term |-> currentTerm[i],
@@ -581,7 +580,7 @@ AppendEntries(i, j) ==
/\ Send(m)
\* Record the most recent index we have sent to this node.
\* (see https://github.com/microsoft/CCF/blob/9fbde45bf5ab856ca7bcf655e8811dc7baf1e8a3/src/consensus/aft/raft.h#L935-L936)
/\ nextIndex' = [nextIndex EXCEPT ![i][j] = @ + Len(m.entries)]
/\ sentIndex' = [sentIndex EXCEPT ![i][j] = @ + Len(m.entries)]
/\ UNCHANGED <<reconfigurationVars, serverVars, candidateVars, matchIndex, logVars>>

\* Candidate i transitions to leader.
@@ -594,8 +593,8 @@ BecomeLeader(i) ==
\* all unsigned log entries of the previous leader.
\* See occurrence of last_committable_index() in raft.h::become_leader.
/\ log' = [log EXCEPT ![i] = SubSeq(log[i],1, MaxCommittableIndex(log[i]))]
\* Reset our nextIndex to the end of the *new* log.
/\ nextIndex' = [nextIndex EXCEPT ![i] = [j \in Servers |-> Len(log'[i]) + 1]]
\* Reset our sentIndex to the end of the *new* log.
/\ sentIndex' = [sentIndex EXCEPT ![i] = [j \in Servers |-> Len(log'[i])]]
/\ matchIndex' = [matchIndex EXCEPT ![i] = [j \in Servers |-> 0]]
\* Shorten the configurations if the removed txs contained reconfigurations
/\ configurations' = [configurations EXCEPT ![i] = ConfigurationsToIndex(i, Len(log'[i]))]
@@ -925,13 +924,13 @@ HandleAppendEntriesResponse(i, j, m) ==
/\ m.success \* successful
\* max(...) because why would we ever want to go backwards on a success response?!
/\ matchIndex' = [matchIndex EXCEPT ![i][j] = max(@, m.lastLogIndex)]
\* nextIndex is unchanged on successful AE response as it was already updated when the AE was dispatched
/\ UNCHANGED nextIndex
\* sentIndex is unchanged on successful AE response as it was already updated when the AE was dispatched
/\ UNCHANGED sentIndex
\/ /\ \lnot m.success \* not successful
/\ LET tm == FindHighestPossibleMatch(log[i], m.lastLogIndex, m.term)
IN nextIndex' = [nextIndex EXCEPT ![i][j] = max(min(tm, nextIndex[i][j]-1), matchIndex[i][j]) + 1 ]
IN sentIndex' = [sentIndex EXCEPT ![i][j] = max(min(tm, sentIndex[i][j]), matchIndex[i][j])]
\* UNCHANGED matchIndex is implied by the following statement in figure 2, page 4 in the raft paper:
\* "If AppendEntries fails because of log inconsistency: decrement nextIndex and retry"
\* "If AppendEntries fails because of log inconsistency: decrement nextIndex (aka sentIndex +1) and retry"
/\ UNCHANGED matchIndex
/\ Discard(m)
/\ UNCHANGED <<reconfigurationVars, serverVars, candidateVars, logVars>>
@@ -1251,10 +1250,11 @@ NoLeaderBeforeInitialTerm ==
\* MatchIndexLowerBoundNextIndexInv is not currently an invariant but
\* we might wish to add it in the future. This could be achieved by updating
\* nextIndex to max of current nextIndex and matchIndex when an AE ACK is received.
MatchIndexLowerBoundNextIndexInv ==
MatchIndexLowerBoundSentIndexInv ==

\A i,j \in Servers :
state[i] = Leader =>
nextIndex[i][j] > matchIndex[i][j]
sentIndex[i][j] >= matchIndex[i][j]

CommitCommittableIndices ==
\A i \in Servers :
@@ -1399,7 +1399,7 @@ DebugAlias ==
commitIndex |-> commitIndex,
committableIndices |-> committableIndices,
votesGranted |-> votesGranted,
nextIndex |-> nextIndex,
sentIndex |-> sentIndex,
matchIndex |-> matchIndex,

_MessagesTo |-> [ s, t \in Servers |-> Network!MessagesTo(s, t) ]