[PATCH -perfbook 0/5] together/applyrcu: Final touches for recent updates

[PATCH -perfbook 0/5] together/applyrcu: Final touches for recent updates

[Akira Yokosawa]

Hi Paul,

Prompted by your recent updates, I have looked into them and made final
touches for them.

Patch 1/5 is an independent update of rcu-test.dat for Linux v6.17.

Patches 2/5 and 4/5 take care of line-count references by embedding labels
in the .litmus sources.

Patches 3/5 and 5/5 add non-breakable white spaces around one-letter
variables and single digit numbers.

All of them have only summary phrases, but I think they should be good
enough.

        Thanks, Akira
--
Akira Yokosawa (5):
  CodeSamples/formal: Update rcu-test.dat for v6.17
  together/applyrcu: Use \clnref{} and its friends in Section 13.5.9
  together/applyrcu: Use nbsp around one-letter variables in Section 13.5.9
  together/applyrcu: Use \clnref{} and its friends in Section 13.5.10
  together/applyrcu: Use nbsp around one-letter variables in Section 13.5.10

 CodeSamples/formal/data/rcu-test.dat          |  1 +
 ...usync-o+o-xchg-rcusync-o+rl-o-o-rul.litmus | 26 +++----
 .../formal/herd/C-double-check-rcu-2.litmus   | 32 ++++-----
 together/applyrcu.tex                         | 71 +++++++++++--------
 4 files changed, 72 insertions(+), 58 deletions(-)


base-commit: fb44848431946e5a42d42fd5dd8a05d6a2298805
-- 
2.43.0

[PATCH -perfbook 1/5] CodeSamples/formal: Update rcu-test.dat for v6.17

[Akira Yokosawa]

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 CodeSamples/formal/data/rcu-test.dat | 1 +
 1 file changed, 1 insertion(+)

diff --git a/CodeSamples/formal/data/rcu-test.dat b/CodeSamples/formal/data/rcu-test.dat
index d63c1bd7..56355595 100644
--- a/CodeSamples/formal/data/rcu-test.dat
+++ b/CodeSamples/formal/data/rcu-test.dat
@@ -104,3 +104,4 @@ v6.12 22834 12313 35147 35.0
 ""    22107 12620 34727 36.3
 ""    22300 12758 35058 36.4
 v6.16 22370 12983 35353 36.7
+""    22437 13261 35698 37.1
-- 
2.43.0

[PATCH -perfbook 2/5] together/applyrcu: Use \clnref{} and its friends in Section 13.5.9

[Akira Yokosawa]

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 ...usync-o+o-xchg-rcusync-o+rl-o-o-rul.litmus | 26 ++++++++---------
 together/applyrcu.tex                         | 29 ++++++++++++-------
 2 files changed, 32 insertions(+), 23 deletions(-)

diff --git a/CodeSamples/formal/herd/C-MP+o-xchg-rcusync-o+o-xchg-rcusync-o+rl-o-o-rul.litmus b/CodeSamples/formal/herd/C-MP+o-xchg-rcusync-o+o-xchg-rcusync-o+rl-o-o-rul.litmus
index 2f0de350..73859c24 100644
--- a/CodeSamples/formal/herd/C-MP+o-xchg-rcusync-o+o-xchg-rcusync-o+rl-o-o-rul.litmus
+++ b/CodeSamples/formal/herd/C-MP+o-xchg-rcusync-o+o-xchg-rcusync-o+rl-o-o-rul.litmus
@@ -5,7 +5,7 @@ C C-MP+o-xchg-rcusync-o+o-xchg-rcusync-o+rl-o-o-rul
 	int a=1;
 	int b;
 	int c;
-	int *p=a;
+	int *p=a;			//\lnlbl[init:p]
 }
 
 P0(int *a, int *b, int *c, int **p)
@@ -13,9 +13,9 @@ P0(int *a, int *b, int *c, int **p)
 	int *r1;
 
 	*b = 1;
-	r1 = xchg(p, b);
-	synchronize_rcu();
-	*r1 = 0; // Emulate kfree();
+	r1 = xchg(p, b);		//\lnlbl[P0:xchg]
+	synchronize_rcu();		//\lnlbl[P0:sync]
+	*r1 = 0; // Emulate kfree();	//\lnlbl[P0:free]
 }
 
 P1(int *a, int *b, int *c, int **p)
@@ -23,9 +23,9 @@ P1(int *a, int *b, int *c, int **p)
 	int *r1;
 
 	*c = 1;
-	r1 = xchg(p, c);
-	synchronize_rcu();
-	*r1 = 0; // Emulate kfree();
+	r1 = xchg(p, c);		//\lnlbl[P1:xchg]
+	synchronize_rcu();		//\lnlbl[P1:sync]
+	*r1 = 0; // Emulate kfree();	//\lnlbl[P1:free]
 }
 
 P2(int *a, int *b, int *c, int **p)
@@ -33,15 +33,15 @@ P2(int *a, int *b, int *c, int **p)
 	int *r1;
 	int r2;
 
-	rcu_read_lock();
-	r1 = rcu_dereference(*p);
-	r2 = *r1;
-	rcu_read_unlock();
+	rcu_read_lock();		//\lnlbl[P2:lock]
+	r1 = rcu_dereference(*p);	//\lnlbl[P2:load]
+	r2 = *r1;			//\lnlbl[P2:deref]
+	rcu_read_unlock();		//\lnlbl[P2:unlock]
 }
 
 //\end[snippet]
 locations [0:r1; 1:r1; 2:r1; 2:r2; a; b; c; p]
 (* Better not be freed!!! *)
-exists (2:r2=0 \/ a=1 \/
+exists (2:r2=0 \/ a=1 \/			(* \lnlbl[ex:1] *)
 	(* Better be only one in use! *)
-	(b=1 /\ c=1) \/ (b=0 /\ c=0))
+	(b=1 /\ c=1) \/ (b=0 /\ c=0))		(* \lnlbl[ex:2] *)
diff --git a/together/applyrcu.tex b/together/applyrcu.tex
index ff1a276b..48eaa685 100644
--- a/together/applyrcu.tex
+++ b/together/applyrcu.tex
@@ -877,25 +877,30 @@ they use \co{rcu_assign_pointer()}.
 However, if we have concurrent lockless updates, one update's
 \co{rcu_assign_pointer()} can be silently overwritten by the next update,
 resulting in a memory leak.
+\begin{fcvref}[ln:formal:C-MP+o-xchg-rcusync-o+o-xchg-rcusync-o+rl-o-o-rul:whole]
 One way to avoid this is to use an atomic \co{xchg()} instruction,
-as shown on lines~15 and~25 of
+as shown on \clnref{P0:xchg, P1:xchg} of
 \cref{lst:formal:Configuration-Update Example}.
 This way, the pointer from the overwritten \co{xchg()} is returned by
 the next \co{xchg()}, allowing the caller to free it after an RCU
-grace period (lines~16 and 26).
+grace period (\clnref{P0:sync, P1:sync}).
 Because the Linux-kernel memory model does not support dynamic allocation,
 this code emulates freeing by storing the value zero.
+\end{fcvref}
 
 \QuickQuiz{
 	Wait!!!
-	Isn't it necessary for lines~17 and~27 of
+	\begin{fcvref}[ln:formal:C-MP+o-xchg-rcusync-o+o-xchg-rcusync-o+rl-o-o-rul:whole]
+	Isn't it necessary for \clnref{P0:free, P1:free} of
 	\cref{lst:formal:Configuration-Update Example}
-	to check for a \co{NULL} pointer returned from lines~15
-	and~25?
+	to check for a \co{NULL} pointer returned from
+	\clnref{P0:xchg, P1:xchg}?
+	\end{fcvref}
 }\QuickQuizAnswer{
 	In this textbook example, no.
 
-	This is because line~7 initialized pointer \co{p} to point to
+	\begin{fcvref}[ln:formal:C-MP+o-xchg-rcusync-o+o-xchg-rcusync-o+rl-o-o-rul:whole]
+	This is because \clnref{init:p} initialized pointer \co{p} to point to
 	variable \co{a}, so that this pointer will never be \co{NULL}.
 	However, this is a very good question to ask because in most
 	production-quality code, a \co{NULL} check would indeed be
@@ -903,19 +908,23 @@ this code emulates freeing by storing the value zero.
 	On top of that, the first sentence of this section suggested
 	that the pointer might in fact be \co{NULL}.
 	Adding the NULL checks is left as an exercise for the reader.
+	\end{fcvref}
 }\QuickQuizEnd
 
+\begin{fcvref}[ln:formal:C-MP+o-xchg-rcusync-o+o-xchg-rcusync-o+rl-o-o-rul:whole]
 The reader can then be written as a straightforward RCU reader
-(lines~35 and~38), loading the current pointer on line~36 and
-dereferencing it on line~37.
+(\clnrefrange{P2:lock}{P2:unlock}),
+loading the current pointer on \clnref{P2:load} and
+dereferencing it on \clnref{P2:deref}.
 
 Running this example
 (\path{CodeSamples/formal/herd/C-MP+o-xchg-rcusync-o+o-xchg-rcusync-o+rl-o-o-rul.litmus})
 through \co{herd}
 (see \cref{sec:formal:Axiomatic Approaches})
-verifies that this algorithm avoid use-after-free errors (line~43) and that it
+verifies that this algorithm avoid use-after-free errors (\clnref{ex:1}) and that it
 emulates freeing of all but one of the objects \co{a}, \co{b}, and \co{c}
-(line~45), thus also avoiding memory leaks.
+(\clnref{ex:2}), thus also avoiding memory leaks.
+\end{fcvref}
 
 \subsection{Lockless Double-Checked Locking}
 \label{sec:together:Lockless Double-Checked Locking}
-- 
2.43.0

[PATCH -perfbook 3/5] together/applyrcu: Use nbsp around one-letter variables in Section 13.5.9

[Akira Yokosawa]

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 together/applyrcu.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/together/applyrcu.tex b/together/applyrcu.tex
index 48eaa685..ff462a3b 100644
--- a/together/applyrcu.tex
+++ b/together/applyrcu.tex
@@ -900,8 +900,8 @@ this code emulates freeing by storing the value zero.
 	In this textbook example, no.
 
 	\begin{fcvref}[ln:formal:C-MP+o-xchg-rcusync-o+o-xchg-rcusync-o+rl-o-o-rul:whole]
-	This is because \clnref{init:p} initialized pointer \co{p} to point to
-	variable \co{a}, so that this pointer will never be \co{NULL}.
+	This is because \clnref{init:p} initialized pointer~\co{p} to point to
+	variable~\co{a}, so that this pointer will never be \co{NULL}.
 	However, this is a very good question to ask because in most
 	production-quality code, a \co{NULL} check would indeed be
 	necessary.
@@ -922,7 +922,7 @@ Running this example
 through \co{herd}
 (see \cref{sec:formal:Axiomatic Approaches})
 verifies that this algorithm avoid use-after-free errors (\clnref{ex:1}) and that it
-emulates freeing of all but one of the objects \co{a}, \co{b}, and \co{c}
+emulates freeing of all but one of the objects~\co{a}, \co{b}, and~\co{c}
 (\clnref{ex:2}), thus also avoiding memory leaks.
 \end{fcvref}
 
-- 
2.43.0

[PATCH -perfbook 4/5] together/applyrcu: Use \clnref{} and its friends in Section 13.5.10

[Akira Yokosawa]

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 .../formal/herd/C-double-check-rcu-2.litmus   | 32 +++++++++----------
 together/applyrcu.tex                         | 32 +++++++++++--------
 2 files changed, 34 insertions(+), 30 deletions(-)

diff --git a/CodeSamples/formal/herd/C-double-check-rcu-2.litmus b/CodeSamples/formal/herd/C-double-check-rcu-2.litmus
index e23bc081..ff7a1dd3 100644
--- a/CodeSamples/formal/herd/C-double-check-rcu-2.litmus
+++ b/CodeSamples/formal/herd/C-double-check-rcu-2.litmus
@@ -12,24 +12,24 @@ P0(int *a, int *b, int **p)
 	int *r1;
 	int r2;
 
-	rcu_read_lock();
-	r1 = rcu_dereference(*p);
-	if (r1) {
-		r2 = *r1;
-		rcu_read_unlock();
+	rcu_read_lock();		//\lnlbl[P0:lock]
+	r1 = rcu_dereference(*p);	//\lnlbl[P0:load]
+	if (r1) {			//\lnlbl[P0:if]
+		r2 = *r1;		//\lnlbl[P0:deref]
+		rcu_read_unlock();	//\lnlbl[P0:unl:1]
 	} else {
-		rcu_read_unlock();
-		*a = 1;
-		r1 = xchg(p, a);
-		if (r1) {
-			synchronize_rcu();
-			*r1 = 0; // Emulate kfree();
+		rcu_read_unlock();	//\lnlbl[P0:unl:2]
+		*a = 1;			//\lnlbl[P0:init:a]
+		r1 = xchg(p, a);	//\lnlbl[P0:xchg]
+		if (r1) {				//\lnlbl[P0:if:2]
+			synchronize_rcu();		//\lnlbl[P0:sync]
+			*r1 = 0; // Emulate kfree();	//\lnlbl[P0:free]
 		}
 		r2 = 1;
 	}
 }
 
-P1(int *a, int *b, int **p)
+P1(int *a, int *b, int **p)		//\lnlbl[P1:b]
 {
 	int *r1;
 	int r2;
@@ -49,11 +49,11 @@ P1(int *a, int *b, int **p)
 		}
 		r2 = 1;
 	}
-}
+}					//\lnlbl[P1:e]
 
 //\end[snippet]
-locations [0:r1; 1:r1; a; b; p]
+locations [0:r1; 1:r1; a; b; p]		(* \lnlbl[loc] *)
 (* Reader better not see freed element!!! *)
-exists (0:r2=0 \/ 1:r2=0 \/
+exists (0:r2=0 \/ 1:r2=0 \/		(* \lnlbl[ex:1] *)
 	(* Better only be one in use! *)
-	(a=1 /\ b=1) \/ (a=0 /\ b=0))
+	(a=1 /\ b=1) \/ (a=0 /\ b=0))	(* \lnlbl[ex:2] *)
diff --git a/together/applyrcu.tex b/together/applyrcu.tex
index ff462a3b..455bf2a1 100644
--- a/together/applyrcu.tex
+++ b/together/applyrcu.tex
@@ -957,31 +957,35 @@ avoid disrupting concurrent readers, for example, as shown in
 
 The fastpath covers the common case where initialization has already
 completed.
-Line~14 begins an RCU read-side critical section, and line~15 fetches
+\begin{fcvref}[ln:formal:C-double-check-rcu-2:whole:P0]
+\Clnref{lock} begins an RCU read-side critical section, and \clnref{load} fetches
 the current pointer.
-If line~16 determines that this pointer is non-\co{NULL}, then
-initialization is complete, so that line~17 fetches the element's contents
-and line~18 exits the critical section.
+If \clnref{if} determines that this pointer is non-\co{NULL}, then
+initialization is complete, so that \clnref{deref} fetches the element's contents
+and \clnref{unl:1} exits the critical section.
 
-Otherwise, line~16 will see the pre-initialization \co{NULL} pointer
-and transfer control to line~20, which exits the RCU read-side critical
+Otherwise, \clnref{if} will see the pre-initialization \co{NULL} pointer
+and transfer control to \clnref{unl:2}, which exits the RCU read-side critical
 section.
-Line~21 initializes the element (abstracting away any required allocation),
-line~22 atomically exchanges the pointer to this element with the global
+\Clnref{init:a} initializes the element (abstracting away any required allocation),
+\clnref{xchg} atomically exchanges the pointer to this element with the global
 pointer \co{p}, returning the old value in \co{r1}.
-If line~23 determines that \co{r1} was non-\co{NULL}, then line~24
-waits for any readers accessing the old element to finish and line~25
+If \clnref{if:2} determines that \co{r1} was non-\co{NULL}, then \clnref{sync}
+waits for any readers accessing the old element to finish and \clnref{free}
 emulates a \co{kfree()}.
 Either way, \co{r2} is set to the initial value of 1.
+\end{fcvref}
 
-Lines~31-51 operate in the same manner, but using element \co{b} instead
+\begin{fcvref}[ln:formal:C-double-check-rcu-2:whole]
+\Clnrefrange{P1:b}{P1:e} operate in the same manner, but using element \co{b} instead
 of \co{a}.
 
-Line~53 displays all variables to ease debugging of the litmus test.
-Line~55 verifies that both processes obtain an initialized value,
-and line~57 verifies that there are no memory leaks and that at least
+\Clnref{loc} displays all variables to ease debugging of the litmus test.
+\Clnref{ex:1} verifies that both processes obtain an initialized value,
+and \clnref{ex:2} verifies that there are no memory leaks and that at least
 one element remains in use.
 Running \co{herd} confirms that this code satisfies these constraints.
+\end{fcvref}
 
 \QuickQuiz{
 	But wouldn't memory allocation also be forbidden in such
-- 
2.43.0

[PATCH -perfbook 5/5] together/applyrcu: Use nbsp around one-letter variables in Section 13.5.10

[Akira Yokosawa]

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 together/applyrcu.tex | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/together/applyrcu.tex b/together/applyrcu.tex
index 455bf2a1..6004cb24 100644
--- a/together/applyrcu.tex
+++ b/together/applyrcu.tex
@@ -969,16 +969,16 @@ and transfer control to \clnref{unl:2}, which exits the RCU read-side critical
 section.
 \Clnref{init:a} initializes the element (abstracting away any required allocation),
 \clnref{xchg} atomically exchanges the pointer to this element with the global
-pointer \co{p}, returning the old value in \co{r1}.
+pointer~\co{p}, returning the old value in \co{r1}.
 If \clnref{if:2} determines that \co{r1} was non-\co{NULL}, then \clnref{sync}
 waits for any readers accessing the old element to finish and \clnref{free}
 emulates a \co{kfree()}.
-Either way, \co{r2} is set to the initial value of 1.
+Either way, \co{r2} is set to the initial value of~1.
 \end{fcvref}
 
 \begin{fcvref}[ln:formal:C-double-check-rcu-2:whole]
-\Clnrefrange{P1:b}{P1:e} operate in the same manner, but using element \co{b} instead
-of \co{a}.
+\Clnrefrange{P1:b}{P1:e} operate in the same manner, but using element~\co{b} instead
+of~\co{a}.
 
 \Clnref{loc} displays all variables to ease debugging of the litmus test.
 \Clnref{ex:1} verifies that both processes obtain an initialized value,
-- 
2.43.0

Re: [PATCH -perfbook 0/5] together/applyrcu: Final touches for recent updates

[Paul E. McKenney]

On Tue, Oct 07, 2025 at 11:48:34PM +0900, Akira Yokosawa wrote:
> Hi Paul,
> 
> Prompted by your recent updates, I have looked into them and made final
> touches for them.
> 
> Patch 1/5 is an independent update of rcu-test.dat for Linux v6.17.
> 
> Patches 2/5 and 4/5 take care of line-count references by embedding labels
> in the .litmus sources.
> 
> Patches 3/5 and 5/5 add non-breakable white spaces around one-letter
> variables and single digit numbers.
> 
> All of them have only summary phrases, but I think they should be good
> enough.

Agreed!  Queued and pushed, and thank you very much!  Those line-count
changes especially will make any future modifications of those litmus
tests much easier.

							Thanx, Paul

>         Thanks, Akira
> --
> Akira Yokosawa (5):
>   CodeSamples/formal: Update rcu-test.dat for v6.17
>   together/applyrcu: Use \clnref{} and its friends in Section 13.5.9
>   together/applyrcu: Use nbsp around one-letter variables in Section 13.5.9
>   together/applyrcu: Use \clnref{} and its friends in Section 13.5.10
>   together/applyrcu: Use nbsp around one-letter variables in Section 13.5.10
> 
>  CodeSamples/formal/data/rcu-test.dat          |  1 +
>  ...usync-o+o-xchg-rcusync-o+rl-o-o-rul.litmus | 26 +++----
>  .../formal/herd/C-double-check-rcu-2.litmus   | 32 ++++-----
>  together/applyrcu.tex                         | 71 +++++++++++--------
>  4 files changed, 72 insertions(+), 58 deletions(-)
> 
> 
> base-commit: fb44848431946e5a42d42fd5dd8a05d6a2298805
> -- 
> 2.43.0
>