From 6e0ba3a88c93911ce9129dec30f41b5ea75e56c7 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Tue, 31 Oct 2023 16:51:29 +0100 Subject: [PATCH] Validate the successor state *after* defining it (#5797) Co-authored-by: Amaury Chamayou --- tla/consensus/Traceccfraft.tla | 67 ++++++++++++++++++---------------- 1 file changed, 36 insertions(+), 31 deletions(-) diff --git a/tla/consensus/Traceccfraft.tla b/tla/consensus/Traceccfraft.tla index 5700b1145495..b41868f244f7 100644 --- 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] ]