* [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