[Proof-of-Concept] Liveness checking ccfraft

tla/consensus/MCabs.cfg

@@ -1,9 +1,10 @@
-SPECIFICATION AbsSpec
+SPECIFICATION WeakFairnessSpec
 
 CONSTANTS
     NodeOne = n1
     NodeTwo = n2
     NodeThree = n3
+    NodeFour = n4
     Servers <- MCServers
     Terms <- MCTerms
     StartTerm <- MCStartTerm
@@ -14,16 +15,36 @@ INVARIANTS
     NoConflicts
     TypeOK
 
-PROPERTIES 
+PROPERTIES
+    \* InSync
+    \* InSyncLockStep
+    Syncing
+    SynchingLockStep
+    AllExtending
+    \* AllExtendingLockStep
+    EmptyLeadsToNonEmpty
     AppendOnlyProp
     \* EquivExtendProp
     \* EquivCopyMaxAndExtendProp
 
-SYMMETRY 
-    Symmetry
+    \* Properties that cause spurious counterexamples here to
+    \* illustrate the limitations of the MonotonicReduction view.
+    \* SpuriousPropA
 
-CONSTRAINT 
-    MaxLogLengthConstraint
+    \* NotAPropA
+    \* NotAPropB
+    \* NotAPropC
+    \* NotAPropD
+    \* NotAPropE
+    \* NotAPropF
+    \* NotAPropG
+    \* NotAPropH
+
+VIEW 
+    MonotonicReduction
+
+CONSTRAINT
+    MaxDivergence
 
 CHECK_DEADLOCK 
     FALSE

tla/consensus/MCabs.tla

@@ -1,6 +1,56 @@
 ---- MODULE MCabs ----
 
-EXTENDS abs, TLC, SequencesExt, FiniteSetsExt
+EXTENDS abs, TLC, SequencesExt, FiniteSetsExt, Integers
+
+\* All (temporal) formulas below are expected to hold but cause a
+\* spurious violation of liveness properties due to our MonothonicReduction
+\* view.
+
+SpuriousPropA ==
+    \* Stenghtened variant of EmptyLeadsToNonEmpty.
+    \A i \in Servers:
+        cLogs[i] = <<>> ~> [](cLogs[i] # <<>>)
+
+----
+
+\* All (temporal) formulas below are expected to result in liveness violations,
+\* as there is nothing in the behavior spec that forces all Terms to be present
+\* in any/all logs.
+
+NotAPropA ==
+    <>(\A i \in Servers: Terms = Range(cLogs[i]) )
+
+NotAPropB ==
+    <>[](\A i \in Servers: Terms = Range(cLogs[i]) )
+
+NotAPropC ==
+    <>(\E i \in Servers: Terms = Range(cLogs[i]) )
+
+NotAPropD ==
+    <>[](\E i \in Servers: Terms = Range(cLogs[i]) )
+
+NotAPropE ==
+    \E i \in Servers:
+        cLogs[i] = <<>> ~> Terms = Range(cLogs[i])
+
+NotAPropF ==
+    \A i \in Servers:
+        \A n \in 1..10: \* 10 is arbitrary but TLC doesn't handle Nat.  LeadsTo is vacausously true if n > Len(cLogs[i]).
+            Len(cLogs[i]) = n ~> cLogs[i] = <<>>
+
+NotAPropG ==
+    \A i \in Servers:
+        \A n \in 1..10:
+            Len(cLogs[i]) = n ~> Len(cLogs[i]) = n - 1
+
+NotAPropH ==
+    \* We would expect NotAPropH to hold if we conjoin  Len(cLogs'[i]) = Len(cLogs[i]) + 1  to abs!Next.
+    \* Instead, we get a spurious violation of liveness properties, similar to SpuriousPropA.
+    \A i \in Servers:
+        \A n \in 0..1:
+            Len(cLogs[i]) = n ~> Len(cLogs[i]) = n + 1
+
+----
 
 Symmetry ==
       Permutations(Servers)
@@ -11,6 +61,12 @@ MCServers == {NodeOne, NodeTwo, NodeThree}
 MCTerms == 2..4
 MCStartTerm == Min(MCTerms)
 MaxExtend == 3
+MCMaxTerm == Max(MCTerms)
+
+ASSUME
+    \* LongestCommonPrefix in View for a single server would always shorten the
+    \* log to <<>>, reducing the state-space to a single state.
+    Cardinality(MCServers) > 1
 
 MCTypeOK ==
     \* 4 because of the initial log.
@@ -19,8 +75,51 @@ MCTypeOK ==
 MCSeq(S) ==
     BoundedSeq(S, MaxExtend)
 
-\* Limit length of logs to terminate model checking.
-MaxLogLengthConstraint ==
-    \A i \in Servers :
-        Len(cLogs[i]) <= 7
+-----
+
+\* Combining the following conditions makes the state space finite:
+\* - Terms is a *finite* set (MCTerms)
+\* - The divergence of any two logs is bounded (MaxDivergence)
+\* - The longest common prefix of all logs is discarded (MonotonicReduction)
+
+Abs(n) ==
+    IF n >= 0 THEN n ELSE -n
+
+MaxDivergence ==
+    \A i, j \in Servers :
+        Abs(Len(cLogs[i]) - Len(cLogs[j])) <= 2
+
+-----
+
+TailFrom(seq, idx) ==
+    SubSeq(seq, idx + 1, Len(seq))
+
+MonotonicReductionLongestCommonPrefix ==
+    \* Find the longest common prefix of all logs and drop it from all logs.
+    LET commonPrefixBound == Len(LongestCommonPrefix(Range(cLogs)))
+    IN [ s \in Servers |-> TailFrom(cLogs[s], commonPrefixBound) ]
+
+MonotonicReductionLongestCommonPrefixAndTerms ==
+    \* Find the longest common prefix of all logs and drop it from all logs.
+    \* We also realign the terms in the remaining suffixes.
+    LET commonPrefixBound == Len(LongestCommonPrefix(Range(cLogs)))
+        minTerm ==
+            \* 3) The minimum term out of all minima.
+            Min({
+                \* 2) The minimum term in the suffix of a log.
+                Min(
+                    \* 1) All terms in the suffix of a log.
+                    Range(TailFrom(cLogs[s], commonPrefixBound))
+                        \* \cup {MCMaxTerm+1} to handle the case where a log is empty.
+                        \* MCMaxTerm+1 to always be greater than any term in the log.
+                        \* If all logs are empty, the minTerm does not matter.
+                        \cup {MCMaxTerm+1}) : s \in Servers})
+        delta == minTerm - StartTerm
+    IN  [ s \in Servers |-> 
+            [ i \in 1..Len(cLogs[s]) - commonPrefixBound |->
+                    cLogs[s][i + commonPrefixBound] - delta ] ]
+
+MonotonicReduction ==
+    MonotonicReductionLongestCommonPrefixAndTerms
+
 ====

tla/consensus/abs.tla

@@ -2,7 +2,7 @@
 \* 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, Relation
+EXTENDS Sequences, SequencesExt, Naturals, FiniteSets, FiniteSetsExt, Relation
 
 CONSTANT Servers
 ASSUME IsFiniteSet(Servers)
@@ -13,7 +13,8 @@ ASSUME /\ IsStrictlyTotallyOrderedUnder(<, Terms)
        /\ \E min \in Terms : \A t \in Terms : t <= min
 
 CONSTANT StartTerm
-ASSUME /\ StartTerm \in Terms
+ASSUME StartTermIsTerm ==
+       /\ StartTerm \in Terms
        /\ \A t \in Terms : StartTerm <= t
 
 \* Commit logs from each node
@@ -90,14 +91,88 @@ OMITTED
 \* The only possible actions are to append log entries.
 \* By construction there cannot be any conflicting log entries
 \* Log entries are copied if the node's log is not the longest.
-Next ==
+NextAxiom ==
     \E i \in Servers : 
         \/ Copy(i) 
         \/ ExtendAxiom(i)
         \/ CopyMaxAndExtendAxiom(i)
 
-AbsSpec == Init /\ [][Next]_cLogs
+SpecAxiom == Init /\ [][NextAxiom]_cLogs
+
+Next ==
+    \E i \in Servers : 
+        \/ Copy(i) 
+        \/ Extend(i)
+        \/ CopyMaxAndExtend(i)
+
+Spec ==
+    Init /\ [][Next]_cLogs
+
+THEOREM Spec <=> SpecAxiom
+
+----
+\* Liveness
+
+InSync ==
+    \A i, j \in Servers : []<>(cLogs[i] = cLogs[j])
+
+InSyncLockStep ==
+    []<>(\A i, j \in Servers : cLogs[i] = cLogs[j])
+
+LEMMA InSyncLockStep => InSync
+
+Syncing ==
+    \* There exists one server whose log is repeatedly strictly extended.
+    \E s \in Servers: []<><<IsStrictPrefix(cLogs[s], cLogs'[s])>>_cLogs
+
+SynchingLockStep ==
+    \* Repeatedly, there exists a state where one server's log is strictly extended.
+    []<><<\E s \in Servers: IsStrictPrefix(cLogs[s], cLogs'[s])>>_cLogs
+
+AllExtending ==
+    \* Repeatedly, all logs of all servers are strictly extended.  However, it
+    \* is not required that all logs are strictly extended in the same state.
+    \A s \in Servers: []<><<IsStrictPrefix(cLogs[s], cLogs'[s])>>_cLogs
+
+AllExtendingLockStep ==
+    \* Repeatedly, there exists a state where all logs are strictly extended.
+    []<><<\A s \in Servers: IsStrictPrefix(cLogs[s], cLogs'[s])>>_cLogs
+
+LEMMA AllExtendingLockStep => AllExtending
+
+EmptyLeadsToNonEmpty ==
+    \A i \in Servers:
+        cLogs[i] = <<>> ~> cLogs[i] # <<>>
+
+FairSpecLockStep ==
+    /\ Spec
+    \* There repeatedly exists a state where the logs of all servers are synced.
+    /\ WF_cLogs(Next) /\ []<><<\A s,t \in Servers: cLogs'[s] = cLogs'[t]>>_cLogs
+
+FairSpec ==
+    /\ Spec
+    \* For all pairs of logs, there repeatedly exists a state where they are synced.
+    /\ WF_cLogs(Next) /\ \A s,t \in Servers: []<><<cLogs'[s] = cLogs'[t]>>_cLogs
+
+WeakFairnessSpec ==
+    /\ Spec
+    /\ WF_cLogs(Next)
+
+THEOREM FairSpecLockStep => 
+    (Syncing /\ SynchingLockStep /\ AllExtending /\ InSync /\ InSyncLockStep /\ EmptyLeadsToNonEmpty)
+
+THEOREM FairSpec =>
+    (Syncing /\ SynchingLockStep /\ AllExtending /\ InSync /\ EmptyLeadsToNonEmpty)
+
+THEOREM WeakFairnessSpec => 
+    (Syncing /\ SynchingLockStep /\ AllExtending /\ EmptyLeadsToNonEmpty)
+
+----
 
+\* abs models ccfraft's logs up to the commitIndex and the extension of the
+\* leader’s log past the commitIndex.  However, contrary to ccfraft, the
+\* leader’s log in abs is never trimmed.  The corresponding property in
+\* ccfraft is CommittedLogAppendOnlyProp.
 AppendOnlyProp ==
     [][\A i \in Servers : IsPrefix(cLogs[i], cLogs'[i])]_cLogs
 

tla/consensus/abs_proof.tla

@@ -0,0 +1,10 @@
+---- MODULE abs_proof ----
+EXTENDS abs, TLAPS
+
+LEMMA Spec => TypeOK
+<1> USE DEF TypeOK
+<1>1. Init => TypeOK BY StartTermIsTerm DEF Init, InitialLogs
+<1>2. TypeOK /\ [Next]_cLogs => TypeOK' BY DEF Next, Extend, Copy, CopyMaxAndExtend
+<1>. QED BY <1>1, <1>2, PTL DEF Spec
+
+======

tla/consensus/ccfraft.tla

@@ -1633,7 +1633,7 @@ MappingToAbs ==
     Terms <- Nat \ 0..StartTerm-1,
     cLogs <- [i \in Servers |-> [j \in 1..commitIndex[i] |-> log[i][j].term]]
 
-RefinementToAbsProp == MappingToAbs!AbsSpec
+RefinementToAbsProp == MappingToAbs!SpecAxiom
 THEOREM Spec => RefinementToAbsProp
 
 ------------------------------------------------------------------------------