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.

Sign up for GitHub

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

Swapping nextIndex for sentIndex #5897

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
76dfd44
nextIndex to sentIndex
heidihoward Jan 8, 2024
907888c
Merge branch 'main' into tla-off-by-one
heidihoward Jan 8, 2024
917f206
forgot to remove MatchIndexLowerBoundNextIndexInv
heidihoward Jan 8, 2024
114acae
messy merge
heidihoward Jan 8, 2024
1003ab4
Merge branch 'main' into tla-off-by-one
heidihoward Jan 8, 2024
feb9d68
Merge branch 'main' into tla-off-by-one
heidihoward Jan 9, 2024
ed6a9a2
missing increment in AppendEntriesBatchsize
heidihoward Jan 9, 2024
33f611d
bonus comment
heidihoward Jan 9, 2024
3b72e44
Merge branch 'main' into tla-off-by-one
heidihoward Jan 9, 2024
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
8 changes: 4 additions & 4 deletions tla/consensus/Traceccfraft.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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)

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -435,7 +435,7 @@ TraceDifferentialInv ==
\* /\ d.clientRequests = clientRequests
\* /\ d.votesGranted = votesGranted
\* /\ d.votesRequested = votesRequested
\* /\ d.nextIndex = nextIndex
\* /\ d.sentIndex = sentIndex
\* /\ d.matchIndex = matchIndex

-------------------------------------------------------------------------------------
Expand Down
49 changes: 25 additions & 24 deletions tla/consensus/ccfraft.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -274,16 +274,16 @@ 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.
\* sentIndex in CCF is similar in function to nextIndex in Raft
\* 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.
Expand All @@ -293,10 +293,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.
Expand Down Expand Up @@ -452,7 +452,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] + 1}


PlausibleSucessorNodes(i) ==
Expand Down Expand Up @@ -496,11 +496,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 ==
Expand Down Expand Up @@ -557,15 +557,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],
Expand All @@ -581,7 +581,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.
Expand All @@ -594,8 +594,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]))]
Expand Down Expand Up @@ -925,13 +925,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>>
Expand Down Expand Up @@ -1251,10 +1251,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 :
Expand Down Expand Up @@ -1399,7 +1400,7 @@ DebugAlias ==
commitIndex |-> commitIndex,
committableIndices |-> committableIndices,
votesGranted |-> votesGranted,
nextIndex |-> nextIndex,
sentIndex |-> sentIndex,
matchIndex |-> matchIndex,

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