Validate the successor state *after* defining it (#5797)

Co-authored-by: Amaury Chamayou <[email protected]>
microsoft · Oct 31, 2023 · 6e0ba3a · 6e0ba3a
1 parent 40a3783
commit 6e0ba3a
Showing 1 changed file with 36 additions and 31 deletions.
diff --git a/tla/consensus/Traceccfraft.tla b/tla/consensus/Traceccfraft.tla
@@ -166,8 +166,8 @@ IsBecomeLeader ==
 
 IsClientRequest ==
     /\ IsEvent("replicate")
-    /\ ~logline.msg.globally_committable
     /\ ClientRequest(logline.msg.state.node_id)
+    /\ ~logline.msg.globally_committable
     \* TODO Consider creating a mapping from clientRequests to actual values in the system trace.
     \* TODO Alternatively, extract the written values from the system trace and redefine clientRequests at startup.
     /\ committableIndices[logline.msg.state.node_id] = Range(logline.msg.state.committable_indices)
@@ -194,19 +194,20 @@ IsRcvAppendEntriesRequest ==
     /\ LET i == logline.msg.state.node_id
            j == logline.msg.from_node_id
        IN /\ \E m \in Network!MessagesTo(i, j):
-              /\ IsAppendEntriesRequest(m, i, j, logline)
+              /\ m.type = AppendEntriesRequest
               /\ \/ HandleAppendEntriesRequest(i, j, m)
                  \/ UpdateTerm(i, j, m) \cdot HandleAppendEntriesRequest(i, j, m)
                  \* ConflictAppendEntriesRequest truncates the log but does *not* consume the AE request. In other words, there is a
                   \* HandleAppendEntriesRequest step that leaves messages unchanged.
                  \/ RAERRAER(m):: (UNCHANGED messages /\ HandleAppendEntriesRequest(i, j, m)) \cdot HandleAppendEntriesRequest(i, j, m)
+              /\ IsAppendEntriesRequest(m, i, j, logline)
 
 IsSendAppendEntriesResponse ==
     \* Skip saer because ccfraft!HandleAppendEntriesRequest atomcially handles the request and sends the response.
        \* Find a similar pattern in Traceccfraft!IsRcvRequestVoteRequest below.
     /\ IsEvent("send_append_entries_response")
-    /\ committableIndices[logline.msg.state.node_id] = Range(logline.msg.state.committable_indices)
     /\ UNCHANGED vars
+    /\ committableIndices[logline.msg.state.node_id] = Range(logline.msg.state.committable_indices)
 
 IsAddConfiguration ==
     /\ IsEvent("add_configuration")
@@ -216,8 +217,8 @@ IsAddConfiguration ==
 
 IsSignCommittableMessages ==
     /\ IsEvent("replicate")
-    /\ logline.msg.globally_committable
     /\ SignCommittableMessages(logline.msg.state.node_id)
+    /\ logline.msg.globally_committable
     \* It is tempting to assert the effect of SignCommittableMessages(...node_id) here, i.e., 
      \* committableIndices'[logline.msg.state.node_id] = Range(logline'.msg.committable_indices).
      \* However, this assumes logline', i.e., TraceLog[l'], is less than or equal Len(TraceLog),
@@ -236,8 +237,8 @@ IsAdvanceCommitIndex ==
              /\ commitIndex'[i] = logline.msg.state.commit_idx
              /\ committableIndices'[i] = Range(logline.msg.state.committable_indices)
     \/ /\ IsEvent("commit")
-       /\ logline.msg.state.leadership_state = "Follower"
        /\ UNCHANGED vars
+       /\ logline.msg.state.leadership_state = "Follower"
 
 IsChangeConfiguration ==
     /\ IsEvent("add_configuration")
@@ -254,11 +255,12 @@ IsRcvAppendEntriesResponse ==
        IN /\ logline.msg.sent_idx + 1 = nextIndex[i][j]
           /\ logline.msg.match_idx = matchIndex[i][j]
           /\ \E m \in Network!MessagesTo(i, j):
-               /\ IsAppendEntriesResponse(m, i, j, logline)
+               /\ m.type = AppendEntriesResponse
                /\ \/ HandleAppendEntriesResponse(i, j, m)
                   \/ UpdateTerm(i, j, m) \cdot HandleAppendEntriesResponse(i, j, m)
                   \/ UpdateTerm(i, j, m) \cdot DropResponseWhenNotInState(i, j, m)
                   \/ DropResponseWhenNotInState(i, j, m)
+               /\ IsAppendEntriesResponse(m, i, j, logline)
     /\ committableIndices[logline.msg.state.node_id] = Range(logline.msg.state.committable_indices)
 
 IsSendRequestVote ==
@@ -298,11 +300,11 @@ IsExecuteAppendEntries ==
     \* Skip append because ccfraft!HandleRequestVoteRequest atomcially handles the request, sends the response,
        \* and appends the entry to the ledger.
        /\ IsEvent("execute_append_entries_sync")
-       /\ state[logline.msg.state.node_id] = Follower
-       /\ currentTerm[logline.msg.state.node_id] = logline.msg.state.current_view
        \* Not asserting committableIndices here because the impl and spec will only be in sync upon the subsequent send_append_entries.
        \* Also see IsSignCommittableMessages above.
        /\ UNCHANGED vars
+       /\ state[logline.msg.state.node_id] = Follower
+       /\ currentTerm[logline.msg.state.node_id] = logline.msg.state.current_view
 
 IsRcvRequestVoteResponse ==
     /\ IsEvent("recv_request_vote_response")
@@ -322,15 +324,15 @@ IsRcvRequestVoteResponse ==
 
 IsBecomeFollower ==
     /\ IsEvent("become_follower")
-    /\ state[logline.msg.state.node_id] \in {Follower}
-    /\ configurations[logline.msg.state.node_id] = ToConfigurations(logline.msg.configurations)
     /\ UNCHANGED vars \* UNCHANGED implies that it doesn't matter if we prime the previous variables.
+    /\ state[logline.msg.state.node_id] = Follower
+    /\ configurations[logline.msg.state.node_id] = ToConfigurations(logline.msg.configurations)
     /\ committableIndices[logline.msg.state.node_id] = Range(logline.msg.state.committable_indices)
 
 IsCheckQuorum ==
     /\ IsEvent("become_follower")
-    /\ state[logline.msg.state.node_id] = Leader
     /\ CheckQuorum(logline.msg.state.node_id)
+    /\ state[logline.msg.state.node_id] = Leader
     /\ committableIndices[logline.msg.state.node_id] = Range(logline.msg.state.committable_indices)
 
 IsRcvProposeVoteRequest ==
@@ -470,26 +472,29 @@ TraceAlias ==
     [
         lvl |-> l,
         ts |-> ts,
-        logline |-> logline.msg,
-        _ENABLED |-> 
-            [
-                Timeout                    |-> [ i \in Servers   |-> ENABLED Timeout(i) ],
-                RequestVote                |-> [ i,j \in Servers |-> ENABLED RequestVote(i, j) ],
-                BecomeLeader               |-> [ i \in Servers   |-> ENABLED BecomeLeader(i) ],
-                ClientRequest              |-> [ i \in Servers   |-> ENABLED ClientRequest(i) ],
-                SignCommittableMessages    |-> [ i \in Servers   |-> ENABLED SignCommittableMessages(i) ],
-                ChangeConfiguration        |-> [ i \in Servers   |-> ENABLED ChangeConfiguration(i) ],
-                NotifyCommit               |-> [ i,j \in Servers |-> ENABLED NotifyCommit(i,j) ],
-                AdvanceCommitIndex         |-> [ i \in Servers   |-> ENABLED AdvanceCommitIndex(i) ],
-                AppendEntries              |-> [ i,j \in Servers |-> ENABLED AppendEntries(i, j) ],
-                CheckQuorum                |-> [ i \in Servers   |-> ENABLED CheckQuorum(i) ],
-                Receive                    |-> [ m,n \in Servers |-> ENABLED Receive(m, n) ],
-                RcvAppendEntriesRequest    |-> [ m,n \in Servers |-> ENABLED RcvAppendEntriesRequest(m, n) ],
-                RcvAppendEntriesResponse   |-> [ m,n \in Servers |-> ENABLED RcvAppendEntriesResponse(m, n) ],
-                RcvUpdateTerm              |-> [ m,n \in Servers |-> ENABLED RcvUpdateTerm(m, n) ],
-                RcvRequestVoteRequest      |-> [ m,n \in Servers |-> ENABLED RcvRequestVoteRequest(m, n) ],
-                RcvRequestVoteResponse     |-> [ m,n \in Servers |-> ENABLED RcvRequestVoteResponse(m, n) ]
-            ]
+        logline |-> logline.msg
+
+        \* Uncomment _ENABLED when debugging the enablement state of ccfraft's actions.
+        \* ,_ENABLED |-> 
+        \*     [
+        \*         Timeout                    |-> [ i \in Servers   |-> ENABLED Timeout(i) ],
+        \*         RequestVote                |-> [ i,j \in Servers |-> ENABLED RequestVote(i, j) ],
+        \*         BecomeLeader               |-> [ i \in Servers   |-> ENABLED BecomeLeader(i) ],
+        \*         ClientRequest              |-> [ i \in Servers   |-> ENABLED ClientRequest(i) ],
+        \*         SignCommittableMessages    |-> [ i \in Servers   |-> ENABLED SignCommittableMessages(i) ],
+        \*         ChangeConfiguration        |-> [ i \in Servers   |-> ENABLED ChangeConfiguration(i) ],
+        \*         NotifyCommit               |-> [ i,j \in Servers |-> ENABLED NotifyCommit(i,j) ],
+        \*         AdvanceCommitIndex         |-> [ i \in Servers   |-> ENABLED AdvanceCommitIndex(i) ],
+        \*         AppendEntries              |-> [ i,j \in Servers |-> ENABLED AppendEntries(i, j) ],
+        \*         CheckQuorum                |-> [ i \in Servers   |-> ENABLED CheckQuorum(i) ],
+        \*         Receive                    |-> [ m,n \in Servers |-> ENABLED Receive(m, n) ],
+        \*         RcvAppendEntriesRequest    |-> [ m,n \in Servers |-> ENABLED RcvAppendEntriesRequest(m, n) ],
+        \*         RcvAppendEntriesResponse   |-> [ m,n \in Servers |-> ENABLED RcvAppendEntriesResponse(m, n) ],
+        \*         RcvUpdateTerm              |-> [ m,n \in Servers |-> ENABLED RcvUpdateTerm(m, n) ],
+        \*         RcvRequestVoteRequest      |-> [ m,n \in Servers |-> ENABLED RcvRequestVoteRequest(m, n) ],
+        \*         RcvRequestVoteResponse     |-> [ m,n \in Servers |-> ENABLED RcvRequestVoteResponse(m, n) ]
+        \*     ]
+
         \* See TraceDifferentialInv above.
         \* ,_TraceDiffState |-> LET t == INSTANCE trace IN t!Trace[l]
     ]