Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Adjust the probabilities based on empirical data to achieve less uneven coverage of the action space during simulation #6562

Merged
merged 4 commits into from
Oct 15, 2024
Merged

Adjust the probabilities based on empirical data to achieve less uneven coverage of the action space during simulation #6562

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
8622249
Collect (more detailed) extended statistics from N independent simula…
lemmy Oct 10, 2024
59922ca
Change StopAfter from a state constraint to a periodic hook.
lemmy Oct 10, 2024
4847693
Adjust the probabilities based on empirical data to achieve less unev…
lemmy Oct 10, 2024
6ea22ff
Update tla/consensus/SIMCoverageccfraft.tla
lemmy Oct 15, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 0 additions & 18 deletions tla/consensus/SIMCoverageccfraft.R
View file
Open in desktop

This file was deleted.

49 changes: 0 additions & 49 deletions tla/consensus/SIMCoverageccfraft.cfg
View file
Open in desktop

This file was deleted.

87 changes: 31 additions & 56 deletions tla/consensus/SIMCoverageccfraft.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,65 +1,40 @@
---------- MODULE SIMCoverageccfraft ----------
EXTENDS ccfraft, TLC, Integers, CSV, TLCExt

CONSTANTS
NodeOne, NodeTwo, NodeThree, NodeFour, NodeFive
$ wget https://nightly.tlapl.us/dist/tla2tools.jar
$ wget https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar
## Run with as many workers as you like to parallelize the nested simulation runs (auto uses all your cores).
$ java -jar tla2tools.jar -config SIMCoverageccfraft.tla SIMCoverageccfraft.tla -workers auto

Servers_mc == {NodeOne, NodeTwo, NodeThree, NodeFour, NodeFive}
----------------------------- MODULE SIMCoverageccfraft -----------------------------
EXTENDS TLC, Naturals, Sequences, IOUtils

Baseline ==
{<<"Next", 0..0, 0..0, 0..0>>}
CmdLine ==
<<"sh", "-c",
lemmy marked this conversation as resolved.
Show resolved Hide resolved
"java " \o
"-XX:+UseParallelGC " \o
"-Dtlc2.tool.impl.Tool.cdot=true " \o
"-Dtlc2.tool.Simulator.extendedStatistics=true " \o
"-jar tla2tools.jar " \o
"-depth 1000 " \o
"-simulate SIMccfraft.tla >> SIMCoverageccfraft.txt 2>&1">>

Confs ==
Baseline \cup
({"SIMNext"} \X {1..1, 1..10, 1..100} \X {201..201, 201..210, 201..300} \X {401..401, 401..410, 401..500})
-----------------------------------------------------------------------------

VARIABLE conf
VARIABLE c, d

CCF == INSTANCE ccfraft
Init ==
/\ c \in [ R: {10, 1000}, C: {10, 1000}, Q: {10, 1000}, T: {10, 1000} ]
/\ d = FALSE

SIMInitReconfigurationVars ==
\/ CCF!InitLogConfigServerVars(Servers, JoinedLog)
\/ CCF!InitReconfigurationVars
Next ==
/\ ~d
/\ d' = TRUE
/\ PrintT(<<"conf", c>>)
/\ IOEnvExec(c, CmdLine).exitValue = 0
/\ UNCHANGED c

SIMCheckQuorum(i) ==
/\ conf[1] # "Next" => RandomElement(1..1000) \in conf[3]
/\ CCF!CheckQuorum(i)

SIMChangeConfigurationInt(i, newConfiguration) ==
/\ conf[1] # "Next" => RandomElement(1..1000) \in conf[4]
/\ CCF!ChangeConfigurationInt(i, newConfiguration)

SIMTimeout(i) ==
/\ \/ RandomElement(1..1000) \in conf[2]
\/ conf[1] # "Next"
\* Always allow Timeout if no messages are in the network
\* and no node is a candidate or leader. Otherwise, the system
\* will deadlock if 1 # RandomElement(...).
\/ /\ \A s \in Servers: leadershipState[s] \notin {Leader, Candidate}
/\ Network!Messages = {}
/\ CCF!Timeout(i)

SIMCoverageSpec ==
/\ Init
/\ conf \in Confs
/\ [][UNCHANGED conf /\ Next]_<<vars, conf>>

------------------------------------------------------------------------------

CSVFile == "SIMCoverageccfraft_S" \o ToString(Cardinality(Servers)) \o ".csv"

CSVColumnHeaders ==
"Spec#P#Q#R#currentTerm#state#commitIndex#log#node"

ASSUME
CSVRecords(CSVFile) = 0 =>
CSVWrite(CSVColumnHeaders, <<>>, CSVFile)

StatisticsStateConstraint ==
(TLCGet("level") > TLCGet("config").depth) =>
TLCDefer(\A s \in Servers : CSVWrite("%1$s#%2$s#%3$s#%4$s#%5$s#%6$s#%7$s#%8$s#%9$s",
<< conf[1], Cardinality(conf[2]), Cardinality(conf[3]), Cardinality(conf[4]),
currentTerm[s], leadershipState[s], commitIndex[s], Len(log[s]), s
>>,
CSVFile))
=============================================================================
---- CONFIG SIMCoverageccfraft ----
INIT Init
NEXT Next
CHECK_DEADLOCK FALSE
====
5 changes: 3 additions & 2 deletions tla/consensus/SIMccfraft.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,7 @@ CONSTANTS
Timeout <- SIMTimeout
ChangeConfigurationInt <-SIMChangeConfigurationInt
CheckQuorum <- SIMCheckQuorum
ClientRequest <- SIMClientRequest

Fairness <- SIMFairness

Expand All @@ -50,8 +51,8 @@ CONSTANTS
Extend <- [abs]ABSExtend
CopyMaxAndExtend <- [abs]ABSCopyMaxAndExtend

CONSTRAINT
StopAfter
_PERIODIC
Periodically

CHECK_DEADLOCK
FALSE
Expand Down
41 changes: 35 additions & 6 deletions tla/consensus/SIMccfraft.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
---------- MODULE SIMccfraft ----------
EXTENDS ccfraft, TLC, Integers, IOUtils, MCAliases
EXTENDS ccfraft, TLC, Integers, IOUtils

CONSTANTS
NodeOne, NodeTwo, NodeThree, NodeFour, NodeFive
Expand All @@ -16,16 +16,32 @@ SIMInitReconfigurationVars ==
\* Start with any subset of servers in the active configuration.
\/ CCF!InitReconfigurationVars

LOCAL R ==
1..IF "R" \in DOMAIN IOEnv THEN atoi(IOEnv.R) ELSE 10
lemmy marked this conversation as resolved.
Show resolved Hide resolved

SIMClientRequest(i) ==
/\ 1 = RandomElement(R)
/\ CCF!ClientRequest(i)

LOCAL Q ==
1..IF "Q" \in DOMAIN IOEnv THEN atoi(IOEnv.Q) ELSE 10

SIMCheckQuorum(i) ==
/\ 1 = RandomElement(1..10)
/\ 1 = RandomElement(Q)
/\ CCF!CheckQuorum(i)

LOCAL C ==
1..IF "C" \in DOMAIN IOEnv THEN atoi(IOEnv.C) ELSE 10

SIMChangeConfigurationInt(i, newConfiguration) ==
/\ 1 = RandomElement(1..100)
/\ 1 = RandomElement(C)
/\ CCF!ChangeConfigurationInt(i, newConfiguration)

LOCAL T ==
1..IF "T" \in DOMAIN IOEnv THEN atoi(IOEnv.T) ELSE 1000

SIMTimeout(i) ==
/\ \/ 1 = RandomElement(1..100)
/\ \/ 1 = RandomElement(T)
\* Always allow Timeout if no messages are in the network
\* and no node is a candidate or leader. Otherwise, the system
\* will deadlock if 1 # RandomElement(...).
Expand Down Expand Up @@ -58,13 +74,26 @@ SIMFairness ==
\E newConfiguration \in SUBSET(Servers) \ {{}}:
WF_vars(CCF!ChangeConfigurationInt(s, newConfiguration))

\* The state constraint StopAfter stops TLC after the alloted
----

\* StopAfter stops TLC after the alloted
\* time budget is up, unless TLC encounters an error first.
StopAfter ==
LET timeout == IF ("SIM_TIMEOUT" \in DOMAIN IOEnv) /\ IOEnv.SIM_TIMEOUT # "" THEN atoi(IOEnv.SIM_TIMEOUT) ELSE 1200
(* The smoke test has a time budget of 20 minutes. *)
IN TLCSet("exit", TLCGet("duration") > timeout)

SerializeFilename ==
"SIMccfraft_" \o "R-" \o ToString(R) \o "_T-" \o ToString(T) \o "_Q-" \o ToString(Q) \o "_C-" \o ToString(C) \o "_ts-" \o ToString(JavaTime) \o ".ndjson"

SerializeTLCStats ==
Serialize(<<TLCGet("stats")>>, SerializeFilename, [format |-> "NDJSON", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "APPEND">>])

Periodically ==
/\ StopAfter
/\ SerializeTLCStats

----

DebugInvUpToDepth ==
\* The following invariant causes TLC to terminate with a counterexample of length
\* -depth after generating the first trace.
Expand Down