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

Remove NotifyCommit to bring spec closer to implementation #5826

Merged
merged 2 commits into from
Nov 10, 2023
Merged

Remove NotifyCommit to bring spec closer to implementation #5826

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
11b8575
Remove NotifyCommit to bring spec closer to implementation
achamayou Nov 10, 2023
adf45af
Merge branch 'main' into remove_notify_commit
achamayou Nov 10, 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
2 changes: 0 additions & 2 deletions tla/consensus/MCccfraft.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,6 @@ CONSTANTS
ClientRequest <- MCClientRequest
SignCommittableMessages <- MCSignCommittableMessages
ChangeConfigurationInt <- MCChangeConfigurationInt
NotifyCommit <- MCNotifyCommit

Nil = Nil

Expand All @@ -29,7 +28,6 @@ CONSTANTS
RequestVoteResponse = RequestVoteResponse
AppendEntriesRequest = AppendEntriesRequest
AppendEntriesResponse = AppendEntriesResponse
NotifyCommitMessage = NotifyCommitMessage
ProposeVoteRequest = ProposeVoteRequest

OrderedNoDup = OrderedNoDup
Expand Down
9 changes: 1 addition & 8 deletions tla/consensus/MCccfraft.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,13 +88,6 @@ MCSend(msg) ==
/\ n.type = AppendEntriesResponse
/\ CCF!Send(msg)

\* CCF: Limit the number of times a RetiredLeader server sends commit
\* notifications per commit Index and server
MCNotifyCommit(i,j) ==
/\ \/ commitsNotified[i][1] < commitIndex[i]
\/ commitsNotified[i][2] < MaxCommitsNotified
/\ CCF!NotifyCommit(i,j)

\* Limit max number of simultaneous candidates
MCInMaxSimultaneousCandidates(i) ==
Cardinality({ s \in GetServerSetForIndex(i, commitIndex[i]) : state[s] = Candidate}) < 1
Expand Down Expand Up @@ -124,7 +117,7 @@ mc_spec ==
Symmetry == Permutations(Servers)

\* Include all variables in the view, which is similar to defining no view.
View == << reconfigurationVars, <<messages, commitsNotified>>, serverVars, candidateVars, leaderVars, logVars >>
View == << reconfigurationVars, <<messages>>, serverVars, candidateVars, leaderVars, logVars >>

----

Expand Down
2 changes: 0 additions & 2 deletions tla/consensus/MCccfraftAtomicReconfig.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,6 @@ CONSTANTS
ClientRequest <- MCClientRequest
SignCommittableMessages <- MCSignCommittableMessages
ChangeConfigurationInt <- MCChangeConfigurationInt
NotifyCommit <- MCNotifyCommit

Nil = Nil

Expand All @@ -29,7 +28,6 @@ CONSTANTS
RequestVoteResponse = RequestVoteResponse
AppendEntriesRequest = AppendEntriesRequest
AppendEntriesResponse = AppendEntriesResponse
NotifyCommitMessage = NotifyCommitMessage
ProposeVoteRequest = ProposeVoteRequest

OrderedNoDup = OrderedNoDup
Expand Down
2 changes: 0 additions & 2 deletions tla/consensus/MCccfraftWithReconfig.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,6 @@ CONSTANTS
ClientRequest <- MCClientRequest
SignCommittableMessages <- MCSignCommittableMessages
ChangeConfigurationInt <- MCChangeConfigurationInt
NotifyCommit <- MCNotifyCommit

Nil = Nil

Expand All @@ -29,7 +28,6 @@ CONSTANTS
RequestVoteResponse = RequestVoteResponse
AppendEntriesRequest = AppendEntriesRequest
AppendEntriesResponse = AppendEntriesResponse
NotifyCommitMessage = NotifyCommitMessage
ProposeVoteRequest = ProposeVoteRequest

OrderedNoDup = OrderedNoDup
Expand Down
1 change: 0 additions & 1 deletion tla/consensus/SIMCoverageccfraft.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,6 @@ CONSTANTS
RequestVoteResponse = RequestVoteResponse
AppendEntriesRequest = AppendEntriesRequest
AppendEntriesResponse = AppendEntriesResponse
NotifyCommitMessage = NotifyCommitMessage

TypeEntry = Entry
TypeSignature = Signature
Expand Down
5 changes: 2 additions & 3 deletions tla/consensus/SIMCoverageccfraft.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,18 +37,17 @@ SIMCoverageSpec ==
CSVFile == "SIMCoverageccfraft_S" \o ToString(Cardinality(Servers)) \o ".csv"

CSVColumnHeaders ==
"Spec#P#Q#R#reconfigurationCount#committedLog#clientRequests#commitsNotified11#commitsNotified12#currentTerm#state#node"
"Spec#P#Q#R#reconfigurationCount#committedLog#clientRequests#currentTerm#state#node"

ASSUME
CSVRecords(CSVFile) = 0 =>
CSVWrite(CSVColumnHeaders, <<>>, CSVFile)

StatisticsStateConstraint ==
(TLCGet("level") > TLCGet("config").depth) =>
TLCDefer(\A srv \in Servers : CSVWrite("%1$s#%2$s#%3$s#%4$s#%5$s#%6$s#%7$s#%8$s#%9$s#%10$s#%11$s#%12$s",
TLCDefer(\A srv \in Servers : CSVWrite("%1$s#%2$s#%3$s#%4$s#%5$s#%6$s#%7$s#%8$s#%9$s#%10$s",
<< conf[1], Cardinality(conf[2]), Cardinality(conf[3]), Cardinality(conf[4]),
reconfigurationCount, committedLog.index, clientRequests,
commitsNotified[srv][1], commitsNotified[srv][2],
currentTerm[srv], state[srv], srv>>,
CSVFile))
=============================================================================
1 change: 0 additions & 1 deletion tla/consensus/SIMccfraft.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,6 @@ CONSTANTS
RequestVoteResponse = RequestVoteResponse
AppendEntriesRequest = AppendEntriesRequest
AppendEntriesResponse = AppendEntriesResponse
NotifyCommitMessage = NotifyCommitMessage
ProposeVoteRequest = ProposeVoteRequest

OrderedNoDup = OrderedNoDup
Expand Down
1 change: 0 additions & 1 deletion tla/consensus/SIMccfraft.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,6 @@ Forward ==
\/ \E i \in Servers : BecomeLeader(i)
\/ \E i \in Servers : ClientRequest(i)
\/ \E i \in Servers : SignCommittableMessages(i)
\/ \E i, j \in Servers : NotifyCommit(i,j)
\/ \E i \in Servers : AdvanceCommitIndex(i)
\/ \E i, j \in Servers : AppendEntries(i, j)
\/ \E i, j \in Servers : Receive(i, j)
Expand Down
1 change: 0 additions & 1 deletion tla/consensus/Traceccfraft.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,6 @@ CONSTANTS
RequestVoteResponse = RequestVoteResponse
AppendEntriesRequest = AppendEntriesRequest
AppendEntriesResponse = AppendEntriesResponse
NotifyCommitMessage = NotifyCommitMessage
ProposeVoteRequest = ProposeVoteRequest

OrderedNoDup = OrderedNoDup
Expand Down
4 changes: 1 addition & 3 deletions tla/consensus/Traceccfraft.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -141,7 +141,7 @@ logline ==
\* accepting that lost messages remain in messages.
DropMessages ==
/\ l \in 1..Len(TraceLog)
/\ UNCHANGED <<reconfigurationVars, commitsNotified, serverVars, candidateVars, leaderVars, logVars>>
/\ UNCHANGED <<reconfigurationVars, serverVars, candidateVars, leaderVars, logVars>>
/\ UNCHANGED <<l, ts>>
/\ Network!DropMessages(logline.msg.state.node_id)

Expand Down Expand Up @@ -456,7 +456,6 @@ TraceDifferentialInv ==
\* /\ d.removedFromConfiguration = removedFromConfiguration
\* /\ d.configurations = configurations
\* /\ d.messages = messages
\* /\ d.commitsNotified = commitsNotified
\* /\ d.currentTerm = currentTerm
\* /\ d.state = state
\* /\ d.votedFor = votedFor
Expand Down Expand Up @@ -484,7 +483,6 @@ TraceAlias ==
\* 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) ],
Expand Down
Loading