From 144cbe06c006ffbed6c707af17d9bb466fca2f2b Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Tue, 31 Oct 2023 19:58:44 +0000 Subject: [PATCH] Adding a new configuration to the model checking CI (#5802) --- .github/workflows/tlaplus.yml | 5 ++ tla/consensus/MCccfraft.tla | 32 ++++++++-- tla/consensus/MCccfraftAtomicReconfig.cfg | 78 +++++++++++++++++++++++ 3 files changed, 110 insertions(+), 5 deletions(-) create mode 100644 tla/consensus/MCccfraftAtomicReconfig.cfg diff --git a/.github/workflows/tlaplus.yml b/.github/workflows/tlaplus.yml index 0f8f6a808f54..aa81023a858e 100644 --- a/.github/workflows/tlaplus.yml +++ b/.github/workflows/tlaplus.yml @@ -28,6 +28,11 @@ jobs: cd tla/ ./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft.trace.tla -dumpTrace json MCccfraft.json + - name: MCccfraftAtomicReconfig.cfg + run: | + cd tla/ + ./tlc.sh -workers auto -config consensus/MCccfraftAtomicReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftAtomicReconfig.trace.tla -dumpTrace json MCccfraftAtomicReconfig.json + - name: MCccfraftWithReconfig.cfg run: | cd tla/ diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla index 5a2ea96c6b50..d55776707c7b 100644 --- a/tla/consensus/MCccfraft.tla +++ b/tla/consensus/MCccfraft.tla @@ -5,6 +5,7 @@ CONSTANTS NodeOne, NodeTwo, NodeThree 1Configuration == <<{NodeOne, NodeTwo, NodeThree}>> +2Configurations == <<{NodeOne}, {NodeTwo}>> 3Configurations == <<{NodeOne}, {NodeOne, NodeTwo}, {NodeTwo}>> CONSTANT Configurations @@ -24,10 +25,13 @@ 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. + +\* Limit the reconfigurations to the next configuration in Configurations MCChangeConfigurationInt(i, newConfiguration) == - /\ reconfigurationCount < Len(Configurations) + /\ reconfigurationCount < Len(Configurations)-1 \* +1 because TLA+ sequences are 1-index - /\ newConfiguration = Configurations[reconfigurationCount+1] + \* +1 to get the next 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 @@ -49,7 +53,7 @@ MCTimeout(i) == /\ CCF!Timeout(i) \* Limit on client requests -RequestLimit == 2 +RequestLimit == 3 \* Limit number of requests (new entries) that can be made MCClientRequest(i) == @@ -93,7 +97,25 @@ MCNotifyCommit(i,j) == MCInMaxSimultaneousCandidates(i) == Cardinality({ s \in GetServerSetForIndex(i, commitIndex[i]) : state[s] = Candidate}) < 1 -mc_spec == Spec +\* Alternative to CCF!InitReconfigurationVars that sets the initial configuration to the first config defined in Configurations +MCInitReconfigurationVars == + /\ reconfigurationCount = 0 + /\ removedFromConfiguration = {} + /\ configurations = [i \in Servers |-> 0 :> Configurations[1]] + +\* Alternative to CCF!Init that uses the above MCInitReconfigurationVars +MCInit == + /\ MCInitReconfigurationVars + /\ CCF!InitMessagesVars + /\ CCF!InitServerVars + /\ CCF!InitCandidateVars + /\ CCF!InitLeaderVars + /\ CCF!InitLogVars + +\* Alternative to CCF!Spec that uses the above MCInit +mc_spec == + /\ MCInit + /\ [][Next]_vars \* Symmetry set over possible servers. May dangerous and is only enabled \* via the Symmetry option in cfg file. @@ -106,7 +128,7 @@ View == << reconfigurationVars, <>, serverVars, candi AllReconfigurationsCommitted == \E s \in ToServers: - \A c \in ToSet(Configurations): + \A c \in ToSet(Tail(Configurations)): \E i \in DOMAIN Committed(s): /\ HasTypeReconfiguration(Committed(s)[i]) /\ Committed(s)[i].configuration = c diff --git a/tla/consensus/MCccfraftAtomicReconfig.cfg b/tla/consensus/MCccfraftAtomicReconfig.cfg new file mode 100644 index 000000000000..0805ce3b785f --- /dev/null +++ b/tla/consensus/MCccfraftAtomicReconfig.cfg @@ -0,0 +1,78 @@ +SPECIFICATION mc_spec + +CONSTANTS + Configurations <- 2Configurations + Servers <- ToServers + + MaxTermLimit = 4 + MaxCommitsNotified = 2 + + Timeout <- MCTimeout + Send <- MCSend + ClientRequest <- MCClientRequest + SignCommittableMessages <- MCSignCommittableMessages + ChangeConfigurationInt <- MCChangeConfigurationInt + NotifyCommit <- MCNotifyCommit + + Nil = Nil + + Follower = Follower + Candidate = Candidate + Leader = Leader + RetiredLeader = RetiredLeader + Pending = Pending + + RequestVoteRequest = RequestVoteRequest + RequestVoteResponse = RequestVoteResponse + AppendEntriesRequest = AppendEntriesRequest + AppendEntriesResponse = AppendEntriesResponse + NotifyCommitMessage = NotifyCommitMessage + ProposeVoteRequest = ProposeVoteRequest + + OrderedNoDup = OrderedNoDup + Ordered = Ordered + ReorderedNoDup = ReorderedNoDup + Reordered = Reordered + Guarantee = OrderedNoDup + + TypeEntry = Entry + TypeSignature = Signature + TypeReconfiguration = Reconfiguration + + NodeOne = n1 + NodeTwo = n2 + NodeThree = n3 + +SYMMETRY Symmetry +VIEW View + +CHECK_DEADLOCK + FALSE + +PROPERTIES + CommittedLogAppendOnlyProp + MonotonicTermProp + MonotonicMatchIndexProp + PermittedLogChangesProp + StateTransitionsProp + PendingBecomesFollowerProp + NeverCommitEntryPrevTermsProp + +INVARIANTS + LogInv + MoreThanOneLeaderInv + CandidateTermNotInLogInv + ElectionSafetyInv + LogMatchingInv + QuorumLogInv + MoreUpToDateCorrectInv + LeaderCompletenessInv + SignatureInv + TypeInv + MonoTermInv + MonoLogInv + LogConfigurationConsistentInv + NoLeaderInTermZeroInv + MatchIndexLowerBoundNextIndexInv + CommitCommittableIndices + CommittableIndicesAreKnownSignaturesInv \ No newline at end of file