>From 44d794c92379e3a939f50cfac1acf7646b22fc16 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@xxxxxxxxx>
Date: Wed, 13 Feb 2019 23:54:04 +0900
Subject: [PATCH 2/2] formal/spinhint: Substitute ':formal:' for ':analysis:' in labels
These historic labels have somehow survived reorganization of
chapters.
Signed-off-by: Akira Yokosawa <akiyks@xxxxxxxxx>
---
formal/dyntickrcu.tex | 4 ++--
formal/spinhint.tex | 64 +++++++++++++++++++++++++--------------------------
2 files changed, 34 insertions(+), 34 deletions(-)
diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
index 41b8bf1..5b2bfed 100644
--- a/formal/dyntickrcu.tex
+++ b/formal/dyntickrcu.tex
@@ -493,8 +493,8 @@ re-entering dynticks-idle mode (for example, that same task blocking).
it is not necessary to model memory barriers.
In fact, one must instead explicitly model lack of memory barriers,
for example, as shown in
- Listing~\ref{lst:analysis:QRCU Unordered Summation} on
- page~\pageref{lst:analysis:QRCU Unordered Summation}.
+ Listing~\ref{lst:formal:QRCU Unordered Summation} on
+ page~\pageref{lst:formal:QRCU Unordered Summation}.
} \QuickQuizEnd
\QuickQuiz{}
diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index 231d861..5a6c08c 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -64,11 +64,11 @@ more complex uses.
\begin{listing}[tbp]
\input{CodeSamples/formal/promela/increment@xxxxxxxxx}
\caption{Promela Code for Non-Atomic Increment}
-\label{lst:analysis:Promela Code for Non-Atomic Increment}
+\label{lst:formal: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}
+Listing~\ref{lst:formal:Promela Code for Non-Atomic Increment}
demonstrates the textbook race condition
resulting from non-atomic increment.
Line~\lnref{nprocs} defines the number of processes to run (we will vary this
@@ -134,11 +134,11 @@ cc -DSAFETY -o pan pan.c # Compile the model
\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}
+\label{lst:formal:Non-Atomic Increment Spin Output}
\end{listing}
This will produce output as shown in
-Listing~\ref{lst:analysis:Non-Atomic Increment Spin Output}.
+Listing~\ref{lst:formal:Non-Atomic Increment Spin Output}.
The first line tells us that our assertion was violated (as expected
given the non-atomic increment!).
The second line that a \co{trail} file was written describing how the
@@ -160,11 +160,11 @@ spin -t -p increment.spin
\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}
+\label{lst:formal:Non-Atomic Increment Error Trail}
\end{listing*}
This gives the output shown in
-Listing~\ref{lst:analysis:Non-Atomic Increment Error Trail}.
+Listing~\ref{lst:formal:Non-Atomic Increment Error Trail}.
As can be seen, the first portion of the init block created both
incrementer processes, both of which first fetched the counter,
then both incremented and stored it, losing a count.
@@ -176,25 +176,25 @@ The assertion then triggered, after which the global state is displayed.
\begin{listing}[htbp]
\input{CodeSamples/formal/promela/atomicincrement@xxxxxxxxxxxxxxx}
\caption{Promela Code for Atomic Increment}
-\label{lst:analysis:Promela Code for Atomic Increment}
+\label{lst:formal:Promela Code for Atomic Increment}
\end{listing}
\begin{listing}[htbp]
\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}
+\label{lst:formal:Atomic Increment Spin Output}
\end{listing}
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}.
+Listing~\ref{lst:formal:Promela Code for Atomic Increment}.
One could also have simply replaced the pair of statements with
\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
-Listing~\ref{lst:analysis:Atomic Increment Spin Output}.
+Listing~\ref{lst:formal:Atomic Increment Spin Output}.
\begin{table}
\rowcolors{1}{}{lightgray}
@@ -406,14 +406,14 @@ fi
them under \co{atomic}. After all, they are not part of the
algorithm. One example of a complex assertion (to be discussed
in more detail later) is as shown in
- Listing~\ref{lst:analysis:Complex Promela Assertion}.
+ Listing~\ref{lst:formal:Complex Promela Assertion}.
There is no reason to evaluate this assertion
non-atomically, since it is not actually part of the algorithm.
Because each statement contributes to state, we can reduce
the number of useless states by enclosing it in an \co{atomic}
block as shown in
- Listing~\ref{lst:analysis:Atomic Block for Complex Promela Assertion}.
+ Listing~\ref{lst:formal:Atomic Block for Complex Promela Assertion}.
\item Promela does not provide functions.
You must instead use C preprocessor macros.
@@ -436,7 +436,7 @@ do
od
\end{VerbatimL}
\caption{Complex Promela Assertion}
-\label{lst:analysis:Complex Promela Assertion}
+\label{lst:formal:Complex Promela Assertion}
\end{listing}
\begin{listing}[tbp]
@@ -456,7 +456,7 @@ atomic {
}
\end{VerbatimL}
\caption{Atomic Block for Complex Promela Assertion}
-\label{lst:analysis:Atomic Block for Complex Promela Assertion}
+\label{lst:formal:Atomic Block for Complex Promela Assertion}
\end{listing}
Now we are ready for more complex examples.
@@ -467,7 +467,7 @@ Now we are ready for more complex examples.
\begin{listing}[tbp]
\input{CodeSamples/formal/promela/lock@xxxxxxxxx}
\caption{Promela Code for Spinlock}
-\label{lst:analysis:Promela Code for Spinlock}
+\label{lst:formal:Promela Code for Spinlock}
\end{listing}
\begin{lineref}[ln:formal:promela:lock:whole]
@@ -475,7 +475,7 @@ 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}.
+Listing~\ref{lst:formal:Promela Code for Spinlock}.
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}.
@@ -509,12 +509,12 @@ weak memory ordering must be explicitly coded.
\begin{listing}[tb]
\input{CodeSamples/formal/promela/lock@xxxxxxxx}
\caption{Promela Code to Test Spinlocks}
-\label{lst:analysis:Promela Code to Test Spinlocks}
+\label{lst:formal: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}.
+Listing~\ref{lst:formal: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~\lnref{nlockers}.
@@ -542,8 +542,8 @@ 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}
-and~\ref{lst:analysis:Promela Code to Test Spinlocks} into
+Listings~\ref{lst:formal:Promela Code for Spinlock}
+and~\ref{lst:formal:Promela Code to Test Spinlocks} into
files named \path{lock.h} and \path{lock.spin}, respectively, and then running
the following commands:
@@ -557,11 +557,11 @@ cc -DSAFETY -o pan pan.c
\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}
+\label{lst:formal:Output for Spinlock Test}
\end{listing}
The output will look something like that shown in
-Listing~\ref{lst:analysis:Output for Spinlock Test}.
+Listing~\ref{lst:formal:Output for Spinlock Test}.
As expected, this run has no assertion failures (``errors: 0'').
\QuickQuiz{}
@@ -656,11 +656,11 @@ April 2008.
\begin{listing}[htbp]
\input{CodeSamples/formal/promela/qrcu@xxxxxxxx}
\caption{QRCU Global Variables}
-\label{lst:analysis:QRCU Global Variables}
+\label{lst:formal:QRCU Global Variables}
\end{listing}
Returning to the Promela code for QRCU, the global variables are as shown in
-Listing~\ref{lst:analysis:QRCU Global Variables}.
+Listing~\ref{lst:formal:QRCU Global Variables}.
This example uses locking, hence including \path{lock.h}.
Both the number of readers and writers can be varied using the
two \co{#define} statements, giving us not one but two ways to create
@@ -685,12 +685,12 @@ Finally, the \co{mutex} variable is used to serialize updaters' slowpaths.
\begin{listing}[htbp]
\input{CodeSamples/formal/promela/qrcu@xxxxxxxxxx}
\caption{QRCU Reader Process}
-\label{lst:analysis:QRCU Reader Process}
+\label{lst:formal: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}.
+Listing~\ref{lst:formal:QRCU Reader Process}.
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.
@@ -709,12 +709,12 @@ thereby exiting the RCU read-side critical section.
\begin{listing}[htbp]
\input{CodeSamples/formal/promela/qrcu@sum_unordered.fcv}
\caption{QRCU Unordered Summation}
-\label{lst:analysis:QRCU Unordered Summation}
+\label{lst:formal: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}
+Listing~\ref{lst:formal:QRCU Unordered Summation}
sums the pair of counters so as to emulate weak memory ordering.
Lines~\lnref{fetch:b}-\lnref{fetch:e} fetch one of the counters,
and line~\lnref{sum_other} fetches the other
@@ -742,13 +742,13 @@ to 0 (so that line~\lnref{sum_other} will fetch the second counter).
\begin{listing}[htbp]
\input{CodeSamples/formal/promela/qrcu@xxxxxxxxxxx}
\caption{QRCU Updater Process}
-\label{lst:analysis:QRCU Updater Process}
+\label{lst:formal: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}.
+Listing~\ref{lst:formal:QRCU Updater Process}.
The update-side process repeats indefinitely, with the corresponding
\co{do-od} loop ranging over lines~\lnref{do}-\lnref{od}.
Each pass through the loop first snapshots the global \co{readerprogress}
@@ -823,12 +823,12 @@ this update still be in progress.
\begin{listing}[htbp]
\input{CodeSamples/formal/promela/qrcu@xxxxxxxx}
\caption{QRCU Initialization Process}
-\label{lst:analysis:QRCU Initialization Process}
+\label{lst:formal: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}.
+Listing~\ref{lst:formal:QRCU Initialization Process}.
This block simply initializes the counter pair on
lines~\lnref{i_ctr:b}-\lnref{i_ctr:e},
spawns the reader processes on
--
2.7.4
