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
