Minimize number of TLC configuration files. (#6511)

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
2024-09-30 01:35:32 -07:00 · 2024-09-30 01:35:32 -07:00 · 2069c68c8a
--- 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
--- 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 <https://docs.microsoft.com/en-us/azure/virtual-machines/hbv3-series>`_.

--- 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
--- 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
--- 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.
--- a/tla/consensus/MCccfraft2Nodes.cfg
+++ b/tla/consensus/MCccfraft2Nodes.cfg
@ -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
--- a/tla/consensus/MCccfraftAtomicReconfig.cfg
+++ b/tla/consensus/MCccfraftAtomicReconfig.cfg
@ -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
--- a/tla/consensus/MCccfraftWithReconfig.cfg
+++ b/tla/consensus/MCccfraftWithReconfig.cfg
@ -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