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

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