* [PATCH 0/6] formal/spinhint: Update code snippet
@ 2019-02-02 15:05 Akira Yokosawa
2019-02-02 15:08 ` [PATCH 1/6] fcvextract.pl: Treat '.spin' files as C sources Akira Yokosawa
` (6 more replies)
0 siblings, 7 replies; 16+ messages in thread
From: Akira Yokosawa @ 2019-02-02 15:05 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
Hi Paul,
Here is another round of code snippet update, with modernization
of outputs of Spin and tables of state search results.
Patch #1 updates fcvextract.pl so that .spin files are handled
as the same as C source files.
Patch #2 applies the new scheme to code snippets. It also contains
minor changes for better typesetting.
Patch #3 replaces captures of Spin outputs with those obtained
from Spin version 6.4.8. This commit adds outputs as .lst files
under CodeSamples/formal/promela/. They are added to the dependency
in the top level Makefile.
Patch #4 updates tables of Spin result. For qrcu.spin, I used
the compiler flag -DCOLLAPSE to complete the state search for
updaters=3 readers=2 on a machine with 16GB memory. As far as
I understand correctly, this compiler flag does not affect the
completeness of state search. So I added some explanation in the text
to mention the flag and the argument -mN of ./pan to increase the
limit of search depth.
Patch #5 tweaks footnote on a cell in a table.
Patch #6 is a nitpick patch to consistently use \co{}.
I'm wondering if Patch #4 is OK from your perspective.
Any feedback is welcome!
Thanks, Akira
--
Akira Yokosawa (6):
fcvextract.pl: Treat '.spin' files as C sources
formal/spinhint: Employ new scheme for code snippet
formal/spinhint: Update output lists of spin
formal/spinhint: Update tables of memory usage of Spin
formal/spinhint: Put footnote on header in table
formal/spinhint: Use \co{...} rather than {\tt ...}
CodeSamples/formal/promela/atomicincrement.spin | 2 +
.../formal/promela/atomicincrement.spin.lst | 28 +
CodeSamples/formal/promela/increment.spin | 46 +-
CodeSamples/formal/promela/increment.spin.lst | 28 +
.../formal/promela/increment.spin.trail.lst | 42 +
CodeSamples/formal/promela/lock.h | 16 +-
CodeSamples/formal/promela/lock.spin | 46 +-
CodeSamples/formal/promela/lock.spin.lst | 29 +
CodeSamples/formal/promela/qrcu.spin | 95 ++-
Makefile | 4 +-
formal/spinhint.tex | 874 ++++++---------------
perfbook.tex | 1 +
utilities/fcvextract.pl | 8 +-
13 files changed, 502 insertions(+), 717 deletions(-)
create mode 100644 CodeSamples/formal/promela/atomicincrement.spin.lst
create mode 100644 CodeSamples/formal/promela/increment.spin.lst
create mode 100644 CodeSamples/formal/promela/increment.spin.trail.lst
create mode 100644 CodeSamples/formal/promela/lock.spin.lst
--
2.7.4
^ permalink raw reply [flat|nested] 16+ messages in thread
* [PATCH 1/6] fcvextract.pl: Treat '.spin' files as C sources
2019-02-02 15:05 [PATCH 0/6] formal/spinhint: Update code snippet Akira Yokosawa
@ 2019-02-02 15:08 ` Akira Yokosawa
2019-02-02 15:09 ` [PATCH 2/6] formal/spinhint: Employ new scheme for code snippet Akira Yokosawa
` (5 subsequent siblings)
6 siblings, 0 replies; 16+ messages in thread
From: Akira Yokosawa @ 2019-02-02 15:08 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From b33a50ba42fee982662ca34001c2495d1787b4fd Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Thu, 31 Jan 2019 00:07:53 +0900
Subject: [PATCH 1/6] fcvextract.pl: Treat '.spin' files as C sources
"spin" command accepts preprocessor directives and comments of
C style. Merge the setup of regular expressions for ".spin" files
with that for C sources.
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
| 8 ++------
1 file changed, 2 insertions(+), 6 deletions(-)
--git a/utilities/fcvextract.pl b/utilities/fcvextract.pl
index f8f274b..8f5797e 100755
--- a/utilities/fcvextract.pl
+++ b/utilities/fcvextract.pl
@@ -105,7 +105,7 @@
# NOTE: "#ifdef FCV_SNIPPET" is not recognized.
# "#else" can be omitted.
#
-# Copyright (C) Akira Yokosawa, 2018
+# Copyright (C) Akira Yokosawa, 2018, 2019
#
# Authors: Akira Yokosawa <akiyks@gmail.com>
@@ -142,14 +142,10 @@ $extract_labelbase = $ARGV[1];
$begin_re = qr/\\begin\{snippet\}.*labelbase=[^,\]]*$extract_labelbase[,\]]/ ;
$end_re = qr/\\end\{snippet\}/;
-if ($src_file =~ /.*\.[ch]$/ ) {
+if ($src_file =~ /.*\.[ch]$/ || $src_file =~ /.*\.spin$/) {
$lnlbl_re = qr!(.*?)(\s*//\s*)\\lnlbl\{(.*)}\s*$!;
$lnlbl_re2 = qr!(.*?)(s*/\*\s*)\\lnlbl\{(.*)}\s*\*/(.*)$!;
$c_src = 1;
-} elsif ($src_file =~ /.*\.c$/ ) {
- $lnlbl_re = qr!(.*?)(\s*//\s*)\\lnlbl\{(.*)}\s*$!;
-} elsif ($src_file =~ /.*\.spin$/ ) {
- $lnlbl_re = qr!(.*?)(\s*//\s*)\\lnlbl\{(.*)}\s*$!;
} elsif ($src_file =~ /.*\.sh$/ ) {
$lnlbl_re = qr!(.*?)(\s*#\s*)\\lnlbl\{(.*)}\s*$!;
} elsif ($src_file =~ /.\.ltms$/ ) {
--
2.7.4
^ permalink raw reply related [flat|nested] 16+ messages in thread
* [PATCH 2/6] formal/spinhint: Employ new scheme for code snippet
2019-02-02 15:05 [PATCH 0/6] formal/spinhint: Update code snippet Akira Yokosawa
2019-02-02 15:08 ` [PATCH 1/6] fcvextract.pl: Treat '.spin' files as C sources Akira Yokosawa
@ 2019-02-02 15:09 ` Akira Yokosawa
2019-02-02 15:11 ` [PATCH 3/6] formal/spinhint: Update output lists of spin Akira Yokosawa
` (4 subsequent siblings)
6 siblings, 0 replies; 16+ messages in thread
From: Akira Yokosawa @ 2019-02-02 15:09 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From 7c319159fddc42f02836e23581a73facd5d54b47 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Thu, 31 Jan 2019 00:08:30 +0900
Subject: [PATCH 2/6] formal/spinhint: Employ new scheme for code snippet
Other than simple transformations, this commit includes the following
changes:
o Move "listing" environment to outside of "enumerate"
environment. This is to avoid slight behavior change of
"VerbatimL" environment inside "enumerate".
("VerbatimN" looks OK inside "enumerate".)
o Embed the unoptimized definition of sum_unordered into
CodeSamples/formal/promela/qrcu.spin using the
"#ifndef FCV_SNIPPET" construct, rather than putting
it in spinhint.tex. Luckily, we don't reference the
optimized definition as a code snippet.
(Related to Quick Quiz 12.3)
o Substitute white spaces for tab characters in snippets
which appear in the middle of a line.
o Enclose "do-od" and "if-fi" in \co{} macros.
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
CodeSamples/formal/promela/atomicincrement.spin | 2 +
CodeSamples/formal/promela/increment.spin | 46 +-
CodeSamples/formal/promela/lock.h | 16 +-
CodeSamples/formal/promela/lock.spin | 46 +-
CodeSamples/formal/promela/qrcu.spin | 95 ++--
formal/spinhint.tex | 681 +++++++-----------------
6 files changed, 318 insertions(+), 568 deletions(-)
diff --git a/CodeSamples/formal/promela/atomicincrement.spin b/CodeSamples/formal/promela/atomicincrement.spin
index 5f4f774..ebeedb2 100644
--- a/CodeSamples/formal/promela/atomicincrement.spin
+++ b/CodeSamples/formal/promela/atomicincrement.spin
@@ -3,6 +3,7 @@
byte counter = 0;
byte progress[NUMPROCS];
+//\begin{snippet}[labelbase=ln:formal:promela:atomicincrement:incrementer,commandchars=\\\@\$]
proctype incrementer(byte me)
{
int temp;
@@ -13,6 +14,7 @@ proctype incrementer(byte me)
}
progress[me] = 1;
}
+//\end{snippet}
init {
int i = 0;
diff --git a/CodeSamples/formal/promela/increment.spin b/CodeSamples/formal/promela/increment.spin
index d82bab1..263d4bd 100644
--- a/CodeSamples/formal/promela/increment.spin
+++ b/CodeSamples/formal/promela/increment.spin
@@ -1,40 +1,42 @@
-#define NUMPROCS 3
+//\begin{snippet}[labelbase=ln:formal:promela:increment:whole,commandchars=\\\@\$]
+#define NUMPROCS 2 //\lnlbl{nprocs}
-byte counter = 0;
-byte progress[NUMPROCS];
+byte counter = 0; //\lnlbl{count}
+byte progress[NUMPROCS]; //\lnlbl{prog}
-proctype incrementer(byte me)
+proctype incrementer(byte me) //\lnlbl{proc:b}
{
int temp;
- temp = counter;
- counter = temp + 1;
- progress[me] = 1;
-}
+ temp = counter; //\lnlbl{incr:b}
+ counter = temp + 1; //\lnlbl{incr:e}
+ progress[me] = 1; //\lnlbl{setprog}
+} //\lnlbl{proc:e}
-init {
+init { //\lnlbl{init:b}
int i = 0;
int sum = 0;
- atomic {
+ atomic { //\lnlbl{doinit:b}
i = 0;
- do
- :: i < NUMPROCS ->
+ do //\lnlbl{dood1:b}
+ :: i < NUMPROCS -> //\lnlbl{block1:b}
progress[i] = 0;
run incrementer(i);
- i++;
- :: i >= NUMPROCS -> break;
- od;
- }
- atomic {
+ i++; //\lnlbl{block1:e}
+ :: i >= NUMPROCS -> break; //\lnlbl{block2}
+ od; //\lnlbl{dood1:e}
+ } //\lnlbl{doinit:e}
+ atomic { //\lnlbl{assert:b}
i = 0;
sum = 0;
- do
+ do //\lnlbl{dood2:b}
:: i < NUMPROCS ->
sum = sum + progress[i];
i++
:: i >= NUMPROCS -> break;
- od;
- assert(sum < NUMPROCS || counter == NUMPROCS);
- }
-}
+ od; //\lnlbl{dood2:e}
+ assert(sum < NUMPROCS || counter == NUMPROCS); //\lnlbl{assert}
+ } //\lnlbl{assert:e}
+} //\lnlbl{init:e}
+//\end{snippet}
diff --git a/CodeSamples/formal/promela/lock.h b/CodeSamples/formal/promela/lock.h
index 069945d..aa046df 100644
--- a/CodeSamples/formal/promela/lock.h
+++ b/CodeSamples/formal/promela/lock.h
@@ -1,14 +1,16 @@
+//\begin{snippet}[labelbase=ln:formal:promela:lock:whole,commandchars=\!\[\]]
#define spin_lock(mutex) \
- do \
- :: 1 -> atomic { \
+ do /* \lnlbl{dood:b} */\
+ :: 1 -> atomic { /* \lnlbl{one} */\
if \
- :: mutex == 0 -> \
- mutex = 1; \
- break \
- :: else -> skip \
+ :: mutex == 0 -> /* \lnlbl{notheld} */\
+ mutex = 1; /* \lnlbl{acq} */\
+ break /* \lnlbl{break} */\
+ :: else -> skip /* \lnlbl{held} */\
fi \
} \
- od
+ od /* \lnlbl{dood:e} */
#define spin_unlock(mutex) \
mutex = 0
+//\end{snippet}
diff --git a/CodeSamples/formal/promela/lock.spin b/CodeSamples/formal/promela/lock.spin
index 0057cec..4bbcbd5 100644
--- a/CodeSamples/formal/promela/lock.spin
+++ b/CodeSamples/formal/promela/lock.spin
@@ -1,35 +1,36 @@
+//\begin{snippet}[labelbase=ln:formal:promela:lock:spin,commandchars=\\\@\$]
#include "lock.h"
-#define N_LOCKERS 3
+#define N_LOCKERS 3 //\lnlbl{nlockers}
-bit mutex = 0;
-bit havelock[N_LOCKERS];
-int sum;
+bit mutex = 0; //\lnlbl{mutex}
+bit havelock[N_LOCKERS]; //\lnlbl{array}
+int sum; //\lnlbl{sum}
-proctype locker(byte me)
+proctype locker(byte me) //\lnlbl{locker:b}
{
do
:: 1 ->
- spin_lock(mutex);
- havelock[me] = 1;
- havelock[me] = 0;
- spin_unlock(mutex)
+ spin_lock(mutex); //\lnlbl{locker:lock}
+ havelock[me] = 1; //\lnlbl{locker:claim}
+ havelock[me] = 0; //\lnlbl{locker:unclaim}
+ spin_unlock(mutex) //\lnlbl{locker:unlock}
od
-}
+} //\lnlbl{locker:e}
-init {
+init { //\lnlbl{init:b}
int i = 0;
int j;
end: do
:: i < N_LOCKERS ->
- havelock[i] = 0;
- run locker(i);
- i++
- :: i >= N_LOCKERS ->
- sum = 0;
- j = 0;
- atomic {
+ havelock[i] = 0; //\lnlbl{init:array}
+ run locker(i); //\lnlbl{init:start}
+ i++ //\lnlbl{init:next}
+ :: i >= N_LOCKERS -> //\lnlbl{init:chkassert}
+ sum = 0; //\lnlbl{init:sum}
+ j = 0; //\lnlbl{init:j}
+ atomic { //\lnlbl{init:atm:b}
do
:: j < N_LOCKERS ->
sum = sum + havelock[j];
@@ -37,8 +38,9 @@ end: do
:: j >= N_LOCKERS ->
break
od
- }
- assert(sum <= 1);
- break
+ } //\lnlbl{init:atm:e}
+ assert(sum <= 1); //\lnlbl{init:assert}
+ break //\lnlbl{init:break}
od
-}
+} //\lnlbl{init:e}
+//\end{snippet}
diff --git a/CodeSamples/formal/promela/qrcu.spin b/CodeSamples/formal/promela/qrcu.spin
index 220e135..74315c9 100644
--- a/CodeSamples/formal/promela/qrcu.spin
+++ b/CodeSamples/formal/promela/qrcu.spin
@@ -1,3 +1,4 @@
+//\begin{snippet}[labelbase=ln:formal:promela:qrcu:gvar,commandchars=\\\{\}]
#include "lock.h"
#define N_QRCU_READERS 2
@@ -7,28 +8,33 @@ bit idx = 0;
byte ctr[2];
byte readerprogress[N_QRCU_READERS];
bit mutex = 0;
+//\end{snippet}
+//\begin{snippet}[labelbase=ln:formal:promela:qrcu:reader,commandchars=\\\@\$]
proctype qrcu_reader(byte me)
{
int myidx;
- do
- :: 1 ->
- myidx = idx;
- atomic {
+ do //\lnlbl{do}
+ :: 1 -> //\lnlbl{one}
+ myidx = idx; //\lnlbl{curidx}
+ atomic { //\lnlbl{atm:b}
if
:: ctr[myidx] > 0 ->
ctr[myidx]++;
break
:: else -> skip
fi
- }
- od;
- readerprogress[me] = 1;
- readerprogress[me] = 2;
- atomic { ctr[myidx]-- }
+ } //\lnlbl{atm:e}
+ od; //\lnlbl{od}
+ readerprogress[me] = 1; //\lnlbl{cs:entry}
+ readerprogress[me] = 2; //\lnlbl{cs:exit}
+ atomic { ctr[myidx]-- } //\lnlbl{atm:dec}
}
+//\end{snippet}
+//\begin{snippet}[labelbase=ln:formal:promela:qrcu:sum_unordered,commandchars=\!\@\$]
+#ifndef FCV_SNIPPET
#define sum_unordered \
atomic { \
if \
@@ -41,19 +47,37 @@ proctype qrcu_reader(byte me)
fi; \
} \
sum = sum + ctr[i]
+#else /* #ifndef FCV_SNIPPET */
+#define sum_unordered \
+ atomic { /* \lnlbl{fetch:b} */\
+ do /* \lnlbl{do} */\
+ :: 1 -> /* \lnlbl{g1} */\
+ sum = ctr[0]; \
+ i = 1; \
+ break \
+ :: 1 -> /* \lnlbl{g2} */\
+ sum = ctr[1]; \
+ i = 0; \
+ break \
+ od; /* \lnlbl{od} */\
+ } /* \lnlbl{fetch:e} */\
+ sum = sum + ctr[i] /* \lnlbl{sum_other} */
+#endif /* #ifndef FCV_SNIPPET */
+//\end{snippet}
+//\begin{snippet}[labelbase=ln:formal:promela:qrcu:updater,keepcomment=yes,commandchars=\\\@\$]
proctype qrcu_updater(byte me)
{
int i;
byte readerstart[N_QRCU_READERS];
int sum;
- do
+ do //\lnlbl{do}
:: 1 ->
/* Snapshot reader state. */
- atomic {
+ atomic { //\lnlbl{atm1:b}
i = 0;
do
:: i < N_QRCU_READERS ->
@@ -62,65 +86,68 @@ proctype qrcu_updater(byte me)
:: i >= N_QRCU_READERS ->
break
od
- }
+ } //\lnlbl{atm1:e}
- sum_unordered;
- if
+ sum_unordered; //\lnlbl{sum_unord}
+ if //\lnlbl{reinvoke:b}
:: sum <= 1 -> sum_unordered
:: else -> skip
- fi;
- if
+ fi; //\lnlbl{reinvoke:e}
+ if //\lnlbl{slow:b}
:: sum > 1 ->
- spin_lock(mutex);
- atomic { ctr[!idx]++ }
+ spin_lock(mutex); //\lnlbl{acq}
+ atomic { ctr[!idx]++ } //\lnlbl{flip_idx:b}
idx = !idx;
- atomic { ctr[!idx]-- }
- do
+ atomic { ctr[!idx]-- } //\lnlbl{flip_idx:e}
+ do //\lnlbl{wait:b}
:: ctr[!idx] > 0 -> skip
:: ctr[!idx] == 0 -> break
- od;
- spin_unlock(mutex);
+ od; //\lnlbl{wait:e}
+ spin_unlock(mutex); //\lnlbl{rel}
:: else -> skip
- fi;
+ fi; //\lnlbl{slow:e}
/* Verify reader progress. */
- atomic {
+ atomic { //\lnlbl{atm2:b}
i = 0;
sum = 0;
do
:: i < N_QRCU_READERS ->
sum = sum + (readerstart[i] == 1 &&
- readerprogress[i] == 1);
+ readerprogress[i] == 1);
i++
:: i >= N_QRCU_READERS ->
- assert(sum == 0);
+ assert(sum == 0); //\lnlbl{assert}
break
od
- }
- od
+ } //\lnlbl{atm2:e}
+ od //\lnlbl{od}
}
+//\end{snippet}
+//\begin{snippet}[labelbase=ln:formal:promela:qrcu:init,commandchars=\\\@\$]
init {
int i;
atomic {
- ctr[idx] = 1;
- ctr[!idx] = 0;
- i = 0;
+ ctr[idx] = 1; //\lnlbl{i_ctr:b}
+ ctr[!idx] = 0; //\lnlbl{i_ctr:e}
+ i = 0; //\lnlbl{spn_r:b}
do
:: i < N_QRCU_READERS ->
readerprogress[i] = 0;
run qrcu_reader(i);
i++
:: i >= N_QRCU_READERS -> break
- od;
- i = 0;
+ od; //\lnlbl{spn_r:e}
+ i = 0; //\lnlbl{spn_u:b}
do
:: i < N_QRCU_UPDATERS ->
run qrcu_updater(i);
i++
:: i >= N_QRCU_UPDATERS -> break
- od
+ od //\lnlbl{spn_u:e}
}
}
+//\end{snippet}
diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index 11c2c7d..5ba9f04 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -62,115 +62,76 @@ more complex uses.
\label{sec:formal:Promela Warm-Up: Non-Atomic Increment}
\begin{listing}[tbp]
-{ \scriptsize
-\begin{verbbox}
- 1 #define NUMPROCS 2
- 2
- 3 byte counter = 0;
- 4 byte progress[NUMPROCS];
- 5
- 6 proctype incrementer(byte me)
- 7 {
- 8 int temp;
- 9
- 10 temp = counter;
- 11 counter = temp + 1;
- 12 progress[me] = 1;
- 13 }
- 14
- 15 init {
- 16 int i = 0;
- 17 int sum = 0;
- 18
- 19 atomic {
- 20 i = 0;
- 21 do
- 22 :: i < NUMPROCS ->
- 23 progress[i] = 0;
- 24 run incrementer(i);
- 25 i++
- 26 :: i >= NUMPROCS -> break
- 27 od;
- 28 }
- 29 atomic {
- 30 i = 0;
- 31 sum = 0;
- 32 do
- 33 :: i < NUMPROCS ->
- 34 sum = sum + progress[i];
- 35 i++
- 36 :: i >= NUMPROCS -> break
- 37 od;
- 38 assert(sum < NUMPROCS || counter == NUMPROCS)
- 39 }
- 40 }
-\end{verbbox}
-}
-\centering
-\theverbbox
+\input{CodeSamples/formal/promela/increment@whole.fcv}
\caption{Promela Code for Non-Atomic Increment}
\label{lst:analysis:Promela Code for Non-Atomic Increment}
\end{listing}
+\begin{lineref}[ln:formal:promela:increment:whole]
Listing~\ref{lst:analysis:Promela Code for Non-Atomic Increment}
demonstrates the textbook race condition
resulting from non-atomic increment.
-Line~1 defines the number of processes to run (we will vary this
-to see the effect on state space), line~3 defines the counter,
-and line~4 is used to implement the assertion that appears on
-lines~29-39.
+Line~\lnref{nprocs} defines the number of processes to run (we will vary this
+to see the effect on state space), line~\lnref{count} defines the counter,
+and line~\lnref{prog} is used to implement the assertion that appears on
+lines~\lnref{assert:b}-\lnref{assert:e}.
-Lines~6-13 define a process that increments the counter non-atomically.
+Lines~\lnref{proc:b}-\lnref{proc:e} define a process that increments
+the counter non-atomically.
The argument \co{me} is the process number, set by the initialization
block later in the code.
Because simple Promela statements are each assumed atomic, we must
-break the increment into the two statements on lines~10-11.
-The assignment on line~12 marks the process's completion.
+break the increment into the two statements on
+lines~\lnref{incr:b}-\lnref{incr:e}.
+The assignment on line~\lnref{setprog} marks the process's completion.
Because the Spin system will fully search the state space, including
all possible sequences of states, there is no need for the loop
that would be used for conventional testing.
-Lines~15-40 are the initialization block, which is executed first.
-Lines~19-28 actually do the initialization, while lines~29-39
+Lines~\lnref{init:b}-\lnref{init:e} are the initialization block,
+which is executed first.
+Lines~\lnref{doinit:b}-\lnref{doinit:e} actually do the initialization,
+while lines~\lnref{assert:b}-\lnref{assert:e}
perform the assertion.
Both are atomic blocks in order to avoid unnecessarily increasing
the state space: because they are not part of the algorithm proper,
we lose no verification coverage by making them atomic.
-The do-od construct on lines~21-27 implements a Promela loop,
+The \co{do-od} construct on lines~\lnref{dood1:b}-\lnref{dood1:e}
+implements a Promela loop,
which can be thought of as a C {\tt for (;;)} loop containing a
\co{switch} statement that allows expressions in case labels.
The condition blocks (prefixed by {\tt ::})
are scanned non-deterministically,
though in this case only one of the conditions can possibly hold at a given
time.
-The first block of the do-od from lines~22-25 initializes the i-th
+The first block of the \co{do-od} from
+lines~\lnref{block1:b}-\lnref{block1:e}
+initializes the i-th
incrementer's progress cell, runs the i-th incrementer's process, and
then increments the variable \co{i}.
-The second block of the do-od on line~26 exits the loop once
+The second block of the \co{do-od} on
+line~\lnref{block2} exits the loop once
these processes have been started.
-The atomic block on lines~29-39 also contains a similar do-od
+The atomic block on lines~\lnref{assert:b}-\lnref{assert:e} also contains
+a similar \co{do-od}
loop that sums up the progress counters.
-The {\tt assert()} statement on line~38 verifies that if all processes
+The \co{assert()} statement on line~\lnref{assert} verifies that
+if all processes
have been completed, then all counts have been correctly recorded.
+\end{lineref}
You can build and run this program as follows:
-\vspace{5pt}
-\begin{minipage}[t]{\columnwidth}
-\scriptsize
-\begin{verbatim}
-spin -a increment.spin # Translate the model to C
-cc -DSAFETY -o pan pan.c # Compile the model
-./pan # Run the model
-\end{verbatim}
-\end{minipage}
-\vspace{5pt}
+\begin{VerbatimU}
+spin -a increment.spin # Translate the model to C
+cc -DSAFETY -o pan pan.c # Compile the model
+./pan # Run the model
+\end{VerbatimU}
\begin{listing*}[tbp]
-{ \scriptsize
-\begin{verbbox}
+\begin{VerbatimL}[numbers=none]
pan: assertion violated ((sum<2)||(counter==2)) (at depth 20)
pan: wrote increment.spin.trail
(Spin Version 4.2.5 -- 2 April 2005)
@@ -191,10 +152,7 @@ State-vector 40 byte, depth reached 22, errors: 1
hash conflicts: 0 (resolved)
2.622 memory usage (Mbyte)
-\end{verbbox}
-}
-\centering
-\theverbbox
+\end{VerbatimL}
\caption{Non-Atomic Increment spin Output}
\label{lst:analysis:Non-Atomic Increment spin Output}
\end{listing*}
@@ -214,18 +172,12 @@ The final line shows memory usage.
The \co{trail} file may be rendered human-readable as follows:
-\vspace{5pt}
-\begin{minipage}[t]{\columnwidth}
-\scriptsize
-\begin{verbatim}
+\begin{VerbatimU}
spin -t -p increment.spin
-\end{verbatim}
-\end{minipage}
-\vspace{5pt}
+\end{VerbatimU}
\begin{listing*}[htbp]
-{ \scriptsize
-\begin{verbbox}
+\begin{VerbatimL}[numbers=none]
Starting :init: with pid 0
1: proc 0 (:init:) line 20 "increment.spin" (state 1) [i = 0]
2: proc 0 (:init:) line 22 "increment.spin" (state 2) [((i<2))]
@@ -268,10 +220,7 @@ spin: trail ends after 21 steps
progress[1] = 1
21: proc 0 (:init:) line 40 "increment.spin" (state 24) <valid end state>
3 processes created
-\end{verbbox}
-}
-\centering
-\theverbbox
+\end{VerbatimL}
\caption{Non-Atomic Increment Error Trail}
\label{lst:analysis:Non-Atomic Increment Error Trail}
\end{listing*}
@@ -287,29 +236,13 @@ The assertion then triggered, after which the global state is displayed.
\label{sec:formal:Promela Warm-Up: Atomic Increment}
\begin{listing}[htbp]
-{ \scriptsize
-\begin{verbbox}
- 1 proctype incrementer(byte me)
- 2 {
- 3 int temp;
- 4
- 5 atomic {
- 6 temp = counter;
- 7 counter = temp + 1;
- 8 }
- 9 progress[me] = 1;
- 10 }
-\end{verbbox}
-}
-\centering
-\theverbbox
+\input{CodeSamples/formal/promela/atomicincrement@incrementer.fcv}
\caption{Promela Code for Atomic Increment}
\label{lst:analysis:Promela Code for Atomic Increment}
\end{listing}
\begin{listing}[htbp]
-{ \scriptsize
-\begin{verbbox}
+\begin{VerbatimL}[numbers=none]
(Spin Version 4.2.5 -- 2 April 2005)
+ Partial Order Reduction
@@ -332,10 +265,7 @@ unreached in proctype incrementer
(0 of 5 states)
unreached in proctype :init:
(0 of 24 states)
-\end{verbbox}
-}
-\centering
-\theverbbox
+\end{VerbatimL}
\caption{Atomic Increment spin Output}
\label{lst:analysis:Atomic Increment spin Output}
\end{listing}
@@ -516,19 +446,14 @@ The following tricks can help you to abuse Promela safely:
matters (e.g., unprotected by locks), but where you have
no memory barriers. This can be modeled in Promela as follows:
-\vspace{5pt}
-\begin{minipage}[t]{\columnwidth}
-\scriptsize
-\begin{verbatim}
- 1 if
- 2 :: 1 -> r1 = x;
- 3 r2 = y
- 4 :: 1 -> r2 = y;
- 5 r1 = x
- 6 fi
-\end{verbatim}
-\end{minipage}
-\vspace{5pt}
+\begin{VerbatimN}[samepage=true]
+if
+:: 1 -> r1 = x;
+ r2 = y
+:: 1 -> r2 = y;
+ r1 = x
+fi
+\end{VerbatimN}
The two branches of the \co{if} statement will be selected
nondeterministically, since they both are available.
@@ -539,52 +464,6 @@ The following tricks can help you to abuse Promela safely:
if used too heavily.
In addition, it requires you to anticipate possible reorderings.
-\begin{listing}[tbp]
-{ \scriptsize
-\begin{verbbox}
- 1 i = 0;
- 2 sum = 0;
- 3 do
- 4 :: i < N_QRCU_READERS ->
- 5 sum = sum + (readerstart[i] == 1 &&
- 6 readerprogress[i] == 1);
- 7 i++
- 8 :: i >= N_QRCU_READERS ->
- 9 assert(sum == 0);
- 10 break
- 11 od
-\end{verbbox}
-}
-\centering
-\theverbbox
-\caption{Complex Promela Assertion}
-\label{lst:analysis:Complex Promela Assertion}
-\end{listing}
-
-\begin{listing}[tbp]
-{ \scriptsize
-\begin{verbbox}
- 1 atomic {
- 2 i = 0;
- 3 sum = 0;
- 4 do
- 5 :: i < N_QRCU_READERS ->
- 6 sum = sum + (readerstart[i] == 1 &&
- 7 readerprogress[i] == 1);
- 8 i++
- 9 :: i >= N_QRCU_READERS ->
- 10 assert(sum == 0);
- 11 break
- 12 od
- 13 }
-\end{verbbox}
-}
-\centering
-\theverbbox
-\caption{Atomic Block for Complex Promela Assertion}
-\label{lst:analysis:Atomic Block for Complex Promela Assertion}
-\end{listing}
-
\item State reduction. If you have complex assertions, evaluate
them under \co{atomic}. After all, they are not part of the
algorithm. One example of a complex assertion (to be discussed
@@ -604,55 +483,77 @@ The following tricks can help you to abuse Promela safely:
combinatorial explosion.
\end{enumerate}
+\begin{listing}[tbp]
+\begin{VerbatimL}
+i = 0;
+sum = 0;
+do
+:: i < N_QRCU_READERS ->
+ sum = sum + (readerstart[i] == 1 &&
+ readerprogress[i] == 1);
+ i++
+:: i >= N_QRCU_READERS ->
+ assert(sum == 0);
+ break
+od
+\end{VerbatimL}
+\caption{Complex Promela Assertion}
+\label{lst:analysis:Complex Promela Assertion}
+\end{listing}
+
+\begin{listing}[tbp]
+\begin{VerbatimL}
+atomic {
+ i = 0;
+ sum = 0;
+ do
+ :: i < N_QRCU_READERS ->
+ sum = sum + (readerstart[i] == 1 &&
+ readerprogress[i] == 1);
+ i++
+ :: i >= N_QRCU_READERS ->
+ assert(sum == 0);
+ break
+ od
+}
+\end{VerbatimL}
+\caption{Atomic Block for Complex Promela Assertion}
+\label{lst:analysis:Atomic Block for Complex Promela Assertion}
+\end{listing}
+
Now we are ready for more complex examples.
\subsection{Promela Example: Locking}
\label{sec:formal:Promela Example: Locking}
\begin{listing}[tbp]
-{ \scriptsize
-\begin{verbbox}
- 1 #define spin_lock(mutex) \
- 2 do \
- 3 :: 1 -> atomic { \
- 4 if \
- 5 :: mutex == 0 -> \
- 6 mutex = 1; \
- 7 break \
- 8 :: else -> skip \
- 9 fi \
- 10 } \
- 11 od
- 12
- 13 #define spin_unlock(mutex) \
- 14 mutex = 0
-\end{verbbox}
-}
-\centering
-\theverbbox
+\input{CodeSamples/formal/promela/lock@whole.fcv}
\caption{Promela Code for Spinlock}
\label{lst:analysis:Promela Code for Spinlock}
\end{listing}
+\begin{lineref}[ln:formal:promela:lock:whole]
Since locks are generally useful, \co{spin_lock()} and
\co{spin_unlock()}
macros are provided in \path{lock.h}, which may be included from
multiple Promela models, as shown in
Listing~\ref{lst:analysis:Promela Code for Spinlock}.
-The \co{spin_lock()} macro contains an infinite do-od loop
-spanning lines~2-11,
-courtesy of the single guard expression of ``1'' on line~3.
+The \co{spin_lock()} macro contains an infinite \co{do-od} loop
+spanning lines~\lnref{dood:b}-\lnref{dood:e},
+courtesy of the single guard expression of ``1'' on line~\lnref{one}.
The body of this loop is a single atomic block that contains
-an if-fi statement.
-The if-fi construct is similar to the do-od construct, except
+an \co{if-fi} statement.
+The \co{if-fi} construct is similar to the \co{do-od} construct, except
that it takes a single pass rather than looping.
-If the lock is not held on line~5, then line~6 acquires it and
-line~7 breaks out of the enclosing do-od loop (and also exits
+If the lock is not held on line~\lnref{notheld}, then
+line~\lnref{acq} acquires it and
+line~\lnref{break} breaks out of the enclosing \co{do-od} loop (and also exits
the atomic block).
-On the other hand, if the lock is already held on line~8,
-we do nothing (\co{skip}), and fall out of the if-fi and the
+On the other hand, if the lock is already held on line~\lnref{held},
+we do nothing (\co{skip}), and fall out of the \co{if-fi} and the
atomic block so as to take another pass through the outer
loop, repeating until the lock is available.
+\end{lineref}
The \co{spin_unlock()} macro simply marks the lock as no
longer held.
@@ -668,81 +569,39 @@ As noted earlier, and as will be seen in a later example,
weak memory ordering must be explicitly coded.
\begin{listing}[tb]
-{ \scriptsize
-\begin{verbbox}
- 1 #include "lock.h"
- 2
- 3 #define N_LOCKERS 3
- 4
- 5 bit mutex = 0;
- 6 bit havelock[N_LOCKERS];
- 7 int sum;
- 8
- 9 proctype locker(byte me)
- 10 {
- 11 do
- 12 :: 1 ->
- 13 spin_lock(mutex);
- 14 havelock[me] = 1;
- 15 havelock[me] = 0;
- 16 spin_unlock(mutex)
- 17 od
- 18 }
- 19
- 20 init {
- 21 int i = 0;
- 22 int j;
- 23
- 24 end: do
- 25 :: i < N_LOCKERS ->
- 26 havelock[i] = 0;
- 27 run locker(i);
- 28 i++
- 29 :: i >= N_LOCKERS ->
- 30 sum = 0;
- 31 j = 0;
- 32 atomic {
- 33 do
- 34 :: j < N_LOCKERS ->
- 35 sum = sum + havelock[j];
- 36 j = j + 1
- 37 :: j >= N_LOCKERS ->
- 38 break
- 39 od
- 40 }
- 41 assert(sum <= 1);
- 42 break
- 43 od
- 44 }
-\end{verbbox}
-}
-\centering
-\theverbbox
+\input{CodeSamples/formal/promela/lock@spin.fcv}
\caption{Promela Code to Test Spinlocks}
\label{lst:analysis:Promela Code to Test Spinlocks}
\end{listing}
+\begin{lineref}[ln:formal:promela:lock:spin]
These macros are tested by the Promela code shown in
Listing~\ref{lst:analysis:Promela Code to Test Spinlocks}.
This code is similar to that used to test the increments,
with the number of locking processes defined by the \co{N_LOCKERS}
-macro definition on line~3.
-The mutex itself is defined on line~5, an array to track the lock owner
-on line~6, and line~7 is used by assertion
+macro definition on line~\lnref{nlockers}.
+The mutex itself is defined on line~\lnref{mutex},
+an array to track the lock owner
+on line~\lnref{array}, and line~\lnref{sum} is used by assertion
code to verify that only one process holds the lock.
-
-The locker process is on lines~9-18, and simply loops forever
-acquiring the lock on line~13, claiming it on line~14,
-unclaiming it on line~15, and releasing it on line~16.
-
-The init block on lines~20-44 initializes the current locker's
-havelock array entry on line~26, starts the current locker on
-line~27, and advances to the next locker on line~28.
-Once all locker processes are spawned, the do-od loop
-moves to line~29, which checks the assertion.
-Lines~30 and~31 initialize the control variables,
-lines~32-40 atomically sum the havelock array entries,
-line~41 is the assertion, and line~42 exits the loop.
+\end{lineref}
+
+\begin{lineref}[ln:formal:promela:lock:spin:locker]
+The locker process is on lines~\lnref{b}-\lnref{e}, and simply loops forever
+acquiring the lock on line~\lnref{lock}, claiming it on line~\lnref{claim},
+unclaiming it on line~\lnref{unclaim}, and releasing it on line~\lnref{unlock}.
+\end{lineref}
+
+\begin{lineref}[ln:formal:promela:lock:spin:init]
+The init block on lines~\lnref{b}-\lnref{e} initializes the current locker's
+havelock array entry on line~\lnref{array}, starts the current locker on
+line~\lnref{start}, and advances to the next locker on line~\lnref{next}.
+Once all locker processes are spawned, the \co{do-od} loop
+moves to line~\lnref{chkassert}, which checks the assertion.
+Lines~\lnref{sum} and~\lnref{j} initialize the control variables,
+lines~\lnref{atm:b}-\lnref{atm:e} atomically sum the havelock array entries,
+line~\lnref{assert} is the assertion, and line~\lnref{break} exits the loop.
+\end{lineref}
We can run this model by placing the two code fragments of
Listings~\ref{lst:analysis:Promela Code for Spinlock}
@@ -750,20 +609,14 @@ and~\ref{lst:analysis:Promela Code to Test Spinlocks} into
files named \path{lock.h} and \path{lock.spin}, respectively, and then running
the following commands:
-\vspace{5pt}
-\begin{minipage}[t]{\columnwidth}
-\scriptsize
-\begin{verbatim}
+\begin{VerbatimU}
spin -a lock.spin
cc -DSAFETY -o pan pan.c
./pan
-\end{verbatim}
-\end{minipage}
-\vspace{5pt}
+\end{VerbatimU}
\begin{listing}[htbp]
-{ \scriptsize
-\begin{verbbox}
+\begin{VerbatimL}[numbers=none]
(Spin Version 4.2.5 -- 2 April 2005)
+ Partial Order Reduction
@@ -787,10 +640,7 @@ unreached in proctype locker
(1 of 20 states)
unreached in proctype :init:
(0 of 22 states)
-\end{verbbox}
-}
-\centering
-\theverbbox
+\end{VerbatimL}
\caption{Output for Spinlock Test}
\label{lst:analysis:Output for Spinlock Test}
\end{listing}
@@ -863,16 +713,11 @@ latencies of most other RCU implementations.
For example:
-\vspace{5pt}
-\begin{minipage}[t]{\columnwidth}
-\scriptsize
-\begin{verbatim}
+\begin{VerbatimU}
idx = qrcu_read_lock(&my_qrcu_struct);
/* read-side critical section. */
qrcu_read_unlock(&my_qrcu_struct, idx);
-\end{verbatim}
-\end{minipage}
-\vspace{5pt}
+\end{VerbatimU}
\item There is a \co{synchronize_qrcu()} primitive that blocks until
all pre-existing QRCU read-side critical sections complete,
@@ -894,21 +739,7 @@ but has not yet been included in the Linux kernel as of
April 2008.
\begin{listing}[htbp]
-{ \scriptsize
-\begin{verbbox}
- 1 #include "lock.h"
- 2
- 3 #define N_QRCU_READERS 2
- 4 #define N_QRCU_UPDATERS 2
- 5
- 6 bit idx = 0;
- 7 byte ctr[2];
- 8 byte readerprogress[N_QRCU_READERS];
- 9 bit mutex = 0;
-\end{verbbox}
-}
-\centering
-\theverbbox
+\input{CodeSamples/formal/promela/qrcu@gvar.fcv}
\caption{QRCU Global Variables}
\label{lst:analysis:QRCU Global Variables}
\end{listing}
@@ -937,194 +768,104 @@ indicating the state of the corresponding reader:
Finally, the \co{mutex} variable is used to serialize updaters' slowpaths.
\begin{listing}[htbp]
-{ \scriptsize
-\begin{verbbox}
- 1 proctype qrcu_reader(byte me)
- 2 {
- 3 int myidx;
- 4
- 5 do
- 6 :: 1 ->
- 7 myidx = idx;
- 8 atomic {
- 9 if
- 10 :: ctr[myidx] > 0 ->
- 11 ctr[myidx]++;
- 12 break
- 13 :: else -> skip
- 14 fi
- 15 }
- 16 od;
- 17 readerprogress[me] = 1;
- 18 readerprogress[me] = 2;
- 19 atomic { ctr[myidx]-- }
- 20 }
-\end{verbbox}
-}
-\centering
-\theverbbox
+\input{CodeSamples/formal/promela/qrcu@reader.fcv}
\caption{QRCU Reader Process}
\label{lst:analysis:QRCU Reader Process}
\end{listing}
+\begin{lineref}[ln:formal:promela:qrcu:reader]
QRCU readers are modeled by the \co{qrcu_reader()} process shown in
Listing~\ref{lst:analysis:QRCU Reader Process}.
-A do-od loop spans lines~5-16, with a single guard of ``1''
-on line~6 that makes it an infinite loop.
-Line~7 captures the current value of the global index, and lines~8-15
+A \co{do-od} loop spans lines~\lnref{do}-\lnref{od},
+with a single guard of ``1''
+on line~\lnref{one} that makes it an infinite loop.
+Line~\lnref{curidx} captures the current value of the global index,
+and lines~\lnref{atm:b}-\lnref{atm:e}
atomically increment it (and break from the infinite loop)
if its value was non-zero (\co{atomic_inc_not_zero()}).
-Line~17 marks entry into the RCU read-side critical section, and
-line~18 marks exit from this critical section, both lines for the benefit of
-the {\tt assert()} statement that we shall encounter later.
-Line~19 atomically decrements the same counter that we incremented,
+Line~\lnref{cs:entry} marks entry into the RCU read-side critical section, and
+line~\lnref{cs:exit} marks exit from this critical section,
+both lines for the benefit of
+the \co{assert()} statement that we shall encounter later.
+Line~\lnref{atm:dec} atomically decrements the same counter that we incremented,
thereby exiting the RCU read-side critical section.
+\end{lineref}
\begin{listing}[htbp]
-{ \scriptsize
-\begin{verbbox}
- 1 #define sum_unordered \
- 2 atomic { \
- 3 do \
- 4 :: 1 -> \
- 5 sum = ctr[0]; \
- 6 i = 1; \
- 7 break \
- 8 :: 1 -> \
- 9 sum = ctr[1]; \
- 10 i = 0; \
- 11 break \
- 12 od; \
- 13 } \
- 14 sum = sum + ctr[i]
-\end{verbbox}
-}
-\centering
-\theverbbox
+\input{CodeSamples/formal/promela/qrcu@sum_unordered.fcv}
\caption{QRCU Unordered Summation}
\label{lst:analysis:QRCU Unordered Summation}
\end{listing}
+\begin{lineref}[ln:formal:promela:qrcu:sum_unordered]
The C-preprocessor macro shown in
Listing~\ref{lst:analysis:QRCU Unordered Summation}
sums the pair of counters so as to emulate weak memory ordering.
-Lines~2-13 fetch one of the counters, and line~14 fetches the other
+Lines~\lnref{fetch:b}-\lnref{fetch:e} fetch one of the counters,
+and line~\lnref{sum_other} fetches the other
of the pair and sums them.
-The atomic block consists of a single do-od statement.
-This do-od statement (spanning lines~3-12) is unusual in that
+The atomic block consists of a single \co{do-od} statement.
+This \co{do-od} statement (spanning lines~\lnref{do}-\lnref{od}) is unusual in that
it contains two unconditional
-branches with guards on lines~4 and~8, which causes Promela to
+branches with guards on lines~\lnref{g1} and~\lnref{g2}, which causes Promela to
non-deterministically choose one of the two (but again, the full
state-space search causes Promela to eventually make all possible
choices in each applicable situation).
The first branch fetches the zero-th counter and sets \co{i} to 1 (so
-that line~14 will fetch the first counter), while the second
+that line~\lnref{sum_other} will fetch the first counter), while the second
branch does the opposite, fetching the first counter and setting \co{i}
-to 0 (so that line~14 will fetch the second counter).
+to 0 (so that line~\lnref{sum_other} will fetch the second counter).
+\end{lineref}
\QuickQuiz{}
- Is there a more straightforward way to code the do-od statement?
+ Is there a more straightforward way to code the \co{do-od} statement?
\QuickQuizAnswer{
Yes.
- Replace it with {\tt if-fi} and remove the two {\tt break} statements.
+ Replace it with \co{if-fi} and remove the two \co{break} statements.
} \QuickQuizEnd
\begin{listing}[htbp]
-{ \scriptsize
-\begin{verbbox}
- 1 proctype qrcu_updater(byte me)
- 2 {
- 3 int i;
- 4 byte readerstart[N_QRCU_READERS];
- 5 int sum;
- 6
- 7 do
- 8 :: 1 ->
- 9
- 10 /* Snapshot reader state. */
- 11
- 12 atomic {
- 13 i = 0;
- 14 do
- 15 :: i < N_QRCU_READERS ->
- 16 readerstart[i] = readerprogress[i];
- 17 i++
- 18 :: i >= N_QRCU_READERS ->
- 19 break
- 20 od
- 21 }
- 22
- 23 sum_unordered;
- 24 if
- 25 :: sum <= 1 -> sum_unordered
- 26 :: else -> skip
- 27 fi;
- 28 if
- 29 :: sum > 1 ->
- 30 spin_lock(mutex);
- 31 atomic { ctr[!idx]++ }
- 32 idx = !idx;
- 33 atomic { ctr[!idx]-- }
- 34 do
- 35 :: ctr[!idx] > 0 -> skip
- 36 :: ctr[!idx] == 0 -> break
- 37 od;
- 38 spin_unlock(mutex);
- 39 :: else -> skip
- 40 fi;
- 41
- 42 /* Verify reader progress. */
- 43
- 44 atomic {
- 45 i = 0;
- 46 sum = 0;
- 47 do
- 48 :: i < N_QRCU_READERS ->
- 49 sum = sum + (readerstart[i] == 1 &&
- 50 readerprogress[i] == 1);
- 51 i++
- 52 :: i >= N_QRCU_READERS ->
- 53 assert(sum == 0);
- 54 break
- 55 od
- 56 }
- 57 od
- 58 }
-\end{verbbox}
-}
-\centering
-\theverbbox
+\input{CodeSamples/formal/promela/qrcu@updater.fcv}
\caption{QRCU Updater Process}
\label{lst:analysis:QRCU Updater Process}
\end{listing}
+\begin{lineref}[ln:formal:promela:qrcu:updater]
With the \co{sum_unordered} macro in place, we can now proceed
to the update-side process shown in
Listing~\ref{lst:analysis:QRCU Updater Process}.
The update-side process repeats indefinitely, with the corresponding
-do-od loop ranging over lines~7-57.
-Each pass through the loop first snapshots the global {\tt readerprogress}
-array into the local {\tt readerstart} array on lines~12-21.
-This snapshot will be used for the assertion on line~53.
-Line~23 invokes \co{sum_unordered}, and then lines~24-27
+\co{do-od} loop ranging over lines~\lnref{do}-\lnref{od}.
+Each pass through the loop first snapshots the global \co{readerprogress}
+array into the local \co{readerstart} array on
+lines~\lnref{atm1:b}-\lnref{atm1:e}.
+This snapshot will be used for the assertion on line~\lnref{assert}.
+Line~\lnref{sum_unord} invokes \co{sum_unordered}, and then
+lines~\lnref{reinvoke:b}-\lnref{reinvoke:e}
re-invoke \co{sum_unordered} if the fastpath is potentially
usable.
-Lines~28-40 execute the slowpath code if need be, with
-lines~30 and~38 acquiring and releasing the update-side lock,
-lines~31-33 flipping the index, and lines~34-37 waiting for
+Lines~\lnref{slow:b}-\lnref{slow:e} execute the slowpath code if need be, with
+lines~\lnref{acq} and~\lnref{rel} acquiring and releasing the update-side lock,
+lines~\lnref{flip_idx:b}-\lnref{flip_idx:e} flipping the index, and
+lines~\lnref{wait:b}-\lnref{wait:e} waiting for
all pre-existing readers to complete.
-Lines~44-56 then compare the current values in the {\tt readerprogress}
-array to those collected in the {\tt readerstart} array,
+Lines~\lnref{atm2:b}-\lnref{atm2:e} then compare the current values
+in the \co{readerprogress}
+array to those collected in the \co{readerstart} array,
forcing an assertion failure should any readers that started before
this update still be in progress.
+\end{lineref}
\QuickQuiz{}
- Why are there atomic blocks at lines~12-21
- and lines~44-56, when the operations within those atomic
+ \begin{lineref}[ln:formal:promela:qrcu:updater]
+ Why are there atomic blocks at lines~\lnref{atm1:b}-\lnref{atm1:e}
+ and lines~\lnref{atm2:b}-\lnref{atm2:e}, when the operations
+ within those atomic
blocks have no atomic implementation on any current
production microprocessor?
+ \end{lineref}
\QuickQuizAnswer{
Because those operations are for the benefit of the
assertion only. They are not part of the algorithm itself.
@@ -1134,8 +875,11 @@ this update still be in progress.
} \QuickQuizEnd
\QuickQuiz{}
- Is the re-summing of the counters on lines~24-27
+ \begin{lineref}[ln:formal:promela:qrcu:updater]
+ Is the re-summing of the counters on
+ lines~\lnref{reinvoke:b}-\lnref{reinvoke:e}
\emph{really} necessary?
+ \end{lineref}
\QuickQuizAnswer{
Yes. To see this, delete these lines and run the model.
@@ -1143,17 +887,17 @@ this update still be in progress.
\begin{enumerate}
\item One process is within its RCU read-side critical
- section, so that the value of {\tt ctr[0]} is zero and
- the value of {\tt ctr[1]} is two.
+ section, so that the value of \co{ctr[0]} is zero and
+ the value of \co{ctr[1]} is two.
\item An updater starts executing, and sees that the sum of
the counters is two so that the fastpath cannot be
executed. It therefore acquires the lock.
\item A second updater starts executing, and fetches the value
- of {\tt ctr[0]}, which is zero.
- \item The first updater adds one to {\tt ctr[0]}, flips
+ of \co{ctr[0]}, which is zero.
+ \item The first updater adds one to \co{ctr[0]}, flips
the index (which now becomes zero), then subtracts
- one from {\tt ctr[1]} (which now becomes one).
- \item The second updater fetches the value of {\tt ctr[1]},
+ one from \co{ctr[1]} (which now becomes one).
+ \item The second updater fetches the value of \co{ctr[1]},
which is now one.
\item The second updater now incorrectly concludes that it
is safe to proceed on the fastpath, despite the fact
@@ -1162,45 +906,21 @@ this update still be in progress.
} \QuickQuizEnd
\begin{listing}[htbp]
-{ \scriptsize
-\begin{verbbox}
- 1 init {
- 2 int i;
- 3
- 4 atomic {
- 5 ctr[idx] = 1;
- 6 ctr[!idx] = 0;
- 7 i = 0;
- 8 do
- 9 :: i < N_QRCU_READERS ->
- 10 readerprogress[i] = 0;
- 11 run qrcu_reader(i);
- 12 i++
- 13 :: i >= N_QRCU_READERS -> break
- 14 od;
- 15 i = 0;
- 16 do
- 17 :: i < N_QRCU_UPDATERS ->
- 18 run qrcu_updater(i);
- 19 i++
- 20 :: i >= N_QRCU_UPDATERS -> break
- 21 od
- 22 }
- 23 }
-\end{verbbox}
-}
-\centering
-\theverbbox
+\input{CodeSamples/formal/promela/qrcu@init.fcv}
\caption{QRCU Initialization Process}
\label{lst:analysis:QRCU Initialization Process}
\end{listing}
+\begin{lineref}[ln:formal:promela:qrcu:init]
All that remains is the initialization block shown in
Listing~\ref{lst:analysis:QRCU Initialization Process}.
-This block simply initializes the counter pair on lines~5-6,
-spawns the reader processes on lines~7-14, and spawns the updater
-processes on lines~15-21.
+This block simply initializes the counter pair on
+lines~\lnref{i_ctr:b}-\lnref{i_ctr:e},
+spawns the reader processes on
+lines~\lnref{spn_r:b}-\lnref{spn_r:e}, and spawns the updater
+processes on lines~\lnref{spn_u:b}-\lnref{spn_u:e}.
This is all done within an atomic block to reduce state space.
+\end{lineref}
\subsubsection{Running the QRCU Example}
\label{sec:formal:Running the QRCU Example}
@@ -1211,16 +931,11 @@ for \co{spin_lock()} and \co{spin_unlock()} into a file named
\path{lock.h}.
Then use the following commands to build and run the QRCU model:
-\vspace{5pt}
-\begin{minipage}[t]{\columnwidth}
-\scriptsize
-\begin{verbatim}
+\begin{VerbatimU}
spin -a qrcu.spin
cc -DSAFETY -o pan pan.c
./pan
-\end{verbatim}
-\end{minipage}
-\vspace{5pt}
+\end{VerbatimU}
\begin{table}
\rowcolors{1}{}{lightgray}
--
2.7.4
^ permalink raw reply related [flat|nested] 16+ messages in thread
* [PATCH 3/6] formal/spinhint: Update output lists of spin
2019-02-02 15:05 [PATCH 0/6] formal/spinhint: Update code snippet Akira Yokosawa
2019-02-02 15:08 ` [PATCH 1/6] fcvextract.pl: Treat '.spin' files as C sources Akira Yokosawa
2019-02-02 15:09 ` [PATCH 2/6] formal/spinhint: Employ new scheme for code snippet Akira Yokosawa
@ 2019-02-02 15:11 ` Akira Yokosawa
2019-02-02 15:13 ` [PATCH 4/6] formal/spinhint: Update tables of memory usage of Spin Akira Yokosawa
` (3 subsequent siblings)
6 siblings, 0 replies; 16+ messages in thread
From: Akira Yokosawa @ 2019-02-02 15:11 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From 986b559571721ae7c57a8d05c7b2da5b03c1ce21 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Thu, 31 Jan 2019 00:11:11 +0900
Subject: [PATCH 3/6] formal/spinhint: Update output lists of spin
Update the captures of output of Spin with those of Spin Version
6.4.8. *.spin.lst and *.spin.trail.lst files are placed under
CodeSamples/formal/promela/.
.spin.lst files are manually folded for 2c layout.
Also add dependency to those .lst files in the top-level Makefile.
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
.../formal/promela/atomicincrement.spin.lst | 28 +++++
CodeSamples/formal/promela/increment.spin.lst | 28 +++++
.../formal/promela/increment.spin.trail.lst | 42 +++++++
CodeSamples/formal/promela/lock.spin.lst | 29 +++++
Makefile | 4 +-
formal/spinhint.tex | 127 ++-------------------
6 files changed, 140 insertions(+), 118 deletions(-)
create mode 100644 CodeSamples/formal/promela/atomicincrement.spin.lst
create mode 100644 CodeSamples/formal/promela/increment.spin.lst
create mode 100644 CodeSamples/formal/promela/increment.spin.trail.lst
create mode 100644 CodeSamples/formal/promela/lock.spin.lst
diff --git a/CodeSamples/formal/promela/atomicincrement.spin.lst b/CodeSamples/formal/promela/atomicincrement.spin.lst
new file mode 100644
index 0000000..ab9150b
--- /dev/null
+++ b/CodeSamples/formal/promela/atomicincrement.spin.lst
@@ -0,0 +1,28 @@
+(Spin Version 6.4.8 -- 2 March 2018)
+ + Partial Order Reduction
+
+Full statespace search for:
+ never claim - (none specified)
+ assertion violations +
+ cycle checks - (disabled by -DSAFETY)
+ invalid end states +
+
+State-vector 48 byte, depth reached 22, errors: 0
+ 52 states, stored
+ 21 states, matched
+ 73 transitions (= stored+matched)
+ 68 atomic steps
+hash conflicts: 0 (resolved)
+
+Stats on memory usage (in Megabytes):
+ 0.004 equivalent memory usage for states
+ (stored*(State-vector + overhead))
+ 0.290 actual memory usage for states
+ 128.000 memory used for hash table (-w24)
+ 0.534 memory used for DFS stack (-m10000)
+ 128.730 total actual memory usage
+
+unreached in proctype incrementer
+ (0 of 5 states)
+unreached in init
+ (0 of 24 states)
diff --git a/CodeSamples/formal/promela/increment.spin.lst b/CodeSamples/formal/promela/increment.spin.lst
new file mode 100644
index 0000000..2cab90f
--- /dev/null
+++ b/CodeSamples/formal/promela/increment.spin.lst
@@ -0,0 +1,28 @@
+pan:1: assertion violated
+ ((sum<2)||(counter==2)) (at depth 22)
+pan: wrote increment.spin.trail
+
+(Spin Version 6.4.8 -- 2 March 2018)
+Warning: Search not completed
+ + Partial Order Reduction
+
+Full statespace search for:
+ never claim - (none specified)
+ assertion violations +
+ cycle checks - (disabled by -DSAFETY)
+ invalid end states +
+
+State-vector 48 byte, depth reached 24, errors: 1
+ 45 states, stored
+ 13 states, matched
+ 58 transitions (= stored+matched)
+ 53 atomic steps
+hash conflicts: 0 (resolved)
+
+Stats on memory usage (in Megabytes):
+ 0.003 equivalent memory usage for states
+ (stored*(State-vector + overhead))
+ 0.290 actual memory usage for states
+ 128.000 memory used for hash table (-w24)
+ 0.534 memory used for DFS stack (-m10000)
+ 128.730 total actual memory usage
diff --git a/CodeSamples/formal/promela/increment.spin.trail.lst b/CodeSamples/formal/promela/increment.spin.trail.lst
new file mode 100644
index 0000000..2416930
--- /dev/null
+++ b/CodeSamples/formal/promela/increment.spin.trail.lst
@@ -0,0 +1,42 @@
+using statement merging
+ 1: proc 0 (:init::1) increment.spin:21 (state 1) [i = 0]
+ 2: proc 0 (:init::1) increment.spin:23 (state 2) [((i<2))]
+ 2: proc 0 (:init::1) increment.spin:24 (state 3) [progress[i] = 0]
+Starting incrementer with pid 1
+ 3: proc 0 (:init::1) increment.spin:25 (state 4) [(run incrementer(i))]
+ 4: proc 0 (:init::1) increment.spin:26 (state 5) [i = (i+1)]
+ 5: proc 0 (:init::1) increment.spin:23 (state 2) [((i<2))]
+ 5: proc 0 (:init::1) increment.spin:24 (state 3) [progress[i] = 0]
+Starting incrementer with pid 2
+ 6: proc 0 (:init::1) increment.spin:25 (state 4) [(run incrementer(i))]
+ 7: proc 0 (:init::1) increment.spin:26 (state 5) [i = (i+1)]
+ 8: proc 0 (:init::1) increment.spin:27 (state 6) [((i>=2))]
+ 9: proc 0 (:init::1) increment.spin:22 (state 10) [break]
+ 10: proc 2 (incrementer:1) increment.spin:11 (state 1) [temp = counter]
+ 11: proc 1 (incrementer:1) increment.spin:11 (state 1) [temp = counter]
+ 12: proc 2 (incrementer:1) increment.spin:12 (state 2) [counter = (temp+1)]
+ 13: proc 2 (incrementer:1) increment.spin:13 (state 3) [progress[me] = 1]
+ 14: proc 2 terminates
+ 15: proc 1 (incrementer:1) increment.spin:12 (state 2) [counter = (temp+1)]
+ 16: proc 1 (incrementer:1) increment.spin:13 (state 3) [progress[me] = 1]
+ 17: proc 1 terminates
+ 18: proc 0 (:init::1) increment.spin:31 (state 12) [i = 0]
+ 18: proc 0 (:init::1) increment.spin:32 (state 13) [sum = 0]
+ 19: proc 0 (:init::1) increment.spin:34 (state 14) [((i<2))]
+ 19: proc 0 (:init::1) increment.spin:35 (state 15) [sum = (sum+progress[i])]
+ 19: proc 0 (:init::1) increment.spin:36 (state 16) [i = (i+1)]
+ 20: proc 0 (:init::1) increment.spin:34 (state 14) [((i<2))]
+ 20: proc 0 (:init::1) increment.spin:35 (state 15) [sum = (sum+progress[i])]
+ 20: proc 0 (:init::1) increment.spin:36 (state 16) [i = (i+1)]
+ 21: proc 0 (:init::1) increment.spin:37 (state 17) [((i>=2))]
+ 22: proc 0 (:init::1) increment.spin:33 (state 21) [break]
+spin: increment.spin:39, Error: assertion violated
+spin: text of failed assertion: assert(((sum<2)||(counter==2)))
+ 23: proc 0 (:init::1) increment.spin:39 (state 22) [assert(((sum<2)||(counter==2)))]
+spin: trail ends after 23 steps
+#processes: 1
+ counter = 1
+ progress[0] = 1
+ progress[1] = 1
+ 23: proc 0 (:init::1) increment.spin:41 (state 24) <valid end state>
+3 processes created
diff --git a/CodeSamples/formal/promela/lock.spin.lst b/CodeSamples/formal/promela/lock.spin.lst
new file mode 100644
index 0000000..c9e9efd
--- /dev/null
+++ b/CodeSamples/formal/promela/lock.spin.lst
@@ -0,0 +1,29 @@
+(Spin Version 6.4.8 -- 2 March 2018)
+ + Partial Order Reduction
+
+Full statespace search for:
+ never claim - (none specified)
+ assertion violations +
+ cycle checks - (disabled by -DSAFETY)
+ invalid end states +
+
+State-vector 52 byte, depth reached 360, errors: 0
+ 576 states, stored
+ 929 states, matched
+ 1505 transitions (= stored+matched)
+ 368 atomic steps
+hash conflicts: 0 (resolved)
+
+Stats on memory usage (in Megabytes):
+ 0.044 equivalent memory usage for states
+ (stored*(State-vector + overhead))
+ 0.288 actual memory usage for states
+ 128.000 memory used for hash table (-w24)
+ 0.534 memory used for DFS stack (-m10000)
+ 128.730 total actual memory usage
+
+unreached in proctype locker
+ lock.spin:19, state 20, "-end-"
+ (1 of 20 states)
+unreached in init
+ (0 of 22 states)
diff --git a/Makefile b/Makefile
index 2ed7500..c15678b 100644
--- a/Makefile
+++ b/Makefile
@@ -11,6 +11,8 @@ LATEXSOURCES = \
*/*.tex \
*/*/*.tex
+LST_SOURCES := $(wildcard CodeSamples/formal/promela/*.lst)
+
LATEXGENERATED = autodate.tex qqz.tex contrib.tex origpub.tex
ABBREVTARGETS := tcb 1c hb msns mss mstx msr msn msnt 1csf
@@ -123,7 +125,7 @@ $(PDFTARGETS): %.pdf: %.tex %.bbl
$(PDFTARGETS:.pdf=.bbl): %.bbl: %.aux $(BIBSOURCES)
bibtex $(basename $@)
-$(PDFTARGETS:.pdf=.aux): $(LATEXGENERATED) $(LATEXSOURCES)
+$(PDFTARGETS:.pdf=.aux): $(LATEXGENERATED) $(LATEXSOURCES) $(LST_SOURCES)
sh utilities/runfirstlatex.sh $(basename $@)
autodate.tex: perfbook.tex $(LATEXSOURCES) $(BIBSOURCES) $(SVGSOURCES) $(FIGSOURCES) $(DOTSOURCES) $(EPSORIGIN) $(SOURCES_OF_SNIPPET) utilities/fcvextract.pl
diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index 5ba9f04..4332f3e 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -130,32 +130,12 @@ cc -DSAFETY -o pan pan.c # Compile the model
./pan # Run the model
\end{VerbatimU}
-\begin{listing*}[tbp]
-\begin{VerbatimL}[numbers=none]
-pan: assertion violated ((sum<2)||(counter==2)) (at depth 20)
-pan: wrote increment.spin.trail
-(Spin Version 4.2.5 -- 2 April 2005)
-Warning: Search not completed
- + Partial Order Reduction
-
-Full statespace search for:
- never claim - (none specified)
- assertion violations +
- cycle checks - (disabled by -DSAFETY)
- invalid end states +
-
-State-vector 40 byte, depth reached 22, errors: 1
- 45 states, stored
- 13 states, matched
- 58 transitions (= stored+matched)
- 51 atomic steps
-hash conflicts: 0 (resolved)
-
-2.622 memory usage (Mbyte)
-\end{VerbatimL}
+\begin{listing}[tbp]
+\VerbatimInput[numbers=none,fontsize=\scriptsize]{CodeSamples/formal/promela/increment.spin.lst}
+\vspace*{-9pt}
\caption{Non-Atomic Increment spin Output}
\label{lst:analysis:Non-Atomic Increment spin Output}
-\end{listing*}
+\end{listing}
This will produce output as shown in
Listing~\ref{lst:analysis:Non-Atomic Increment spin Output}.
@@ -177,50 +157,8 @@ spin -t -p increment.spin
\end{VerbatimU}
\begin{listing*}[htbp]
-\begin{VerbatimL}[numbers=none]
-Starting :init: with pid 0
- 1: proc 0 (:init:) line 20 "increment.spin" (state 1) [i = 0]
- 2: proc 0 (:init:) line 22 "increment.spin" (state 2) [((i<2))]
- 2: proc 0 (:init:) line 23 "increment.spin" (state 3) [progress[i] = 0]
-Starting incrementer with pid 1
- 3: proc 0 (:init:) line 24 "increment.spin" (state 4) [(run incrementer(i))]
- 3: proc 0 (:init:) line 25 "increment.spin" (state 5) [i = (i+1)]
- 4: proc 0 (:init:) line 22 "increment.spin" (state 2) [((i<2))]
- 4: proc 0 (:init:) line 23 "increment.spin" (state 3) [progress[i] = 0]
-Starting incrementer with pid 2
- 5: proc 0 (:init:) line 24 "increment.spin" (state 4) [(run incrementer(i))]
- 5: proc 0 (:init:) line 25 "increment.spin" (state 5) [i = (i+1)]
- 6: proc 0 (:init:) line 26 "increment.spin" (state 6) [((i>=2))]
- 7: proc 0 (:init:) line 21 "increment.spin" (state 10) [break]
- 8: proc 2 (incrementer) line 10 "increment.spin" (state 1) [temp = counter]
- 9: proc 1 (incrementer) line 10 "increment.spin" (state 1) [temp = counter]
-10: proc 2 (incrementer) line 11 "increment.spin" (state 2) [counter = (temp+1)]
-11: proc 2 (incrementer) line 12 "increment.spin" (state 3) [progress[me] = 1]
-12: proc 2 terminates
-13: proc 1 (incrementer) line 11 "increment.spin" (state 2) [counter = (temp+1)]
-14: proc 1 (incrementer) line 12 "increment.spin" (state 3) [progress[me] = 1]
-15: proc 1 terminates
-16: proc 0 (:init:) line 30 "increment.spin" (state 12) [i = 0]
-16: proc 0 (:init:) line 31 "increment.spin" (state 13) [sum = 0]
-17: proc 0 (:init:) line 33 "increment.spin" (state 14) [((i<2))]
-17: proc 0 (:init:) line 34 "increment.spin" (state 15) [sum = (sum+progress[i])]
-17: proc 0 (:init:) line 35 "increment.spin" (state 16) [i = (i+1)]
-18: proc 0 (:init:) line 33 "increment.spin" (state 14) [((i<2))]
-18: proc 0 (:init:) line 34 "increment.spin" (state 15) [sum = (sum+progress[i])]
-18: proc 0 (:init:) line 35 "increment.spin" (state 16) [i = (i+1)]
-19: proc 0 (:init:) line 36 "increment.spin" (state 17) [((i>=2))]
-20: proc 0 (:init:) line 32 "increment.spin" (state 21) [break]
-spin: line 38 "increment.spin", Error: assertion violated
-spin: text of failed assertion: assert(((sum<2)||(counter==2)))
- 21: proc 0 (:init:) line 38 "increment.spin" (state 22) [assert(((sum<2)||(counter==2)))]
-spin: trail ends after 21 steps
-#processes: 1
- counter = 1
- progress[0] = 1
- progress[1] = 1
-21: proc 0 (:init:) line 40 "increment.spin" (state 24) <valid end state>
-3 processes created
-\end{VerbatimL}
+\VerbatimInput[numbers=none,fontsize=\scriptsize]{CodeSamples/formal/promela/increment.spin.trail.lst}
+\vspace*{-9pt}
\caption{Non-Atomic Increment Error Trail}
\label{lst:analysis:Non-Atomic Increment Error Trail}
\end{listing*}
@@ -242,30 +180,8 @@ The assertion then triggered, after which the global state is displayed.
\end{listing}
\begin{listing}[htbp]
-\begin{VerbatimL}[numbers=none]
-(Spin Version 4.2.5 -- 2 April 2005)
- + Partial Order Reduction
-
-Full statespace search for:
- never claim - (none specified)
- assertion violations +
- cycle checks - (disabled by -DSAFETY)
- invalid end states +
-
-State-vector 40 byte, depth reached 20, errors: 0
- 52 states, stored
- 21 states, matched
- 73 transitions (= stored+matched)
- 66 atomic steps
-hash conflicts: 0 (resolved)
-
-2.622 memory usage (Mbyte)
-
-unreached in proctype incrementer
- (0 of 5 states)
-unreached in proctype :init:
- (0 of 24 states)
-\end{VerbatimL}
+\VerbatimInput[numbers=none,fontsize=\scriptsize]{CodeSamples/formal/promela/atomicincrement.spin.lst}
+\vspace*{-9pt}
\caption{Atomic Increment spin Output}
\label{lst:analysis:Atomic Increment spin Output}
\end{listing}
@@ -616,31 +532,8 @@ cc -DSAFETY -o pan pan.c
\end{VerbatimU}
\begin{listing}[htbp]
-\begin{VerbatimL}[numbers=none]
-(Spin Version 4.2.5 -- 2 April 2005)
- + Partial Order Reduction
-
-Full statespace search for:
- never claim - (none specified)
- assertion violations +
- cycle checks - (disabled by -DSAFETY)
- invalid end states +
-
-State-vector 40 byte, depth reached 357, errors: 0
- 564 states, stored
- 929 states, matched
- 1493 transitions (= stored+matched)
- 368 atomic steps
-hash conflicts: 0 (resolved)
-
-2.622 memory usage (Mbyte)
-
-unreached in proctype locker
- line 18, state 20, "-end-"
- (1 of 20 states)
-unreached in proctype :init:
- (0 of 22 states)
-\end{VerbatimL}
+\VerbatimInput[numbers=none,fontsize=\scriptsize]{CodeSamples/formal/promela/lock.spin.lst}
+\vspace*{-9pt}
\caption{Output for Spinlock Test}
\label{lst:analysis:Output for Spinlock Test}
\end{listing}
--
2.7.4
^ permalink raw reply related [flat|nested] 16+ messages in thread
* [PATCH 4/6] formal/spinhint: Update tables of memory usage of Spin
2019-02-02 15:05 [PATCH 0/6] formal/spinhint: Update code snippet Akira Yokosawa
` (2 preceding siblings ...)
2019-02-02 15:11 ` [PATCH 3/6] formal/spinhint: Update output lists of spin Akira Yokosawa
@ 2019-02-02 15:13 ` Akira Yokosawa
2019-02-02 15:14 ` [PATCH 5/6] formal/spinhint: Put footnote on header in table Akira Yokosawa
` (2 subsequent siblings)
6 siblings, 0 replies; 16+ messages in thread
From: Akira Yokosawa @ 2019-02-02 15:13 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From 72b1807d846432592d01c8642cebfa6a655802ed Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Thu, 31 Jan 2019 00:13:21 +0900
Subject: [PATCH 4/6] formal/spinhint: Update tables of memory usage of Spin
Update tables of memory usage of increment.spin and qrcu.spin.
As for qrcu.spin, to complete search of 3 updaters and 2 readers
on a machine with 16GB memory, the "-DCOLLAPSE" flag is necessary
to avoid memory exhaustion. This doesn't affect the completeness of
state search. Add explantion of the flag and update the table of
qrcu.spin with the usage obtained with the flag enabled.
There seems to have been incomplete searches due to insufficient
search depth. Update "# state" figures from the complete results
obtained with deeper search limits.
Depth reached:
updaters readers depth
1 1 95
1 2 218
1 3 385
2 1 859
2 2 2352
2 3 12857
3 1 53809
3 2 328014
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
formal/spinhint.tex | 64 ++++++++++++++++++++++++++++++++---------------------
1 file changed, 39 insertions(+), 25 deletions(-)
diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index 4332f3e..9c56b00 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -198,22 +198,22 @@ Listing~\ref{lst:analysis:Atomic Increment spin Output}.
\begin{table}
\rowcolors{1}{}{lightgray}
-\renewcommand*{\arraystretch}{1.2}
\small
+\renewcommand*{\arraystretch}{1.2}
\centering
\begin{tabular}{S[table-format = 1.0]S[table-format = 7.0]S[table-format = 3.1]}
\toprule
\multicolumn{1}{l}{\# incrementers} &
\multicolumn{1}{r}{\# states} &
- \multicolumn{1}{r}{megabytes} \\
+ \multicolumn{1}{r}{total memory usage (MB)} \\
\midrule
- 1 & 11 & 2.6 \\
- 2 & 52 & 2.6 \\
- 3 & 372 & 2.6 \\
- 4 & 3 496 & 2.7 \\
- 5 & 40 221 & 5.0 \\
- 6 & 545 720 & 40.5 \\
- 7 & 8 521 450 & 652.7 \\
+ 1 & 11 & 128.7 \\
+ 2 & 52 & 128.7 \\
+ 3 & 372 & 128.7 \\
+ 4 & 3 496 & 128.9 \\
+ 5 & 40 221 & 131.7 \\
+ 6 & 545 720 & 174.0 \\
+ 7 & 8 521 446 & 881.9 \\
\bottomrule
\end{tabular}
\caption{Memory Usage of Increment Model}
@@ -226,7 +226,7 @@ as a function of number of incrementers modeled
(by redefining {\tt NUMPROCS}):
Running unnecessarily large models is thus subtly discouraged, although
-652\,MB is well within the limits of modern desktop and laptop machines.
+882\,MB is well within the limits of modern desktop and laptop machines.
With this example under our belt, let's take a closer look at the
commands used to analyze Promela models and then look at more
@@ -240,7 +240,7 @@ Given a source file \path{qrcu.spin}, one can use the following commands:
\begin{description}[style=nextline]
\item [\tco{spin -a qrcu.spin}]
Create a file \path{pan.c} that fully searches the state machine.
-\item [\tco{cc -DSAFETY -o pan pan.c}]
+\item [\tco{cc -DSAFETY [-DCOLLAPSE] -o pan pan.c}]
Compile the generated state-machine search. The \co{-DSAFETY}
generates optimizations that are appropriate if you have only
assertions (and perhaps \co{never} statements). If you have
@@ -253,12 +253,20 @@ Given a source file \path{qrcu.spin}, one can use the following commands:
An example situation where you cannot use \co{-DSAFETY} is
when checking for livelocks (AKA ``non-progress cycles'')
via \co{-DNP}.
-\item [\tco{./pan}]
+
+ The optional \co{-DCOLLAPSE} generates code for a state vector
+ compression mode.
+\item [\tco{./pan [-mN]}]
This actually searches the state space. The number of states
can reach into the tens of millions with very small state
machines, so you will need a machine with large memory.
- For example, \path{qrcu.spin} with 3 readers and 2 updaters required
- 2.7\,GB of memory.
+ For example, \path{qrcu.spin} with 3~updaters and 2~readers required
+ 10.5\,GB of memory even with the \co{-DCOLLAPSE} flag.
+
+ If you see a message from \co{pan} saying:
+ ``error: max search depth too small'', you need to increase
+ the maximum depth by a \co{-mN} flag for a complete search.
+ The default is \co{-m10000}.
If you aren't sure whether your machine has enough memory,
run \co{top} in one window and \co{./pan} in another. Keep the
@@ -269,6 +277,10 @@ Given a source file \path{qrcu.spin}, one can use the following commands:
windowing system to grab enough memory to do anything for
you.
+ Another option to avoid memory exhaustion is the
+ \co{-DMEMLIM=N} compiler flag. \co{-DMEMLIM=2000}
+ would set the maximum of 2\,GB.
+
Don't forget to capture the output, especially
if you are working on a remote machine.
@@ -826,8 +838,8 @@ Then use the following commands to build and run the QRCU model:
\begin{VerbatimU}
spin -a qrcu.spin
-cc -DSAFETY -o pan pan.c
-./pan
+cc -DSAFETY [-DCOLLAPSE] -o pan pan.c
+./pan [-mN]
\end{VerbatimU}
\begin{table}
@@ -843,14 +855,14 @@ cc -DSAFETY -o pan pan.c
\multicolumn{1}{r}{\# states} &
\multicolumn{1}{r}{MB} \\
\midrule
- 1 & 1 & 376 & 2.6 \\
- 1 & 2 & 6 177 & 2.9 \\
- 1 & 3 & 82 127 & 7.5 \\
- 2 & 1 & 29 399 & 4.5 \\
- 2 & 2 & 1 071 180 & 75.4 \\
- 2 & 3 & 33 866 700 & 2 715.2 \\
- 3 & 1 & 258 605 & 22.3 \\
- 3 & 2 & 169 533 000 & 14 979.9 \\
+ 1 & 1 & 376 & 128.7 \\
+ 1 & 2 & 6 177 & 128.9 \\
+ 1 & 3 & 99 728 & 132.6 \\
+ 2 & 1 & 29 399 & 129.8 \\
+ 2 & 2 & 1 071 181 & 169.6 \\
+ 2 & 3 & 33 866 736 & 1 540.8 \\
+ 3 & 1 & 2 749 453 & 236.6 \\
+ 3 & 2 & 186 202 860 & 10 483.7 \\
\bottomrule
\end{tabular}
\caption{Memory Usage of QRCU Model}
@@ -859,7 +871,9 @@ cc -DSAFETY -o pan pan.c
The resulting output shows that this model passes all of the cases
shown in
-Table~\ref{tab:advsync:Memory Usage of QRCU Model}.
+Table~\ref{tab:advsync:Memory Usage of QRCU Model}.\footnote{
+ Figures in the table are obtained with the \co{-DCOLLAPSE}
+ compiler flag specified.}
Now, it would be nice to run the case with three readers and three
updaters, however, simple extrapolation indicates that this will
require on the order of a terabyte of memory best case.
--
2.7.4
^ permalink raw reply related [flat|nested] 16+ messages in thread
* [PATCH 5/6] formal/spinhint: Put footnote on header in table
2019-02-02 15:05 [PATCH 0/6] formal/spinhint: Update code snippet Akira Yokosawa
` (3 preceding siblings ...)
2019-02-02 15:13 ` [PATCH 4/6] formal/spinhint: Update tables of memory usage of Spin Akira Yokosawa
@ 2019-02-02 15:14 ` Akira Yokosawa
2019-02-02 15:15 ` [PATCH 6/6] formal/spinhint: Use \co{...} rather than {\tt ...} Akira Yokosawa
2019-02-02 17:34 ` [PATCH 0/6] formal/spinhint: Update code snippet Paul E. McKenney
6 siblings, 0 replies; 16+ messages in thread
From: Akira Yokosawa @ 2019-02-02 15:14 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From 5db712d3f30c38dc5e2dbc6bf0ad68dd0b24870b Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Thu, 31 Jan 2019 00:14:56 +0900
Subject: [PATCH 5/6] formal/spinhint: Put footnote on header in table
The "savenotes" environment provided by the "footnote" package
allows us to put a footnote in a table whose text is placed at
the bottom of the page.
Also wordsmith the footnote's text.
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
formal/spinhint.tex | 10 ++++++----
perfbook.tex | 1 +
2 files changed, 7 insertions(+), 4 deletions(-)
diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index 9c56b00..a13374a 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -842,6 +842,7 @@ cc -DSAFETY [-DCOLLAPSE] -o pan pan.c
./pan [-mN]
\end{VerbatimU}
+\begin{savenotes}
\begin{table}
\rowcolors{1}{}{lightgray}
\renewcommand*{\arraystretch}{1.2}
@@ -853,7 +854,9 @@ cc -DSAFETY [-DCOLLAPSE] -o pan pan.c
\multicolumn{1}{r}{updaters} &
\multicolumn{1}{r}{readers} &
\multicolumn{1}{r}{\# states} &
- \multicolumn{1}{r}{MB} \\
+ \multicolumn{1}{r}{MB\footnote{
+ Obtained with the compiler flag \co{-DCOLLAPSE}
+ specified.}} \\
\midrule
1 & 1 & 376 & 128.7 \\
1 & 2 & 6 177 & 128.9 \\
@@ -868,12 +871,11 @@ cc -DSAFETY [-DCOLLAPSE] -o pan pan.c
\caption{Memory Usage of QRCU Model}
\label{tab:advsync:Memory Usage of QRCU Model}
\end{table}
+\end{savenotes}
The resulting output shows that this model passes all of the cases
shown in
-Table~\ref{tab:advsync:Memory Usage of QRCU Model}.\footnote{
- Figures in the table are obtained with the \co{-DCOLLAPSE}
- compiler flag specified.}
+Table~\ref{tab:advsync:Memory Usage of QRCU Model}.
Now, it would be nice to run the case with three readers and three
updaters, however, simple extrapolation indicates that this will
require on the order of a terabyte of memory best case.
diff --git a/perfbook.tex b/perfbook.tex
index 2eb4cd8..c740619 100644
--- a/perfbook.tex
+++ b/perfbook.tex
@@ -52,6 +52,7 @@
\usepackage[bottom]{footmisc} % place footnotes under floating figures/tables
\usepackage{tabularx}
\usepackage[hyphens]{url}
+\usepackage{footnote}
\usepackage[bookmarks=true,bookmarksnumbered=true,pdfborder={0 0 0}]{hyperref}
\usepackage{footnotebackref} % to enable cross-ref of footnote
\usepackage[all]{hypcap} % for going to the top of figure and table
--
2.7.4
^ permalink raw reply related [flat|nested] 16+ messages in thread
* [PATCH 6/6] formal/spinhint: Use \co{...} rather than {\tt ...}
2019-02-02 15:05 [PATCH 0/6] formal/spinhint: Update code snippet Akira Yokosawa
` (4 preceding siblings ...)
2019-02-02 15:14 ` [PATCH 5/6] formal/spinhint: Put footnote on header in table Akira Yokosawa
@ 2019-02-02 15:15 ` Akira Yokosawa
2019-02-02 17:34 ` [PATCH 0/6] formal/spinhint: Update code snippet Paul E. McKenney
6 siblings, 0 replies; 16+ messages in thread
From: Akira Yokosawa @ 2019-02-02 15:15 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From 211a647f0530d7c7fbdab93ae5e76e71e04295f6 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Sat, 2 Feb 2019 20:00:36 +0900
Subject: [PATCH 6/6] formal/spinhint: Use \co{...} rather than {\tt ...}
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
formal/spinhint.tex | 14 +++++++-------
1 file changed, 7 insertions(+), 7 deletions(-)
diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index a13374a..d99254e 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -99,9 +99,9 @@ we lose no verification coverage by making them atomic.
The \co{do-od} construct on lines~\lnref{dood1:b}-\lnref{dood1:e}
implements a Promela loop,
-which can be thought of as a C {\tt for (;;)} loop containing a
+which can be thought of as a C \co{for (;;)} loop containing a
\co{switch} statement that allows expressions in case labels.
-The condition blocks (prefixed by {\tt ::})
+The condition blocks (prefixed by \co{::})
are scanned non-deterministically,
though in this case only one of the conditions can possibly hold at a given
time.
@@ -190,7 +190,7 @@ It is easy to fix this example by placing the body of the incrementer
processes in an atomic blocks as shown in
Listing~\ref{lst:analysis:Promela Code for Atomic Increment}.
One could also have simply replaced the pair of statements with
-{\tt counter = counter + 1}, because Promela statements are
+\co{counter = counter + 1}, because Promela statements are
atomic.
Either way, running this modified model gives us an error-free traversal
of the state space, as shown in
@@ -223,7 +223,7 @@ Listing~\ref{lst:analysis:Atomic Increment spin Output}.
Table~\ref{tab:advsync:Memory Usage of Increment Model}
shows the number of states and memory consumed
as a function of number of incrementers modeled
-(by redefining {\tt NUMPROCS}):
+(by redefining \co{NUMPROCS}):
Running unnecessarily large models is thus subtly discouraged, although
882\,MB is well within the limits of modern desktop and laptop machines.
@@ -571,15 +571,15 @@ As expected, this run has no assertion failures (``errors: 0'').
\QuickQuizAnswer{
There are several:
\begin{enumerate}
- \item The declaration of {\tt sum} should be moved to within
+ \item The declaration of \co{sum} should be moved to within
the init block, since it is not used anywhere else.
\item The assertion code should be moved outside of the
initialization loop. The initialization loop can
then be placed in an atomic block, greatly reducing
the state space (by how much?).
\item The atomic block covering the assertion code should
- be extended to include the initialization of {\tt sum}
- and {\tt j}, and also to cover the assertion.
+ be extended to include the initialization of \co{sum}
+ and \co{j}, and also to cover the assertion.
This also reduces the state space (again, by how
much?).
\end{enumerate}
--
2.7.4
^ permalink raw reply related [flat|nested] 16+ messages in thread
* Re: [PATCH 0/6] formal/spinhint: Update code snippet
2019-02-02 15:05 [PATCH 0/6] formal/spinhint: Update code snippet Akira Yokosawa
` (5 preceding siblings ...)
2019-02-02 15:15 ` [PATCH 6/6] formal/spinhint: Use \co{...} rather than {\tt ...} Akira Yokosawa
@ 2019-02-02 17:34 ` Paul E. McKenney
2019-02-06 22:42 ` Akira Yokosawa
6 siblings, 1 reply; 16+ messages in thread
From: Paul E. McKenney @ 2019-02-02 17:34 UTC (permalink / raw)
To: Akira Yokosawa; +Cc: perfbook
On Sun, Feb 03, 2019 at 12:05:32AM +0900, Akira Yokosawa wrote:
> Hi Paul,
>
> Here is another round of code snippet update, with modernization
> of outputs of Spin and tables of state search results.
>
> Patch #1 updates fcvextract.pl so that .spin files are handled
> as the same as C source files.
>
> Patch #2 applies the new scheme to code snippets. It also contains
> minor changes for better typesetting.
>
> Patch #3 replaces captures of Spin outputs with those obtained
> from Spin version 6.4.8. This commit adds outputs as .lst files
> under CodeSamples/formal/promela/. They are added to the dependency
> in the top level Makefile.
>
> Patch #4 updates tables of Spin result. For qrcu.spin, I used
> the compiler flag -DCOLLAPSE to complete the state search for
> updaters=3 readers=2 on a machine with 16GB memory. As far as
> I understand correctly, this compiler flag does not affect the
> completeness of state search. So I added some explanation in the text
> to mention the flag and the argument -mN of ./pan to increase the
> limit of search depth.
>
> Patch #5 tweaks footnote on a cell in a table.
>
> Patch #6 is a nitpick patch to consistently use \co{}.
>
> I'm wondering if Patch #4 is OK from your perspective.
> Any feedback is welcome!
Very good, applied and pushed! I added a small patch on top of Patch #4
updating the extrapolation. It was about a terabyte, and is now about
half that. I agree that -DCOLLAPSE is a pure optimization, so it should
be OK. If we trust the documentation, anyway! ;-)
Thanx, Paul
> Thanks, Akira
> --
> Akira Yokosawa (6):
> fcvextract.pl: Treat '.spin' files as C sources
> formal/spinhint: Employ new scheme for code snippet
> formal/spinhint: Update output lists of spin
> formal/spinhint: Update tables of memory usage of Spin
> formal/spinhint: Put footnote on header in table
> formal/spinhint: Use \co{...} rather than {\tt ...}
>
> CodeSamples/formal/promela/atomicincrement.spin | 2 +
> .../formal/promela/atomicincrement.spin.lst | 28 +
> CodeSamples/formal/promela/increment.spin | 46 +-
> CodeSamples/formal/promela/increment.spin.lst | 28 +
> .../formal/promela/increment.spin.trail.lst | 42 +
> CodeSamples/formal/promela/lock.h | 16 +-
> CodeSamples/formal/promela/lock.spin | 46 +-
> CodeSamples/formal/promela/lock.spin.lst | 29 +
> CodeSamples/formal/promela/qrcu.spin | 95 ++-
> Makefile | 4 +-
> formal/spinhint.tex | 874 ++++++---------------
> perfbook.tex | 1 +
> utilities/fcvextract.pl | 8 +-
> 13 files changed, 502 insertions(+), 717 deletions(-)
> create mode 100644 CodeSamples/formal/promela/atomicincrement.spin.lst
> create mode 100644 CodeSamples/formal/promela/increment.spin.lst
> create mode 100644 CodeSamples/formal/promela/increment.spin.trail.lst
> create mode 100644 CodeSamples/formal/promela/lock.spin.lst
>
> --
> 2.7.4
>
^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [PATCH 0/6] formal/spinhint: Update code snippet
2019-02-02 17:34 ` [PATCH 0/6] formal/spinhint: Update code snippet Paul E. McKenney
@ 2019-02-06 22:42 ` Akira Yokosawa
2019-02-07 9:17 ` Paul E. McKenney
0 siblings, 1 reply; 16+ messages in thread
From: Akira Yokosawa @ 2019-02-06 22:42 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
On 2019/02/02 09:34:37 -0800, Paul E. McKenney wrote:
> On Sun, Feb 03, 2019 at 12:05:32AM +0900, Akira Yokosawa wrote:
>> Hi Paul,
>>
>> Here is another round of code snippet update, with modernization
>> of outputs of Spin and tables of state search results.
>>
>> Patch #1 updates fcvextract.pl so that .spin files are handled
>> as the same as C source files.
>>
>> Patch #2 applies the new scheme to code snippets. It also contains
>> minor changes for better typesetting.
>>
>> Patch #3 replaces captures of Spin outputs with those obtained
>> from Spin version 6.4.8. This commit adds outputs as .lst files
>> under CodeSamples/formal/promela/. They are added to the dependency
>> in the top level Makefile.
>>
>> Patch #4 updates tables of Spin result. For qrcu.spin, I used
>> the compiler flag -DCOLLAPSE to complete the state search for
>> updaters=3 readers=2 on a machine with 16GB memory. As far as
>> I understand correctly, this compiler flag does not affect the
>> completeness of state search. So I added some explanation in the text
>> to mention the flag and the argument -mN of ./pan to increase the
>> limit of search depth.
>>
>> Patch #5 tweaks footnote on a cell in a table.
>>
>> Patch #6 is a nitpick patch to consistently use \co{}.
>>
>> I'm wondering if Patch #4 is OK from your perspective.
>> Any feedback is welcome!
>
> Very good, applied and pushed! I added a small patch on top of Patch #4
> updating the extrapolation. It was about a terabyte, and is now about
> half that.
Half a terabyte is not prohibitively large these days, and Spin has
another compaction option "-DMA=N" which aggressively reduces memory
consumption in exchange of search speed.
It took three days to complete, with the total memory usage of 6.5GB.
The output looks as follows:
--------
(Spin Version 6.4.6 -- 2 December 2016)
+ Partial Order Reduction
+ Graph Encoding (-DMA=96)
Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +
State-vector 96 byte, depth reached 2055621, errors: 0
MA stats: -DMA=84 is sufficient
Minimized Automaton: 56420520 nodes and 1.75128e+08 edges
9.6647071e+09 states, stored
9.7503813e+09 states, matched
1.9415088e+10 transitions (= stored+matched)
7.2047951e+09 atomic steps
Stats on memory usage (in Megabytes):
1142905.887 equivalent memory usage for states (stored*(State-vector + overhead))
5448.879 actual memory usage for states (compression: 0.48%)
1068.115 memory used for DFS stack (-m20000000)
1.619 memory lost to fragmentation
6515.375 total actual memory usage
unreached in proctype qrcu_reader
(0 of 18 states)
unreached in proctype qrcu_updater
qrcu.spin:102, state 82, "-end-"
(1 of 82 states)
unreached in init
(0 of 23 states)
pan: elapsed time 2.72e+05 seconds
pan: rate 35500.523 states/second
--------
I'm not sure if this result is worthy enough to be mentioned
in the text.
Thoughts?
Thanks, Akira
> I agree that -DCOLLAPSE is a pure optimization, so it should
> be OK. If we trust the documentation, anyway! ;-)
>
> Thanx, Paul
>
>> Thanks, Akira
>> --
>> Akira Yokosawa (6):
>> fcvextract.pl: Treat '.spin' files as C sources
>> formal/spinhint: Employ new scheme for code snippet
>> formal/spinhint: Update output lists of spin
>> formal/spinhint: Update tables of memory usage of Spin
>> formal/spinhint: Put footnote on header in table
>> formal/spinhint: Use \co{...} rather than {\tt ...}
>>
>> CodeSamples/formal/promela/atomicincrement.spin | 2 +
>> .../formal/promela/atomicincrement.spin.lst | 28 +
>> CodeSamples/formal/promela/increment.spin | 46 +-
>> CodeSamples/formal/promela/increment.spin.lst | 28 +
>> .../formal/promela/increment.spin.trail.lst | 42 +
>> CodeSamples/formal/promela/lock.h | 16 +-
>> CodeSamples/formal/promela/lock.spin | 46 +-
>> CodeSamples/formal/promela/lock.spin.lst | 29 +
>> CodeSamples/formal/promela/qrcu.spin | 95 ++-
>> Makefile | 4 +-
>> formal/spinhint.tex | 874 ++++++---------------
>> perfbook.tex | 1 +
>> utilities/fcvextract.pl | 8 +-
>> 13 files changed, 502 insertions(+), 717 deletions(-)
>> create mode 100644 CodeSamples/formal/promela/atomicincrement.spin.lst
>> create mode 100644 CodeSamples/formal/promela/increment.spin.lst
>> create mode 100644 CodeSamples/formal/promela/increment.spin.trail.lst
>> create mode 100644 CodeSamples/formal/promela/lock.spin.lst
>>
>> --
>> 2.7.4
>>
>
^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [PATCH 0/6] formal/spinhint: Update code snippet
2019-02-06 22:42 ` Akira Yokosawa
@ 2019-02-07 9:17 ` Paul E. McKenney
2019-02-11 15:08 ` [PATCH 0/3] formal/spinhint: Add result and discussion of 3 readers 3 updaters QRCU Spin run Akira Yokosawa
0 siblings, 1 reply; 16+ messages in thread
From: Paul E. McKenney @ 2019-02-07 9:17 UTC (permalink / raw)
To: Akira Yokosawa; +Cc: perfbook
On Thu, Feb 07, 2019 at 07:42:26AM +0900, Akira Yokosawa wrote:
> On 2019/02/02 09:34:37 -0800, Paul E. McKenney wrote:
> > On Sun, Feb 03, 2019 at 12:05:32AM +0900, Akira Yokosawa wrote:
> >> Hi Paul,
> >>
> >> Here is another round of code snippet update, with modernization
> >> of outputs of Spin and tables of state search results.
> >>
> >> Patch #1 updates fcvextract.pl so that .spin files are handled
> >> as the same as C source files.
> >>
> >> Patch #2 applies the new scheme to code snippets. It also contains
> >> minor changes for better typesetting.
> >>
> >> Patch #3 replaces captures of Spin outputs with those obtained
> >> from Spin version 6.4.8. This commit adds outputs as .lst files
> >> under CodeSamples/formal/promela/. They are added to the dependency
> >> in the top level Makefile.
> >>
> >> Patch #4 updates tables of Spin result. For qrcu.spin, I used
> >> the compiler flag -DCOLLAPSE to complete the state search for
> >> updaters=3 readers=2 on a machine with 16GB memory. As far as
> >> I understand correctly, this compiler flag does not affect the
> >> completeness of state search. So I added some explanation in the text
> >> to mention the flag and the argument -mN of ./pan to increase the
> >> limit of search depth.
> >>
> >> Patch #5 tweaks footnote on a cell in a table.
> >>
> >> Patch #6 is a nitpick patch to consistently use \co{}.
> >>
> >> I'm wondering if Patch #4 is OK from your perspective.
> >> Any feedback is welcome!
> >
> > Very good, applied and pushed! I added a small patch on top of Patch #4
> > updating the extrapolation. It was about a terabyte, and is now about
> > half that.
>
> Half a terabyte is not prohibitively large these days, and Spin has
> another compaction option "-DMA=N" which aggressively reduces memory
> consumption in exchange of search speed.
>
> It took three days to complete, with the total memory usage of 6.5GB.
> The output looks as follows:
>
> --------
> (Spin Version 6.4.6 -- 2 December 2016)
> + Partial Order Reduction
> + Graph Encoding (-DMA=96)
>
> Full statespace search for:
> never claim - (none specified)
> assertion violations +
> cycle checks - (disabled by -DSAFETY)
> invalid end states +
>
> State-vector 96 byte, depth reached 2055621, errors: 0
> MA stats: -DMA=84 is sufficient
> Minimized Automaton: 56420520 nodes and 1.75128e+08 edges
> 9.6647071e+09 states, stored
> 9.7503813e+09 states, matched
> 1.9415088e+10 transitions (= stored+matched)
> 7.2047951e+09 atomic steps
>
> Stats on memory usage (in Megabytes):
> 1142905.887 equivalent memory usage for states (stored*(State-vector + overhead))
> 5448.879 actual memory usage for states (compression: 0.48%)
> 1068.115 memory used for DFS stack (-m20000000)
> 1.619 memory lost to fragmentation
> 6515.375 total actual memory usage
>
>
> unreached in proctype qrcu_reader
> (0 of 18 states)
> unreached in proctype qrcu_updater
> qrcu.spin:102, state 82, "-end-"
> (1 of 82 states)
> unreached in init
> (0 of 23 states)
>
> pan: elapsed time 2.72e+05 seconds
> pan: rate 35500.523 states/second
> --------
>
> I'm not sure if this result is worthy enough to be mentioned
> in the text.
But of course!
As long as the entire table is generated with the same arguments and
configuration, and those arguments and configuration are called out
somewhere (perhaps in a script somewhere in CodeSamples), please do
send me a patch!
Perhaps even better would be to call out those configurations and
arguments earlier on in the section giving advice on how to use
Promela and spin.
Thanx, Paul
> Thoughts?
>
> Thanks, Akira
>
> > I agree that -DCOLLAPSE is a pure optimization, so it should
> > be OK. If we trust the documentation, anyway! ;-)
> >
> > Thanx, Paul
> >
> >> Thanks, Akira
> >> --
> >> Akira Yokosawa (6):
> >> fcvextract.pl: Treat '.spin' files as C sources
> >> formal/spinhint: Employ new scheme for code snippet
> >> formal/spinhint: Update output lists of spin
> >> formal/spinhint: Update tables of memory usage of Spin
> >> formal/spinhint: Put footnote on header in table
> >> formal/spinhint: Use \co{...} rather than {\tt ...}
> >>
> >> CodeSamples/formal/promela/atomicincrement.spin | 2 +
> >> .../formal/promela/atomicincrement.spin.lst | 28 +
> >> CodeSamples/formal/promela/increment.spin | 46 +-
> >> CodeSamples/formal/promela/increment.spin.lst | 28 +
> >> .../formal/promela/increment.spin.trail.lst | 42 +
> >> CodeSamples/formal/promela/lock.h | 16 +-
> >> CodeSamples/formal/promela/lock.spin | 46 +-
> >> CodeSamples/formal/promela/lock.spin.lst | 29 +
> >> CodeSamples/formal/promela/qrcu.spin | 95 ++-
> >> Makefile | 4 +-
> >> formal/spinhint.tex | 874 ++++++---------------
> >> perfbook.tex | 1 +
> >> utilities/fcvextract.pl | 8 +-
> >> 13 files changed, 502 insertions(+), 717 deletions(-)
> >> create mode 100644 CodeSamples/formal/promela/atomicincrement.spin.lst
> >> create mode 100644 CodeSamples/formal/promela/increment.spin.lst
> >> create mode 100644 CodeSamples/formal/promela/increment.spin.trail.lst
> >> create mode 100644 CodeSamples/formal/promela/lock.spin.lst
> >>
> >> --
> >> 2.7.4
> >>
> >
>
^ permalink raw reply [flat|nested] 16+ messages in thread
* [PATCH 0/3] formal/spinhint: Add result and discussion of 3 readers 3 updaters QRCU Spin run
2019-02-07 9:17 ` Paul E. McKenney
@ 2019-02-11 15:08 ` Akira Yokosawa
2019-02-11 15:11 ` [PATCH 1/3] formal/spinhint: Add result " Akira Yokosawa
` (2 more replies)
0 siblings, 3 replies; 16+ messages in thread
From: Akira Yokosawa @ 2019-02-11 15:08 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
Hi Paul,
This patch set adds the result and discussion you suggested in this
thread.
Instead of replacing the existing table of memory usage (with the
flag "-DCOLLAPSE"), I added another table comparing the memory usage
and runtime obtained with "-DCOLLAPSE" and "-DMA=N".
Patch #1 adds the result as a summary table and give some discussion
of the usage of the compiler flag "-DMA=N". It also adds a quick
quiz comparing the result of "-DCOLLAPSE" and "-DMA=N" with 2 readers
and 3 updaters.
Patch #2 adds a column of search depth in the existing Table 12.2 of
memory usage with "-DCOLLAPSE". This helps the extrapolation of
necessary search depth for 3 readers and 3 updaters.
Patch #3 is a minor tweak of a footnote in Table 12.2.
It should be possible to reconstruct the story to reference only the
added summary table, but I took another way to minimize the change
of story. The point is that as long as you have sufficient memory,
there is no need to use "-DMA=N". The search speed can be slower
than that with the flag "-DCOLLAPSE" by nearly one order of magnitude.
Any feedback/update is more than welcome!
Thanks, Akira
--
Akira Yokosawa (3):
formal/spinhint: Add result of 3 readers 3 updaters QRCU Spin run
formal/spinhint: Add column of search depth in Table 12.2
formal/spinhint: Place footnote inside floating table
.../formal/promela/atomicincrement.spin.lst | 2 +-
CodeSamples/formal/promela/increment.spin.lst | 2 +-
CodeSamples/formal/promela/lock.spin.lst | 2 +-
CodeSamples/formal/promela/qrcu.spin.33ma.lst | 37 +++++
.../formal/promela/qrcu.spin.col-ma.diff.lst | 48 ++++++
formal/spinhint.tex | 185 ++++++++++++++++++---
perfbook.tex | 2 +-
7 files changed, 254 insertions(+), 24 deletions(-)
create mode 100644 CodeSamples/formal/promela/qrcu.spin.33ma.lst
create mode 100644 CodeSamples/formal/promela/qrcu.spin.col-ma.diff.lst
--
2.7.4
^ permalink raw reply [flat|nested] 16+ messages in thread
* [PATCH 1/3] formal/spinhint: Add result of 3 readers 3 updaters QRCU Spin run
2019-02-11 15:08 ` [PATCH 0/3] formal/spinhint: Add result and discussion of 3 readers 3 updaters QRCU Spin run Akira Yokosawa
@ 2019-02-11 15:11 ` Akira Yokosawa
2019-02-11 15:28 ` Akira Yokosawa
2019-02-11 15:12 ` [PATCH 2/3] formal/spinhint: Add column of search depth in Table 12.2 Akira Yokosawa
2019-02-11 15:13 ` [PATCH 3/3] formal/spinhint: Place footnote inside floating table Akira Yokosawa
2 siblings, 1 reply; 16+ messages in thread
From: Akira Yokosawa @ 2019-02-11 15:11 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From fe701731c7296b90deae52747f5f3be556511289 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Sun, 10 Feb 2019 00:02:26 +0900
Subject: [PATCH 1/3] formal/spinhint: Add result of 3 readers 3 updaters QRCU Spin run
By using the compiler flag "-DMA=N", run of qrcu.spin with 3 readers
and 3 updaters can be completed with the memory usage of 6.5GHz.
This commit adds the result and the command used to run the
verification. A Quick Quiz is added to present an indirect
evidence of search completeness.
As the compiler flag "-DCOLLAPSE" generates much faster code,
memory usage table with "-DCOLLAPSE" is kept. The complete
table for the runs with the flag "-DMA=N" is added as another
table.
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
.../formal/promela/atomicincrement.spin.lst | 2 +-
CodeSamples/formal/promela/increment.spin.lst | 2 +-
CodeSamples/formal/promela/lock.spin.lst | 2 +-
CodeSamples/formal/promela/qrcu.spin.33ma.lst | 37 +++++
.../formal/promela/qrcu.spin.col-ma.diff.lst | 48 +++++++
formal/spinhint.tex | 150 ++++++++++++++++++++-
6 files changed, 234 insertions(+), 7 deletions(-)
create mode 100644 CodeSamples/formal/promela/qrcu.spin.33ma.lst
create mode 100644 CodeSamples/formal/promela/qrcu.spin.col-ma.diff.lst
diff --git a/CodeSamples/formal/promela/atomicincrement.spin.lst b/CodeSamples/formal/promela/atomicincrement.spin.lst
index ab9150b..61dbe54 100644
--- a/CodeSamples/formal/promela/atomicincrement.spin.lst
+++ b/CodeSamples/formal/promela/atomicincrement.spin.lst
@@ -16,7 +16,7 @@ hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.004 equivalent memory usage for states
- (stored*(State-vector + overhead))
+ (stored*(State-vector + overhead))
0.290 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
diff --git a/CodeSamples/formal/promela/increment.spin.lst b/CodeSamples/formal/promela/increment.spin.lst
index 2cab90f..c6765be 100644
--- a/CodeSamples/formal/promela/increment.spin.lst
+++ b/CodeSamples/formal/promela/increment.spin.lst
@@ -21,7 +21,7 @@ hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.003 equivalent memory usage for states
- (stored*(State-vector + overhead))
+ (stored*(State-vector + overhead))
0.290 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
diff --git a/CodeSamples/formal/promela/lock.spin.lst b/CodeSamples/formal/promela/lock.spin.lst
index c9e9efd..807a732 100644
--- a/CodeSamples/formal/promela/lock.spin.lst
+++ b/CodeSamples/formal/promela/lock.spin.lst
@@ -16,7 +16,7 @@ hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.044 equivalent memory usage for states
- (stored*(State-vector + overhead))
+ (stored*(State-vector + overhead))
0.288 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
diff --git a/CodeSamples/formal/promela/qrcu.spin.33ma.lst b/CodeSamples/formal/promela/qrcu.spin.33ma.lst
new file mode 100644
index 0000000..bd43b4c
--- /dev/null
+++ b/CodeSamples/formal/promela/qrcu.spin.33ma.lst
@@ -0,0 +1,37 @@
+(Spin Version 6.4.6 -- 2 December 2016)
+ + Partial Order Reduction
+ + Graph Encoding (-DMA=96)
+
+Full statespace search for:
+ never claim - (none specified)
+ assertion violations +
+ cycle checks - (disabled by -DSAFETY)
+ invalid end states +
+
+State-vector 96 byte, depth reached 2055621, errors: 0
+MA stats: -DMA=84 is sufficient
+Minimized Automaton: 56420520 nodes and 1.75128e+08 edges
+9.6647071e+09 states, stored
+9.7503813e+09 states, matched
+1.9415088e+10 transitions (= stored+matched)
+7.2047951e+09 atomic steps
+
+Stats on memory usage (in Megabytes):
+1142905.887 equivalent memory usage for states
+ (stored*(State-vector + overhead))
+ 5448.879 actual memory usage for states
+ (compression: 0.48%)
+ 1068.115 memory used for DFS stack (-m20000000)
+ 1.619 memory lost to fragmentation
+ 6515.375 total actual memory usage
+
+unreached in proctype qrcu_reader
+ (0 of 18 states)
+unreached in proctype qrcu_updater
+ qrcu.spin:102, state 82, "-end-"
+ (1 of 82 states)
+unreached in init
+ (0 of 23 states)
+
+pan: elapsed time 2.72e+05 seconds
+pan: rate 35500.523 states/second
diff --git a/CodeSamples/formal/promela/qrcu.spin.col-ma.diff.lst b/CodeSamples/formal/promela/qrcu.spin.col-ma.diff.lst
new file mode 100644
index 0000000..61e527d
--- /dev/null
+++ b/CodeSamples/formal/promela/qrcu.spin.col-ma.diff.lst
@@ -0,0 +1,48 @@
+@@ -1,6 +1,6 @@
+ (Spin Version 6.4.6 -- 2 December 2016)
+ + Partial Order Reduction
+- + Compression
++ + Graph Encoding (-DMA=88)
+
+ Full statespace search for:
+ never claim - (none specified)
+@@ -9,27 +9,22 @@
+ invalid end states +
+
+ State-vector 88 byte, depth reached 328014, errors: 0
++MA stats: -DMA=77 is sufficient
++Minimized Automaton: 2084798 nodes and 6.38445e+06 edges
+ 1.8620286e+08 states, stored
+ 1.7759831e+08 states, matched
+ 3.6380117e+08 transitions (= stored+matched)
+ 1.3724093e+08 atomic steps
+-hash conflicts: 1.1445626e+08 (resolved)
+
+ Stats on memory usage (in Megabytes):
+ 20598.919 equivalent memory usage for states
+ (stored*(State-vector + overhead))
+- 8418.559 actual memory usage for states
+- (compression: 40.87%)
+- state-vector as stored =
+- 19 byte + 28 byte overhead
+- 2048.000 memory used for hash table (-w28)
++ 204.907 actual memory usage for states
++ (compression: 0.99%)
+ 17.624 memory used for DFS stack (-m330000)
+- 1.509 memory lost to fragmentation
+-10482.675 total actual memory usage
++ 222.388 total actual memory usage
+
+-nr of templates: [ 0:globals 1:chans 2:procs ]
+-collapse counts: [ 0:1021 2:32 3:1869 4:2 ]
+ unreached in proctype qrcu_reader
+ (0 of 18 states)
+ unreached in proctype qrcu_updater
+@@ -38,5 +33,5 @@
+ unreached in init
+ (0 of 23 states)
+
+-pan: elapsed time 369 seconds
+-pan: rate 505107.58 states/second
++pan: elapsed time 2.68e+03 seconds
++pan: rate 69453.282 states/second
diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index 53e674a..bbbaa10 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -240,7 +240,7 @@ Given a source file \path{qrcu.spin}, one can use the following commands:
\begin{description}[style=nextline]
\item [\tco{spin -a qrcu.spin}]
Create a file \path{pan.c} that fully searches the state machine.
-\item [\tco{cc -DSAFETY [-DCOLLAPSE] -o pan pan.c}]
+\item [\tco{cc -DSAFETY [-DCOLLAPSE] [-DMA=N] -o pan pan.c}]
Compile the generated state-machine search. The \co{-DSAFETY}
generates optimizations that are appropriate if you have only
assertions (and perhaps \co{never} statements). If you have
@@ -256,18 +256,28 @@ Given a source file \path{qrcu.spin}, one can use the following commands:
The optional \co{-DCOLLAPSE} generates code for a state vector
compression mode.
-\item [\tco{./pan [-mN]}]
+
+ Another optional flag \co{-DMA=N} generates code for a slow
+ but aggressive state-space memory compression mode.
+\item [\tco{./pan [-mN] [-wN]}]
This actually searches the state space. The number of states
can reach into the tens of millions with very small state
machines, so you will need a machine with large memory.
For example, \path{qrcu.spin} with 3~updaters and 2~readers required
10.5\,GB of memory even with the \co{-DCOLLAPSE} flag.
- If you see a message from \co{pan} saying:
+ If you see a message from \co{./pan} saying:
``error: max search depth too small'', you need to increase
- the maximum depth by a \co{-mN} flag for a complete search.
+ the maximum depth by a \co{-mN} option for a complete search.
The default is \co{-m10000}.
+ The \co{-wN} option specifies the hashtable size.
+ The default for full state-space search is \co{-w24}.\footnote{
+ As of Spin Version 6.4.6 and 6.4.8. In the online manual of
+ Spin dated 10 July 2011, the default for exhaustive search
+ mode is said to be \co{-w19}, which does not meet
+ the actual behavior.}
+
If you aren't sure whether your machine has enough memory,
run \co{top} in one window and \co{./pan} in another. Keep the
focus on the \co{./pan} window so that you can quickly kill
@@ -880,6 +890,138 @@ Now, it would be nice to run the case with three readers and three
updaters, however, simple extrapolation indicates that this will
require on the order of half a terabyte of memory best case.
So, what to do?
+
+As a last resort for full search of large state spaces,
+Spin provides a compiler flag \co{-DMA=N}
+which generates code for aggressive compression of
+state-space memory in exchange of search speed.
+Use of the flag is suggested in the output of an incomplete run of
+\co{./pan} due to lack of memory.
+An example from three readers and three updaters reads:
+
+\begin{VerbatimU}
+hint: to reduce memory, recompile with
+ -DCOLLAPSE # good, fast compression, or
+ -DMA=96 # better/slower compression, or
+ -DHC # hash-compaction, approximation
+ -DBITSTATE # supertrace, approximation
+\end{VerbatimU}
+
+So let's try the following:
+
+\begin{VerbatimU}
+spin -a qrcu.spin
+cc -DSAFETY -DMA=96 -O2 -o pan pan.c
+./pan -m20000000
+\end{VerbatimU}
+
+Here, the depth limit of 20,000,000 is one order of magnitude
+larger than the expected depth deduced from simple extrapolation.
+This will increase up-front memory usage, but we don't want
+a long run to end up in an incomplete search by specifying
+a tight limit.
+
+It took a little more than 3~days on a \Power{9} server.
+The result is shown in
+Listing~\ref{lst:formal:spinhint:3 Readers 3 Updaters QRCU Spin Output with -DMA=96}.
+As you can see, this Spin run completed with the total memory
+usage of \emph{only} 6.5\,GB, and the model passed this case
+as well.
+
+\begin{listing}
+\VerbatimInput[numbers=none,fontsize=\scriptsize]{CodeSamples/formal/promela/qrcu.spin.33ma.lst}
+\vspace*{-9pt}
+\caption{3 Readers 3 Updaters QRCU Spin Output with \co{-DMA=96}}
+\label{lst:formal:spinhint:3 Readers 3 Updaters QRCU Spin Output with -DMA=96}
+\end{listing}
+
+\QuickQuiz{}
+ Compression rate of 0.48\,\%! Is the state-space search
+ really exhaustive???
+\QuickQuizAnswer{
+ As long as you believe documentation of Spin, yes, it should
+ be.
+
+\begin{listing}
+\VerbatimInput[numbers=none,fontsize=\scriptsize]{CodeSamples/formal/promela/qrcu.spin.col-ma.diff.lst}
+\vspace*{-9pt}
+\caption{Spin Output Diff of \co{-DCOLLAPSE} and \co{-DMA=88}}
+\label{lst:formal:promela:Spin Output Diff of -DCOLLAPSE and -DMA=88}
+\end{listing}
+
+ As an indirect evidence, let's compare the results of
+ runs with \co{-DCOLLAPSE} and with \co{-DMA=88}
+ (two readers and three updaters).
+ The diff of outputs of those runs is shown in
+ Listing~\ref{lst:formal:promela:Spin Output Diff of -DCOLLAPSE and -DMA=88}.
+ As you can see, they agree on the numbers of states
+ (stored and matched).
+} \QuickQuizEnd
+
+\begin{table*}[tbp]
+\rowcolors{6}{}{lightgray}
+\renewcommand*{\arraystretch}{1.2}
+\footnotesize
+\centering
+\OneColumnHSpace{-0.7in}%
+\begin{tabular}{S[table-format = 1.0]S[table-format = 1.0]S[table-format = 9.0]
+ S[table-format = 9.0]S[table-format = 2.0]S[table-format = 5.2]
+ S[table-format = 4.2]S[table-format = 2.0]S[table-format = 4.2]
+ S[table-format = 6.2]}
+ \toprule
+ \multicolumn{4}{r}{} & \multicolumn{3}{c}{\tco{-DCOLLAPSE}} &
+ \multicolumn{3}{c}{\tco{-DMA=N}} \\
+ \cmidrule(l){5-7} \cmidrule(l){8-10}
+ \multicolumn{1}{r}{updaters} &
+ \multicolumn{1}{r}{readers} &
+ \multicolumn{1}{r}{\# states} &
+ \multicolumn{1}{r}{depth reached} &
+ \multicolumn{1}{r}{\tco{-wN}} &
+ \multicolumn{1}{r}{memory (MB)} &
+ \multicolumn{1}{r}{runtime (s)} &
+ \multicolumn{1}{r}{\tco{N}} &
+ \multicolumn{1}{r}{memory (MB)} &
+ \multicolumn{1}{r}{runtime (s)} \\
+ \cmidrule{1-4} \cmidrule(l){5-7} \cmidrule(l){8-10}
+ 1 & 1 & 376 & 95 & 12 & 0.10 & 0.00 &
+ 40 & 0.29 & 0.00 \\
+ 1 & 2 & 6 177 & 218 & 12 & 0.39 & 0.01 &
+ 47 & 0.59 & 0.02 \\
+ 1 & 3 & 99 728 & 385 & 16 & 4.60 & 0.14 &
+ 54 & 3.04 & 0.45 \\
+ 2 & 1 & 29 399 & 859 & 16 & 2.30 & 0.03 &
+ 55 & 0.70 & 0.13 \\
+ 2 & 2 & 1 071 181 & 2 352 & 20 & 49.24 & 1.45 &
+ 62 & 7.77 & 5.76 \\
+ 2 & 3 & 33 866 736 & 12 857 & 24 & 1 540.70 & 62.5 &
+ 69 & 111.66 & 326 \\
+ 3 & 1 & 2 749 453 & 53 809 & 21 & 125.25 & 4.01 &
+ 70 & 11.41 & 19.5 \\
+ 3 & 2 & 186 202 860 & 328 014 & 28 & 10 482.51 & 390 &
+ 77 & 222.26 & 2560 \\
+ 3 & 3 & 9 664 707 100 & 2 055 621 & & & &
+ 84 & 6515.38 & 272000 \\
+ \bottomrule
+\end{tabular}
+\caption{QRCU Spin Result Summary}
+\label{tab:formal:promela:QRCU Spin Result Summary}
+\end{table*}
+
+For reference, Table~\ref{tab:formal:promela:QRCU Spin Result Summary}
+summarizes the Spin results with \co{-DCOLLAPSE} and \co{-DMA=N}
+compiler flags.
+The memory usage is obtained with minimal sufficient
+search depths and \co{-DMA=N} parameters shown in the table.
+As for \co{-DCOLLAPSE}, hash table sizes are tweaked by
+the \co{-wN} option of \co{./pan} to avoid using too much
+memory for hashing small state space. Hence the memory usage is
+smaller than what is shown in
+Table~\ref{tab:advsync:Memory Usage of QRCU Model}.
+The runtime is taken on a \Power{9} server.
+
+So far so good. But as can be easily seen, full state-space search
+would be infeasible if you add a few more updaters\slash readers.
+So what to do?
Here are some possible approaches:
\begin{enumerate}
--
2.7.4
^ permalink raw reply related [flat|nested] 16+ messages in thread
* [PATCH 2/3] formal/spinhint: Add column of search depth in Table 12.2
2019-02-11 15:08 ` [PATCH 0/3] formal/spinhint: Add result and discussion of 3 readers 3 updaters QRCU Spin run Akira Yokosawa
2019-02-11 15:11 ` [PATCH 1/3] formal/spinhint: Add result " Akira Yokosawa
@ 2019-02-11 15:12 ` Akira Yokosawa
2019-02-11 15:13 ` [PATCH 3/3] formal/spinhint: Place footnote inside floating table Akira Yokosawa
2 siblings, 0 replies; 16+ messages in thread
From: Akira Yokosawa @ 2019-02-11 15:12 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From 5c56bad538021adfb91fbb6b65ff0b5544f4e849 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Mon, 11 Feb 2019 08:44:25 +0900
Subject: [PATCH 2/3] formal/spinhint: Add column of search depth in Table 12.2
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
formal/spinhint.tex | 27 ++++++++++++++-------------
1 file changed, 14 insertions(+), 13 deletions(-)
diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index bbbaa10..deddbbc 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -856,26 +856,27 @@ cc -DSAFETY [-DCOLLAPSE] -o pan pan.c
\begin{table}
\rowcolors{1}{}{lightgray}
\renewcommand*{\arraystretch}{1.2}
-\small
+\footnotesize
\centering
\begin{tabular}{S[table-format = 1.0]S[table-format = 1.0]S[table-format = 9.0]
- S[table-format = 5.1]}
+ S[table-format = 6.0]S[table-format = 5.1]}
\toprule
\multicolumn{1}{r}{updaters} &
\multicolumn{1}{r}{readers} &
\multicolumn{1}{r}{\# states} &
- \multicolumn{1}{r}{MB\footnote{
- Obtained with the compiler flag \co{-DCOLLAPSE}
- specified.}} \\
+ \multicolumn{1}{r}{depth} &
+ \multicolumn{1}{r}{memory (MB)\footnote{
+ Obtained with the compiler flag \co{-DCOLLAPSE}
+ specified.}} \\
\midrule
- 1 & 1 & 376 & 128.7 \\
- 1 & 2 & 6 177 & 128.9 \\
- 1 & 3 & 99 728 & 132.6 \\
- 2 & 1 & 29 399 & 129.8 \\
- 2 & 2 & 1 071 181 & 169.6 \\
- 2 & 3 & 33 866 736 & 1 540.8 \\
- 3 & 1 & 2 749 453 & 236.6 \\
- 3 & 2 & 186 202 860 & 10 483.7 \\
+ 1 & 1 & 376 & 95 & 128.7 \\
+ 1 & 2 & 6 177 & 218 & 128.9 \\
+ 1 & 3 & 99 728 & 385 & 132.6 \\
+ 2 & 1 & 29 399 & 859 & 129.8 \\
+ 2 & 2 & 1 071 181 & 2 352 & 169.6 \\
+ 2 & 3 & 33 866 736 & 12 857 & 1 540.8 \\
+ 3 & 1 & 2 749 453 & 53 809 & 236.6 \\
+ 3 & 2 & 186 202 860 & 328 014 & 10 483.7 \\
\bottomrule
\end{tabular}
\caption{Memory Usage of QRCU Model}
--
2.7.4
^ permalink raw reply related [flat|nested] 16+ messages in thread
* [PATCH 3/3] formal/spinhint: Place footnote inside floating table
2019-02-11 15:08 ` [PATCH 0/3] formal/spinhint: Add result and discussion of 3 readers 3 updaters QRCU Spin run Akira Yokosawa
2019-02-11 15:11 ` [PATCH 1/3] formal/spinhint: Add result " Akira Yokosawa
2019-02-11 15:12 ` [PATCH 2/3] formal/spinhint: Add column of search depth in Table 12.2 Akira Yokosawa
@ 2019-02-11 15:13 ` Akira Yokosawa
2 siblings, 0 replies; 16+ messages in thread
From: Akira Yokosawa @ 2019-02-11 15:13 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From 05dd848e5c6610278ed6975bcb3cab256b9136d4 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Mon, 11 Feb 2019 10:43:57 +0900
Subject: [PATCH 3/3] formal/spinhint: Place footnote inside floating table
It turns out the "savenotes" environment tried in commit
5df9ce3b9449 ("formal/spinhint: Put footnote on header in table")
is not robust enough. Depending on the layout, text of a footnote
can appear at the bottom of a page ahead of (or behind) the page
where the floating table itself is typeset.
Putting such footnotes inside a floating table by the help of the
"threeparttable" package looks like an orthodox way recommended
in the LaTeX community [1].
[1]: https://texfaq.org/FAQ-footintab
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
formal/spinhint.tex | 14 ++++++++------
perfbook.tex | 2 +-
2 files changed, 9 insertions(+), 7 deletions(-)
diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index deddbbc..cee1c59 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -852,12 +852,12 @@ cc -DSAFETY [-DCOLLAPSE] -o pan pan.c
./pan [-mN]
\end{VerbatimU}
-\begin{savenotes}
\begin{table}
+\centering
+\begin{threeparttable}
\rowcolors{1}{}{lightgray}
\renewcommand*{\arraystretch}{1.2}
\footnotesize
-\centering
\begin{tabular}{S[table-format = 1.0]S[table-format = 1.0]S[table-format = 9.0]
S[table-format = 6.0]S[table-format = 5.1]}
\toprule
@@ -865,9 +865,7 @@ cc -DSAFETY [-DCOLLAPSE] -o pan pan.c
\multicolumn{1}{r}{readers} &
\multicolumn{1}{r}{\# states} &
\multicolumn{1}{r}{depth} &
- \multicolumn{1}{r}{memory (MB)\footnote{
- Obtained with the compiler flag \co{-DCOLLAPSE}
- specified.}} \\
+ \multicolumn{1}{r}{memory (MB)\tnote{a}} \\
\midrule
1 & 1 & 376 & 95 & 128.7 \\
1 & 2 & 6 177 & 218 & 128.9 \\
@@ -879,10 +877,14 @@ cc -DSAFETY [-DCOLLAPSE] -o pan pan.c
3 & 2 & 186 202 860 & 328 014 & 10 483.7 \\
\bottomrule
\end{tabular}
+\begin{tablenotes}
+ \item [a] Obtained with the compiler flag \co{-DCOLLAPSE}
+ specified.
+\end{tablenotes}
+\end{threeparttable}
\caption{Memory Usage of QRCU Model}
\label{tab:advsync:Memory Usage of QRCU Model}
\end{table}
-\end{savenotes}
The resulting output shows that this model passes all of the cases
shown in
diff --git a/perfbook.tex b/perfbook.tex
index c740619..9caeee8 100644
--- a/perfbook.tex
+++ b/perfbook.tex
@@ -52,7 +52,7 @@
\usepackage[bottom]{footmisc} % place footnotes under floating figures/tables
\usepackage{tabularx}
\usepackage[hyphens]{url}
-\usepackage{footnote}
+\usepackage{threeparttable}
\usepackage[bookmarks=true,bookmarksnumbered=true,pdfborder={0 0 0}]{hyperref}
\usepackage{footnotebackref} % to enable cross-ref of footnote
\usepackage[all]{hypcap} % for going to the top of figure and table
--
2.7.4
^ permalink raw reply related [flat|nested] 16+ messages in thread
* Re: [PATCH 1/3] formal/spinhint: Add result of 3 readers 3 updaters QRCU Spin run
2019-02-11 15:11 ` [PATCH 1/3] formal/spinhint: Add result " Akira Yokosawa
@ 2019-02-11 15:28 ` Akira Yokosawa
2019-02-11 19:34 ` Paul E. McKenney
0 siblings, 1 reply; 16+ messages in thread
From: Akira Yokosawa @ 2019-02-11 15:28 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
Paul,
There was a typo in the commit log.
On 2019/02/12 00:11:23 +0900, Akira Yokosawa wrote:
> From fe701731c7296b90deae52747f5f3be556511289 Mon Sep 17 00:00:00 2001
> From: Akira Yokosawa <akiyks@gmail.com>
> Date: Sun, 10 Feb 2019 00:02:26 +0900
> Subject: [PATCH 1/3] formal/spinhint: Add result of 3 readers 3 updaters QRCU Spin run
>
> By using the compiler flag "-DMA=N", run of qrcu.spin with 3 readers
> and 3 updaters can be completed with the memory usage of 6.5GHz.
^^^^
6.5GB.
Can you amend it for me?
Thanks, Akira
>
> This commit adds the result and the command used to run the
> verification. A Quick Quiz is added to present an indirect
> evidence of search completeness.
>
> As the compiler flag "-DCOLLAPSE" generates much faster code,
> memory usage table with "-DCOLLAPSE" is kept. The complete
> table for the runs with the flag "-DMA=N" is added as another
> table.
>
> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> ---
> .../formal/promela/atomicincrement.spin.lst | 2 +-
> CodeSamples/formal/promela/increment.spin.lst | 2 +-
> CodeSamples/formal/promela/lock.spin.lst | 2 +-
> CodeSamples/formal/promela/qrcu.spin.33ma.lst | 37 +++++
> .../formal/promela/qrcu.spin.col-ma.diff.lst | 48 +++++++
> formal/spinhint.tex | 150 ++++++++++++++++++++-
> 6 files changed, 234 insertions(+), 7 deletions(-)
> create mode 100644 CodeSamples/formal/promela/qrcu.spin.33ma.lst
> create mode 100644 CodeSamples/formal/promela/qrcu.spin.col-ma.diff.lst
>
[...]
^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [PATCH 1/3] formal/spinhint: Add result of 3 readers 3 updaters QRCU Spin run
2019-02-11 15:28 ` Akira Yokosawa
@ 2019-02-11 19:34 ` Paul E. McKenney
0 siblings, 0 replies; 16+ messages in thread
From: Paul E. McKenney @ 2019-02-11 19:34 UTC (permalink / raw)
To: Akira Yokosawa; +Cc: perfbook
On Tue, Feb 12, 2019 at 12:28:12AM +0900, Akira Yokosawa wrote:
> Paul,
>
> There was a typo in the commit log.
>
> On 2019/02/12 00:11:23 +0900, Akira Yokosawa wrote:
> > From fe701731c7296b90deae52747f5f3be556511289 Mon Sep 17 00:00:00 2001
> > From: Akira Yokosawa <akiyks@gmail.com>
> > Date: Sun, 10 Feb 2019 00:02:26 +0900
> > Subject: [PATCH 1/3] formal/spinhint: Add result of 3 readers 3 updaters QRCU Spin run
> >
> > By using the compiler flag "-DMA=N", run of qrcu.spin with 3 readers
> > and 3 updaters can be completed with the memory usage of 6.5GHz.
>
> ^^^^
> 6.5GB.
>
> Can you amend it for me?
Done! I queued and pushed all three, and also pushed out some minor
wordsmithing. Please let me know if I messed anything up.
And nice approach showing the strengths and weaknesses of the two
approaches, good stuff, thank you!
Thanx, Paul
> Thanks, Akira
>
> >
> > This commit adds the result and the command used to run the
> > verification. A Quick Quiz is added to present an indirect
> > evidence of search completeness.
> >
> > As the compiler flag "-DCOLLAPSE" generates much faster code,
> > memory usage table with "-DCOLLAPSE" is kept. The complete
> > table for the runs with the flag "-DMA=N" is added as another
> > table.
> >
> > Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> > ---
> > .../formal/promela/atomicincrement.spin.lst | 2 +-
> > CodeSamples/formal/promela/increment.spin.lst | 2 +-
> > CodeSamples/formal/promela/lock.spin.lst | 2 +-
> > CodeSamples/formal/promela/qrcu.spin.33ma.lst | 37 +++++
> > .../formal/promela/qrcu.spin.col-ma.diff.lst | 48 +++++++
> > formal/spinhint.tex | 150 ++++++++++++++++++++-
> > 6 files changed, 234 insertions(+), 7 deletions(-)
> > create mode 100644 CodeSamples/formal/promela/qrcu.spin.33ma.lst
> > create mode 100644 CodeSamples/formal/promela/qrcu.spin.col-ma.diff.lst
> >
> [...]
>
^ permalink raw reply [flat|nested] 16+ messages in thread
end of thread, other threads:[~2019-02-11 19:34 UTC | newest]
Thread overview: 16+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2019-02-02 15:05 [PATCH 0/6] formal/spinhint: Update code snippet Akira Yokosawa
2019-02-02 15:08 ` [PATCH 1/6] fcvextract.pl: Treat '.spin' files as C sources Akira Yokosawa
2019-02-02 15:09 ` [PATCH 2/6] formal/spinhint: Employ new scheme for code snippet Akira Yokosawa
2019-02-02 15:11 ` [PATCH 3/6] formal/spinhint: Update output lists of spin Akira Yokosawa
2019-02-02 15:13 ` [PATCH 4/6] formal/spinhint: Update tables of memory usage of Spin Akira Yokosawa
2019-02-02 15:14 ` [PATCH 5/6] formal/spinhint: Put footnote on header in table Akira Yokosawa
2019-02-02 15:15 ` [PATCH 6/6] formal/spinhint: Use \co{...} rather than {\tt ...} Akira Yokosawa
2019-02-02 17:34 ` [PATCH 0/6] formal/spinhint: Update code snippet Paul E. McKenney
2019-02-06 22:42 ` Akira Yokosawa
2019-02-07 9:17 ` Paul E. McKenney
2019-02-11 15:08 ` [PATCH 0/3] formal/spinhint: Add result and discussion of 3 readers 3 updaters QRCU Spin run Akira Yokosawa
2019-02-11 15:11 ` [PATCH 1/3] formal/spinhint: Add result " Akira Yokosawa
2019-02-11 15:28 ` Akira Yokosawa
2019-02-11 19:34 ` Paul E. McKenney
2019-02-11 15:12 ` [PATCH 2/3] formal/spinhint: Add column of search depth in Table 12.2 Akira Yokosawa
2019-02-11 15:13 ` [PATCH 3/3] formal/spinhint: Place footnote inside floating table Akira Yokosawa
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.