diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg index 72e062bdbd34..ee9a7c1697df 100644 --- a/tla/consensus/MCabs.cfg +++ b/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 diff --git a/tla/consensus/MCabs.tla b/tla/consensus/MCabs.tla index 89b571c8c63d..371e0c0e7704 100644 --- a/tla/consensus/MCabs.tla +++ b/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 + ==== \ No newline at end of file diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla index 15968333d554..a665073d3c64 100644 --- a/tla/consensus/abs.tla +++ b/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: []<><>_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: []<><>_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 + +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 diff --git a/tla/consensus/abs_proof.tla b/tla/consensus/abs_proof.tla new file mode 100644 index 000000000000..520bbed8e82c --- /dev/null +++ b/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 + +====== \ No newline at end of file diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla index e969df7f626b..cebe7aaea9ef 100644 --- a/tla/consensus/ccfraft.tla +++ b/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 ------------------------------------------------------------------------------