Limiting the terms reached by ProposeVote (#6535)

microsoft · Oct 7, 2024 · 9e7fb2d · 9e7fb2d
1 parent 261602d
commit 9e7fb2d
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 0 deletions.
diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg
@@ -4,6 +4,7 @@ CONSTANTS
     Servers <- ToServers
 
     Timeout <- MCTimeout
+    RcvProposeVoteRequest <- MCRcvProposeVoteRequest
     Send <- MCSend
     ClientRequest <- MCClientRequest
     SignCommittableMessages <- MCSignCommittableMessages

diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla
@@ -68,6 +68,11 @@ MCTimeout(i) ==
     /\ Cardinality({ s \in GetServerSetForIndex(i, commitIndex[i]) : leadershipState[s] = Candidate}) < 1
     /\ CCF!Timeout(i)
 
+\* Limit the number of terms that can be reached
+MCRcvProposeVoteRequest(i, j) ==
+    /\ currentTerm[i] < StartTerm + TermCount
+    /\ CCF!RcvProposeVoteRequest(i, j)
+
 \* Limit number of requests (new entries) that can be made
 MCClientRequest(i) ==
     \* Allocation-free variant of Len(SelectSeq(log[i], LAMBDA e: e.contentType = TypeEntry)) <= RequestCount