Refactor JoinedState and StartState into one.

microsoft · Nov 20, 2023 · 7404e3d · 7404e3d
1 parent 0f59a5d
commit 7404e3d
Show file tree

Hide file tree

Showing 3 changed files with 33 additions and 42 deletions.
diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla
@@ -94,16 +94,20 @@ MCSend(msg) ==
 MCInMaxSimultaneousCandidates(i) ==
     Cardinality({ s \in GetServerSetForIndex(i, commitIndex[i]) : state[s] = Candidate}) < 1
 
-\* Alternative to CCF!Init that uses the above MCInitReconfigurationVars
+JoinedLog(startNode, nextNodes) ==
+    StartLog(startNode, nextNodes) \o
+        << [term |-> StartTerm, contentType |-> TypeReconfiguration, configuration |-> nextNodes],
+           [term |-> StartTerm, contentType |-> TypeSignature] >>
+
 MCInit ==
-    /\ CCF!InitMessagesVars
-    /\ CCF!InitCandidateVars
-    /\ CCF!InitLeaderVars
+    /\ InitMessagesVars
+    /\ InitCandidateVars
+    /\ InitLeaderVars
     /\ IF Cardinality(Configurations[1]) = 1
-       \* If the first config is just one node, we can start with a two-tx log and a single config
-       THEN CCF!StartState(CHOOSE s \in Configurations[1]: TRUE, ToServers)
-       \* If we want to start with multiple nodes, a four-tx log with a reconfiguration already appended
-       ELSE CCF!JoinedState(Configurations[1], ToServers)
+       \* If the first config is just one node, we can start with a two-tx log and a single config.
+       THEN InitLogConfigServerVars(Configurations[1], StartLog)
+       \* If we want to start with multiple nodes, we can start with a four-tx log with a reconfiguration already appended.
+       ELSE InitLogConfigServerVars(Configurations[1], JoinedLog)
 
 \* Alternative to CCF!Spec that uses the above MCInit
 mc_spec ==   

diff --git a/tla/consensus/Traceccfraft.tla b/tla/consensus/Traceccfraft.tla
@@ -85,8 +85,7 @@ TraceAppendEntriesBatchsize(i, j) ==
 TraceInitReconfigurationVars ==
     /\ reconfigurationCount = 0
     /\ removedFromConfiguration = {}
-    /\ LET startNode == TraceLog[1].msg.state.node_id
-       IN StartState(startNode, TraceServers)
+    /\ InitLogConfigServerVars({TraceLog[1].msg.state.node_id}, StartLog)
 
 -------------------------------------------------------------------------------------
 

diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla
@@ -459,45 +459,33 @@ PlausibleSucessorNodes(i) ==
         highestMatchServers == {n \in activeServers : \A m \in activeServers : matchIndex[i][n] >= matchIndex[i][m]}
     IN {n \in highestMatchServers : \A m \in highestMatchServers: HighestConfigurationWithNode(i, n) >= HighestConfigurationWithNode(i, m)}
 
-\* Generate initial state for a given startNode
-StartState(startNode, servers) ==
-    /\ reconfigurationCount = 0
-    /\ removedFromConfiguration = {}
-    /\ configurations = [ i \in servers |-> IF i = startNode THEN (1 :> {startNode}) ELSE << >>]
-    /\ currentTerm = [i \in servers |-> IF i = startNode THEN StartTerm ELSE 0]
-    /\ state       = [i \in servers |-> IF i = startNode THEN Leader ELSE None]
-    /\ votedFor    = [i \in servers |-> Nil]
-    /\ log         = [i \in servers |-> IF i = startNode
-                                        THEN << [term |-> StartTerm, contentType |-> TypeReconfiguration, configuration |-> {startNode}],
-                                                [term |-> StartTerm, contentType |-> TypeSignature] >>
-                                        ELSE << >>]
-    /\ commitIndex  = [i \in servers |-> IF i = startNode THEN Len(log[i]) ELSE 0]
-    /\ committableIndices  = [i \in servers |-> {}]
-
-\* Generate initial state for a startNodes configuration
-JoinedState(startNodes, servers) ==
+StartLog(startNode, _ignored) ==
+    << [term |-> StartTerm, contentType |-> TypeReconfiguration, configuration |-> startNode],
+       [term |-> StartTerm, contentType |-> TypeSignature] >>
+
+InitLogConfigServerVars(startNodes, logPrefix(_,_)) ==
     /\ reconfigurationCount = 0
     /\ removedFromConfiguration = {}
-    /\ \E startNode \in startNodes:
-        /\ configurations = [ i \in servers |-> IF i \in startNodes  THEN (3 :> startNodes) ELSE << >>]
-        /\ currentTerm = [i \in servers |-> IF i \in startNodes THEN StartTerm ELSE 0]
-        /\ state       = [i \in servers |-> IF i = startNode THEN Leader ELSE IF i \in startNodes THEN Follower ELSE None]
-        /\ votedFor    = [i \in servers |-> Nil]
-        /\ log         = [i \in servers |-> IF i \in startNodes
-                                            THEN << [term |-> StartTerm, contentType |-> TypeReconfiguration, configuration |-> {startNode}],
-                                                    [term |-> StartTerm, contentType |-> TypeSignature],
-                                                    [term |-> StartTerm, contentType |-> TypeReconfiguration, configuration |-> startNodes],
-                                                    [term |-> StartTerm, contentType |-> TypeSignature] >>
-                                            ELSE << >>]
-        /\ commitIndex  = [i \in servers |-> IF i \in startNodes THEN Len(log[i]) ELSE 0]
-        /\ committableIndices  = [i \in servers |-> {}]
-
+    /\ committableIndices  = [i \in Servers |-> {}]
+    /\ votedFor    = [i \in Servers |-> Nil]
+    /\ currentTerm = [i \in Servers |-> IF i \in startNodes THEN StartTerm ELSE 0]
+    /\ \E sn \in startNodes:
+        \* We make the following assumption about logPrefix, whose violation would violate SignatureInv and LogConfigurationConsistentInv.
+        \* Alternative, we could have conjoined this formula to Init, but this would have caused TLC to generate no initial states on a
+        \* bogus logPrefix.
+        \* <<[term |-> StartTerm, contentType |-> TypeReconfiguration, configuration |-> startNodes], 
+        \*   [term |-> StartTerm, contentType |-> TypeSignature]>> \in Suffixes(logPrefix({sn}, startNodes))
+        /\ log         = [i \in Servers |-> IF i \in startNodes THEN logPrefix({sn}, startNodes) ELSE << >>]
+        /\ state       = [i \in Servers |-> IF i = sn THEN Leader ELSE IF i \in startNodes THEN Follower ELSE None]
+        /\ commitIndex = [i \in Servers |-> IF i \in startNodes THEN Len(logPrefix({sn}, startNodes)) ELSE 0]
+    /\ configurations = [i \in Servers |-> IF i \in startNodes  THEN (Len(log[i])-1 :> startNodes) ELSE << >>]
+    
 ------------------------------------------------------------------------------
 \* Define initial values for all variables
 
 InitReconfigurationVars ==
     \E startNode \in Servers:
-        StartState(startNode, Servers)
+        InitLogConfigServerVars({startNode}, StartLog)
 
 InitMessagesVars ==
     /\ Network!InitMessageVar