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
