add apply index

JointConsensus/JointConsensus.tla

@@ -2,6 +2,7 @@
 \* This is the formal specification for the Raft consensus algorithm.
 \*
 \* Copyright 2014 Diego Ongaro.
+\* 
 \* This work is licensed under the Creative Commons Attribution-4.0
 \* International License https://creativecommons.org/licenses/by/4.0/
 
@@ -10,7 +11,7 @@ EXTENDS Naturals, FiniteSets, Sequences, TLC
 \* The set of server IDs
 CONSTANTS InitialServers, NewServers
 
-CONSTANTS ValueEntry,ConfigEntry
+CONSTANTS NormalEntry, BeginConfChange, FinalizeConfChange
 
 \* Servers states.
 CONSTANTS Follower, Candidate, Leader
@@ -67,9 +68,11 @@ VARIABLE clientRequests
 \* log entry. Unfortunately, the Sequence module defines Head(s) as the entry
 \* with index 1, so be careful not to use that!
 VARIABLE log
-\* The index of the latest entry in the log the state machine may apply.
+\* The index of the latest entry in the log the state machine has commited.
 VARIABLE commitIndex
-logVars == <<log, commitIndex, clientRequests>>
+\* The index of the latest entry in the log the state machine has apply.
+VARIABLE applyIndex
+logVars == <<log, commitIndex, applyIndex, clientRequests>>
 
 \* The following variables are used only on candidates:
 \* The set of servers from which the candidate has received a RequestVote
@@ -134,7 +137,7 @@ Max(s) == CHOOSE x \in s : \A y \in s : x >= y
 
 \* Get the maximum config from log[1..l].
 GetMaxConfigIndex(i, l) ==
-    LET chonfigIndexes == {index \in 1..l: log[i][index].type = ConfigEntry}
+    LET chonfigIndexes == {index \in 1..l: log[i][index].type = BeginConfChange \/ log[i][index].type = FinalizeConfChange}
     IN IF chonfigIndexes = {} THEN 0
        ELSE Max(chonfigIndexes)
 \* Get the latest config in all log of server i.
@@ -280,46 +283,56 @@ AdvanceCommitIndex(i) ==
                   commitIndex[i]
        IN /\ commitIndex' = [commitIndex EXCEPT ![i] = newCommitIndex]
     /\ UNCHANGED <<messages, serverVars, candidateVars, leaderVars, log, clientRequests, nodeVars>>
-
-\* Leader i apply its committed confiuration.
-ApplyConfig(i) ==
-    /\ GetMaxConfigIndex(i, commitIndex[i]) > 0
-    /\ LET config == GetLatestCommitConfig(i)
-       IN IF voters[i] /= config.newConf
-          THEN /\ \/ \* leader not in the new configuration.
-                     \* switch to Follwer.
-                     /\ i \notin config.newConf
-                     /\ state[i] = Leader
-                     /\ state' = [state EXCEPT ![i] = Follower]
-                  \/ /\ i \in config.newConf
-                     /\ UNCHANGED <<state>>
-               /\ voters' = [ voters EXCEPT ![i] = config.newConf]
-               /\ nextVoters' = [nextVoters EXCEPT ![i] = {}]
-          ELSE UNCHANGED <<voters, state, nextVoters>>
-    /\ UNCHANGED <<messages, currentTerm, votedFor, candidateVars, leaderVars, logVars, allServers>>
+
+\* ApplyLog apply the commit entrys of server i.
+ApplyLog(i) ==
+    LET 
+        next == applyIndex[i] + 1
+        entry == log[i][next]
+    IN 
+       /\ applyIndex[i] < commitIndex[i]
+       /\ \/ \* apply normal entry
+             /\ entry.type = NormalEntry
+             /\ applyIndex' = [ applyIndex EXCEPT ![i] = next ]
+          \/ \* begin the membership change
+             /\ entry.type = BeginConfChange
+             /\ nextVoters' = [nextVoters EXCEPT ![i] = entry.newConf]
+             /\ applyIndex' = [ applyIndex EXCEPT ![i] = next ]
+          \/ \* finalize the membership change    
+             /\ entry.type = FinalizeConfChange
+             /\ /\ \/ \* leader not in the new configuration.
+                      \* step to Follwer.
+                      /\ i \notin entry.newConf
+                      /\ state[i] = Leader
+                      /\ state' = [state EXCEPT ![i] = Follower]
+                   \/ /\ i \in entry.newConf
+                      /\ UNCHANGED <<state>>
+             /\ voters' = [ voters EXCEPT ![i] = entry.newConf]
+             /\ nextVoters' = [nextVoters EXCEPT ![i] = {}]
+             /\ applyIndex' = [ applyIndex EXCEPT ![i] = next ]
+       /\ UNCHANGED <<messages, currentTerm, votedFor, candidateVars, leaderVars, logVars, allServers>>
 
 \* Leader i add a group servers to cluster.
-SetNodes(i, newNodes) ==
+ProposeMembership(i, newNodes) ==
     /\ state[i] = Leader
     /\ \* for reducing the state space, just verify once.
-       Len(SelectSeq(log[i], LAMBDA logEntry : logEntry.type = ConfigEntry)) = 0
+       Len(SelectSeq(log[i], LAMBDA logEntry : logEntry.type = BeginConfChange)) = 0
     /\ LET oldConfig == voters[i]
            entry == [term    |-> currentTerm[i],
-                     type    |-> ConfigEntry,
+                     type    |-> BeginConfChange,
                      newConf |-> newNodes,
                      oldConf |-> oldConfig]
            newLog == Append(log[i], entry)
-       IN /\ log' = [log EXCEPT ![i] = Append(@,entry)]
-          /\ nextVoters' = [nextVoters EXCEPT ![i] = newNodes]
+       IN log' = [log EXCEPT ![i] = Append(@,entry)]
     /\ UNCHANGED <<messages, state, votedFor, currentTerm, candidateVars,
-                leaderVars, commitIndex, allServers, voters, clientRequests>>
+                leaderVars, commitIndex, applyIndex, allServers, voters, nextVoters, clientRequests>>
 
 \* Leader i receives a client request to add v to the log.
 ClientRequest(i) ==
     /\ state[i] = Leader
     /\ clientRequests < MaxClientRequests
     /\ LET entry == [term  |-> currentTerm[i],
-                     type  |-> ValueEntry,
+                     type  |-> NormalEntry,
                      value |-> clientRequests]
            newLog == Append(log[i], entry)
        IN /\ log' = [log EXCEPT ![i] = newLog]
@@ -503,11 +516,11 @@ Next ==
     \* Client request
     \/ \E i \in allServers : ClientRequest(i)
     \* Config changed with joint consensus
-    \/ \E i \in allServers: SetNodes(i, NewServers)
+    \/ \E i \in allServers: ProposeMembership(i, NewServers)
     \* Log replica
     \/ \E i,j \in allServers : AppendEntries(i, j)
     \/ \E i \in allServers : AdvanceCommitIndex(i)
-    \/ \E i \in allServers : ApplyConfig(i)
+    \/ \E i \in allServers : ApplyLog(i)
 
 \* The specification must start with the initial state and transition according
 \* to Next.