From 2069c68c8a4b85344075fdae6588378ec95f24bc Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 30 Sep 2024 01:35:32 -0700 Subject: [PATCH] Minimize number of TLC configuration files. (#6511) Signed-off-by: Markus Alexander Kuppe --- .github/workflows/tlaplus.yml | 16 ++-- doc/architecture/raft_tla.rst | 2 +- tla/StatsFile.tla | 10 ++- tla/consensus/MCccfraft.cfg | 14 ++-- tla/consensus/MCccfraft.tla | 35 ++++++--- tla/consensus/MCccfraft2Nodes.cfg | 93 ---------------------- tla/consensus/MCccfraftAtomicReconfig.cfg | 96 ----------------------- tla/consensus/MCccfraftWithReconfig.cfg | 95 ---------------------- 8 files changed, 46 insertions(+), 315 deletions(-) delete mode 100644 tla/consensus/MCccfraft2Nodes.cfg delete mode 100644 tla/consensus/MCccfraftAtomicReconfig.cfg delete mode 100644 tla/consensus/MCccfraftWithReconfig.cfg diff --git a/.github/workflows/tlaplus.yml b/.github/workflows/tlaplus.yml index 72f54db25dfe..7d3cfa8bdeed 100644 --- a/.github/workflows/tlaplus.yml +++ b/.github/workflows/tlaplus.yml @@ -135,23 +135,23 @@ jobs: cd tla/ ./tlc.sh -workers auto consensus/MCabs.tla -dumpTrace tla MCabs.trace.tla -dumpTrace json MCabs.json - - name: MCccfraft.cfg + - name: MCccfraft - Configurations=1C2N run: | set -x cd tla/ - ./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft.trace.tla -dumpTrace json MCccfraft.json + Configurations=1C2N MaxTermLimit=2 RequestLimit=3 ./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft1C2NT2R3.trace.tla -dumpTrace json MCccfraft1C2NT2R3.json - - name: MCccfraft2Nodes.cfg + - name: MCccfraft - Configurations=1C3N run: | set -x cd tla/ - ./tlc.sh -workers auto -config consensus/MCccfraft2Nodes.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraft2Nodes.trace.tla -dumpTrace json MCccfraft2Nodes.json + Configurations=1C3N MaxTermLimit=2 RequestLimit=3 ./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft1C3N2T3R.trace.tla -dumpTrace json MCccfraft1C3N2T3R.json - - name: MCccfraftAtomicReconfig.cfg + - name: MCccfraft - Configurations=2C2N (atomic reconf) MaxTermLimit=4 RequestLimit=3 NoCheckQuorum run: | set -x cd tla/ - ./tlc.sh -workers auto -config consensus/MCccfraftAtomicReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftAtomicReconfig.trace.tla -dumpTrace json MCccfraftAtomicReconfig.json + Configurations=2C2N MaxTermLimit=4 RequestLimit=1 NoCheckQuorum= ./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft2C2N4T1R.trace.tla -dumpTrace json MCccfraft2C2N4T1R.json - name: Upload TLC's out file as an artifact. Can be imported into the TLA+ Toolbox. uses: actions/upload-artifact@v4 @@ -175,11 +175,11 @@ jobs: sudo apt install -y default-jre python3 ./tla/install_deps.py - - name: MCccfraftWithReconfig.cfg + - name: MCccfraft - Configurations=3C2N MaxTermLimit=4 RequestLimit=1 NoCheckQuorum run: | set -x cd tla/ - ./tlc.sh -workers auto -config consensus/MCccfraftWithReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftWithReconfig.trace.tla -dumpTrace json MCccfraftWithReconfig.json + Configurations=3C2N MaxTermLimit=4 RequestLimit=1 NoCheckQuorum= ./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft3C2N4T1R.trace.tla -dumpTrace json MCccfraft3C2N4T1R.json - name: Upload TLC's out file as an artifact. Can be imported into the TLA+ Toolbox. uses: actions/upload-artifact@v4 diff --git a/doc/architecture/raft_tla.rst b/doc/architecture/raft_tla.rst index d57b739788f7..2a88ce60a4a6 100644 --- a/doc/architecture/raft_tla.rst +++ b/doc/architecture/raft_tla.rst @@ -29,7 +29,7 @@ You can also check the consensus specification including reconfiguration as foll .. code-block:: bash - $ ./tlc.sh consensus/MCccfraft.tla -config consensus/MCccfraftWithReconfig.cfg + $ Configurations=3C2N MaxTermLimit=4 RequestLimit=1 NoCheckQuorum= ./tlc.sh consensus/MCccfraft.tla Using TLC to exhaustively check our models can take any time between minutes (for small configurations) and days (especially for the full consensus model with reconfiguration) on a 128 core VM (specifically, we used an `Azure HBv3 instance `_. diff --git a/tla/StatsFile.tla b/tla/StatsFile.tla index d227deac91e8..a77089170744 100644 --- a/tla/StatsFile.tla +++ b/tla/StatsFile.tla @@ -2,11 +2,17 @@ EXTENDS TLC, Json, Sequences, Naturals, IOUtils \* Filename to write TLC stats to -CONSTANT StatsFilename +StatsFilename == + IF "StatsFileName" \in DOMAIN IOEnv + THEN IOEnv.StatsFileName + ELSE Print("Found no env var StatsFileName. Falling back to MCccfraft_stats.json.", "MCccfraft_stats.json") ASSUME StatsFilename \in STRING \* Filename to write TLC coverage to -CONSTANT CoverageFilename +CoverageFilename == + IF "CoverageFilename" \in DOMAIN IOEnv + THEN IOEnv.CoverageFilename + ELSE Print("Found no env var CoverageFilename. Falling back to MCccfraft_coverage.json.", "MCccfraft_coverage.json") ASSUME CoverageFilename \in STRING \* Writes TLC stats (such as number of states and duration) to StatsFilename in ndJson format diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg index edb36049d08f..8a774bbf336f 100644 --- a/tla/consensus/MCccfraft.cfg +++ b/tla/consensus/MCccfraft.cfg @@ -1,20 +1,14 @@ SPECIFICATION mc_spec CONSTANTS - Configurations <- 1Configuration3Nodes Servers <- ToServers - - MaxTermLimit = 2 - RequestLimit = 3 - - StatsFilename = "MCccfraft_stats.json" - CoverageFilename = "MCccfraft_coverage.json" Timeout <- MCTimeout Send <- MCSend ClientRequest <- MCClientRequest SignCommittableMessages <- MCSignCommittableMessages ChangeConfigurationInt <- MCChangeConfigurationInt + CheckQuorum <- MCCheckQuorum Nil = Nil @@ -59,6 +53,9 @@ CHECK_DEADLOCK POSTCONDITION WriteStatsFile +_PERIODIC + SerializeCoverage + PROPERTIES CommittedLogAppendOnlyProp MonotonicTermProp @@ -68,7 +65,8 @@ PROPERTIES MembershipStateTransitionsProp PendingBecomesFollowerProp NeverCommitEntryPrevTermsProp - RefinementToAbsProp + \* Will be checked after https://github.com/microsoft/CCF/pull/6509 + \* RefinementToAbsProp INVARIANTS LogInv diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla index 222a1719cead..e9844328a74a 100644 --- a/tla/consensus/MCccfraft.tla +++ b/tla/consensus/MCccfraft.tla @@ -1,25 +1,33 @@ ---------- MODULE MCccfraft ---------- -EXTENDS ccfraft, StatsFile, MCAliases +EXTENDS ccfraft, StatsFile, MCAliases, TLC, IOUtils CONSTANTS NodeOne, NodeTwo, NodeThree -\* No reconfiguration -1Configuration2Nodes == <<{NodeOne, NodeTwo}>> -1Configuration3Nodes == <<{NodeOne, NodeTwo, NodeThree}>> -\* Atomic reconfiguration from NodeOne to NodeTwo -2Configurations == <<{NodeOne}, {NodeTwo}>> -\* Incremental reconfiguration from NodeOne to NodeOne and NodeTwo, and then to NodeTwo -3Configurations == <<{NodeOne}, {NodeOne, NodeTwo}, {NodeTwo}>> - -CONSTANT Configurations +Configurations == + LET default == <<{NodeOne, NodeTwo}>> IN + IF "Configurations" \in DOMAIN IOEnv THEN + \* Don't parse and process the string Configurations but keep it simple and just check for known values. + CASE IOEnv.Configurations = "1C1N" -> <<{NodeOne}>> + [] IOEnv.Configurations = "1C2N" -> default + [] IOEnv.Configurations = "1C3N" -> <<{NodeOne, NodeTwo, NodeThree}>> + [] IOEnv.Configurations = "2C2N" -> <<{NodeOne}, {NodeTwo}>> + [] IOEnv.Configurations = "3C2N" -> <<{NodeOne}, {NodeOne, NodeTwo}, {NodeTwo}>> + [] OTHER -> Print("Unknown value for env var Configurations. Falling back to <<{NodeOne, NodeTwo}>>.", default) + ELSE Print("Found no env var Configurations. Falling back to <<{NodeOne, NodeTwo}>>.", default) ASSUME Configurations \in Seq(SUBSET Servers) -CONSTANT MaxTermLimit +MaxTermLimit == + IF "MaxTermLimit" \in DOMAIN IOEnv + THEN atoi(IOEnv.MaxTermLimit) + ELSE Print("Found no env var MaxTermLimit. Falling back to 2 terms.", 2) ASSUME MaxTermLimit \in Nat \* Limit on client requests -CONSTANT RequestLimit +RequestLimit == + IF "RequestLimit" \in DOMAIN IOEnv + THEN atoi(IOEnv.RequestLimit) + ELSE Print("Found no env var RequestLimit. Falling back to 3 requests.", 3) ASSUME RequestLimit \in Nat ToServers == @@ -27,6 +35,9 @@ ToServers == CCF == INSTANCE ccfraft +MCCheckQuorum(i) == + IF "NoCheckQuorum" \in DOMAIN IOEnv THEN FALSE ELSE CCF!CheckQuorum(i) + \* 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. diff --git a/tla/consensus/MCccfraft2Nodes.cfg b/tla/consensus/MCccfraft2Nodes.cfg deleted file mode 100644 index 0faa5fd9f3f5..000000000000 --- a/tla/consensus/MCccfraft2Nodes.cfg +++ /dev/null @@ -1,93 +0,0 @@ -SPECIFICATION mc_spec - -CONSTANTS - Configurations <- 1Configuration2Nodes - Servers <- ToServers - - MaxTermLimit = 4 - RequestLimit = 3 - - StatsFilename = "MCccfraft_stats.json" - CoverageFilename = "MCccfraft_coverage.json" - - Timeout <- MCTimeout - Send <- MCSend - ClientRequest <- MCClientRequest - SignCommittableMessages <- MCSignCommittableMessages - ChangeConfigurationInt <- MCChangeConfigurationInt - - Nil = Nil - - Follower = L_Follower - Candidate = L_Candidate - Leader = L_Leader - None = L_None - - Active = R_Active - RetirementOrdered = R_RetirementOrdered - RetirementSigned = R_RetirementSigned - RetirementCompleted = R_RetirementCompleted - RetiredCommitted = R_RetiredCommitted - - RequestVoteRequest = M_RequestVoteRequest - RequestVoteResponse = M_RequestVoteResponse - AppendEntriesRequest = M_AppendEntriesRequest - AppendEntriesResponse = M_AppendEntriesResponse - ProposeVoteRequest = M_ProposeVoteRequest - - OrderedNoDup = N_OrderedNoDup - Ordered = N_Ordered - ReorderedNoDup = N_ReorderedNoDup - Reordered = N_Reordered - Guarantee = N_OrderedNoDup - - TypeEntry = T_Entry - TypeSignature = T_Signature - TypeReconfiguration = T_Reconfiguration - TypeRetired = T_Retired - - NodeOne = n1 - NodeTwo = n2 - NodeThree = n3 - -SYMMETRY Symmetry -VIEW View - -CHECK_DEADLOCK - FALSE - -POSTCONDITION - WriteStatsFile - -PROPERTIES - CommittedLogAppendOnlyProp - MonotonicTermProp - MonotonicMatchIndexProp - PermittedLogChangesProp - StateTransitionsProp - MembershipStateTransitionsProp - PendingBecomesFollowerProp - NeverCommitEntryPrevTermsProp - \* Does not currently work because abs is Copy XOR Extend on state changes - \* RefinementToAbsProp - -INVARIANTS - LogInv - MoreThanOneLeaderInv - CandidateTermNotInLogInv - ElectionSafetyInv - LogMatchingInv - QuorumLogInv - LeaderCompletenessInv - SignatureInv - TypeInv - MonoTermInv - MonoLogInv - NoLeaderBeforeInitialTerm - LogConfigurationConsistentInv - MembershipStateConsistentInv - CommitCommittableIndices - ReplicationInv - RetiredCommittedInv - RetirementCompletedNotInConfigsInv - RetirementCompletedAreRetirementCompletedInv diff --git a/tla/consensus/MCccfraftAtomicReconfig.cfg b/tla/consensus/MCccfraftAtomicReconfig.cfg deleted file mode 100644 index fe5426e1bed7..000000000000 --- a/tla/consensus/MCccfraftAtomicReconfig.cfg +++ /dev/null @@ -1,96 +0,0 @@ -SPECIFICATION mc_spec - -CONSTANTS - Configurations <- 2Configurations - Servers <- ToServers - - MaxTermLimit = 4 - RequestLimit = 1 - - StatsFilename = "MCccfraftAtomicReconfig_stats.json" - CoverageFilename = "MCccfraftAtomicReconfig_coverage.json" - - Timeout <- MCTimeout - Send <- MCSend - ClientRequest <- MCClientRequest - SignCommittableMessages <- MCSignCommittableMessages - ChangeConfigurationInt <- MCChangeConfigurationInt - \* Disable CheckQuorum when model checking in CI to keep execution time manageable - CheckQuorum <- FALSE - - Nil = Nil - - Follower = L_Follower - Candidate = L_Candidate - Leader = L_Leader - None = L_None - - Active = R_Active - RetirementOrdered = R_RetirementOrdered - RetirementSigned = R_RetirementSigned - RetirementCompleted = R_RetirementCompleted - RetiredCommitted = R_RetiredCommitted - - RequestVoteRequest = M_RequestVoteRequest - RequestVoteResponse = M_RequestVoteResponse - AppendEntriesRequest = M_AppendEntriesRequest - AppendEntriesResponse = M_AppendEntriesResponse - ProposeVoteRequest = M_ProposeVoteRequest - - OrderedNoDup = N_OrderedNoDup - Ordered = N_Ordered - ReorderedNoDup = N_ReorderedNoDup - Reordered = N_Reordered - Guarantee = N_OrderedNoDup - - TypeEntry = T_Entry - TypeSignature = T_Signature - TypeReconfiguration = T_Reconfiguration - TypeRetired = T_Retired - - NodeOne = n1 - NodeTwo = n2 - NodeThree = n3 - -SYMMETRY Symmetry -VIEW View - -CHECK_DEADLOCK - FALSE - -POSTCONDITION - WriteStatsFile - -PROPERTIES - CommittedLogAppendOnlyProp - MonotonicTermProp - MonotonicMatchIndexProp - PermittedLogChangesProp - StateTransitionsProp - MembershipStateTransitionsProp - PendingBecomesFollowerProp - NeverCommitEntryPrevTermsProp - -INVARIANTS - LogInv - MoreThanOneLeaderInv - CandidateTermNotInLogInv - ElectionSafetyInv - LogMatchingInv - QuorumLogInv - LeaderCompletenessInv - SignatureInv - TypeInv - MonoTermInv - MonoLogInv - LogConfigurationConsistentInv - MembershipStateConsistentInv - NoLeaderBeforeInitialTerm - CommitCommittableIndices - ReplicationInv - RetiredCommittedInv - RetirementCompletedNotInConfigsInv - RetirementCompletedAreRetirementCompletedInv - -_PERIODIC - SerializeCoverage \ No newline at end of file diff --git a/tla/consensus/MCccfraftWithReconfig.cfg b/tla/consensus/MCccfraftWithReconfig.cfg deleted file mode 100644 index 62dcb8da95ec..000000000000 --- a/tla/consensus/MCccfraftWithReconfig.cfg +++ /dev/null @@ -1,95 +0,0 @@ -SPECIFICATION mc_spec - -CONSTANTS - Configurations <- 3Configurations - Servers <- ToServers - - MaxTermLimit = 4 - RequestLimit = 1 - - StatsFilename = "MCccfraftWithReconfig_stats.json" - CoverageFilename = "MCccfraftWithReconfig_coverage.json" - - Timeout <- MCTimeout - Send <- MCSend - ClientRequest <- MCClientRequest - SignCommittableMessages <- MCSignCommittableMessages - ChangeConfigurationInt <- MCChangeConfigurationInt - CheckQuorum <- FALSE - - Nil = Nil - - Follower = L_Follower - Candidate = L_Candidate - Leader = L_Leader - None = L_None - - Active = R_Active - RetirementOrdered = R_RetirementOrdered - RetirementSigned = R_RetirementSigned - RetirementCompleted = R_RetirementCompleted - RetiredCommitted = R_RetiredCommitted - - RequestVoteRequest = M_RequestVoteRequest - RequestVoteResponse = M_RequestVoteResponse - AppendEntriesRequest = M_AppendEntriesRequest - AppendEntriesResponse = M_AppendEntriesResponse - ProposeVoteRequest = M_ProposeVoteRequest - - OrderedNoDup = N_OrderedNoDup - Ordered = N_Ordered - ReorderedNoDup = N_ReorderedNoDup - Reordered = N_Reordered - Guarantee = N_OrderedNoDup - - TypeEntry = T_Entry - TypeSignature = T_Signature - TypeReconfiguration = T_Reconfiguration - TypeRetired = T_Retired - - NodeOne = n1 - NodeTwo = n2 - NodeThree = n3 - -SYMMETRY Symmetry -VIEW View - -CHECK_DEADLOCK - FALSE - -POSTCONDITION - WriteStatsFile - -PROPERTIES - CommittedLogAppendOnlyProp - MonotonicTermProp - MonotonicMatchIndexProp - PermittedLogChangesProp - StateTransitionsProp - MembershipStateTransitionsProp - PendingBecomesFollowerProp - NeverCommitEntryPrevTermsProp - -INVARIANTS - LogInv - MoreThanOneLeaderInv - CandidateTermNotInLogInv - ElectionSafetyInv - LogMatchingInv - QuorumLogInv - LeaderCompletenessInv - SignatureInv - TypeInv - MonoTermInv - MonoLogInv - NoLeaderBeforeInitialTerm - LogConfigurationConsistentInv - MembershipStateConsistentInv - CommitCommittableIndices - ReplicationInv - RetiredCommittedInv - RetirementCompletedNotInConfigsInv - RetirementCompletedAreRetirementCompletedInv - -_PERIODIC - SerializeCoverage \ No newline at end of file