sketch a spec for replicated broker

This commit is contained in:
Christian Schwarz
2025-01-19 16:40:32 +01:00
parent 0c54e5fb83
commit 933b4719cb
80 changed files with 5282 additions and 0 deletions

BIN
storage_broker/spec/replicated/.DS_Store vendored Normal file

Binary file not shown.

View File

@@ -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 <<broker_state, pageserver_state>>
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 <<broker_state, pageserver_state>>
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 <<safekeeper_state, pageserver_state>>
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 <<safekeeper_state, broker_state>>
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 <<safekeeper_state, broker_state>>
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 = {}
)
====

View File

@@ -0,0 +1,24 @@
<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
<name>replicated</name>
<comment></comment>
<projects>
</projects>
<buildSpec>
<buildCommand>
<name>toolbox.builder.TLAParserBuilder</name>
<arguments>
</arguments>
</buildCommand>
</buildSpec>
<natures>
<nature>toolbox.natures.TLANature</nature>
</natures>
<linkedResources>
<link>
<name>replicated.tla</name>
<type>1</type>
<locationURI>PARENT-1-PROJECT_LOC/replicated.tla</locationURI>
</link>
</linkedResources>
</projectDescription>

View File

@@ -0,0 +1,2 @@
ProjectRootFile=PARENT-1-PROJECT_LOC/replicated.tla
eclipse.preferences.version=1

View File

@@ -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

View File

@@ -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 @!@!@

View File

@@ -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

View File

@@ -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 @!@!@

View File

@@ -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 <<broker_state, pageserver_state>>
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 <<broker_state, pageserver_state>>
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 <<safekeeper_state, pageserver_state>>
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 <<safekeeper_state, broker_state>>
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 <<safekeeper_state, broker_state>>
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 = {}
)
====

View File

@@ -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

View File

@@ -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 @!@!@

View File

@@ -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

View File

@@ -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 @!@!@

View File

@@ -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 <<broker_state, pageserver_state>>
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 <<safekeeper_state, pageserver_state>>
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 <<safekeeper_state, broker_state>>
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 <<safekeeper_state, broker_state>>
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
====

View File

@@ -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

View File

@@ -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 @!@!@

View File

@@ -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

View File

@@ -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 @!@!@

View File

@@ -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 <<broker_state, pageserver_state>>
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 <<safekeeper_state, pageserver_state>>
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 <<safekeeper_state, broker_state>>
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 <<safekeeper_state, broker_state>>
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
====

View File

@@ -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

View File

@@ -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 @!@!@

View File

@@ -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

View File

@@ -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 @!@!@

View File

@@ -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 <<broker_state, pageserver_state>>
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 <<safekeeper_state, pageserver_state>>
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 <<safekeeper_state, broker_state>>
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 <<safekeeper_state, broker_state>>
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
====

View File

@@ -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

View File

@@ -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 @!@!@

View File

@@ -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

View File

@@ -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 @!@!@

View File

@@ -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 <<broker_state, pageserver_state>>
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 <<safekeeper_state, pageserver_state>>
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 <<safekeeper_state, broker_state>>
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 <<safekeeper_state, broker_state>>
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 = {}
)
====

View File

@@ -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

View File

@@ -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: <Initial predicate>
/\ 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: <SkCommit line 40, col 5 to line 47, col 51 of module fullmesh>
/\ 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: <SkPeerRecovery line 50, col 5 to line 51, col 102 of module fullmesh>
/\ 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 @!@!@
<Init line 33, col 1 to line 33, col 4 of module fullmesh>: 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 @!@!@
<SkCommit line 39, col 1 to line 39, col 16 of module fullmesh>: 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 @!@!@
<SkPeerRecovery line 49, col 1 to line 49, col 21 of module fullmesh>: 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 @!@!@
<SkPushToBroker line 53, col 1 to line 53, col 19 of module fullmesh>: 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 @!@!@
<PsRecvBroker line 64, col 1 to line 64, col 19 of module fullmesh>: 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 @!@!@
<PsChooseSk line 82, col 1 to line 82, col 13 of module fullmesh>: 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 @!@!@

View File

@@ -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

View File

@@ -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: <Initial predicate>
/\ 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: <SkCommit line 40, col 5 to line 47, col 51 of module fullmesh>
/\ 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: <SkPeerRecovery line 50, col 5 to line 51, col 102 of module fullmesh>
/\ 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 @!@!@
<Init line 33, col 1 to line 33, col 4 of module fullmesh>: 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 @!@!@
<SkCommit line 39, col 1 to line 39, col 16 of module fullmesh>: 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 @!@!@
<SkPeerRecovery line 49, col 1 to line 49, col 21 of module fullmesh>: 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 @!@!@
<SkPushToBroker line 53, col 1 to line 53, col 19 of module fullmesh>: 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 @!@!@
<PsRecvBroker line 64, col 1 to line 64, col 19 of module fullmesh>: 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 @!@!@
<PsChooseSk line 82, col 1 to line 82, col 13 of module fullmesh>: 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 @!@!@

View File

@@ -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 <<broker_state, pageserver_state>>
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 <<safekeeper_state, pageserver_state>>
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 <<safekeeper_state, broker_state>>
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 <<safekeeper_state, broker_state>>
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 = {}
)
====

View File

@@ -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

View File

@@ -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: <Initial predicate>
/\ 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: <SkCommit line 40, col 5 to line 48, col 51 of module fullmesh>
/\ 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: <SkCommit line 40, col 5 to line 48, col 51 of module fullmesh>
/\ 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: <SkPeerRecovery line 51, col 5 to line 52, col 102 of module fullmesh>
/\ 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 @!@!@
<Init line 33, col 1 to line 33, col 4 of module fullmesh>: 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 @!@!@
<SkCommit line 39, col 1 to line 39, col 16 of module fullmesh>: 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 @!@!@
<SkPeerRecovery line 50, col 1 to line 50, col 21 of module fullmesh>: 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 @!@!@
<SkPushToBroker line 54, col 1 to line 54, col 19 of module fullmesh>: 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 @!@!@
<PsRecvBroker line 65, col 1 to line 65, col 19 of module fullmesh>: 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 @!@!@
<PsChooseSk line 83, col 1 to line 83, col 13 of module fullmesh>: 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 @!@!@

View File

@@ -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

View File

@@ -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: <Initial predicate>
/\ 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: <SkCommit line 40, col 5 to line 48, col 51 of module fullmesh>
/\ 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: <SkCommit line 40, col 5 to line 48, col 51 of module fullmesh>
/\ 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: <SkPeerRecovery line 51, col 5 to line 52, col 102 of module fullmesh>
/\ 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 @!@!@
<Init line 33, col 1 to line 33, col 4 of module fullmesh>: 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 @!@!@
<SkCommit line 39, col 1 to line 39, col 16 of module fullmesh>: 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 @!@!@
<SkPeerRecovery line 50, col 1 to line 50, col 21 of module fullmesh>: 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 @!@!@
<SkPushToBroker line 54, col 1 to line 54, col 19 of module fullmesh>: 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 @!@!@
<PsRecvBroker line 65, col 1 to line 65, col 19 of module fullmesh>: 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 @!@!@
<PsChooseSk line 83, col 1 to line 83, col 13 of module fullmesh>: 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 @!@!@

View File

@@ -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 <<broker_state, pageserver_state>>
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 <<safekeeper_state, pageserver_state>>
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 <<safekeeper_state, broker_state>>
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 <<safekeeper_state, broker_state>>
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 = {}
)
====

View File

@@ -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

View File

@@ -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 @!@!@

View File

@@ -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

View File

@@ -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 @!@!@

View File

@@ -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 <<broker_state, pageserver_state>>
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 <<broker_state, safekeeper_state>>
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 <<safekeeper_state, pageserver_state>>
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 <<safekeeper_state, broker_state>>
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 <<safekeeper_state, broker_state>>
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 = {}
)
====

View File

@@ -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

View File

@@ -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 @!@!@
<Init line 33, col 1 to line 33, col 4 of module fullmesh>: 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 @!@!@
<SkCommit line 39, col 1 to line 39, col 16 of module fullmesh>: 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 @!@!@
<SkPeerRecovery line 50, col 1 to line 50, col 21 of module fullmesh>: 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 @!@!@
<SkPushToBroker line 55, col 1 to line 55, col 19 of module fullmesh>: 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 @!@!@
<PsRecvBroker line 66, col 1 to line 66, col 19 of module fullmesh>: 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 @!@!@
<PsChooseSk line 84, col 1 to line 84, col 13 of module fullmesh>: 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 @!@!@

View File

@@ -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

View File

@@ -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 @!@!@
<Init line 33, col 1 to line 33, col 4 of module fullmesh>: 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 @!@!@
<SkCommit line 39, col 1 to line 39, col 16 of module fullmesh>: 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 @!@!@
<SkPeerRecovery line 50, col 1 to line 50, col 21 of module fullmesh>: 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 @!@!@
<SkPushToBroker line 55, col 1 to line 55, col 19 of module fullmesh>: 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 @!@!@
<PsRecvBroker line 66, col 1 to line 66, col 19 of module fullmesh>: 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 @!@!@
<PsChooseSk line 84, col 1 to line 84, col 13 of module fullmesh>: 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 @!@!@

View File

@@ -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 <<broker_state, pageserver_state>>
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 <<broker_state, pageserver_state>>
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 <<safekeeper_state, pageserver_state>>
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 <<safekeeper_state, broker_state>>
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 <<safekeeper_state, broker_state>>
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 = {}
)
====

View File

@@ -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

View File

@@ -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 @!@!@

View File

@@ -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

View File

@@ -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 @!@!@

View File

@@ -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 <<broker_state, pageserver_state>>
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 <<broker_state, pageserver_state>>
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 <<safekeeper_state, pageserver_state>>
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 <<safekeeper_state, broker_state>>
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 <<safekeeper_state, broker_state>>
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 = {}
)
====

View File

@@ -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

View File

@@ -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 @!@!@

View File

@@ -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

View File

@@ -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 @!@!@

View File

@@ -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 <<broker_state, pageserver_state>>
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 <<broker_state, pageserver_state>>
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 <<safekeeper_state, pageserver_state>>
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 <<safekeeper_state, broker_state>>
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 <<safekeeper_state, broker_state>>
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 = {}
)
====

View File

@@ -0,0 +1,58 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
<stringAttribute key="TLCCmdLineParameters" value=""/>
<intAttribute key="collectCoverage" value="1"/>
<stringAttribute key="configurationName" value="Model_1"/>
<booleanAttribute key="deferLiveness" value="false"/>
<intAttribute key="dfidDepth" value="100"/>
<booleanAttribute key="dfidMode" value="false"/>
<intAttribute key="distributedFPSetCount" value="0"/>
<stringAttribute key="distributedNetworkInterface" value="100.65.224.26"/>
<intAttribute key="distributedNodesCount" value="1"/>
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
<intAttribute key="fpBits" value="1"/>
<intAttribute key="fpIndex" value="119"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="25"/>
<intAttribute key="maxSetSize" value="1000000"/>
<booleanAttribute key="mcMode" value="true"/>
<stringAttribute key="modelBehaviorInit" value=""/>
<stringAttribute key="modelBehaviorNext" value=""/>
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
<intAttribute key="modelBehaviorSpecType" value="1"/>
<stringAttribute key="modelBehaviorVars" value="pageserver_state, broker_state, safekeeper_state"/>
<stringAttribute key="modelComments" value=""/>
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
<listAttribute key="modelCorrectnessInvariants"/>
<listAttribute key="modelCorrectnessProperties">
<listEntry value="1EventuallyLaggingSkIsNotPreferredSk"/>
</listAttribute>
<intAttribute key="modelEditorOpenTabs" value="14"/>
<stringAttribute key="modelExpressionEval" value=""/>
<stringAttribute key="modelParameterActionConstraint" value=""/>
<listAttribute key="modelParameterConstants">
<listEntry value="brokers;;{b1, b2, b3};1;1"/>
<listEntry value="NULL;;NULL;1;0"/>
<listEntry value="safekeepers;;{s1, s2, s3};1;1"/>
<listEntry value="pageservers;;{p1, p2};1;1"/>
<listEntry value="max_commit_lsn;;2;0;0"/>
<listEntry value="az_mapping;;[ az1 |-&gt; {b1,s1,p1} , az2 |-&gt; {b2,s2,p2} , az3 |-&gt; {b3,s3}];0;0"/>
<listEntry value="azs;;{az1, az2, az3};1;1"/>
</listAttribute>
<stringAttribute key="modelParameterContraint" value="StateConstraint"/>
<listAttribute key="modelParameterDefinitions"/>
<stringAttribute key="modelParameterModelValues" value="{}"/>
<stringAttribute key="modelParameterNewDefinitions" value=""/>
<intAttribute key="modelVersion" value="20191005"/>
<intAttribute key="numberOfWorkers" value="4"/>
<booleanAttribute key="recover" value="false"/>
<stringAttribute key="result.mail.address" value=""/>
<intAttribute key="simuAril" value="-1"/>
<intAttribute key="simuDepth" value="100"/>
<intAttribute key="simuSeed" value="-1"/>
<stringAttribute key="specName" value="replicated"/>
<stringAttribute key="tlcResourcesProfile" value="local custom"/>
<stringAttribute key="view" value=""/>
<booleanAttribute key="visualizeStateGraph" value="false"/>
</launchConfiguration>

View File

@@ -0,0 +1,38 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
<stringAttribute key="configurationName" value="Model_1_SnapShot_1737296416956"/>
<intAttribute key="distributedFPSetCount" value="0"/>
<stringAttribute key="distributedNetworkInterface" value="100.65.224.26"/>
<intAttribute key="distributedNodesCount" value="1"/>
<stringAttribute key="distributedTLC" value="off"/>
<intAttribute key="fpIndex" value="60"/>
<intAttribute key="maxHeapSize" value="25"/>
<stringAttribute key="modelBehaviorInit" value=""/>
<stringAttribute key="modelBehaviorNext" value=""/>
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
<intAttribute key="modelBehaviorSpecType" value="1"/>
<stringAttribute key="modelBehaviorVars" value="pageserver_state, broker_state, safekeeper_state"/>
<stringAttribute key="modelComments" value=""/>
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
<listAttribute key="modelCorrectnessInvariants"/>
<listAttribute key="modelCorrectnessProperties"/>
<intAttribute key="modelEditorOpenTabs" value="10"/>
<stringAttribute key="modelExpressionEval" value=""/>
<stringAttribute key="modelParameterActionConstraint" value=""/>
<listAttribute key="modelParameterConstants">
<listEntry value="brokers;;{b1, b2, b3};1;1"/>
<listEntry value="NULL;;NULL;1;0"/>
<listEntry value="safekeepers;;{s1, s2, s3};1;1"/>
<listEntry value="pageservers;;{p1, p2};1;1"/>
<listEntry value="max_commit_lsn;;2;0;0"/>
</listAttribute>
<stringAttribute key="modelParameterContraint" value="StateConstraint"/>
<listAttribute key="modelParameterDefinitions"/>
<stringAttribute key="modelParameterModelValues" value="{}"/>
<stringAttribute key="modelParameterNewDefinitions" value=""/>
<intAttribute key="modelVersion" value="20191005"/>
<intAttribute key="numberOfWorkers" value="4"/>
<stringAttribute key="result.mail.address" value=""/>
<stringAttribute key="specName" value="replicated"/>
<stringAttribute key="tlcResourcesProfile" value="local custom"/>
</launchConfiguration>

View File

@@ -0,0 +1,40 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
<stringAttribute key="configurationName" value="Model_1_SnapShot_1737297534393"/>
<intAttribute key="distributedFPSetCount" value="0"/>
<stringAttribute key="distributedNetworkInterface" value="100.65.224.26"/>
<intAttribute key="distributedNodesCount" value="1"/>
<stringAttribute key="distributedTLC" value="off"/>
<intAttribute key="fpIndex" value="130"/>
<intAttribute key="maxHeapSize" value="25"/>
<stringAttribute key="modelBehaviorInit" value=""/>
<stringAttribute key="modelBehaviorNext" value=""/>
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
<intAttribute key="modelBehaviorSpecType" value="1"/>
<stringAttribute key="modelBehaviorVars" value="pageserver_state, broker_state, safekeeper_state"/>
<stringAttribute key="modelComments" value=""/>
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
<listAttribute key="modelCorrectnessInvariants"/>
<listAttribute key="modelCorrectnessProperties"/>
<intAttribute key="modelEditorOpenTabs" value="10"/>
<stringAttribute key="modelExpressionEval" value=""/>
<stringAttribute key="modelParameterActionConstraint" value=""/>
<listAttribute key="modelParameterConstants">
<listEntry value="brokers;;{b1, b2, b3};1;1"/>
<listEntry value="NULL;;NULL;1;0"/>
<listEntry value="safekeepers;;{s1, s2, s3};1;1"/>
<listEntry value="pageservers;;{p1, p2};1;1"/>
<listEntry value="max_commit_lsn;;2;0;0"/>
<listEntry value="az_mapping;;[ az1 |-&gt; {b1,s1,p1} , az2 |-&gt; {b2,s2,p2} , az3 |-&gt; {b3,s3}];0;0"/>
<listEntry value="azs;;{az1, az2, az3};1;1"/>
</listAttribute>
<stringAttribute key="modelParameterContraint" value="StateConstraint"/>
<listAttribute key="modelParameterDefinitions"/>
<stringAttribute key="modelParameterModelValues" value="{}"/>
<stringAttribute key="modelParameterNewDefinitions" value=""/>
<intAttribute key="modelVersion" value="20191005"/>
<intAttribute key="numberOfWorkers" value="4"/>
<stringAttribute key="result.mail.address" value=""/>
<stringAttribute key="specName" value="replicated"/>
<stringAttribute key="tlcResourcesProfile" value="local custom"/>
</launchConfiguration>

View File

@@ -0,0 +1,40 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
<stringAttribute key="configurationName" value="Model_1_SnapShot_1737297999722"/>
<intAttribute key="distributedFPSetCount" value="0"/>
<stringAttribute key="distributedNetworkInterface" value="100.65.224.26"/>
<intAttribute key="distributedNodesCount" value="1"/>
<stringAttribute key="distributedTLC" value="off"/>
<intAttribute key="fpIndex" value="0"/>
<intAttribute key="maxHeapSize" value="25"/>
<stringAttribute key="modelBehaviorInit" value=""/>
<stringAttribute key="modelBehaviorNext" value=""/>
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
<intAttribute key="modelBehaviorSpecType" value="1"/>
<stringAttribute key="modelBehaviorVars" value="pageserver_state, broker_state, safekeeper_state"/>
<stringAttribute key="modelComments" value=""/>
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
<listAttribute key="modelCorrectnessInvariants"/>
<listAttribute key="modelCorrectnessProperties"/>
<intAttribute key="modelEditorOpenTabs" value="10"/>
<stringAttribute key="modelExpressionEval" value=""/>
<stringAttribute key="modelParameterActionConstraint" value=""/>
<listAttribute key="modelParameterConstants">
<listEntry value="brokers;;{b1, b2, b3};1;1"/>
<listEntry value="NULL;;NULL;1;0"/>
<listEntry value="safekeepers;;{s1, s2, s3};1;1"/>
<listEntry value="pageservers;;{p1, p2};1;1"/>
<listEntry value="max_commit_lsn;;2;0;0"/>
<listEntry value="az_mapping;;[ az1 |-&gt; {b1,s1,p1} , az2 |-&gt; {b2,s2,p2} , az3 |-&gt; {b3,s3}];0;0"/>
<listEntry value="azs;;{az1, az2, az3};1;1"/>
</listAttribute>
<stringAttribute key="modelParameterContraint" value="StateConstraint"/>
<listAttribute key="modelParameterDefinitions"/>
<stringAttribute key="modelParameterModelValues" value="{}"/>
<stringAttribute key="modelParameterNewDefinitions" value=""/>
<intAttribute key="modelVersion" value="20191005"/>
<intAttribute key="numberOfWorkers" value="4"/>
<stringAttribute key="result.mail.address" value=""/>
<stringAttribute key="specName" value="replicated"/>
<stringAttribute key="tlcResourcesProfile" value="local custom"/>
</launchConfiguration>

View File

@@ -0,0 +1,42 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
<stringAttribute key="configurationName" value="Model_1_SnapShot_1737299352762"/>
<intAttribute key="distributedFPSetCount" value="0"/>
<stringAttribute key="distributedNetworkInterface" value="100.65.224.26"/>
<intAttribute key="distributedNodesCount" value="1"/>
<stringAttribute key="distributedTLC" value="off"/>
<intAttribute key="fpIndex" value="119"/>
<intAttribute key="maxHeapSize" value="25"/>
<stringAttribute key="modelBehaviorInit" value=""/>
<stringAttribute key="modelBehaviorNext" value=""/>
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
<intAttribute key="modelBehaviorSpecType" value="1"/>
<stringAttribute key="modelBehaviorVars" value="pageserver_state, broker_state, safekeeper_state"/>
<stringAttribute key="modelComments" value=""/>
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
<listAttribute key="modelCorrectnessInvariants">
<listEntry value="1EventuallyLaggingSkIsNotPreferredSk"/>
</listAttribute>
<listAttribute key="modelCorrectnessProperties"/>
<intAttribute key="modelEditorOpenTabs" value="10"/>
<stringAttribute key="modelExpressionEval" value=""/>
<stringAttribute key="modelParameterActionConstraint" value=""/>
<listAttribute key="modelParameterConstants">
<listEntry value="brokers;;{b1, b2, b3};1;1"/>
<listEntry value="NULL;;NULL;1;0"/>
<listEntry value="safekeepers;;{s1, s2, s3};1;1"/>
<listEntry value="pageservers;;{p1, p2};1;1"/>
<listEntry value="max_commit_lsn;;2;0;0"/>
<listEntry value="az_mapping;;[ az1 |-&gt; {b1,s1,p1} , az2 |-&gt; {b2,s2,p2} , az3 |-&gt; {b3,s3}];0;0"/>
<listEntry value="azs;;{az1, az2, az3};1;1"/>
</listAttribute>
<stringAttribute key="modelParameterContraint" value="StateConstraint"/>
<listAttribute key="modelParameterDefinitions"/>
<stringAttribute key="modelParameterModelValues" value="{}"/>
<stringAttribute key="modelParameterNewDefinitions" value=""/>
<intAttribute key="modelVersion" value="20191005"/>
<intAttribute key="numberOfWorkers" value="4"/>
<stringAttribute key="result.mail.address" value=""/>
<stringAttribute key="specName" value="replicated"/>
<stringAttribute key="tlcResourcesProfile" value="local custom"/>
</launchConfiguration>

View File

@@ -0,0 +1,58 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
<stringAttribute key="TLCCmdLineParameters" value=""/>
<intAttribute key="collectCoverage" value="1"/>
<stringAttribute key="configurationName" value="Model_1_SnapShot_1737299381423"/>
<booleanAttribute key="deferLiveness" value="false"/>
<intAttribute key="dfidDepth" value="100"/>
<booleanAttribute key="dfidMode" value="false"/>
<intAttribute key="distributedFPSetCount" value="0"/>
<stringAttribute key="distributedNetworkInterface" value="100.65.224.26"/>
<intAttribute key="distributedNodesCount" value="1"/>
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
<intAttribute key="fpBits" value="1"/>
<intAttribute key="fpIndex" value="119"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="25"/>
<intAttribute key="maxSetSize" value="1000000"/>
<booleanAttribute key="mcMode" value="true"/>
<stringAttribute key="modelBehaviorInit" value=""/>
<stringAttribute key="modelBehaviorNext" value=""/>
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
<intAttribute key="modelBehaviorSpecType" value="1"/>
<stringAttribute key="modelBehaviorVars" value="pageserver_state, broker_state, safekeeper_state"/>
<stringAttribute key="modelComments" value=""/>
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
<listAttribute key="modelCorrectnessInvariants"/>
<listAttribute key="modelCorrectnessProperties">
<listEntry value="1EventuallyLaggingSkIsNotPreferredSk"/>
</listAttribute>
<intAttribute key="modelEditorOpenTabs" value="14"/>
<stringAttribute key="modelExpressionEval" value=""/>
<stringAttribute key="modelParameterActionConstraint" value=""/>
<listAttribute key="modelParameterConstants">
<listEntry value="brokers;;{b1, b2, b3};1;1"/>
<listEntry value="NULL;;NULL;1;0"/>
<listEntry value="safekeepers;;{s1, s2, s3};1;1"/>
<listEntry value="pageservers;;{p1, p2};1;1"/>
<listEntry value="max_commit_lsn;;2;0;0"/>
<listEntry value="az_mapping;;[ az1 |-&gt; {b1,s1,p1} , az2 |-&gt; {b2,s2,p2} , az3 |-&gt; {b3,s3}];0;0"/>
<listEntry value="azs;;{az1, az2, az3};1;1"/>
</listAttribute>
<stringAttribute key="modelParameterContraint" value="StateConstraint"/>
<listAttribute key="modelParameterDefinitions"/>
<stringAttribute key="modelParameterModelValues" value="{}"/>
<stringAttribute key="modelParameterNewDefinitions" value=""/>
<intAttribute key="modelVersion" value="20191005"/>
<intAttribute key="numberOfWorkers" value="4"/>
<booleanAttribute key="recover" value="false"/>
<stringAttribute key="result.mail.address" value=""/>
<intAttribute key="simuAril" value="-1"/>
<intAttribute key="simuDepth" value="100"/>
<intAttribute key="simuSeed" value="-1"/>
<stringAttribute key="specName" value="replicated"/>
<stringAttribute key="tlcResourcesProfile" value="local custom"/>
<stringAttribute key="view" value=""/>
<booleanAttribute key="visualizeStateGraph" value="false"/>
</launchConfiguration>

View File

@@ -0,0 +1,58 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
<stringAttribute key="TLCCmdLineParameters" value=""/>
<intAttribute key="collectCoverage" value="1"/>
<stringAttribute key="configurationName" value="Model_1_SnapShot_1737299469039"/>
<booleanAttribute key="deferLiveness" value="false"/>
<intAttribute key="dfidDepth" value="100"/>
<booleanAttribute key="dfidMode" value="false"/>
<intAttribute key="distributedFPSetCount" value="0"/>
<stringAttribute key="distributedNetworkInterface" value="100.65.224.26"/>
<intAttribute key="distributedNodesCount" value="1"/>
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
<intAttribute key="fpBits" value="1"/>
<intAttribute key="fpIndex" value="119"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="25"/>
<intAttribute key="maxSetSize" value="1000000"/>
<booleanAttribute key="mcMode" value="true"/>
<stringAttribute key="modelBehaviorInit" value=""/>
<stringAttribute key="modelBehaviorNext" value=""/>
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
<intAttribute key="modelBehaviorSpecType" value="1"/>
<stringAttribute key="modelBehaviorVars" value="pageserver_state, broker_state, safekeeper_state"/>
<stringAttribute key="modelComments" value=""/>
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
<listAttribute key="modelCorrectnessInvariants"/>
<listAttribute key="modelCorrectnessProperties">
<listEntry value="1EventuallyLaggingSkIsNotPreferredSk"/>
</listAttribute>
<intAttribute key="modelEditorOpenTabs" value="14"/>
<stringAttribute key="modelExpressionEval" value=""/>
<stringAttribute key="modelParameterActionConstraint" value=""/>
<listAttribute key="modelParameterConstants">
<listEntry value="brokers;;{b1, b2, b3};1;1"/>
<listEntry value="NULL;;NULL;1;0"/>
<listEntry value="safekeepers;;{s1, s2, s3};1;1"/>
<listEntry value="pageservers;;{p1, p2};1;1"/>
<listEntry value="max_commit_lsn;;2;0;0"/>
<listEntry value="az_mapping;;[ az1 |-&gt; {b1,s1,p1} , az2 |-&gt; {b2,s2,p2} , az3 |-&gt; {b3,s3}];0;0"/>
<listEntry value="azs;;{az1, az2, az3};1;1"/>
</listAttribute>
<stringAttribute key="modelParameterContraint" value="StateConstraint"/>
<listAttribute key="modelParameterDefinitions"/>
<stringAttribute key="modelParameterModelValues" value="{}"/>
<stringAttribute key="modelParameterNewDefinitions" value=""/>
<intAttribute key="modelVersion" value="20191005"/>
<intAttribute key="numberOfWorkers" value="4"/>
<booleanAttribute key="recover" value="false"/>
<stringAttribute key="result.mail.address" value=""/>
<intAttribute key="simuAril" value="-1"/>
<intAttribute key="simuDepth" value="100"/>
<intAttribute key="simuSeed" value="-1"/>
<stringAttribute key="specName" value="replicated"/>
<stringAttribute key="tlcResourcesProfile" value="local custom"/>
<stringAttribute key="view" value=""/>
<booleanAttribute key="visualizeStateGraph" value="false"/>
</launchConfiguration>

View File

@@ -0,0 +1,58 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
<stringAttribute key="TLCCmdLineParameters" value=""/>
<intAttribute key="collectCoverage" value="1"/>
<stringAttribute key="configurationName" value="Model_1_SnapShot_1737299542008"/>
<booleanAttribute key="deferLiveness" value="false"/>
<intAttribute key="dfidDepth" value="100"/>
<booleanAttribute key="dfidMode" value="false"/>
<intAttribute key="distributedFPSetCount" value="0"/>
<stringAttribute key="distributedNetworkInterface" value="100.65.224.26"/>
<intAttribute key="distributedNodesCount" value="1"/>
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
<intAttribute key="fpBits" value="1"/>
<intAttribute key="fpIndex" value="119"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="25"/>
<intAttribute key="maxSetSize" value="1000000"/>
<booleanAttribute key="mcMode" value="true"/>
<stringAttribute key="modelBehaviorInit" value=""/>
<stringAttribute key="modelBehaviorNext" value=""/>
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
<intAttribute key="modelBehaviorSpecType" value="1"/>
<stringAttribute key="modelBehaviorVars" value="pageserver_state, broker_state, safekeeper_state"/>
<stringAttribute key="modelComments" value=""/>
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
<listAttribute key="modelCorrectnessInvariants"/>
<listAttribute key="modelCorrectnessProperties">
<listEntry value="1EventuallyLaggingSkIsNotPreferredSk"/>
</listAttribute>
<intAttribute key="modelEditorOpenTabs" value="14"/>
<stringAttribute key="modelExpressionEval" value=""/>
<stringAttribute key="modelParameterActionConstraint" value=""/>
<listAttribute key="modelParameterConstants">
<listEntry value="brokers;;{b1, b2, b3};1;1"/>
<listEntry value="NULL;;NULL;1;0"/>
<listEntry value="safekeepers;;{s1, s2, s3};1;1"/>
<listEntry value="pageservers;;{p1, p2};1;1"/>
<listEntry value="max_commit_lsn;;2;0;0"/>
<listEntry value="az_mapping;;[ az1 |-&gt; {b1,s1,p1} , az2 |-&gt; {b2,s2,p2} , az3 |-&gt; {b3,s3}];0;0"/>
<listEntry value="azs;;{az1, az2, az3};1;1"/>
</listAttribute>
<stringAttribute key="modelParameterContraint" value="StateConstraint"/>
<listAttribute key="modelParameterDefinitions"/>
<stringAttribute key="modelParameterModelValues" value="{}"/>
<stringAttribute key="modelParameterNewDefinitions" value=""/>
<intAttribute key="modelVersion" value="20191005"/>
<intAttribute key="numberOfWorkers" value="4"/>
<booleanAttribute key="recover" value="false"/>
<stringAttribute key="result.mail.address" value=""/>
<intAttribute key="simuAril" value="-1"/>
<intAttribute key="simuDepth" value="100"/>
<intAttribute key="simuSeed" value="-1"/>
<stringAttribute key="specName" value="replicated"/>
<stringAttribute key="tlcResourcesProfile" value="local custom"/>
<stringAttribute key="view" value=""/>
<booleanAttribute key="visualizeStateGraph" value="false"/>
</launchConfiguration>

View File

@@ -0,0 +1,58 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
<stringAttribute key="TLCCmdLineParameters" value=""/>
<intAttribute key="collectCoverage" value="1"/>
<stringAttribute key="configurationName" value="Model_1_SnapShot_1737299744229"/>
<booleanAttribute key="deferLiveness" value="false"/>
<intAttribute key="dfidDepth" value="100"/>
<booleanAttribute key="dfidMode" value="false"/>
<intAttribute key="distributedFPSetCount" value="0"/>
<stringAttribute key="distributedNetworkInterface" value="100.65.224.26"/>
<intAttribute key="distributedNodesCount" value="1"/>
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
<intAttribute key="fpBits" value="1"/>
<intAttribute key="fpIndex" value="119"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="25"/>
<intAttribute key="maxSetSize" value="1000000"/>
<booleanAttribute key="mcMode" value="true"/>
<stringAttribute key="modelBehaviorInit" value=""/>
<stringAttribute key="modelBehaviorNext" value=""/>
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
<intAttribute key="modelBehaviorSpecType" value="1"/>
<stringAttribute key="modelBehaviorVars" value="pageserver_state, broker_state, safekeeper_state"/>
<stringAttribute key="modelComments" value=""/>
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
<listAttribute key="modelCorrectnessInvariants"/>
<listAttribute key="modelCorrectnessProperties">
<listEntry value="1EventuallyLaggingSkIsNotPreferredSk"/>
</listAttribute>
<intAttribute key="modelEditorOpenTabs" value="14"/>
<stringAttribute key="modelExpressionEval" value=""/>
<stringAttribute key="modelParameterActionConstraint" value=""/>
<listAttribute key="modelParameterConstants">
<listEntry value="brokers;;{b1, b2, b3};1;1"/>
<listEntry value="NULL;;NULL;1;0"/>
<listEntry value="safekeepers;;{s1, s2, s3};1;1"/>
<listEntry value="pageservers;;{p1, p2};1;1"/>
<listEntry value="max_commit_lsn;;2;0;0"/>
<listEntry value="az_mapping;;[ az1 |-&gt; {b1,s1,p1} , az2 |-&gt; {b2,s2,p2} , az3 |-&gt; {b3,s3}];0;0"/>
<listEntry value="azs;;{az1, az2, az3};1;1"/>
</listAttribute>
<stringAttribute key="modelParameterContraint" value="StateConstraint"/>
<listAttribute key="modelParameterDefinitions"/>
<stringAttribute key="modelParameterModelValues" value="{}"/>
<stringAttribute key="modelParameterNewDefinitions" value=""/>
<intAttribute key="modelVersion" value="20191005"/>
<intAttribute key="numberOfWorkers" value="4"/>
<booleanAttribute key="recover" value="false"/>
<stringAttribute key="result.mail.address" value=""/>
<intAttribute key="simuAril" value="-1"/>
<intAttribute key="simuDepth" value="100"/>
<intAttribute key="simuSeed" value="-1"/>
<stringAttribute key="specName" value="replicated"/>
<stringAttribute key="tlcResourcesProfile" value="local custom"/>
<stringAttribute key="view" value=""/>
<booleanAttribute key="visualizeStateGraph" value="false"/>
</launchConfiguration>

View File

@@ -0,0 +1,58 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
<stringAttribute key="TLCCmdLineParameters" value=""/>
<intAttribute key="collectCoverage" value="1"/>
<stringAttribute key="configurationName" value="Model_1_SnapShot_1737301172627"/>
<booleanAttribute key="deferLiveness" value="false"/>
<intAttribute key="dfidDepth" value="100"/>
<booleanAttribute key="dfidMode" value="false"/>
<intAttribute key="distributedFPSetCount" value="0"/>
<stringAttribute key="distributedNetworkInterface" value="100.65.224.26"/>
<intAttribute key="distributedNodesCount" value="1"/>
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
<intAttribute key="fpBits" value="1"/>
<intAttribute key="fpIndex" value="119"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="25"/>
<intAttribute key="maxSetSize" value="1000000"/>
<booleanAttribute key="mcMode" value="true"/>
<stringAttribute key="modelBehaviorInit" value=""/>
<stringAttribute key="modelBehaviorNext" value=""/>
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
<intAttribute key="modelBehaviorSpecType" value="1"/>
<stringAttribute key="modelBehaviorVars" value="pageserver_state, broker_state, safekeeper_state"/>
<stringAttribute key="modelComments" value=""/>
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
<listAttribute key="modelCorrectnessInvariants"/>
<listAttribute key="modelCorrectnessProperties">
<listEntry value="1EventuallyLaggingSkIsNotPreferredSk"/>
</listAttribute>
<intAttribute key="modelEditorOpenTabs" value="14"/>
<stringAttribute key="modelExpressionEval" value=""/>
<stringAttribute key="modelParameterActionConstraint" value=""/>
<listAttribute key="modelParameterConstants">
<listEntry value="brokers;;{b1, b2, b3};1;1"/>
<listEntry value="NULL;;NULL;1;0"/>
<listEntry value="safekeepers;;{s1, s2, s3};1;1"/>
<listEntry value="pageservers;;{p1, p2};1;1"/>
<listEntry value="max_commit_lsn;;2;0;0"/>
<listEntry value="az_mapping;;[ az1 |-&gt; {b1,s1,p1} , az2 |-&gt; {b2,s2,p2} , az3 |-&gt; {b3,s3}];0;0"/>
<listEntry value="azs;;{az1, az2, az3};1;1"/>
</listAttribute>
<stringAttribute key="modelParameterContraint" value="StateConstraint"/>
<listAttribute key="modelParameterDefinitions"/>
<stringAttribute key="modelParameterModelValues" value="{}"/>
<stringAttribute key="modelParameterNewDefinitions" value=""/>
<intAttribute key="modelVersion" value="20191005"/>
<intAttribute key="numberOfWorkers" value="4"/>
<booleanAttribute key="recover" value="false"/>
<stringAttribute key="result.mail.address" value=""/>
<intAttribute key="simuAril" value="-1"/>
<intAttribute key="simuDepth" value="100"/>
<intAttribute key="simuSeed" value="-1"/>
<stringAttribute key="specName" value="replicated"/>
<stringAttribute key="tlcResourcesProfile" value="local custom"/>
<stringAttribute key="view" value=""/>
<booleanAttribute key="visualizeStateGraph" value="false"/>
</launchConfiguration>

View File

@@ -0,0 +1,58 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
<stringAttribute key="TLCCmdLineParameters" value=""/>
<intAttribute key="collectCoverage" value="1"/>
<stringAttribute key="configurationName" value="Model_1_SnapShot_1737301223409"/>
<booleanAttribute key="deferLiveness" value="false"/>
<intAttribute key="dfidDepth" value="100"/>
<booleanAttribute key="dfidMode" value="false"/>
<intAttribute key="distributedFPSetCount" value="0"/>
<stringAttribute key="distributedNetworkInterface" value="100.65.224.26"/>
<intAttribute key="distributedNodesCount" value="1"/>
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
<intAttribute key="fpBits" value="1"/>
<intAttribute key="fpIndex" value="119"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="25"/>
<intAttribute key="maxSetSize" value="1000000"/>
<booleanAttribute key="mcMode" value="true"/>
<stringAttribute key="modelBehaviorInit" value=""/>
<stringAttribute key="modelBehaviorNext" value=""/>
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
<intAttribute key="modelBehaviorSpecType" value="1"/>
<stringAttribute key="modelBehaviorVars" value="pageserver_state, broker_state, safekeeper_state"/>
<stringAttribute key="modelComments" value=""/>
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
<listAttribute key="modelCorrectnessInvariants"/>
<listAttribute key="modelCorrectnessProperties">
<listEntry value="1EventuallyLaggingSkIsNotPreferredSk"/>
</listAttribute>
<intAttribute key="modelEditorOpenTabs" value="14"/>
<stringAttribute key="modelExpressionEval" value=""/>
<stringAttribute key="modelParameterActionConstraint" value=""/>
<listAttribute key="modelParameterConstants">
<listEntry value="brokers;;{b1, b2, b3};1;1"/>
<listEntry value="NULL;;NULL;1;0"/>
<listEntry value="safekeepers;;{s1, s2, s3};1;1"/>
<listEntry value="pageservers;;{p1, p2};1;1"/>
<listEntry value="max_commit_lsn;;2;0;0"/>
<listEntry value="az_mapping;;[ az1 |-&gt; {b1,s1,p1} , az2 |-&gt; {b2,s2,p2} , az3 |-&gt; {b3,s3}];0;0"/>
<listEntry value="azs;;{az1, az2, az3};1;1"/>
</listAttribute>
<stringAttribute key="modelParameterContraint" value="StateConstraint"/>
<listAttribute key="modelParameterDefinitions"/>
<stringAttribute key="modelParameterModelValues" value="{}"/>
<stringAttribute key="modelParameterNewDefinitions" value=""/>
<intAttribute key="modelVersion" value="20191005"/>
<intAttribute key="numberOfWorkers" value="4"/>
<booleanAttribute key="recover" value="false"/>
<stringAttribute key="result.mail.address" value=""/>
<intAttribute key="simuAril" value="-1"/>
<intAttribute key="simuDepth" value="100"/>
<intAttribute key="simuSeed" value="-1"/>
<stringAttribute key="specName" value="replicated"/>
<stringAttribute key="tlcResourcesProfile" value="local custom"/>
<stringAttribute key="view" value=""/>
<booleanAttribute key="visualizeStateGraph" value="false"/>
</launchConfiguration>