On Fri, Oct 13, 2017 at 12:39:37AM +0900, Akira Yokosawa wrote:
> >From 22e222957a1e08b744380d681cc2eb67097314d7 Mon Sep 17 00:00:00 2001
> From: Akira Yokosawa <akiyks@xxxxxxxxx>
> Date: Fri, 13 Oct 2017 00:34:22 +0900
> Subject: [PATCH] Convert code snippets to 'listing' env (datastruct, debugging, formal)
>
> Also convert those in SMPdesign/beyond.tex.
Queued and pushed, thank you!
Thanx, Paul
> Signed-off-by: Akira Yokosawa <akiyks@xxxxxxxxx>
> ---
> SMPdesign/beyond.tex | 46 +++++++-------
> datastruct/datastruct.tex | 158 +++++++++++++++++++++++-----------------------
> debugging/debugging.tex | 20 +++---
> formal/axiomatic.tex | 18 +++---
> formal/dyntickrcu.tex | 80 +++++++++++------------
> formal/ppcmem.tex | 38 +++++------
> formal/spinhint.tex | 124 ++++++++++++++++++------------------
> 7 files changed, 242 insertions(+), 242 deletions(-)
>
> diff --git a/SMPdesign/beyond.tex b/SMPdesign/beyond.tex
> index 1fb2a6b..65f2518 100644
> --- a/SMPdesign/beyond.tex
> +++ b/SMPdesign/beyond.tex
> @@ -53,7 +53,7 @@ presents future directions and concluding remarks.
> \subsection{Work-Queue Parallel Maze Solver}
> \label{sec:SMPdesign:Work-Queue Parallel Maze Solver}
>
> -\begin{figure}[tbp]
> +\begin{listing}[tbp]
> { \scriptsize
> \begin{verbbox}
> 1 int maze_solve(maze *mp, cell sc, cell ec)
> @@ -83,11 +83,11 @@ presents future directions and concluding remarks.
> \centering
> \theverbbox
> \caption{SEQ Pseudocode}
> -\label{fig:SMPdesign:SEQ Pseudocode}
> -\end{figure}
> +\label{lst:SMPdesign:SEQ Pseudocode}
> +\end{listing}
>
> PWQ is based on SEQ, which is shown in
> -Figure~\ref{fig:SMPdesign:SEQ Pseudocode}
> +Listing~\ref{lst:SMPdesign:SEQ Pseudocode}
> (\path{maze_seq.c}).
> The maze is represented by a 2D array of cells and
> a linear-array-based work queue named \co{->visited}.
> @@ -99,7 +99,7 @@ visited cell with an unvisited neighbor, and the loop spanning
> lines~14-19 traverses one fork of the submaze headed by that neighbor.
> Line~20 initializes for the next pass through the outer loop.
>
> -\begin{figure}[tbp]
> +\begin{listing}[tbp]
> { \scriptsize
> \begin{verbbox}
> 1 int maze_try_visit_cell(struct maze *mp, cell c, cell t,
> @@ -135,11 +135,11 @@ Line~20 initializes for the next pass through the outer loop.
> \centering
> \theverbbox
> \caption{SEQ Helper Pseudocode}
> -\label{fig:SMPdesign:SEQ Helper Pseudocode}
> -\end{figure}
> +\label{lst:SMPdesign:SEQ Helper Pseudocode}
> +\end{listing}
>
> The pseudocode for \co{maze_try_visit_cell()} is shown on lines~1-12
> -of Figure~\ref{fig:SMPdesign:SEQ Helper Pseudocode}
> +of Listing~\ref{lst:SMPdesign:SEQ Helper Pseudocode}
> (\path{maze.c}).
> Line~4 checks to see if cells \co{c} and \co{n} are adjacent and connected,
> while line~5 checks to see if cell \co{n} has not yet been visited.
> @@ -151,7 +151,7 @@ is now full, and line~10 marks this cell as visited and also records
> the distance from the maze start. Line~11 then returns success.
>
> The pseudocode for \co{maze_find_any_next_cell()} is shown on lines~14-28
> -of Figure~\ref{fig:SMPdesign:SEQ Helper Pseudocode}
> +of Listing~\ref{lst:SMPdesign:SEQ Helper Pseudocode}
> (\path{maze.c}).
> Line~17 picks up the current cell's distance plus 1,
> while lines~19, 21, 23, and~25
> @@ -185,13 +185,13 @@ consecutively decreasing cell numbers traverses the solution.
>
> The parallel work-queue solver is a straightforward parallelization
> of the algorithm shown in
> -Figures~\ref{fig:SMPdesign:SEQ Pseudocode} and ~\ref{fig:SMPdesign:SEQ Helper Pseudocode}.
> -Line~10 of Figure~\ref{fig:SMPdesign:SEQ Pseudocode} must use fetch-and-add,
> +Listings~\ref{lst:SMPdesign:SEQ Pseudocode} and~\ref{lst:SMPdesign:SEQ Helper Pseudocode}.
> +Line~10 of Listing~\ref{lst:SMPdesign:SEQ Pseudocode} must use fetch-and-add,
> and the local variable \co{vi} must be shared among the various threads.
> -Lines~5 and~10 of Figure~\ref{fig:SMPdesign:SEQ Helper Pseudocode} must be
> +Lines~5 and~10 of Listing~\ref{lst:SMPdesign:SEQ Helper Pseudocode} must be
> combined into a CAS loop, with CAS failure indicating a loop in the
> maze.
> -Lines~8-9 of this figure must use fetch-and-add to arbitrate concurrent
> +Lines~8-9 of this listing must use fetch-and-add to arbitrate concurrent
> attempts to record cells in the \co{->visited[]} array.
>
> This approach does provide significant speedups on a dual-CPU
> @@ -227,7 +227,7 @@ This section applies this strategy, using two child threads that start
> at opposite ends of the solution path, and takes a brief look at the
> performance and scalability consequences.
>
> -\begin{figure}[tbp]
> +\begin{listing}[tbp]
> { \scriptsize
> \begin{verbbox}
> 1 int maze_solve_child(maze *mp, cell *visited, cell sc)
> @@ -260,11 +260,11 @@ performance and scalability consequences.
> \centering
> \theverbbox
> \caption{Partitioned Parallel Solver Pseudocode}
> -\label{fig:SMPdesign:Partitioned Parallel Solver Pseudocode}
> -\end{figure}
> +\label{lst:SMPdesign:Partitioned Parallel Solver Pseudocode}
> +\end{listing}
>
> The partitioned parallel algorithm (PART), shown in
> -Figure~\ref{fig:SMPdesign:Partitioned Parallel Solver Pseudocode}
> +Listing~\ref{lst:SMPdesign:Partitioned Parallel Solver Pseudocode}
> (\path{maze_part.c}),
> is similar to SEQ, but has a few important differences.
> First, each child thread has its own \co{visited} array, passed in by
> @@ -290,7 +290,7 @@ compare-and-swap to mark a cell as visited, however
> no constraints on ordering are required beyond those provided by
> thread creation and join.
>
> -\begin{figure}[tbp]
> +\begin{listing}[tbp]
> { \scriptsize
> \begin{verbbox}
> 1 int maze_try_visit_cell(struct maze *mp, int c, int t,
> @@ -321,14 +321,14 @@ thread creation and join.
> \centering
> \theverbbox
> \caption{Partitioned Parallel Helper Pseudocode}
> -\label{fig:SMPdesign:Partitioned Parallel Helper Pseudocode}
> -\end{figure}
> +\label{lst:SMPdesign:Partitioned Parallel Helper Pseudocode}
> +\end{listing}
>
> The pseudocode for \co{maze_find_any_next_cell()} is identical to that shown in
> -Figure~\ref{fig:SMPdesign:SEQ Helper Pseudocode},
> +Listing~\ref{lst:SMPdesign:SEQ Helper Pseudocode},
> but the pseudocode for \co{maze_try_visit_cell()} differs, and
> is shown in
> -Figure~\ref{fig:SMPdesign:Partitioned Parallel Helper Pseudocode}.
> +Listing~\ref{lst:SMPdesign:Partitioned Parallel Helper Pseudocode}.
> Lines~8-9 check to see if the cells are connected, returning failure
> if not.
> The loop spanning lines~11-18 attempts to mark the new cell visited.
> @@ -500,7 +500,7 @@ please proceed to the next section.
> The presence of algorithmic superlinear speedups suggests simulating
> parallelism via co-routines, for example, manually switching context
> between threads on each pass through the main do-while loop in
> -Figure~\ref{fig:SMPdesign:Partitioned Parallel Solver Pseudocode}.
> +Listing~\ref{lst:SMPdesign:Partitioned Parallel Solver Pseudocode}.
> This context switching is straightforward because the context
> consists only of the variables \co{c} and \co{vi}: Of the numerous
> ways to achieve the effect, this is a good tradeoff between
> diff --git a/datastruct/datastruct.tex b/datastruct/datastruct.tex
> index 8b8dd0a..e6c3f17 100644
> --- a/datastruct/datastruct.tex
> +++ b/datastruct/datastruct.tex
> @@ -140,7 +140,7 @@ offers excellent scalability.
> \subsection{Hash-Table Implementation}
> \label{sec:datastruct:Hash-Table Implementation}
>
> -\begin{figure}[tb]
> +\begin{listing}[tb]
> { \scriptsize
> \begin{verbbox}
> 1 struct ht_elem {
> @@ -162,8 +162,8 @@ offers excellent scalability.
> \centering
> \theverbbox
> \caption{Hash-Table Data Structures}
> -\label{fig:datastruct:Hash-Table Data Structures}
> -\end{figure}
> +\label{lst:datastruct:Hash-Table Data Structures}
> +\end{listing}
>
> \begin{figure}[tb]
> \centering
> @@ -172,22 +172,22 @@ offers excellent scalability.
> \label{fig:datastruct:Hash-Table Data-Structure Diagram}
> \end{figure}
>
> -Figure~\ref{fig:datastruct:Hash-Table Data Structures}
> +Listing~\ref{lst:datastruct:Hash-Table Data Structures}
> (\path{hash_bkt.c})
> shows a set of data structures used in a simple fixed-sized hash
> table using chaining and per-hash-bucket locking, and
> Figure~\ref{fig:datastruct:Hash-Table Data-Structure Diagram}
> diagrams how they fit together.
> The \co{hashtab} structure (lines~11-14 in
> -Figure~\ref{fig:datastruct:Hash-Table Data Structures})
> +Listing~\ref{lst:datastruct:Hash-Table Data Structures})
> contains four \co{ht_bucket} structures (lines~6-9 in
> -Figure~\ref{fig:datastruct:Hash-Table Data Structures}),
> +Listing~\ref{lst:datastruct:Hash-Table Data Structures}),
> with the \co{->ht_nbuckets} field controlling the number of buckets.
> Each such bucket contains a list header \co{->htb_head} and
> a lock \co{->htb_lock}.
> The list headers chain \co{ht_elem} structures
> (lines~1-4 in
> -Figure~\ref{fig:datastruct:Hash-Table Data Structures})
> +Listing~\ref{lst:datastruct:Hash-Table Data Structures})
> through their
> \co{->hte_next} fields, and each \co{ht_elem} structure also caches
> the corresponding element's hash value in the \co{->hte_hash} field.
> @@ -199,7 +199,7 @@ The diagram shown in
> Figure~\ref{fig:datastruct:Hash-Table Data-Structure Diagram}
> has bucket~0 with two elements and bucket~2 with one.
>
> -\begin{figure}[tb]
> +\begin{listing}[tb]
> { \scriptsize
> \begin{verbbox}
> 1 #define HASH2BKT(htp, h) \
> @@ -221,10 +221,10 @@ has bucket~0 with two elements and bucket~2 with one.
> \centering
> \theverbbox
> \caption{Hash-Table Mapping and Locking}
> -\label{fig:datastruct:Hash-Table Mapping and Locking}
> -\end{figure}
> +\label{lst:datastruct:Hash-Table Mapping and Locking}
> +\end{listing}
>
> -Figure~\ref{fig:datastruct:Hash-Table Mapping and Locking}
> +Listing~\ref{lst:datastruct:Hash-Table Mapping and Locking}
> shows mapping and locking functions.
> Lines~1 and~2 show the macro \co{HASH2BKT()}, which maps from a hash value
> to the corresponding \co{ht_bucket} structure.
> @@ -233,7 +233,7 @@ the caller needs to implement it when mapping from key to hash value.
> The remaining two functions acquire and release the \co{->htb_lock}
> corresponding to the specified hash value.
>
> -\begin{figure}[tb]
> +\begin{listing}[tb]
> { \scriptsize
> \begin{verbbox}
> 1 struct ht_elem *
> @@ -262,10 +262,10 @@ corresponding to the specified hash value.
> \centering
> \theverbbox
> \caption{Hash-Table Lookup}
> -\label{fig:datastruct:Hash-Table Lookup}
> -\end{figure}
> +\label{lst:datastruct:Hash-Table Lookup}
> +\end{listing}
>
> -Figure~\ref{fig:datastruct:Hash-Table Lookup}
> +Listing~\ref{lst:datastruct:Hash-Table Lookup}
> shows \co{hashtab_lookup()},
> which returns a pointer to the element with the specified hash and key if it
> exists, or \co{NULL} otherwise.
> @@ -285,7 +285,7 @@ If no element matches, line~20 returns \co{NULL}.
>
> \QuickQuiz{}
> But isn't the double comparison on lines~15-18 in
> - Figure~\ref{fig:datastruct:Hash-Table Lookup} inefficient
> + Listing~\ref{lst:datastruct:Hash-Table Lookup} inefficient
> in the case where the key fits into an unsigned long?
> \QuickQuizAnswer{
> Indeed it is!
> @@ -297,7 +297,7 @@ If no element matches, line~20 returns \co{NULL}.
> for the reader.
> } \QuickQuizEnd
>
> -\begin{figure}[tb]
> +\begin{listing}[tb]
> { \scriptsize
> \begin{verbbox}
> 1 void
> @@ -319,10 +319,10 @@ If no element matches, line~20 returns \co{NULL}.
> \centering
> \theverbbox
> \caption{Hash-Table Modification}
> -\label{fig:datastruct:Hash-Table Modification}
> -\end{figure}
> +\label{lst:datastruct:Hash-Table Modification}
> +\end{listing}
>
> -Figure~\ref{fig:datastruct:Hash-Table Modification}
> +Listing~\ref{lst:datastruct:Hash-Table Modification}
> shows the \co{hashtab_add()} and \co{hashtab_del()} functions
> that add and delete elements from the hash table, respectively.
>
> @@ -337,7 +337,7 @@ ensure that no other thread is accessing
> or modifying this same bucket, for example, by invoking
> \co{hashtab_lock()} beforehand.
>
> -\begin{figure}[tb]
> +\begin{listing}[tb]
> { \scriptsize
> \begin{verbbox}
> 1 struct hashtab *
> @@ -368,10 +368,10 @@ or modifying this same bucket, for example, by invoking
> \centering
> \theverbbox
> \caption{Hash-Table Allocation and Free}
> -\label{fig:datastruct:Hash-Table Allocation and Free}
> -\end{figure}
> +\label{lst:datastruct:Hash-Table Allocation and Free}
> +\end{listing}
>
> -Figure~\ref{fig:datastruct:Hash-Table Allocation and Free}
> +Listing~\ref{lst:datastruct:Hash-Table Allocation and Free}
> shows \co{hashtab_alloc()} and \co{hashtab_free()},
> which do hash-table allocation and freeing, respectively.
> Allocation begins on lines~7-9 with allocation of the underlying memory.
> @@ -546,7 +546,7 @@ section~\cite{McKenney:2013:SDS:2483852.2483867}.
> \subsection{RCU-Protected Hash Table Implementation}
> \label{sec:datastruct:RCU-Protected Hash Table Implementation}
>
> -\begin{figure}[tb]
> +\begin{listing}[tb]
> { \scriptsize
> \begin{verbbox}
> 1 static void hashtab_lock_lookup(struct hashtab *htp,
> @@ -565,24 +565,24 @@ section~\cite{McKenney:2013:SDS:2483852.2483867}.
> \centering
> \theverbbox
> \caption{RCU-Protected Hash-Table Read-Side Concurrency Control}
> -\label{fig:datastruct:RCU-Protected Hash-Table Read-Side Concurrency Control}
> -\end{figure}
> +\label{lst:datastruct:RCU-Protected Hash-Table Read-Side Concurrency Control}
> +\end{listing}
>
> For an RCU-protected hash table with per-bucket locking,
> updaters use locking exactly as described in
> Section~\ref{sec:datastruct:Partitionable Data Structures},
> but readers use RCU.
> The data structures remain as shown in
> -Figure~\ref{fig:datastruct:Hash-Table Data Structures},
> +Listing~\ref{lst:datastruct:Hash-Table Data Structures},
> and the \co{HASH2BKT()}, \co{hashtab_lock()}, and \co{hashtab_unlock()}
> functions remain as shown in
> -Figure~\ref{fig:datastruct:Hash-Table Mapping and Locking}.
> +Listing~\ref{lst:datastruct:Hash-Table Mapping and Locking}.
> However, readers use the lighter-weight concurrency-control embodied
> by \co{hashtab_lock_lookup()} and \co{hashtab_unlock_lookup()}
> shown in
> -Figure~\ref{fig:datastruct:RCU-Protected Hash-Table Read-Side Concurrency Control}.
> +Listing~\ref{lst:datastruct:RCU-Protected Hash-Table Read-Side Concurrency Control}.
>
> -\begin{figure}[tb]
> +\begin{listing}[tb]
> { \scriptsize
> \begin{verbbox}
> 1 struct ht_elem
> @@ -611,14 +611,14 @@ Figure~\ref{fig:datastruct:RCU-Protected Hash-Table Read-Side Concurrency Contro
> \centering
> \theverbbox
> \caption{RCU-Protected Hash-Table Lookup}
> -\label{fig:datastruct:RCU-Protected Hash-Table Lookup}
> -\end{figure}
> +\label{lst:datastruct:RCU-Protected Hash-Table Lookup}
> +\end{listing}
>
> -Figure~\ref{fig:datastruct:RCU-Protected Hash-Table Lookup}
> +Listing~\ref{lst:datastruct:RCU-Protected Hash-Table Lookup}
> shows \co{hashtab_lookup()} for the RCU-protected per-bucket-locked
> hash table.
> This is identical to that in
> -Figure~\ref{fig:datastruct:Hash-Table Lookup}
> +Listing~\ref{lst:datastruct:Hash-Table Lookup}
> except that \co{cds_list_for_each_entry()} is replaced
> by \co{cds_list_for_each_entry_rcu()}.
> Both of these primitives sequence down the hash chain referenced
> @@ -651,7 +651,7 @@ RCU read-side critical section, for example, the caller must invoke
> before freeing the deleted element.
> } \QuickQuizEnd
>
> -\begin{figure}[tb]
> +\begin{listing}[tb]
> { \scriptsize
> \begin{verbbox}
> 1 void
> @@ -673,14 +673,14 @@ RCU read-side critical section, for example, the caller must invoke
> \centering
> \theverbbox
> \caption{RCU-Protected Hash-Table Modification}
> -\label{fig:datastruct:RCU-Protected Hash-Table Modification}
> -\end{figure}
> +\label{lst:datastruct:RCU-Protected Hash-Table Modification}
> +\end{listing}
>
> -Figure~\ref{fig:datastruct:RCU-Protected Hash-Table Modification}
> +Listing~\ref{lst:datastruct:RCU-Protected Hash-Table Modification}
> shows \co{hashtab_add()} and \co{hashtab_del()}, both of which
> are quite similar to their counterparts in the non-RCU hash table
> shown in
> -Figure~\ref{fig:datastruct:Hash-Table Modification}.
> +Listing~\ref{lst:datastruct:Hash-Table Modification}.
> The \co{hashtab_add()} function uses \co{cds_list_add_rcu()} instead
> of \co{cds_list_add()} in order to ensure proper ordering when
> an element is added to the hash table at the same time that it is
> @@ -1014,7 +1014,7 @@ which is the subject of the next section.
> \subsection{Resizable Hash Table Implementation}
> \label{sec:datastruct:Resizable Hash Table Implementation}
>
> -\begin{figure}[tb]
> +\begin{listing}[tb]
> { \scriptsize
> \begin{verbbox}
> 1 struct ht_elem {
> @@ -1052,13 +1052,13 @@ which is the subject of the next section.
> \centering
> \theverbbox
> \caption{Resizable Hash-Table Data Structures}
> -\label{fig:datastruct:Resizable Hash-Table Data Structures}
> -\end{figure}
> +\label{lst:datastruct:Resizable Hash-Table Data Structures}
> +\end{listing}
>
> Resizing is accomplished by the classic approach of inserting a level
> of indirection, in this case, the \co{ht} structure shown on
> lines~12-25 of
> -Figure~\ref{fig:datastruct:Resizable Hash-Table Data Structures}.
> +Listing~\ref{lst:datastruct:Resizable Hash-Table Data Structures}.
> The \co{hashtab} structure shown on lines~27-30 contains only a
> pointer to the current \co{ht} structure along with a spinlock that
> is used to serialize concurrent attempts to resize the hash table.
> @@ -1121,7 +1121,7 @@ Conversely, if the bucket that would be selected from the old table
> has not yet been distributed, then the bucket should be selected from
> the old table.
>
> -\begin{figure}[tb]
> +\begin{listing}[tb]
> { \scriptsize
> \begin{verbbox}
> 1 static struct ht_bucket *
> @@ -1153,11 +1153,11 @@ the old table.
> \centering
> \theverbbox
> \caption{Resizable Hash-Table Bucket Selection}
> -\label{fig:datastruct:Resizable Hash-Table Bucket Selection}
> -\end{figure}
> +\label{lst:datastruct:Resizable Hash-Table Bucket Selection}
> +\end{listing}
>
> Bucket selection is shown in
> -Figure~\ref{fig:datastruct:Resizable Hash-Table Bucket Selection},
> +Listing~\ref{lst:datastruct:Resizable Hash-Table Bucket Selection},
> which shows \co{ht_get_bucket_single()} on lines~1-8 and
> \co{ht_get_bucket()} on lines~10-24.
> The \co{ht_get_bucket_single()} function returns a reference to the bucket
> @@ -1179,7 +1179,7 @@ again storing the hash value through parameter \co{b}.
>
> \QuickQuiz{}
> The code in
> - Figure~\ref{fig:datastruct:Resizable Hash-Table Bucket Selection}
> + Listing~\ref{lst:datastruct:Resizable Hash-Table Bucket Selection}
> computes the hash twice!
> Why this blatant inefficiency?
> \QuickQuizAnswer{
> @@ -1195,7 +1195,7 @@ Finally, line~23 returns a reference to the selected hash bucket.
>
> \QuickQuiz{}
> How does the code in
> - Figure~\ref{fig:datastruct:Resizable Hash-Table Bucket Selection}
> + Listing~\ref{lst:datastruct:Resizable Hash-Table Bucket Selection}
> protect against the resizing process progressing past the
> selected bucket?
> \QuickQuizAnswer{
> @@ -1209,7 +1209,7 @@ This implementation of
> will permit lookups and modifications to run concurrently
> with a resize operation.
>
> -\begin{figure}[tb]
> +\begin{listing}[tb]
> { \scriptsize
> \begin{verbbox}
> 1 void hashtab_lock_mod(struct hashtab *htp_master,
> @@ -1249,18 +1249,18 @@ with a resize operation.
> \centering
> \theverbbox
> \caption{Resizable Hash-Table Update-Side Concurrency Control}
> -\label{fig:datastruct:Resizable Hash-Table Update-Side Concurrency Control}
> -\end{figure}
> +\label{lst:datastruct:Resizable Hash-Table Update-Side Concurrency Control}
> +\end{listing}
>
> Read-side concurrency control is provided by RCU as was shown in
> -Figure~\ref{fig:datastruct:RCU-Protected Hash-Table Read-Side Concurrency Control},
> +Listing~\ref{lst:datastruct:RCU-Protected Hash-Table Read-Side Concurrency Control},
> but the update-side concurrency-control functions
> \co{hashtab_lock_mod()} and \co{hashtab_unlock_mod()}
> must now deal with the possibility of a
> concurrent resize operation as shown in
> -Figure~\ref{fig:datastruct:Resizable Hash-Table Update-Side Concurrency Control}.
> +Listing~\ref{lst:datastruct:Resizable Hash-Table Update-Side Concurrency Control}.
>
> -The \co{hashtab_lock_mod()} spans lines~1-19 in the figure.
> +The \co{hashtab_lock_mod()} spans lines~1-19 in the listing.
> Line~9 enters an RCU read-side critical section to prevent
> the data structures from being freed during the traversal,
> line~10 acquires a reference to the current hash table, and then
> @@ -1285,8 +1285,8 @@ section.
>
> \QuickQuiz{}
> The code in
> - Figures~\ref{fig:datastruct:Resizable Hash-Table Bucket Selection}
> - and~\ref{fig:datastruct:Resizable Hash-Table Update-Side Concurrency Control}
> + Listing~\ref{lst:datastruct:Resizable Hash-Table Bucket Selection}
> + and~\ref{lst:datastruct:Resizable Hash-Table Update-Side Concurrency Control}
> computes the hash and executes the bucket-selection logic twice for
> updates!
> Why this blatant inefficiency?
> @@ -1327,7 +1327,7 @@ RCU read-side critical section.
> critical section to complete.
> } \QuickQuizEnd
>
> -\begin{figure}[tb]
> +\begin{listing}[tb]
> { \scriptsize
> \begin{verbbox}
> 1 struct ht_elem *
> @@ -1387,14 +1387,14 @@ RCU read-side critical section.
> \centering
> \theverbbox
> \caption{Resizable Hash-Table Access Functions}
> -\label{fig:datastruct:Resizable Hash-Table Access Functions}
> -\end{figure}
> +\label{lst:datastruct:Resizable Hash-Table Access Functions}
> +\end{listing}
>
> Now that we have bucket selection and concurrency control in place,
> we are ready to search and update our resizable hash table.
> The \co{hashtab_lookup()}, \co{hashtab_add()}, and \co{hashtab_del()}
> functions shown in
> -Figure~\ref{fig:datastruct:Resizable Hash-Table Access Functions}.
> +Listing~\ref{lst:datastruct:Resizable Hash-Table Access Functions}.
>
> The \co{hashtab_lookup()} function on lines~1-21 of the figure does
> hash lookups.
> @@ -1412,7 +1412,7 @@ failure.
>
> \QuickQuiz{}
> In the \co{hashtab_lookup()} function in
> - Figure~\ref{fig:datastruct:Resizable Hash-Table Access Functions},
> + Listing~\ref{lst:datastruct:Resizable Hash-Table Access Functions},
> the code carefully finds the right bucket in the new hash table
> if the element to be looked up has already been distributed
> by a concurrent resize operation.
> @@ -1452,7 +1452,7 @@ a concurrent resize operation.
>
> \QuickQuiz{}
> The \co{hashtab_del()} function in
> - Figure~\ref{fig:datastruct:Resizable Hash-Table Access Functions}
> + Listing~\ref{lst:datastruct:Resizable Hash-Table Access Functions}
> does not always remove the element from the old hash table.
> Doesn't this mean that readers might access this newly removed
> element after it has been freed?
> @@ -1472,7 +1472,7 @@ a concurrent resize operation.
> \co{hashtab_lookup()} operations.
> } \QuickQuizEnd
>
> -\begin{figure*}[tb]
> +\begin{listing*}[tb]
> { \scriptsize
> \begin{verbbox}
> 1 int hashtab_resize(struct hashtab *htp_master,
> @@ -1530,12 +1530,12 @@ a concurrent resize operation.
> \centering
> \theverbbox
> \caption{Resizable Hash-Table Resizing}
> -\label{fig:datastruct:Resizable Hash-Table Resizing}
> -\end{figure*}
> +\label{lst:datastruct:Resizable Hash-Table Resizing}
> +\end{listing*}
>
> The actual resizing itself is carried out by \co{hashtab_resize}, shown in
> -Figure~\ref{fig:datastruct:Resizable Hash-Table Resizing} on
> -page~\pageref{fig:datastruct:Resizable Hash-Table Resizing}.
> +Listing~\ref{lst:datastruct:Resizable Hash-Table Resizing} on
> +page~\pageref{lst:datastruct:Resizable Hash-Table Resizing}.
> Line~17 conditionally acquires the top-level \co{->ht_lock}, and if
> this acquisition fails, line~18 returns \co{-EBUSY} to indicate that
> a resize is already in progress.
> @@ -1562,14 +1562,14 @@ line~35 acquires that bucket's spinlock, and line~36 updates
>
> \QuickQuiz{}
> In the \co{hashtab_resize()} function in
> - Figure~\ref{fig:datastruct:Resizable Hash-Table Access Functions},
> + Listing~\ref{lst:datastruct:Resizable Hash-Table Access Functions},
> what guarantees that the update to \co{->ht_new} on line~29
> will be seen as happening before the update to \co{->ht_resize_cur}
> on line~36 from the perspective of \co{hashtab_lookup()},
> \co{hashtab_add()}, and \co{hashtab_del()}?
> \QuickQuizAnswer{
> The \co{synchronize_rcu()} on line~30 of
> - Figure~\ref{fig:datastruct:Resizable Hash-Table Access Functions}
> + Listing~\ref{lst:datastruct:Resizable Hash-Table Access Functions}
> ensures that all pre-existing RCU readers have completed between
> the time that we install the new hash-table reference on
> line~29 and the time that we update \co{->ht_resize_cur} on
> @@ -1931,8 +1931,8 @@ This overhead can be eliminated by specializing a hash-table implementation
> to a given key type and hash function.
> Doing so eliminates the \co{->ht_cmp()}, \co{->ht_gethash()}, and
> \co{->ht_getkey()} function pointers in the \co{ht} structure shown in
> -Figure~\ref{fig:datastruct:Resizable Hash-Table Data Structures} on
> -page~\pageref{fig:datastruct:Resizable Hash-Table Data Structures}.
> +Listing~\ref{lst:datastruct:Resizable Hash-Table Data Structures} on
> +page~\pageref{lst:datastruct:Resizable Hash-Table Data Structures}.
> It also eliminates the corresponding calls through these pointers,
> which could allow the compiler to inline the resulting fixed functions,
> eliminating not only the overhead of the call instruction, but the
> @@ -1985,8 +1985,8 @@ days of four-kilobyte address spaces.
> The hash tables discussed in this chapter made almost no attempt to conserve
> memory.
> For example, the \co{->ht_idx} field in the \co{ht} structure in
> -Figure~\ref{fig:datastruct:Resizable Hash-Table Data Structures} on
> -page~\pageref{fig:datastruct:Resizable Hash-Table Data Structures}
> +Listing~\ref{lst:datastruct:Resizable Hash-Table Data Structures} on
> +page~\pageref{lst:datastruct:Resizable Hash-Table Data Structures}
> always has a value of either zero or one, yet takes up a full 32 bits
> of memory.
> It could be eliminated, for example, by stealing a bit from the
> @@ -2069,7 +2069,7 @@ If other CPUs attempted to traverse the hash bucket list containing
> that element, they would incur expensive cache misses, degrading both
> performance and scalability.
>
> -\begin{figure}[tb]
> +\begin{listing}[tb]
> { \scriptsize
> \begin{verbbox}
> 1 struct hash_elem {
> @@ -2081,11 +2081,11 @@ performance and scalability.
> \centering
> \theverbbox
> \caption{Alignment for 64-Byte Cache Lines}
> -\label{fig:datastruct:Alignment for 64-Byte Cache Lines}
> -\end{figure}
> +\label{lst:datastruct:Alignment for 64-Byte Cache Lines}
> +\end{listing}
>
> One way to solve this problem on systems with 64-byte cache line is shown in
> -Figure~\ref{fig:datastruct:Alignment for 64-Byte Cache Lines}.
> +Listing~\ref{lst:datastruct:Alignment for 64-Byte Cache Lines}.
> Here \GCC's \co{aligned} attribute is used to force the \co{->counter}
> and the \co{ht_elem} structure into separate cache lines.
> This would allow CPUs to traverse the hash bucket list at full speed
> diff --git a/debugging/debugging.tex b/debugging/debugging.tex
> index 7a5f71d..a4537b0 100644
> --- a/debugging/debugging.tex
> +++ b/debugging/debugging.tex
> @@ -2094,7 +2094,7 @@ On Linux-based systems, this context switch will be visible in
> Similarly, interrupt-based interference can be detected via the
> \path{/proc/interrupts} file.
>
> -\begin{figure}[tb]
> +\begin{listing}[tb]
> { \scriptsize
> \begin{verbbox}
> 1 #include <sys/time.h>
> @@ -2123,13 +2123,13 @@ Similarly, interrupt-based interference can be detected via the
> \centering
> \theverbbox
> \caption{Using \tco{getrusage()} to Detect Context Switches}
> -\label{fig:count:Using getrusage() to Detect Context Switches}
> -\end{figure}
> +\label{lst:count:Using getrusage() to Detect Context Switches}
> +\end{listing}
>
> Opening and reading files is not the way to low overhead, and it is
> possible to get the count of context switches for a given thread
> by using the \co{getrusage()} system call, as shown in
> -Figure~\ref{fig:count:Using getrusage() to Detect Context Switches}.
> +Listing~\ref{lst:count:Using getrusage() to Detect Context Switches}.
> This same system call can be used to detect minor page faults (\co{ru_minflt})
> and major page faults (\co{ru_majflt}).
>
> @@ -2177,7 +2177,7 @@ the average inter-element distance for the portion of the list accepted
> thus far, then the next element is accepted and the process repeats.
> Otherwise, the remainder of the list is rejected.
>
> -\begin{figure}[tb]
> +\begin{listing}[tb]
> { \scriptsize
> \begin{verbbox}
> 1 divisor=3
> @@ -2238,10 +2238,10 @@ Otherwise, the remainder of the list is rejected.
> \centering
> \theverbbox
> \caption{Statistical Elimination of Interference}
> -\label{fig:count:Statistical Elimination of Interference}
> -\end{figure}
> +\label{lst:count:Statistical Elimination of Interference}
> +\end{listing}
>
> -Figure~\ref{fig:count:Statistical Elimination of Interference}
> +Listing~\ref{lst:count:Statistical Elimination of Interference}
> shows a simple \co{sh}/\co{awk} script implementing this notion.
> Input consists of an x-value followed by an arbitrarily long list of y-values,
> and output consists of one line for each input line, with fields as follows:
> @@ -2277,7 +2277,7 @@ This script takes three optional arguments as follows:
> \end{description}
>
> Lines~1-3 of
> -Figure~\ref{fig:count:Statistical Elimination of Interference}
> +Listing~\ref{lst:count:Statistical Elimination of Interference}
> set the default values for the parameters, and lines~4-21 parse
> any command-line overriding of these parameters.
> The \co{awk} invocation on lines~23 and~24 sets the values of the
> @@ -2339,7 +2339,7 @@ Lines~44-52 then compute and print the statistics for the data set.
>
> Of course, it is possible to create a script similar to
> that in
> - Figure~\ref{fig:count:Statistical Elimination of Interference}
> + Listing~\ref{lst:count:Statistical Elimination of Interference}
> that uses standard deviation rather than absolute difference
> to get a similar effect,
> and this is left as an exercise for the interested reader.
> diff --git a/formal/axiomatic.tex b/formal/axiomatic.tex
> index 903d509..5d79887 100644
> --- a/formal/axiomatic.tex
> +++ b/formal/axiomatic.tex
> @@ -4,7 +4,7 @@
> \label{sec:formal:Axiomatic Approaches}
> \OriginallyPublished{Section}{sec:formal:Axiomatic Approaches}{Axiomatic Approaches}{Linux Weekly News}{PaulEMcKenney2014weakaxiom}
>
> -\begin{figure*}[tb]
> +\begin{listing*}[tb]
> { \scriptsize
> \begin{verbbox}
> 1 PPC IRIW.litmus
> @@ -28,12 +28,12 @@
> \centering
> \theverbbox
> \caption{IRIW Litmus Test}
> -\label{fig:formal:IRIW Litmus Test}
> -\end{figure*}
> +\label{lst:formal:IRIW Litmus Test}
> +\end{listing*}
>
> Although the PPCMEM tool can solve the famous ``independent reads of
> independent writes'' (IRIW) litmus test shown in
> -Figure~\ref{fig:formal:IRIW Litmus Test}, doing so requires no less than
> +Listing~\ref{lst:formal:IRIW Litmus Test}, doing so requires no less than
> fourteen CPU hours and generates no less than ten gigabytes of state space.
> That said, this situation is a great improvement over that before the advent
> of PPCMEM, where solving this problem required perusing volumes of
> @@ -70,9 +70,9 @@ converts litmus tests to theorems that might be proven or disproven
> over this set of axioms.
> The resulting tool, called ``herd'', conveniently takes as input the
> same litmus tests as PPCMEM, including the IRIW litmus test shown in
> -Figure~\ref{fig:formal:IRIW Litmus Test}.
> +Listing~\ref{lst:formal:IRIW Litmus Test}.
>
> -\begin{figure*}[tb]
> +\begin{listing*}[tb]
> { \scriptsize
> \begin{verbbox}
> 1 PPC IRIW5.litmus
> @@ -102,8 +102,8 @@ Figure~\ref{fig:formal:IRIW Litmus Test}.
> \centering
> \theverbbox
> \caption{Expanded IRIW Litmus Test}
> -\label{fig:formal:Expanded IRIW Litmus Test}
> -\end{figure*}
> +\label{lst:formal:Expanded IRIW Litmus Test}
> +\end{listing*}
>
> However, where PPCMEM requires 14 CPU hours to solve IRIW, herd does so
> in 17 milliseconds, which represents a speedup of more than six orders
> @@ -112,7 +112,7 @@ That said, the problem is exponential in nature, so we should expect
> herd to exhibit exponential slowdowns for larger problems.
> And this is exactly what happens, for example, if we add four more writes
> per writing CPU as shown in
> -Figure~\ref{fig:formal:Expanded IRIW Litmus Test},
> +Listing~\ref{lst:formal:Expanded IRIW Litmus Test},
> herd slows down by a factor of more than 50,000, requiring more than
> 15 \emph{minutes} of CPU time.
> Adding threads also results in exponential
> diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
> index 2ae41ae..41b8bf1 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
> - Figure~\ref{fig:analysis:QRCU Unordered Summation} on
> - page~\pageref{fig:analysis:QRCU Unordered Summation}.
> + Listing~\ref{lst:analysis:QRCU Unordered Summation} on
> + page~\pageref{lst:analysis:QRCU Unordered Summation}.
> } \QuickQuizEnd
>
> \QuickQuiz{}
> @@ -1759,7 +1759,7 @@ states, passing without errors.
> \subsubsection{Lessons (Re)Learned}
> \label{sec:formal:Lessons (Re)Learned}
>
> -\begin{figure}[tbp]
> +\begin{listing}[tbp]
> { \scriptsize
> \begin{verbbox}
> static inline void rcu_enter_nohz(void)
> @@ -1780,10 +1780,10 @@ states, passing without errors.
> \centering
> \theverbbox
> \caption{Memory-Barrier Fix Patch}
> -\label{fig:formal:Memory-Barrier Fix Patch}
> -\end{figure}
> +\label{lst:formal:Memory-Barrier Fix Patch}
> +\end{listing}
>
> -\begin{figure}[tbp]
> +\begin{listing}[tbp]
> { \scriptsize
> \begin{verbbox}
> - if ((curr - snap) > 2 || (snap & 0x1) == 0)
> @@ -1793,8 +1793,8 @@ states, passing without errors.
> \centering
> \theverbbox
> \caption{Variable-Name-Typo Fix Patch}
> -\label{fig:formal:Variable-Name-Typo Fix Patch}
> -\end{figure}
> +\label{lst:formal:Variable-Name-Typo Fix Patch}
> +\end{listing}
>
> This effort provided some lessons (re)learned:
>
> @@ -1806,14 +1806,14 @@ This effort provided some lessons (re)learned:
> a misplaced memory barrier in
> \co{rcu_enter_nohz()} and \co{rcu_exit_nohz()},
> as shown by the patch in
> - Figure~\ref{fig:formal:Memory-Barrier Fix Patch}.
> + Listing~\ref{lst:formal:Memory-Barrier Fix Patch}.
> \item {\bf Validate your code early, often, and up to the point
> of destruction.}
> This effort located one subtle bug in
> \co{rcu_try_flip_waitack_needed()}
> that would have been quite difficult to test or debug, as
> shown by the patch in
> - Figure~\ref{fig:formal:Variable-Name-Typo Fix Patch}.
> + Listing~\ref{lst:formal:Variable-Name-Typo Fix Patch}.
> \item {\bf Always verify your verification code.}
> The usual way to do this is to insert a deliberate bug
> and verify that the verification code catches it. Of course,
> @@ -1853,7 +1853,7 @@ Manfred Spraul~\cite{ManfredSpraul2008StateMachineRCU}.
> \subsubsection{State Variables for Simplified Dynticks Interface}
> \label{sec:formal:State Variables for Simplified Dynticks Interface}
>
> -\begin{figure}[tbp]
> +\begin{listing}[tbp]
> { \scriptsize
> \begin{verbbox}
> 1 struct rcu_dynticks {
> @@ -1873,10 +1873,10 @@ Manfred Spraul~\cite{ManfredSpraul2008StateMachineRCU}.
> \centering
> \theverbbox
> \caption{Variables for Simple Dynticks Interface}
> -\label{fig:formal:Variables for Simple Dynticks Interface}
> -\end{figure}
> +\label{lst:formal:Variables for Simple Dynticks Interface}
> +\end{listing}
>
> -Figure~\ref{fig:formal:Variables for Simple Dynticks Interface}
> +Listing~\ref{lst:formal:Variables for Simple Dynticks Interface}
> shows the new per-CPU state variables.
> These variables are grouped into structs to allow multiple independent
> RCU implementations (e.g., \co{rcu} and \co{rcu_bh}) to conveniently
> @@ -1939,7 +1939,7 @@ passed through a quiescent state during that interval.
> \subsubsection{Entering and Leaving Dynticks-Idle Mode}
> \label{sec:formal:Entering and Leaving Dynticks-Idle Mode}
>
> -\begin{figure}[tbp]
> +\begin{listing}[tbp]
> { \scriptsize
> \begin{verbbox}
> 1 void rcu_enter_nohz(void)
> @@ -1974,10 +1974,10 @@ passed through a quiescent state during that interval.
> \centering
> \theverbbox
> \caption{Entering and Exiting Dynticks-Idle Mode}
> -\label{fig:formal:Entering and Exiting Dynticks-Idle Mode}
> -\end{figure}
> +\label{lst:formal:Entering and Exiting Dynticks-Idle Mode}
> +\end{listing}
>
> -Figure~\ref{fig:formal:Entering and Exiting Dynticks-Idle Mode}
> +Listing~\ref{lst:formal:Entering and Exiting Dynticks-Idle Mode}
> shows the \co{rcu_enter_nohz()} and \co{rcu_exit_nohz()},
> which enter and exit dynticks-idle mode, also known as ``nohz'' mode.
> These two functions are invoked from process context.
> @@ -2000,7 +2000,7 @@ the opposite \co{dynticks} polarity.
> \subsubsection{NMIs From Dynticks-Idle Mode}
> \label{sec:formal:NMIs From Dynticks-Idle Mode}
>
> -\begin{figure}[tbp]
> +\begin{listing}[tbp]
> { \scriptsize
> \begin{verbbox}
> 1 void rcu_nmi_enter(void)
> @@ -2031,10 +2031,10 @@ the opposite \co{dynticks} polarity.
> \centering
> \theverbbox
> \caption{NMIs From Dynticks-Idle Mode}
> -\label{fig:formal:NMIs From Dynticks-Idle Mode}
> -\end{figure}
> +\label{lst:formal:NMIs From Dynticks-Idle Mode}
> +\end{listing}
>
> -Figure~\ref{fig:formal:NMIs From Dynticks-Idle Mode}
> +Listing~\ref{lst:formal:NMIs From Dynticks-Idle Mode}
> shows the \co{rcu_nmi_enter()} and \co{rcu_nmi_exit()} functions,
> which inform RCU of NMI entry and exit, respectively, from dynticks-idle
> mode.
> @@ -2052,7 +2052,7 @@ respectively.
> \subsubsection{Interrupts From Dynticks-Idle Mode}
> \label{sec:formal:Interrupts From Dynticks-Idle Mode}
>
> -\begin{figure}[tbp]
> +\begin{listing}[tbp]
> { \scriptsize
> \begin{verbbox}
> 1 void rcu_irq_enter(void)
> @@ -2086,10 +2086,10 @@ respectively.
> \centering
> \theverbbox
> \caption{Interrupts From Dynticks-Idle Mode}
> -\label{fig:formal:Interrupts From Dynticks-Idle Mode}
> -\end{figure}
> +\label{lst:formal:Interrupts From Dynticks-Idle Mode}
> +\end{listing}
>
> -Figure~\ref{fig:formal:Interrupts From Dynticks-Idle Mode}
> +Listing~\ref{lst:formal:Interrupts From Dynticks-Idle Mode}
> shows \co{rcu_irq_enter()} and \co{rcu_irq_exit()}, which
> inform RCU of entry to and exit from, respectively, \IRQ\ context.
> Line~6 of \co{rcu_irq_enter()} increments \co{dynticks_nesting},
> @@ -2117,7 +2117,7 @@ a reschedule API if so.
> \subsubsection{Checking For Dynticks Quiescent States}
> \label{sec:formal:Checking For Dynticks Quiescent States}
>
> -\begin{figure}[tbp]
> +\begin{listing}[tbp]
> { \scriptsize
> \begin{verbbox}
> 1 static int
> @@ -2143,19 +2143,19 @@ a reschedule API if so.
> \centering
> \theverbbox
> \caption{Saving Dyntick Progress Counters}
> -\label{fig:formal:Saving Dyntick Progress Counters}
> -\end{figure}
> +\label{lst:formal:Saving Dyntick Progress Counters}
> +\end{listing}
>
> -Figure~\ref{fig:formal:Saving Dyntick Progress Counters}
> +Listing~\ref{lst:formal:Saving Dyntick Progress Counters}
> shows \co{dyntick_save_progress_counter()}, which takes a snapshot
> of the specified CPU's \co{dynticks} and \co{dynticks_nmi}
> counters.
> Lines~8 and~9 snapshot these two variables to locals, line~10
> executes a memory barrier to pair with the memory barriers in
> the functions in
> -Figures~\ref{fig:formal:Entering and Exiting Dynticks-Idle Mode},
> -\ref{fig:formal:NMIs From Dynticks-Idle Mode}, and
> -\ref{fig:formal:Interrupts From Dynticks-Idle Mode}.
> +Listings~\ref{lst:formal:Entering and Exiting Dynticks-Idle Mode},
> +\ref{lst:formal:NMIs From Dynticks-Idle Mode}, and
> +\ref{lst:formal:Interrupts From Dynticks-Idle Mode}.
> Lines~11 and~12 record the snapshots for later calls to
> \co{rcu_implicit_dynticks_qs()},
> and lines~13 and~14 check to see if the CPU is in dynticks-idle mode with
> @@ -2164,7 +2164,7 @@ have even values), hence in an extended quiescent state.
> If so, lines~15 and~16 count this event, and line~17 returns
> true if the CPU was in a quiescent state.
>
> -\begin{figure}[tbp]
> +\begin{listing}[tbp]
> { \scriptsize
> \begin{verbbox}
> 1 static int
> @@ -2193,10 +2193,10 @@ true if the CPU was in a quiescent state.
> \centering
> \theverbbox
> \caption{Checking Dyntick Progress Counters}
> -\label{fig:formal:Checking Dyntick Progress Counters}
> -\end{figure}
> +\label{lst:formal:Checking Dyntick Progress Counters}
> +\end{listing}
>
> -Figure~\ref{fig:formal:Checking Dyntick Progress Counters}
> +Listing~\ref{lst:formal:Checking Dyntick Progress Counters}
> shows \co{rcu_implicit_dynticks_qs()}, which is called to check
> whether a CPU has entered dyntick-idle mode subsequent to a call
> to \co{dynticks_save_progress_counter()}.
> @@ -2207,9 +2207,9 @@ retrieve the snapshots saved earlier by
> Line~13 then
> executes a memory barrier to pair with the memory barriers in
> the functions in
> -Figures~\ref{fig:formal:Entering and Exiting Dynticks-Idle Mode},
> -\ref{fig:formal:NMIs From Dynticks-Idle Mode}, and
> -\ref{fig:formal:Interrupts From Dynticks-Idle Mode}.
> +Listings~\ref{lst:formal:Entering and Exiting Dynticks-Idle Mode},
> +\ref{lst:formal:NMIs From Dynticks-Idle Mode}, and
> +\ref{lst:formal:Interrupts From Dynticks-Idle Mode}.
> Lines~14-16 then check to see if the CPU is either currently in
> a quiescent state (\co{curr} and \co{curr_nmi} having even values) or
> has passed through a quiescent state since the last call to
> diff --git a/formal/ppcmem.tex b/formal/ppcmem.tex
> index 7dc9675..9e1bfc6 100644
> --- a/formal/ppcmem.tex
> +++ b/formal/ppcmem.tex
> @@ -54,7 +54,7 @@ discusses the implications.
> \subsection{Anatomy of a Litmus Test}
> \label{sec:formal:Anatomy of a Litmus Test}
>
> -\begin{figure}[tbp]
> +\begin{listing}[tbp]
> { \scriptsize
> \begin{verbbox}
> 1 PPC SB+lwsync-RMW-lwsync+isync-simple
> @@ -82,11 +82,11 @@ discusses the implications.
> \centering
> \theverbbox
> \caption{PPCMEM Litmus Test}
> -\label{fig:sec:formal:PPCMEM Litmus Test}
> -\end{figure}
> +\label{lst:sec:formal:PPCMEM Litmus Test}
> +\end{listing}
>
> An example PowerPC litmus test for PPCMEM is shown in
> -Figure~\ref{fig:sec:formal:PPCMEM Litmus Test}.
> +Listing~\ref{lst:sec:formal:PPCMEM Litmus Test}.
> The ARM interface works exactly the same way, but with ARM instructions
> substituted for the Power instructions and with the initial ``PPC''
> replaced by ``ARM''. You can select the ARM interface by clicking on
> @@ -117,7 +117,7 @@ in actual use.
>
> \QuickQuiz{}
> Why does line~8
> - of Figure~\ref{fig:sec:formal:PPCMEM Litmus Test}
> + of Listing~\ref{lst:sec:formal:PPCMEM Litmus Test}
> initialize the registers?
> Why not instead initialize them on lines~4 and~5?
> \QuickQuizAnswer{
> @@ -176,7 +176,7 @@ and line~11 is equivalent to the C statement \co{r3=x}.
>
> \QuickQuiz{}
> But whatever happened to line~17 of
> - Figure~\ref{fig:sec:formal:PPCMEM Litmus Test},
> + Listing~\ref{lst:sec:formal:PPCMEM Litmus Test},
> the one that is the \co{Fail:} label?
> \QuickQuizAnswer{
> The implementation of powerpc version of \co{atomic_add_return()}
> @@ -192,7 +192,7 @@ and line~11 is equivalent to the C statement \co{r3=x}.
> applicable, but I have not seen an example where it fails.
> } \QuickQuizEnd
>
> -\begin{figure}[tbp]
> +\begin{listing}[tbp]
> { \scriptsize
> \begin{verbbox}
> 1 void P0(void)
> @@ -217,12 +217,12 @@ and line~11 is equivalent to the C statement \co{r3=x}.
> \centering
> \theverbbox
> \caption{Meaning of PPCMEM Litmus Test}
> -\label{fig:sec:formal:Meaning of PPCMEM Litmus Test}
> -\end{figure}
> +\label{lst:sec:formal:Meaning of PPCMEM Litmus Test}
> +\end{listing}
>
> Putting all this together, the C-language equivalent to the entire litmus
> test is as shown in
> -Figure~\ref{fig:sec:formal:Meaning of PPCMEM Litmus Test}.
> +Listing~\ref{lst:sec:formal:Meaning of PPCMEM Litmus Test}.
> The key point is that if \co{atomic_add_return()} acts as a full
> memory barrier (as the Linux kernel requires it to),
> then it should be impossible for \co{P0()}'s and \co{P1()}'s \co{r3}
> @@ -242,7 +242,7 @@ Because it is very difficult to be sure that you have checked every
> possible sequence of events, a separate tool is provided for this
> purpose~\cite{PaulEMcKenney2011ppcmem}.
>
> -\begin{figure}[tbp]
> +\begin{listing}[tbp]
> { \scriptsize
> \begin{verbbox}
> ./ppcmem -model lwsync_read_block \
> @@ -264,16 +264,16 @@ Observation SB+lwsync-RMW-lwsync+isync Sometimes 1
> \centering
> \theverbbox
> \caption{PPCMEM Detects an Error}
> -\label{fig:sec:formal:PPCMEM Detects an Error}
> -\end{figure}
> +\label{lst:sec:formal:PPCMEM Detects an Error}
> +\end{listing}
>
> Because the litmus test shown in
> -Figure~\ref{fig:sec:formal:PPCMEM Litmus Test}
> +Listing~\ref{lst:sec:formal:PPCMEM Litmus Test}
> contains read-modify-write instructions, we must add \co{-model}
> arguments to the command line.
> If the litmus test is stored in \co{filename.litmus},
> this will result in the output shown in
> -Figure~\ref{fig:sec:formal:PPCMEM Detects an Error},
> +Listing~\ref{lst:sec:formal:PPCMEM Detects an Error},
> where the \co{...} stands for voluminous making-progress output.
> The list of states includes \co{0:r3=0; 1:r3=0;}, indicating once again
> that the old PowerPC implementation of \co{atomic_add_return()} does
> @@ -281,7 +281,7 @@ not act as a full barrier.
> The ``Sometimes'' on the last line confirms this: the assertion triggers
> for some executions, but not all of the time.
>
> -\begin{figure}[tbp]
> +\begin{listing}[tbp]
> { \scriptsize
> \begin{verbbox}
> ./ppcmem -model lwsync_read_block \
> @@ -302,12 +302,12 @@ Observation SB+lwsync-RMW-lwsync+sync Never 0 5
> \centering
> \theverbbox
> \caption{PPCMEM on Repaired Litmus Test}
> -\label{fig:sec:formal:PPCMEM on Repaired Litmus Test}
> -\end{figure}
> +\label{lst:sec:formal:PPCMEM on Repaired Litmus Test}
> +\end{listing}
>
> The fix to this Linux-kernel bug is to replace P0's \co{isync} with
> \co{sync}, which results in the output shown in
> -Figure~\ref{fig:sec:formal:PPCMEM on Repaired Litmus Test}.
> +Listing~\ref{lst:sec:formal:PPCMEM on Repaired Litmus Test}.
> As you can see, \co{0:r3=0; 1:r3=0;} does not appear in the list of states,
> and the last line calls out ``Never''.
> Therefore, the model predicts that the offending execution sequence
> diff --git a/formal/spinhint.tex b/formal/spinhint.tex
> index 27df639..ff33839 100644
> --- a/formal/spinhint.tex
> +++ b/formal/spinhint.tex
> @@ -58,7 +58,7 @@ more complex uses.
> \subsubsection{Promela Warm-Up: Non-Atomic Increment}
> \label{sec:formal:Promela Warm-Up: Non-Atomic Increment}
>
> -\begin{figure}[tbp]
> +\begin{listing}[tbp]
> { \scriptsize
> \begin{verbbox}
> 1 #define NUMPROCS 2
> @@ -106,10 +106,10 @@ more complex uses.
> \centering
> \theverbbox
> \caption{Promela Code for Non-Atomic Increment}
> -\label{fig:analysis:Promela Code for Non-Atomic Increment}
> -\end{figure}
> +\label{lst:analysis:Promela Code for Non-Atomic Increment}
> +\end{listing}
>
> -Figure~\ref{fig:analysis:Promela Code for Non-Atomic Increment}
> +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
> @@ -165,7 +165,7 @@ cc -DSAFETY -o pan pan.c # Compile the model
> \end{minipage}
> \vspace{5pt}
>
> -\begin{figure*}[tbp]
> +\begin{listing*}[tbp]
> { \scriptsize
> \begin{verbbox}
> pan: assertion violated ((sum<2)||(counter==2)) (at depth 20)
> @@ -193,11 +193,11 @@ hash conflicts: 0 (resolved)
> \centering
> \theverbbox
> \caption{Non-Atomic Increment spin Output}
> -\label{fig:analysis:Non-Atomic Increment spin Output}
> -\end{figure*}
> +\label{lst:analysis:Non-Atomic Increment spin Output}
> +\end{listing*}
>
> This will produce output as shown in
> -Figure~\ref{fig: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
> @@ -220,7 +220,7 @@ spin -t -p increment.spin
> \end{minipage}
> \vspace{5pt}
>
> -\begin{figure*}[htbp]
> +\begin{listing*}[htbp]
> { \scriptsize
> \begin{verbbox}
> Starting :init: with pid 0
> @@ -270,11 +270,11 @@ spin: trail ends after 21 steps
> \centering
> \theverbbox
> \caption{Non-Atomic Increment Error Trail}
> -\label{fig:analysis:Non-Atomic Increment Error Trail}
> -\end{figure*}
> +\label{lst:analysis:Non-Atomic Increment Error Trail}
> +\end{listing*}
>
> This gives the output shown in
> -Figure~\ref{fig:analysis:Non-Atomic Increment Error Trail}.
> +Listing~\ref{lst:analysis: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.
> @@ -283,7 +283,7 @@ The assertion then triggered, after which the global state is displayed.
> \subsubsection{Promela Warm-Up: Atomic Increment}
> \label{sec:formal:Promela Warm-Up: Atomic Increment}
>
> -\begin{figure}[htbp]
> +\begin{listing}[htbp]
> { \scriptsize
> \begin{verbbox}
> 1 proctype incrementer(byte me)
> @@ -301,10 +301,10 @@ The assertion then triggered, after which the global state is displayed.
> \centering
> \theverbbox
> \caption{Promela Code for Atomic Increment}
> -\label{fig:analysis:Promela Code for Atomic Increment}
> -\end{figure}
> +\label{lst:analysis:Promela Code for Atomic Increment}
> +\end{listing}
>
> -\begin{figure}[htbp]
> +\begin{listing}[htbp]
> { \scriptsize
> \begin{verbbox}
> (Spin Version 4.2.5 -- 2 April 2005)
> @@ -334,18 +334,18 @@ unreached in proctype :init:
> \centering
> \theverbbox
> \caption{Atomic Increment spin Output}
> -\label{fig:analysis:Atomic Increment spin Output}
> -\end{figure}
> +\label{lst:analysis: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
> -Figure~\ref{fig:analysis:Promela Code for Atomic Increment}.
> +Listing~\ref{lst:analysis:Promela Code for Atomic Increment}.
> One could also have simply replaced the pair of statements with
> {\tt counter = counter + 1}, because Promela statements are
> atomic.
> Either way, running this modified model gives us an error-free traversal
> of the state space, as shown in
> -Figure~\ref{fig:analysis:Atomic Increment spin Output}.
> +Listing~\ref{lst:analysis:Atomic Increment spin Output}.
>
> \begin{table}
> \footnotesize
> @@ -537,7 +537,7 @@ The following tricks can help you to abuse Promela safely:
> if used too heavily.
> In addition, it requires you to anticipate possible reorderings.
>
> -\begin{figure}[tbp]
> +\begin{listing}[tbp]
> { \scriptsize
> \begin{verbbox}
> 1 i = 0;
> @@ -556,10 +556,10 @@ The following tricks can help you to abuse Promela safely:
> \centering
> \theverbbox
> \caption{Complex Promela Assertion}
> -\label{fig:analysis:Complex Promela Assertion}
> -\end{figure}
> +\label{lst:analysis:Complex Promela Assertion}
> +\end{listing}
>
> -\begin{figure}[tbp]
> +\begin{listing}[tbp]
> { \scriptsize
> \begin{verbbox}
> 1 atomic {
> @@ -580,21 +580,21 @@ The following tricks can help you to abuse Promela safely:
> \centering
> \theverbbox
> \caption{Atomic Block for Complex Promela Assertion}
> -\label{fig:analysis:Atomic Block for Complex Promela Assertion}
> -\end{figure}
> +\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
> in more detail later) is as shown in
> - Figure~\ref{fig:analysis:Complex Promela Assertion}.
> + Listing~\ref{lst:analysis: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
> - Figure~\ref{fig:analysis:Atomic Block for Complex Promela Assertion}.
> + Listing~\ref{lst:analysis:Atomic Block for Complex Promela Assertion}.
>
> \item Promela does not provide functions.
> You must instead use C preprocessor macros.
> @@ -607,7 +607,7 @@ Now we are ready for more complex examples.
> \subsection{Promela Example: Locking}
> \label{sec:formal:Promela Example: Locking}
>
> -\begin{figure}[tbp]
> +\begin{listing}[tbp]
> { \scriptsize
> \begin{verbbox}
> 1 #define spin_lock(mutex) \
> @@ -629,14 +629,14 @@ Now we are ready for more complex examples.
> \centering
> \theverbbox
> \caption{Promela Code for Spinlock}
> -\label{fig:analysis:Promela Code for Spinlock}
> -\end{figure}
> +\label{lst:analysis:Promela Code for Spinlock}
> +\end{listing}
>
> 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
> -Figure~\ref{fig:analysis:Promela Code for Spinlock}.
> +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.
> @@ -665,7 +665,7 @@ used by a few computer systems (such as MIPS and PA-RISC).
> As noted earlier, and as will be seen in a later example,
> weak memory ordering must be explicitly coded.
>
> -\begin{figure}[tb]
> +\begin{listing}[tb]
> { \scriptsize
> \begin{verbbox}
> 1 #include "lock.h"
> @@ -717,11 +717,11 @@ weak memory ordering must be explicitly coded.
> \centering
> \theverbbox
> \caption{Promela Code to Test Spinlocks}
> -\label{fig:analysis:Promela Code to Test Spinlocks}
> -\end{figure}
> +\label{lst:analysis:Promela Code to Test Spinlocks}
> +\end{listing}
>
> These macros are tested by the Promela code shown in
> -Figure~\ref{fig:analysis:Promela Code to Test Spinlocks}.
> +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.
> @@ -743,8 +743,8 @@ lines~32-40 atomically sum the havelock array entries,
> line~41 is the assertion, and line~42 exits the loop.
>
> We can run this model by placing the two code fragments of
> -Figures~\ref{fig:analysis:Promela Code for Spinlock}
> -and~\ref{fig:analysis:Promela Code to Test Spinlocks} into
> +Listings~\ref{lst:analysis:Promela Code for Spinlock}
> +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:
>
> @@ -759,7 +759,7 @@ cc -DSAFETY -o pan pan.c
> \end{minipage}
> \vspace{5pt}
>
> -\begin{figure}[htbp]
> +\begin{listing}[htbp]
> { \scriptsize
> \begin{verbbox}
> (Spin Version 4.2.5 -- 2 April 2005)
> @@ -790,11 +790,11 @@ unreached in proctype :init:
> \centering
> \theverbbox
> \caption{Output for Spinlock Test}
> -\label{fig:analysis:Output for Spinlock Test}
> -\end{figure}
> +\label{lst:analysis:Output for Spinlock Test}
> +\end{listing}
>
> The output will look something like that shown in
> -Figure~\ref{fig:analysis:Output for Spinlock Test}.
> +Listing~\ref{lst:analysis:Output for Spinlock Test}.
> As expected, this run has no assertion failures (``errors: 0'').
>
> \QuickQuiz{}
> @@ -891,7 +891,7 @@ produced~\cite{PaulMcKenney2007QRCUpatch},
> but has not yet been included in the Linux kernel as of
> April 2008.
>
> -\begin{figure}[htbp]
> +\begin{listing}[htbp]
> { \scriptsize
> \begin{verbbox}
> 1 #include "lock.h"
> @@ -908,11 +908,11 @@ April 2008.
> \centering
> \theverbbox
> \caption{QRCU Global Variables}
> -\label{fig:analysis:QRCU Global Variables}
> -\end{figure}
> +\label{lst:analysis:QRCU Global Variables}
> +\end{listing}
>
> Returning to the Promela code for QRCU, the global variables are as shown in
> -Figure~\ref{fig:analysis:QRCU Global Variables}.
> +Listing~\ref{lst:analysis: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
> @@ -934,7 +934,7 @@ indicating the state of the corresponding reader:
>
> Finally, the \co{mutex} variable is used to serialize updaters' slowpaths.
>
> -\begin{figure}[htbp]
> +\begin{listing}[htbp]
> { \scriptsize
> \begin{verbbox}
> 1 proctype qrcu_reader(byte me)
> @@ -962,11 +962,11 @@ Finally, the \co{mutex} variable is used to serialize updaters' slowpaths.
> \centering
> \theverbbox
> \caption{QRCU Reader Process}
> -\label{fig:analysis:QRCU Reader Process}
> -\end{figure}
> +\label{lst:analysis:QRCU Reader Process}
> +\end{listing}
>
> QRCU readers are modeled by the \co{qrcu_reader()} process shown in
> -Figure~\ref{fig:analysis:QRCU Reader Process}.
> +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
> @@ -978,7 +978,7 @@ the {\tt assert()} statement that we shall encounter later.
> Line~19 atomically decrements the same counter that we incremented,
> thereby exiting the RCU read-side critical section.
>
> -\begin{figure}[htbp]
> +\begin{listing}[htbp]
> { \scriptsize
> \begin{verbbox}
> 1 #define sum_unordered \
> @@ -1000,11 +1000,11 @@ thereby exiting the RCU read-side critical section.
> \centering
> \theverbbox
> \caption{QRCU Unordered Summation}
> -\label{fig:analysis:QRCU Unordered Summation}
> -\end{figure}
> +\label{lst:analysis:QRCU Unordered Summation}
> +\end{listing}
>
> The C-preprocessor macro shown in
> -Figure~\ref{fig:analysis:QRCU Unordered Summation}
> +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
> of the pair and sums them.
> @@ -1027,7 +1027,7 @@ to 0 (so that line~14 will fetch the second counter).
> Replace it with {\tt if-fi} and remove the two {\tt break} statements.
> } \QuickQuizEnd
>
> -\begin{figure}[htbp]
> +\begin{listing}[htbp]
> { \scriptsize
> \begin{verbbox}
> 1 proctype qrcu_updater(byte me)
> @@ -1093,12 +1093,12 @@ to 0 (so that line~14 will fetch the second counter).
> \centering
> \theverbbox
> \caption{QRCU Updater Process}
> -\label{fig:analysis:QRCU Updater Process}
> -\end{figure}
> +\label{lst:analysis:QRCU Updater Process}
> +\end{listing}
>
> With the \co{sum_unordered} macro in place, we can now proceed
> to the update-side process shown in
> -Figure~\ref{fig:analysis:QRCU Updater Process}.
> +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}
> @@ -1159,7 +1159,7 @@ this update still be in progress.
> \end{enumerate}
> } \QuickQuizEnd
>
> -\begin{figure}[htbp]
> +\begin{listing}[htbp]
> { \scriptsize
> \begin{verbbox}
> 1 init {
> @@ -1190,11 +1190,11 @@ this update still be in progress.
> \centering
> \theverbbox
> \caption{QRCU Initialization Process}
> -\label{fig:analysis:QRCU Initialization Process}
> -\end{figure}
> +\label{lst:analysis:QRCU Initialization Process}
> +\end{listing}
>
> All that remains is the initialization block shown in
> -Figure~\ref{fig:analysis:QRCU Initialization Process}.
> +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.
> --
> 2.7.4
>
--
To unsubscribe from this list: send the line "unsubscribe perfbook" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at http://vger.kernel.org/majordomo-info.html
