Raft Paper section 5.4.2: "[A leader] never commits log entries from …

…previous terms...".
microsoft · Oct 19, 2023 · 7593bea · 7593bea
1 parent bcb0613
commit 7593bea
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 0 deletions.
diff --git a/tla/MCccfraft.cfg b/tla/MCccfraft.cfg
@@ -57,6 +57,7 @@ PROPERTIES
     PermittedLogChangesProp
     StateTransitionsProp
     PendingBecomesFollowerProp
+    NeverCommitEntryPrevTermsProp
 
 INVARIANTS
     LogInv

diff --git a/tla/MCccfraftWithReconfig.cfg b/tla/MCccfraftWithReconfig.cfg
@@ -57,6 +57,7 @@ PROPERTIES
     PermittedLogChangesProp
     StateTransitionsProp
     PendingBecomesFollowerProp
+    NeverCommitEntryPrevTermsProp
 
 INVARIANTS
     LogInv

diff --git a/tla/SIMccfraft.cfg b/tla/SIMccfraft.cfg
@@ -47,6 +47,7 @@ PROPERTIES
     PermittedLogChangesProp
     StateTransitionsProp
     PendingBecomesFollowerProp
+    NeverCommitEntryPrevTermsProp
 
 INVARIANTS
     LogInv

diff --git a/tla/ccfraft.tla b/tla/ccfraft.tla
@@ -1364,6 +1364,13 @@ PendingBecomesFollowerProp ==
             s \in GetServerSet(s)' => 
                 state[s]' = Follower]_vars
 
+\* Raft Paper section 5.4.2: "[A leader] never commits log entries from previous terms...".
+NeverCommitEntryPrevTermsProp ==
+    [][\A i \in { s \in Servers : state[s] = Leader }:
+        \* If the commitIndex of a leader changes, the log entry's term that the new commitIndex
+        \* points to equals the leader's term.
+        commitIndex'[i] > commitIndex[i] => log[i][commitIndex'[i]].term = currentTerm'[i] ]_vars
+
 LogMatchingProp ==
     \A i, j \in Servers : []<>(log[i] = log[j])