Skip to content

Commit

Permalink
some comments
Browse files Browse the repository at this point in the history
  • Loading branch information
heidihoward committed Jan 8, 2024
1 parent effaa85 commit 2c21dd2
Showing 1 changed file with 4 additions and 0 deletions.
4 changes: 4 additions & 0 deletions tla/consensus/ccfraft.tla
Original file line number Diff line number Diff line change
Expand Up @@ -273,7 +273,10 @@ CandidateVarsTypeInv ==
/\ VotesGrantedTypeInv

\* The following variables are used only on leaders:

\* The next entry to send to each follower.
\* nextIndex is called send_idx in raft.h
\* In CCF, the leader updates nextIndex optimically when an AE message is dispatched
VARIABLE nextIndex

\* nextIndex cannot be zero as its the index of the first log
Expand Down Expand Up @@ -921,6 +924,7 @@ 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
\/ /\ \lnot m.success \* not successful
/\ LET tm == FindHighestPossibleMatch(log[i], m.lastLogIndex, m.term)
Expand Down

0 comments on commit 2c21dd2

Please sign in to comment.