diff --git a/storage_broker/spec/replicated/.DS_Store b/storage_broker/spec/replicated/.DS_Store new file mode 100644 index 0000000000..5008ddfcf5 Binary files /dev/null and b/storage_broker/spec/replicated/.DS_Store differ diff --git a/storage_broker/spec/replicated/replicated.tla b/storage_broker/spec/replicated/replicated.tla new file mode 100644 index 0000000000..14910364fe --- /dev/null +++ b/storage_broker/spec/replicated/replicated.tla @@ -0,0 +1,117 @@ +---- MODULE replicated ---- + +EXTENDS Integers + +VARIABLES broker_state, safekeeper_state, pageserver_state + + +CONSTANT + brokers, + safekeepers, + pageservers, + azs, + az_mapping + +CONSTANT + NULL + +CONSTANT + max_commit_lsn + +StateConstraint == + /\ \A s \in safekeepers: + /\ safekeeper_state[s].commit_lsn <= max_commit_lsn + /\ \A b \in brokers: + /\ \A s \in DOMAIN broker_state[b].sk: + /\ broker_state[b].sk[s].commit_lsn <= max_commit_lsn + + +InitSafekeeper == [pruned_lsn |-> 0, commit_lsn |-> 0] +InitBroker == [sk |-> [s \in safekeepers |-> [commit_lsn |-> 0]]] +InitPageserver == [last_record_lsn |-> 0, preferred_sk |-> NULL, sk |-> [s \in safekeepers |-> [commit_lsn |-> 0]]] + +Init == + /\ broker_state = [b \in brokers |-> InitBroker] + /\ safekeeper_state = [s \in safekeepers |-> InitSafekeeper] + /\ pageserver_state = [p \in pageservers |-> InitPageserver] + + +SkCommit(s1, s2) == + /\ s1 # s2 + /\ safekeeper_state[s1].commit_lsn = safekeeper_state[s2].commit_lsn + /\ LET + new_commit_lsn == safekeeper_state[s1].commit_lsn + 1 + IN + safekeeper_state' = [safekeeper_state EXCEPT + ![s1].commit_lsn = new_commit_lsn, + ![s2].commit_lsn = new_commit_lsn] + /\ UNCHANGED <> + +SkPeerRecovery(s1,s2) == + /\ safekeeper_state[s1].commit_lsn < safekeeper_state[s2].commit_lsn + /\ safekeeper_state' = [safekeeper_state EXCEPT![s1].commit_lsn = safekeeper_state[s2].commit_lsn] + /\ UNCHANGED <> + +SkPushToBroker(s,b) == + /\ broker_state' = IF broker_state[b].sk[s].commit_lsn < safekeeper_state[s].commit_lsn + THEN + LET + bsk == broker_state[b].sk + updbsk == [bsk EXCEPT ![s].commit_lsn = safekeeper_state[s].commit_lsn] + IN + [broker_state EXCEPT ![b].sk = updbsk] + ELSE broker_state + /\ UNCHANGED <> + +PsRecvBroker(b,p,s) == + /\ LET + bsk == broker_state[b].sk[s] + psk == pageserver_state[p].sk[s] + updpsk == [psk EXCEPT !["commit_lsn"] = bsk.commit_lsn] + IN + pageserver_state' = IF bsk.commit_lsn > psk.commit_lsn + THEN [pageserver_state EXCEPT ![p].sk[s] = updpsk] + ELSE pageserver_state + /\ UNCHANGED <> + + +SksWithNewerWal(p) == + LET + ps == pageserver_state[p] + IN + {s \in DOMAIN ps.sk: ps.sk[s].commit_lsn > ps.last_record_lsn} + +PsChooseSk(p) == + /\ SksWithNewerWal(p) # {} + /\ pageserver_state' = [pageserver_state EXCEPT![p].preferred_sk = CHOOSE s \in SksWithNewerWal(p): TRUE] + /\ UNCHANGED <> + + +Next == + + \/ \E s1 \in safekeepers: \E s2 \in safekeepers: + \/ SkCommit(s1, s2) + \/ SkPeerRecovery(s1, s2) + \/ \E s \in safekeepers: \E b \in brokers: SkPushToBroker(s, b) + \/ \E s \in safekeepers: \E b \in brokers: \E p \in pageservers: PsRecvBroker(b,p,s) + \/ \E p \in pageservers: PsChooseSk(p) + + +Spec == Init /\ [][Next]_<< broker_state, safekeeper_state, pageserver_state >> + + +\* invariants + +EventuallyLaggingSkIsNotPreferredSk == <>( + LET + sks == safekeeper_state + lagging_sks == { s \in safekeepers: \A s2 \in safekeepers: sks[s].commit_lsn <= sks[s2].commit_lsn } + preferred_sks == {pageserver_state[p].preferred_sk: p \in pageservers} + IN + preferred_sks \cap lagging_sks = {} + + ) + + + +==== \ No newline at end of file diff --git a/storage_broker/spec/replicated/replicated.toolbox/.project b/storage_broker/spec/replicated/replicated.toolbox/.project new file mode 100644 index 0000000000..6cd6e13bd0 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/.project @@ -0,0 +1,24 @@ + + + replicated + + + + + + toolbox.builder.TLAParserBuilder + + + + + + toolbox.natures.TLANature + + + + replicated.tla + 1 + PARENT-1-PROJECT_LOC/replicated.tla + + + diff --git a/storage_broker/spec/replicated/replicated.toolbox/.settings/org.lamport.tla.toolbox.prefs b/storage_broker/spec/replicated/replicated.toolbox/.settings/org.lamport.tla.toolbox.prefs new file mode 100644 index 0000000000..968871daf6 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/.settings/org.lamport.tla.toolbox.prefs @@ -0,0 +1,2 @@ +ProjectRootFile=PARENT-1-PROJECT_LOC/replicated.tla +eclipse.preferences.version=1 diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1/25-01-19-16-40-15/MC-0.st b/storage_broker/spec/replicated/replicated.toolbox/Model_1/25-01-19-16-40-15/MC-0.st new file mode 100644 index 0000000000..ea733796c7 Binary files /dev/null and b/storage_broker/spec/replicated/replicated.toolbox/Model_1/25-01-19-16-40-15/MC-0.st differ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1/25-01-19-16-40-15/MC-1.st b/storage_broker/spec/replicated/replicated.toolbox/Model_1/25-01-19-16-40-15/MC-1.st new file mode 100644 index 0000000000..0b468bb253 Binary files /dev/null and b/storage_broker/spec/replicated/replicated.toolbox/Model_1/25-01-19-16-40-15/MC-1.st differ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1/25-01-19-16-40-15/MC-2.st b/storage_broker/spec/replicated/replicated.toolbox/Model_1/25-01-19-16-40-15/MC-2.st new file mode 100644 index 0000000000..5a85056577 Binary files /dev/null and b/storage_broker/spec/replicated/replicated.toolbox/Model_1/25-01-19-16-40-15/MC-2.st differ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1/25-01-19-16-40-15/MC-3.st b/storage_broker/spec/replicated/replicated.toolbox/Model_1/25-01-19-16-40-15/MC-3.st new file mode 100644 index 0000000000..2eece7fbb5 Binary files /dev/null and b/storage_broker/spec/replicated/replicated.toolbox/Model_1/25-01-19-16-40-15/MC-3.st differ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1/25-01-19-16-40-15/MC.st b/storage_broker/spec/replicated/replicated.toolbox/Model_1/25-01-19-16-40-15/MC.st new file mode 100644 index 0000000000..e69de29bb2 diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1/25-01-19-16-40-15/MC_0.fp b/storage_broker/spec/replicated/replicated.toolbox/Model_1/25-01-19-16-40-15/MC_0.fp new file mode 100644 index 0000000000..e69de29bb2 diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1/25-01-19-16-40-15/MC_1.fp b/storage_broker/spec/replicated/replicated.toolbox/Model_1/25-01-19-16-40-15/MC_1.fp new file mode 100644 index 0000000000..e69de29bb2 diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1/25-01-19-16-40-15/nodes_0 b/storage_broker/spec/replicated/replicated.toolbox/Model_1/25-01-19-16-40-15/nodes_0 new file mode 100644 index 0000000000..e69de29bb2 diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1/25-01-19-16-40-15/ptrs_0 b/storage_broker/spec/replicated/replicated.toolbox/Model_1/25-01-19-16-40-15/ptrs_0 new file mode 100644 index 0000000000..e69de29bb2 diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1/MC.cfg b/storage_broker/spec/replicated/replicated.toolbox/Model_1/MC.cfg new file mode 100644 index 0000000000..1dcac21267 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1/MC.cfg @@ -0,0 +1,51 @@ +\* MV CONSTANT declarations +CONSTANTS +b1 = b1 +b2 = b2 +b3 = b3 +\* MV CONSTANT declarations +CONSTANTS +s1 = s1 +s2 = s2 +s3 = s3 +\* MV CONSTANT declarations +CONSTANTS +p1 = p1 +p2 = p2 +\* MV CONSTANT declarations +CONSTANTS +az1 = az1 +az2 = az2 +az3 = az3 +\* MV CONSTANT definitions +CONSTANT +brokers <- const_17373012151752000 +\* CONSTANT declarations +CONSTANT NULL = NULL +\* MV CONSTANT definitions +CONSTANT +safekeepers <- const_17373012151763000 +\* MV CONSTANT definitions +CONSTANT +pageservers <- const_17373012151764000 +\* MV CONSTANT definitions +CONSTANT +azs <- const_17373012151765000 +\* SYMMETRY definition +SYMMETRY symm_17373012151766000 +\* CONSTANT definitions +CONSTANT +max_commit_lsn <- const_17373012151767000 +\* CONSTANT definitions +CONSTANT +az_mapping <- const_17373012151768000 +\* CONSTRAINT definition +CONSTRAINT +constr_17373012151769000 +\* SPECIFICATION definition +SPECIFICATION +Spec +\* PROPERTY definition +PROPERTY +EventuallyLaggingSkIsNotPreferredSk +\* Generated on Sun Jan 19 16:40:15 CET 2025 \ No newline at end of file diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1/MC.out b/storage_broker/spec/replicated/replicated.toolbox/Model_1/MC.out new file mode 100644 index 0000000000..ab92cbb3d7 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1/MC.out @@ -0,0 +1,53 @@ +@!@!@STARTMSG 2262:0 @!@!@ +TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802) +@!@!@ENDMSG 2262 @!@!@ +@!@!@STARTMSG 2187:0 @!@!@ +Running breadth-first search Model-Checking with fp 20 and seed 6372772458573668883 with 4 workers on 8 cores with 2428MB heap and 5460MB offheap memory [pid: 9898] (Mac OS X 10.16 x86_64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue). +@!@!@ENDMSG 2187 @!@!@ +@!@!@STARTMSG 2220:0 @!@!@ +Starting SANY... +@!@!@ENDMSG 2220 @!@!@ +Parsing file /Users/cs/src/neon/storage_broker/spec/replicated/replicated.toolbox/Model_1/MC.tla +Parsing file /Users/cs/src/neon/storage_broker/spec/replicated/replicated.toolbox/Model_1/replicated.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/TLC.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Integers.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Naturals.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Sequences.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/FiniteSets.tla +Semantic processing of module Naturals +Semantic processing of module Integers +Semantic processing of module replicated +Semantic processing of module Sequences +Semantic processing of module FiniteSets +Semantic processing of module TLC +Semantic processing of module MC +@!@!@STARTMSG 2219:0 @!@!@ +SANY finished. +@!@!@ENDMSG 2219 @!@!@ +@!@!@STARTMSG 2185:0 @!@!@ +Starting... (2025-01-19 16:40:16) +@!@!@ENDMSG 2185 @!@!@ +@!@!@STARTMSG 2279:3 @!@!@ +Declaring symmetry during liveness checking is dangerous. It might cause TLC to miss violations of the stated liveness properties. Please check liveness without symmetry defined. +@!@!@ENDMSG 2279 @!@!@ +@!@!@STARTMSG 2284:3 @!@!@ +Declaring state or action constraints during liveness checking is dangerous: Please read section 14.3.5 on page 247 of Specifying Systems (https://lamport.azurewebsites.net/tla/book.html) and optionally the discussion at https://discuss.tlapl.us/msg00994.html for more details. +@!@!@ENDMSG 2284 @!@!@ +@!@!@STARTMSG 2212:0 @!@!@ +Implied-temporal checking--satisfiability problem has 1 branches. +@!@!@ENDMSG 2212 @!@!@ +@!@!@STARTMSG 2189:0 @!@!@ +Computing initial states... +@!@!@ENDMSG 2189 @!@!@ +@!@!@STARTMSG 2190:0 @!@!@ +Finished computing initial states: 1 distinct state generated at 2025-01-19 16:40:18. +@!@!@ENDMSG 2190 @!@!@ +@!@!@STARTMSG 2192:0 @!@!@ +Checking temporal properties for the current state space with 1217 total distinct states at (2025-01-19 16:40:21) +@!@!@ENDMSG 2192 @!@!@ +@!@!@STARTMSG 2267:0 @!@!@ +Finished checking temporal properties in 00s at 2025-01-19 16:40:21 +@!@!@ENDMSG 2267 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(11) at 2025-01-19 16:40:21: 39.816 states generated (39.816 s/min), 3.288 distinct states found (3.288 ds/min), 2.067 states left on queue. +@!@!@ENDMSG 2200 @!@!@ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1/MC.tla b/storage_broker/spec/replicated/replicated.toolbox/Model_1/MC.tla new file mode 100644 index 0000000000..316c6f4df7 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1/MC.tla @@ -0,0 +1,65 @@ +---- MODULE MC ---- +EXTENDS replicated, TLC + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +b1, b2, b3 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +s1, s2, s3 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +p1, p2 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +az1, az2, az3 +---- + +\* MV CONSTANT definitions brokers +const_17373012151752000 == +{b1, b2, b3} +---- + +\* MV CONSTANT definitions safekeepers +const_17373012151763000 == +{s1, s2, s3} +---- + +\* MV CONSTANT definitions pageservers +const_17373012151764000 == +{p1, p2} +---- + +\* MV CONSTANT definitions azs +const_17373012151765000 == +{az1, az2, az3} +---- + +\* SYMMETRY definition +symm_17373012151766000 == +Permutations(const_17373012151752000) \union Permutations(const_17373012151763000) \union Permutations(const_17373012151764000) \union Permutations(const_17373012151765000) +---- + +\* CONSTANT definitions @modelParameterConstants:4max_commit_lsn +const_17373012151767000 == +2 +---- + +\* CONSTANT definitions @modelParameterConstants:5az_mapping +const_17373012151768000 == +[ az1 |-> {b1,s1,p1} , az2 |-> {b2,s2,p2} , az3 |-> {b3,s3}] +---- + +\* CONSTRAINT definition @modelParameterContraint:0 +constr_17373012151769000 == +StateConstraint +---- +============================================================================= +\* Modification History +\* Created Sun Jan 19 16:40:15 CET 2025 by cs diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1/MC_TE.out b/storage_broker/spec/replicated/replicated.toolbox/Model_1/MC_TE.out new file mode 100644 index 0000000000..ab92cbb3d7 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1/MC_TE.out @@ -0,0 +1,53 @@ +@!@!@STARTMSG 2262:0 @!@!@ +TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802) +@!@!@ENDMSG 2262 @!@!@ +@!@!@STARTMSG 2187:0 @!@!@ +Running breadth-first search Model-Checking with fp 20 and seed 6372772458573668883 with 4 workers on 8 cores with 2428MB heap and 5460MB offheap memory [pid: 9898] (Mac OS X 10.16 x86_64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue). +@!@!@ENDMSG 2187 @!@!@ +@!@!@STARTMSG 2220:0 @!@!@ +Starting SANY... +@!@!@ENDMSG 2220 @!@!@ +Parsing file /Users/cs/src/neon/storage_broker/spec/replicated/replicated.toolbox/Model_1/MC.tla +Parsing file /Users/cs/src/neon/storage_broker/spec/replicated/replicated.toolbox/Model_1/replicated.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/TLC.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Integers.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Naturals.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Sequences.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/FiniteSets.tla +Semantic processing of module Naturals +Semantic processing of module Integers +Semantic processing of module replicated +Semantic processing of module Sequences +Semantic processing of module FiniteSets +Semantic processing of module TLC +Semantic processing of module MC +@!@!@STARTMSG 2219:0 @!@!@ +SANY finished. +@!@!@ENDMSG 2219 @!@!@ +@!@!@STARTMSG 2185:0 @!@!@ +Starting... (2025-01-19 16:40:16) +@!@!@ENDMSG 2185 @!@!@ +@!@!@STARTMSG 2279:3 @!@!@ +Declaring symmetry during liveness checking is dangerous. It might cause TLC to miss violations of the stated liveness properties. Please check liveness without symmetry defined. +@!@!@ENDMSG 2279 @!@!@ +@!@!@STARTMSG 2284:3 @!@!@ +Declaring state or action constraints during liveness checking is dangerous: Please read section 14.3.5 on page 247 of Specifying Systems (https://lamport.azurewebsites.net/tla/book.html) and optionally the discussion at https://discuss.tlapl.us/msg00994.html for more details. +@!@!@ENDMSG 2284 @!@!@ +@!@!@STARTMSG 2212:0 @!@!@ +Implied-temporal checking--satisfiability problem has 1 branches. +@!@!@ENDMSG 2212 @!@!@ +@!@!@STARTMSG 2189:0 @!@!@ +Computing initial states... +@!@!@ENDMSG 2189 @!@!@ +@!@!@STARTMSG 2190:0 @!@!@ +Finished computing initial states: 1 distinct state generated at 2025-01-19 16:40:18. +@!@!@ENDMSG 2190 @!@!@ +@!@!@STARTMSG 2192:0 @!@!@ +Checking temporal properties for the current state space with 1217 total distinct states at (2025-01-19 16:40:21) +@!@!@ENDMSG 2192 @!@!@ +@!@!@STARTMSG 2267:0 @!@!@ +Finished checking temporal properties in 00s at 2025-01-19 16:40:21 +@!@!@ENDMSG 2267 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(11) at 2025-01-19 16:40:21: 39.816 states generated (39.816 s/min), 3.288 distinct states found (3.288 ds/min), 2.067 states left on queue. +@!@!@ENDMSG 2200 @!@!@ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1/replicated.tla b/storage_broker/spec/replicated/replicated.toolbox/Model_1/replicated.tla new file mode 100644 index 0000000000..14910364fe --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1/replicated.tla @@ -0,0 +1,117 @@ +---- MODULE replicated ---- + +EXTENDS Integers + +VARIABLES broker_state, safekeeper_state, pageserver_state + + +CONSTANT + brokers, + safekeepers, + pageservers, + azs, + az_mapping + +CONSTANT + NULL + +CONSTANT + max_commit_lsn + +StateConstraint == + /\ \A s \in safekeepers: + /\ safekeeper_state[s].commit_lsn <= max_commit_lsn + /\ \A b \in brokers: + /\ \A s \in DOMAIN broker_state[b].sk: + /\ broker_state[b].sk[s].commit_lsn <= max_commit_lsn + + +InitSafekeeper == [pruned_lsn |-> 0, commit_lsn |-> 0] +InitBroker == [sk |-> [s \in safekeepers |-> [commit_lsn |-> 0]]] +InitPageserver == [last_record_lsn |-> 0, preferred_sk |-> NULL, sk |-> [s \in safekeepers |-> [commit_lsn |-> 0]]] + +Init == + /\ broker_state = [b \in brokers |-> InitBroker] + /\ safekeeper_state = [s \in safekeepers |-> InitSafekeeper] + /\ pageserver_state = [p \in pageservers |-> InitPageserver] + + +SkCommit(s1, s2) == + /\ s1 # s2 + /\ safekeeper_state[s1].commit_lsn = safekeeper_state[s2].commit_lsn + /\ LET + new_commit_lsn == safekeeper_state[s1].commit_lsn + 1 + IN + safekeeper_state' = [safekeeper_state EXCEPT + ![s1].commit_lsn = new_commit_lsn, + ![s2].commit_lsn = new_commit_lsn] + /\ UNCHANGED <> + +SkPeerRecovery(s1,s2) == + /\ safekeeper_state[s1].commit_lsn < safekeeper_state[s2].commit_lsn + /\ safekeeper_state' = [safekeeper_state EXCEPT![s1].commit_lsn = safekeeper_state[s2].commit_lsn] + /\ UNCHANGED <> + +SkPushToBroker(s,b) == + /\ broker_state' = IF broker_state[b].sk[s].commit_lsn < safekeeper_state[s].commit_lsn + THEN + LET + bsk == broker_state[b].sk + updbsk == [bsk EXCEPT ![s].commit_lsn = safekeeper_state[s].commit_lsn] + IN + [broker_state EXCEPT ![b].sk = updbsk] + ELSE broker_state + /\ UNCHANGED <> + +PsRecvBroker(b,p,s) == + /\ LET + bsk == broker_state[b].sk[s] + psk == pageserver_state[p].sk[s] + updpsk == [psk EXCEPT !["commit_lsn"] = bsk.commit_lsn] + IN + pageserver_state' = IF bsk.commit_lsn > psk.commit_lsn + THEN [pageserver_state EXCEPT ![p].sk[s] = updpsk] + ELSE pageserver_state + /\ UNCHANGED <> + + +SksWithNewerWal(p) == + LET + ps == pageserver_state[p] + IN + {s \in DOMAIN ps.sk: ps.sk[s].commit_lsn > ps.last_record_lsn} + +PsChooseSk(p) == + /\ SksWithNewerWal(p) # {} + /\ pageserver_state' = [pageserver_state EXCEPT![p].preferred_sk = CHOOSE s \in SksWithNewerWal(p): TRUE] + /\ UNCHANGED <> + + +Next == + + \/ \E s1 \in safekeepers: \E s2 \in safekeepers: + \/ SkCommit(s1, s2) + \/ SkPeerRecovery(s1, s2) + \/ \E s \in safekeepers: \E b \in brokers: SkPushToBroker(s, b) + \/ \E s \in safekeepers: \E b \in brokers: \E p \in pageservers: PsRecvBroker(b,p,s) + \/ \E p \in pageservers: PsChooseSk(p) + + +Spec == Init /\ [][Next]_<< broker_state, safekeeper_state, pageserver_state >> + + +\* invariants + +EventuallyLaggingSkIsNotPreferredSk == <>( + LET + sks == safekeeper_state + lagging_sks == { s \in safekeepers: \A s2 \in safekeepers: sks[s].commit_lsn <= sks[s2].commit_lsn } + preferred_sks == {pageserver_state[p].preferred_sk: p \in pageservers} + IN + preferred_sks \cap lagging_sks = {} + + ) + + + +==== \ No newline at end of file diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737296416956/MC.cfg b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737296416956/MC.cfg new file mode 100644 index 0000000000..315dcb696c --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737296416956/MC.cfg @@ -0,0 +1,37 @@ +\* MV CONSTANT declarations +CONSTANTS +b1 = b1 +b2 = b2 +b3 = b3 +\* MV CONSTANT declarations +CONSTANTS +s1 = s1 +s2 = s2 +s3 = s3 +\* MV CONSTANT declarations +CONSTANTS +p1 = p1 +p2 = p2 +\* MV CONSTANT definitions +CONSTANT +brokers <- const_1737296402193120000 +\* CONSTANT declarations +CONSTANT NULL = NULL +\* MV CONSTANT definitions +CONSTANT +safekeepers <- const_1737296402194121000 +\* MV CONSTANT definitions +CONSTANT +pageservers <- const_1737296402194122000 +\* SYMMETRY definition +SYMMETRY symm_1737296402194123000 +\* CONSTANT definitions +CONSTANT +max_commit_lsn <- const_1737296402194124000 +\* CONSTRAINT definition +CONSTRAINT +constr_1737296402194125000 +\* SPECIFICATION definition +SPECIFICATION +Spec +\* Generated on Sun Jan 19 15:20:02 CET 2025 \ No newline at end of file diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737296416956/MC.out b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737296416956/MC.out new file mode 100644 index 0000000000..696943b056 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737296416956/MC.out @@ -0,0 +1,38 @@ +@!@!@STARTMSG 2262:0 @!@!@ +TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802) +@!@!@ENDMSG 2262 @!@!@ +@!@!@STARTMSG 2187:0 @!@!@ +Running breadth-first search Model-Checking with fp 60 and seed 6751784514943401101 with 4 workers on 8 cores with 2428MB heap and 5460MB offheap memory [pid: 5476] (Mac OS X 10.16 x86_64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue). +@!@!@ENDMSG 2187 @!@!@ +@!@!@STARTMSG 2220:0 @!@!@ +Starting SANY... +@!@!@ENDMSG 2220 @!@!@ +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/MC.tla +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/fullmesh.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/TLC.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Integers.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Naturals.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Sequences.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/FiniteSets.tla +Semantic processing of module Naturals +Semantic processing of module Integers +Semantic processing of module fullmesh +Semantic processing of module Sequences +Semantic processing of module FiniteSets +Semantic processing of module TLC +Semantic processing of module MC +@!@!@STARTMSG 2219:0 @!@!@ +SANY finished. +@!@!@ENDMSG 2219 @!@!@ +@!@!@STARTMSG 2185:0 @!@!@ +Starting... (2025-01-19 15:20:03) +@!@!@ENDMSG 2185 @!@!@ +@!@!@STARTMSG 2189:0 @!@!@ +Computing initial states... +@!@!@ENDMSG 2189 @!@!@ +@!@!@STARTMSG 2190:0 @!@!@ +Finished computing initial states: 1 distinct state generated at 2025-01-19 15:20:04. +@!@!@ENDMSG 2190 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(12) at 2025-01-19 15:20:07: 163.015 states generated (163.015 s/min), 12.588 distinct states found (12.588 ds/min), 7.372 states left on queue. +@!@!@ENDMSG 2200 @!@!@ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737296416956/MC.tla b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737296416956/MC.tla new file mode 100644 index 0000000000..d30390320b --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737296416956/MC.tla @@ -0,0 +1,50 @@ +---- MODULE MC ---- +EXTENDS fullmesh, TLC + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +b1, b2, b3 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +s1, s2, s3 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +p1, p2 +---- + +\* MV CONSTANT definitions brokers +const_1737296402193120000 == +{b1, b2, b3} +---- + +\* MV CONSTANT definitions safekeepers +const_1737296402194121000 == +{s1, s2, s3} +---- + +\* MV CONSTANT definitions pageservers +const_1737296402194122000 == +{p1, p2} +---- + +\* SYMMETRY definition +symm_1737296402194123000 == +Permutations(const_1737296402193120000) \union Permutations(const_1737296402194121000) \union Permutations(const_1737296402194122000) +---- + +\* CONSTANT definitions @modelParameterConstants:4max_commit_lsn +const_1737296402194124000 == +2 +---- + +\* CONSTRAINT definition @modelParameterContraint:0 +constr_1737296402194125000 == +StateConstraint +---- +============================================================================= +\* Modification History +\* Created Sun Jan 19 15:20:02 CET 2025 by cs diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737296416956/MC_TE.out b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737296416956/MC_TE.out new file mode 100644 index 0000000000..696943b056 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737296416956/MC_TE.out @@ -0,0 +1,38 @@ +@!@!@STARTMSG 2262:0 @!@!@ +TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802) +@!@!@ENDMSG 2262 @!@!@ +@!@!@STARTMSG 2187:0 @!@!@ +Running breadth-first search Model-Checking with fp 60 and seed 6751784514943401101 with 4 workers on 8 cores with 2428MB heap and 5460MB offheap memory [pid: 5476] (Mac OS X 10.16 x86_64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue). +@!@!@ENDMSG 2187 @!@!@ +@!@!@STARTMSG 2220:0 @!@!@ +Starting SANY... +@!@!@ENDMSG 2220 @!@!@ +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/MC.tla +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/fullmesh.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/TLC.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Integers.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Naturals.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Sequences.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/FiniteSets.tla +Semantic processing of module Naturals +Semantic processing of module Integers +Semantic processing of module fullmesh +Semantic processing of module Sequences +Semantic processing of module FiniteSets +Semantic processing of module TLC +Semantic processing of module MC +@!@!@STARTMSG 2219:0 @!@!@ +SANY finished. +@!@!@ENDMSG 2219 @!@!@ +@!@!@STARTMSG 2185:0 @!@!@ +Starting... (2025-01-19 15:20:03) +@!@!@ENDMSG 2185 @!@!@ +@!@!@STARTMSG 2189:0 @!@!@ +Computing initial states... +@!@!@ENDMSG 2189 @!@!@ +@!@!@STARTMSG 2190:0 @!@!@ +Finished computing initial states: 1 distinct state generated at 2025-01-19 15:20:04. +@!@!@ENDMSG 2190 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(12) at 2025-01-19 15:20:07: 163.015 states generated (163.015 s/min), 12.588 distinct states found (12.588 ds/min), 7.372 states left on queue. +@!@!@ENDMSG 2200 @!@!@ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737296416956/fullmesh.tla b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737296416956/fullmesh.tla new file mode 100644 index 0000000000..a70d3aeb85 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737296416956/fullmesh.tla @@ -0,0 +1,85 @@ +---- MODULE fullmesh ---- + +EXTENDS Integers + +VARIABLES broker_state, safekeeper_state, pageserver_state + +vars == << broker_state, safekeeper_state, pageserver_state >> + +CONSTANT + brokers, + safekeepers, + pageservers + +CONSTANT + NULL + +CONSTANT + max_commit_lsn + +StateConstraint == + /\ \A s \in safekeepers: + /\ safekeeper_state[s].commit_lsn <= max_commit_lsn + /\ \A b \in brokers: + /\ \A s \in DOMAIN broker_state[b].sk: + /\ broker_state[b].sk[s].commit_lsn <= max_commit_lsn + + +InitSafekeeper == [pruned_lsn |-> 0, commit_lsn |-> 0] +InitBroker == [sk |-> [s \in safekeepers |-> [commit_lsn |-> 0]]] +InitPageserver == [last_record_lsn |-> 0, preferred_sk |-> NULL, sk |-> [s \in safekeepers |-> [commit_lsn |-> 0]]] + +Init == + /\ broker_state = [b \in brokers |-> InitBroker] + /\ safekeeper_state = [s \in safekeepers |-> InitSafekeeper] + /\ pageserver_state = [p \in pageservers |-> InitPageserver] + +SkCommit(s) == + /\ safekeeper_state' = [safekeeper_state EXCEPT ![s].commit_lsn = safekeeper_state[s].commit_lsn + 1] + /\ UNCHANGED <> + +SkPushToBroker(s,b) == + /\ broker_state' = IF broker_state[b].sk[s].commit_lsn < safekeeper_state[s].commit_lsn + THEN + LET + bsk == broker_state[b].sk + updbsk == [bsk EXCEPT ![s].commit_lsn = safekeeper_state[s].commit_lsn] + IN + [broker_state EXCEPT ![b].sk = updbsk] + ELSE broker_state + /\ UNCHANGED <> + +PsRecvBroker(b,p,s) == + /\ LET + bsk == broker_state[b].sk[s] + psk == pageserver_state[p].sk[s] + updpsk == [psk EXCEPT !["commit_lsn"] = bsk.commit_lsn] + IN + pageserver_state' = IF bsk.commit_lsn > psk.commit_lsn + THEN [pageserver_state EXCEPT ![p].sk[s] = updpsk] + ELSE pageserver_state + /\ UNCHANGED <> + + +SksWithNewerWal(p) == + LET + ps == pageserver_state[p] + IN + {s \in DOMAIN ps.sk: ps.sk[s].commit_lsn > ps.last_record_lsn} + +PsChooseSk(p) == + /\ SksWithNewerWal(p) # {} + /\ pageserver_state' = [pageserver_state EXCEPT![p].preferred_sk = CHOOSE s \in SksWithNewerWal(p): TRUE] + /\ UNCHANGED <> + + +Next == + \/ \E s \in safekeepers: SkCommit(s) + \/ \E s \in safekeepers: \E b \in brokers: SkPushToBroker(s, b) + \/ \E s \in safekeepers: \E b \in brokers: \E p \in pageservers: PsRecvBroker(b,p,s) + \/ \E p \in pageservers: PsChooseSk(p) + + +Spec == Init /\ [][Next]_vars + +==== \ No newline at end of file diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297534393/MC.cfg b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297534393/MC.cfg new file mode 100644 index 0000000000..5d0e77461a --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297534393/MC.cfg @@ -0,0 +1,48 @@ +\* MV CONSTANT declarations +CONSTANTS +b1 = b1 +b2 = b2 +b3 = b3 +\* MV CONSTANT declarations +CONSTANTS +s1 = s1 +s2 = s2 +s3 = s3 +\* MV CONSTANT declarations +CONSTANTS +p1 = p1 +p2 = p2 +\* MV CONSTANT declarations +CONSTANTS +az1 = az1 +az2 = az2 +az3 = az3 +\* MV CONSTANT definitions +CONSTANT +brokers <- const_1737297530693169000 +\* CONSTANT declarations +CONSTANT NULL = NULL +\* MV CONSTANT definitions +CONSTANT +safekeepers <- const_1737297530694170000 +\* MV CONSTANT definitions +CONSTANT +pageservers <- const_1737297530694171000 +\* MV CONSTANT definitions +CONSTANT +azs <- const_1737297530694172000 +\* SYMMETRY definition +SYMMETRY symm_1737297530694173000 +\* CONSTANT definitions +CONSTANT +max_commit_lsn <- const_1737297530694174000 +\* CONSTANT definitions +CONSTANT +az_mapping <- const_1737297530694175000 +\* CONSTRAINT definition +CONSTRAINT +constr_1737297530694176000 +\* SPECIFICATION definition +SPECIFICATION +Spec +\* Generated on Sun Jan 19 15:38:50 CET 2025 \ No newline at end of file diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297534393/MC.out b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297534393/MC.out new file mode 100644 index 0000000000..6ab9f0e5e4 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297534393/MC.out @@ -0,0 +1,35 @@ +@!@!@STARTMSG 2262:0 @!@!@ +TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802) +@!@!@ENDMSG 2262 @!@!@ +@!@!@STARTMSG 2187:0 @!@!@ +Running breadth-first search Model-Checking with fp 130 and seed 4267255892797165884 with 4 workers on 8 cores with 2428MB heap and 5460MB offheap memory [pid: 6327] (Mac OS X 10.16 x86_64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue). +@!@!@ENDMSG 2187 @!@!@ +@!@!@STARTMSG 2220:0 @!@!@ +Starting SANY... +@!@!@ENDMSG 2220 @!@!@ +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/MC.tla +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/fullmesh.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/TLC.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Integers.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Naturals.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Sequences.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/FiniteSets.tla +Semantic processing of module Naturals +Semantic processing of module Integers +Semantic processing of module fullmesh +Semantic processing of module Sequences +Semantic processing of module FiniteSets +Semantic processing of module TLC +Semantic processing of module MC +@!@!@STARTMSG 2219:0 @!@!@ +SANY finished. +@!@!@ENDMSG 2219 @!@!@ +@!@!@STARTMSG 2185:0 @!@!@ +Starting... (2025-01-19 15:38:51) +@!@!@ENDMSG 2185 @!@!@ +@!@!@STARTMSG 2189:0 @!@!@ +Computing initial states... +@!@!@ENDMSG 2189 @!@!@ +@!@!@STARTMSG 2190:0 @!@!@ +Finished computing initial states: 1 distinct state generated at 2025-01-19 15:38:53. +@!@!@ENDMSG 2190 @!@!@ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297534393/MC.tla b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297534393/MC.tla new file mode 100644 index 0000000000..ec7157637f --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297534393/MC.tla @@ -0,0 +1,65 @@ +---- MODULE MC ---- +EXTENDS fullmesh, TLC + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +b1, b2, b3 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +s1, s2, s3 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +p1, p2 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +az1, az2, az3 +---- + +\* MV CONSTANT definitions brokers +const_1737297530693169000 == +{b1, b2, b3} +---- + +\* MV CONSTANT definitions safekeepers +const_1737297530694170000 == +{s1, s2, s3} +---- + +\* MV CONSTANT definitions pageservers +const_1737297530694171000 == +{p1, p2} +---- + +\* MV CONSTANT definitions azs +const_1737297530694172000 == +{az1, az2, az3} +---- + +\* SYMMETRY definition +symm_1737297530694173000 == +Permutations(const_1737297530693169000) \union Permutations(const_1737297530694170000) \union Permutations(const_1737297530694171000) \union Permutations(const_1737297530694172000) +---- + +\* CONSTANT definitions @modelParameterConstants:4max_commit_lsn +const_1737297530694174000 == +2 +---- + +\* CONSTANT definitions @modelParameterConstants:5az_mapping +const_1737297530694175000 == +[ az1 |-> {b1,s1,p1} , az2 |-> {b2,s2,p2} , az3 |-> {b3,s3}] +---- + +\* CONSTRAINT definition @modelParameterContraint:0 +constr_1737297530694176000 == +StateConstraint +---- +============================================================================= +\* Modification History +\* Created Sun Jan 19 15:38:50 CET 2025 by cs diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297534393/MC_TE.out b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297534393/MC_TE.out new file mode 100644 index 0000000000..6ab9f0e5e4 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297534393/MC_TE.out @@ -0,0 +1,35 @@ +@!@!@STARTMSG 2262:0 @!@!@ +TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802) +@!@!@ENDMSG 2262 @!@!@ +@!@!@STARTMSG 2187:0 @!@!@ +Running breadth-first search Model-Checking with fp 130 and seed 4267255892797165884 with 4 workers on 8 cores with 2428MB heap and 5460MB offheap memory [pid: 6327] (Mac OS X 10.16 x86_64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue). +@!@!@ENDMSG 2187 @!@!@ +@!@!@STARTMSG 2220:0 @!@!@ +Starting SANY... +@!@!@ENDMSG 2220 @!@!@ +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/MC.tla +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/fullmesh.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/TLC.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Integers.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Naturals.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Sequences.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/FiniteSets.tla +Semantic processing of module Naturals +Semantic processing of module Integers +Semantic processing of module fullmesh +Semantic processing of module Sequences +Semantic processing of module FiniteSets +Semantic processing of module TLC +Semantic processing of module MC +@!@!@STARTMSG 2219:0 @!@!@ +SANY finished. +@!@!@ENDMSG 2219 @!@!@ +@!@!@STARTMSG 2185:0 @!@!@ +Starting... (2025-01-19 15:38:51) +@!@!@ENDMSG 2185 @!@!@ +@!@!@STARTMSG 2189:0 @!@!@ +Computing initial states... +@!@!@ENDMSG 2189 @!@!@ +@!@!@STARTMSG 2190:0 @!@!@ +Finished computing initial states: 1 distinct state generated at 2025-01-19 15:38:53. +@!@!@ENDMSG 2190 @!@!@ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297534393/fullmesh.tla b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297534393/fullmesh.tla new file mode 100644 index 0000000000..9346db0d45 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297534393/fullmesh.tla @@ -0,0 +1,91 @@ +---- MODULE fullmesh ---- + +EXTENDS Integers + +VARIABLES broker_state, safekeeper_state, pageserver_state + + +CONSTANT + brokers, + safekeepers, + pageservers, + azs, + az_mapping + +CONSTANT + NULL + +CONSTANT + max_commit_lsn + +StateConstraint == + /\ \A s \in safekeepers: + /\ safekeeper_state[s].commit_lsn <= max_commit_lsn + /\ \A b \in brokers: + /\ \A s \in DOMAIN broker_state[b].sk: + /\ broker_state[b].sk[s].commit_lsn <= max_commit_lsn + + +InitSafekeeper == [pruned_lsn |-> 0, commit_lsn |-> 0] +InitBroker == [sk |-> [s \in safekeepers |-> [commit_lsn |-> 0]]] +InitPageserver == [last_record_lsn |-> 0, preferred_sk |-> NULL, sk |-> [s \in safekeepers |-> [commit_lsn |-> 0]]] + +Init == + /\ broker_state = [b \in brokers |-> InitBroker] + /\ safekeeper_state = [s \in safekeepers |-> InitSafekeeper] + /\ pageserver_state = [p \in pageservers |-> InitPageserver] + +SkCommit(s) == + /\ safekeeper_state' = [safekeeper_state EXCEPT ![s].commit_lsn = safekeeper_state[s].commit_lsn + 1] + /\ UNCHANGED <> + +SkPushToBroker(s,b) == + /\ broker_state' = IF broker_state[b].sk[s].commit_lsn < safekeeper_state[s].commit_lsn + THEN + LET + bsk == broker_state[b].sk + updbsk == [bsk EXCEPT ![s].commit_lsn = safekeeper_state[s].commit_lsn] + IN + [broker_state EXCEPT ![b].sk = updbsk] + ELSE broker_state + /\ UNCHANGED <> + +PsRecvBroker(b,p,s) == + /\ LET + bsk == broker_state[b].sk[s] + psk == pageserver_state[p].sk[s] + updpsk == [psk EXCEPT !["commit_lsn"] = bsk.commit_lsn] + IN + pageserver_state' = IF bsk.commit_lsn > psk.commit_lsn + THEN [pageserver_state EXCEPT ![p].sk[s] = updpsk] + ELSE pageserver_state + /\ UNCHANGED <> + + +SksWithNewerWal(p) == + LET + ps == pageserver_state[p] + IN + {s \in DOMAIN ps.sk: ps.sk[s].commit_lsn > ps.last_record_lsn} + +PsChooseSk(p) == + /\ SksWithNewerWal(p) # {} + /\ pageserver_state' = [pageserver_state EXCEPT![p].preferred_sk = CHOOSE s \in SksWithNewerWal(p): TRUE] + /\ UNCHANGED <> + + +Next == + \/ \E s \in safekeepers: SkCommit(s) + \/ \E s \in safekeepers: \E b \in brokers: SkPushToBroker(s, b) + \/ \E s \in safekeepers: \E b \in brokers: \E p \in pageservers: PsRecvBroker(b,p,s) + \/ \E p \in pageservers: PsChooseSk(p) + + +Spec == Init /\ [][Next]_<< broker_state, safekeeper_state, pageserver_state >> + + +\* invariants + + + +==== \ No newline at end of file diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297999722/MC.cfg b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297999722/MC.cfg new file mode 100644 index 0000000000..317368faaf --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297999722/MC.cfg @@ -0,0 +1,48 @@ +\* MV CONSTANT declarations +CONSTANTS +b1 = b1 +b2 = b2 +b3 = b3 +\* MV CONSTANT declarations +CONSTANTS +s1 = s1 +s2 = s2 +s3 = s3 +\* MV CONSTANT declarations +CONSTANTS +p1 = p1 +p2 = p2 +\* MV CONSTANT declarations +CONSTANTS +az1 = az1 +az2 = az2 +az3 = az3 +\* MV CONSTANT definitions +CONSTANT +brokers <- const_1737297992949177000 +\* CONSTANT declarations +CONSTANT NULL = NULL +\* MV CONSTANT definitions +CONSTANT +safekeepers <- const_1737297992949178000 +\* MV CONSTANT definitions +CONSTANT +pageservers <- const_1737297992949179000 +\* MV CONSTANT definitions +CONSTANT +azs <- const_1737297992949180000 +\* SYMMETRY definition +SYMMETRY symm_1737297992949181000 +\* CONSTANT definitions +CONSTANT +max_commit_lsn <- const_1737297992949182000 +\* CONSTANT definitions +CONSTANT +az_mapping <- const_1737297992949183000 +\* CONSTRAINT definition +CONSTRAINT +constr_1737297992949184000 +\* SPECIFICATION definition +SPECIFICATION +Spec +\* Generated on Sun Jan 19 15:46:32 CET 2025 \ No newline at end of file diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297999722/MC.out b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297999722/MC.out new file mode 100644 index 0000000000..be1df74b07 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297999722/MC.out @@ -0,0 +1,38 @@ +@!@!@STARTMSG 2262:0 @!@!@ +TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802) +@!@!@ENDMSG 2262 @!@!@ +@!@!@STARTMSG 2187:0 @!@!@ +Running breadth-first search Model-Checking with fp 0 and seed -5924036830053169413 with 4 workers on 8 cores with 2428MB heap and 5460MB offheap memory [pid: 6690] (Mac OS X 10.16 x86_64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue). +@!@!@ENDMSG 2187 @!@!@ +@!@!@STARTMSG 2220:0 @!@!@ +Starting SANY... +@!@!@ENDMSG 2220 @!@!@ +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/MC.tla +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/fullmesh.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/TLC.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Integers.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Naturals.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Sequences.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/FiniteSets.tla +Semantic processing of module Naturals +Semantic processing of module Integers +Semantic processing of module fullmesh +Semantic processing of module Sequences +Semantic processing of module FiniteSets +Semantic processing of module TLC +Semantic processing of module MC +@!@!@STARTMSG 2219:0 @!@!@ +SANY finished. +@!@!@ENDMSG 2219 @!@!@ +@!@!@STARTMSG 2185:0 @!@!@ +Starting... (2025-01-19 15:46:33) +@!@!@ENDMSG 2185 @!@!@ +@!@!@STARTMSG 2189:0 @!@!@ +Computing initial states... +@!@!@ENDMSG 2189 @!@!@ +@!@!@STARTMSG 2190:0 @!@!@ +Finished computing initial states: 1 distinct state generated at 2025-01-19 15:46:35. +@!@!@ENDMSG 2190 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(10) at 2025-01-19 15:46:38: 41.300 states generated (41.300 s/min), 3.445 distinct states found (3.445 ds/min), 2.202 states left on queue. +@!@!@ENDMSG 2200 @!@!@ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297999722/MC.tla b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297999722/MC.tla new file mode 100644 index 0000000000..ee8e18c7a3 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297999722/MC.tla @@ -0,0 +1,65 @@ +---- MODULE MC ---- +EXTENDS fullmesh, TLC + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +b1, b2, b3 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +s1, s2, s3 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +p1, p2 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +az1, az2, az3 +---- + +\* MV CONSTANT definitions brokers +const_1737297992949177000 == +{b1, b2, b3} +---- + +\* MV CONSTANT definitions safekeepers +const_1737297992949178000 == +{s1, s2, s3} +---- + +\* MV CONSTANT definitions pageservers +const_1737297992949179000 == +{p1, p2} +---- + +\* MV CONSTANT definitions azs +const_1737297992949180000 == +{az1, az2, az3} +---- + +\* SYMMETRY definition +symm_1737297992949181000 == +Permutations(const_1737297992949177000) \union Permutations(const_1737297992949178000) \union Permutations(const_1737297992949179000) \union Permutations(const_1737297992949180000) +---- + +\* CONSTANT definitions @modelParameterConstants:4max_commit_lsn +const_1737297992949182000 == +2 +---- + +\* CONSTANT definitions @modelParameterConstants:5az_mapping +const_1737297992949183000 == +[ az1 |-> {b1,s1,p1} , az2 |-> {b2,s2,p2} , az3 |-> {b3,s3}] +---- + +\* CONSTRAINT definition @modelParameterContraint:0 +constr_1737297992949184000 == +StateConstraint +---- +============================================================================= +\* Modification History +\* Created Sun Jan 19 15:46:32 CET 2025 by cs diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297999722/MC_TE.out b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297999722/MC_TE.out new file mode 100644 index 0000000000..be1df74b07 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297999722/MC_TE.out @@ -0,0 +1,38 @@ +@!@!@STARTMSG 2262:0 @!@!@ +TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802) +@!@!@ENDMSG 2262 @!@!@ +@!@!@STARTMSG 2187:0 @!@!@ +Running breadth-first search Model-Checking with fp 0 and seed -5924036830053169413 with 4 workers on 8 cores with 2428MB heap and 5460MB offheap memory [pid: 6690] (Mac OS X 10.16 x86_64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue). +@!@!@ENDMSG 2187 @!@!@ +@!@!@STARTMSG 2220:0 @!@!@ +Starting SANY... +@!@!@ENDMSG 2220 @!@!@ +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/MC.tla +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/fullmesh.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/TLC.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Integers.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Naturals.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Sequences.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/FiniteSets.tla +Semantic processing of module Naturals +Semantic processing of module Integers +Semantic processing of module fullmesh +Semantic processing of module Sequences +Semantic processing of module FiniteSets +Semantic processing of module TLC +Semantic processing of module MC +@!@!@STARTMSG 2219:0 @!@!@ +SANY finished. +@!@!@ENDMSG 2219 @!@!@ +@!@!@STARTMSG 2185:0 @!@!@ +Starting... (2025-01-19 15:46:33) +@!@!@ENDMSG 2185 @!@!@ +@!@!@STARTMSG 2189:0 @!@!@ +Computing initial states... +@!@!@ENDMSG 2189 @!@!@ +@!@!@STARTMSG 2190:0 @!@!@ +Finished computing initial states: 1 distinct state generated at 2025-01-19 15:46:35. +@!@!@ENDMSG 2190 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(10) at 2025-01-19 15:46:38: 41.300 states generated (41.300 s/min), 3.445 distinct states found (3.445 ds/min), 2.202 states left on queue. +@!@!@ENDMSG 2200 @!@!@ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297999722/fullmesh.tla b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297999722/fullmesh.tla new file mode 100644 index 0000000000..b752cd48e2 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737297999722/fullmesh.tla @@ -0,0 +1,97 @@ +---- MODULE fullmesh ---- + +EXTENDS Integers + +VARIABLES broker_state, safekeeper_state, pageserver_state + + +CONSTANT + brokers, + safekeepers, + pageservers, + azs, + az_mapping + +CONSTANT + NULL + +CONSTANT + max_commit_lsn + +StateConstraint == + /\ \A s \in safekeepers: + /\ safekeeper_state[s].commit_lsn <= max_commit_lsn + /\ \A b \in brokers: + /\ \A s \in DOMAIN broker_state[b].sk: + /\ broker_state[b].sk[s].commit_lsn <= max_commit_lsn + + +InitSafekeeper == [pruned_lsn |-> 0, commit_lsn |-> 0] +InitBroker == [sk |-> [s \in safekeepers |-> [commit_lsn |-> 0]]] +InitPageserver == [last_record_lsn |-> 0, preferred_sk |-> NULL, sk |-> [s \in safekeepers |-> [commit_lsn |-> 0]]] + +Init == + /\ broker_state = [b \in brokers |-> InitBroker] + /\ safekeeper_state = [s \in safekeepers |-> InitSafekeeper] + /\ pageserver_state = [p \in pageservers |-> InitPageserver] + +SkCommit(s1, s2) == + /\ safekeeper_state[s1].commit_lsn = safekeeper_state[s2].commit_lsn + /\ LET + new_commit_lsn == safekeeper_state[s1].commit_lsn + 1 + IN + safekeeper_state' = [safekeeper_state EXCEPT + ![s1].commit_lsn = new_commit_lsn, + ![s2].commit_lsn = new_commit_lsn] + /\ UNCHANGED <> + +SkPushToBroker(s,b) == + /\ broker_state' = IF broker_state[b].sk[s].commit_lsn < safekeeper_state[s].commit_lsn + THEN + LET + bsk == broker_state[b].sk + updbsk == [bsk EXCEPT ![s].commit_lsn = safekeeper_state[s].commit_lsn] + IN + [broker_state EXCEPT ![b].sk = updbsk] + ELSE broker_state + /\ UNCHANGED <> + +PsRecvBroker(b,p,s) == + /\ LET + bsk == broker_state[b].sk[s] + psk == pageserver_state[p].sk[s] + updpsk == [psk EXCEPT !["commit_lsn"] = bsk.commit_lsn] + IN + pageserver_state' = IF bsk.commit_lsn > psk.commit_lsn + THEN [pageserver_state EXCEPT ![p].sk[s] = updpsk] + ELSE pageserver_state + /\ UNCHANGED <> + + +SksWithNewerWal(p) == + LET + ps == pageserver_state[p] + IN + {s \in DOMAIN ps.sk: ps.sk[s].commit_lsn > ps.last_record_lsn} + +PsChooseSk(p) == + /\ SksWithNewerWal(p) # {} + /\ pageserver_state' = [pageserver_state EXCEPT![p].preferred_sk = CHOOSE s \in SksWithNewerWal(p): TRUE] + /\ UNCHANGED <> + + +Next == + \/ \E s1 \in safekeepers: \E s2 \in safekeepers: SkCommit(s1, s2) + \/ \E s \in safekeepers: \E b \in brokers: SkPushToBroker(s, b) + \/ \E s \in safekeepers: \E b \in brokers: \E p \in pageservers: PsRecvBroker(b,p,s) + \/ \E p \in pageservers: PsChooseSk(p) + + +Spec == Init /\ [][Next]_<< broker_state, safekeeper_state, pageserver_state >> + + +\* invariants + + + +==== \ No newline at end of file diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299352762/MC.cfg b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299352762/MC.cfg new file mode 100644 index 0000000000..fa522b981a --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299352762/MC.cfg @@ -0,0 +1,51 @@ +\* MV CONSTANT declarations +CONSTANTS +b1 = b1 +b2 = b2 +b3 = b3 +\* MV CONSTANT declarations +CONSTANTS +s1 = s1 +s2 = s2 +s3 = s3 +\* MV CONSTANT declarations +CONSTANTS +p1 = p1 +p2 = p2 +\* MV CONSTANT declarations +CONSTANTS +az1 = az1 +az2 = az2 +az3 = az3 +\* MV CONSTANT definitions +CONSTANT +brokers <- const_1737299350679194000 +\* CONSTANT declarations +CONSTANT NULL = NULL +\* MV CONSTANT definitions +CONSTANT +safekeepers <- const_1737299350679195000 +\* MV CONSTANT definitions +CONSTANT +pageservers <- const_1737299350679196000 +\* MV CONSTANT definitions +CONSTANT +azs <- const_1737299350679197000 +\* SYMMETRY definition +SYMMETRY symm_1737299350679198000 +\* CONSTANT definitions +CONSTANT +max_commit_lsn <- const_1737299350679199000 +\* CONSTANT definitions +CONSTANT +az_mapping <- const_1737299350679200000 +\* CONSTRAINT definition +CONSTRAINT +constr_1737299350680201000 +\* SPECIFICATION definition +SPECIFICATION +Spec +\* INVARIANT definition +INVARIANT +EventuallyLaggingSkIsNotPreferredSk +\* Generated on Sun Jan 19 16:09:10 CET 2025 \ No newline at end of file diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299352762/MC.out b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299352762/MC.out new file mode 100644 index 0000000000..27a0150e6e --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299352762/MC.out @@ -0,0 +1,35 @@ +@!@!@STARTMSG 2262:0 @!@!@ +TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802) +@!@!@ENDMSG 2262 @!@!@ +@!@!@STARTMSG 2187:0 @!@!@ +Running breadth-first search Model-Checking with fp 119 and seed -1908114041878732601 with 4 workers on 8 cores with 2428MB heap and 5460MB offheap memory [pid: 7665] (Mac OS X 10.16 x86_64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue). +@!@!@ENDMSG 2187 @!@!@ +@!@!@STARTMSG 2220:0 @!@!@ +Starting SANY... +@!@!@ENDMSG 2220 @!@!@ +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/MC.tla +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/fullmesh.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/TLC.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Integers.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Naturals.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Sequences.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/FiniteSets.tla +Semantic processing of module Naturals +Semantic processing of module Integers +Semantic processing of module fullmesh +Semantic processing of module Sequences +Semantic processing of module FiniteSets +Semantic processing of module TLC +Semantic processing of module MC +@!@!@STARTMSG 2219:0 @!@!@ +SANY finished. +@!@!@ENDMSG 2219 @!@!@ +@!@!@STARTMSG 2185:0 @!@!@ +Starting... (2025-01-19 16:09:11) +@!@!@ENDMSG 2185 @!@!@ +@!@!@STARTMSG 2146:1 @!@!@ +The invariant EventuallyLaggingSkIsNotPreferredSk is not a state predicate (one with no primes or temporal operators). +@!@!@ENDMSG 2146 @!@!@ +@!@!@STARTMSG 2186:0 @!@!@ +Finished in 994ms at (2025-01-19 16:09:11) +@!@!@ENDMSG 2186 @!@!@ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299352762/MC.tla b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299352762/MC.tla new file mode 100644 index 0000000000..1dd82bc923 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299352762/MC.tla @@ -0,0 +1,65 @@ +---- MODULE MC ---- +EXTENDS fullmesh, TLC + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +b1, b2, b3 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +s1, s2, s3 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +p1, p2 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +az1, az2, az3 +---- + +\* MV CONSTANT definitions brokers +const_1737299350679194000 == +{b1, b2, b3} +---- + +\* MV CONSTANT definitions safekeepers +const_1737299350679195000 == +{s1, s2, s3} +---- + +\* MV CONSTANT definitions pageservers +const_1737299350679196000 == +{p1, p2} +---- + +\* MV CONSTANT definitions azs +const_1737299350679197000 == +{az1, az2, az3} +---- + +\* SYMMETRY definition +symm_1737299350679198000 == +Permutations(const_1737299350679194000) \union Permutations(const_1737299350679195000) \union Permutations(const_1737299350679196000) \union Permutations(const_1737299350679197000) +---- + +\* CONSTANT definitions @modelParameterConstants:4max_commit_lsn +const_1737299350679199000 == +2 +---- + +\* CONSTANT definitions @modelParameterConstants:5az_mapping +const_1737299350679200000 == +[ az1 |-> {b1,s1,p1} , az2 |-> {b2,s2,p2} , az3 |-> {b3,s3}] +---- + +\* CONSTRAINT definition @modelParameterContraint:0 +constr_1737299350680201000 == +StateConstraint +---- +============================================================================= +\* Modification History +\* Created Sun Jan 19 16:09:10 CET 2025 by cs diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299352762/MC_TE.out b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299352762/MC_TE.out new file mode 100644 index 0000000000..27a0150e6e --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299352762/MC_TE.out @@ -0,0 +1,35 @@ +@!@!@STARTMSG 2262:0 @!@!@ +TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802) +@!@!@ENDMSG 2262 @!@!@ +@!@!@STARTMSG 2187:0 @!@!@ +Running breadth-first search Model-Checking with fp 119 and seed -1908114041878732601 with 4 workers on 8 cores with 2428MB heap and 5460MB offheap memory [pid: 7665] (Mac OS X 10.16 x86_64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue). +@!@!@ENDMSG 2187 @!@!@ +@!@!@STARTMSG 2220:0 @!@!@ +Starting SANY... +@!@!@ENDMSG 2220 @!@!@ +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/MC.tla +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/fullmesh.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/TLC.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Integers.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Naturals.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Sequences.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/FiniteSets.tla +Semantic processing of module Naturals +Semantic processing of module Integers +Semantic processing of module fullmesh +Semantic processing of module Sequences +Semantic processing of module FiniteSets +Semantic processing of module TLC +Semantic processing of module MC +@!@!@STARTMSG 2219:0 @!@!@ +SANY finished. +@!@!@ENDMSG 2219 @!@!@ +@!@!@STARTMSG 2185:0 @!@!@ +Starting... (2025-01-19 16:09:11) +@!@!@ENDMSG 2185 @!@!@ +@!@!@STARTMSG 2146:1 @!@!@ +The invariant EventuallyLaggingSkIsNotPreferredSk is not a state predicate (one with no primes or temporal operators). +@!@!@ENDMSG 2146 @!@!@ +@!@!@STARTMSG 2186:0 @!@!@ +Finished in 994ms at (2025-01-19 16:09:11) +@!@!@ENDMSG 2186 @!@!@ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299352762/fullmesh.tla b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299352762/fullmesh.tla new file mode 100644 index 0000000000..a6c5e2ea3f --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299352762/fullmesh.tla @@ -0,0 +1,115 @@ +---- MODULE fullmesh ---- + +EXTENDS Integers + +VARIABLES broker_state, safekeeper_state, pageserver_state + + +CONSTANT + brokers, + safekeepers, + pageservers, + azs, + az_mapping + +CONSTANT + NULL + +CONSTANT + max_commit_lsn + +StateConstraint == + /\ \A s \in safekeepers: + /\ safekeeper_state[s].commit_lsn <= max_commit_lsn + /\ \A b \in brokers: + /\ \A s \in DOMAIN broker_state[b].sk: + /\ broker_state[b].sk[s].commit_lsn <= max_commit_lsn + + +InitSafekeeper == [pruned_lsn |-> 0, commit_lsn |-> 0] +InitBroker == [sk |-> [s \in safekeepers |-> [commit_lsn |-> 0]]] +InitPageserver == [last_record_lsn |-> 0, preferred_sk |-> NULL, sk |-> [s \in safekeepers |-> [commit_lsn |-> 0]]] + +Init == + /\ broker_state = [b \in brokers |-> InitBroker] + /\ safekeeper_state = [s \in safekeepers |-> InitSafekeeper] + /\ pageserver_state = [p \in pageservers |-> InitPageserver] + + +SkCommit(s1, s2) == + /\ safekeeper_state[s1].commit_lsn = safekeeper_state[s2].commit_lsn + /\ LET + new_commit_lsn == safekeeper_state[s1].commit_lsn + 1 + IN + safekeeper_state' = [safekeeper_state EXCEPT + ![s1].commit_lsn = new_commit_lsn, + ![s2].commit_lsn = new_commit_lsn] + /\ UNCHANGED <> + +SkPeerRecovery(s1,s2) == + /\ safekeeper_state[s1].commit_lsn < safekeeper_state[s2].commit_lsn + /\ safekeeper_state' = [safekeeper_state EXCEPT![s1].commit_lsn = safekeeper_state[s2].commit_lsn] + +SkPushToBroker(s,b) == + /\ broker_state' = IF broker_state[b].sk[s].commit_lsn < safekeeper_state[s].commit_lsn + THEN + LET + bsk == broker_state[b].sk + updbsk == [bsk EXCEPT ![s].commit_lsn = safekeeper_state[s].commit_lsn] + IN + [broker_state EXCEPT ![b].sk = updbsk] + ELSE broker_state + /\ UNCHANGED <> + +PsRecvBroker(b,p,s) == + /\ LET + bsk == broker_state[b].sk[s] + psk == pageserver_state[p].sk[s] + updpsk == [psk EXCEPT !["commit_lsn"] = bsk.commit_lsn] + IN + pageserver_state' = IF bsk.commit_lsn > psk.commit_lsn + THEN [pageserver_state EXCEPT ![p].sk[s] = updpsk] + ELSE pageserver_state + /\ UNCHANGED <> + + +SksWithNewerWal(p) == + LET + ps == pageserver_state[p] + IN + {s \in DOMAIN ps.sk: ps.sk[s].commit_lsn > ps.last_record_lsn} + +PsChooseSk(p) == + /\ SksWithNewerWal(p) # {} + /\ pageserver_state' = [pageserver_state EXCEPT![p].preferred_sk = CHOOSE s \in SksWithNewerWal(p): TRUE] + /\ UNCHANGED <> + + +Next == + + \/ \E s1 \in safekeepers: \E s2 \in safekeepers: + \/ SkCommit(s1, s2) + \/ SkPeerRecovery(s1, s2) + \/ \E s \in safekeepers: \E b \in brokers: SkPushToBroker(s, b) + \/ \E s \in safekeepers: \E b \in brokers: \E p \in pageservers: PsRecvBroker(b,p,s) + \/ \E p \in pageservers: PsChooseSk(p) + + +Spec == Init /\ [][Next]_<< broker_state, safekeeper_state, pageserver_state >> + + +\* invariants + +EventuallyLaggingSkIsNotPreferredSk == <>( + LET + sks == safekeeper_state + lagging_sks == { s \in safekeepers: \A s2 \in safekeepers: sks[s].commit_lsn <= sks[s2].commit_lsn } + preferred_sks == {pageserver_state[p].preferred_sk: p \in pageservers} + IN + preferred_sks \cap lagging_sks = {} + + ) + + + +==== \ No newline at end of file diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299381423/MC.cfg b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299381423/MC.cfg new file mode 100644 index 0000000000..b9bc8092a2 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299381423/MC.cfg @@ -0,0 +1,51 @@ +\* MV CONSTANT declarations +CONSTANTS +b1 = b1 +b2 = b2 +b3 = b3 +\* MV CONSTANT declarations +CONSTANTS +s1 = s1 +s2 = s2 +s3 = s3 +\* MV CONSTANT declarations +CONSTANTS +p1 = p1 +p2 = p2 +\* MV CONSTANT declarations +CONSTANTS +az1 = az1 +az2 = az2 +az3 = az3 +\* MV CONSTANT definitions +CONSTANT +brokers <- const_1737299377376212000 +\* CONSTANT declarations +CONSTANT NULL = NULL +\* MV CONSTANT definitions +CONSTANT +safekeepers <- const_1737299377376213000 +\* MV CONSTANT definitions +CONSTANT +pageservers <- const_1737299377376214000 +\* MV CONSTANT definitions +CONSTANT +azs <- const_1737299377376215000 +\* SYMMETRY definition +SYMMETRY symm_1737299377376216000 +\* CONSTANT definitions +CONSTANT +max_commit_lsn <- const_1737299377376217000 +\* CONSTANT definitions +CONSTANT +az_mapping <- const_1737299377376218000 +\* CONSTRAINT definition +CONSTRAINT +constr_1737299377376219000 +\* SPECIFICATION definition +SPECIFICATION +Spec +\* PROPERTY definition +PROPERTY +EventuallyLaggingSkIsNotPreferredSk +\* Generated on Sun Jan 19 16:09:37 CET 2025 \ No newline at end of file diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299381423/MC.out b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299381423/MC.out new file mode 100644 index 0000000000..7760635dfb --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299381423/MC.out @@ -0,0 +1,186 @@ +@!@!@STARTMSG 2262:0 @!@!@ +TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802) +@!@!@ENDMSG 2262 @!@!@ +@!@!@STARTMSG 2187:0 @!@!@ +Running breadth-first search Model-Checking with fp 3 and seed -7432767478319300652 with 4 workers on 8 cores with 2428MB heap and 5460MB offheap memory [pid: 7681] (Mac OS X 10.16 x86_64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue). +@!@!@ENDMSG 2187 @!@!@ +@!@!@STARTMSG 2220:0 @!@!@ +Starting SANY... +@!@!@ENDMSG 2220 @!@!@ +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/MC.tla +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/fullmesh.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/TLC.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Integers.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Naturals.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Sequences.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/FiniteSets.tla +Semantic processing of module Naturals +Semantic processing of module Integers +Semantic processing of module fullmesh +Semantic processing of module Sequences +Semantic processing of module FiniteSets +Semantic processing of module TLC +Semantic processing of module MC +@!@!@STARTMSG 2219:0 @!@!@ +SANY finished. +@!@!@ENDMSG 2219 @!@!@ +@!@!@STARTMSG 2185:0 @!@!@ +Starting... (2025-01-19 16:09:38) +@!@!@ENDMSG 2185 @!@!@ +@!@!@STARTMSG 2279:3 @!@!@ +Declaring symmetry during liveness checking is dangerous. It might cause TLC to miss violations of the stated liveness properties. Please check liveness without symmetry defined. +@!@!@ENDMSG 2279 @!@!@ +@!@!@STARTMSG 2284:3 @!@!@ +Declaring state or action constraints during liveness checking is dangerous: Please read section 14.3.5 on page 247 of Specifying Systems (https://lamport.azurewebsites.net/tla/book.html) and optionally the discussion at https://discuss.tlapl.us/msg00994.html for more details. +@!@!@ENDMSG 2284 @!@!@ +@!@!@STARTMSG 2212:0 @!@!@ +Implied-temporal checking--satisfiability problem has 1 branches. +@!@!@ENDMSG 2212 @!@!@ +@!@!@STARTMSG 2189:0 @!@!@ +Computing initial states... +@!@!@ENDMSG 2189 @!@!@ +@!@!@STARTMSG 2190:0 @!@!@ +Finished computing initial states: 1 distinct state generated at 2025-01-19 16:09:40. +@!@!@ENDMSG 2190 @!@!@ +@!@!@STARTMSG 2109:1 @!@!@ +Successor state is not completely specified by action SkPeerRecovery of the next-state relation. The following variables are not assigned: broker_state, pageserver_state. + +@!@!@ENDMSG 2109 @!@!@ +@!@!@STARTMSG 2121:1 @!@!@ +The behavior up to this point is: +@!@!@ENDMSG 2121 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +1: +/\ pageserver_state = (p1 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0]), last_record_lsn |-> 0, preferred_sk |-> NULL] @@ p2 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0]), last_record_lsn |-> 0, preferred_sk |-> NULL]) +/\ broker_state = (b1 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])] @@ b2 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])] @@ b3 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])]) +/\ safekeeper_state = (s1 :> [commit_lsn |-> 0, pruned_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0, pruned_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0, pruned_lsn |-> 0]) + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +2: +/\ pageserver_state = (p1 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0]), last_record_lsn |-> 0, preferred_sk |-> NULL] @@ p2 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0]), last_record_lsn |-> 0, preferred_sk |-> NULL]) +/\ broker_state = (b1 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])] @@ b2 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])] @@ b3 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])]) +/\ safekeeper_state = (s1 :> [commit_lsn |-> 1, pruned_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0, pruned_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0, pruned_lsn |-> 0]) + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +3: +/\ pageserver_state = null +/\ broker_state = null +/\ safekeeper_state = (s1 :> [commit_lsn |-> 1, pruned_lsn |-> 0] @@ s2 :> [commit_lsn |-> 1, pruned_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0, pruned_lsn |-> 0]) + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2201:0 @!@!@ +The coverage statistics at 2025-01-19 16:09:40 +@!@!@ENDMSG 2201 @!@!@ +@!@!@STARTMSG 2773:0 @!@!@ +: 2:2 +@!@!@ENDMSG 2773 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 34, col 5 to line 36, col 64 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 5:17 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 40, col 8 to line 40, col 72 of module fullmesh: 46 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 40, col 8 to line 40, col 38 of module fullmesh: 29 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 40, col 42 to line 40, col 72 of module fullmesh: 29 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 44, col 13 to line 46, col 50 of module fullmesh: 17 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 47, col 8 to line 47, col 51 of module fullmesh: 17 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 0:4 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 50, col 8 to line 50, col 72 of module fullmesh: 1 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 50, col 8 to line 50, col 38 of module fullmesh: 28 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 50, col 42 to line 50, col 72 of module fullmesh: 28 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 51, col 8 to line 51, col 102 of module fullmesh: 1 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 51, col 28 to line 51, col 102 of module fullmesh: 4 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 0:9 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 54, col 8 to line 61, col 29 of module fullmesh: 9 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 62, col 8 to line 62, col 55 of module fullmesh: 9 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 0:18 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 70, col 13 to line 72, col 37 of module fullmesh: 18 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 73, col 8 to line 73, col 51 of module fullmesh: 18 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 0:0 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 83, col 8 to line 83, col 30 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 83, col 8 to line 83, col 25 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 78, col 15 to line 78, col 33 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 80, col 5 to line 80, col 66 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 80, col 26 to line 80, col 65 of module fullmesh: 6 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 80, col 12 to line 80, col 23 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 83, col 24 to line 83, col 24 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 83, col 29 to line 83, col 30 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 84, col 8 to line 84, col 109 of module fullmesh: 0 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 85, col 8 to line 85, col 51 of module fullmesh: 0 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2202:0 @!@!@ +End of statistics. +@!@!@ENDMSG 2202 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(3) at 2025-01-19 16:09:40: 46 states generated (1.044 s/min), 6 distinct states found (136 ds/min), 2 states left on queue. +@!@!@ENDMSG 2200 @!@!@ +@!@!@STARTMSG 2199:0 @!@!@ +46 states generated, 6 distinct states found, 2 states left on queue. +@!@!@ENDMSG 2199 @!@!@ +@!@!@STARTMSG 2194:0 @!@!@ +The depth of the complete state graph search is 3. +@!@!@ENDMSG 2194 @!@!@ +@!@!@STARTMSG 2268:0 @!@!@ +The average outdegree of the complete state graph is 2 (minimum is 2, the maximum 2 and the 95th percentile is 2). +@!@!@ENDMSG 2268 @!@!@ +@!@!@STARTMSG 2186:0 @!@!@ +Finished in 2658ms at (2025-01-19 16:09:40) +@!@!@ENDMSG 2186 @!@!@ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299381423/MC.tla b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299381423/MC.tla new file mode 100644 index 0000000000..9df26a2fc9 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299381423/MC.tla @@ -0,0 +1,65 @@ +---- MODULE MC ---- +EXTENDS fullmesh, TLC + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +b1, b2, b3 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +s1, s2, s3 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +p1, p2 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +az1, az2, az3 +---- + +\* MV CONSTANT definitions brokers +const_1737299377376212000 == +{b1, b2, b3} +---- + +\* MV CONSTANT definitions safekeepers +const_1737299377376213000 == +{s1, s2, s3} +---- + +\* MV CONSTANT definitions pageservers +const_1737299377376214000 == +{p1, p2} +---- + +\* MV CONSTANT definitions azs +const_1737299377376215000 == +{az1, az2, az3} +---- + +\* SYMMETRY definition +symm_1737299377376216000 == +Permutations(const_1737299377376212000) \union Permutations(const_1737299377376213000) \union Permutations(const_1737299377376214000) \union Permutations(const_1737299377376215000) +---- + +\* CONSTANT definitions @modelParameterConstants:4max_commit_lsn +const_1737299377376217000 == +2 +---- + +\* CONSTANT definitions @modelParameterConstants:5az_mapping +const_1737299377376218000 == +[ az1 |-> {b1,s1,p1} , az2 |-> {b2,s2,p2} , az3 |-> {b3,s3}] +---- + +\* CONSTRAINT definition @modelParameterContraint:0 +constr_1737299377376219000 == +StateConstraint +---- +============================================================================= +\* Modification History +\* Created Sun Jan 19 16:09:37 CET 2025 by cs diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299381423/MC_TE.out b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299381423/MC_TE.out new file mode 100644 index 0000000000..7760635dfb --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299381423/MC_TE.out @@ -0,0 +1,186 @@ +@!@!@STARTMSG 2262:0 @!@!@ +TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802) +@!@!@ENDMSG 2262 @!@!@ +@!@!@STARTMSG 2187:0 @!@!@ +Running breadth-first search Model-Checking with fp 3 and seed -7432767478319300652 with 4 workers on 8 cores with 2428MB heap and 5460MB offheap memory [pid: 7681] (Mac OS X 10.16 x86_64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue). +@!@!@ENDMSG 2187 @!@!@ +@!@!@STARTMSG 2220:0 @!@!@ +Starting SANY... +@!@!@ENDMSG 2220 @!@!@ +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/MC.tla +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/fullmesh.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/TLC.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Integers.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Naturals.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Sequences.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/FiniteSets.tla +Semantic processing of module Naturals +Semantic processing of module Integers +Semantic processing of module fullmesh +Semantic processing of module Sequences +Semantic processing of module FiniteSets +Semantic processing of module TLC +Semantic processing of module MC +@!@!@STARTMSG 2219:0 @!@!@ +SANY finished. +@!@!@ENDMSG 2219 @!@!@ +@!@!@STARTMSG 2185:0 @!@!@ +Starting... (2025-01-19 16:09:38) +@!@!@ENDMSG 2185 @!@!@ +@!@!@STARTMSG 2279:3 @!@!@ +Declaring symmetry during liveness checking is dangerous. It might cause TLC to miss violations of the stated liveness properties. Please check liveness without symmetry defined. +@!@!@ENDMSG 2279 @!@!@ +@!@!@STARTMSG 2284:3 @!@!@ +Declaring state or action constraints during liveness checking is dangerous: Please read section 14.3.5 on page 247 of Specifying Systems (https://lamport.azurewebsites.net/tla/book.html) and optionally the discussion at https://discuss.tlapl.us/msg00994.html for more details. +@!@!@ENDMSG 2284 @!@!@ +@!@!@STARTMSG 2212:0 @!@!@ +Implied-temporal checking--satisfiability problem has 1 branches. +@!@!@ENDMSG 2212 @!@!@ +@!@!@STARTMSG 2189:0 @!@!@ +Computing initial states... +@!@!@ENDMSG 2189 @!@!@ +@!@!@STARTMSG 2190:0 @!@!@ +Finished computing initial states: 1 distinct state generated at 2025-01-19 16:09:40. +@!@!@ENDMSG 2190 @!@!@ +@!@!@STARTMSG 2109:1 @!@!@ +Successor state is not completely specified by action SkPeerRecovery of the next-state relation. The following variables are not assigned: broker_state, pageserver_state. + +@!@!@ENDMSG 2109 @!@!@ +@!@!@STARTMSG 2121:1 @!@!@ +The behavior up to this point is: +@!@!@ENDMSG 2121 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +1: +/\ pageserver_state = (p1 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0]), last_record_lsn |-> 0, preferred_sk |-> NULL] @@ p2 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0]), last_record_lsn |-> 0, preferred_sk |-> NULL]) +/\ broker_state = (b1 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])] @@ b2 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])] @@ b3 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])]) +/\ safekeeper_state = (s1 :> [commit_lsn |-> 0, pruned_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0, pruned_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0, pruned_lsn |-> 0]) + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +2: +/\ pageserver_state = (p1 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0]), last_record_lsn |-> 0, preferred_sk |-> NULL] @@ p2 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0]), last_record_lsn |-> 0, preferred_sk |-> NULL]) +/\ broker_state = (b1 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])] @@ b2 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])] @@ b3 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])]) +/\ safekeeper_state = (s1 :> [commit_lsn |-> 1, pruned_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0, pruned_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0, pruned_lsn |-> 0]) + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +3: +/\ pageserver_state = null +/\ broker_state = null +/\ safekeeper_state = (s1 :> [commit_lsn |-> 1, pruned_lsn |-> 0] @@ s2 :> [commit_lsn |-> 1, pruned_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0, pruned_lsn |-> 0]) + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2201:0 @!@!@ +The coverage statistics at 2025-01-19 16:09:40 +@!@!@ENDMSG 2201 @!@!@ +@!@!@STARTMSG 2773:0 @!@!@ +: 2:2 +@!@!@ENDMSG 2773 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 34, col 5 to line 36, col 64 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 5:17 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 40, col 8 to line 40, col 72 of module fullmesh: 46 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 40, col 8 to line 40, col 38 of module fullmesh: 29 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 40, col 42 to line 40, col 72 of module fullmesh: 29 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 44, col 13 to line 46, col 50 of module fullmesh: 17 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 47, col 8 to line 47, col 51 of module fullmesh: 17 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 0:4 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 50, col 8 to line 50, col 72 of module fullmesh: 1 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 50, col 8 to line 50, col 38 of module fullmesh: 28 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 50, col 42 to line 50, col 72 of module fullmesh: 28 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 51, col 8 to line 51, col 102 of module fullmesh: 1 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 51, col 28 to line 51, col 102 of module fullmesh: 4 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 0:9 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 54, col 8 to line 61, col 29 of module fullmesh: 9 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 62, col 8 to line 62, col 55 of module fullmesh: 9 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 0:18 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 70, col 13 to line 72, col 37 of module fullmesh: 18 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 73, col 8 to line 73, col 51 of module fullmesh: 18 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 0:0 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 83, col 8 to line 83, col 30 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 83, col 8 to line 83, col 25 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 78, col 15 to line 78, col 33 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 80, col 5 to line 80, col 66 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 80, col 26 to line 80, col 65 of module fullmesh: 6 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 80, col 12 to line 80, col 23 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 83, col 24 to line 83, col 24 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 83, col 29 to line 83, col 30 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 84, col 8 to line 84, col 109 of module fullmesh: 0 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 85, col 8 to line 85, col 51 of module fullmesh: 0 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2202:0 @!@!@ +End of statistics. +@!@!@ENDMSG 2202 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(3) at 2025-01-19 16:09:40: 46 states generated (1.044 s/min), 6 distinct states found (136 ds/min), 2 states left on queue. +@!@!@ENDMSG 2200 @!@!@ +@!@!@STARTMSG 2199:0 @!@!@ +46 states generated, 6 distinct states found, 2 states left on queue. +@!@!@ENDMSG 2199 @!@!@ +@!@!@STARTMSG 2194:0 @!@!@ +The depth of the complete state graph search is 3. +@!@!@ENDMSG 2194 @!@!@ +@!@!@STARTMSG 2268:0 @!@!@ +The average outdegree of the complete state graph is 2 (minimum is 2, the maximum 2 and the 95th percentile is 2). +@!@!@ENDMSG 2268 @!@!@ +@!@!@STARTMSG 2186:0 @!@!@ +Finished in 2658ms at (2025-01-19 16:09:40) +@!@!@ENDMSG 2186 @!@!@ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299381423/fullmesh.tla b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299381423/fullmesh.tla new file mode 100644 index 0000000000..a6c5e2ea3f --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299381423/fullmesh.tla @@ -0,0 +1,115 @@ +---- MODULE fullmesh ---- + +EXTENDS Integers + +VARIABLES broker_state, safekeeper_state, pageserver_state + + +CONSTANT + brokers, + safekeepers, + pageservers, + azs, + az_mapping + +CONSTANT + NULL + +CONSTANT + max_commit_lsn + +StateConstraint == + /\ \A s \in safekeepers: + /\ safekeeper_state[s].commit_lsn <= max_commit_lsn + /\ \A b \in brokers: + /\ \A s \in DOMAIN broker_state[b].sk: + /\ broker_state[b].sk[s].commit_lsn <= max_commit_lsn + + +InitSafekeeper == [pruned_lsn |-> 0, commit_lsn |-> 0] +InitBroker == [sk |-> [s \in safekeepers |-> [commit_lsn |-> 0]]] +InitPageserver == [last_record_lsn |-> 0, preferred_sk |-> NULL, sk |-> [s \in safekeepers |-> [commit_lsn |-> 0]]] + +Init == + /\ broker_state = [b \in brokers |-> InitBroker] + /\ safekeeper_state = [s \in safekeepers |-> InitSafekeeper] + /\ pageserver_state = [p \in pageservers |-> InitPageserver] + + +SkCommit(s1, s2) == + /\ safekeeper_state[s1].commit_lsn = safekeeper_state[s2].commit_lsn + /\ LET + new_commit_lsn == safekeeper_state[s1].commit_lsn + 1 + IN + safekeeper_state' = [safekeeper_state EXCEPT + ![s1].commit_lsn = new_commit_lsn, + ![s2].commit_lsn = new_commit_lsn] + /\ UNCHANGED <> + +SkPeerRecovery(s1,s2) == + /\ safekeeper_state[s1].commit_lsn < safekeeper_state[s2].commit_lsn + /\ safekeeper_state' = [safekeeper_state EXCEPT![s1].commit_lsn = safekeeper_state[s2].commit_lsn] + +SkPushToBroker(s,b) == + /\ broker_state' = IF broker_state[b].sk[s].commit_lsn < safekeeper_state[s].commit_lsn + THEN + LET + bsk == broker_state[b].sk + updbsk == [bsk EXCEPT ![s].commit_lsn = safekeeper_state[s].commit_lsn] + IN + [broker_state EXCEPT ![b].sk = updbsk] + ELSE broker_state + /\ UNCHANGED <> + +PsRecvBroker(b,p,s) == + /\ LET + bsk == broker_state[b].sk[s] + psk == pageserver_state[p].sk[s] + updpsk == [psk EXCEPT !["commit_lsn"] = bsk.commit_lsn] + IN + pageserver_state' = IF bsk.commit_lsn > psk.commit_lsn + THEN [pageserver_state EXCEPT ![p].sk[s] = updpsk] + ELSE pageserver_state + /\ UNCHANGED <> + + +SksWithNewerWal(p) == + LET + ps == pageserver_state[p] + IN + {s \in DOMAIN ps.sk: ps.sk[s].commit_lsn > ps.last_record_lsn} + +PsChooseSk(p) == + /\ SksWithNewerWal(p) # {} + /\ pageserver_state' = [pageserver_state EXCEPT![p].preferred_sk = CHOOSE s \in SksWithNewerWal(p): TRUE] + /\ UNCHANGED <> + + +Next == + + \/ \E s1 \in safekeepers: \E s2 \in safekeepers: + \/ SkCommit(s1, s2) + \/ SkPeerRecovery(s1, s2) + \/ \E s \in safekeepers: \E b \in brokers: SkPushToBroker(s, b) + \/ \E s \in safekeepers: \E b \in brokers: \E p \in pageservers: PsRecvBroker(b,p,s) + \/ \E p \in pageservers: PsChooseSk(p) + + +Spec == Init /\ [][Next]_<< broker_state, safekeeper_state, pageserver_state >> + + +\* invariants + +EventuallyLaggingSkIsNotPreferredSk == <>( + LET + sks == safekeeper_state + lagging_sks == { s \in safekeepers: \A s2 \in safekeepers: sks[s].commit_lsn <= sks[s2].commit_lsn } + preferred_sks == {pageserver_state[p].preferred_sk: p \in pageservers} + IN + preferred_sks \cap lagging_sks = {} + + ) + + + +==== \ No newline at end of file diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299469039/MC.cfg b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299469039/MC.cfg new file mode 100644 index 0000000000..3de9dad2e7 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299469039/MC.cfg @@ -0,0 +1,51 @@ +\* MV CONSTANT declarations +CONSTANTS +b1 = b1 +b2 = b2 +b3 = b3 +\* MV CONSTANT declarations +CONSTANTS +s1 = s1 +s2 = s2 +s3 = s3 +\* MV CONSTANT declarations +CONSTANTS +p1 = p1 +p2 = p2 +\* MV CONSTANT declarations +CONSTANTS +az1 = az1 +az2 = az2 +az3 = az3 +\* MV CONSTANT definitions +CONSTANT +brokers <- const_1737299464992221000 +\* CONSTANT declarations +CONSTANT NULL = NULL +\* MV CONSTANT definitions +CONSTANT +safekeepers <- const_1737299464992222000 +\* MV CONSTANT definitions +CONSTANT +pageservers <- const_1737299464992223000 +\* MV CONSTANT definitions +CONSTANT +azs <- const_1737299464992224000 +\* SYMMETRY definition +SYMMETRY symm_1737299464992225000 +\* CONSTANT definitions +CONSTANT +max_commit_lsn <- const_1737299464992226000 +\* CONSTANT definitions +CONSTANT +az_mapping <- const_1737299464992227000 +\* CONSTRAINT definition +CONSTRAINT +constr_1737299464992228000 +\* SPECIFICATION definition +SPECIFICATION +Spec +\* PROPERTY definition +PROPERTY +EventuallyLaggingSkIsNotPreferredSk +\* Generated on Sun Jan 19 16:11:04 CET 2025 \ No newline at end of file diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299469039/MC.out b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299469039/MC.out new file mode 100644 index 0000000000..3299ac8cfa --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299469039/MC.out @@ -0,0 +1,202 @@ +@!@!@STARTMSG 2262:0 @!@!@ +TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802) +@!@!@ENDMSG 2262 @!@!@ +@!@!@STARTMSG 2187:0 @!@!@ +Running breadth-first search Model-Checking with fp 105 and seed 4277674636266930199 with 4 workers on 8 cores with 2428MB heap and 5460MB offheap memory [pid: 7749] (Mac OS X 10.16 x86_64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue). +@!@!@ENDMSG 2187 @!@!@ +@!@!@STARTMSG 2220:0 @!@!@ +Starting SANY... +@!@!@ENDMSG 2220 @!@!@ +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/MC.tla +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/fullmesh.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/TLC.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Integers.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Naturals.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Sequences.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/FiniteSets.tla +Semantic processing of module Naturals +Semantic processing of module Integers +Semantic processing of module fullmesh +Semantic processing of module Sequences +Semantic processing of module FiniteSets +Semantic processing of module TLC +Semantic processing of module MC +@!@!@STARTMSG 2219:0 @!@!@ +SANY finished. +@!@!@ENDMSG 2219 @!@!@ +@!@!@STARTMSG 2185:0 @!@!@ +Starting... (2025-01-19 16:11:06) +@!@!@ENDMSG 2185 @!@!@ +@!@!@STARTMSG 2279:3 @!@!@ +Declaring symmetry during liveness checking is dangerous. It might cause TLC to miss violations of the stated liveness properties. Please check liveness without symmetry defined. +@!@!@ENDMSG 2279 @!@!@ +@!@!@STARTMSG 2284:3 @!@!@ +Declaring state or action constraints during liveness checking is dangerous: Please read section 14.3.5 on page 247 of Specifying Systems (https://lamport.azurewebsites.net/tla/book.html) and optionally the discussion at https://discuss.tlapl.us/msg00994.html for more details. +@!@!@ENDMSG 2284 @!@!@ +@!@!@STARTMSG 2212:0 @!@!@ +Implied-temporal checking--satisfiability problem has 1 branches. +@!@!@ENDMSG 2212 @!@!@ +@!@!@STARTMSG 2189:0 @!@!@ +Computing initial states... +@!@!@ENDMSG 2189 @!@!@ +@!@!@STARTMSG 2190:0 @!@!@ +Finished computing initial states: 1 distinct state generated at 2025-01-19 16:11:07. +@!@!@ENDMSG 2190 @!@!@ +@!@!@STARTMSG 2109:1 @!@!@ +Successor state is not completely specified by action SkPeerRecovery of the next-state relation. The following variables are not assigned: broker_state, pageserver_state. + +@!@!@ENDMSG 2109 @!@!@ +@!@!@STARTMSG 2121:1 @!@!@ +The behavior up to this point is: +@!@!@ENDMSG 2121 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +1: +/\ pageserver_state = (p1 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0]), last_record_lsn |-> 0, preferred_sk |-> NULL] @@ p2 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0]), last_record_lsn |-> 0, preferred_sk |-> NULL]) +/\ broker_state = (b1 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])] @@ b2 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])] @@ b3 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])]) +/\ safekeeper_state = (s1 :> [commit_lsn |-> 0, pruned_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0, pruned_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0, pruned_lsn |-> 0]) + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +2: +/\ pageserver_state = (p1 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0]), last_record_lsn |-> 0, preferred_sk |-> NULL] @@ p2 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0]), last_record_lsn |-> 0, preferred_sk |-> NULL]) +/\ broker_state = (b1 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])] @@ b2 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])] @@ b3 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])]) +/\ safekeeper_state = (s1 :> [commit_lsn |-> 1, pruned_lsn |-> 0] @@ s2 :> [commit_lsn |-> 1, pruned_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0, pruned_lsn |-> 0]) + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +3: +/\ pageserver_state = (p1 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0]), last_record_lsn |-> 0, preferred_sk |-> NULL] @@ p2 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0]), last_record_lsn |-> 0, preferred_sk |-> NULL]) +/\ broker_state = (b1 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])] @@ b2 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])] @@ b3 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])]) +/\ safekeeper_state = (s1 :> [commit_lsn |-> 2, pruned_lsn |-> 0] @@ s2 :> [commit_lsn |-> 2, pruned_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0, pruned_lsn |-> 0]) + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +4: +/\ pageserver_state = null +/\ broker_state = null +/\ safekeeper_state = (s1 :> [commit_lsn |-> 2, pruned_lsn |-> 0] @@ s2 :> [commit_lsn |-> 2, pruned_lsn |-> 0] @@ s3 :> [commit_lsn |-> 2, pruned_lsn |-> 0]) + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2201:0 @!@!@ +The coverage statistics at 2025-01-19 16:11:07 +@!@!@ENDMSG 2201 @!@!@ +@!@!@STARTMSG 2773:0 @!@!@ +: 2:2 +@!@!@ENDMSG 2773 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 34, col 5 to line 36, col 64 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 2:14 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 40, col 8 to line 40, col 14 of module fullmesh: 48 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 40, col 8 to line 40, col 9 of module fullmesh: 34 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 40, col 13 to line 40, col 14 of module fullmesh: 34 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 41, col 8 to line 41, col 72 of module fullmesh: 37 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 41, col 8 to line 41, col 38 of module fullmesh: 23 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 41, col 42 to line 41, col 72 of module fullmesh: 23 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 45, col 13 to line 47, col 50 of module fullmesh: 14 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 48, col 8 to line 48, col 51 of module fullmesh: 14 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 0:3 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 51, col 8 to line 51, col 72 of module fullmesh: 1 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 51, col 8 to line 51, col 38 of module fullmesh: 32 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 51, col 42 to line 51, col 72 of module fullmesh: 32 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 52, col 8 to line 52, col 102 of module fullmesh: 1 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 52, col 28 to line 52, col 102 of module fullmesh: 3 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 0:9 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 55, col 8 to line 62, col 29 of module fullmesh: 9 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 63, col 8 to line 63, col 55 of module fullmesh: 9 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 0:18 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 71, col 13 to line 73, col 37 of module fullmesh: 18 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 74, col 8 to line 74, col 51 of module fullmesh: 18 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 0:0 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 84, col 8 to line 84, col 30 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 84, col 8 to line 84, col 25 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 79, col 15 to line 79, col 33 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 81, col 5 to line 81, col 66 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 81, col 26 to line 81, col 65 of module fullmesh: 6 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 81, col 12 to line 81, col 23 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 84, col 24 to line 84, col 24 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 84, col 29 to line 84, col 30 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 85, col 8 to line 85, col 109 of module fullmesh: 0 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 86, col 8 to line 86, col 51 of module fullmesh: 0 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2202:0 @!@!@ +End of statistics. +@!@!@ENDMSG 2202 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(3) at 2025-01-19 16:11:07: 40 states generated (992 s/min), 3 distinct states found (74 ds/min), 0 states left on queue. +@!@!@ENDMSG 2200 @!@!@ +@!@!@STARTMSG 2199:0 @!@!@ +40 states generated, 3 distinct states found, 0 states left on queue. +@!@!@ENDMSG 2199 @!@!@ +@!@!@STARTMSG 2194:0 @!@!@ +The depth of the complete state graph search is 3. +@!@!@ENDMSG 2194 @!@!@ +@!@!@STARTMSG 2268:0 @!@!@ +The average outdegree of the complete state graph is 1 (minimum is 1, the maximum 1 and the 95th percentile is 1). +@!@!@ENDMSG 2268 @!@!@ +@!@!@STARTMSG 2186:0 @!@!@ +Finished in 2440ms at (2025-01-19 16:11:07) +@!@!@ENDMSG 2186 @!@!@ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299469039/MC.tla b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299469039/MC.tla new file mode 100644 index 0000000000..eceb21dd0b --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299469039/MC.tla @@ -0,0 +1,65 @@ +---- MODULE MC ---- +EXTENDS fullmesh, TLC + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +b1, b2, b3 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +s1, s2, s3 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +p1, p2 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +az1, az2, az3 +---- + +\* MV CONSTANT definitions brokers +const_1737299464992221000 == +{b1, b2, b3} +---- + +\* MV CONSTANT definitions safekeepers +const_1737299464992222000 == +{s1, s2, s3} +---- + +\* MV CONSTANT definitions pageservers +const_1737299464992223000 == +{p1, p2} +---- + +\* MV CONSTANT definitions azs +const_1737299464992224000 == +{az1, az2, az3} +---- + +\* SYMMETRY definition +symm_1737299464992225000 == +Permutations(const_1737299464992221000) \union Permutations(const_1737299464992222000) \union Permutations(const_1737299464992223000) \union Permutations(const_1737299464992224000) +---- + +\* CONSTANT definitions @modelParameterConstants:4max_commit_lsn +const_1737299464992226000 == +2 +---- + +\* CONSTANT definitions @modelParameterConstants:5az_mapping +const_1737299464992227000 == +[ az1 |-> {b1,s1,p1} , az2 |-> {b2,s2,p2} , az3 |-> {b3,s3}] +---- + +\* CONSTRAINT definition @modelParameterContraint:0 +constr_1737299464992228000 == +StateConstraint +---- +============================================================================= +\* Modification History +\* Created Sun Jan 19 16:11:04 CET 2025 by cs diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299469039/MC_TE.out b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299469039/MC_TE.out new file mode 100644 index 0000000000..3299ac8cfa --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299469039/MC_TE.out @@ -0,0 +1,202 @@ +@!@!@STARTMSG 2262:0 @!@!@ +TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802) +@!@!@ENDMSG 2262 @!@!@ +@!@!@STARTMSG 2187:0 @!@!@ +Running breadth-first search Model-Checking with fp 105 and seed 4277674636266930199 with 4 workers on 8 cores with 2428MB heap and 5460MB offheap memory [pid: 7749] (Mac OS X 10.16 x86_64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue). +@!@!@ENDMSG 2187 @!@!@ +@!@!@STARTMSG 2220:0 @!@!@ +Starting SANY... +@!@!@ENDMSG 2220 @!@!@ +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/MC.tla +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/fullmesh.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/TLC.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Integers.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Naturals.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Sequences.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/FiniteSets.tla +Semantic processing of module Naturals +Semantic processing of module Integers +Semantic processing of module fullmesh +Semantic processing of module Sequences +Semantic processing of module FiniteSets +Semantic processing of module TLC +Semantic processing of module MC +@!@!@STARTMSG 2219:0 @!@!@ +SANY finished. +@!@!@ENDMSG 2219 @!@!@ +@!@!@STARTMSG 2185:0 @!@!@ +Starting... (2025-01-19 16:11:06) +@!@!@ENDMSG 2185 @!@!@ +@!@!@STARTMSG 2279:3 @!@!@ +Declaring symmetry during liveness checking is dangerous. It might cause TLC to miss violations of the stated liveness properties. Please check liveness without symmetry defined. +@!@!@ENDMSG 2279 @!@!@ +@!@!@STARTMSG 2284:3 @!@!@ +Declaring state or action constraints during liveness checking is dangerous: Please read section 14.3.5 on page 247 of Specifying Systems (https://lamport.azurewebsites.net/tla/book.html) and optionally the discussion at https://discuss.tlapl.us/msg00994.html for more details. +@!@!@ENDMSG 2284 @!@!@ +@!@!@STARTMSG 2212:0 @!@!@ +Implied-temporal checking--satisfiability problem has 1 branches. +@!@!@ENDMSG 2212 @!@!@ +@!@!@STARTMSG 2189:0 @!@!@ +Computing initial states... +@!@!@ENDMSG 2189 @!@!@ +@!@!@STARTMSG 2190:0 @!@!@ +Finished computing initial states: 1 distinct state generated at 2025-01-19 16:11:07. +@!@!@ENDMSG 2190 @!@!@ +@!@!@STARTMSG 2109:1 @!@!@ +Successor state is not completely specified by action SkPeerRecovery of the next-state relation. The following variables are not assigned: broker_state, pageserver_state. + +@!@!@ENDMSG 2109 @!@!@ +@!@!@STARTMSG 2121:1 @!@!@ +The behavior up to this point is: +@!@!@ENDMSG 2121 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +1: +/\ pageserver_state = (p1 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0]), last_record_lsn |-> 0, preferred_sk |-> NULL] @@ p2 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0]), last_record_lsn |-> 0, preferred_sk |-> NULL]) +/\ broker_state = (b1 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])] @@ b2 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])] @@ b3 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])]) +/\ safekeeper_state = (s1 :> [commit_lsn |-> 0, pruned_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0, pruned_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0, pruned_lsn |-> 0]) + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +2: +/\ pageserver_state = (p1 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0]), last_record_lsn |-> 0, preferred_sk |-> NULL] @@ p2 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0]), last_record_lsn |-> 0, preferred_sk |-> NULL]) +/\ broker_state = (b1 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])] @@ b2 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])] @@ b3 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])]) +/\ safekeeper_state = (s1 :> [commit_lsn |-> 1, pruned_lsn |-> 0] @@ s2 :> [commit_lsn |-> 1, pruned_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0, pruned_lsn |-> 0]) + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +3: +/\ pageserver_state = (p1 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0]), last_record_lsn |-> 0, preferred_sk |-> NULL] @@ p2 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0]), last_record_lsn |-> 0, preferred_sk |-> NULL]) +/\ broker_state = (b1 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])] @@ b2 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])] @@ b3 :> [sk |-> (s1 :> [commit_lsn |-> 0] @@ s2 :> [commit_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0])]) +/\ safekeeper_state = (s1 :> [commit_lsn |-> 2, pruned_lsn |-> 0] @@ s2 :> [commit_lsn |-> 2, pruned_lsn |-> 0] @@ s3 :> [commit_lsn |-> 0, pruned_lsn |-> 0]) + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +4: +/\ pageserver_state = null +/\ broker_state = null +/\ safekeeper_state = (s1 :> [commit_lsn |-> 2, pruned_lsn |-> 0] @@ s2 :> [commit_lsn |-> 2, pruned_lsn |-> 0] @@ s3 :> [commit_lsn |-> 2, pruned_lsn |-> 0]) + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2201:0 @!@!@ +The coverage statistics at 2025-01-19 16:11:07 +@!@!@ENDMSG 2201 @!@!@ +@!@!@STARTMSG 2773:0 @!@!@ +: 2:2 +@!@!@ENDMSG 2773 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 34, col 5 to line 36, col 64 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 2:14 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 40, col 8 to line 40, col 14 of module fullmesh: 48 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 40, col 8 to line 40, col 9 of module fullmesh: 34 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 40, col 13 to line 40, col 14 of module fullmesh: 34 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 41, col 8 to line 41, col 72 of module fullmesh: 37 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 41, col 8 to line 41, col 38 of module fullmesh: 23 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 41, col 42 to line 41, col 72 of module fullmesh: 23 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 45, col 13 to line 47, col 50 of module fullmesh: 14 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 48, col 8 to line 48, col 51 of module fullmesh: 14 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 0:3 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 51, col 8 to line 51, col 72 of module fullmesh: 1 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 51, col 8 to line 51, col 38 of module fullmesh: 32 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 51, col 42 to line 51, col 72 of module fullmesh: 32 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 52, col 8 to line 52, col 102 of module fullmesh: 1 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 52, col 28 to line 52, col 102 of module fullmesh: 3 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 0:9 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 55, col 8 to line 62, col 29 of module fullmesh: 9 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 63, col 8 to line 63, col 55 of module fullmesh: 9 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 0:18 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 71, col 13 to line 73, col 37 of module fullmesh: 18 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 74, col 8 to line 74, col 51 of module fullmesh: 18 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 0:0 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 84, col 8 to line 84, col 30 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 84, col 8 to line 84, col 25 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 79, col 15 to line 79, col 33 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 81, col 5 to line 81, col 66 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 81, col 26 to line 81, col 65 of module fullmesh: 6 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 81, col 12 to line 81, col 23 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 84, col 24 to line 84, col 24 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 84, col 29 to line 84, col 30 of module fullmesh: 2 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 85, col 8 to line 85, col 109 of module fullmesh: 0 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 86, col 8 to line 86, col 51 of module fullmesh: 0 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2202:0 @!@!@ +End of statistics. +@!@!@ENDMSG 2202 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(3) at 2025-01-19 16:11:07: 40 states generated (992 s/min), 3 distinct states found (74 ds/min), 0 states left on queue. +@!@!@ENDMSG 2200 @!@!@ +@!@!@STARTMSG 2199:0 @!@!@ +40 states generated, 3 distinct states found, 0 states left on queue. +@!@!@ENDMSG 2199 @!@!@ +@!@!@STARTMSG 2194:0 @!@!@ +The depth of the complete state graph search is 3. +@!@!@ENDMSG 2194 @!@!@ +@!@!@STARTMSG 2268:0 @!@!@ +The average outdegree of the complete state graph is 1 (minimum is 1, the maximum 1 and the 95th percentile is 1). +@!@!@ENDMSG 2268 @!@!@ +@!@!@STARTMSG 2186:0 @!@!@ +Finished in 2440ms at (2025-01-19 16:11:07) +@!@!@ENDMSG 2186 @!@!@ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299469039/fullmesh.tla b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299469039/fullmesh.tla new file mode 100644 index 0000000000..047ececfe2 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299469039/fullmesh.tla @@ -0,0 +1,116 @@ +---- MODULE fullmesh ---- + +EXTENDS Integers + +VARIABLES broker_state, safekeeper_state, pageserver_state + + +CONSTANT + brokers, + safekeepers, + pageservers, + azs, + az_mapping + +CONSTANT + NULL + +CONSTANT + max_commit_lsn + +StateConstraint == + /\ \A s \in safekeepers: + /\ safekeeper_state[s].commit_lsn <= max_commit_lsn + /\ \A b \in brokers: + /\ \A s \in DOMAIN broker_state[b].sk: + /\ broker_state[b].sk[s].commit_lsn <= max_commit_lsn + + +InitSafekeeper == [pruned_lsn |-> 0, commit_lsn |-> 0] +InitBroker == [sk |-> [s \in safekeepers |-> [commit_lsn |-> 0]]] +InitPageserver == [last_record_lsn |-> 0, preferred_sk |-> NULL, sk |-> [s \in safekeepers |-> [commit_lsn |-> 0]]] + +Init == + /\ broker_state = [b \in brokers |-> InitBroker] + /\ safekeeper_state = [s \in safekeepers |-> InitSafekeeper] + /\ pageserver_state = [p \in pageservers |-> InitPageserver] + + +SkCommit(s1, s2) == + /\ s1 # s2 + /\ safekeeper_state[s1].commit_lsn = safekeeper_state[s2].commit_lsn + /\ LET + new_commit_lsn == safekeeper_state[s1].commit_lsn + 1 + IN + safekeeper_state' = [safekeeper_state EXCEPT + ![s1].commit_lsn = new_commit_lsn, + ![s2].commit_lsn = new_commit_lsn] + /\ UNCHANGED <> + +SkPeerRecovery(s1,s2) == + /\ safekeeper_state[s1].commit_lsn < safekeeper_state[s2].commit_lsn + /\ safekeeper_state' = [safekeeper_state EXCEPT![s1].commit_lsn = safekeeper_state[s2].commit_lsn] + +SkPushToBroker(s,b) == + /\ broker_state' = IF broker_state[b].sk[s].commit_lsn < safekeeper_state[s].commit_lsn + THEN + LET + bsk == broker_state[b].sk + updbsk == [bsk EXCEPT ![s].commit_lsn = safekeeper_state[s].commit_lsn] + IN + [broker_state EXCEPT ![b].sk = updbsk] + ELSE broker_state + /\ UNCHANGED <> + +PsRecvBroker(b,p,s) == + /\ LET + bsk == broker_state[b].sk[s] + psk == pageserver_state[p].sk[s] + updpsk == [psk EXCEPT !["commit_lsn"] = bsk.commit_lsn] + IN + pageserver_state' = IF bsk.commit_lsn > psk.commit_lsn + THEN [pageserver_state EXCEPT ![p].sk[s] = updpsk] + ELSE pageserver_state + /\ UNCHANGED <> + + +SksWithNewerWal(p) == + LET + ps == pageserver_state[p] + IN + {s \in DOMAIN ps.sk: ps.sk[s].commit_lsn > ps.last_record_lsn} + +PsChooseSk(p) == + /\ SksWithNewerWal(p) # {} + /\ pageserver_state' = [pageserver_state EXCEPT![p].preferred_sk = CHOOSE s \in SksWithNewerWal(p): TRUE] + /\ UNCHANGED <> + + +Next == + + \/ \E s1 \in safekeepers: \E s2 \in safekeepers: + \/ SkCommit(s1, s2) + \/ SkPeerRecovery(s1, s2) + \/ \E s \in safekeepers: \E b \in brokers: SkPushToBroker(s, b) + \/ \E s \in safekeepers: \E b \in brokers: \E p \in pageservers: PsRecvBroker(b,p,s) + \/ \E p \in pageservers: PsChooseSk(p) + + +Spec == Init /\ [][Next]_<< broker_state, safekeeper_state, pageserver_state >> + + +\* invariants + +EventuallyLaggingSkIsNotPreferredSk == <>( + LET + sks == safekeeper_state + lagging_sks == { s \in safekeepers: \A s2 \in safekeepers: sks[s].commit_lsn <= sks[s2].commit_lsn } + preferred_sks == {pageserver_state[p].preferred_sk: p \in pageservers} + IN + preferred_sks \cap lagging_sks = {} + + ) + + + +==== \ No newline at end of file diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299542008/MC.cfg b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299542008/MC.cfg new file mode 100644 index 0000000000..85f59f2a5a --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299542008/MC.cfg @@ -0,0 +1,51 @@ +\* MV CONSTANT declarations +CONSTANTS +b1 = b1 +b2 = b2 +b3 = b3 +\* MV CONSTANT declarations +CONSTANTS +s1 = s1 +s2 = s2 +s3 = s3 +\* MV CONSTANT declarations +CONSTANTS +p1 = p1 +p2 = p2 +\* MV CONSTANT declarations +CONSTANTS +az1 = az1 +az2 = az2 +az3 = az3 +\* MV CONSTANT definitions +CONSTANT +brokers <- const_1737299528165230000 +\* CONSTANT declarations +CONSTANT NULL = NULL +\* MV CONSTANT definitions +CONSTANT +safekeepers <- const_1737299528166231000 +\* MV CONSTANT definitions +CONSTANT +pageservers <- const_1737299528166232000 +\* MV CONSTANT definitions +CONSTANT +azs <- const_1737299528166233000 +\* SYMMETRY definition +SYMMETRY symm_1737299528166234000 +\* CONSTANT definitions +CONSTANT +max_commit_lsn <- const_1737299528166235000 +\* CONSTANT definitions +CONSTANT +az_mapping <- const_1737299528166236000 +\* CONSTRAINT definition +CONSTRAINT +constr_1737299528166237000 +\* SPECIFICATION definition +SPECIFICATION +Spec +\* PROPERTY definition +PROPERTY +EventuallyLaggingSkIsNotPreferredSk +\* Generated on Sun Jan 19 16:12:08 CET 2025 \ No newline at end of file diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299542008/MC.out b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299542008/MC.out new file mode 100644 index 0000000000..50c1506166 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299542008/MC.out @@ -0,0 +1,57 @@ +@!@!@STARTMSG 2262:0 @!@!@ +TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802) +@!@!@ENDMSG 2262 @!@!@ +@!@!@STARTMSG 2187:0 @!@!@ +Running breadth-first search Model-Checking with fp 90 and seed -131482239732531000 with 4 workers on 8 cores with 2428MB heap and 5460MB offheap memory [pid: 7787] (Mac OS X 10.16 x86_64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue). +@!@!@ENDMSG 2187 @!@!@ +@!@!@STARTMSG 2220:0 @!@!@ +Starting SANY... +@!@!@ENDMSG 2220 @!@!@ +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/MC.tla +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/fullmesh.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/TLC.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Integers.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Naturals.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Sequences.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/FiniteSets.tla +Semantic processing of module Naturals +Semantic processing of module Integers +Semantic processing of module fullmesh +Semantic processing of module Sequences +Semantic processing of module FiniteSets +Semantic processing of module TLC +Semantic processing of module MC +@!@!@STARTMSG 2219:0 @!@!@ +SANY finished. +@!@!@ENDMSG 2219 @!@!@ +@!@!@STARTMSG 2185:0 @!@!@ +Starting... (2025-01-19 16:12:09) +@!@!@ENDMSG 2185 @!@!@ +@!@!@STARTMSG 2279:3 @!@!@ +Declaring symmetry during liveness checking is dangerous. It might cause TLC to miss violations of the stated liveness properties. Please check liveness without symmetry defined. +@!@!@ENDMSG 2279 @!@!@ +@!@!@STARTMSG 2284:3 @!@!@ +Declaring state or action constraints during liveness checking is dangerous: Please read section 14.3.5 on page 247 of Specifying Systems (https://lamport.azurewebsites.net/tla/book.html) and optionally the discussion at https://discuss.tlapl.us/msg00994.html for more details. +@!@!@ENDMSG 2284 @!@!@ +@!@!@STARTMSG 2212:0 @!@!@ +Implied-temporal checking--satisfiability problem has 1 branches. +@!@!@ENDMSG 2212 @!@!@ +@!@!@STARTMSG 2189:0 @!@!@ +Computing initial states... +@!@!@ENDMSG 2189 @!@!@ +@!@!@STARTMSG 2190:0 @!@!@ +Finished computing initial states: 1 distinct state generated at 2025-01-19 16:12:10. +@!@!@ENDMSG 2190 @!@!@ +@!@!@STARTMSG 2143:3 @!@!@ +The variable safekeeper_state was changed while it is specified as UNCHANGED at +line 53, col 34 to line 53, col 49 of module fullmesh +@!@!@ENDMSG 2143 @!@!@ +@!@!@STARTMSG 2192:0 @!@!@ +Checking temporal properties for the current state space with 1454 total distinct states at (2025-01-19 16:12:13) +@!@!@ENDMSG 2192 @!@!@ +@!@!@STARTMSG 2267:0 @!@!@ +Finished checking temporal properties in 00s at 2025-01-19 16:12:13 +@!@!@ENDMSG 2267 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(11) at 2025-01-19 16:12:13: 44.264 states generated (44.264 s/min), 2.994 distinct states found (2.994 ds/min), 1.536 states left on queue. +@!@!@ENDMSG 2200 @!@!@ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299542008/MC.tla b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299542008/MC.tla new file mode 100644 index 0000000000..c9a0a6f895 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299542008/MC.tla @@ -0,0 +1,65 @@ +---- MODULE MC ---- +EXTENDS fullmesh, TLC + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +b1, b2, b3 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +s1, s2, s3 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +p1, p2 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +az1, az2, az3 +---- + +\* MV CONSTANT definitions brokers +const_1737299528165230000 == +{b1, b2, b3} +---- + +\* MV CONSTANT definitions safekeepers +const_1737299528166231000 == +{s1, s2, s3} +---- + +\* MV CONSTANT definitions pageservers +const_1737299528166232000 == +{p1, p2} +---- + +\* MV CONSTANT definitions azs +const_1737299528166233000 == +{az1, az2, az3} +---- + +\* SYMMETRY definition +symm_1737299528166234000 == +Permutations(const_1737299528165230000) \union Permutations(const_1737299528166231000) \union Permutations(const_1737299528166232000) \union Permutations(const_1737299528166233000) +---- + +\* CONSTANT definitions @modelParameterConstants:4max_commit_lsn +const_1737299528166235000 == +2 +---- + +\* CONSTANT definitions @modelParameterConstants:5az_mapping +const_1737299528166236000 == +[ az1 |-> {b1,s1,p1} , az2 |-> {b2,s2,p2} , az3 |-> {b3,s3}] +---- + +\* CONSTRAINT definition @modelParameterContraint:0 +constr_1737299528166237000 == +StateConstraint +---- +============================================================================= +\* Modification History +\* Created Sun Jan 19 16:12:08 CET 2025 by cs diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299542008/MC_TE.out b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299542008/MC_TE.out new file mode 100644 index 0000000000..50c1506166 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299542008/MC_TE.out @@ -0,0 +1,57 @@ +@!@!@STARTMSG 2262:0 @!@!@ +TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802) +@!@!@ENDMSG 2262 @!@!@ +@!@!@STARTMSG 2187:0 @!@!@ +Running breadth-first search Model-Checking with fp 90 and seed -131482239732531000 with 4 workers on 8 cores with 2428MB heap and 5460MB offheap memory [pid: 7787] (Mac OS X 10.16 x86_64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue). +@!@!@ENDMSG 2187 @!@!@ +@!@!@STARTMSG 2220:0 @!@!@ +Starting SANY... +@!@!@ENDMSG 2220 @!@!@ +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/MC.tla +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/fullmesh.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/TLC.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Integers.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Naturals.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Sequences.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/FiniteSets.tla +Semantic processing of module Naturals +Semantic processing of module Integers +Semantic processing of module fullmesh +Semantic processing of module Sequences +Semantic processing of module FiniteSets +Semantic processing of module TLC +Semantic processing of module MC +@!@!@STARTMSG 2219:0 @!@!@ +SANY finished. +@!@!@ENDMSG 2219 @!@!@ +@!@!@STARTMSG 2185:0 @!@!@ +Starting... (2025-01-19 16:12:09) +@!@!@ENDMSG 2185 @!@!@ +@!@!@STARTMSG 2279:3 @!@!@ +Declaring symmetry during liveness checking is dangerous. It might cause TLC to miss violations of the stated liveness properties. Please check liveness without symmetry defined. +@!@!@ENDMSG 2279 @!@!@ +@!@!@STARTMSG 2284:3 @!@!@ +Declaring state or action constraints during liveness checking is dangerous: Please read section 14.3.5 on page 247 of Specifying Systems (https://lamport.azurewebsites.net/tla/book.html) and optionally the discussion at https://discuss.tlapl.us/msg00994.html for more details. +@!@!@ENDMSG 2284 @!@!@ +@!@!@STARTMSG 2212:0 @!@!@ +Implied-temporal checking--satisfiability problem has 1 branches. +@!@!@ENDMSG 2212 @!@!@ +@!@!@STARTMSG 2189:0 @!@!@ +Computing initial states... +@!@!@ENDMSG 2189 @!@!@ +@!@!@STARTMSG 2190:0 @!@!@ +Finished computing initial states: 1 distinct state generated at 2025-01-19 16:12:10. +@!@!@ENDMSG 2190 @!@!@ +@!@!@STARTMSG 2143:3 @!@!@ +The variable safekeeper_state was changed while it is specified as UNCHANGED at +line 53, col 34 to line 53, col 49 of module fullmesh +@!@!@ENDMSG 2143 @!@!@ +@!@!@STARTMSG 2192:0 @!@!@ +Checking temporal properties for the current state space with 1454 total distinct states at (2025-01-19 16:12:13) +@!@!@ENDMSG 2192 @!@!@ +@!@!@STARTMSG 2267:0 @!@!@ +Finished checking temporal properties in 00s at 2025-01-19 16:12:13 +@!@!@ENDMSG 2267 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(11) at 2025-01-19 16:12:13: 44.264 states generated (44.264 s/min), 2.994 distinct states found (2.994 ds/min), 1.536 states left on queue. +@!@!@ENDMSG 2200 @!@!@ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299542008/fullmesh.tla b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299542008/fullmesh.tla new file mode 100644 index 0000000000..06c69da79a --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299542008/fullmesh.tla @@ -0,0 +1,117 @@ +---- MODULE fullmesh ---- + +EXTENDS Integers + +VARIABLES broker_state, safekeeper_state, pageserver_state + + +CONSTANT + brokers, + safekeepers, + pageservers, + azs, + az_mapping + +CONSTANT + NULL + +CONSTANT + max_commit_lsn + +StateConstraint == + /\ \A s \in safekeepers: + /\ safekeeper_state[s].commit_lsn <= max_commit_lsn + /\ \A b \in brokers: + /\ \A s \in DOMAIN broker_state[b].sk: + /\ broker_state[b].sk[s].commit_lsn <= max_commit_lsn + + +InitSafekeeper == [pruned_lsn |-> 0, commit_lsn |-> 0] +InitBroker == [sk |-> [s \in safekeepers |-> [commit_lsn |-> 0]]] +InitPageserver == [last_record_lsn |-> 0, preferred_sk |-> NULL, sk |-> [s \in safekeepers |-> [commit_lsn |-> 0]]] + +Init == + /\ broker_state = [b \in brokers |-> InitBroker] + /\ safekeeper_state = [s \in safekeepers |-> InitSafekeeper] + /\ pageserver_state = [p \in pageservers |-> InitPageserver] + + +SkCommit(s1, s2) == + /\ s1 # s2 + /\ safekeeper_state[s1].commit_lsn = safekeeper_state[s2].commit_lsn + /\ LET + new_commit_lsn == safekeeper_state[s1].commit_lsn + 1 + IN + safekeeper_state' = [safekeeper_state EXCEPT + ![s1].commit_lsn = new_commit_lsn, + ![s2].commit_lsn = new_commit_lsn] + /\ UNCHANGED <> + +SkPeerRecovery(s1,s2) == + /\ safekeeper_state[s1].commit_lsn < safekeeper_state[s2].commit_lsn + /\ safekeeper_state' = [safekeeper_state EXCEPT![s1].commit_lsn = safekeeper_state[s2].commit_lsn] + /\ UNCHANGED <> + +SkPushToBroker(s,b) == + /\ broker_state' = IF broker_state[b].sk[s].commit_lsn < safekeeper_state[s].commit_lsn + THEN + LET + bsk == broker_state[b].sk + updbsk == [bsk EXCEPT ![s].commit_lsn = safekeeper_state[s].commit_lsn] + IN + [broker_state EXCEPT ![b].sk = updbsk] + ELSE broker_state + /\ UNCHANGED <> + +PsRecvBroker(b,p,s) == + /\ LET + bsk == broker_state[b].sk[s] + psk == pageserver_state[p].sk[s] + updpsk == [psk EXCEPT !["commit_lsn"] = bsk.commit_lsn] + IN + pageserver_state' = IF bsk.commit_lsn > psk.commit_lsn + THEN [pageserver_state EXCEPT ![p].sk[s] = updpsk] + ELSE pageserver_state + /\ UNCHANGED <> + + +SksWithNewerWal(p) == + LET + ps == pageserver_state[p] + IN + {s \in DOMAIN ps.sk: ps.sk[s].commit_lsn > ps.last_record_lsn} + +PsChooseSk(p) == + /\ SksWithNewerWal(p) # {} + /\ pageserver_state' = [pageserver_state EXCEPT![p].preferred_sk = CHOOSE s \in SksWithNewerWal(p): TRUE] + /\ UNCHANGED <> + + +Next == + + \/ \E s1 \in safekeepers: \E s2 \in safekeepers: + \/ SkCommit(s1, s2) + \/ SkPeerRecovery(s1, s2) + \/ \E s \in safekeepers: \E b \in brokers: SkPushToBroker(s, b) + \/ \E s \in safekeepers: \E b \in brokers: \E p \in pageservers: PsRecvBroker(b,p,s) + \/ \E p \in pageservers: PsChooseSk(p) + + +Spec == Init /\ [][Next]_<< broker_state, safekeeper_state, pageserver_state >> + + +\* invariants + +EventuallyLaggingSkIsNotPreferredSk == <>( + LET + sks == safekeeper_state + lagging_sks == { s \in safekeepers: \A s2 \in safekeepers: sks[s].commit_lsn <= sks[s2].commit_lsn } + preferred_sks == {pageserver_state[p].preferred_sk: p \in pageservers} + IN + preferred_sks \cap lagging_sks = {} + + ) + + + +==== \ No newline at end of file diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299744229/MC.cfg b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299744229/MC.cfg new file mode 100644 index 0000000000..a8b002b0f3 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299744229/MC.cfg @@ -0,0 +1,51 @@ +\* MV CONSTANT declarations +CONSTANTS +b1 = b1 +b2 = b2 +b3 = b3 +\* MV CONSTANT declarations +CONSTANTS +s1 = s1 +s2 = s2 +s3 = s3 +\* MV CONSTANT declarations +CONSTANTS +p1 = p1 +p2 = p2 +\* MV CONSTANT declarations +CONSTANTS +az1 = az1 +az2 = az2 +az3 = az3 +\* MV CONSTANT definitions +CONSTANT +brokers <- const_1737299548592239000 +\* CONSTANT declarations +CONSTANT NULL = NULL +\* MV CONSTANT definitions +CONSTANT +safekeepers <- const_1737299548592240000 +\* MV CONSTANT definitions +CONSTANT +pageservers <- const_1737299548592241000 +\* MV CONSTANT definitions +CONSTANT +azs <- const_1737299548592242000 +\* SYMMETRY definition +SYMMETRY symm_1737299548592243000 +\* CONSTANT definitions +CONSTANT +max_commit_lsn <- const_1737299548592244000 +\* CONSTANT definitions +CONSTANT +az_mapping <- const_1737299548592245000 +\* CONSTRAINT definition +CONSTRAINT +constr_1737299548592246000 +\* SPECIFICATION definition +SPECIFICATION +Spec +\* PROPERTY definition +PROPERTY +EventuallyLaggingSkIsNotPreferredSk +\* Generated on Sun Jan 19 16:12:28 CET 2025 \ No newline at end of file diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299744229/MC.out b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299744229/MC.out new file mode 100644 index 0000000000..071b6e732d --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299744229/MC.out @@ -0,0 +1,323 @@ +@!@!@STARTMSG 2262:0 @!@!@ +TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802) +@!@!@ENDMSG 2262 @!@!@ +@!@!@STARTMSG 2187:0 @!@!@ +Running breadth-first search Model-Checking with fp 7 and seed 1961239747497010948 with 4 workers on 8 cores with 2428MB heap and 5460MB offheap memory [pid: 7839] (Mac OS X 10.16 x86_64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue). +@!@!@ENDMSG 2187 @!@!@ +@!@!@STARTMSG 2220:0 @!@!@ +Starting SANY... +@!@!@ENDMSG 2220 @!@!@ +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/MC.tla +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/fullmesh.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/TLC.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Integers.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Naturals.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Sequences.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/FiniteSets.tla +Semantic processing of module Naturals +Semantic processing of module Integers +Semantic processing of module fullmesh +Semantic processing of module Sequences +Semantic processing of module FiniteSets +Semantic processing of module TLC +Semantic processing of module MC +@!@!@STARTMSG 2219:0 @!@!@ +SANY finished. +@!@!@ENDMSG 2219 @!@!@ +@!@!@STARTMSG 2185:0 @!@!@ +Starting... (2025-01-19 16:12:29) +@!@!@ENDMSG 2185 @!@!@ +@!@!@STARTMSG 2279:3 @!@!@ +Declaring symmetry during liveness checking is dangerous. It might cause TLC to miss violations of the stated liveness properties. Please check liveness without symmetry defined. +@!@!@ENDMSG 2279 @!@!@ +@!@!@STARTMSG 2284:3 @!@!@ +Declaring state or action constraints during liveness checking is dangerous: Please read section 14.3.5 on page 247 of Specifying Systems (https://lamport.azurewebsites.net/tla/book.html) and optionally the discussion at https://discuss.tlapl.us/msg00994.html for more details. +@!@!@ENDMSG 2284 @!@!@ +@!@!@STARTMSG 2212:0 @!@!@ +Implied-temporal checking--satisfiability problem has 1 branches. +@!@!@ENDMSG 2212 @!@!@ +@!@!@STARTMSG 2189:0 @!@!@ +Computing initial states... +@!@!@ENDMSG 2189 @!@!@ +@!@!@STARTMSG 2190:0 @!@!@ +Finished computing initial states: 1 distinct state generated at 2025-01-19 16:12:31. +@!@!@ENDMSG 2190 @!@!@ +@!@!@STARTMSG 2192:0 @!@!@ +Checking temporal properties for the current state space with 1175 total distinct states at (2025-01-19 16:12:34) +@!@!@ENDMSG 2192 @!@!@ +@!@!@STARTMSG 2267:0 @!@!@ +Finished checking temporal properties in 00s at 2025-01-19 16:12:34 +@!@!@ENDMSG 2267 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(11) at 2025-01-19 16:12:34: 38.396 states generated (38.396 s/min), 3.250 distinct states found (3.250 ds/min), 2.071 states left on queue. +@!@!@ENDMSG 2200 @!@!@ +@!@!@STARTMSG 2192:0 @!@!@ +Checking temporal properties for the current state space with 45381 total distinct states at (2025-01-19 16:13:34) +@!@!@ENDMSG 2192 @!@!@ +@!@!@STARTMSG 2267:0 @!@!@ +Finished checking temporal properties in 00s at 2025-01-19 16:13:34 +@!@!@ENDMSG 2267 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(15) at 2025-01-19 16:13:34: 1.510.623 states generated (1.472.227 s/min), 97.716 distinct states found (94.466 ds/min), 52.332 states left on queue. +@!@!@ENDMSG 2200 @!@!@ +@!@!@STARTMSG 2192:0 @!@!@ +Checking temporal properties for the current state space with 92513 total distinct states at (2025-01-19 16:14:34) +@!@!@ENDMSG 2192 @!@!@ +@!@!@STARTMSG 2267:0 @!@!@ +Finished checking temporal properties in 00s at 2025-01-19 16:14:34 +@!@!@ENDMSG 2267 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(16) at 2025-01-19 16:14:34: 3.093.230 states generated (1.582.607 s/min), 182.372 distinct states found (84.656 ds/min), 89.855 states left on queue. +@!@!@ENDMSG 2200 @!@!@ +@!@!@STARTMSG 2192:0 @!@!@ +Checking temporal properties for the current state space with 140861 total distinct states at (2025-01-19 16:15:34) +@!@!@ENDMSG 2192 @!@!@ +@!@!@STARTMSG 2267:0 @!@!@ +Finished checking temporal properties in 00s at 2025-01-19 16:15:34 +@!@!@ENDMSG 2267 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(17) at 2025-01-19 16:15:34: 4.742.508 states generated (1.649.278 s/min), 257.179 distinct states found (74.807 ds/min), 116.314 states left on queue. +@!@!@ENDMSG 2200 @!@!@ +@!@!@STARTMSG 2201:0 @!@!@ +The coverage statistics at 2025-01-19 16:15:34 +@!@!@ENDMSG 2201 @!@!@ +@!@!@STARTMSG 2773:0 @!@!@ +: 1:1 +@!@!@ENDMSG 2773 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 34, col 5 to line 36, col 64 of module fullmesh: 1 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 54:531874 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 40, col 8 to line 40, col 14 of module fullmesh: 1799789 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 40, col 8 to line 40, col 9 of module fullmesh: 1267920 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 40, col 13 to line 40, col 14 of module fullmesh: 1267920 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 41, col 8 to line 41, col 72 of module fullmesh: 1377160 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 41, col 8 to line 41, col 38 of module fullmesh: 845280 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 41, col 8 to line 41, col 27 of module fullmesh: 845280 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 41, col 8 to line 41, col 23 of module fullmesh: 845280 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 41, col 25 to line 41, col 26 of module fullmesh: 845280 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 41, col 42 to line 41, col 72 of module fullmesh: 845280 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 45, col 13 to line 47, col 50 of module fullmesh: 531880 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 48, col 8 to line 48, col 51 of module fullmesh: 531878 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 148:156702 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 51, col 8 to line 51, col 72 of module fullmesh: 156716 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 51, col 8 to line 51, col 38 of module fullmesh: 1267992 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 51, col 8 to line 51, col 27 of module fullmesh: 1267999 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 51, col 8 to line 51, col 23 of module fullmesh: 1268010 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 51, col 25 to line 51, col 26 of module fullmesh: 1268010 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 51, col 42 to line 51, col 72 of module fullmesh: 1268010 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 52, col 8 to line 52, col 102 of module fullmesh: 156720 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 53, col 8 to line 53, col 51 of module fullmesh: 156716 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 13409:1268009 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 56, col 8 to line 63, col 29 of module fullmesh: 1268023 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 56, col 24 to line 63, col 29 of module fullmesh: 1268028 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 56, col 27 to line 56, col 91 of module fullmesh: 1268028 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 56, col 27 to line 56, col 58 of module fullmesh: 1268028 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||||line 56, col 27 to line 56, col 47 of module fullmesh: 1268028 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||||line 56, col 27 to line 56, col 44 of module fullmesh: 1268028 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||||||line 56, col 27 to line 56, col 41 of module fullmesh: 1268028 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||||||line 56, col 27 to line 56, col 38 of module fullmesh: 1268028 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||||||line 56, col 40 to line 56, col 40 of module fullmesh: 1268028 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||||line 56, col 46 to line 56, col 46 of module fullmesh: 1268028 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 56, col 62 to line 56, col 91 of module fullmesh: 1268028 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 59, col 28 to line 59, col 45 of module fullmesh: 793908 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 59, col 28 to line 59, col 42 of module fullmesh: 793908 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 60, col 31 to line 60, col 91 of module fullmesh: 793908 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 60, col 32 to line 60, col 34 of module fullmesh: 793908 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 60, col 43 to line 60, col 90 of module fullmesh: 793906 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 62, col 17 to line 62, col 54 of module fullmesh: 793908 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 63, col 18 to line 63, col 29 of module fullmesh: 474120 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 64, col 8 to line 64, col 55 of module fullmesh: 1268023 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 130578:2536105 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 72, col 13 to line 74, col 37 of module fullmesh: 2536113 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 72, col 33 to line 74, col 37 of module fullmesh: 2536117 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 72, col 36 to line 72, col 66 of module fullmesh: 2536118 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 72, col 36 to line 72, col 49 of module fullmesh: 2536119 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 72, col 53 to line 72, col 66 of module fullmesh: 2536121 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||||line 72, col 53 to line 72, col 55 of module fullmesh: 2536122 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||||line 69, col 20 to line 69, col 44 of module fullmesh: 2536123 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||||||line 69, col 20 to line 69, col 41 of module fullmesh: 2536124 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||||||line 69, col 20 to line 69, col 38 of module fullmesh: 2536125 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||||||line 69, col 43 to line 69, col 43 of module fullmesh: 2536126 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 73, col 22 to line 73, col 66 of module fullmesh: 818090 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 74, col 22 to line 74, col 37 of module fullmesh: 1718038 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 75, col 8 to line 75, col 51 of module fullmesh: 2536113 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 113018:250807 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 85, col 8 to line 85, col 30 of module fullmesh: 532607 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 85, col 8 to line 85, col 25 of module fullmesh: 281798 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 80, col 15 to line 80, col 33 of module fullmesh: 281798 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 82, col 5 to line 82, col 66 of module fullmesh: 281798 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 82, col 26 to line 82, col 65 of module fullmesh: 845394 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 82, col 12 to line 82, col 23 of module fullmesh: 281798 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 85, col 24 to line 85, col 24 of module fullmesh: 281798 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 85, col 29 to line 85, col 30 of module fullmesh: 281800 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 86, col 8 to line 86, col 109 of module fullmesh: 250813 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 86, col 28 to line 86, col 109 of module fullmesh: 250815 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 86, col 29 to line 86, col 44 of module fullmesh: 250815 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 86, col 52 to line 86, col 108 of module fullmesh: 250807 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 86, col 72 to line 86, col 108 of module fullmesh: 250815 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 86, col 105 to line 86, col 108 of module fullmesh: 250814 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 86, col 85 to line 86, col 102 of module fullmesh: 250815 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||||line 80, col 15 to line 80, col 33 of module fullmesh: 250814 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2775:0 @!@!@ + ||||line 82, col 5 to line 82, col 66 of module fullmesh: 250814:250814 +@!@!@ENDMSG 2775 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||||line 82, col 26 to line 82, col 65 of module fullmesh: 752442 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||||line 82, col 12 to line 82, col 23 of module fullmesh: 250814 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||||line 86, col 101 to line 86, col 101 of module fullmesh: 250814 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 87, col 8 to line 87, col 51 of module fullmesh: 250807 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2202:0 @!@!@ +End of statistics. +@!@!@ENDMSG 2202 @!@!@ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299744229/MC.tla b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299744229/MC.tla new file mode 100644 index 0000000000..fc42ac157a --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299744229/MC.tla @@ -0,0 +1,65 @@ +---- MODULE MC ---- +EXTENDS fullmesh, TLC + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +b1, b2, b3 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +s1, s2, s3 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +p1, p2 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +az1, az2, az3 +---- + +\* MV CONSTANT definitions brokers +const_1737299548592239000 == +{b1, b2, b3} +---- + +\* MV CONSTANT definitions safekeepers +const_1737299548592240000 == +{s1, s2, s3} +---- + +\* MV CONSTANT definitions pageservers +const_1737299548592241000 == +{p1, p2} +---- + +\* MV CONSTANT definitions azs +const_1737299548592242000 == +{az1, az2, az3} +---- + +\* SYMMETRY definition +symm_1737299548592243000 == +Permutations(const_1737299548592239000) \union Permutations(const_1737299548592240000) \union Permutations(const_1737299548592241000) \union Permutations(const_1737299548592242000) +---- + +\* CONSTANT definitions @modelParameterConstants:4max_commit_lsn +const_1737299548592244000 == +2 +---- + +\* CONSTANT definitions @modelParameterConstants:5az_mapping +const_1737299548592245000 == +[ az1 |-> {b1,s1,p1} , az2 |-> {b2,s2,p2} , az3 |-> {b3,s3}] +---- + +\* CONSTRAINT definition @modelParameterContraint:0 +constr_1737299548592246000 == +StateConstraint +---- +============================================================================= +\* Modification History +\* Created Sun Jan 19 16:12:28 CET 2025 by cs diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299744229/MC_TE.out b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299744229/MC_TE.out new file mode 100644 index 0000000000..071b6e732d --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299744229/MC_TE.out @@ -0,0 +1,323 @@ +@!@!@STARTMSG 2262:0 @!@!@ +TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802) +@!@!@ENDMSG 2262 @!@!@ +@!@!@STARTMSG 2187:0 @!@!@ +Running breadth-first search Model-Checking with fp 7 and seed 1961239747497010948 with 4 workers on 8 cores with 2428MB heap and 5460MB offheap memory [pid: 7839] (Mac OS X 10.16 x86_64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue). +@!@!@ENDMSG 2187 @!@!@ +@!@!@STARTMSG 2220:0 @!@!@ +Starting SANY... +@!@!@ENDMSG 2220 @!@!@ +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/MC.tla +Parsing file /Users/cs/Desktop/broker/fullmesh/fullmesh.toolbox/Model_1/fullmesh.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/TLC.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Integers.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Naturals.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Sequences.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/FiniteSets.tla +Semantic processing of module Naturals +Semantic processing of module Integers +Semantic processing of module fullmesh +Semantic processing of module Sequences +Semantic processing of module FiniteSets +Semantic processing of module TLC +Semantic processing of module MC +@!@!@STARTMSG 2219:0 @!@!@ +SANY finished. +@!@!@ENDMSG 2219 @!@!@ +@!@!@STARTMSG 2185:0 @!@!@ +Starting... (2025-01-19 16:12:29) +@!@!@ENDMSG 2185 @!@!@ +@!@!@STARTMSG 2279:3 @!@!@ +Declaring symmetry during liveness checking is dangerous. It might cause TLC to miss violations of the stated liveness properties. Please check liveness without symmetry defined. +@!@!@ENDMSG 2279 @!@!@ +@!@!@STARTMSG 2284:3 @!@!@ +Declaring state or action constraints during liveness checking is dangerous: Please read section 14.3.5 on page 247 of Specifying Systems (https://lamport.azurewebsites.net/tla/book.html) and optionally the discussion at https://discuss.tlapl.us/msg00994.html for more details. +@!@!@ENDMSG 2284 @!@!@ +@!@!@STARTMSG 2212:0 @!@!@ +Implied-temporal checking--satisfiability problem has 1 branches. +@!@!@ENDMSG 2212 @!@!@ +@!@!@STARTMSG 2189:0 @!@!@ +Computing initial states... +@!@!@ENDMSG 2189 @!@!@ +@!@!@STARTMSG 2190:0 @!@!@ +Finished computing initial states: 1 distinct state generated at 2025-01-19 16:12:31. +@!@!@ENDMSG 2190 @!@!@ +@!@!@STARTMSG 2192:0 @!@!@ +Checking temporal properties for the current state space with 1175 total distinct states at (2025-01-19 16:12:34) +@!@!@ENDMSG 2192 @!@!@ +@!@!@STARTMSG 2267:0 @!@!@ +Finished checking temporal properties in 00s at 2025-01-19 16:12:34 +@!@!@ENDMSG 2267 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(11) at 2025-01-19 16:12:34: 38.396 states generated (38.396 s/min), 3.250 distinct states found (3.250 ds/min), 2.071 states left on queue. +@!@!@ENDMSG 2200 @!@!@ +@!@!@STARTMSG 2192:0 @!@!@ +Checking temporal properties for the current state space with 45381 total distinct states at (2025-01-19 16:13:34) +@!@!@ENDMSG 2192 @!@!@ +@!@!@STARTMSG 2267:0 @!@!@ +Finished checking temporal properties in 00s at 2025-01-19 16:13:34 +@!@!@ENDMSG 2267 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(15) at 2025-01-19 16:13:34: 1.510.623 states generated (1.472.227 s/min), 97.716 distinct states found (94.466 ds/min), 52.332 states left on queue. +@!@!@ENDMSG 2200 @!@!@ +@!@!@STARTMSG 2192:0 @!@!@ +Checking temporal properties for the current state space with 92513 total distinct states at (2025-01-19 16:14:34) +@!@!@ENDMSG 2192 @!@!@ +@!@!@STARTMSG 2267:0 @!@!@ +Finished checking temporal properties in 00s at 2025-01-19 16:14:34 +@!@!@ENDMSG 2267 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(16) at 2025-01-19 16:14:34: 3.093.230 states generated (1.582.607 s/min), 182.372 distinct states found (84.656 ds/min), 89.855 states left on queue. +@!@!@ENDMSG 2200 @!@!@ +@!@!@STARTMSG 2192:0 @!@!@ +Checking temporal properties for the current state space with 140861 total distinct states at (2025-01-19 16:15:34) +@!@!@ENDMSG 2192 @!@!@ +@!@!@STARTMSG 2267:0 @!@!@ +Finished checking temporal properties in 00s at 2025-01-19 16:15:34 +@!@!@ENDMSG 2267 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(17) at 2025-01-19 16:15:34: 4.742.508 states generated (1.649.278 s/min), 257.179 distinct states found (74.807 ds/min), 116.314 states left on queue. +@!@!@ENDMSG 2200 @!@!@ +@!@!@STARTMSG 2201:0 @!@!@ +The coverage statistics at 2025-01-19 16:15:34 +@!@!@ENDMSG 2201 @!@!@ +@!@!@STARTMSG 2773:0 @!@!@ +: 1:1 +@!@!@ENDMSG 2773 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 34, col 5 to line 36, col 64 of module fullmesh: 1 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 54:531874 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 40, col 8 to line 40, col 14 of module fullmesh: 1799789 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 40, col 8 to line 40, col 9 of module fullmesh: 1267920 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 40, col 13 to line 40, col 14 of module fullmesh: 1267920 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 41, col 8 to line 41, col 72 of module fullmesh: 1377160 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 41, col 8 to line 41, col 38 of module fullmesh: 845280 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 41, col 8 to line 41, col 27 of module fullmesh: 845280 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 41, col 8 to line 41, col 23 of module fullmesh: 845280 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 41, col 25 to line 41, col 26 of module fullmesh: 845280 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 41, col 42 to line 41, col 72 of module fullmesh: 845280 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 45, col 13 to line 47, col 50 of module fullmesh: 531880 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 48, col 8 to line 48, col 51 of module fullmesh: 531878 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 148:156702 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 51, col 8 to line 51, col 72 of module fullmesh: 156716 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 51, col 8 to line 51, col 38 of module fullmesh: 1267992 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 51, col 8 to line 51, col 27 of module fullmesh: 1267999 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 51, col 8 to line 51, col 23 of module fullmesh: 1268010 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 51, col 25 to line 51, col 26 of module fullmesh: 1268010 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 51, col 42 to line 51, col 72 of module fullmesh: 1268010 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 52, col 8 to line 52, col 102 of module fullmesh: 156720 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 53, col 8 to line 53, col 51 of module fullmesh: 156716 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 13409:1268009 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 56, col 8 to line 63, col 29 of module fullmesh: 1268023 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 56, col 24 to line 63, col 29 of module fullmesh: 1268028 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 56, col 27 to line 56, col 91 of module fullmesh: 1268028 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 56, col 27 to line 56, col 58 of module fullmesh: 1268028 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||||line 56, col 27 to line 56, col 47 of module fullmesh: 1268028 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||||line 56, col 27 to line 56, col 44 of module fullmesh: 1268028 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||||||line 56, col 27 to line 56, col 41 of module fullmesh: 1268028 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||||||line 56, col 27 to line 56, col 38 of module fullmesh: 1268028 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||||||line 56, col 40 to line 56, col 40 of module fullmesh: 1268028 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||||line 56, col 46 to line 56, col 46 of module fullmesh: 1268028 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 56, col 62 to line 56, col 91 of module fullmesh: 1268028 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 59, col 28 to line 59, col 45 of module fullmesh: 793908 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 59, col 28 to line 59, col 42 of module fullmesh: 793908 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 60, col 31 to line 60, col 91 of module fullmesh: 793908 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 60, col 32 to line 60, col 34 of module fullmesh: 793908 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 60, col 43 to line 60, col 90 of module fullmesh: 793906 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 62, col 17 to line 62, col 54 of module fullmesh: 793908 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 63, col 18 to line 63, col 29 of module fullmesh: 474120 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 64, col 8 to line 64, col 55 of module fullmesh: 1268023 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 130578:2536105 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 72, col 13 to line 74, col 37 of module fullmesh: 2536113 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 72, col 33 to line 74, col 37 of module fullmesh: 2536117 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 72, col 36 to line 72, col 66 of module fullmesh: 2536118 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 72, col 36 to line 72, col 49 of module fullmesh: 2536119 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 72, col 53 to line 72, col 66 of module fullmesh: 2536121 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||||line 72, col 53 to line 72, col 55 of module fullmesh: 2536122 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||||line 69, col 20 to line 69, col 44 of module fullmesh: 2536123 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||||||line 69, col 20 to line 69, col 41 of module fullmesh: 2536124 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||||||line 69, col 20 to line 69, col 38 of module fullmesh: 2536125 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||||||line 69, col 43 to line 69, col 43 of module fullmesh: 2536126 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 73, col 22 to line 73, col 66 of module fullmesh: 818090 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 74, col 22 to line 74, col 37 of module fullmesh: 1718038 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 75, col 8 to line 75, col 51 of module fullmesh: 2536113 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2772:0 @!@!@ +: 113018:250807 +@!@!@ENDMSG 2772 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 85, col 8 to line 85, col 30 of module fullmesh: 532607 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 85, col 8 to line 85, col 25 of module fullmesh: 281798 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 80, col 15 to line 80, col 33 of module fullmesh: 281798 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 82, col 5 to line 82, col 66 of module fullmesh: 281798 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 82, col 26 to line 82, col 65 of module fullmesh: 845394 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 82, col 12 to line 82, col 23 of module fullmesh: 281798 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 85, col 24 to line 85, col 24 of module fullmesh: 281798 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 85, col 29 to line 85, col 30 of module fullmesh: 281800 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 86, col 8 to line 86, col 109 of module fullmesh: 250813 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |line 86, col 28 to line 86, col 109 of module fullmesh: 250815 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 86, col 29 to line 86, col 44 of module fullmesh: 250815 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 86, col 52 to line 86, col 108 of module fullmesh: 250807 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||line 86, col 72 to line 86, col 108 of module fullmesh: 250815 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 86, col 105 to line 86, col 108 of module fullmesh: 250814 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||line 86, col 85 to line 86, col 102 of module fullmesh: 250815 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||||line 80, col 15 to line 80, col 33 of module fullmesh: 250814 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2775:0 @!@!@ + ||||line 82, col 5 to line 82, col 66 of module fullmesh: 250814:250814 +@!@!@ENDMSG 2775 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||||line 82, col 26 to line 82, col 65 of module fullmesh: 752442 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + |||||line 82, col 12 to line 82, col 23 of module fullmesh: 250814 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + ||||line 86, col 101 to line 86, col 101 of module fullmesh: 250814 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2221:0 @!@!@ + line 87, col 8 to line 87, col 51 of module fullmesh: 250807 +@!@!@ENDMSG 2221 @!@!@ +@!@!@STARTMSG 2202:0 @!@!@ +End of statistics. +@!@!@ENDMSG 2202 @!@!@ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299744229/fullmesh.tla b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299744229/fullmesh.tla new file mode 100644 index 0000000000..b010e35f80 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737299744229/fullmesh.tla @@ -0,0 +1,117 @@ +---- MODULE fullmesh ---- + +EXTENDS Integers + +VARIABLES broker_state, safekeeper_state, pageserver_state + + +CONSTANT + brokers, + safekeepers, + pageservers, + azs, + az_mapping + +CONSTANT + NULL + +CONSTANT + max_commit_lsn + +StateConstraint == + /\ \A s \in safekeepers: + /\ safekeeper_state[s].commit_lsn <= max_commit_lsn + /\ \A b \in brokers: + /\ \A s \in DOMAIN broker_state[b].sk: + /\ broker_state[b].sk[s].commit_lsn <= max_commit_lsn + + +InitSafekeeper == [pruned_lsn |-> 0, commit_lsn |-> 0] +InitBroker == [sk |-> [s \in safekeepers |-> [commit_lsn |-> 0]]] +InitPageserver == [last_record_lsn |-> 0, preferred_sk |-> NULL, sk |-> [s \in safekeepers |-> [commit_lsn |-> 0]]] + +Init == + /\ broker_state = [b \in brokers |-> InitBroker] + /\ safekeeper_state = [s \in safekeepers |-> InitSafekeeper] + /\ pageserver_state = [p \in pageservers |-> InitPageserver] + + +SkCommit(s1, s2) == + /\ s1 # s2 + /\ safekeeper_state[s1].commit_lsn = safekeeper_state[s2].commit_lsn + /\ LET + new_commit_lsn == safekeeper_state[s1].commit_lsn + 1 + IN + safekeeper_state' = [safekeeper_state EXCEPT + ![s1].commit_lsn = new_commit_lsn, + ![s2].commit_lsn = new_commit_lsn] + /\ UNCHANGED <> + +SkPeerRecovery(s1,s2) == + /\ safekeeper_state[s1].commit_lsn < safekeeper_state[s2].commit_lsn + /\ safekeeper_state' = [safekeeper_state EXCEPT![s1].commit_lsn = safekeeper_state[s2].commit_lsn] + /\ UNCHANGED <> + +SkPushToBroker(s,b) == + /\ broker_state' = IF broker_state[b].sk[s].commit_lsn < safekeeper_state[s].commit_lsn + THEN + LET + bsk == broker_state[b].sk + updbsk == [bsk EXCEPT ![s].commit_lsn = safekeeper_state[s].commit_lsn] + IN + [broker_state EXCEPT ![b].sk = updbsk] + ELSE broker_state + /\ UNCHANGED <> + +PsRecvBroker(b,p,s) == + /\ LET + bsk == broker_state[b].sk[s] + psk == pageserver_state[p].sk[s] + updpsk == [psk EXCEPT !["commit_lsn"] = bsk.commit_lsn] + IN + pageserver_state' = IF bsk.commit_lsn > psk.commit_lsn + THEN [pageserver_state EXCEPT ![p].sk[s] = updpsk] + ELSE pageserver_state + /\ UNCHANGED <> + + +SksWithNewerWal(p) == + LET + ps == pageserver_state[p] + IN + {s \in DOMAIN ps.sk: ps.sk[s].commit_lsn > ps.last_record_lsn} + +PsChooseSk(p) == + /\ SksWithNewerWal(p) # {} + /\ pageserver_state' = [pageserver_state EXCEPT![p].preferred_sk = CHOOSE s \in SksWithNewerWal(p): TRUE] + /\ UNCHANGED <> + + +Next == + + \/ \E s1 \in safekeepers: \E s2 \in safekeepers: + \/ SkCommit(s1, s2) + \/ SkPeerRecovery(s1, s2) + \/ \E s \in safekeepers: \E b \in brokers: SkPushToBroker(s, b) + \/ \E s \in safekeepers: \E b \in brokers: \E p \in pageservers: PsRecvBroker(b,p,s) + \/ \E p \in pageservers: PsChooseSk(p) + + +Spec == Init /\ [][Next]_<< broker_state, safekeeper_state, pageserver_state >> + + +\* invariants + +EventuallyLaggingSkIsNotPreferredSk == <>( + LET + sks == safekeeper_state + lagging_sks == { s \in safekeepers: \A s2 \in safekeepers: sks[s].commit_lsn <= sks[s2].commit_lsn } + preferred_sks == {pageserver_state[p].preferred_sk: p \in pageservers} + IN + preferred_sks \cap lagging_sks = {} + + ) + + + +==== \ No newline at end of file diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301172627/MC.cfg b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301172627/MC.cfg new file mode 100644 index 0000000000..4963984e72 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301172627/MC.cfg @@ -0,0 +1,51 @@ +\* MV CONSTANT declarations +CONSTANTS +b1 = b1 +b2 = b2 +b3 = b3 +\* MV CONSTANT declarations +CONSTANTS +s1 = s1 +s2 = s2 +s3 = s3 +\* MV CONSTANT declarations +CONSTANTS +p1 = p1 +p2 = p2 +\* MV CONSTANT declarations +CONSTANTS +az1 = az1 +az2 = az2 +az3 = az3 +\* MV CONSTANT definitions +CONSTANT +brokers <- const_17373011685892000 +\* CONSTANT declarations +CONSTANT NULL = NULL +\* MV CONSTANT definitions +CONSTANT +safekeepers <- const_17373011685893000 +\* MV CONSTANT definitions +CONSTANT +pageservers <- const_17373011685894000 +\* MV CONSTANT definitions +CONSTANT +azs <- const_17373011685895000 +\* SYMMETRY definition +SYMMETRY symm_17373011685896000 +\* CONSTANT definitions +CONSTANT +max_commit_lsn <- const_17373011685897000 +\* CONSTANT definitions +CONSTANT +az_mapping <- const_17373011685898000 +\* CONSTRAINT definition +CONSTRAINT +constr_17373011685899000 +\* SPECIFICATION definition +SPECIFICATION +Spec +\* PROPERTY definition +PROPERTY +EventuallyLaggingSkIsNotPreferredSk +\* Generated on Sun Jan 19 16:39:28 CET 2025 \ No newline at end of file diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301172627/MC.out b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301172627/MC.out new file mode 100644 index 0000000000..32aec7b880 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301172627/MC.out @@ -0,0 +1,44 @@ +@!@!@STARTMSG 2262:0 @!@!@ +TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802) +@!@!@ENDMSG 2262 @!@!@ +@!@!@STARTMSG 2187:0 @!@!@ +Running breadth-first search Model-Checking with fp 71 and seed 2330797625274141225 with 4 workers on 8 cores with 2428MB heap and 5460MB offheap memory [pid: 9710] (Mac OS X 10.16 x86_64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue). +@!@!@ENDMSG 2187 @!@!@ +@!@!@STARTMSG 2220:0 @!@!@ +Starting SANY... +@!@!@ENDMSG 2220 @!@!@ +Parsing file /Users/cs/src/neon/storage_broker/spec/replicated/replicated.toolbox/Model_1/MC.tla +Parsing file /Users/cs/src/neon/storage_broker/spec/replicated/replicated.toolbox/Model_1/replicated.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/TLC.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Integers.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Naturals.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Sequences.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/FiniteSets.tla +Semantic processing of module Naturals +Semantic processing of module Integers +Semantic processing of module replicated +Semantic processing of module Sequences +Semantic processing of module FiniteSets +Semantic processing of module TLC +Semantic processing of module MC +@!@!@STARTMSG 2219:0 @!@!@ +SANY finished. +@!@!@ENDMSG 2219 @!@!@ +@!@!@STARTMSG 2185:0 @!@!@ +Starting... (2025-01-19 16:39:29) +@!@!@ENDMSG 2185 @!@!@ +@!@!@STARTMSG 2279:3 @!@!@ +Declaring symmetry during liveness checking is dangerous. It might cause TLC to miss violations of the stated liveness properties. Please check liveness without symmetry defined. +@!@!@ENDMSG 2279 @!@!@ +@!@!@STARTMSG 2284:3 @!@!@ +Declaring state or action constraints during liveness checking is dangerous: Please read section 14.3.5 on page 247 of Specifying Systems (https://lamport.azurewebsites.net/tla/book.html) and optionally the discussion at https://discuss.tlapl.us/msg00994.html for more details. +@!@!@ENDMSG 2284 @!@!@ +@!@!@STARTMSG 2212:0 @!@!@ +Implied-temporal checking--satisfiability problem has 1 branches. +@!@!@ENDMSG 2212 @!@!@ +@!@!@STARTMSG 2189:0 @!@!@ +Computing initial states... +@!@!@ENDMSG 2189 @!@!@ +@!@!@STARTMSG 2190:0 @!@!@ +Finished computing initial states: 1 distinct state generated at 2025-01-19 16:39:31. +@!@!@ENDMSG 2190 @!@!@ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301172627/MC.tla b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301172627/MC.tla new file mode 100644 index 0000000000..a2397f5d47 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301172627/MC.tla @@ -0,0 +1,65 @@ +---- MODULE MC ---- +EXTENDS replicated, TLC + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +b1, b2, b3 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +s1, s2, s3 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +p1, p2 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +az1, az2, az3 +---- + +\* MV CONSTANT definitions brokers +const_17373011685892000 == +{b1, b2, b3} +---- + +\* MV CONSTANT definitions safekeepers +const_17373011685893000 == +{s1, s2, s3} +---- + +\* MV CONSTANT definitions pageservers +const_17373011685894000 == +{p1, p2} +---- + +\* MV CONSTANT definitions azs +const_17373011685895000 == +{az1, az2, az3} +---- + +\* SYMMETRY definition +symm_17373011685896000 == +Permutations(const_17373011685892000) \union Permutations(const_17373011685893000) \union Permutations(const_17373011685894000) \union Permutations(const_17373011685895000) +---- + +\* CONSTANT definitions @modelParameterConstants:4max_commit_lsn +const_17373011685897000 == +2 +---- + +\* CONSTANT definitions @modelParameterConstants:5az_mapping +const_17373011685898000 == +[ az1 |-> {b1,s1,p1} , az2 |-> {b2,s2,p2} , az3 |-> {b3,s3}] +---- + +\* CONSTRAINT definition @modelParameterContraint:0 +constr_17373011685899000 == +StateConstraint +---- +============================================================================= +\* Modification History +\* Created Sun Jan 19 16:39:28 CET 2025 by cs diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301172627/MC_TE.out b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301172627/MC_TE.out new file mode 100644 index 0000000000..32aec7b880 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301172627/MC_TE.out @@ -0,0 +1,44 @@ +@!@!@STARTMSG 2262:0 @!@!@ +TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802) +@!@!@ENDMSG 2262 @!@!@ +@!@!@STARTMSG 2187:0 @!@!@ +Running breadth-first search Model-Checking with fp 71 and seed 2330797625274141225 with 4 workers on 8 cores with 2428MB heap and 5460MB offheap memory [pid: 9710] (Mac OS X 10.16 x86_64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue). +@!@!@ENDMSG 2187 @!@!@ +@!@!@STARTMSG 2220:0 @!@!@ +Starting SANY... +@!@!@ENDMSG 2220 @!@!@ +Parsing file /Users/cs/src/neon/storage_broker/spec/replicated/replicated.toolbox/Model_1/MC.tla +Parsing file /Users/cs/src/neon/storage_broker/spec/replicated/replicated.toolbox/Model_1/replicated.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/TLC.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Integers.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Naturals.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Sequences.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/FiniteSets.tla +Semantic processing of module Naturals +Semantic processing of module Integers +Semantic processing of module replicated +Semantic processing of module Sequences +Semantic processing of module FiniteSets +Semantic processing of module TLC +Semantic processing of module MC +@!@!@STARTMSG 2219:0 @!@!@ +SANY finished. +@!@!@ENDMSG 2219 @!@!@ +@!@!@STARTMSG 2185:0 @!@!@ +Starting... (2025-01-19 16:39:29) +@!@!@ENDMSG 2185 @!@!@ +@!@!@STARTMSG 2279:3 @!@!@ +Declaring symmetry during liveness checking is dangerous. It might cause TLC to miss violations of the stated liveness properties. Please check liveness without symmetry defined. +@!@!@ENDMSG 2279 @!@!@ +@!@!@STARTMSG 2284:3 @!@!@ +Declaring state or action constraints during liveness checking is dangerous: Please read section 14.3.5 on page 247 of Specifying Systems (https://lamport.azurewebsites.net/tla/book.html) and optionally the discussion at https://discuss.tlapl.us/msg00994.html for more details. +@!@!@ENDMSG 2284 @!@!@ +@!@!@STARTMSG 2212:0 @!@!@ +Implied-temporal checking--satisfiability problem has 1 branches. +@!@!@ENDMSG 2212 @!@!@ +@!@!@STARTMSG 2189:0 @!@!@ +Computing initial states... +@!@!@ENDMSG 2189 @!@!@ +@!@!@STARTMSG 2190:0 @!@!@ +Finished computing initial states: 1 distinct state generated at 2025-01-19 16:39:31. +@!@!@ENDMSG 2190 @!@!@ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301172627/replicated.tla b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301172627/replicated.tla new file mode 100644 index 0000000000..14910364fe --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301172627/replicated.tla @@ -0,0 +1,117 @@ +---- MODULE replicated ---- + +EXTENDS Integers + +VARIABLES broker_state, safekeeper_state, pageserver_state + + +CONSTANT + brokers, + safekeepers, + pageservers, + azs, + az_mapping + +CONSTANT + NULL + +CONSTANT + max_commit_lsn + +StateConstraint == + /\ \A s \in safekeepers: + /\ safekeeper_state[s].commit_lsn <= max_commit_lsn + /\ \A b \in brokers: + /\ \A s \in DOMAIN broker_state[b].sk: + /\ broker_state[b].sk[s].commit_lsn <= max_commit_lsn + + +InitSafekeeper == [pruned_lsn |-> 0, commit_lsn |-> 0] +InitBroker == [sk |-> [s \in safekeepers |-> [commit_lsn |-> 0]]] +InitPageserver == [last_record_lsn |-> 0, preferred_sk |-> NULL, sk |-> [s \in safekeepers |-> [commit_lsn |-> 0]]] + +Init == + /\ broker_state = [b \in brokers |-> InitBroker] + /\ safekeeper_state = [s \in safekeepers |-> InitSafekeeper] + /\ pageserver_state = [p \in pageservers |-> InitPageserver] + + +SkCommit(s1, s2) == + /\ s1 # s2 + /\ safekeeper_state[s1].commit_lsn = safekeeper_state[s2].commit_lsn + /\ LET + new_commit_lsn == safekeeper_state[s1].commit_lsn + 1 + IN + safekeeper_state' = [safekeeper_state EXCEPT + ![s1].commit_lsn = new_commit_lsn, + ![s2].commit_lsn = new_commit_lsn] + /\ UNCHANGED <> + +SkPeerRecovery(s1,s2) == + /\ safekeeper_state[s1].commit_lsn < safekeeper_state[s2].commit_lsn + /\ safekeeper_state' = [safekeeper_state EXCEPT![s1].commit_lsn = safekeeper_state[s2].commit_lsn] + /\ UNCHANGED <> + +SkPushToBroker(s,b) == + /\ broker_state' = IF broker_state[b].sk[s].commit_lsn < safekeeper_state[s].commit_lsn + THEN + LET + bsk == broker_state[b].sk + updbsk == [bsk EXCEPT ![s].commit_lsn = safekeeper_state[s].commit_lsn] + IN + [broker_state EXCEPT ![b].sk = updbsk] + ELSE broker_state + /\ UNCHANGED <> + +PsRecvBroker(b,p,s) == + /\ LET + bsk == broker_state[b].sk[s] + psk == pageserver_state[p].sk[s] + updpsk == [psk EXCEPT !["commit_lsn"] = bsk.commit_lsn] + IN + pageserver_state' = IF bsk.commit_lsn > psk.commit_lsn + THEN [pageserver_state EXCEPT ![p].sk[s] = updpsk] + ELSE pageserver_state + /\ UNCHANGED <> + + +SksWithNewerWal(p) == + LET + ps == pageserver_state[p] + IN + {s \in DOMAIN ps.sk: ps.sk[s].commit_lsn > ps.last_record_lsn} + +PsChooseSk(p) == + /\ SksWithNewerWal(p) # {} + /\ pageserver_state' = [pageserver_state EXCEPT![p].preferred_sk = CHOOSE s \in SksWithNewerWal(p): TRUE] + /\ UNCHANGED <> + + +Next == + + \/ \E s1 \in safekeepers: \E s2 \in safekeepers: + \/ SkCommit(s1, s2) + \/ SkPeerRecovery(s1, s2) + \/ \E s \in safekeepers: \E b \in brokers: SkPushToBroker(s, b) + \/ \E s \in safekeepers: \E b \in brokers: \E p \in pageservers: PsRecvBroker(b,p,s) + \/ \E p \in pageservers: PsChooseSk(p) + + +Spec == Init /\ [][Next]_<< broker_state, safekeeper_state, pageserver_state >> + + +\* invariants + +EventuallyLaggingSkIsNotPreferredSk == <>( + LET + sks == safekeeper_state + lagging_sks == { s \in safekeepers: \A s2 \in safekeepers: sks[s].commit_lsn <= sks[s2].commit_lsn } + preferred_sks == {pageserver_state[p].preferred_sk: p \in pageservers} + IN + preferred_sks \cap lagging_sks = {} + + ) + + + +==== \ No newline at end of file diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301223409/MC.cfg b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301223409/MC.cfg new file mode 100644 index 0000000000..1dcac21267 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301223409/MC.cfg @@ -0,0 +1,51 @@ +\* MV CONSTANT declarations +CONSTANTS +b1 = b1 +b2 = b2 +b3 = b3 +\* MV CONSTANT declarations +CONSTANTS +s1 = s1 +s2 = s2 +s3 = s3 +\* MV CONSTANT declarations +CONSTANTS +p1 = p1 +p2 = p2 +\* MV CONSTANT declarations +CONSTANTS +az1 = az1 +az2 = az2 +az3 = az3 +\* MV CONSTANT definitions +CONSTANT +brokers <- const_17373012151752000 +\* CONSTANT declarations +CONSTANT NULL = NULL +\* MV CONSTANT definitions +CONSTANT +safekeepers <- const_17373012151763000 +\* MV CONSTANT definitions +CONSTANT +pageservers <- const_17373012151764000 +\* MV CONSTANT definitions +CONSTANT +azs <- const_17373012151765000 +\* SYMMETRY definition +SYMMETRY symm_17373012151766000 +\* CONSTANT definitions +CONSTANT +max_commit_lsn <- const_17373012151767000 +\* CONSTANT definitions +CONSTANT +az_mapping <- const_17373012151768000 +\* CONSTRAINT definition +CONSTRAINT +constr_17373012151769000 +\* SPECIFICATION definition +SPECIFICATION +Spec +\* PROPERTY definition +PROPERTY +EventuallyLaggingSkIsNotPreferredSk +\* Generated on Sun Jan 19 16:40:15 CET 2025 \ No newline at end of file diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301223409/MC.out b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301223409/MC.out new file mode 100644 index 0000000000..ab92cbb3d7 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301223409/MC.out @@ -0,0 +1,53 @@ +@!@!@STARTMSG 2262:0 @!@!@ +TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802) +@!@!@ENDMSG 2262 @!@!@ +@!@!@STARTMSG 2187:0 @!@!@ +Running breadth-first search Model-Checking with fp 20 and seed 6372772458573668883 with 4 workers on 8 cores with 2428MB heap and 5460MB offheap memory [pid: 9898] (Mac OS X 10.16 x86_64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue). +@!@!@ENDMSG 2187 @!@!@ +@!@!@STARTMSG 2220:0 @!@!@ +Starting SANY... +@!@!@ENDMSG 2220 @!@!@ +Parsing file /Users/cs/src/neon/storage_broker/spec/replicated/replicated.toolbox/Model_1/MC.tla +Parsing file /Users/cs/src/neon/storage_broker/spec/replicated/replicated.toolbox/Model_1/replicated.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/TLC.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Integers.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Naturals.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Sequences.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/FiniteSets.tla +Semantic processing of module Naturals +Semantic processing of module Integers +Semantic processing of module replicated +Semantic processing of module Sequences +Semantic processing of module FiniteSets +Semantic processing of module TLC +Semantic processing of module MC +@!@!@STARTMSG 2219:0 @!@!@ +SANY finished. +@!@!@ENDMSG 2219 @!@!@ +@!@!@STARTMSG 2185:0 @!@!@ +Starting... (2025-01-19 16:40:16) +@!@!@ENDMSG 2185 @!@!@ +@!@!@STARTMSG 2279:3 @!@!@ +Declaring symmetry during liveness checking is dangerous. It might cause TLC to miss violations of the stated liveness properties. Please check liveness without symmetry defined. +@!@!@ENDMSG 2279 @!@!@ +@!@!@STARTMSG 2284:3 @!@!@ +Declaring state or action constraints during liveness checking is dangerous: Please read section 14.3.5 on page 247 of Specifying Systems (https://lamport.azurewebsites.net/tla/book.html) and optionally the discussion at https://discuss.tlapl.us/msg00994.html for more details. +@!@!@ENDMSG 2284 @!@!@ +@!@!@STARTMSG 2212:0 @!@!@ +Implied-temporal checking--satisfiability problem has 1 branches. +@!@!@ENDMSG 2212 @!@!@ +@!@!@STARTMSG 2189:0 @!@!@ +Computing initial states... +@!@!@ENDMSG 2189 @!@!@ +@!@!@STARTMSG 2190:0 @!@!@ +Finished computing initial states: 1 distinct state generated at 2025-01-19 16:40:18. +@!@!@ENDMSG 2190 @!@!@ +@!@!@STARTMSG 2192:0 @!@!@ +Checking temporal properties for the current state space with 1217 total distinct states at (2025-01-19 16:40:21) +@!@!@ENDMSG 2192 @!@!@ +@!@!@STARTMSG 2267:0 @!@!@ +Finished checking temporal properties in 00s at 2025-01-19 16:40:21 +@!@!@ENDMSG 2267 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(11) at 2025-01-19 16:40:21: 39.816 states generated (39.816 s/min), 3.288 distinct states found (3.288 ds/min), 2.067 states left on queue. +@!@!@ENDMSG 2200 @!@!@ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301223409/MC.tla b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301223409/MC.tla new file mode 100644 index 0000000000..316c6f4df7 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301223409/MC.tla @@ -0,0 +1,65 @@ +---- MODULE MC ---- +EXTENDS replicated, TLC + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +b1, b2, b3 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +s1, s2, s3 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +p1, p2 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +az1, az2, az3 +---- + +\* MV CONSTANT definitions brokers +const_17373012151752000 == +{b1, b2, b3} +---- + +\* MV CONSTANT definitions safekeepers +const_17373012151763000 == +{s1, s2, s3} +---- + +\* MV CONSTANT definitions pageservers +const_17373012151764000 == +{p1, p2} +---- + +\* MV CONSTANT definitions azs +const_17373012151765000 == +{az1, az2, az3} +---- + +\* SYMMETRY definition +symm_17373012151766000 == +Permutations(const_17373012151752000) \union Permutations(const_17373012151763000) \union Permutations(const_17373012151764000) \union Permutations(const_17373012151765000) +---- + +\* CONSTANT definitions @modelParameterConstants:4max_commit_lsn +const_17373012151767000 == +2 +---- + +\* CONSTANT definitions @modelParameterConstants:5az_mapping +const_17373012151768000 == +[ az1 |-> {b1,s1,p1} , az2 |-> {b2,s2,p2} , az3 |-> {b3,s3}] +---- + +\* CONSTRAINT definition @modelParameterContraint:0 +constr_17373012151769000 == +StateConstraint +---- +============================================================================= +\* Modification History +\* Created Sun Jan 19 16:40:15 CET 2025 by cs diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301223409/MC_TE.out b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301223409/MC_TE.out new file mode 100644 index 0000000000..ab92cbb3d7 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301223409/MC_TE.out @@ -0,0 +1,53 @@ +@!@!@STARTMSG 2262:0 @!@!@ +TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802) +@!@!@ENDMSG 2262 @!@!@ +@!@!@STARTMSG 2187:0 @!@!@ +Running breadth-first search Model-Checking with fp 20 and seed 6372772458573668883 with 4 workers on 8 cores with 2428MB heap and 5460MB offheap memory [pid: 9898] (Mac OS X 10.16 x86_64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue). +@!@!@ENDMSG 2187 @!@!@ +@!@!@STARTMSG 2220:0 @!@!@ +Starting SANY... +@!@!@ENDMSG 2220 @!@!@ +Parsing file /Users/cs/src/neon/storage_broker/spec/replicated/replicated.toolbox/Model_1/MC.tla +Parsing file /Users/cs/src/neon/storage_broker/spec/replicated/replicated.toolbox/Model_1/replicated.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/TLC.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Integers.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Naturals.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/Sequences.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202408081326/tla2sany/StandardModules/FiniteSets.tla +Semantic processing of module Naturals +Semantic processing of module Integers +Semantic processing of module replicated +Semantic processing of module Sequences +Semantic processing of module FiniteSets +Semantic processing of module TLC +Semantic processing of module MC +@!@!@STARTMSG 2219:0 @!@!@ +SANY finished. +@!@!@ENDMSG 2219 @!@!@ +@!@!@STARTMSG 2185:0 @!@!@ +Starting... (2025-01-19 16:40:16) +@!@!@ENDMSG 2185 @!@!@ +@!@!@STARTMSG 2279:3 @!@!@ +Declaring symmetry during liveness checking is dangerous. It might cause TLC to miss violations of the stated liveness properties. Please check liveness without symmetry defined. +@!@!@ENDMSG 2279 @!@!@ +@!@!@STARTMSG 2284:3 @!@!@ +Declaring state or action constraints during liveness checking is dangerous: Please read section 14.3.5 on page 247 of Specifying Systems (https://lamport.azurewebsites.net/tla/book.html) and optionally the discussion at https://discuss.tlapl.us/msg00994.html for more details. +@!@!@ENDMSG 2284 @!@!@ +@!@!@STARTMSG 2212:0 @!@!@ +Implied-temporal checking--satisfiability problem has 1 branches. +@!@!@ENDMSG 2212 @!@!@ +@!@!@STARTMSG 2189:0 @!@!@ +Computing initial states... +@!@!@ENDMSG 2189 @!@!@ +@!@!@STARTMSG 2190:0 @!@!@ +Finished computing initial states: 1 distinct state generated at 2025-01-19 16:40:18. +@!@!@ENDMSG 2190 @!@!@ +@!@!@STARTMSG 2192:0 @!@!@ +Checking temporal properties for the current state space with 1217 total distinct states at (2025-01-19 16:40:21) +@!@!@ENDMSG 2192 @!@!@ +@!@!@STARTMSG 2267:0 @!@!@ +Finished checking temporal properties in 00s at 2025-01-19 16:40:21 +@!@!@ENDMSG 2267 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(11) at 2025-01-19 16:40:21: 39.816 states generated (39.816 s/min), 3.288 distinct states found (3.288 ds/min), 2.067 states left on queue. +@!@!@ENDMSG 2200 @!@!@ diff --git a/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301223409/replicated.tla b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301223409/replicated.tla new file mode 100644 index 0000000000..14910364fe --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/Model_1_SnapShot_1737301223409/replicated.tla @@ -0,0 +1,117 @@ +---- MODULE replicated ---- + +EXTENDS Integers + +VARIABLES broker_state, safekeeper_state, pageserver_state + + +CONSTANT + brokers, + safekeepers, + pageservers, + azs, + az_mapping + +CONSTANT + NULL + +CONSTANT + max_commit_lsn + +StateConstraint == + /\ \A s \in safekeepers: + /\ safekeeper_state[s].commit_lsn <= max_commit_lsn + /\ \A b \in brokers: + /\ \A s \in DOMAIN broker_state[b].sk: + /\ broker_state[b].sk[s].commit_lsn <= max_commit_lsn + + +InitSafekeeper == [pruned_lsn |-> 0, commit_lsn |-> 0] +InitBroker == [sk |-> [s \in safekeepers |-> [commit_lsn |-> 0]]] +InitPageserver == [last_record_lsn |-> 0, preferred_sk |-> NULL, sk |-> [s \in safekeepers |-> [commit_lsn |-> 0]]] + +Init == + /\ broker_state = [b \in brokers |-> InitBroker] + /\ safekeeper_state = [s \in safekeepers |-> InitSafekeeper] + /\ pageserver_state = [p \in pageservers |-> InitPageserver] + + +SkCommit(s1, s2) == + /\ s1 # s2 + /\ safekeeper_state[s1].commit_lsn = safekeeper_state[s2].commit_lsn + /\ LET + new_commit_lsn == safekeeper_state[s1].commit_lsn + 1 + IN + safekeeper_state' = [safekeeper_state EXCEPT + ![s1].commit_lsn = new_commit_lsn, + ![s2].commit_lsn = new_commit_lsn] + /\ UNCHANGED <> + +SkPeerRecovery(s1,s2) == + /\ safekeeper_state[s1].commit_lsn < safekeeper_state[s2].commit_lsn + /\ safekeeper_state' = [safekeeper_state EXCEPT![s1].commit_lsn = safekeeper_state[s2].commit_lsn] + /\ UNCHANGED <> + +SkPushToBroker(s,b) == + /\ broker_state' = IF broker_state[b].sk[s].commit_lsn < safekeeper_state[s].commit_lsn + THEN + LET + bsk == broker_state[b].sk + updbsk == [bsk EXCEPT ![s].commit_lsn = safekeeper_state[s].commit_lsn] + IN + [broker_state EXCEPT ![b].sk = updbsk] + ELSE broker_state + /\ UNCHANGED <> + +PsRecvBroker(b,p,s) == + /\ LET + bsk == broker_state[b].sk[s] + psk == pageserver_state[p].sk[s] + updpsk == [psk EXCEPT !["commit_lsn"] = bsk.commit_lsn] + IN + pageserver_state' = IF bsk.commit_lsn > psk.commit_lsn + THEN [pageserver_state EXCEPT ![p].sk[s] = updpsk] + ELSE pageserver_state + /\ UNCHANGED <> + + +SksWithNewerWal(p) == + LET + ps == pageserver_state[p] + IN + {s \in DOMAIN ps.sk: ps.sk[s].commit_lsn > ps.last_record_lsn} + +PsChooseSk(p) == + /\ SksWithNewerWal(p) # {} + /\ pageserver_state' = [pageserver_state EXCEPT![p].preferred_sk = CHOOSE s \in SksWithNewerWal(p): TRUE] + /\ UNCHANGED <> + + +Next == + + \/ \E s1 \in safekeepers: \E s2 \in safekeepers: + \/ SkCommit(s1, s2) + \/ SkPeerRecovery(s1, s2) + \/ \E s \in safekeepers: \E b \in brokers: SkPushToBroker(s, b) + \/ \E s \in safekeepers: \E b \in brokers: \E p \in pageservers: PsRecvBroker(b,p,s) + \/ \E p \in pageservers: PsChooseSk(p) + + +Spec == Init /\ [][Next]_<< broker_state, safekeeper_state, pageserver_state >> + + +\* invariants + +EventuallyLaggingSkIsNotPreferredSk == <>( + LET + sks == safekeeper_state + lagging_sks == { s \in safekeepers: \A s2 \in safekeepers: sks[s].commit_lsn <= sks[s2].commit_lsn } + preferred_sks == {pageserver_state[p].preferred_sk: p \in pageservers} + IN + preferred_sks \cap lagging_sks = {} + + ) + + + +==== \ No newline at end of file diff --git a/storage_broker/spec/replicated/replicated.toolbox/fullmesh.tla.pmap b/storage_broker/spec/replicated/replicated.toolbox/fullmesh.tla.pmap new file mode 100644 index 0000000000..a224f42aac Binary files /dev/null and b/storage_broker/spec/replicated/replicated.toolbox/fullmesh.tla.pmap differ diff --git a/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1.launch b/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1.launch new file mode 100644 index 0000000000..e7455da5fd --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1.launch @@ -0,0 +1,58 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737296416956.launch b/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737296416956.launch new file mode 100644 index 0000000000..b6473f673b --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737296416956.launch @@ -0,0 +1,38 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737297534393.launch b/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737297534393.launch new file mode 100644 index 0000000000..2d71f66906 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737297534393.launch @@ -0,0 +1,40 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737297999722.launch b/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737297999722.launch new file mode 100644 index 0000000000..1a09cb6ee5 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737297999722.launch @@ -0,0 +1,40 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737299352762.launch b/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737299352762.launch new file mode 100644 index 0000000000..d7f0f71f05 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737299352762.launch @@ -0,0 +1,42 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737299381423.launch b/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737299381423.launch new file mode 100644 index 0000000000..20569969c6 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737299381423.launch @@ -0,0 +1,58 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737299469039.launch b/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737299469039.launch new file mode 100644 index 0000000000..66fb925b63 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737299469039.launch @@ -0,0 +1,58 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737299542008.launch b/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737299542008.launch new file mode 100644 index 0000000000..971c7c5a63 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737299542008.launch @@ -0,0 +1,58 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737299744229.launch b/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737299744229.launch new file mode 100644 index 0000000000..d8b504d669 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737299744229.launch @@ -0,0 +1,58 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737301172627.launch b/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737301172627.launch new file mode 100644 index 0000000000..3acafd183d --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737301172627.launch @@ -0,0 +1,58 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737301223409.launch b/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737301223409.launch new file mode 100644 index 0000000000..79f0c2c1e8 --- /dev/null +++ b/storage_broker/spec/replicated/replicated.toolbox/replicated___Model_1_SnapShot_1737301223409.launch @@ -0,0 +1,58 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +