Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Validate the successor state *after* defining it #5797

Merged
merged 5 commits into from
Oct 31, 2023
Merged

Validate the successor state *after* defining it #5797

Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
0545b73
Validate after defining the successor state.
lemmy Oct 27, 2023
1343865
Minor simplification.
lemmy Oct 27, 2023
36f3890
Uncomment _ENABLED when debugging the enablement state of ccfraft's a…
lemmy Oct 30, 2023
2fe7064
Merge branch 'main' into mku-defineThenMatch
achamayou Oct 31, 2023
028eb60
Merge branch 'main' into mku-defineThenMatch
lemmy Oct 31, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
67 changes: 36 additions & 31 deletions tla/consensus/Traceccfraft.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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")
Expand All @@ -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),
Expand All @@ -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")
Expand All @@ -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 ==
Expand Down Expand Up @@ -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")
Expand All @@ -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 ==
Expand Down Expand Up @@ -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]
]
Expand Down