Merge branch 'main' into f/0-remove-quic-doc-page

microsoft · Sep 27, 2024 · c4a2a76 · c4a2a76
2 parents 42dcce4 + 6fb0b5f
commit c4a2a76
Show file tree

Hide file tree

Showing 8 changed files with 125 additions and 15 deletions.
diff --git 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/MCabs.cfg b/tla/consensus/MCabs.cfg
@@ -14,4 +14,6 @@ INVARIANTS
 
 PROPERTIES 
     AppendOnlyProp
-
+
+SYMMETRY 
+    Symmetry
diff --git 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/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
@@ -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
@@ -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
diff --git 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

diff --git 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 == {
-    <<>>,
-    <<StartTerm, StartTerm>>,
-    <<StartTerm, StartTerm, StartTerm, StartTerm>>}
+InitialLogs == 
+    UNION {[ 1..n -> {StartTerm} ] : n \in {0,2,4}}
 
 Init ==
     cLogs \in [Servers -> InitialLogs]