From 5e615a9c9790755a1efcbf9ee17e5658fb1e57ea Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Thu, 26 Sep 2024 05:00:39 -0700 Subject: [PATCH 1/3] Revert https://github.com/microsoft/CCF/pull/5939 (#6501) Signed-off-by: Markus Alexander Kuppe --- tla/consensus/SIMccfraft.cfg | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/tla/consensus/SIMccfraft.cfg b/tla/consensus/SIMccfraft.cfg index 17dc9ed0d215..4a40ea248a84 100644 --- a/tla/consensus/SIMccfraft.cfg +++ b/tla/consensus/SIMccfraft.cfg @@ -78,9 +78,8 @@ INVARIANTS CandidateTermNotInLogInv ElectionSafetyInv LogMatchingInv - \* Disabled until retirement is modeled correctly in the spec - \* QuorumLogInv - \* LeaderCompletenessInv + QuorumLogInv + LeaderCompletenessInv SignatureInv ReconfigurationVarsTypeInv From f798800ae9f100b41aa090c41487c39950b37ae0 Mon Sep 17 00:00:00 2001 From: Amaury Chamayou Date: Thu, 26 Sep 2024 21:47:12 +0100 Subject: [PATCH 2/3] Add 2-Node consensus MC (#6504) --- .github/workflows/tlaplus.yml | 6 ++ tla/consensus/MCccfraft.cfg | 2 +- tla/consensus/MCccfraft.tla | 3 +- tla/consensus/MCccfraft2Nodes.cfg | 93 +++++++++++++++++++++++++++++++ 4 files changed, 102 insertions(+), 2 deletions(-) create mode 100644 tla/consensus/MCccfraft2Nodes.cfg diff --git a/.github/workflows/tlaplus.yml b/.github/workflows/tlaplus.yml index 92104052b9b5..72f54db25dfe 100644 --- a/.github/workflows/tlaplus.yml +++ b/.github/workflows/tlaplus.yml @@ -141,6 +141,12 @@ jobs: cd tla/ ./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft.trace.tla -dumpTrace json MCccfraft.json + - name: MCccfraft2Nodes.cfg + 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 + - name: MCccfraftAtomicReconfig.cfg run: | set -x diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg index 4d62a74afacc..edb36049d08f 100644 --- a/tla/consensus/MCccfraft.cfg +++ b/tla/consensus/MCccfraft.cfg @@ -1,7 +1,7 @@ SPECIFICATION mc_spec CONSTANTS - Configurations <- 1Configuration + Configurations <- 1Configuration3Nodes Servers <- ToServers MaxTermLimit = 2 diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla index b314b05e6bf8..222a1719cead 100644 --- a/tla/consensus/MCccfraft.tla +++ b/tla/consensus/MCccfraft.tla @@ -5,7 +5,8 @@ CONSTANTS NodeOne, NodeTwo, NodeThree \* No reconfiguration -1Configuration == <<{NodeOne, NodeTwo, NodeThree}>> +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 diff --git a/tla/consensus/MCccfraft2Nodes.cfg b/tla/consensus/MCccfraft2Nodes.cfg new file mode 100644 index 000000000000..0faa5fd9f3f5 --- /dev/null +++ b/tla/consensus/MCccfraft2Nodes.cfg @@ -0,0 +1,93 @@ +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 From 6fb0b5f0b9c8d70cc780465c5c7d9792be597015 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Thu, 26 Sep 2024 17:50:50 -0700 Subject: [PATCH 3/3] Refactor abstract consensus specification (#6475) * Refactor (simplify) TypeOK to use (more concise) Sequences!Seq operator. * Define InitialLogs less explicitly. * Add assumptions about abs.tla's constants (TLAPS will likely need those assumptions should we attempt writing a proof). * Mitigate state-space explosion during explicit-state model checking by declaring constant Servers to be symmetric. Signed-off-by: Markus Alexander Kuppe --- tla/consensus/MCabs.cfg | 4 +++- tla/consensus/MCabs.tla | 5 ++++- tla/consensus/abs.tla | 22 ++++++++++++++-------- 3 files changed, 21 insertions(+), 10 deletions(-) diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg index 3a104fd2d151..d81a6ab809ed 100644 --- a/tla/consensus/MCabs.cfg +++ b/tla/consensus/MCabs.cfg @@ -14,4 +14,6 @@ INVARIANTS PROPERTIES AppendOnlyProp - \ No newline at end of file + +SYMMETRY + Symmetry \ No newline at end of file diff --git a/tla/consensus/MCabs.tla b/tla/consensus/MCabs.tla index 02abc41ebd58..71fe0967ae23 100644 --- a/tla/consensus/MCabs.tla +++ b/tla/consensus/MCabs.tla @@ -1,6 +1,9 @@ ---- MODULE MCabs ---- -EXTENDS abs +EXTENDS abs, TLC + +Symmetry == + Permutations(Servers) CONSTANTS NodeOne, NodeTwo, NodeThree diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla index b0855392f03d..b1b88e29b4b4 100644 --- a/tla/consensus/abs.tla +++ b/tla/consensus/abs.tla @@ -2,24 +2,30 @@ \* Abstract specification for a distributed consensus algorithm. \* Assumes that any node can atomically inspect the state of all other nodes. -EXTENDS Sequences, SequencesExt, Naturals, FiniteSets, FiniteSetsExt +EXTENDS Sequences, SequencesExt, Naturals, FiniteSets, FiniteSetsExt, Relation -CONSTANT Servers, Terms, MaxLogLength +CONSTANT Servers +ASSUME IsFiniteSet(Servers) + +\* Terms is (strictly) totally ordered with a smallest element. +CONSTANT Terms +ASSUME /\ IsStrictlyTotallyOrderedUnder(<, Terms) + /\ \E min \in Terms : \A t \in Terms : t <= min + +CONSTANT MaxLogLength +ASSUME MaxLogLength \in Nat \* Commit logs from each node \* Each log is append-only and the logs will never diverge. VARIABLE cLogs TypeOK == - /\ cLogs \in [Servers -> - UNION {[1..l -> Terms] : l \in 0..MaxLogLength}] + cLogs \in [Servers -> Seq(Terms)] StartTerm == Min(Terms) -InitialLogs == { - <<>>, - <>, - <>} +InitialLogs == + UNION {[ 1..n -> {StartTerm} ] : n \in {0,2,4}} Init == cLogs \in [Servers -> InitialLogs]