зеркало из https://github.com/microsoft/CCF.git
Refactor state-space constraint into MCccfraft.tla.
This commit is contained in:
Markus Alexander Kuppe
Родитель
c7df1e171b
Коммит
80b9995235
|
|
@ -2,13 +2,13 @@ SPECIFICATION mc_spec
|
|||
|
||||
CONSTANTS
|
||||
Servers <- Servers_mc
|
||||
IsInConfigurations <- MCIsInConfigurations
|
||||
InTermLimit <- MCInTermLimit
|
||||
InRequestLimit <- MCInRequestLimit
|
||||
InRequestVoteLimit <- MCInRequestVoteLimit
|
||||
InMessagesLimit <- MCInMessagesLimit
|
||||
InMaxSimultaneousCandidates <- MCInMaxSimultaneousCandidates
|
||||
InCommitNotificationLimit <- MCInCommitNotificationLimit
|
||||
|
||||
Timeout <- MCTimeout
|
||||
RequestVote <- MCRequestVote
|
||||
Send <- MCSend
|
||||
ClientRequest <- MCClientRequest
|
||||
ChangeConfigurationInt <- MCChangeConfigurationInt
|
||||
NotifyCommit <- MCNotifyCommit
|
||||
|
||||
Nil = Nil
|
||||
|
||||
|
|
|
|||
|
|
@ -4,32 +4,52 @@ EXTENDS ccfraft, TLC
|
|||
Servers_mc == {NodeOne, NodeTwo, NodeThree}
|
||||
Configurations == <<{NodeOne, NodeTwo, NodeThree}>>
|
||||
|
||||
CCF == INSTANCE ccfraft
|
||||
|
||||
\* This file controls the constants as seen below.
|
||||
\* In addition to basic settings of how many nodes are to be model checked,
|
||||
\* the model allows to place additional limitations on the state space of the program.
|
||||
MCIsInConfigurations(i, newConfiguration) ==
|
||||
MCChangeConfigurationInt(i, newConfiguration) ==
|
||||
/\ reconfigurationCount < Len(Configurations)-1
|
||||
\* +1 because TLA+ sequences are 1-index
|
||||
\* +1 to lookup the *next* and not the current configuration.
|
||||
/\ newConfiguration = Configurations[reconfigurationCount+2]
|
||||
/\ CCF!ChangeConfigurationInt(i, newConfiguration)
|
||||
|
||||
\* Limit the terms that can be reached. Needs to be set to at least 3 to
|
||||
\* evaluate all relevant states. If set to only 2, the candidate_quorum
|
||||
\* constraint below is too restrictive.
|
||||
MCInTermLimit(i) ==
|
||||
currentTerm[i] < 1
|
||||
MCTimeout(i) ==
|
||||
\* Limit the term of each server to reduce state space
|
||||
/\ currentTerm[i] < 1
|
||||
\* Limit max number of simultaneous candidates
|
||||
\* We made several restrictions to the state space of Raft. However since we
|
||||
\* made these restrictions, Deadlocks can occur at places that Raft would in
|
||||
\* real-world deployments handle graciously.
|
||||
\* One example of this is if a Quorum of nodes becomes Candidate but can not
|
||||
\* timeout anymore since we constrained the terms. Then, an artificial Deadlock
|
||||
\* is reached. We solve this below. If TermLimit is set to any number >2, this is
|
||||
\* not an issue since breadth-first search will make sure that a similar
|
||||
\* situation is simulated at term==1 which results in a term increase to 2.
|
||||
/\ Cardinality({ s \in GetServerSetForIndex(i, commitIndex[i]) : state[s] = Candidate}) < 1
|
||||
/\ CCF!Timeout(i)
|
||||
|
||||
\* Limit on client requests
|
||||
RequestLimit == 2
|
||||
|
||||
\* Limit number of requests (new entries) that can be made
|
||||
RequestLimit == 2
|
||||
MCInRequestLimit ==
|
||||
clientRequests <= RequestLimit
|
||||
MCClientRequest(i) ==
|
||||
/\ clientRequests <= RequestLimit
|
||||
/\ CCF!ClientRequest(i)
|
||||
|
||||
\* Limit on number of request votes that can be sent to each other node
|
||||
MCInRequestVoteLimit(i,j) ==
|
||||
votesRequested[i][j] < 1
|
||||
MCRequestVote(i,j) ==
|
||||
/\ votesRequested[i][j] < 1
|
||||
/\ CCF!RequestVote(i,j)
|
||||
|
||||
\* CCF: Limit how many identical append entries messages each node can send to another
|
||||
\* Limit number of duplicate messages sent to the same server
|
||||
MCInMessagesLimit(i, j, index, msg) ==
|
||||
MCSend(msg) ==
|
||||
\* One AppendEntriesRequest per node-pair at a time:
|
||||
\* a) No AppendEntries request from i to j.
|
||||
/\ ~ \E n \in Messages:
|
||||
|
|
@ -42,14 +62,14 @@ MCInMessagesLimit(i, j, index, msg) ==
|
|||
/\ n.source = msg.dest
|
||||
/\ n.term = msg.term
|
||||
/\ n.type = AppendEntriesResponse
|
||||
/\ CCF!Send(msg)
|
||||
|
||||
\* Limit number of times a RetiredLeader server sends commit notifications
|
||||
MCInCommitNotificationLimit(i) ==
|
||||
commitsNotified[i][2] < 0
|
||||
|
||||
\* Limit max number of simultaneous candidates
|
||||
MCInMaxSimultaneousCandidates(i) ==
|
||||
Cardinality({ s \in GetServerSetForIndex(i, commitIndex[i]) : state[s] = Candidate}) < 1
|
||||
\* 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] < 0
|
||||
/\ CCF!NotifyCommit(i,j)
|
||||
|
||||
mc_spec == Spec
|
||||
|
||||
|
|
|
|||
|
|
@ -350,45 +350,6 @@ TypeInv ==
|
|||
/\ LeaderVarsTypeInv
|
||||
/\ LogVarsTypeInv
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
\* Fine-grained state constraint "hooks" for model-checking with TLC.
|
||||
|
||||
\* State limitation: Limit requested votes
|
||||
InRequestVoteLimit(i,j) ==
|
||||
TRUE
|
||||
|
||||
\* Limit on terms
|
||||
\* By default, all servers start as followers in term 0
|
||||
InTermLimit(i) ==
|
||||
TRUE
|
||||
|
||||
\* CCF: Limit how many identical append entries messages each node can send to another
|
||||
InMessagesLimit(i, j, index, msg) ==
|
||||
TRUE
|
||||
|
||||
\* CCF: Limit the number of commit notifications per commit Index and server
|
||||
InCommitNotificationLimit(i) ==
|
||||
TRUE
|
||||
|
||||
\* Limit max number of simultaneous candidates
|
||||
\* We made several restrictions to the state space of Raft. However since we
|
||||
\* made these restrictions, Deadlocks can occur at places that Raft would in
|
||||
\* real-world deployments handle graciously.
|
||||
\* One example of this is if a Quorum of nodes becomes Candidate but can not
|
||||
\* timeout anymore since we constrained the terms. Then, an artificial Deadlock
|
||||
\* is reached. We solve this below. If TermLimit is set to any number >2, this is
|
||||
\* not an issue since breadth-first search will make sure that a similar
|
||||
\* situation is simulated at term==1 which results in a term increase to 2.
|
||||
InMaxSimultaneousCandidates(i) ==
|
||||
TRUE
|
||||
|
||||
\* Limit on client requests
|
||||
InRequestLimit ==
|
||||
TRUE
|
||||
|
||||
IsInConfigurations(i, newConfiguration) ==
|
||||
TRUE
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
\* Helpers
|
||||
|
||||
|
|
@ -569,13 +530,8 @@ Init ==
|
|||
|
||||
\* Server i times out and starts a new election.
|
||||
Timeout(i) ==
|
||||
\* Limit the term of each server to reduce state space
|
||||
/\ InTermLimit(i)
|
||||
\* Only servers that are followers/candidates can become candidates
|
||||
/\ state[i] \in {Follower, Candidate}
|
||||
\* Limit number of candidates in our relevant server set
|
||||
\* (i.e., simulate that not more than a given limit of servers in each configuration times out)
|
||||
/\ InMaxSimultaneousCandidates(i)
|
||||
\* Check that the reconfiguration which added this node is at least committable
|
||||
/\ \E c \in DOMAIN configurations[i] :
|
||||
/\ i \in configurations[i][c]
|
||||
|
|
@ -603,7 +559,6 @@ RequestVote(i,j) ==
|
|||
/\ i /= j
|
||||
\* Only requests vote if we are candidate
|
||||
/\ state[i] = Candidate
|
||||
/\ InRequestVoteLimit(i, j)
|
||||
\* Reconfiguration: Make sure j is in a configuration of i
|
||||
/\ IsInServerSet(j, i)
|
||||
/\ votesRequested' = [votesRequested EXCEPT ![i][j] = votesRequested[i][j] + 1]
|
||||
|
|
@ -639,7 +594,6 @@ AppendEntries(i, j) ==
|
|||
IN
|
||||
/\ \E b \in AppendEntriesBatchsize(i, j):
|
||||
LET m == msg(b) IN
|
||||
/\ InMessagesLimit(i, j, b, m)
|
||||
/\ Send(m)
|
||||
\* Record the most recent index we have sent to this node.
|
||||
\* (see https://github.com/microsoft/CCF/blob/9fbde45bf5ab856ca7bcf655e8811dc7baf1e8a3/src/consensus/aft/raft.h#L935-L936)
|
||||
|
|
@ -668,8 +622,6 @@ BecomeLeader(i) ==
|
|||
|
||||
\* Leader i receives a client request to add v to the log.
|
||||
ClientRequest(i) ==
|
||||
\* Limit number of client requests
|
||||
/\ InRequestLimit
|
||||
\* Only leaders receive client requests
|
||||
/\ state[i] = Leader
|
||||
/\ LET entry == [
|
||||
|
|
@ -712,8 +664,6 @@ SignCommittableMessages(i) ==
|
|||
ChangeConfigurationInt(i, newConfiguration) ==
|
||||
\* Only leader can propose changes
|
||||
/\ state[i] = Leader
|
||||
\* Limit reconfigurations
|
||||
/\ IsInConfigurations(i, newConfiguration)
|
||||
\* Configuration is non empty
|
||||
/\ newConfiguration /= {}
|
||||
\* Configuration is a proper subset of the Servers
|
||||
|
|
@ -796,8 +746,7 @@ NotifyCommit(i,j) ==
|
|||
/\ state[i] = RetiredLeader
|
||||
\* Only send notifications of commit to servers in the server set
|
||||
/\ IsInServerSetForIndex(j, i, commitIndex[i])
|
||||
/\ \/ commitsNotified[i][1] < commitIndex[i]
|
||||
\/ InCommitNotificationLimit(i)
|
||||
/\ commitsNotified[i][1] < commitIndex[i]
|
||||
/\ LET new_notified == IF commitsNotified[i][1] = commitIndex[i]
|
||||
THEN <<commitsNotified[i][1], commitsNotified[i][2] + 1>>
|
||||
ELSE <<commitIndex[i], 1>>
|
||||
|
|
|
|||
Загрузка…
Ссылка в новой задаче