Remove unused variable committedLog.

The variable committedLog is not part of the original Raft specification but was introduced later in the still open pull request ongardie/raft.tla#4.
lemmy · Nov 3, 2022 · 9ab520f · 9ab520f
1 parent e1b4e08
commit 9ab520f
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 26 deletions.
diff --git a/tla/MCccfraft.cfg b/tla/MCccfraft.cfg
@@ -40,7 +40,6 @@ CHECK_DEADLOCK
     FALSE
 
 INVARIANTS
-    LogInv
     MoreThanOneLeaderInv
     CandidateTermNotInLogInv
     ElectionSafetyInv

diff --git a/tla/ccfraft.tla b/tla/ccfraft.tla
@@ -133,11 +133,7 @@ VARIABLE log
 \* The index of the latest entry in the log the state machine may apply.
 VARIABLE commitIndex
 
-\* The index that gets committed.  This is a history variable (in TLA+ jargon) that 
-\* does not exist in an implementation.
-VARIABLE committedLog
-
-logVars == <<log, commitIndex, clientRequests, committedLog>>
+logVars == <<log, commitIndex, clientRequests>>
 
 \* The set of servers from which the candidate has received a vote in its
 \* currentTerm.
@@ -340,7 +336,6 @@ InitLogVars ==
     /\ log          = [i \in Servers |-> << >>]
     /\ commitIndex  = [i \in Servers |-> 0]
     /\ clientRequests = 1
-    /\ committedLog = << >>
 
 Init ==
     /\ InitReconfigurationVars
@@ -459,7 +454,7 @@ BecomeLeader(i) ==
         \* Potentially also shorten the currentConfiguration if the removed index contained a configuration
         /\ configurations' = [configurations EXCEPT ![i] = RestrictPred(@, LAMBDA c : c <= new_conf_index)]
     /\ UNCHANGED <<reconfigurationCount, messageVars, currentTerm, votedFor, votesRequested, candidateVars,
-        commitIndex, clientRequests, committedLog>>
+        commitIndex, clientRequests>>
 
 \* Leader i receives a client request to add v to the log.
 ClientRequest(i) ==
@@ -475,7 +470,7 @@ ClientRequest(i) ==
            \* Make sure that each request is unique, reduce state space to be explored
            /\ clientRequests' = clientRequests + 1
     /\ UNCHANGED <<reconfigurationVars, messageVars, serverVars, candidateVars,
-                   leaderVars, commitIndex, committedLog>>
+                   leaderVars, commitIndex>>
 
 \*  SNIPPET_START: signing
 \* CCF extension: Signed commits
@@ -499,7 +494,7 @@ SignCommittableMessages(i) ==
             newLog == Append(log[i], entry)
             IN log' = [log EXCEPT ![i] = newLog]
         /\ UNCHANGED <<reconfigurationVars, messageVars, serverVars, candidateVars, clientRequests,
-                    leaderVars, commitIndex, committedLog>>
+                    leaderVars, commitIndex>>
 \* SNIPPET_END: signing
 
 \*  SNIPPET_START: reconfig
@@ -530,7 +525,7 @@ ChangeConfiguration(i, newConfiguration) ==
            /\ log' = [log EXCEPT ![i] = newLog]
            /\ configurations' = [configurations EXCEPT ![i] = @ @@ Len(log[i]) + 1 :> newConfiguration]
     /\ UNCHANGED <<messageVars, serverVars, candidateVars, clientRequests,
-                    leaderVars, commitIndex, committedLog>>
+                    leaderVars, commitIndex>>
 \* SNIPPET_END: reconfig
 
 
@@ -565,12 +560,6 @@ AdvanceCommitIndex(i) ==
          \* only advance if necessary (this is basically a sanity check after the Min above)
         /\ commitIndex[i] < new_index
         /\ commitIndex' = [commitIndex EXCEPT ![i] = new_index]
-        /\ IF new_index <= Len(committedLog) THEN
-            /\ Assert(\A j \in 1..new_index : committedLog[j] = new_log[j], "committedLogConflict")
-            /\ UNCHANGED committedLog
-           ELSE
-            /\ Assert(\A j \in 1..Len(committedLog) : committedLog[j] = new_log[j], "committedLogConflict")
-            /\ committedLog' = new_log
         \* If commit index surpasses the next configuration, pop the first config, and eventually retire as leader
         /\ \/ /\ Cardinality(DOMAIN configurations[i]) > 1
               /\ new_index >= NextConfigurationIndex(i)
@@ -696,7 +685,7 @@ AppendEntriesAlreadyDone(i, j, index, m) ==
               msource         |-> i,
               mdest           |-> j],
               m)
-    /\ UNCHANGED <<reconfigurationVars, messagesSent, commitsNotified, serverVars, log, clientRequests, committedLog>>
+    /\ UNCHANGED <<reconfigurationVars, messagesSent, commitsNotified, serverVars, log, clientRequests>>
 
 ConflictAppendEntriesRequest(i, index, m) ==
     /\ m.mentries /= << >>
@@ -713,7 +702,7 @@ ConflictAppendEntriesRequest(i, index, m) ==
                 |-> [n \in 1..min(Len(messagesSent[i][j]) - 1, index - 1)
                 |-> messagesSent[i][j][n]]]
        IN messagesSent' = [messagesSent EXCEPT ![i] = newCounts ]
-    /\ UNCHANGED <<reconfigurationCount, serverVars, commitIndex, messages, commitsNotified, clientRequests, committedLog>>
+    /\ UNCHANGED <<reconfigurationCount, serverVars, commitIndex, messages, commitsNotified, clientRequests>>
 
 NoConflictAppendEntriesRequest(i, j, m) ==
     /\ m.mentries /= << >>
@@ -759,7 +748,7 @@ NoConflictAppendEntriesRequest(i, j, m) ==
               msource         |-> i,
               mdest           |-> j],
               m)
-    /\ UNCHANGED <<reconfigurationCount, messagesSent, commitsNotified, currentTerm, votedFor, clientRequests, committedLog>>
+    /\ UNCHANGED <<reconfigurationCount, messagesSent, commitsNotified, currentTerm, votedFor, clientRequests>>
 
 AcceptAppendEntriesRequest(i, j, logOk, m) ==
     \* accept request
@@ -850,7 +839,7 @@ UpdateCommitIndex(i,j,m) ==
         /\ commitIndex' = [commitIndex EXCEPT ![i] = new_commit_index]
         /\ configurations' = [configurations EXCEPT ![i] = new_config]
     /\ UNCHANGED <<reconfigurationCount, messages, messagesSent, commitsNotified, currentTerm,
-                   votedFor, candidateVars, leaderVars, log, clientRequests, committedLog>>
+                   votedFor, candidateVars, leaderVars, log, clientRequests>>
 
 \* Receive a message.
 Receive ==
@@ -904,10 +893,6 @@ Spec == Init /\ [][Next]_vars
 \* Correctness invariants
 \* These invariants should be true for all possible states
 
-\* Committed log entries should not conflict
-LogInv ==
-    /\ \A i \in Servers : IsPrefix(Committed(i),committedLog)
-
 \* There should not be more than one leader per term at the same time
 \* Note that this does not rule out multiple leaders in the same term at different times
 MoreThanOneLeaderInv ==
@@ -1063,7 +1048,6 @@ LogVarsTypeInv ==
         /\ LogTypeOK(log[i])
         /\ commitIndex[i] \in Nat
     /\ clientRequests \in Nat \ {0}
-    /\ LogTypeOK(committedLog)
 
 \* Invariant to check the type safety of all variables
 TypeInv ==