Skip to content

Commit 4e227ab

Browse files
lemmylemmy
committed
v38 (Statistics): WIP
1 parent ea02b87 commit 4e227ab

File tree

3 files changed

+263
-0
lines changed

3 files changed

+263
-0
lines changed

‎BlockingQueuePoisonApple_stats.R‎

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
#!/usr/bin/env Rscript
2+
args = commandArgs(trailingOnly=TRUE)
3+
4+
library(ggplot2)
5+
library(stringr)
6+
library(svglite)
7+
8+
data <- read.csv(header=TRUE, sep = ",", file = args[1])
9+
10+
## Poor-mans version of grouping the data according to 'P', 'B', and 'C' by concatenating the 0-padded values.
11+
data <- within(data, config <- paste(sep = "/", str_pad(data$P, 3, pad = "0"), str_pad(data$C, 3, pad = "0"),str_pad(data$B, 3, pad = "0")))
12+
13+
## Group data by the 'config' column and calculate mean for 'over' and 'under'.
14+
ag.means <- aggregate(cbind(data$over, data$under), by=list(config=data$config), FUN=mean)
15+
names(ag.means)[names(ag.means)=="V1"] <- "mean_over"
16+
names(ag.means)[names(ag.means)=="V2"] <- "mean_under"
17+
18+
## Group data by the 'config' column and calculate standard deviation for 'over' and 'under'.
19+
ag.sd <- aggregate(cbind(data$over, data$under), by=list(config=data$config), FUN=sd)
20+
names(ag.sd)[names(ag.sd)=="V1"] <- "sd_over"
21+
names(ag.sd)[names(ag.sd)=="V2"] <- "sd_under"
22+
23+
## Merge the two data frames by the common 'config' column.
24+
df <- merge(ag.means, ag.sd)
25+
26+
p <- ggplot(df, aes(x = config, y = mean_over, fill = config)) +
27+
geom_errorbar(aes(ymin=mean_over-sd_over, ymax=mean_over+sd_over), width=.2, position=position_dodge(.9)) +
28+
geom_bar(stat = "identity") +
29+
geom_bar(aes(x= config, y = mean_under, fill=config), stat="identity",position="dodge") +
30+
geom_errorbar(aes(ymin=mean_under-sd_under, ymax=mean_under+sd_under), width=.2, position=position_dodge(.9)) +
31+
geom_hline(yintercept = 0, alpha = 0.3) +
32+
#scale_x_discrete(guide = guide_axis(n.dodge=3))+
33+
scale_x_discrete(guide = guide_axis(check.overlap = TRUE))+
34+
coord_flip() +
35+
theme_minimal() +
36+
theme(legend.position = "none") +
37+
labs(
38+
x = "Configuration |P|/|C|/B",
39+
y = "Average under- and over-provisioning of consumers (positive |ac|>|ap|)",
40+
title = paste(
41+
"Traces:", nrow(data), format(Sys.time(), "(%a %b %d %X %Y)")
42+
)
43+
)
44+
ggsave(gsub(".csv$", ".svg", args[1]), plot = last_plot(), bg = "white", device = "svg")

‎BlockingQueuePoisonApple_stats.tla‎

Lines changed: 156 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,156 @@
1+
-------------------- MODULE BlockingQueuePoisonApple_stats -------------------
2+
EXTENDS BlockingQueuePoisonApple, CSV, TLC, TLCExt, Integers, IOUtils
3+
4+
Max(a,b) ==
5+
IF a > b THEN a ELSE b
6+
7+
Min(a,b) ==
8+
IF a < b THEN a ELSE b
9+
10+
-----------------------------------------------------------------------------
11+
12+
\* Collecting statistics does not work with an ordinary TLA+ spec such as
13+
\* BlockingQueuePoisonApple because of its non-determinism. The statistics
14+
\* would be all over the board and not meaningful. Instead, we break the
15+
\* non-determinism by mimiking a real-world workload s.t. each Producer adds
16+
\* a (fixed) number of elements to the queue. In other words, we remove
17+
\* those behaviors from the state space that we do not expect to see in the
18+
\* executions of an implementation of the TLA+ spec.
19+
\* It would be more convenient to conjoin a liveness property that stipulates
20+
\* that each producer adds N elements to the queue instead of amending the
21+
\* original next-state relation Next with SNext below. However, I don't
22+
\* see a way to get around adding the (auxiliary) pending variable that keeps
23+
\* track of the number of elements added by each producer.
24+
\* Alternatively, a more variable approach, compared to producers adding a
25+
\* fixed number of elements to the queue, would be to add probabilities that
26+
\* model the likelyhood of a Put and Terminate actions to occur (with
27+
\* Put having a much higher probability). This is straighforward to model
28+
\* with TLC's RandomElement operator by conjoining it to Put and
29+
\* Terminate:
30+
\* RandomElement(1..10) \in 1..9
31+
\* and
32+
\* RandomElement(1..10) \in 10..10
33+
\* A more sophisticated example is at
34+
\* https://github.com/lemmy/PageQueue/blob/master/PageQueue.tla
35+
36+
\* Number of elements to put into the queue by each producer.
37+
CONSTANT Work
38+
ASSUME Work \in (Nat \ {0})
39+
40+
\* Count how many elements have been added by each producer. This variable
41+
\* is how we model workloads.
42+
VARIABLES pending
43+
auxVars == <<pending>>
44+
45+
\* The two auxilary variables are used to measure the over- and under-provisioning
46+
\* of consumers.
47+
\* TODO: Make Welford's algorithm for variance and standard deviation available
48+
\* here (https://en.wikipedia.org/wiki/Algorithms_for_calculating_variance#Welford's_online_algorithm)
49+
\* It would free users from doing things in R, ... , and probably be useful
50+
\* in 99% of collecting statistics.
51+
VARIABLE over, under
52+
statsVars == <<over, under>>
53+
54+
STypeInv ==
55+
/\ pending \in [ Producers -> 0..Work ]
56+
/\ over \in Int
57+
/\ under \in Int
58+
59+
SInit ==
60+
\* Verbatim copy (redundant) of the original spec.
61+
/\ buffer = <<>>
62+
/\ waitSet = {}
63+
/\ cons = [ c \in Consumers |-> Cardinality(Producers) ]
64+
/\ prod = [ p \in Producers |-> Cardinality(Consumers) ]
65+
\* Workload:
66+
/\ pending = [ p \in Producers |-> Work ]
67+
\* Statistics:
68+
/\ over = 0
69+
/\ under = 0
70+
71+
SNext ==
72+
/\ \/ \E p \in Producers: /\ Put(p, p)
73+
\* Decrement pending iff the buffer changed.
74+
/\ IF buffer # buffer'
75+
THEN pending' = [pending EXCEPT ![p]=@-1]
76+
ELSE UNCHANGED pending
77+
\/ \E c \in Consumers: /\ Get(c)
78+
/\ UNCHANGED pending
79+
\* Update the statistics.
80+
/\ over' = Max(over, Cardinality(ac) - Cardinality(ap))
81+
/\ under' = Min(under, Cardinality(ac) - Cardinality(ap))
82+
83+
StatsSpec ==
84+
SInit /\ [][SNext]_<<vars, auxVars, statsVars>>
85+
86+
-----------------------------------------------------------------------------
87+
88+
CONSTANT CSVFile
89+
90+
StatsInv ==
91+
\* Per-behavior stats written to CSVfile on global termination. Global
92+
\* termination is defined by the union of the active producers and consumers
93+
\* being the empty set.
94+
/\ (ap \cup ac = {}) =>
95+
CSVWrite("%1$s,%2$s,%3$s,%4$s,%5$s,%6$s,%7$s",
96+
<<
97+
\* TLCGet("stats").traces equals the number of traces generated
98+
\* so far. Thus, individual records in the CSV can be aggregated
99+
\* later. TLCGet("level") can be seen as the timestamp of the
100+
\* record.
101+
TLCGet("stats").traces, TLCGet("level"),
102+
\*
103+
Cardinality(Producers), Cardinality(Consumers), BufCapacity,
104+
\* ...the actual statistics.
105+
over, under
106+
>>, CSVFile)
107+
108+
-----------------------------------------------------------------------------
109+
110+
\* Below, we read the values from the OS environment and turn them into constants
111+
\* of this spec. The operators s2n and SetOfNModelValues should probably be
112+
\* moved into IOUtils.
113+
114+
s2n(str) ==
115+
CHOOSE n \in 0..2^16: ToString(n) = str
116+
117+
SetOfNModelValues(lbl, N) ==
118+
{ TLCModelValue(lbl \o ToString(i)) : i \in 1..N }
119+
120+
-----------------------------------------------------------------------------
121+
122+
B ==
123+
s2n(IOEnv.B)
124+
125+
P ==
126+
SetOfNModelValues("p", s2n(IOEnv.P))
127+
128+
C ==
129+
SetOfNModelValues("c", s2n(IOEnv.C))
130+
131+
W ==
132+
s2n(IOEnv.W)
133+
134+
Out ==
135+
IOEnv.Out
136+
137+
===========================================================================
138+
139+
--------------------- CONFIG BlockingQueuePoisonApple_stats ---------------------
140+
CONSTANTS
141+
BufCapacity <- B
142+
Producers <- P
143+
Consumers <- C
144+
Work <- W
145+
CSVFile <- Out
146+
Poison = Poison
147+
148+
SPECIFICATION StatsSpec
149+
150+
CHECK_DEADLOCK FALSE
151+
152+
INVARIANT STypeInv
153+
154+
INVARIANT StatsInv
155+
156+
=============================================================================

‎BlockingQueuePoisonApple_statsSC.tla‎

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
--------------------- MODULE BlockingQueuePoisonApple_statsSC ---------------------
2+
EXTENDS TLC, IOUtils, Naturals, Sequences, CSV
3+
4+
\* Assume a recent version of TLC that has support for all shenanigans below.
5+
ASSUME TLCGet("revision").timestamp >= 1628118195
6+
7+
-----------------------------------------------------------------------------
8+
9+
\* Filename for the CSV file that appears also in the R script and is passed
10+
\* to the nested TLC instances that are forked below.
11+
CSVFile ==
12+
"BQPA_B_" \o ToString(JavaTime) \o ".csv"
13+
14+
\* Write column headers to CSV file at startup of TLC instance that "runs"
15+
\* this script and forks the nested instances of TLC that simulate the spec
16+
\* and collect the statistics.
17+
ASSUME
18+
CSVWrite("trace,level,P,C,B,over,under", <<>>, CSVFile)
19+
20+
PlotStatistics ==
21+
\* Have TLC execute the R script on the generated CSV file.
22+
LET proc == IOExec(<<
23+
\* Find R on the current system (known to work on macOS and Linux).
24+
"/usr/bin/env", "Rscript",
25+
"BlockingQueuePoisonApple_stats.R", CSVFile>>)
26+
IN \/ proc.exitValue = 0
27+
\/ PrintT(proc) \* Print stdout and stderr if R script fails.
28+
29+
-----------------------------------------------------------------------------
30+
31+
\* Command to fork nested TLC instances that simulate the spec and collect the
32+
\* statistics. TLCGet("config").install gives the path to the TLC jar also
33+
\* running this script.
34+
Cmd == LET absolutePathOfTLC == TLCGet("config").install
35+
IN <<"java", "-jar",
36+
absolutePathOfTLC,
37+
"-generate", "num=100",
38+
"-config", "BlockingQueuePoisonApple_stats.tla",
39+
"BlockingQueuePoisonApple_stats">>
40+
41+
Success(e) ==
42+
/\ PrintT(e)
43+
/\ PlotStatistics
44+
45+
ASSUME \A conf \in
46+
{ r \in [ {"P","C","B"} -> {1,2,4,8,16,32}]:
47+
\* Check only symmetric configs of Producers and Consumers.
48+
\* Over/Under-provisioning for asymmetrics numbers of
49+
\* Producers and Consumers.
50+
r.P = r.C }:
51+
LET ret == IOEnvExec(conf @@ [W |-> 16, Out |-> CSVFile], Cmd).exitValue
52+
IN CASE ret = 0 -> Success(conf)
53+
[] ret = 10 -> PrintT(<<conf, "Assumption violation">>)
54+
[] ret = 12 -> PrintT(<<conf, "Safety violation">>)
55+
[] ret = 13 -> PrintT(<<conf, "Liveness violation">>)
56+
[] OTHER -> Print(<<conf, IOEnvExec(conf, Cmd), "Error">>, FALSE)
57+
58+
=============================================================================
59+
---- CONFIG BlockingQueuePoisonAppleSC ----
60+
\* TLC always expects a configuration file, but an empty one will do in this case.
61+
\* If this approach proves useful, TLC should be extended to launch without a config
62+
\* file.
63+
====

0 commit comments

Comments
 (0)