* [PATCH 1/4] defer/hazptr: Extract snippet from hazptr.c
2019-04-21 10:03 [PATCH 0/4] Updates and fixes in defer/hazptr and formal/dyntickrcu Akira Yokosawa
@ 2019-04-21 10:06 ` Akira Yokosawa
2019-04-21 10:07 ` [PATCH 2/4] defer/hazptr: Fix trivial typo Akira Yokosawa
` (3 subsequent siblings)
4 siblings, 0 replies; 8+ messages in thread
From: Akira Yokosawa @ 2019-04-21 10:06 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, 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
^ permalink raw reply related [flat|nested] 8+ messages in thread* [PATCH 2/4] defer/hazptr: Fix trivial typo
2019-04-21 10:03 [PATCH 0/4] Updates and fixes in defer/hazptr and formal/dyntickrcu Akira Yokosawa
2019-04-21 10:06 ` [PATCH 1/4] defer/hazptr: Extract snippet from hazptr.c Akira Yokosawa
@ 2019-04-21 10:07 ` Akira Yokosawa
2019-04-21 10:09 ` [PATCH 3/4] RCU.bib: Add entry of git commit of Tree RCU Akira Yokosawa
` (2 subsequent siblings)
4 siblings, 0 replies; 8+ messages in thread
From: Akira Yokosawa @ 2019-04-21 10:07 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, 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
^ permalink raw reply related [flat|nested] 8+ messages in thread* [PATCH 3/4] RCU.bib: Add entry of git commit of Tree RCU
2019-04-21 10:03 [PATCH 0/4] Updates and fixes in defer/hazptr and formal/dyntickrcu Akira Yokosawa
2019-04-21 10:06 ` [PATCH 1/4] defer/hazptr: Extract snippet from hazptr.c Akira Yokosawa
2019-04-21 10:07 ` [PATCH 2/4] defer/hazptr: Fix trivial typo Akira Yokosawa
@ 2019-04-21 10:09 ` Akira Yokosawa
2019-04-21 10:10 ` [PATCH 4/4] formal/dyntickrcu: Adjust context and fix typo Akira Yokosawa
2019-04-21 15:25 ` [Not a patch] Possible incomplete sentence/clause in defer/hazptr Akira Yokosawa
4 siblings, 0 replies; 8+ messages in thread
From: Akira Yokosawa @ 2019-04-21 10:09 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, 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
^ permalink raw reply related [flat|nested] 8+ messages in thread* [PATCH 4/4] formal/dyntickrcu: Adjust context and fix typo
2019-04-21 10:03 [PATCH 0/4] Updates and fixes in defer/hazptr and formal/dyntickrcu Akira Yokosawa
` (2 preceding siblings ...)
2019-04-21 10:09 ` [PATCH 3/4] RCU.bib: Add entry of git commit of Tree RCU Akira Yokosawa
@ 2019-04-21 10:10 ` Akira Yokosawa
2019-04-21 15:25 ` [Not a patch] Possible incomplete sentence/clause in defer/hazptr Akira Yokosawa
4 siblings, 0 replies; 8+ messages in thread
From: Akira Yokosawa @ 2019-04-21 10:10 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, 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
^ permalink raw reply related [flat|nested] 8+ messages in thread* [Not a patch] Possible incomplete sentence/clause in defer/hazptr
2019-04-21 10:03 [PATCH 0/4] Updates and fixes in defer/hazptr and formal/dyntickrcu Akira Yokosawa
` (3 preceding siblings ...)
2019-04-21 10:10 ` [PATCH 4/4] formal/dyntickrcu: Adjust context and fix typo Akira Yokosawa
@ 2019-04-21 15:25 ` Akira Yokosawa
[not found] ` <20190421184506.GD24840@linux.ibm.com>
4 siblings, 1 reply; 8+ messages in thread
From: Akira Yokosawa @ 2019-04-21 15:25 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, 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.
^ permalink raw reply related [flat|nested] 8+ messages in thread