[PATCH 0/4] Updates and fixes in defer/hazptr and formal/dyntickrcu

[PATCH 0/4] Updates and fixes in defer/hazptr and formal/dyntickrcu

[Akira Yokosawa]

Hi Paul,

Your latest commit 50c5b95d30bc ("defer/hazptr: Add discussion of
hazptr_free_later()") embeds a code snippet in .tex which can be
extracted from hazptr.c.  My guess is it was easier for you to do so
rather than to tame fcvextract.pl to do what you wanted.
There is an option "gobbleblank=yes" to suppress blank/empty lines
from appearing in the resulting snippet. I couldn't help doing
it myself.

Patch #1 does the necessary changes in hazptr.c and embedding of
line labels.
Patch #2 is a trivial typo fix I noticed along the way.

If you encounter any conflict, please skip patch #1.

Patches #3 and #4 are the followup changes to formal/dyntickrcu,
including the addition of Linux kernel version info. Please refer to
the change log of patch #4.

        Thanks, Akira
--
Akira Yokosawa (4):
  defer/hazptr: Extract snippet from hazptr.c
  defer/hazptr: Fix trivial typo
  RCU.bib: Add entry of git commit of Tree RCU
  formal/dyntickrcu: Adjust context and fix typo

 CodeSamples/defer/hazptr.c |  77 +++++++++++++------------
 bib/RCU.bib                |  11 ++++
 defer/hazptr.tex           | 113 ++++++++++++-------------------------
 formal/dyntickrcu.tex      |  31 ++++++----
 4 files changed, 108 insertions(+), 124 deletions(-)

-- 
2.17.1

[PATCH 1/4] defer/hazptr: Extract snippet from hazptr.c

[Akira Yokosawa]

From fc38eb9741c49aa7907d60806158499affe36bfa Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Sun, 21 Apr 2019 15:14:25 +0900
Subject: [PATCH 1/4] defer/hazptr: Extract snippet from hazptr.c

By using "gobbleblank=yes" option of \begin{snippet} meta command,
fcvextract.pl can extract the snippet in a proper form.
Also embed line labels and reference them in the text.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 CodeSamples/defer/hazptr.c |  77 +++++++++++++------------
 defer/hazptr.tex           | 111 ++++++++++++-------------------------
 2 files changed, 76 insertions(+), 112 deletions(-)

diff --git a/CodeSamples/defer/hazptr.c b/CodeSamples/defer/hazptr.c
index ee7b8075..3def441b 100644
--- a/CodeSamples/defer/hazptr.c
+++ b/CodeSamples/defer/hazptr.c
@@ -72,12 +72,13 @@ void hazptr_reinitialize()
  *    0 : a == b
  *  > 0 : a > b
  */
-int compare (const void *a, const void *b)
+//\begin{snippet}[labelbase=ln:defer:hazptr:scan_free,gobbleblank=yes,commandchars=\%\@\$]
+int compare(const void *a, const void *b)
 {
-  return ( *(hazptr_head_t **)a - *(hazptr_head_t **)b );
+	return ( *(hazptr_head_t **)a - *(hazptr_head_t **)b );
 }
-
-void hazptr_scan()
+							//\fcvblank
+void hazptr_scan()				//\lnlbl{scan:b}
 {
 	/* Iteratation variables. */
 	hazptr_head_t *cur;
@@ -89,14 +90,19 @@ void hazptr_scan()
 	/* List of hazard pointers, and its size. */
 	hazptr_head_t **plist = gplist;
 	unsigned long psize;
-
-	if (plist == NULL) {
-		plist = (hazptr_head_t **)malloc(sizeof(hazptr_head_t *) * K * NR_THREADS);
+							//\fcvblank
+	if (plist == NULL) {			//\lnlbl{scan:check}
+		psize = sizeof(hazptr_head_t *) * K * NR_THREADS; //\lnlbl{scan:alloc:b}
+		plist = (hazptr_head_t **)malloc(psize);
+#ifndef FCV_SNIPPET
 		if (plist == NULL) {
 			fprintf(stderr, "hazptr_scan: out of memory\n");
 			exit(EXIT_FAILURE);
 		}
-		gplist = plist;
+#else /* FCV_SNIPPET */
+		BUG_ON(!plist);
+#endif /* FCV_SNIPPET */
+		gplist = plist;			//\lnlbl{scan:alloc:e}
 	}
 
 	/*
@@ -111,52 +117,53 @@ void hazptr_scan()
 	 *   A -> B -> C ---> A -> B      ---> A -> C
 	 *                    B -> POISON      B -> POISON
 	 */
-	smp_mb();
+	smp_mb();				//\lnlbl{scan:mb1}
 
 	/* Stage 1: Scan HP list and insert non-null values in plist. */
 	psize = 0;
-	for (i = 0; i < H; i++) {
+	for (i = 0; i < H; i++) {		//\lnlbl{scan:loop:b}
 		uintptr_t hp = (uintptr_t)READ_ONCE(HP[i].p);
-
+							//\fcvblank
 		if (!hp)
 			continue;
 		plist[psize++] = (hazptr_head_t *)(hp & ~0x1UL);
-	}
-	smp_mb(); /* ensure freeing happens after scan. */
+	}					//\lnlbl{scan:loop:e}
+	smp_mb(); /* ensure freeing happens after scan. */ //\lnlbl{scan:mb2}
 	
 	/* Stage 2: Sort the plist. */
-	qsort(plist, psize, sizeof(hazptr_head_t *), compare);
+	qsort(plist, psize, sizeof(hazptr_head_t *), compare); //\lnlbl{scan:sort}
 
 	/* Stage 3: Free non-harzardous nodes. */
-	tmplist = rlist;
-	rlist = NULL;
-	rcount = 0;
-	while (tmplist != NULL) {
+	tmplist = rlist;			//\lnlbl{scan:rem:b}
+	rlist = NULL;				//\lnlbl{scan:rem:e}
+	rcount = 0;				//\lnlbl{scan:zero}
+	while (tmplist != NULL) {		//\lnlbl{scan:loop2:b}
 		/* Pop cur off top of tmplist. */
-		cur = tmplist;
-		tmplist = tmplist->next;
+		cur = tmplist;			//\lnlbl{scan:rem1st:b}
+		tmplist = tmplist->next;	//\lnlbl{scan:rem1st:e}
 
-		if (bsearch(&cur, plist, psize, sizeof(hazptr_head_t *), compare)) {
-			cur->next = rlist;
+		if (bsearch(&cur, plist, psize,	//\lnlbl{scan:chkhazp:b}
+		            sizeof(hazptr_head_t *), compare)) { //\lnlbl{scan:chkhazp:e}
+			cur->next = rlist;	//\lnlbl{scan:back:b}
 			rlist = cur;
-			rcount++;
+			rcount++;		//\lnlbl{scan:back:e}
 		} else {
-			hazptr_free(cur);
+			hazptr_free(cur);	//\lnlbl{scan:free}
 		}
-	}
-}
-
-void hazptr_free_later(hazptr_head_t *n)
+	}					//\lnlbl{scan:loop2:e}
+}						//\lnlbl{scan:e}
+							//\fcvblank
+void hazptr_free_later(hazptr_head_t *n)	//\lnlbl{free:b}
 {
-	n->next = rlist;
-	rlist = n;
-	rcount++;
+	n->next = rlist;			//\lnlbl{free:enq:b}
+	rlist = n;				//\lnlbl{free:enq:e}
+	rcount++;				//\lnlbl{free:count}
 
-	if (rcount >= R) {
-		hazptr_scan();
+	if (rcount >= R) {			//\lnlbl{free:check}
+		hazptr_scan();			//\lnlbl{free:scan}
 	}
-}
-
+}						//\lnlbl{free:e}
+//\end{snippet}
 #ifdef TEST
 #include "hazptrtorture.h"
 #endif /* #ifdef TEST */
diff --git a/defer/hazptr.tex b/defer/hazptr.tex
index 46592957..84fd15bc 100644
--- a/defer/hazptr.tex
+++ b/defer/hazptr.tex
@@ -116,105 +116,62 @@ the hazard pointer to \co{NULL}.
 \end{lineref}
 
 \begin{listing}[tbp]
-\begin{VerbatimL}
-int compare (const void *a, const void *b)
-{
-	return (*(hazptr_head_t **)a - *(hazptr_head_t **)b);
-}
-
-void hazptr_scan()
-{
-	hazptr_head_t *cur;
-	int i;
-	hazptr_head_t *tmplist;
-	hazptr_head_t **plist = gplist;
-	unsigned long psize;
-
-	if (plist == NULL) {
-		psize = sizeof(hazptr_head_t *) * K * NR_THREADS;
-		plist = malloc(psize);
-		BUG_ON(!plist);
-		gplist = plist;
-	}
-	smp_mb();
-	psize = 0;
-	for (i = 0; i < H; i++) {
-		uintptr_t hp  = (uintptr_t)READ_ONCE(HP[i].p);
-
-		if (!hp)
-			continue;
-		plist[psize++] = (hazptr_head_t *)(hp & ~0x1UL);
-	}
-	smp_mb();
-	qsort(plist, psize, sizeof(hazptr_head_t *), compare);
-	tmplist = rlist;
-	rlist = NULL;
-	rcount = 0;
-	while (tmplist != NULL) {
-		cur = tmplist;
-		tmplist = tmplist->next;
-		if (bsearch(&cur, plist, psize,
-		    sizeof(hazptr_head_t *), compare)) {
-			cur->next = rlist;
-			rlist = cur;
-			rcount++;
-		} else {
-			hazptr_free(cur);
-		}
-	}
-}
-
-void hazptr_free_later(hazptr_head_t *n)
-{
-	n->next = rlist;
-	rlist = n;
-	rcount++;
-	if (rcount >= R) {
-		hazptr_scan();
-	}
-}
-\end{VerbatimL}
+\input{CodeSamples/defer/hazptr@scan_free.fcv}
 \caption{Hazard-Pointer Scanning and Freeing}
 \label{lst:defer:Hazard-Pointer Scanning and Freeing}
 \end{listing}
 
+\begin{lineref}[ln:defer:hazptr:scan_free:free]
 Once a hazard-pointer-protected object has been removed from its
 linked data structure, so that it is now inaccessible to future
 hazard-pointer readers, it is passed to \co{hazptr_free_later()},
-which is shown on lines~48-56 of
+which is shown on lines~\lnref{b}-\lnref{e} of
 Listing~\ref{lst:defer:Hazard-Pointer Scanning and Freeing}
 (\path{hazptr.c}).
-Lines~50 and~51 enqueue the object on a per-thread list \co{rlist}
-and line~52 counts the object in \co{rcount}.
-If line~53 sees that a sufficiently large number of objects are now
-queued, line~54 invokes \co{hazptr_scan()} to attempt to free some of them.
+Lines~\lnref{enq:b} and~\lnref{enq:e}
+enqueue the object on a per-thread list \co{rlist}
+and line~\lnref{count} counts the object in \co{rcount}.
+If line~\lnref{check} sees that a sufficiently large number of objects are now
+queued, line~\lnref{scan} invokes \co{hazptr_scan()} to attempt to
+free some of them.
+\end{lineref}
 
-The \co{hazptr_scan()} function is shown on lines~6--46 of the listing.
+\begin{lineref}[ln:defer:hazptr:scan_free:scan]
+The \co{hazptr_scan()} function is shown on lines~\lnref{b}-\lnref{e}
+of the listing.
 This function relies on a fixed maximum number of threads (\co{NR_THREADS})
 and a fixed maximum number of hazard pointers per thread (\co{K}),
 which allows a fixed-size array of hazard pointers to be used.
 Because any thread might need to scan the hazard pointers, each thread
 maintains its own array, which is referenced by the per-thread variable
 \co{gplist}.
-If line~14 determines that this thread has not yet allocated its
-\co{gplist}, lines~15--18 carry out the allocation.
-The memory barrier on line~20 ensures that all threads see the
-removal of all objects by this thread before lines~22-28 scan
+If line~\lnref{check} determines that this thread has not yet allocated its
+\co{gplist}, lines~\lnref{alloc:b}-\lnref{alloc:e} carry out the allocation.
+The memory barrier on line~\lnref{mb1} ensures that all threads see the
+removal of all objects by this thread before
+lines~\lnref{loop:b}-\lnref{loop:e} scan
 all of the hazard pointers, accumulating non-NULL pointers into
 the \co{plist} array and counting them in \co{psize}.
-The memory barrier on line~30 ensures that the reads of the hazard pointers
+The memory barrier on line~\lnref{mb2} ensures that the reads of
+the hazard pointers
 happen before any objects are freed.
-Line~30 then sorts this array to enable use of binary search below.
+Line~\lnref{sort} then sorts this array to enable use of binary search below.
 
-Lines~31 and 32 remove all elements from this thread's list of
+Lines~\lnref{rem:b} and~\lnref{rem:e}
+remove all elements from this thread's list of
 to-be-freed objects, placing them on the local \co{tmplist}
-and line~33 zeroes the count.
-Each pass through the loop spanning lines~34-45 processes each
+and line~\lnref{zero} zeroes the count.
+Each pass through the loop spanning
+lines~\lnref{loop2:b}-\lnref{loop2:e} processes each
 of the to-be-freed objects.
-Lines~35 and~36 remove the first object from \co{tmplist},
-and if lines~37 and~38 determine that there is a hazard pointer
-protecting this object, lines~39-41 place it back onto \co{rlist}.
-Otherwise, line~43 frees the object.
+Lines~\lnref{rem1st:b} and~\lnref{rem1st:e}
+remove the first object from \co{tmplist},
+and if lines~\lnref{chkhazp:b} and~\lnref{chkhazp:e}
+determine that there is a hazard pointer
+protecting this object, lines~\lnref{back:b}-\lnref{back:e}
+place it back onto \co{rlist}.
+Otherwise, line~\lnref{free} frees the object.
+\end{lineref}
 
 \begin{listing}[tbp]
 \input{CodeSamples/defer/route_hazptr@lookup.fcv}
-- 
2.17.1

[PATCH 2/4] defer/hazptr: Fix trivial typo

[Akira Yokosawa]

From 38be90e94c8ee91c54c6312ece01c9e0a89e2c1c Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Sun, 21 Apr 2019 18:15:51 +0900
Subject: [PATCH 2/4] defer/hazptr: Fix trivial typo

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 defer/hazptr.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/defer/hazptr.tex b/defer/hazptr.tex
index 84fd15bc..4b61d34d 100644
--- a/defer/hazptr.tex
+++ b/defer/hazptr.tex
@@ -80,7 +80,7 @@ If the value of the original pointer has not changed, then the hazard
 pointer protects the pointed-to object, and in that case,
 line~\lnref{htr:success} returns a pointer to that object, which also
 indicates success to the caller.
-Otherwise, if the pointer changed between the to \co{READ_ONCE()}
+Otherwise, if the pointer changed between the two \co{READ_ONCE()}
 invocations, line~\lnref{htr:race2} indicates failure.
 
 \QuickQuiz{}
-- 
2.17.1

[PATCH 3/4] RCU.bib: Add entry of git commit of Tree RCU

[Akira Yokosawa]

From 9bbb1eced9e6c0c44e0582329511a78d86d6b6a7 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Tue, 16 Apr 2019 00:39:17 +0900
Subject: [PATCH 3/4] RCU.bib: Add entry of git commit of Tree RCU

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 bib/RCU.bib | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/bib/RCU.bib b/bib/RCU.bib
index 1617f71b..eb3613cf 100644
--- a/bib/RCU.bib
+++ b/bib/RCU.bib
@@ -1488,6 +1488,17 @@ lot of {Linux} into your technology!!!"
 ,note="\url{http://lwn.net/Articles/305782/}"
 }
 
+@unpublished{PaulEMcKenney2008commit:64db4cfff99c
+,Author="Paul E. McKenney"
+,Title={{"Tree RCU"}: scalable classic {RCU} implementation}
+,month="December"
+,day="18"
+,year="2008"
+,note="Git commit:
+\url{https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/commit/?id=64db4cfff99c}"
+,lastchecked="April 15, 2019"
+}
+
 @unpublished{PaulEMcKenney2009BloatwatchRCU
 ,Author="Paul E. McKenney"
 ,Title="Re: [{PATCH} fyi] {RCU}: the bloatwatch edition"
-- 
2.17.1

[PATCH 4/4] formal/dyntickrcu: Adjust context and fix typo

[Akira Yokosawa]

From 199c8cb24044010e6079899cfb9e8cf97be78eee Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Tue, 16 Apr 2019 00:42:25 +0900
Subject: [PATCH 4/4] formal/dyntickrcu: Adjust context and fix typo

List of changes:
    o Remove redundant reference to Promela and Spin. (We are
      in the middle of that chapter.)
    o Mention compiler flags to reduce memory usage of Spin.
    o Update introduction of section organization.
    o Mention Linux kernel version whose code we are talking
      about.
    o Fix a trivial typo.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 formal/dyntickrcu.tex | 31 ++++++++++++++++++++-----------
 1 file changed, 20 insertions(+), 11 deletions(-)

diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
index 2ba58cd3..4b7a8ade 100644
--- a/formal/dyntickrcu.tex
+++ b/formal/dyntickrcu.tex
@@ -44,7 +44,7 @@ interfaces called from the
 entry/exit functions.
 These \co{rcu_irq_enter()} and \co{rcu_irq_exit()}
 functions are needed to allow RCU to reliably handle situations where
-a dynticks-idle CPUs is momentarily powered up for an interrupt
+a dynticks-idle CPU is momentarily powered up for an interrupt
 handler containing RCU read-side critical sections.
 With these changes in place, Steve's system booted reliably,
 but Paul continued inspecting the code periodically on the assumption
@@ -58,8 +58,7 @@ illusory.
 
 Near the end of February, Paul grew tired of this game.
 He therefore decided to enlist the aid of
-Promela and Spin~\cite{Holzmann03a}, as described in
-Chapter~\ref{chp:Formal Verification}.
+Promela and Spin.
 The following presents a series of seven increasingly realistic
 Promela models, the last of which passes, consuming about
 40\,GB of main memory for the state space.
@@ -74,6 +73,9 @@ More important, Promela and Spin did find a very subtle bug for me!
 	Relax, there are a number of lawful answers to
 	this question:
 	\begin{enumerate}
+	\item	Try compiler flags \co{-DCOLLAPSE} and \co{-DMA=N}
+		to reduce memory consumption.
+		See Section~\ref{sec:formal:Running the QRCU Example}.
 	\item	Further optimize the model, reducing its memory consumption.
 	\item	Work out a pencil-and-paper proof, perhaps starting with the
 		comments in the code in the Linux kernel.
@@ -96,12 +98,11 @@ that has a smaller state space.
 Even better would be an algorithm so simple that its correctness was
 obvious to the casual observer!
 
-Section~\ref{sec:formal:Introduction to Preemptible RCU and dynticks}
-gives an overview of preemptible RCU's dynticks interface,
-Section~\ref{sec:formal:Validating Preemptible RCU and dynticks},
-and
-Section~\ref{sec:formal:Lessons (Re)Learned} lists
-lessons (re)learned during this effort.
+Sections~\ref{sec:formal:Introduction to Preemptible RCU and dynticks}-\ref{sec:formal:Grace-Period Interface}
+give an overview of preemptible RCU's dynticks interface,
+followed by
+Section~\ref{sec:formal:Validating Preemptible RCU and dynticks}'s
+discussion of the validation of the interface.
 
 \subsubsection{Introduction to Preemptible RCU and dynticks}
 \label{sec:formal:Introduction to Preemptible RCU and dynticks}
@@ -126,7 +127,7 @@ determine when a dynticks-idle CPU may safely be ignored.
 The following three sections give an overview of the task
 interface, the interrupt/NMI interface, and the use of
 the \co{dynticks_progress_counter} variable by the
-grace-period machinery.
+grace-period machinery as of Linux kernel v2.6.25-rc4.
 
 \subsubsection{Task Interface}
 \label{sec:formal:Task Interface}
@@ -438,10 +439,16 @@ code.
 \label{sec:formal:Validating Preemptible RCU and dynticks}
 
 This section develops a Promela model for the interface between
-dynticks and RCU step by step, with each of the following sections
+dynticks and RCU step by step, with each of
+Sections~\ref{sec:formal:Basic Model}-\ref{sec:formal:Validating NMI Handlers}
 illustrating one step, starting with the process-level code,
 adding assertions, interrupts, and finally NMIs.
 
+Section~\ref{sec:formal:Lessons (Re)Learned} lists
+lessons (re)learned during this effort, and
+Sections~\ref{sec:formal:Simplicity Avoids Formal Verification}-\ref{sec:formal:Discussion}
+present a simpler solution to RCU's dynticks problem.
+
 \subsubsection{Basic Model}
 \label{sec:formal:Basic Model}
 
@@ -1196,6 +1203,8 @@ for \IRQ s and NMIs, as has been done for
 hierarchical RCU~\cite{PaulEMcKenney2008HierarchicalRCU}
 as indirectly suggested by
 Manfred Spraul~\cite{ManfredSpraul2008StateMachineRCU}.
+This work was pulled into mainline kernel during the v2.6.29
+development cycle~\cite{PaulEMcKenney2008commit:64db4cfff99c}.
 
 \subsubsection{State Variables for Simplified Dynticks Interface}
 \label{sec:formal:State Variables for Simplified Dynticks Interface}
-- 
2.17.1

[Not a patch] Possible incomplete sentence/clause in defer/hazptr

[Akira Yokosawa]

Hi Paul,

The sentence shown below as a diff looks incomplete to me.
What is your intention here?

        Thanks, Akira
--
diff --git a/defer/hazptr.tex b/defer/hazptr.tex
index 4b61d34d..7297e90e 100644
--- a/defer/hazptr.tex
+++ b/defer/hazptr.tex
@@ -240,6 +240,7 @@ element~C, which means that Thread~0's subsequent accesses might have
 resulted in arbitrarily horrible memory corruption, especially if the
 memory for element~C had since been re-allocated for some other purpose.
 Therefore, statically allocated global variables), hazard-pointer
+% @@@ looks incomplete @@@
 readers must typically restart the full traversal in the face of a
 concurrent deletion.

Re: [Not a patch] Possible incomplete sentence/clause in defer/hazptr

[Akira Yokosawa]

On Sun, 21 Apr 2019 11:45:06 -0700, Paul E. McKenney wrote:
> On Mon, Apr 22, 2019 at 12:25:00AM +0900, Akira Yokosawa wrote:
>> Hi Paul,
>>
>> The sentence shown below as a diff looks incomplete to me.
>> What is your intention here?
> 
> Not that!  Thank you for catching this!!!  Please see below for an
> attempted fix.  Thoughts?
> 
> I have queued your four patches.  My problems are (1) force of habit
> and (2) failing to remember that comment-only lines are discarded.

And please remember the option "keepcomment=yes" can change the
behavior.  This reminds me that I need to update style guide.

> I am not all that happy with the #ifdef, but it beats the alternative.
> But what I did in this case was to just remove the fprintf() in favor
> of the BUG_ON().  ;-)

Yes, that sounds reasonable.

> 
> 							Thanx, Paul
> 
> ------------------------------------------------------------------------
> 
> commit 72e774fda87eaead9637d887426b701ec229664d
> Author: Paul E. McKenney <paulmck@linux.ibm.com>
> Date:   Sun Apr 21 11:33:49 2019 -0700
> 
>     defer/hazptr: Fix broken statement of restart location constraints
>     
>     Reported-by: Akira Yokosawa <akiyks@gmail.com>
>     Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
> 
> diff --git a/defer/hazptr.tex b/defer/hazptr.tex
> index 4b61d34d334c..b491c590ae2d 100644
> --- a/defer/hazptr.tex
> +++ b/defer/hazptr.tex
> @@ -239,9 +239,12 @@ Which is a very good thing, because B's successor is the now-freed
>  element~C, which means that Thread~0's subsequent accesses might have
>  resulted in arbitrarily horrible memory corruption, especially if the
>  memory for element~C had since been re-allocated for some other purpose.
> -Therefore, statically allocated global variables), hazard-pointer
> -readers must typically restart the full traversal in the face of a
> -concurrent deletion.
> +Therefore, hazard-pointer readers must typically restart the full
> +traversal in the face of a concurrent deletion.
> +Often the restart must go back to some global (and thus immortal) pointer,
> +but it is sometimes possible to restart at some intermediate location
> +if that location is guaranteed to still be live, for example, due to
> +the current thread holding a lock, a reference count, etc.

Looks good to me!

        Thanks, Akira

>  
>  \QuickQuiz{}
>  	Readers must ``typically'' restart?
> 

Re: [Not a patch] Possible incomplete sentence/clause in defer/hazptr

[Paul E. McKenney]

On Mon, Apr 22, 2019 at 07:19:36AM +0900, Akira Yokosawa wrote:
> On Sun, 21 Apr 2019 11:45:06 -0700, Paul E. McKenney wrote:
> > On Mon, Apr 22, 2019 at 12:25:00AM +0900, Akira Yokosawa wrote:
> >> Hi Paul,
> >>
> >> The sentence shown below as a diff looks incomplete to me.
> >> What is your intention here?
> > 
> > Not that!  Thank you for catching this!!!  Please see below for an
> > attempted fix.  Thoughts?
> > 
> > I have queued your four patches.  My problems are (1) force of habit
> > and (2) failing to remember that comment-only lines are discarded.
> 
> And please remember the option "keepcomment=yes" can change the
> behavior.  This reminds me that I need to update style guide.

Ah, good point!  And please do!

> > I am not all that happy with the #ifdef, but it beats the alternative.
> > But what I did in this case was to just remove the fprintf() in favor
> > of the BUG_ON().  ;-)
> 
> Yes, that sounds reasonable.

Very good, I have pushed these changes.

							Thanx, Paul

> > ------------------------------------------------------------------------
> > 
> > commit 72e774fda87eaead9637d887426b701ec229664d
> > Author: Paul E. McKenney <paulmck@linux.ibm.com>
> > Date:   Sun Apr 21 11:33:49 2019 -0700
> > 
> >     defer/hazptr: Fix broken statement of restart location constraints
> >     
> >     Reported-by: Akira Yokosawa <akiyks@gmail.com>
> >     Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
> > 
> > diff --git a/defer/hazptr.tex b/defer/hazptr.tex
> > index 4b61d34d334c..b491c590ae2d 100644
> > --- a/defer/hazptr.tex
> > +++ b/defer/hazptr.tex
> > @@ -239,9 +239,12 @@ Which is a very good thing, because B's successor is the now-freed
> >  element~C, which means that Thread~0's subsequent accesses might have
> >  resulted in arbitrarily horrible memory corruption, especially if the
> >  memory for element~C had since been re-allocated for some other purpose.
> > -Therefore, statically allocated global variables), hazard-pointer
> > -readers must typically restart the full traversal in the face of a
> > -concurrent deletion.
> > +Therefore, hazard-pointer readers must typically restart the full
> > +traversal in the face of a concurrent deletion.
> > +Often the restart must go back to some global (and thus immortal) pointer,
> > +but it is sometimes possible to restart at some intermediate location
> > +if that location is guaranteed to still be live, for example, due to
> > +the current thread holding a lock, a reference count, etc.
> 
> Looks good to me!
> 
>         Thanks, Akira
> 
> >  
> >  \QuickQuiz{}
> >  	Readers must ``typically'' restart?
> > 
>