Merge branch 'main' into spec_only_send_ae_to_known_servers

microsoft · Jan 8, 2024 · 017f404 · 017f404
2 parents 3c27ad5 + 7cb07bb
commit 017f404
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 6 deletions.
diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg
@@ -77,6 +77,5 @@ INVARIANTS
     MonoLogInv
     NoLeaderBeforeInitialTerm
     LogConfigurationConsistentInv
-    MatchIndexLowerBoundNextIndexInv
     CommitCommittableIndices
     CommittableIndicesAreKnownSignaturesInv
diff --git a/tla/consensus/MCccfraftWithReconfig.cfg b/tla/consensus/MCccfraftWithReconfig.cfg
@@ -77,6 +77,5 @@ INVARIANTS
     MonoLogInv
     NoLeaderBeforeInitialTerm
     LogConfigurationConsistentInv
-    MatchIndexLowerBoundNextIndexInv
     CommitCommittableIndices
     CommittableIndicesAreKnownSignaturesInv
diff --git a/tla/consensus/SIMccfraft.cfg b/tla/consensus/SIMccfraft.cfg
@@ -77,8 +77,6 @@ INVARIANTS
     NoLeaderBeforeInitialTerm
     LogConfigurationConsistentInv
 
-    MatchIndexLowerBoundNextIndexInv
-
     CommitCommittableIndices
 
     CommittableIndicesAreKnownSignaturesInv

diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla
@@ -273,7 +273,10 @@ CandidateVarsTypeInv ==
     /\ VotesGrantedTypeInv
 
 \* The following variables are used only on leaders:
-\* The next entry to send to each follower.
+
+\* The next entry to send to each follower, called sent_idx in raft.h
+\* 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
 
 \* nextIndex cannot be zero as its the index of the first log
@@ -922,7 +925,8 @@ 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'  = [nextIndex  EXCEPT ![i][j] = max(@, m.lastLogIndex + 1)]
+          \* 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)
              IN nextIndex' = [nextIndex EXCEPT ![i][j] = max(min(tm, nextIndex[i][j]-1), matchIndex[i][j]) + 1 ]
@@ -1244,6 +1248,9 @@ NoLeaderBeforeInitialTerm ==
     \A i \in Servers :
         currentTerm[i] < StartTerm => state[i] # Leader
 
+\* 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 ==
     \A i,j \in Servers :
         state[i] = Leader =>