From aba804ebd772b20d88f6df11275d4fbe17e86b73 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Tue, 22 Oct 2024 17:40:26 -0700 Subject: [PATCH 01/25] * Add Spec and SpecAxiom * Add FairSpec and InSync property * Comment TypeOK because violated by (non-axiom) Spec (TLC checks invariants even for states that are excluded by a state constraint) The liveness property `InSync` should be violated because the fairness constraint is too weak. However, TLC won't find the violation because of the naive state constraint. ```shell -> % tlc -note MCabs.tla TLC2 Version 2.20 of Day Month 20?? (rev: cc65eef) Running breadth-first search Model-Checking with fp 47 and seed 8464703399013400155 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 58100] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.25 x86_64, MSBDiskFPSet, DiskStateQueue). Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/MCabs.tla Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/abs.tla Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14783782376297602783/TLC.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14783782376297602783/SequencesExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/SequencesExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14783782376297602783/FiniteSetsExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/FiniteSetsExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14783782376297602783/Sequences.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14783782376297602783/Naturals.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14783782376297602783/FiniteSets.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14783782376297602783/Relation.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Relation.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14783782376297602783/Folds.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Folds.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14783782376297602783/Functions.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Functions.tla) Semantic processing of module Naturals Semantic processing of module Sequences Semantic processing of module FiniteSets Semantic processing of module Folds Semantic processing of module Functions Semantic processing of module FiniteSetsExt Semantic processing of module TLC Semantic processing of module SequencesExt Semantic processing of module Relation Semantic processing of module abs Semantic processing of module MCabs Starting... (2024-10-22 17:44:30) Implied-temporal checking--satisfiability problem has 1 branches. Computing initial states... Computed 2 initial states... Computed 4 initial states... Computed 8 initial states... Computed 16 initial states... Finished computing initial states: 27 distinct states generated at 2024-10-22 17:44:30. Checking temporal properties for the current state space with 1698 total distinct states at (2024-10-22 17:44:33) Finished checking temporal properties in 00s at 2024-10-22 17:44:33 Progress(4) at 2024-10-22 17:44:33: 292,065 states generated (292,065 s/min), 33,113 distinct states found (33,113 ds/min), 31,441 states left on queue. Checking temporal properties for the current state space with 69444 total distinct states at (2024-10-22 17:45:33) Finished checking temporal properties in 00s at 2024-10-22 17:45:33 Progress(5) at 2024-10-22 17:45:33: 12,119,265 states generated (11,827,200 s/min), 372,262 distinct states found (339,149 ds/min), 302,817 states left on queue. Checking temporal properties for the current state space with 154698 total distinct states at (2024-10-22 17:46:33) Finished checking temporal properties in 01s at 2024-10-22 17:46:35 Progress(5) at 2024-10-22 17:46:35: 27,220,596 states generated (15,101,331 s/min), 467,752 distinct states found (95,490 ds/min), 313,053 states left on queue. Checking temporal properties for the current state space with 244201 total distinct states at (2024-10-22 17:47:35) Finished checking temporal properties in 02s at 2024-10-22 17:47:38 Progress(5) at 2024-10-22 17:47:38: 42,968,607 states generated (15,748,011 s/min), 487,462 distinct states found (19,710 ds/min), 243,260 states left on queue. Checking temporal properties for the current state space with 345878 total distinct states at (2024-10-22 17:48:38) Finished checking temporal properties in 03s at 2024-10-22 17:48:42 Progress(6) at 2024-10-22 17:48:42: 63,237,877 states generated (20,269,270 s/min), 490,432 distinct states found (2,970 ds/min), 144,553 states left on queue. Checking temporal properties for the current state space with 451165 total distinct states at (2024-10-22 17:49:42) Finished checking temporal properties in 05s at 2024-10-22 17:49:47 Progress(6) at 2024-10-22 17:49:47: 84,563,041 states generated (21,325,164 s/min), 490,432 distinct states found (0 ds/min), 39,266 states left on queue. Progress(6) at 2024-10-22 17:50:16: 94,419,147 states generated, 490,432 distinct states found, 0 states left on queue. Checking temporal properties for the complete state space with 490432 total distinct states at (2024-10-22 17:50:16) Finished checking temporal properties in 05s at 2024-10-22 17:50:22 Model checking completed. No error has been found. Estimates of the probability that TLC did not check all reachable states because two distinct states had the same fingerprint: calculated (optimistic): val = 2.5E-6 based on the actual fingerprints: val = 2.6E-8 94419147 states generated, 490432 distinct states found, 0 states left on queue. The depth of the complete state graph search is 6. The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 31 and the 95th percentile is 4). Finished in 05min 52s at (2024-10-22 17:50:22) ``` Signed-off-by: Markus Alexander Kuppe --- tla/consensus/MCabs.cfg | 8 +++----- tla/consensus/abs.tla | 27 +++++++++++++++++++++++++-- tla/consensus/ccfraft.tla | 2 +- 3 files changed, 29 insertions(+), 8 deletions(-) diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg index 72e062bdbd34..05c2990f5cd9 100644 --- a/tla/consensus/MCabs.cfg +++ b/tla/consensus/MCabs.cfg @@ -1,4 +1,4 @@ -SPECIFICATION AbsSpec +SPECIFICATION FairSpec CONSTANTS NodeOne = n1 @@ -12,16 +12,14 @@ CONSTANTS INVARIANTS NoConflicts - TypeOK + \* TypeOK \* Commented because violated with non-axiomatic Spec PROPERTIES + InSync AppendOnlyProp \* EquivExtendProp \* EquivCopyMaxAndExtendProp -SYMMETRY - Symmetry - CONSTRAINT MaxLogLengthConstraint diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla index 15968333d554..12a46ab87e40 100644 --- a/tla/consensus/abs.tla +++ b/tla/consensus/abs.tla @@ -90,13 +90,36 @@ 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 + +---- + +FairSpec == + Spec /\ WF_cLogs(Next) \* TODO Won't suffice for InSync. + +InSync == + []<>(\A i, j \in Servers : cLogs[i] = cLogs[j]) + +THEOREM Spec => InSync + +---- AppendOnlyProp == [][\A i \in Servers : IsPrefix(cLogs[i], cLogs'[i])]_cLogs 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 ------------------------------------------------------------------------------ From 080c981224c017081e3ae502c8f8b7f0755fea3a Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Tue, 22 Oct 2024 18:03:38 -0700 Subject: [PATCH 02/25] * Second state constraint that binds the divergence of any two logs * Add the MonotonicReduction disjunct to Next that reduces the infinite state space to a finite one As expected, the action property AppendOnlyProp is immediately violated: ```shell -> % tlc -note MCabs.tla TLC2 Version 2.20 of Day Month 20?? (rev: cc65eef) Running breadth-first search Model-Checking with fp 46 and seed 9013274278368943051 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 60575] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.25 x86_64, MSBDiskFPSet, DiskStateQueue). Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/MCabs.tla Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/abs.tla Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-17957423033042532951/TLC.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-17957423033042532951/SequencesExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/SequencesExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-17957423033042532951/FiniteSetsExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/FiniteSetsExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-17957423033042532951/Integers.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Integers.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-17957423033042532951/Sequences.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-17957423033042532951/Naturals.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-17957423033042532951/FiniteSets.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-17957423033042532951/Relation.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Relation.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-17957423033042532951/Folds.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Folds.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-17957423033042532951/Functions.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Functions.tla) Semantic processing of module Naturals Semantic processing of module Sequences Semantic processing of module FiniteSets Semantic processing of module Folds Semantic processing of module Functions Semantic processing of module FiniteSetsExt Semantic processing of module TLC Semantic processing of module SequencesExt Semantic processing of module Relation Semantic processing of module abs Semantic processing of module Integers Semantic processing of module MCabs Starting... (2024-10-22 18:02:23) Implied-temporal checking--satisfiability problem has 1 branches. Computing initial states... Computed 2 initial states... Computed 4 initial states... Computed 8 initial states... Computed 16 initial states... Finished computing initial states: 27 states generated, with 15 of them distinct at 2024-10-22 18:02:23. Error: Action property AppendOnlyProp is violated. Error: The behavior up to this point is: State 1: cLogs = (n1 :> <<2, 2>> @@ n2 :> <<2, 2>> @@ n3 :> <<2, 2>>) State 2: cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>>) 2153 states generated, 90 distinct states found, 82 states left on queue. The depth of the complete state graph search is 2. Finished in 00s at (2024-10-22 18:02:23) ``` Signed-off-by: Markus Alexander Kuppe --- tla/consensus/MCabs.cfg | 1 + tla/consensus/MCabs.tla | 10 +++++++++- tla/consensus/abs.tla | 14 +++++++++++++- 3 files changed, 23 insertions(+), 2 deletions(-) diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg index 05c2990f5cd9..ccfd3fc8ab14 100644 --- a/tla/consensus/MCabs.cfg +++ b/tla/consensus/MCabs.cfg @@ -22,6 +22,7 @@ PROPERTIES CONSTRAINT MaxLogLengthConstraint + MaxDivergence CHECK_DEADLOCK FALSE diff --git a/tla/consensus/MCabs.tla b/tla/consensus/MCabs.tla index 89b571c8c63d..5260d063436d 100644 --- a/tla/consensus/MCabs.tla +++ b/tla/consensus/MCabs.tla @@ -1,6 +1,6 @@ ---- MODULE MCabs ---- -EXTENDS abs, TLC, SequencesExt, FiniteSetsExt +EXTENDS abs, TLC, SequencesExt, FiniteSetsExt, Integers Symmetry == Permutations(Servers) @@ -23,4 +23,12 @@ MCSeq(S) == MaxLogLengthConstraint == \A i \in Servers : Len(cLogs[i]) <= 7 + +Abs(n) == + IF n >= 0 THEN n ELSE -n + +MaxDivergence == + \A i, j \in Servers : + Abs(Len(cLogs[i]) - Len(cLogs[j])) <= 2 + ==== \ No newline at end of file diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla index 12a46ab87e40..0b596869001f 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) @@ -98,11 +98,23 @@ NextAxiom == SpecAxiom == Init /\ [][NextAxiom]_cLogs +TailFrom(seq, idx) == + SubSeq(seq, idx + 1, Len(seq)) + +MonotonicReduction == + \* Find the longest common prefix of all logs and drop it from all logs. We realign the terms in the remaining suffixes to start at StartTerm. + LET lcp == LongestCommonPrefix(Range(cLogs)) + commonPrefixBound == Len(lcp) + minTerm == Min({Min(Range(TailFrom(cLogs[s], commonPrefixBound)) \cup {0}) : s \in Servers}) \* \cup {0} to handle the case where the log is empty. + IN + cLogs' = [ s \in Servers |-> [i \in 1..Len(cLogs[s])-commonPrefixBound |-> cLogs[s][i + commonPrefixBound] - minTerm ] ] + Next == \E i \in Servers : \/ Copy(i) \/ Extend(i) \/ CopyMaxAndExtend(i) + \/ MonotonicReduction Spec == Init /\ [][Next]_cLogs From 26a445c340d8ccbfef993bcb1080a5adf331dc63 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Tue, 22 Oct 2024 18:08:45 -0700 Subject: [PATCH 03/25] Commenting AppendOnlyProp make TLC find a violation of InSync ```tla -> % tlc -note MCabs.tla TLC2 Version 2.20 of Day Month 20?? (rev: cc65eef) Running breadth-first search Model-Checking with fp 40 and seed 2933531752807036538 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 61862] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.25 x86_64, MSBDiskFPSet, DiskStateQueue). Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/MCabs.tla Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/abs.tla Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13148651527763708847/TLC.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13148651527763708847/SequencesExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/SequencesExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13148651527763708847/FiniteSetsExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/FiniteSetsExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13148651527763708847/Integers.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Integers.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13148651527763708847/Sequences.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13148651527763708847/Naturals.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13148651527763708847/FiniteSets.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13148651527763708847/Relation.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Relation.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13148651527763708847/Folds.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Folds.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13148651527763708847/Functions.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Functions.tla) Semantic processing of module Naturals Semantic processing of module Sequences Semantic processing of module FiniteSets Semantic processing of module Folds Semantic processing of module Functions Semantic processing of module FiniteSetsExt Semantic processing of module TLC Semantic processing of module SequencesExt Semantic processing of module Relation Semantic processing of module abs Semantic processing of module Integers Semantic processing of module MCabs Starting... (2024-10-22 18:07:45) Implied-temporal checking--satisfiability problem has 1 branches. Computing initial states... Computed 2 initial states... Computed 4 initial states... Computed 8 initial states... Computed 16 initial states... Finished computing initial states: 27 states generated, with 15 of them distinct at 2024-10-22 18:07:45. Checking temporal properties for the current state space with 2979 total distinct states at (2024-10-22 18:07:48) Error: Temporal properties were violated. Error: The following behavior constitutes a counter-example: State 1: cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2, 2>>) State 2: cLogs = (n1 :> <<2, 2>> @@ n2 :> <<>> @@ n3 :> <<2, 2>>) State 3: cLogs = (n1 :> <<2, 2>> @@ n2 :> <<2, 2, 4, 4>> @@ n3 :> <<2, 2>>) State 4: cLogs = (n1 :> <<2, 2, 4, 4>> @@ n2 :> <<2, 2, 4, 4>> @@ n3 :> <<2, 2>>) State 5: cLogs = (n1 :> <<2, 2, 4, 4>> @@ n2 :> <<2, 2, 4, 4>> @@ n3 :> <<2, 2, 4, 4, 2, 2>>) Back to state 1: Finished checking temporal properties in 00s at 2024-10-22 18:07:48 614674 states generated, 9999 distinct states found, 7020 states left on queue. The depth of the complete state graph search is 6. Finished in 03s at (2024-10-22 18:07:48) ``` Signed-off-by: Markus Alexander Kuppe --- tla/consensus/MCabs.cfg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg index ccfd3fc8ab14..ed05a89b3a81 100644 --- a/tla/consensus/MCabs.cfg +++ b/tla/consensus/MCabs.cfg @@ -16,7 +16,7 @@ INVARIANTS PROPERTIES InSync - AppendOnlyProp + \* AppendOnlyProp \* Violated if MonotonicityReduction disjoined to Next. \* EquivExtendProp \* EquivCopyMaxAndExtendProp From 415168d00fd804a52010ccfe87c5e4e3d46b99e9 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Tue, 22 Oct 2024 18:17:11 -0700 Subject: [PATCH 04/25] TLC finds a valid counterexample for another *insufficient* fairness constraint: ```tla -> % tlc -note MCabs.tla TLC2 Version 2.20 of Day Month 20?? (rev: cc65eef) Running breadth-first search Model-Checking with fp 112 and seed -8448579411904421790 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 62776] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.25 x86_64, MSBDiskFPSet, DiskStateQueue). Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/MCabs.tla Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/abs.tla Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11473022655680028070/TLC.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11473022655680028070/SequencesExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/SequencesExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11473022655680028070/FiniteSetsExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/FiniteSetsExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11473022655680028070/Integers.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Integers.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11473022655680028070/Sequences.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11473022655680028070/Naturals.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11473022655680028070/FiniteSets.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11473022655680028070/Relation.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Relation.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11473022655680028070/Folds.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Folds.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11473022655680028070/Functions.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Functions.tla) Semantic processing of module Naturals Semantic processing of module Sequences Semantic processing of module FiniteSets Semantic processing of module Folds Semantic processing of module Functions Semantic processing of module FiniteSetsExt Semantic processing of module TLC Semantic processing of module SequencesExt Semantic processing of module Relation Semantic processing of module abs Semantic processing of module Integers Semantic processing of module MCabs Starting... (2024-10-22 18:13:27) Implied-temporal checking--satisfiability problem has 1 branches. Computing initial states... Computed 2 initial states... Computed 4 initial states... Computed 8 initial states... Computed 16 initial states... Finished computing initial states: 27 states generated, with 15 of them distinct at 2024-10-22 18:13:27. Checking temporal properties for the current state space with 2633 total distinct states at (2024-10-22 18:13:30) Error: Temporal properties were violated. Error: The following behavior constitutes a counter-example: State 1: cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2, 2>>) State 2: cLogs = (n1 :> <<2, 2>> @@ n2 :> <<>> @@ n3 :> <<2, 2>>) State 3: cLogs = (n1 :> <<2, 2>> @@ n2 :> <<2, 2, 2, 4>> @@ n3 :> <<2, 2>>) State 4: cLogs = (n1 :> <<2, 2>> @@ n2 :> <<2, 2, 2, 4>> @@ n3 :> <<2, 2, 2, 4>>) State 5: cLogs = (n1 :> <<2, 2, 2, 4, 4, 3>> @@ n2 :> <<2, 2, 2, 4>> @@ n3 :> <<2, 2, 2, 4>>) State 6: cLogs = (n1 :> <<4, 3>> @@ n2 :> <<>> @@ n3 :> <<>>) State 7: cLogs = (n1 :> <<4, 3>> @@ n2 :> <<4, 3>> @@ n3 :> <<>>) State 8: cLogs = (n1 :> <<4, 3>> @@ n2 :> <<4, 3>> @@ n3 :> <<4, 3, 2, 2>>) Back to state 1: Finished checking temporal properties in 00s at 2024-10-22 18:13:30 530896 states generated, 7831 distinct states found, 5198 states left on queue. The depth of the complete state graph search is 6. Finished in 03s at (2024-10-22 18:13:30) ``` Signed-off-by: Markus Alexander Kuppe --- tla/consensus/abs.tla | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla index 0b596869001f..ed0c85c5394f 100644 --- a/tla/consensus/abs.tla +++ b/tla/consensus/abs.tla @@ -124,7 +124,7 @@ THEOREM Spec <=> SpecAxiom ---- FairSpec == - Spec /\ WF_cLogs(Next) \* TODO Won't suffice for InSync. + Spec /\ \A i \in Servers: WF_cLogs(CopyMaxAndExtend(i)) InSync == []<>(\A i, j \in Servers : cLogs[i] = cLogs[j]) From a2f61b3be96b787f8e89a241cf697709d9643631 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Tue, 22 Oct 2024 18:21:40 -0700 Subject: [PATCH 05/25] Converting MonotonicReduction into a TLC view allows us to again verify AppendOnlyProp. However, TLC produces a bogus counterexample for InSync: ```tla -> % tlc -note MCabs.tla TLC2 Version 2.20 of Day Month 20?? (rev: cc65eef) Running breadth-first search Model-Checking with fp 40 and seed -6940681262185035164 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 63895] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.25 x86_64, MSBDiskFPSet, DiskStateQueue). Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/MCabs.tla Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/abs.tla Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4426784817192118700/TLC.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4426784817192118700/SequencesExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/SequencesExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4426784817192118700/FiniteSetsExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/FiniteSetsExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4426784817192118700/Integers.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Integers.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4426784817192118700/Sequences.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4426784817192118700/Naturals.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4426784817192118700/FiniteSets.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4426784817192118700/Relation.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Relation.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4426784817192118700/Folds.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Folds.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4426784817192118700/Functions.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Functions.tla) Semantic processing of module Naturals Semantic processing of module Sequences Semantic processing of module FiniteSets Semantic processing of module Folds Semantic processing of module Functions Semantic processing of module FiniteSetsExt Semantic processing of module TLC Semantic processing of module SequencesExt Semantic processing of module Relation Semantic processing of module abs Semantic processing of module Integers Semantic processing of module MCabs Starting... (2024-10-22 18:18:47) Implied-temporal checking--satisfiability problem has 1 branches. Computing initial states... Computed 2 initial states... Computed 4 initial states... Computed 8 initial states... Computed 16 initial states... Finished computing initial states: 27 states generated, with 7 of them distinct at 2024-10-22 18:18:47. Progress(3) at 2024-10-22 18:18:47: 26,895 states generated, 127 distinct states found, 0 states left on queue. Checking temporal properties for the complete state space with 127 total distinct states at (2024-10-22 18:18:47) Error: Temporal properties were violated. Error: The following behavior constitutes a counter-example: State 1: cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2, 2>>) State 2: cLogs = (n1 :> <<2, 2>> @@ n2 :> <<>> @@ n3 :> <<2, 2>>) State 3: cLogs = (n1 :> <<2, 2>> @@ n2 :> <<2, 2, 2, 3>> @@ n3 :> <<2, 2>>) State 4: cLogs = (n1 :> <<2, 2>> @@ n2 :> <<2, 2, 2, 3>> @@ n3 :> <<2, 2, 2, 3>>) State 5: cLogs = (n1 :> <<2, 2, 2, 3, 2, 3>> @@ n2 :> <<2, 2, 2, 3>> @@ n3 :> <<2, 2, 2, 3>>) State 6: cLogs = (n1 :> <<2, 2, 2, 3, 2, 3>> @@ n2 :> <<2, 2, 2, 3, 2, 3>> @@ n3 :> <<2, 2, 2, 3>>) Back to state 1: Finished checking temporal properties in 00s at 2024-10-22 18:18:47 26895 states generated, 127 distinct states found, 0 states left on queue. The depth of the complete state graph search is 3. Finished in 00s at (2024-10-22 18:18:47) ``` Related: * https://github.com/tlaplus/tlaplus/issues/1045 * https://github.com/tlaplus/tlaplus/issues/854 Signed-off-by: Markus Alexander Kuppe --- tla/consensus/MCabs.cfg | 7 +++++-- tla/consensus/MCabs.tla | 13 ++++++++++++- tla/consensus/abs.tla | 12 ------------ 3 files changed, 17 insertions(+), 15 deletions(-) diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg index ed05a89b3a81..4b92e62d2b14 100644 --- a/tla/consensus/MCabs.cfg +++ b/tla/consensus/MCabs.cfg @@ -12,14 +12,17 @@ CONSTANTS INVARIANTS NoConflicts - \* TypeOK \* Commented because violated with non-axiomatic Spec + TypeOK PROPERTIES InSync - \* AppendOnlyProp \* Violated if MonotonicityReduction disjoined to Next. + AppendOnlyProp \* EquivExtendProp \* EquivCopyMaxAndExtendProp +VIEW + MonotonicReduction + CONSTRAINT MaxLogLengthConstraint MaxDivergence diff --git a/tla/consensus/MCabs.tla b/tla/consensus/MCabs.tla index 5260d063436d..a19a36f1e17e 100644 --- a/tla/consensus/MCabs.tla +++ b/tla/consensus/MCabs.tla @@ -30,5 +30,16 @@ Abs(n) == MaxDivergence == \A i, j \in Servers : Abs(Len(cLogs[i]) - Len(cLogs[j])) <= 2 - + +TailFrom(seq, idx) == + SubSeq(seq, idx + 1, Len(seq)) + +MonotonicReduction == + \* Find the longest common prefix of all logs and drop it from all logs. We realign the terms in the remaining suffixes to start at StartTerm. + LET lcp == LongestCommonPrefix(Range(cLogs)) + commonPrefixBound == Len(lcp) + minTerm == Min({Min(Range(TailFrom(cLogs[s], commonPrefixBound)) \cup {0}) : s \in Servers}) \* \cup {0} to handle the case where the log is empty. + IN + [ s \in Servers |-> [i \in 1..Len(cLogs[s])-commonPrefixBound |-> cLogs[s][i + commonPrefixBound] - minTerm ] ] + ==== \ No newline at end of file diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla index ed0c85c5394f..8c4e0f5d891d 100644 --- a/tla/consensus/abs.tla +++ b/tla/consensus/abs.tla @@ -98,23 +98,11 @@ NextAxiom == SpecAxiom == Init /\ [][NextAxiom]_cLogs -TailFrom(seq, idx) == - SubSeq(seq, idx + 1, Len(seq)) - -MonotonicReduction == - \* Find the longest common prefix of all logs and drop it from all logs. We realign the terms in the remaining suffixes to start at StartTerm. - LET lcp == LongestCommonPrefix(Range(cLogs)) - commonPrefixBound == Len(lcp) - minTerm == Min({Min(Range(TailFrom(cLogs[s], commonPrefixBound)) \cup {0}) : s \in Servers}) \* \cup {0} to handle the case where the log is empty. - IN - cLogs' = [ s \in Servers |-> [i \in 1..Len(cLogs[s])-commonPrefixBound |-> cLogs[s][i + commonPrefixBound] - minTerm ] ] - Next == \E i \in Servers : \/ Copy(i) \/ Extend(i) \/ CopyMaxAndExtend(i) - \/ MonotonicReduction Spec == Init /\ [][Next]_cLogs From 6bb27e5a5918b596806aec03942eede7bed1445f Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Tue, 22 Oct 2024 18:25:57 -0700 Subject: [PATCH 06/25] The deliberate introduction of a bug is correctly found by TLC: ```tla -> % tlc -note MCabs.tla TLC2 Version 2.20 of Day Month 20?? (rev: cc65eef) Running breadth-first search Model-Checking with fp 69 and seed 7965754324960689978 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 65817] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.25 x86_64, MSBDiskFPSet, DiskStateQueue). Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/MCabs.tla Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/abs.tla Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-5146248408337384612/TLC.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-5146248408337384612/SequencesExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/SequencesExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-5146248408337384612/FiniteSetsExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/FiniteSetsExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-5146248408337384612/Integers.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Integers.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-5146248408337384612/Sequences.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-5146248408337384612/Naturals.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-5146248408337384612/FiniteSets.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-5146248408337384612/Relation.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Relation.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-5146248408337384612/Folds.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Folds.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-5146248408337384612/Functions.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Functions.tla) Semantic processing of module Naturals Semantic processing of module Sequences Semantic processing of module FiniteSets Semantic processing of module Folds Semantic processing of module Functions Semantic processing of module FiniteSetsExt Semantic processing of module TLC Semantic processing of module SequencesExt Semantic processing of module Relation Semantic processing of module abs Semantic processing of module Integers Semantic processing of module MCabs Starting... (2024-10-22 18:24:24) Computing initial states... Computed 2 initial states... Computed 4 initial states... Computed 8 initial states... Computed 16 initial states... Finished computing initial states: 27 states generated, with 7 of them distinct at 2024-10-22 18:24:24. Error: Action property AppendOnlyProp is violated. Error: The behavior up to this point is: State 1: cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2, 2>>) State 2: cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2>>) 632 states generated, 46 distinct states found, 44 states left on queue. The depth of the complete state graph search is 2. Finished in 00s at (2024-10-22 18:24:24) ``` Signed-off-by: Markus Alexander Kuppe --- tla/consensus/MCabs.cfg | 4 ++-- tla/consensus/abs.tla | 5 ++++- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg index 4b92e62d2b14..aca388485e7a 100644 --- a/tla/consensus/MCabs.cfg +++ b/tla/consensus/MCabs.cfg @@ -11,11 +11,11 @@ CONSTANTS TypeOK <- MCTypeOK INVARIANTS - NoConflicts +\* NoConflicts TypeOK PROPERTIES - InSync + \* InSync AppendOnlyProp \* EquivExtendProp \* EquivCopyMaxAndExtendProp diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla index 8c4e0f5d891d..b289c37509b4 100644 --- a/tla/consensus/abs.tla +++ b/tla/consensus/abs.tla @@ -63,6 +63,9 @@ LEMMA ASSUME NEW i \in Servers PROVE ExtendAxiom(i) <=> Extend(i) OMITTED +TTail(seq) == + IF seq = <<>> THEN <<>> ELSE Tail(seq) + \* Copy one of the longest logs (from whoever server \* has it) and extend it further upto length k. This \* is equivalent to Copy(i) \cdot Extend(i, k) , @@ -71,7 +74,7 @@ CopyMaxAndExtend(i) == \E j \in Servers : /\ \A r \in Servers: Len(cLogs[r]) \leq Len(cLogs[j]) /\ \E s \in Seq(Terms) : - cLogs' = [cLogs EXCEPT ![i] = cLogs[j] \o s] + cLogs' = [cLogs EXCEPT ![i] = TTail(cLogs[j]) \o s] CopyMaxAndExtendAxiom(i) == \E s \in Servers : From d0378d29e90472aa88a707044e2a3ecc12b86af3 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Tue, 22 Oct 2024 18:30:52 -0700 Subject: [PATCH 07/25] No violation with a non-machine closed fairness constraint: ```tla -> % tlc -note MCabs.tla TLC2 Version 2.20 of Day Month 20?? (rev: cc65eef) Running breadth-first search Model-Checking with fp 51 and seed -2425574771500255732 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 67342] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.25 x86_64, MSBDiskFPSet, DiskStateQueue). Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/MCabs.tla Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/abs.tla Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13080965223161871241/TLC.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13080965223161871241/SequencesExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/SequencesExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13080965223161871241/FiniteSetsExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/FiniteSetsExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13080965223161871241/Integers.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Integers.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13080965223161871241/Sequences.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13080965223161871241/Naturals.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13080965223161871241/FiniteSets.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13080965223161871241/Relation.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Relation.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13080965223161871241/Folds.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Folds.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13080965223161871241/Functions.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Functions.tla) Semantic processing of module Naturals Semantic processing of module Sequences Semantic processing of module FiniteSets Semantic processing of module Folds Semantic processing of module Functions Semantic processing of module FiniteSetsExt Semantic processing of module TLC Semantic processing of module SequencesExt Semantic processing of module Relation Semantic processing of module abs Semantic processing of module Integers Semantic processing of module MCabs Starting... (2024-10-22 18:30:15) Implied-temporal checking--satisfiability problem has 1 branches. Computing initial states... Computed 2 initial states... Computed 4 initial states... Computed 8 initial states... Computed 16 initial states... Finished computing initial states: 27 states generated, with 7 of them distinct at 2024-10-22 18:30:15. Progress(3) at 2024-10-22 18:30:16: 26,895 states generated, 127 distinct states found, 0 states left on queue. Checking temporal properties for the complete state space with 127 total distinct states at (2024-10-22 18:30:16) Finished checking temporal properties in 00s at 2024-10-22 18:30:16 Model checking completed. No error has been found. Estimates of the probability that TLC did not check all reachable states because two distinct states had the same fingerprint: calculated (optimistic): val = 1.8E-13 26895 states generated, 127 distinct states found, 0 states left on queue. The depth of the complete state graph search is 3. The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 31 and the 95th percentile is 4). Finished in 00s at (2024-10-22 18:30:16) ``` Signed-off-by: Markus Alexander Kuppe --- tla/consensus/MCabs.cfg | 4 ++-- tla/consensus/abs.tla | 11 ++++------- 2 files changed, 6 insertions(+), 9 deletions(-) diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg index aca388485e7a..4b92e62d2b14 100644 --- a/tla/consensus/MCabs.cfg +++ b/tla/consensus/MCabs.cfg @@ -11,11 +11,11 @@ CONSTANTS TypeOK <- MCTypeOK INVARIANTS -\* NoConflicts + NoConflicts TypeOK PROPERTIES - \* InSync + InSync AppendOnlyProp \* EquivExtendProp \* EquivCopyMaxAndExtendProp diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla index b289c37509b4..1637144ca295 100644 --- a/tla/consensus/abs.tla +++ b/tla/consensus/abs.tla @@ -63,9 +63,6 @@ LEMMA ASSUME NEW i \in Servers PROVE ExtendAxiom(i) <=> Extend(i) OMITTED -TTail(seq) == - IF seq = <<>> THEN <<>> ELSE Tail(seq) - \* Copy one of the longest logs (from whoever server \* has it) and extend it further upto length k. This \* is equivalent to Copy(i) \cdot Extend(i, k) , @@ -74,7 +71,7 @@ CopyMaxAndExtend(i) == \E j \in Servers : /\ \A r \in Servers: Len(cLogs[r]) \leq Len(cLogs[j]) /\ \E s \in Seq(Terms) : - cLogs' = [cLogs EXCEPT ![i] = TTail(cLogs[j]) \o s] + cLogs' = [cLogs EXCEPT ![i] = cLogs[j] \o s] CopyMaxAndExtendAxiom(i) == \E s \in Servers : @@ -114,12 +111,12 @@ THEOREM Spec <=> SpecAxiom ---- -FairSpec == - Spec /\ \A i \in Servers: WF_cLogs(CopyMaxAndExtend(i)) - InSync == []<>(\A i, j \in Servers : cLogs[i] = cLogs[j]) +FairSpec == + Spec /\ InSync + THEOREM Spec => InSync ---- From 33d617e9389afb4dc1b878524056afea2c1d091b Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 23 Oct 2024 11:39:55 -0700 Subject: [PATCH 08/25] Replace fairness constraint that turns FairSpec => InSync into a tautology into a sufficient constraint that is not a tautology. However, the fairness constraint is not machine closed, and it is stronger than it has to be. In fact, we only need "long enough" sequences of Copy actions, but we cannot express "long enough". Signed-off-by: Markus Alexander Kuppe --- tla/consensus/abs.tla | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla index 1637144ca295..8f8b16e9f6bd 100644 --- a/tla/consensus/abs.tla +++ b/tla/consensus/abs.tla @@ -115,9 +115,10 @@ InSync == []<>(\A i, j \in Servers : cLogs[i] = cLogs[j]) FairSpec == - Spec /\ InSync + /\ Spec + /\ WF_cLogs(Next) /\ \A s \in Servers: <>[][Copy(s)]_cLogs -THEOREM Spec => InSync +THEOREM FairSpec => InSync ---- From d6adf9a0dd8fa4c68becd9197409a54373db3684 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 28 Oct 2024 09:39:23 -0700 Subject: [PATCH 09/25] Note the differences of AppendOnlyProp and ccfraft's CommittedLogAppendOnlyProp. Signed-off-by: Markus Alexander Kuppe --- tla/consensus/abs.tla | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla index 8f8b16e9f6bd..fd336b4c2bdf 100644 --- a/tla/consensus/abs.tla +++ b/tla/consensus/abs.tla @@ -122,6 +122,10 @@ THEOREM FairSpec => InSync ---- +\* 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 From 5bfccc292f18ff22dadc6b86a49783e4077b02be Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 28 Oct 2024 09:53:16 -0700 Subject: [PATCH 10/25] InSync cannot be guaranteed without a non-machine-close fairness constraint because it requires the leader to let followers to catch up. However, the leader cannot know how far a follower is behind, unless it can atomically access/read that follower's state. ```tla -> % tlc -note MCabs.tla TLC2 Version 2.20 of Day Month 20?? (rev: cc65eef) Running breadth-first search Model-Checking with fp 128 and seed -4337590855307700118 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 20380] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.25 x86_64, MSBDiskFPSet, DiskStateQueue). Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/MCabs.tla Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/abs.tla Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15636453091352892932/TLC.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15636453091352892932/SequencesExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/SequencesExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15636453091352892932/FiniteSetsExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/FiniteSetsExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15636453091352892932/Integers.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Integers.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15636453091352892932/Sequences.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15636453091352892932/Naturals.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15636453091352892932/FiniteSets.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15636453091352892932/Relation.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Relation.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15636453091352892932/Folds.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Folds.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15636453091352892932/Functions.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Functions.tla) Semantic processing of module Naturals Semantic processing of module Sequences Semantic processing of module FiniteSets Semantic processing of module Folds Semantic processing of module Functions Semantic processing of module FiniteSetsExt Semantic processing of module TLC Semantic processing of module SequencesExt Semantic processing of module Relation Semantic processing of module abs Semantic processing of module Integers Semantic processing of module MCabs Starting... (2024-10-28 09:56:39) Implied-temporal checking--satisfiability problem has 1 branches. Computing initial states... Computed 2 initial states... Computed 4 initial states... Computed 8 initial states... Computed 16 initial states... Finished computing initial states: 27 states generated, with 7 of them distinct at 2024-10-28 09:56:39. Progress(3) at 2024-10-28 09:56:40: 26,895 states generated, 127 distinct states found, 0 states left on queue. Checking temporal properties for the complete state space with 127 total distinct states at (2024-10-28 09:56:40) Error: Temporal properties were violated. Error: The following behavior constitutes a counter-example: State 1: cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2, 2>>) State 2: cLogs = (n1 :> <<2, 2>> @@ n2 :> <<>> @@ n3 :> <<2, 2>>) State 3: cLogs = (n1 :> <<2, 2>> @@ n2 :> <<2, 2, 2, 2>> @@ n3 :> <<2, 2>>) State 4: cLogs = (n1 :> <<2, 2, 2, 2>> @@ n2 :> <<2, 2, 2, 2>> @@ n3 :> <<2, 2>>) Back to state 1: Finished checking temporal properties in 00s at 2024-10-28 09:56:40 26895 states generated, 127 distinct states found, 0 states left on queue. The depth of the complete state graph search is 3. Finished in 01s at (2024-10-28 09:56:40) ``` Signed-off-by: Markus Alexander Kuppe --- tla/consensus/MCabs.cfg | 2 +- tla/consensus/abs.tla | 4 ++++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg index 4b92e62d2b14..af085e43a004 100644 --- a/tla/consensus/MCabs.cfg +++ b/tla/consensus/MCabs.cfg @@ -1,4 +1,4 @@ -SPECIFICATION FairSpec +SPECIFICATION MachineClosedFairSpec CONSTANTS NodeOne = n1 diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla index fd336b4c2bdf..f1774679909e 100644 --- a/tla/consensus/abs.tla +++ b/tla/consensus/abs.tla @@ -120,6 +120,10 @@ FairSpec == THEOREM FairSpec => InSync +MachineClosedFairSpec == + /\ Spec + /\ WF_cLogs(Next) + ---- \* abs models ccfraft's logs up to the commitIndex and the extension of the From 647e4c7ba356cbfeceafd8e4db434654b7675d8e Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 28 Oct 2024 10:05:56 -0700 Subject: [PATCH 11/25] Syntactically refactor MonotonicReduction. Signed-off-by: Markus Alexander Kuppe --- tla/consensus/MCabs.tla | 25 ++++++++++++++++--------- 1 file changed, 16 insertions(+), 9 deletions(-) diff --git a/tla/consensus/MCabs.tla b/tla/consensus/MCabs.tla index a19a36f1e17e..6774a54672ae 100644 --- a/tla/consensus/MCabs.tla +++ b/tla/consensus/MCabs.tla @@ -31,15 +31,22 @@ MaxDivergence == \A i, j \in Servers : Abs(Len(cLogs[i]) - Len(cLogs[j])) <= 2 -TailFrom(seq, idx) == - SubSeq(seq, idx + 1, Len(seq)) - MonotonicReduction == - \* Find the longest common prefix of all logs and drop it from all logs. We realign the terms in the remaining suffixes to start at StartTerm. - LET lcp == LongestCommonPrefix(Range(cLogs)) - commonPrefixBound == Len(lcp) - minTerm == Min({Min(Range(TailFrom(cLogs[s], commonPrefixBound)) \cup {0}) : s \in Servers}) \* \cup {0} to handle the case where the log is empty. - IN - [ s \in Servers |-> [i \in 1..Len(cLogs[s])-commonPrefixBound |-> cLogs[s][i + commonPrefixBound] - minTerm ] ] + LET TailFrom(seq, idx) == SubSeq(seq, idx + 1, Len(seq)) + \* Find the longest common prefix of all logs and drop it from all logs. + \* We realign the terms in the remaining suffixes to start at StartTerm. + 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 {0} to handle the case where a log is empty. + \cup {0}) : s \in Servers}) + IN [ s \in Servers |-> + [ i \in 1..Len(cLogs[s]) - commonPrefixBound |-> + cLogs[s][i + commonPrefixBound] - minTerm ] ] ==== \ No newline at end of file From 71e50d7fa82ce2017a7203045b3b880cdcd8609f Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 28 Oct 2024 10:08:48 -0700 Subject: [PATCH 12/25] Add second liveness property Syncing that mandates that the log of at least one server is repeatedly extended. With InSync commented in MCabs.cfg. ```tla -> % tlc -note MCabs.tla TLC2 Version 2.20 of Day Month 20?? (rev: cc65eef) Running breadth-first search Model-Checking with fp 121 and seed -4916710017190118041 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 26014] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.25 x86_64, MSBDiskFPSet, DiskStateQueue). Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/MCabs.tla Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/abs.tla Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-974701093072543730/TLC.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-974701093072543730/SequencesExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/SequencesExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-974701093072543730/FiniteSetsExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/FiniteSetsExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-974701093072543730/Integers.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Integers.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-974701093072543730/Sequences.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-974701093072543730/Naturals.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-974701093072543730/FiniteSets.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-974701093072543730/Relation.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Relation.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-974701093072543730/Folds.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Folds.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-974701093072543730/Functions.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Functions.tla) Semantic processing of module Naturals Semantic processing of module Sequences Semantic processing of module FiniteSets Semantic processing of module Folds Semantic processing of module Functions Semantic processing of module FiniteSetsExt Semantic processing of module TLC Semantic processing of module SequencesExt Semantic processing of module Relation Semantic processing of module abs Semantic processing of module Integers Semantic processing of module MCabs Starting... (2024-10-28 10:16:11) Implied-temporal checking--satisfiability problem has 1 branches. Computing initial states... Computed 2 initial states... Computed 4 initial states... Computed 8 initial states... Computed 16 initial states... Finished computing initial states: 27 states generated, with 7 of them distinct at 2024-10-28 10:16:11. Progress(3) at 2024-10-28 10:16:12: 26,895 states generated, 127 distinct states found, 0 states left on queue. Checking temporal properties for the complete state space with 127 total distinct states at (2024-10-28 10:16:12) Finished checking temporal properties in 00s at 2024-10-28 10:16:12 Model checking completed. No error has been found. Estimates of the probability that TLC did not check all reachable states because two distinct states had the same fingerprint: calculated (optimistic): val = 1.8E-13 26895 states generated, 127 distinct states found, 0 states left on queue. The depth of the complete state graph search is 3. The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 31 and the 95th percentile is 4). Finished in 00s at (2024-10-28 10:16:12) ``` Signed-off-by: Markus Alexander Kuppe --- tla/consensus/MCabs.cfg | 1 + tla/consensus/abs.tla | 11 +++++++++++ 2 files changed, 12 insertions(+) diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg index af085e43a004..8ef524eba5f3 100644 --- a/tla/consensus/MCabs.cfg +++ b/tla/consensus/MCabs.cfg @@ -16,6 +16,7 @@ INVARIANTS PROPERTIES InSync + Syncing AppendOnlyProp \* EquivExtendProp \* EquivCopyMaxAndExtendProp diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla index f1774679909e..dd4e2abb4021 100644 --- a/tla/consensus/abs.tla +++ b/tla/consensus/abs.tla @@ -124,6 +124,17 @@ MachineClosedFairSpec == /\ Spec /\ WF_cLogs(Next) +Syncing == + \* At the level of ccfraft, the desired property is that commitIndex of + \* all (active) nodes repeatedly increases, i.e., + \* []<>(\A s \in Servers: commitIndex[s] < commitIndex'[s]) + \* . Note the \le and not \leq comparison! This is stronger (and a liveness + \* property) compared to + \* [][\A s \in Servers: commitIndex[s] < commitIndex'[s]]_commitIndex + []<><<\E s \in Servers: IsStrictPrefix(cLogs[s], cLogs'[s])>>_cLogs + +THEOREM MachineClosedFairSpec => Syncing + ---- \* abs models ccfraft's logs up to the commitIndex and the extension of the From 14e386656602815e93036865a6f5fb389dfe6407 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 28 Oct 2024 10:31:49 -0700 Subject: [PATCH 13/25] As expect, AllSyncing is not a theorem of the spec: ```tla -> % tlc -note MCabs.tla TLC2 Version 2.20 of Day Month 20?? (rev: cc65eef) Running breadth-first search Model-Checking with fp 8 and seed -6640873860738991250 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 28225] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.25 x86_64, MSBDiskFPSet, DiskStateQueue). Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/MCabs.tla Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/abs.tla Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/TLC.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/SequencesExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/SequencesExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/FiniteSetsExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/FiniteSetsExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/Integers.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Integers.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/Sequences.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/Naturals.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/FiniteSets.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/Relation.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Relation.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/Folds.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Folds.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/Functions.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Functions.tla) Semantic processing of module Naturals Semantic processing of module Sequences Semantic processing of module FiniteSets Semantic processing of module Folds Semantic processing of module Functions Semantic processing of module FiniteSetsExt Semantic processing of module TLC Semantic processing of module SequencesExt Semantic processing of module Relation Semantic processing of module abs Semantic processing of module Integers Semantic processing of module MCabs Starting... (2024-10-28 10:30:27) Implied-temporal checking--satisfiability problem has 1 branches. Computing initial states... Computed 2 initial states... Computed 4 initial states... Computed 8 initial states... Computed 16 initial states... Finished computing initial states: 27 states generated, with 7 of them distinct at 2024-10-28 10:30:27. Progress(3) at 2024-10-28 10:30:28: 26,895 states generated, 127 distinct states found, 0 states left on queue. Checking temporal properties for the complete state space with 127 total distinct states at (2024-10-28 10:30:28) Error: Temporal properties were violated. Error: The following behavior constitutes a counter-example: State 1: cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>>) State 2: cLogs = (n1 :> <<3, 2>> @@ n2 :> <<>> @@ n3 :> <<>>) State 3: cLogs = (n1 :> <<3, 2>> @@ n2 :> <<3, 2>> @@ n3 :> <<>>) Back to state 1: Finished checking temporal properties in 00s at 2024-10-28 10:30:28 26895 states generated, 127 distinct states found, 0 states left on queue. The depth of the complete state graph search is 3. Finished in 00s at (2024-10-28 10:30:28) ``` Signed-off-by: Markus Alexander Kuppe --- tla/consensus/MCabs.cfg | 1 + tla/consensus/abs.tla | 4 ++++ 2 files changed, 5 insertions(+) diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg index 8ef524eba5f3..4e275454c56f 100644 --- a/tla/consensus/MCabs.cfg +++ b/tla/consensus/MCabs.cfg @@ -17,6 +17,7 @@ INVARIANTS PROPERTIES InSync Syncing + AllSyncing AppendOnlyProp \* EquivExtendProp \* EquivCopyMaxAndExtendProp diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla index dd4e2abb4021..f76a14891666 100644 --- a/tla/consensus/abs.tla +++ b/tla/consensus/abs.tla @@ -135,6 +135,10 @@ Syncing == THEOREM MachineClosedFairSpec => Syncing +AllSyncing == + []<><<\A s \in Servers: IsStrictPrefix(cLogs[s], cLogs'[s])>>_cLogs + +\* NOT A THEOREM: MachineClosedFairSpec => AllSyncing ---- \* abs models ccfraft's logs up to the commitIndex and the extension of the From b0084915b6a19be7df51db2bd984c6623b15132f Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 28 Oct 2024 10:51:41 -0700 Subject: [PATCH 14/25] Prove abs type-correct. Proved with TLAPS built from git commit ffb8846ff3c49d53ee6eeedfc4c8c4c409306ae3 https://github.com/tlaplus/tlapm/commit/ffb8846ff3c49d53ee6eeedfc4c8c4c409306ae3 Signed-off-by: Markus Alexander Kuppe --- tla/consensus/abs.tla | 3 ++- tla/consensus/abs_proof.tla | 10 ++++++++++ 2 files changed, 12 insertions(+), 1 deletion(-) create mode 100644 tla/consensus/abs_proof.tla diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla index f76a14891666..840e6fae8419 100644 --- a/tla/consensus/abs.tla +++ b/tla/consensus/abs.tla @@ -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 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 From f9980440e041da25f4ff324bdfbda719a4c6f5cd Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 28 Oct 2024 11:08:14 -0700 Subject: [PATCH 15/25] The properties InSync and AllSyncing are not expected to hold for MachineClosedFairSpec. Signed-off-by: Markus Alexander Kuppe --- tla/consensus/MCabs.cfg | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg index 4e275454c56f..dd94f29d3008 100644 --- a/tla/consensus/MCabs.cfg +++ b/tla/consensus/MCabs.cfg @@ -15,9 +15,10 @@ INVARIANTS TypeOK PROPERTIES - InSync + \* InSync and AllSyncing not expected to hold for MachineClosedFairSpec. + \* InSync + \* AllSyncing Syncing - AllSyncing AppendOnlyProp \* EquivExtendProp \* EquivCopyMaxAndExtendProp From cb2e45587e9e10cbf85187c14f088d0edcf36764 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 28 Oct 2024 11:40:54 -0700 Subject: [PATCH 16/25] No need to constrain the log length under a view and a bounded divergence. Signed-off-by: Markus Alexander Kuppe --- tla/consensus/MCabs.cfg | 3 +-- tla/consensus/MCabs.tla | 5 ----- 2 files changed, 1 insertion(+), 7 deletions(-) diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg index dd94f29d3008..7e4c2bc3359e 100644 --- a/tla/consensus/MCabs.cfg +++ b/tla/consensus/MCabs.cfg @@ -26,8 +26,7 @@ PROPERTIES VIEW MonotonicReduction -CONSTRAINT - MaxLogLengthConstraint +CONSTRAINT MaxDivergence CHECK_DEADLOCK diff --git a/tla/consensus/MCabs.tla b/tla/consensus/MCabs.tla index 6774a54672ae..95caa16530e3 100644 --- a/tla/consensus/MCabs.tla +++ b/tla/consensus/MCabs.tla @@ -19,11 +19,6 @@ MCTypeOK == MCSeq(S) == BoundedSeq(S, MaxExtend) -\* Limit length of logs to terminate model checking. -MaxLogLengthConstraint == - \A i \in Servers : - Len(cLogs[i]) <= 7 - Abs(n) == IF n >= 0 THEN n ELSE -n From 90925c95e8b0ee6b190ee9f39fb119c53972b1f0 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 28 Oct 2024 14:53:23 -0700 Subject: [PATCH 17/25] Refactor liveness properties. Signed-off-by: Markus Alexander Kuppe --- tla/consensus/MCabs.cfg | 9 ++++--- tla/consensus/abs.tla | 53 +++++++++++++++++++++++++++++------------ 2 files changed, 44 insertions(+), 18 deletions(-) diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg index 7e4c2bc3359e..16195fe110f1 100644 --- a/tla/consensus/MCabs.cfg +++ b/tla/consensus/MCabs.cfg @@ -4,6 +4,7 @@ CONSTANTS NodeOne = n1 NodeTwo = n2 NodeThree = n3 + NodeFour = n4 Servers <- MCServers Terms <- MCTerms StartTerm <- MCStartTerm @@ -14,11 +15,13 @@ INVARIANTS NoConflicts TypeOK -PROPERTIES - \* InSync and AllSyncing not expected to hold for MachineClosedFairSpec. +PROPERTIES \* InSync - \* AllSyncing + \* InSyncLockStep Syncing + SynchingLockStep + AllExtending + \* AllExtendingLockStep AppendOnlyProp \* EquivExtendProp \* EquivCopyMaxAndExtendProp diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla index 840e6fae8419..282bece14ce9 100644 --- a/tla/consensus/abs.tla +++ b/tla/consensus/abs.tla @@ -111,35 +111,58 @@ Spec == THEOREM Spec <=> SpecAxiom ---- +\* Liveness InSync == + \A i, j \in Servers : []<>(cLogs[i] = cLogs[j]) + +InSyncLockStep == []<>(\A i, j \in Servers : cLogs[i] = cLogs[j]) -FairSpec == +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 + +FairSpecLockStep == /\ Spec - /\ WF_cLogs(Next) /\ \A s \in Servers: <>[][Copy(s)]_cLogs + \* 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 -THEOREM FairSpec => InSync +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 MachineClosedFairSpec == /\ Spec /\ WF_cLogs(Next) -Syncing == - \* At the level of ccfraft, the desired property is that commitIndex of - \* all (active) nodes repeatedly increases, i.e., - \* []<>(\A s \in Servers: commitIndex[s] < commitIndex'[s]) - \* . Note the \le and not \leq comparison! This is stronger (and a liveness - \* property) compared to - \* [][\A s \in Servers: commitIndex[s] < commitIndex'[s]]_commitIndex - []<><<\E s \in Servers: IsStrictPrefix(cLogs[s], cLogs'[s])>>_cLogs +THEOREM FairSpecLockStep => + (Syncing /\ SynchingLockStep /\ AllExtending /\ InSync /\ InSyncLockStep) -THEOREM MachineClosedFairSpec => Syncing +THEOREM FairSpec => + (Syncing /\ SynchingLockStep /\ AllExtending /\ InSync) -AllSyncing == - []<><<\A s \in Servers: IsStrictPrefix(cLogs[s], cLogs'[s])>>_cLogs +THEOREM MachineClosedFairSpec => + (Syncing /\ SynchingLockStep /\ AllExtending) -\* NOT A THEOREM: MachineClosedFairSpec => AllSyncing ---- \* abs models ccfraft's logs up to the commitIndex and the extension of the From e63ad0ae5f0e0d84ea01f9c1afe1011d3587909a Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 30 Oct 2024 09:58:19 -0700 Subject: [PATCH 18/25] Refactor name of fairness constraint. Signed-off-by: Markus Alexander Kuppe --- tla/consensus/MCabs.cfg | 2 +- tla/consensus/abs.tla | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg index 16195fe110f1..12b22c8288a7 100644 --- a/tla/consensus/MCabs.cfg +++ b/tla/consensus/MCabs.cfg @@ -1,4 +1,4 @@ -SPECIFICATION MachineClosedFairSpec +SPECIFICATION WeakFairnessSpec CONSTANTS NodeOne = n1 diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla index 282bece14ce9..7c81bc01c3a8 100644 --- a/tla/consensus/abs.tla +++ b/tla/consensus/abs.tla @@ -150,7 +150,7 @@ FairSpec == \* For all pairs of logs, there repeatedly exists a state where they are synced. /\ WF_cLogs(Next) /\ \A s,t \in Servers: []<><>_cLogs -MachineClosedFairSpec == +WeakFairnessSpec == /\ Spec /\ WF_cLogs(Next) @@ -160,7 +160,7 @@ THEOREM FairSpecLockStep => THEOREM FairSpec => (Syncing /\ SynchingLockStep /\ AllExtending /\ InSync) -THEOREM MachineClosedFairSpec => +THEOREM WeakFairnessSpec => (Syncing /\ SynchingLockStep /\ AllExtending) ---- From 626e0d533d9494b8d6782913f5974dbacc6c5b2b Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 30 Oct 2024 10:01:07 -0700 Subject: [PATCH 19/25] With a single node, the View reduces the state-space to a single state. More formally: LongestCommonPrefix({log}) = log Signed-off-by: Markus Alexander Kuppe --- tla/consensus/MCabs.tla | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tla/consensus/MCabs.tla b/tla/consensus/MCabs.tla index 95caa16530e3..319b4d52e281 100644 --- a/tla/consensus/MCabs.tla +++ b/tla/consensus/MCabs.tla @@ -11,6 +11,10 @@ MCServers == {NodeOne, NodeTwo, NodeThree} MCTerms == 2..4 MCStartTerm == Min(MCTerms) MaxExtend == 3 +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. From 3211a1ba4d2a4727dd812c5e29d5795707824e44 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 30 Oct 2024 10:04:00 -0700 Subject: [PATCH 20/25] There is no (explicit) upper bound on the length of logs; explain what makes the state space finite. Signed-off-by: Markus Alexander Kuppe --- tla/consensus/MCabs.tla | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/tla/consensus/MCabs.tla b/tla/consensus/MCabs.tla index 319b4d52e281..1c8ff12a5005 100644 --- a/tla/consensus/MCabs.tla +++ b/tla/consensus/MCabs.tla @@ -23,6 +23,13 @@ MCTypeOK == MCSeq(S) == BoundedSeq(S, MaxExtend) +----- + +\* 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 From b5a538d1f0a29659a9013fe6a5d3d196a5a0a168 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Thu, 31 Oct 2024 11:28:55 -0700 Subject: [PATCH 21/25] Add a simpler variant of the MonotonicReduction that just drops the common prefix but leaves the Terms untouched. Signed-off-by: Markus Alexander Kuppe --- tla/consensus/MCabs.tla | 22 ++++++++++++++++------ 1 file changed, 16 insertions(+), 6 deletions(-) diff --git a/tla/consensus/MCabs.tla b/tla/consensus/MCabs.tla index 1c8ff12a5005..614ee6c597b6 100644 --- a/tla/consensus/MCabs.tla +++ b/tla/consensus/MCabs.tla @@ -37,11 +37,20 @@ MaxDivergence == \A i, j \in Servers : Abs(Len(cLogs[i]) - Len(cLogs[j])) <= 2 -MonotonicReduction == - LET TailFrom(seq, idx) == SubSeq(seq, idx + 1, Len(seq)) - \* Find the longest common prefix of all logs and drop it from all logs. - \* We realign the terms in the remaining suffixes to start at StartTerm. - commonPrefixBound == Len(LongestCommonPrefix(Range(cLogs))) +----- + +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 to start at StartTerm. + LET commonPrefixBound == Len(LongestCommonPrefix(Range(cLogs))) minTerm == \* 3) The minimum term out of all minima. Min({ @@ -53,6 +62,7 @@ MonotonicReduction == \cup {0}) : s \in Servers}) IN [ s \in Servers |-> [ i \in 1..Len(cLogs[s]) - commonPrefixBound |-> - cLogs[s][i + commonPrefixBound] - minTerm ] ] +MonotonicReduction == + MonotonicReductionLongestCommonPrefixAndTerms ==== \ No newline at end of file From 50b6015f82ac4f0b9db447a7a729c4eb420a5362 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Thu, 31 Oct 2024 15:12:44 -0700 Subject: [PATCH 22/25] 0 is a bogus default that causes both MonotonicReduction* definitions to be equivalent (...AndTerms always substracts 0). Signed-off-by: Markus Alexander Kuppe --- tla/consensus/MCabs.tla | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/tla/consensus/MCabs.tla b/tla/consensus/MCabs.tla index 614ee6c597b6..e394d9bf8829 100644 --- a/tla/consensus/MCabs.tla +++ b/tla/consensus/MCabs.tla @@ -11,6 +11,8 @@ 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. @@ -49,7 +51,7 @@ MonotonicReductionLongestCommonPrefix == MonotonicReductionLongestCommonPrefixAndTerms == \* Find the longest common prefix of all logs and drop it from all logs. - \* We also realign the terms in the remaining suffixes to start at StartTerm. + \* We also realign the terms in the remaining suffixes. LET commonPrefixBound == Len(LongestCommonPrefix(Range(cLogs))) minTerm == \* 3) The minimum term out of all minima. @@ -58,10 +60,15 @@ MonotonicReductionLongestCommonPrefixAndTerms == Min( \* 1) All terms in the suffix of a log. Range(TailFrom(cLogs[s], commonPrefixBound)) - \* \cup {0} to handle the case where a log is empty. - \cup {0}) : s \in Servers}) + \* \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 From 1c5a7cea5d7fab0eb6604b1b9d8e55bb4e728801 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 30 Oct 2024 10:26:15 -0700 Subject: [PATCH 23/25] Add a leads-to property EmptyLeadsToNonEmpty to the properties we check under the MonotonicReduction view. Signed-off-by: Markus Alexander Kuppe --- tla/consensus/MCabs.cfg | 1 + tla/consensus/abs.tla | 10 +++++++--- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg index 12b22c8288a7..25bc3aa63592 100644 --- a/tla/consensus/MCabs.cfg +++ b/tla/consensus/MCabs.cfg @@ -22,6 +22,7 @@ PROPERTIES SynchingLockStep AllExtending \* AllExtendingLockStep + EmptyLeadsToNonEmpty AppendOnlyProp \* EquivExtendProp \* EquivCopyMaxAndExtendProp diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla index 7c81bc01c3a8..a665073d3c64 100644 --- a/tla/consensus/abs.tla +++ b/tla/consensus/abs.tla @@ -140,6 +140,10 @@ AllExtendingLockStep == 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. @@ -155,13 +159,13 @@ WeakFairnessSpec == /\ WF_cLogs(Next) THEOREM FairSpecLockStep => - (Syncing /\ SynchingLockStep /\ AllExtending /\ InSync /\ InSyncLockStep) + (Syncing /\ SynchingLockStep /\ AllExtending /\ InSync /\ InSyncLockStep /\ EmptyLeadsToNonEmpty) THEOREM FairSpec => - (Syncing /\ SynchingLockStep /\ AllExtending /\ InSync) + (Syncing /\ SynchingLockStep /\ AllExtending /\ InSync /\ EmptyLeadsToNonEmpty) THEOREM WeakFairnessSpec => - (Syncing /\ SynchingLockStep /\ AllExtending) + (Syncing /\ SynchingLockStep /\ AllExtending /\ EmptyLeadsToNonEmpty) ---- From c15091f58cb190ba34f51ab921b3f4fa3b4962f4 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Thu, 31 Oct 2024 11:09:55 -0700 Subject: [PATCH 24/25] Properties that cause spurious counterexamples here to illustrate the limitations of the MonotonicReduction view. ```tla Starting... (2024-10-31 11:22:03) Implied-temporal checking--satisfiability problem has 7 branches. Computing initial states... Computed 2 initial states... Computed 4 initial states... Computed 8 initial states... Computed 16 initial states... Finished computing initial states: 27 states generated, with 7 of them distinct at 2024-10-31 11:22:03. Progress(3) at 2024-10-31 11:22:05: 26,895 states generated, 127 distinct states found, 0 states left on queue. Checking 7 branches of temporal properties for the complete state space with 889 total distinct states at (2024-10-31 11:22:05) Error: Temporal properties were violated. Error: The following behavior constitutes a counter-example: State 1: cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>>) State 2: cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<3, 4>>) State 3: cLogs = (n1 :> <<>> @@ n2 :> <<3, 4>> @@ n3 :> <<3, 4>>) State 4: cLogs = (n1 :> <<3, 4>> @@ n2 :> <<3, 4>> @@ n3 :> <<3, 4>>) Back to state 2: Finished checking temporal properties in 00s at 2024-10-31 11:22:05 26895 states generated, 127 distinct states found, 0 states left on queue. The depth of the complete state graph search is 3. Finished in 02s at (2024-10-31 11:22:05) ``` Signed-off-by: Markus Alexander Kuppe --- tla/consensus/MCabs.cfg | 4 ++++ tla/consensus/MCabs.tla | 9 +++++++++ 2 files changed, 13 insertions(+) diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg index 25bc3aa63592..642cabc109dc 100644 --- a/tla/consensus/MCabs.cfg +++ b/tla/consensus/MCabs.cfg @@ -27,6 +27,10 @@ PROPERTIES \* EquivExtendProp \* EquivCopyMaxAndExtendProp + \* Properties that cause spurious counterexamples here to + \* illustrate the limitations of the MonotonicReduction view. + \* SpuriousPropA + VIEW MonotonicReduction diff --git a/tla/consensus/MCabs.tla b/tla/consensus/MCabs.tla index e394d9bf8829..43f60e1572d1 100644 --- a/tla/consensus/MCabs.tla +++ b/tla/consensus/MCabs.tla @@ -2,6 +2,15 @@ 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] # <<>>) + Symmetry == Permutations(Servers) From 976b6d268e454ce092720e0d03d5597acbb79763 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 30 Oct 2024 10:06:42 -0700 Subject: [PATCH 25/25] Add (temporal) formulas that are expected to result in counterexamples as sanity checks. Signed-off-by: Markus Alexander Kuppe --- tla/consensus/MCabs.cfg | 9 +++++++++ tla/consensus/MCabs.tla | 41 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 50 insertions(+) diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg index 642cabc109dc..ee9a7c1697df 100644 --- a/tla/consensus/MCabs.cfg +++ b/tla/consensus/MCabs.cfg @@ -31,6 +31,15 @@ PROPERTIES \* illustrate the limitations of the MonotonicReduction view. \* SpuriousPropA + \* NotAPropA + \* NotAPropB + \* NotAPropC + \* NotAPropD + \* NotAPropE + \* NotAPropF + \* NotAPropG + \* NotAPropH + VIEW MonotonicReduction diff --git a/tla/consensus/MCabs.tla b/tla/consensus/MCabs.tla index 43f60e1572d1..371e0c0e7704 100644 --- a/tla/consensus/MCabs.tla +++ b/tla/consensus/MCabs.tla @@ -11,6 +11,47 @@ SpuriousPropA == \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)