From 1e2708f7c504ca4eb91d9dfaf756c5793e369702 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Thu, 1 Dec 2022 10:21:49 -0800 Subject: [PATCH] Bias random simulation to forward-progress actions. (#4658) --- tla/.gitignore | 5 ++++ tla/SIMCoverageccfraft.R | 26 ++++++++++++++++++ tla/SIMCoverageccfraft.cfg | 32 ++++++++++++++++++++++ tla/SIMCoverageccfraft.tla | 54 ++++++++++++++++++++++++++++++++++++++ tla/SIMccfraft.tla | 29 +++++++++++++------- 5 files changed, 136 insertions(+), 10 deletions(-) create mode 100644 tla/SIMCoverageccfraft.R create mode 100644 tla/SIMCoverageccfraft.cfg create mode 100644 tla/SIMCoverageccfraft.tla diff --git a/tla/.gitignore b/tla/.gitignore index f86b75fb34cb..02be2aeac69a 100644 --- a/tla/.gitignore +++ b/tla/.gitignore @@ -4,3 +4,8 @@ tools/ *.out *.toolbox/ *.tlaps/ +.Rproj.user/ +.RData +.Rhistory +*.Rproj +.DS_Store \ No newline at end of file diff --git a/tla/SIMCoverageccfraft.R b/tla/SIMCoverageccfraft.R new file mode 100644 index 000000000000..a404c82c614b --- /dev/null +++ b/tla/SIMCoverageccfraft.R @@ -0,0 +1,26 @@ +require(ggplot2) +require(dplyr) + +df <- unique(read.csv(header = TRUE, sep = "#", file = "./SIMCoverageccfraft_S5.csv")) + +# Add a column to df that combines the three columns Spec, P, and C. +df$SpecP <- paste(df$Spec, df$P, df$Q, df$R, sep = "_") + +# Eyeball if all configurations are roughly equally represented. +df %>% group_by(SpecP) %>% summarize(count = n()) + +# Print configurations where leaders retire. +df %>% + group_by(SpecP, state) %>% + summarize(count = n()) %>% + filter(state == "RetiredLeader") + +# Count the occurrences of each character sequence in column state +# grouped by column SpecP. +df %>% + group_by(SpecP, state) %>% + summarize(count = n()) %>% + ggplot(aes(x=SpecP, fill=state, y=count)) + + geom_bar(stat="identity") + + theme(axis.text.x = element_text(angle = 90, vjust = 0.5, hjust=1)) + diff --git a/tla/SIMCoverageccfraft.cfg b/tla/SIMCoverageccfraft.cfg new file mode 100644 index 000000000000..326dd390e73c --- /dev/null +++ b/tla/SIMCoverageccfraft.cfg @@ -0,0 +1,32 @@ +SPECIFICATION SIMCoverageSpec + +CONSTANTS + Servers <- Servers_mc + + Nil = Nil + + Follower = Follower + Candidate = Candidate + Leader = Leader + RetiredLeader = RetiredLeader + Pending = Pending + + RequestVoteRequest = RequestVoteRequest + RequestVoteResponse = RequestVoteResponse + AppendEntriesRequest = AppendEntriesRequest + AppendEntriesResponse = AppendEntriesResponse + NotifyCommitMessage = NotifyCommitMessage + + TypeEntry = Entry + TypeSignature = Signature + TypeReconfiguration = Reconfiguration + + NodeOne = n1 + NodeTwo = n2 + NodeThree = n3 + NodeFour = n4 + NodeFive = n5 + + +CONSTRAINT + StatisticsStateConstraint diff --git a/tla/SIMCoverageccfraft.tla b/tla/SIMCoverageccfraft.tla new file mode 100644 index 000000000000..17e5aa628036 --- /dev/null +++ b/tla/SIMCoverageccfraft.tla @@ -0,0 +1,54 @@ +---------- MODULE SIMCoverageccfraft ---------- +EXTENDS SIMccfraft, TLC, Integers, CSV, TLCExt + +Baseline == + {<<"Next", 0..0, 0..0, 0..0>>} + +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 + +SIMCoverageNext == + \* To increase coverage, favor sub-actions during simulation that move the + \* system state forward. + LET rnd == RandomElement(1..1000) + \* TODO Evaluating ENABLED is a performance bottleneck. An upcoming + \* TODO change in TLC should remove the need for ENABLED to prevent + \* TODO deadlocks. + \* An orthogonal problem is that TLC does not split the next-state + \* relation into multiple Action instances, which would allow us to + \* collect sub-action level statistics to assess coverage. With SIMNext, + \* TLC's statistics reports only the number of SIMNext steps in behaviors. + IN + CASE rnd \in conf[2] /\ ENABLED TO -> TO + [] rnd \in conf[3] /\ ENABLED CQ -> CQ + [] rnd \in conf[4] /\ ENABLED CC -> CC + [] OTHER -> IF ENABLED Forward THEN Forward ELSE Next + +SIMCoverageSpec == + /\ Init + /\ conf \in Confs + /\ [][UNCHANGED conf /\ IF conf[1] = "SIMNext" THEN SIMCoverageNext ELSE Next]_<> + +------------------------------------------------------------------------------ + +CSVFile == "SIMCoverageccfraft_S" \o ToString(Cardinality(Servers)) \o ".csv" + +CSVColumnHeaders == + "Spec#P#Q#R#reconfigurationCount#committedLog#clientRequests#commitsNotified11#commitsNotified12#currentTerm#state#node" + +ASSUME + CSVRecords(CSVFile) = 0 => + CSVWrite(CSVColumnHeaders, <<>>, CSVFile) + +StatisticsStateConstraint == + (TLCGet("level") > TLCGet("config").depth) => + TLCDefer(\A srv \in Servers : CSVWrite("%1$s#%2$s#%3$s#%4$s#%5$s#%6$s#%7$s#%8$s#%9$s#%10$s#%11$s#%12$s", + << conf[1], Cardinality(conf[2]), Cardinality(conf[3]), Cardinality(conf[4]), + reconfigurationCount, committedLog.index, clientRequests, + commitsNotified[srv][1], commitsNotified[srv][2], + currentTerm[srv], state[srv], srv>>, + CSVFile)) +============================================================================= diff --git a/tla/SIMccfraft.tla b/tla/SIMccfraft.tla index 20da29cd13fa..880511794636 100644 --- a/tla/SIMccfraft.tla +++ b/tla/SIMccfraft.tla @@ -4,10 +4,17 @@ EXTENDS ccfraft, TLC, Integers Servers_mc == {NodeOne, NodeTwo, NodeThree, NodeFour, NodeFive} ---- -Fail == - \/ \E i \in Servers : Timeout(i) - \/ \E i \in Servers : \E c \in SUBSET(Servers) : ChangeConfiguration(i, c) - \/ \E i \in Servers : CheckQuorum(i) + +CC == + \E i \in Servers : + \E c \in SUBSET(Servers) : + ChangeConfiguration(i, c) + +CQ == + \E i \in Servers : CheckQuorum(i) + +TO == + \E i \in Servers : Timeout(i) Forward == \/ \E i, j \in Servers : RequestVote(i, j) @@ -22,11 +29,13 @@ Forward == SIMNext == \* To increase coverage, favor sub-actions during simulation that move the \* system state forward. - LET rnd == RandomElement(1..100) - IN IF rnd = 1 THEN Fail - \* TODO Evaluating ENABLED Forward is a performance bottleneck. An upcoming - \* TODO change in TLC should remove the need for ENABLED Forward. - ELSE IF ENABLED Forward THEN Forward ELSE Fail + LET rnd == RandomElement(1..1000) + IN \* TODO Evaluating ENABLED A is a performance bottleneck. An upcoming + \* TODO change in TLC should remove the need for ENABLED A. + CASE rnd = 1 /\ ENABLED TO -> TO + [] rnd = 2 /\ ENABLED CQ -> CQ + [] rnd \in 10..20 /\ ENABLED CC -> CC + [] OTHER -> IF ENABLED Forward THEN Forward ELSE Next SIMSpec == Init /\ [][SIMNext]_vars @@ -61,4 +70,4 @@ $ echo 500 > depth.txt $ while true; do TS=$(date +%s) DEPTH=$(cat depth.txt) && tlc SIMccfraft -simulate -workers auto -depth $DEPTH -postcondition 'SIMPostCondition!SIMPostCondition' -dumptrace tlc SIMccfraft-$TS.bin > SIMccfraft-$TS.out && sleep 5; - done \ No newline at end of file + done