Bias random simulation to forward-progress actions. (#4658)

tla/.gitignore

@@ -4,3 +4,8 @@ tools/
 *.out
 *.toolbox/
 *.tlaps/
+.Rproj.user/
+.RData
+.Rhistory
+*.Rproj
+.DS_Store

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))
+

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

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]_<<vars, conf>>
+
+------------------------------------------------------------------------------
+
+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))
+=============================================================================

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
+    done