* [PATCH 1/2] formal/spinhint: Update memory usage in QRCU Spin summary table @ 2019-02-13 15:17 Akira Yokosawa 2019-02-13 15:19 ` [PATCH 2/2] formal/spinhint: Substitute ':formal:' for ':analysis:' in labels Akira Yokosawa 0 siblings, 1 reply; 3+ messages in thread From: Akira Yokosawa @ 2019-02-13 15:17 UTC (permalink / raw) To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa From 28d0c3ce44cc2267b2a27aef333c5b15511b8125 Mon Sep 17 00:00:00 2001 From: Akira Yokosawa <akiyks@gmail.com> Date: Wed, 13 Feb 2019 23:26:07 +0900 Subject: [PATCH 1/2] formal/spinhint: Update memory usage in QRCU Spin summary table The memory usage and runtime data of 3 readers and 3 updaters presented in Table 12.3 were from a run with a depth limit an order of magnitude larger than the reached depth. Update the data from a just finished run with a tighter depth limit. Also fix a typo and substitute "Spin" for "spin" for consistency. Signed-off-by: Akira Yokosawa <akiyks@gmail.com> --- formal/spinhint.tex | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/formal/spinhint.tex b/formal/spinhint.tex index 39826cd..231d861 100644 --- a/formal/spinhint.tex +++ b/formal/spinhint.tex @@ -6,12 +6,12 @@ \epigraph{Follow every byway / Every path you know.} {\emph{``Climb Every Mountain'', Rodgers \& Hammerstein}} -This section features the general-purpose Promela and spin tools, +This section features the general-purpose Promela and Spin tools, which may be used to carry out a full state-space search of many types of multi-threaded code. They are also quite useful for verifying data communication protocols. Section~\ref{sec:formal:Promela and Spin} -introduces Promela and spin, including a couple of warm-up exercises +introduces Promela and Spin, including a couple of warm-up exercises verifying both non-atomic and atomic increment. Section~\ref{sec:formal:How to Use Promela} describes use of Promela, including example command lines and a @@ -133,12 +133,12 @@ cc -DSAFETY -o pan pan.c # Compile the model \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} +\caption{Non-Atomic Increment Spin Output} +\label{lst:analysis: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:analysis: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 @@ -182,8 +182,8 @@ The assertion then triggered, after which the global state is displayed. \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} +\caption{Atomic Increment Spin Output} +\label{lst:analysis:Atomic Increment Spin Output} \end{listing} It is easy to fix this example by placing the body of the incrementer @@ -194,7 +194,7 @@ One could also have simply replaced the pair of statements with 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:analysis:Atomic Increment Spin Output}. \begin{table} \rowcolors{1}{}{lightgray} @@ -999,7 +999,7 @@ lower than the \co{-DCOLLAPSE} usage of about half a terabyte. 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 \\ + 84 & 5557.02 & 266000 \\ \bottomrule \end{tabular} \caption{QRCU Spin Result Summary} @@ -1019,7 +1019,7 @@ Table~\ref{tab:advsync:Memory Usage of QRCU Model}, where the hashtable size starts from the default of \co{-w24}. The runtime is from a \Power{9} server, which shows that \co{-DMA=N} suffers up to about an order of magnitude higher CPU overhead -than does \co{-DCOLLAPSE}, but on the other hand reduces memroy overhead +than does \co{-DCOLLAPSE}, but on the other hand reduces memory overhead by well over an order of magnitude. So far so good. -- 2.7.4 ^ permalink raw reply related [flat|nested] 3+ messages in thread
* [PATCH 2/2] formal/spinhint: Substitute ':formal:' for ':analysis:' in labels 2019-02-13 15:17 [PATCH 1/2] formal/spinhint: Update memory usage in QRCU Spin summary table Akira Yokosawa @ 2019-02-13 15:19 ` Akira Yokosawa 2019-02-13 16:05 ` Paul E. McKenney 0 siblings, 1 reply; 3+ messages in thread From: Akira Yokosawa @ 2019-02-13 15:19 UTC (permalink / raw) To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa From 44d794c92379e3a939f50cfac1acf7646b22fc16 Mon Sep 17 00:00:00 2001 From: Akira Yokosawa <akiyks@gmail.com> 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@gmail.com> --- 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@whole.fcv} \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@incrementer.fcv} \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@whole.fcv} \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@spin.fcv} \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@gvar.fcv} \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@reader.fcv} \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@updater.fcv} \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@init.fcv} \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 ^ permalink raw reply related [flat|nested] 3+ messages in thread
* Re: [PATCH 2/2] formal/spinhint: Substitute ':formal:' for ':analysis:' in labels 2019-02-13 15:19 ` [PATCH 2/2] formal/spinhint: Substitute ':formal:' for ':analysis:' in labels Akira Yokosawa @ 2019-02-13 16:05 ` Paul E. McKenney 0 siblings, 0 replies; 3+ messages in thread From: Paul E. McKenney @ 2019-02-13 16:05 UTC (permalink / raw) To: Akira Yokosawa; +Cc: perfbook On Thu, Feb 14, 2019 at 12:19:38AM +0900, Akira Yokosawa wrote: > >From 44d794c92379e3a939f50cfac1acf7646b22fc16 Mon Sep 17 00:00:00 2001 > From: Akira Yokosawa <akiyks@gmail.com> > 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@gmail.com> Good catches, and good updates on the first patch, thank you! I have queued and pushed both of them. Thanx, Paul > --- > 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@whole.fcv} > \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@incrementer.fcv} > \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@whole.fcv} > \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@spin.fcv} > \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@gvar.fcv} > \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@reader.fcv} > \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@updater.fcv} > \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@init.fcv} > \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 > > ^ permalink raw reply [flat|nested] 3+ messages in thread
end of thread, other threads:[~2019-02-13 16:05 UTC | newest] Thread overview: 3+ messages (download: mbox.gz follow: Atom feed -- links below jump to the message on this page -- 2019-02-13 15:17 [PATCH 1/2] formal/spinhint: Update memory usage in QRCU Spin summary table Akira Yokosawa 2019-02-13 15:19 ` [PATCH 2/2] formal/spinhint: Substitute ':formal:' for ':analysis:' in labels Akira Yokosawa 2019-02-13 16:05 ` Paul E. McKenney
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.