Remove NotifyCommit to bring spec closer to implementation (#5826)

microsoft · Nov 10, 2023 · 56ee39e · 56ee39e
1 parent 942ff3a
commit 56ee39e
Show file tree

Hide file tree

Showing 11 changed files with 20 additions and 91 deletions.
diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg
@@ -15,7 +15,6 @@ CONSTANTS
     ClientRequest <- MCClientRequest
     SignCommittableMessages <- MCSignCommittableMessages
     ChangeConfigurationInt <- MCChangeConfigurationInt
-    NotifyCommit <- MCNotifyCommit
 
     Nil = Nil
 
@@ -29,7 +28,6 @@ CONSTANTS
     RequestVoteResponse = RequestVoteResponse
     AppendEntriesRequest = AppendEntriesRequest
     AppendEntriesResponse = AppendEntriesResponse
-    NotifyCommitMessage = NotifyCommitMessage
     ProposeVoteRequest = ProposeVoteRequest
 
     OrderedNoDup = OrderedNoDup

diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla
@@ -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
@@ -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 >>
 
 ----
 

diff --git a/tla/consensus/MCccfraftAtomicReconfig.cfg b/tla/consensus/MCccfraftAtomicReconfig.cfg
@@ -15,7 +15,6 @@ CONSTANTS
     ClientRequest <- MCClientRequest
     SignCommittableMessages <- MCSignCommittableMessages
     ChangeConfigurationInt <- MCChangeConfigurationInt
-    NotifyCommit <- MCNotifyCommit
 
     Nil = Nil
 
@@ -29,7 +28,6 @@ CONSTANTS
     RequestVoteResponse = RequestVoteResponse
     AppendEntriesRequest = AppendEntriesRequest
     AppendEntriesResponse = AppendEntriesResponse
-    NotifyCommitMessage = NotifyCommitMessage
     ProposeVoteRequest = ProposeVoteRequest
 
     OrderedNoDup = OrderedNoDup

diff --git a/tla/consensus/MCccfraftWithReconfig.cfg b/tla/consensus/MCccfraftWithReconfig.cfg
@@ -15,7 +15,6 @@ CONSTANTS
     ClientRequest <- MCClientRequest
     SignCommittableMessages <- MCSignCommittableMessages
     ChangeConfigurationInt <- MCChangeConfigurationInt
-    NotifyCommit <- MCNotifyCommit
 
     Nil = Nil
 
@@ -29,7 +28,6 @@ CONSTANTS
     RequestVoteResponse = RequestVoteResponse
     AppendEntriesRequest = AppendEntriesRequest
     AppendEntriesResponse = AppendEntriesResponse
-    NotifyCommitMessage = NotifyCommitMessage
     ProposeVoteRequest = ProposeVoteRequest
 
     OrderedNoDup = OrderedNoDup

diff --git a/tla/consensus/SIMCoverageccfraft.cfg b/tla/consensus/SIMCoverageccfraft.cfg
@@ -15,7 +15,6 @@ CONSTANTS
     RequestVoteResponse = RequestVoteResponse
     AppendEntriesRequest = AppendEntriesRequest
     AppendEntriesResponse = AppendEntriesResponse
-    NotifyCommitMessage = NotifyCommitMessage
 
     TypeEntry = Entry
     TypeSignature = Signature

diff --git a/tla/consensus/SIMCoverageccfraft.tla b/tla/consensus/SIMCoverageccfraft.tla
@@ -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))
 =============================================================================
diff --git a/tla/consensus/SIMccfraft.cfg b/tla/consensus/SIMccfraft.cfg
@@ -15,7 +15,6 @@ CONSTANTS
     RequestVoteResponse = RequestVoteResponse
     AppendEntriesRequest = AppendEntriesRequest
     AppendEntriesResponse = AppendEntriesResponse
-    NotifyCommitMessage = NotifyCommitMessage
     ProposeVoteRequest = ProposeVoteRequest
 
     OrderedNoDup = OrderedNoDup

diff --git a/tla/consensus/SIMccfraft.tla b/tla/consensus/SIMccfraft.tla
@@ -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)

diff --git a/tla/consensus/Traceccfraft.cfg b/tla/consensus/Traceccfraft.cfg
@@ -57,7 +57,6 @@ CONSTANTS
     RequestVoteResponse = RequestVoteResponse
     AppendEntriesRequest = AppendEntriesRequest
     AppendEntriesResponse = AppendEntriesResponse
-    NotifyCommitMessage = NotifyCommitMessage
     ProposeVoteRequest = ProposeVoteRequest
 
     OrderedNoDup = OrderedNoDup

diff --git a/tla/consensus/Traceccfraft.tla b/tla/consensus/Traceccfraft.tla
@@ -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)
 
@@ -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
@@ -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) ],