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

Signed-off-by: Akira Yokosawa <[email protected]>
---
 ...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