[PATCH 0/6] ppcmem: Apply new scheme of code snippets

[PATCH 0/6] ppcmem: Apply new scheme of code snippets

[Akira Yokosawa]

Subject: [PATCH 0/6] ppcmem: Apply new scheme of code snippets

Hi Paul,

This patch series mostly consists of code snippet updates in
formal/ppcmem.tex.

Patch #1 fixes a trivial typo in dyntickrcu.
Patch #2 is the main changes in this series. It also employs
"cleveref" way of cross references.

Patches #3--#6 touches the text and add a couples of references
to PowerPC atomic updates in the Linux kernel.

Patch #3 adds entries in bib/swtools
Patch #4 adds citation of Git commit in 2013
Patches #5 and #6 add a Quick Quiz on another missing full memory
barrier in the beginning. I'm not that sure the added Quick Quiz
makes sense, though. If it doesn't, please skip #5 and #6.

I remember asking you about the difference of the code emitted by
an atomic built-in of PowerPC-GCC and the code in Linux kernel [1].
IIUC, the added references and Quick Quiz are related to the
question.

[1]: https://www.spinics.net/lists/perfbook/msg02077.html

Seeing the history of the changes and your answer to [1], I suspect
that now that PPC_ATOMIC_ENTRY_BARRIER is "sync", "isync" might be
sufficient for PPC_ATOMIC_EXIT_BARRIER. Obviously I'm not an expert
of PowerPC and can be missing something, but I couldn't help
mentioning.

        Thanks, Akira
--
Akira Yokosawa (6):
  dyntickrcu: Fix trivial typo
  ppcmem: Apply new scheme of code snippets
  bib/swtools: Add refereneces to PowerPC atomic RMW fixes
  ppcmem: Cite Git commit of PowerPC atomic_xxx_return fix
  ppcmem: Add Quick Quiz on lwsync in Listing 12.23
  ppcmem: Move final sentence of Answer to QQZ 12.27 to the next

 bib/swtools.bib       |  33 +++++++
 formal/dyntickrcu.tex |   2 +-
 formal/ppcmem.tex     | 210 +++++++++++++++++++++++-------------------
 3 files changed, 149 insertions(+), 96 deletions(-)

-- 
2.17.1

[PATCH 1/6] dyntickrcu: Fix trivial typo

[Akira Yokosawa]

From 6030baea7bd1226024265db45efd771dacf430d3 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Sun, 21 Jul 2019 17:05:21 +0900
Subject: [PATCH 1/6] dyntickrcu: Fix trivial typo

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 formal/dyntickrcu.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
index 4b7a8ade..a7dd2d74 100644
--- a/formal/dyntickrcu.tex
+++ b/formal/dyntickrcu.tex
@@ -1189,7 +1189,7 @@ This effort provided some lessons (re)learned:
 	a need to re-think your design.}
 \end{enumerate}
 
-To this last point, it turn out that there is a much simpler solution to
+To this last point, it turns out that there is a much simpler solution to
 the dynticks problem, which is presented in the next section.
 
 \subsubsection{Simplicity Avoids Formal Verification}
-- 
2.17.1

[PATCH 2/6] ppcmem: Apply new scheme of code snippets

[Akira Yokosawa]

From 1648cb79f31d86f1dc284fc41937cf60cfd2adf4 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Fri, 27 Sep 2019 21:38:19 +0900
Subject: [PATCH 2/6] ppcmem: Apply new scheme of code snippets

Also employ "cleveref" way of cross-reference.

Note: While putting two labels on a line as is done in the "PPC"
flavor litmus test is not covered by fcvextract.pl at the moment,
it works in this case where the contents of the snippet is
directly coded in the listing environment.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 formal/ppcmem.tex | 189 +++++++++++++++++++++++-----------------------
 1 file changed, 95 insertions(+), 94 deletions(-)

diff --git a/formal/ppcmem.tex b/formal/ppcmem.tex
index c72a7a08..a5cb90e3 100644
--- a/formal/ppcmem.tex
+++ b/formal/ppcmem.tex
@@ -14,7 +14,7 @@ understand memory models used by production systems, greatly simplifying the
 verification of weakly ordered code.
 
 For example,
-Section~\ref{sec:formal:Promela Example: QRCU}
+\cref{sec:formal:Promela Example: QRCU}
 showed how to convince Promela to account for weak memory ordering.
 Although this approach can work well, it requires that the developer
 fully understand the system's memory model.
@@ -45,62 +45,63 @@ produced the PPCMEM tool based on the Power and ARM formalizations.
 
 The PPCMEM tool takes \emph{litmus tests} as input.
 A sample litmus test is presented in
-Section~\ref{sec:formal:Anatomy of a Litmus Test}.
-Section~\ref{sec:formal:What Does This Litmus Test Mean?}
+\cref{sec:formal:Anatomy of a Litmus Test}.
+\Cref{sec:formal:What Does This Litmus Test Mean?}
 relates this litmus test to the equivalent C-language program,
-Section~\ref{sec:formal:Running a Litmus Test} describes how to
+\cref{sec:formal:Running a Litmus Test} describes how to
 apply PPCMEM to this litmus test, and
-Section~\ref{sec:formal:PPCMEM Discussion}
+\cref{sec:formal:PPCMEM Discussion}
 discusses the implications.
 
 \subsection{Anatomy of a Litmus Test}
 \label{sec:formal:Anatomy of a Litmus Test}
 
 \begin{listing}[tbp]
-{ \scriptsize
-\begin{verbbox}
- 1 PPC SB+lwsync-RMW-lwsync+isync-simple
- 2 ""
- 3 {
- 4 0:r2=x; 0:r3=2; 0:r4=y; 0:r10=0; 0:r11=0; 0:r12=z;
- 5 1:r2=y; 1:r4=x;
- 6 }
- 7  P0                 | P1           ;
- 8  li r1,1            | li r1,1      ;
- 9  stw r1,0(r2)       | stw r1,0(r2) ;
-10  lwsync             | sync         ;
-11                     | lwz r3,0(r4) ;
-12  lwarx  r11,r10,r12 | ;
-13  stwcx. r11,r10,r12 | ;
-14  bne Fail1          | ;
-15  isync              | ;
-16  lwz r3,0(r4)       | ;
-17  Fail1:             | ;
-18 
-19 exists
-20 (0:r3=0 /\ 1:r3=0)
-\end{verbbox}
-}
-\centering
-\theverbbox
+\begin{linelabel}[ln:formal:PPCMEM Litmus Test]
+\begin{VerbatimL}[commandchars=\@\[\]]
+PPC SB+lwsync-RMW-lwsync+isync-simple		@lnlbl[type]
+""						@lnlbl[altname]
+{						@lnlbl[init:b]
+0:r2=x; 0:r3=2; 0:r4=y; 0:r10=0; 0:r11=0; 0:r12=z; @lnlbl[init:0]
+1:r2=y; 1:r4=x;					@lnlbl[init:1]
+}						@lnlbl[init:e]
+ P0                 | P1           ;		@lnlbl[procid]
+ li r1,1            | li r1,1      ;		@lnlbl[reginit]
+ stw r1,0(r2)       | stw r1,0(r2) ;		@lnlbl[stw]
+ lwsync             | sync         ; @lnlbl[P0lwsync] @lnlbl[P1sync]
+                    | lwz r3,0(r4) ; @lnlbl[P0empty]  @lnlbl[P1lwz]
+ lwarx  r11,r10,r12 | ;		@lnlbl[P0lwarx] @lnlbl[P1empty:b]
+ stwcx. r11,r10,r12 | ;		@lnlbl[P0stwcx]
+ bne Fail1          | ;		@lnlbl[P0bne]
+ isync              | ;		@lnlbl[P0isync]
+ lwz r3,0(r4)       | ;		@lnlbl[P0lwz]
+ Fail1:             | ;		@lnlbl[P0fail1] @lnlbl[P1empty:e]
+
+exists						@lnlbl[assert:b]
+(0:r3=0 /\ 1:r3=0)				@lnlbl[assert:e]
+\end{VerbatimL}
+\end{linelabel}
 \caption{PPCMEM Litmus Test}
 \label{lst:formal:PPCMEM Litmus Test}
 \end{listing}
 
 An example PowerPC litmus test for PPCMEM is shown in
-Listing~\ref{lst:formal:PPCMEM Litmus Test}.
+\cref{lst:formal:PPCMEM Litmus Test}.
 The ARM interface works exactly the same way, but with ARM instructions
 substituted for the Power instructions and with the initial ``PPC''
 replaced by ``ARM''. You can select the ARM interface by clicking on
 ``Change to ARM Model'' at the web page called out above.
 
-In the example, line~1 identifies the type of system (``ARM'' or ``PPC'')
-and contains the title for the model. Line~2 provides a place for an
+\begin{lineref}[ln:formal:PPCMEM Litmus Test]
+In the example, \clnref{type} identifies the type of system (``ARM'' or
+``PPC'') and contains the title for the model. \Clnref{altname}
+provides a place for an
 alternative name for the test, which you will usually want to leave
 blank as shown in the above example. Comments can be inserted between
-lines~2 and~3 using the OCaml (or Pascal) syntax of \nbco{(* *)}.
+\clnref{altname,init:b} using the OCaml (or Pascal) syntax of \nbco{(* *)}.
 
-Lines~3-6 give initial values for all registers; each is of the form
+\Clnrefrange{init:b}{init:e} give initial values for all registers;
+each is of the form
 \co{P:R=V}, where \co{P} is the process identifier, \co{R} is the register
 identifier, and \co{V} is the value. For example, process 0's register
 r3 initially contains the value 2. If the value is a variable (\co{x},
@@ -110,18 +111,21 @@ of variables, for example, \co{x=1} initializes the value of \co{x} to
 1. Uninitialized variables default to the value zero, so that in the
 example, \co{x}, \co{y}, and \co{z} are all initially zero.
 
-Line~7 provides identifiers for the two processes, so that the \co{0:r3=2}
-on line~4 could instead have been written \co{P0:r3=2}. Line~7 is
+\Clnref{procid} provides identifiers for the two processes, so that
+the \co{0:r3=2} on \clnref{init:0} could instead have been written
+\co{P0:r3=2}. \Clnref{procid} is
 required, and the identifiers must be of the form \co{Pn}, where \co{n}
 is the column number, starting from zero for the left-most column. This
 may seem unnecessarily strict, but it does prevent considerable confusion
 in actual use.
+\end{lineref}
 
 \QuickQuiz{}
-	Why does line~8
-	of Listing~\ref{lst:formal:PPCMEM Litmus Test}
+	\begin{lineref}[ln:formal:PPCMEM Litmus Test]
+	Why does \clnref{reginit} of \cref{lst:formal:PPCMEM Litmus Test}
 	initialize the registers?
-	Why not instead initialize them on lines~4 and~5?
+	Why not instead initialize them on \clnref{init:0,init:1}?
+	\end{lineref}
 \QuickQuizAnswer{
 	Either way works.
 	However, in general, it is better to use initialization than
@@ -134,15 +138,18 @@ in actual use.
 	initialization instructions.
 } \QuickQuizEnd
 
-Lines~8-17 are the lines of code for each process. A given process
-can have empty lines, as is the case for P0's line~11 and P1's
-lines~12-17.
+\begin{lineref}[ln:formal:PPCMEM Litmus Test]
+\Clnrefrange{reginit}{P0fail1} are the lines of code for each process.
+A given process can have empty lines, as is the case for P0's
+\clnref{P0empty} and P1's \clnrefrange{P1empty:b}{P1empty:e}.
 Labels and branches are permitted, as demonstrated by the branch
-on line~14 to the label on line~17. That said, too-free use of branches
+on \clnref{P0bne} to the label on \clnref{P0fail1}.
+That said, too-free use of branches
 will expand the state space. Use of loops is a particularly good way to
 explode your state space.
 
-Lines~19-20 show the assertion, which in this case indicates that we
+\Clnrefrange{assert:b}{assert:e} show the assertion, which in this case
+indicates that we
 are interested in whether P0's and P1's r3 registers can both contain
 zero after both threads complete execution. This assertion is important
 because there are a number of use cases that would fail miserably if
@@ -160,26 +167,32 @@ your Power or ARM memory-ordering question.
 \subsection{What Does This Litmus Test Mean?}
 \label{sec:formal:What Does This Litmus Test Mean?}
 
-P0's lines~8 and~9 are equivalent to the C statement \co{x=1} because
-line~4 defines P0's register \co{r2} to be the address of \co{x}. P0's
-lines~12 and~13 are the mnemonics for load-linked (``load register
+P0's \clnref{reginit,stw} are equivalent to the C statement \co{x=1}
+because \clnref{init:0} defines P0's register \co{r2} to be the address
+of \co{x}. P0's \clnref{P0lwarx,P0stwcx} are the mnemonics for
+load-linked (``load register
 exclusive'' in ARM parlance and ``load reserve'' in Power parlance)
 and store-conditional (``store register exclusive'' in ARM parlance),
 respectively. When these are used together, they form an atomic
 instruction sequence, roughly similar to the compare-and-swap sequences
 exemplified by the x86 \co{lock;cmpxchg} instruction. Moving to a higher
-level of abstraction, the sequence from lines~10-15 is equivalent to
-the Linux kernel's \co{atomic_add_return(&z, 0)}. Finally, line~16 is
+level of abstraction, the sequence from \clnrefrange{P0lwsync}{P0isync}
+is equivalent to the Linux kernel's \co{atomic_add_return(&z, 0)}.
+Finally, \clnref{P0lwz} is
 roughly equivalent to the C statement \co{r3=y}.
 
-P1's lines~8 and~9 are equivalent to the C statement \co{y=1}, line~10
+P1's \clnref{reginit,stw} are equivalent to the C statement \co{y=1},
+\clnref{P1sync}
 is a memory barrier, equivalent to the Linux kernel statement \co{smp_mb()},
-and line~11 is equivalent to the C statement \co{r3=x}.
+and \clnref{P1lwz} is equivalent to the C statement \co{r3=x}.
+\end{lineref}
 
 \QuickQuiz{}
-	But whatever happened to line~17 of
-	Listing~\ref{lst:formal:PPCMEM Litmus Test},
-	the one that is the \co{Fail:} label?
+	\begin{lineref}[ln:formal:PPCMEM Litmus Test]
+	But whatever happened to \clnref{P0fail1} of
+	\cref{lst:formal:PPCMEM Litmus Test},
+	the one that is the \co{Fail1:} label?
+	\end{lineref}
 \QuickQuizAnswer{
 	The implementation of powerpc version of \co{atomic_add_return()}
 	loops when the \co{stwcx} instruction fails, which it communicates
@@ -195,36 +208,32 @@ and line~11 is equivalent to the C statement \co{r3=x}.
 } \QuickQuizEnd
 
 \begin{listing}[tbp]
-{ \scriptsize
-\begin{verbbox}
- 1 void P0(void)
- 2 {
- 3   int r3;
- 4 
- 5   x = 1; /* Lines 8 and 9 */
- 6   atomic_add_return(&z, 0); /* Lines 10-15 */
- 7   r3 = y; /* Line 16 */
- 8 }
- 9 
-10 void P1(void)
-11 {
-12   int r3;
-13 
-14   y = 1; /* Lines 8-9 */
-15   smp_mb(); /* Line 10 */
-16   r3 = x; /* Line 11 */
-17 }
-\end{verbbox}
+\begin{VerbatimL}
+void P0(void)
+{
+	int r3;
+
+	x = 1; /* Lines 8 and 9 */
+	atomic_add_return(&z, 0); /* Lines 10-15 */
+	r3 = y; /* Line 16 */
+}
+
+void P1(void)
+{
+	int r3;
+
+	y = 1; /* Lines 8-9 */
+	smp_mb(); /* Line 10 */
+	r3 = x; /* Line 11 */
 }
-\centering
-\theverbbox
+\end{VerbatimL}
 \caption{Meaning of PPCMEM Litmus Test}
 \label{lst:formal:Meaning of PPCMEM Litmus Test}
 \end{listing}
 
 Putting all this together, the C-language equivalent to the entire litmus
 test is as shown in
-Listing~\ref{lst:formal:Meaning of PPCMEM Litmus Test}.
+\cref{lst:formal:Meaning of PPCMEM Litmus Test}.
 The key point is that if \co{atomic_add_return()} acts as a full
 memory barrier (as the Linux kernel requires it to), 
 then it should be impossible for \co{P0()}'s and \co{P1()}'s \co{r3}
@@ -245,8 +254,7 @@ possible sequence of events, a separate tool is provided for this
 purpose~\cite{PaulEMcKenney2011ppcmem}.
 
 \begin{listing}[tbp]
-{ \scriptsize
-\begin{verbbox}
+\begin{VerbatimL}[numbers=none,xleftmargin=0pt]
 ./ppcmem -model lwsync_read_block \
          -model coherence_points filename.litmus
 ...
@@ -261,21 +269,18 @@ Ok
 Condition exists (0:r3=0 /\ 1:r3=0)
 Hash=e2240ce2072a2610c034ccd4fc964e77
 Observation SB+lwsync-RMW-lwsync+isync Sometimes 1
-\end{verbbox}
-}
-\centering
-\theverbbox
+\end{VerbatimL}
 \caption{PPCMEM Detects an Error}
 \label{lst:formal:PPCMEM Detects an Error}
 \end{listing}
 
 Because the litmus test shown in
-Listing~\ref{lst:formal:PPCMEM Litmus Test}
+\cref{lst:formal:PPCMEM Litmus Test}
 contains read-modify-write instructions, we must add \co{-model}
 arguments to the command line.
 If the litmus test is stored in \co{filename.litmus},
 this will result in the output shown in
-Listing~\ref{lst:formal:PPCMEM Detects an Error},
+\cref{lst:formal:PPCMEM Detects an Error},
 where the \co{...} stands for voluminous making-progress output.
 The list of states includes \co{0:r3=0; 1:r3=0;}, indicating once again
 that the old PowerPC implementation of \co{atomic_add_return()} does
@@ -284,8 +289,7 @@ The ``Sometimes'' on the last line confirms this: the assertion triggers
 for some executions, but not all of the time.
 
 \begin{listing}[tbp]
-{ \scriptsize
-\begin{verbbox}
+\begin{VerbatimL}[numbers=none,xleftmargin=0pt]
 ./ppcmem -model lwsync_read_block \
          -model coherence_points filename.litmus
 ...
@@ -299,17 +303,14 @@ No (allowed not found)
 Condition exists (0:r3=0 /\ 1:r3=0)
 Hash=77dd723cda9981248ea4459fcdf6097d
 Observation SB+lwsync-RMW-lwsync+sync Never 0 5
-\end{verbbox}
-}
-\centering
-\theverbbox
+\end{VerbatimL}
 \caption{PPCMEM on Repaired Litmus Test}
 \label{lst:formal:PPCMEM on Repaired Litmus Test}
 \end{listing}
 
 The fix to this Linux-kernel bug is to replace P0's \co{isync} with
 \co{sync}, which results in the output shown in
-Listing~\ref{lst:formal:PPCMEM on Repaired Litmus Test}.
+\cref{lst:formal:PPCMEM on Repaired Litmus Test}.
 As you can see, \co{0:r3=0; 1:r3=0;} does not appear in the list of states,
 and the last line calls out ``Never''.
 Therefore, the model predicts that the offending execution sequence
-- 
2.17.1

[PATCH 3/6] bib/swtools: Add refereneces to PowerPC atomic RMW fixes

[Akira Yokosawa]

From 8db4e623387758479ffcf2ba1c50587f3acef283 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Fri, 27 Sep 2019 21:56:39 +0900
Subject: [PATCH 3/6] bib/swtools: Add refereneces to PowerPC atomic RMW fixes

BenjaminHerrenschmidt2011:powerpc:atomic_return is the commit
replacing "isync" with "sync".

Paulmck2015:powerpc:value-returning-atomics points to an email
thread on the use of "lwsync".

BoqunFeng2015:powerpc:value-returning-atomics is the commit
replacing "lwsync" with "sync".

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 bib/swtools.bib | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)

diff --git a/bib/swtools.bib b/bib/swtools.bib
index 55356664..c9c159b1 100644
--- a/bib/swtools.bib
+++ b/bib/swtools.bib
@@ -197,6 +197,17 @@
 ,keywords = {compiler optimizations, relaxed memory models, semantics}
 }
 
+@unpublished{BenjaminHerrenschmidt2011:powerpc:atomic_return
+,Author="Benjamin Herrenschmidt"
+,Title="powerpc: Fix atomic\_xxx\_return barrier semantics"
+,month="November"
+,day="16"
+,year="2011"
+,note="Git commit:
+\url{https://git.kernel.org/linus/b97021f85517}"
+,lastchecked="August 7, 2019"
+}
+
 @unpublished{RexBlack2012SQA
 ,author="Rex Black and Capers Jones"
 ,title="Economics of Software Quality: An Interview with {Capers} {Jones}, Part 1 of 2 (Podcast Transcript)"
@@ -884,6 +895,28 @@ Michalis Kokologiannakis"
 ,note="\url{http://www.rdrop.com/users/paulmck/scalability/paper/Validation.2016.04.06e.SpecMtg.pdf}"
 }
 
+@unpublished{Paulmck2015:powerpc:value-returning-atomics
+,Author="Paul E. McKenney"
+,Title="Re: [PATCH tip/locking/core v4 1/6] powerpc: atomic: Make *xchg and *cmpxchg a full barrier"
+,month="October"
+,day="14"
+,year="2015"
+,note="Email thread:
+\url{https://lore.kernel.org/lkml/20151014201916.GB3910@linux.vnet.ibm.com/}"
+,lastchecked="August 7, 2019"
+}
+
+@unpublished{BoqunFeng2015:powerpc:value-returning-atomics
+,Author="Boqun Feng"
+,Title="powerpc: Make value-returning atomics fully ordered"
+,month="November"
+,day="2"
+,year="2015"
+,note="Git commit:
+\url{https://git.kernel.org/linus/49e9cf3f0c04}"
+,lastchecked="August 7, 2019"
+}
+
 @misc{PeterZijlstra2016aLKMM
 ,author = {Peter Zijlstra}
 ,title = {{[tip:perf/urgent]} perf/core: Fix sys\_perf\_event\_open() vs. hotplug}
-- 
2.17.1

[PATCH 4/6] ppcmem: Cite Git commit of PowerPC atomic_xxx_return fix

[Akira Yokosawa]

From 9f0e3855ed4b366167248ae8a4398920c8ac3a40 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Fri, 27 Sep 2019 21:58:20 +0900
Subject: [PATCH 4/6] ppcmem: Cite Git commit of PowerPC atomic_xxx_return fix

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 formal/ppcmem.tex | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/formal/ppcmem.tex b/formal/ppcmem.tex
index a5cb90e3..d292b7da 100644
--- a/formal/ppcmem.tex
+++ b/formal/ppcmem.tex
@@ -322,7 +322,8 @@ cannot happen.
 	ARM does not have this particular bug because that it places
 	\co{smp_mb()} before and after the \co{atomic_add_return()}
 	function's assembly-language implementation.
-	PowerPC no longer has this bug; it has long since been fixed.
+	PowerPC no longer has this bug; it has long since been
+	fixed~\cite{BenjaminHerrenschmidt2011:powerpc:atomic_return}.
 	Finding any other bugs that the Linux kernel might have is left
 	as an exercise for the reader.
 } \QuickQuizEnd
-- 
2.17.1

[PATCH 5/6] ppcmem: Add Quick Quiz on lwsync in Listing 12.23

[Akira Yokosawa]

From 305c387fd4b8e6d3c5599b4ddbd67a03d939f832 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Fri, 27 Sep 2019 22:02:41 +0900
Subject: [PATCH 5/6] ppcmem: Add Quick Quiz on lwsync in Listing 12.23

The "lwsync" in front of ll-sc in atomic_add_return() is not
good enough for Linux kernel's semantics.
Add a Quick Quiz on the use of lwsync.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 formal/ppcmem.tex | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/formal/ppcmem.tex b/formal/ppcmem.tex
index d292b7da..a1960e2d 100644
--- a/formal/ppcmem.tex
+++ b/formal/ppcmem.tex
@@ -328,6 +328,24 @@ cannot happen.
 	as an exercise for the reader.
 } \QuickQuizEnd
 
+\QuickQuiz{}
+	\begin{lineref}[ln:formal:PPCMEM Litmus Test]
+	Is the \co{lwsync} on \clnref{P0lwsync} in
+	\cref{lst:formal:PPCMEM Litmus Test} good enough?
+	\end{lineref}
+\QuickQuizAnswer{
+	It depends on the semantics you expect.
+	As is discussed in
+	\cref{chp:Advanced Synchronization: Memory Ordering},
+	Linux kernel's momory consistency model requires
+	value-returning atomic RMW operations to be fully ordered
+	on both sides. \co{lwsync} is insufficient in this case and
+	should be \co{sync} instead. It has since been fixed~%
+	\cite{BoqunFeng2015:powerpc:value-returning-atomics}
+	as a result of an email thread on a couple of other litmus
+	tests~\cite{Paulmck2015:powerpc:value-returning-atomics}.
+} \QuickQuizEnd
+
 \subsection{PPCMEM Discussion}
 \label{sec:formal:PPCMEM Discussion}
 
-- 
2.17.1

[PATCH 6/6] ppcmem: Move final sentence of Answer to QQZ 12.27 to the next

[Akira Yokosawa]

From 6442399eab974be84927a3b57d34f31de7e81700 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Fri, 27 Sep 2019 22:05:08 +0900
Subject: [PATCH 6/6] ppcmem: Move final sentence of Answer to QQZ 12.27 to the next

Given the added Quick Quiz, this sentence looks better fitted in
the next one.

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

diff --git a/formal/ppcmem.tex b/formal/ppcmem.tex
index a1960e2d..dff0b0b2 100644
--- a/formal/ppcmem.tex
+++ b/formal/ppcmem.tex
@@ -324,8 +324,6 @@ cannot happen.
 	function's assembly-language implementation.
 	PowerPC no longer has this bug; it has long since been
 	fixed~\cite{BenjaminHerrenschmidt2011:powerpc:atomic_return}.
-	Finding any other bugs that the Linux kernel might have is left
-	as an exercise for the reader.
 } \QuickQuizEnd
 
 \QuickQuiz{}
@@ -344,6 +342,8 @@ cannot happen.
 	\cite{BoqunFeng2015:powerpc:value-returning-atomics}
 	as a result of an email thread on a couple of other litmus
 	tests~\cite{Paulmck2015:powerpc:value-returning-atomics}.
+	Finding any other bugs that the Linux kernel might have is left
+	as an exercise for the reader.
 } \QuickQuizEnd
 
 \subsection{PPCMEM Discussion}
-- 
2.17.1

Re: [PATCH 0/6] ppcmem: Apply new scheme of code snippets

[Paul E. McKenney]

On Sat, Sep 28, 2019 at 10:56:10AM +0900, Akira Yokosawa wrote:
> Subject: [PATCH 0/6] ppcmem: Apply new scheme of code snippets
> 
> Hi Paul,
> 
> This patch series mostly consists of code snippet updates in
> formal/ppcmem.tex.
> 
> Patch #1 fixes a trivial typo in dyntickrcu.
> Patch #2 is the main changes in this series. It also employs
> "cleveref" way of cross references.
> 
> Patches #3--#6 touches the text and add a couples of references
> to PowerPC atomic updates in the Linux kernel.
> 
> Patch #3 adds entries in bib/swtools
> Patch #4 adds citation of Git commit in 2013
> Patches #5 and #6 add a Quick Quiz on another missing full memory
> barrier in the beginning. I'm not that sure the added Quick Quiz
> makes sense, though. If it doesn't, please skip #5 and #6.

I believe that the additional Quick Quiz is worthwhile, but I felt
the need to edit it a bit.  I have queued and pushed the result.
Could you please double-check it?

And good stuff, thank you!

							Thanx, Paul

> I remember asking you about the difference of the code emitted by
> an atomic built-in of PowerPC-GCC and the code in Linux kernel [1].
> IIUC, the added references and Quick Quiz are related to the
> question.
> 
> [1]: https://www.spinics.net/lists/perfbook/msg02077.html
> 
> Seeing the history of the changes and your answer to [1], I suspect
> that now that PPC_ATOMIC_ENTRY_BARRIER is "sync", "isync" might be
> sufficient for PPC_ATOMIC_EXIT_BARRIER. Obviously I'm not an expert
> of PowerPC and can be missing something, but I couldn't help
> mentioning.
> 
>         Thanks, Akira
> --
> Akira Yokosawa (6):
>   dyntickrcu: Fix trivial typo
>   ppcmem: Apply new scheme of code snippets
>   bib/swtools: Add refereneces to PowerPC atomic RMW fixes
>   ppcmem: Cite Git commit of PowerPC atomic_xxx_return fix
>   ppcmem: Add Quick Quiz on lwsync in Listing 12.23
>   ppcmem: Move final sentence of Answer to QQZ 12.27 to the next
> 
>  bib/swtools.bib       |  33 +++++++
>  formal/dyntickrcu.tex |   2 +-
>  formal/ppcmem.tex     | 210 +++++++++++++++++++++++-------------------
>  3 files changed, 149 insertions(+), 96 deletions(-)
> 
> -- 
> 2.17.1
> 

Re: [PATCH 0/6] ppcmem: Apply new scheme of code snippets

[Akira Yokosawa]

On Wed, 2 Oct 2019 19:50:09 -0700, Paul E. McKenney wrote:
> On Sat, Sep 28, 2019 at 10:56:10AM +0900, Akira Yokosawa wrote:
>> Subject: [PATCH 0/6] ppcmem: Apply new scheme of code snippets
>>
>> Hi Paul,
>>
>> This patch series mostly consists of code snippet updates in
>> formal/ppcmem.tex.
>>
>> Patch #1 fixes a trivial typo in dyntickrcu.
>> Patch #2 is the main changes in this series. It also employs
>> "cleveref" way of cross references.
>>
>> Patches #3--#6 touches the text and add a couples of references
>> to PowerPC atomic updates in the Linux kernel.
>>
>> Patch #3 adds entries in bib/swtools
>> Patch #4 adds citation of Git commit in 2013
>> Patches #5 and #6 add a Quick Quiz on another missing full memory
>> barrier in the beginning. I'm not that sure the added Quick Quiz
>> makes sense, though. If it doesn't, please skip #5 and #6.
> 
> I believe that the additional Quick Quiz is worthwhile, but I felt
> the need to edit it a bit.  I have queued and pushed the result.
> Could you please double-check it?

As always, your edit looks perfect to me!

> 
> And good stuff, thank you!
> 
> 							Thanx, Paul
> 
>> I remember asking you about the difference of the code emitted by
>> an atomic built-in of PowerPC-GCC and the code in Linux kernel [1].
>> IIUC, the added references and Quick Quiz are related to the
>> question.
>>
>> [1]: https://www.spinics.net/lists/perfbook/msg02077.html
>>
>> Seeing the history of the changes and your answer to [1], I suspect
>> that now that PPC_ATOMIC_ENTRY_BARRIER is "sync", "isync" might be
>> sufficient for PPC_ATOMIC_EXIT_BARRIER. Obviously I'm not an expert
>> of PowerPC and can be missing something, but I couldn't help
>> mentioning.

Now I think I finally understand that PPC_ATOMIC_EXIT_BARRIER needs to
be "sync".

Semantics of __ATOMIC_SEQ_CST of GCC's atomic built-in:

__ATOMIC_SEQ_CST:

    Enforces total ordering with all other __ATOMIC_SEQ_CST operations. 

OTOH, Linux kernel's value-returning atomic RMW operations need to be
strongly ordered from any observer.  So their semantics are different.

        Thanks, Akira

>>
>>         Thanks, Akira
>> --
>> Akira Yokosawa (6):
>>   dyntickrcu: Fix trivial typo
>>   ppcmem: Apply new scheme of code snippets
>>   bib/swtools: Add refereneces to PowerPC atomic RMW fixes
>>   ppcmem: Cite Git commit of PowerPC atomic_xxx_return fix
>>   ppcmem: Add Quick Quiz on lwsync in Listing 12.23
>>   ppcmem: Move final sentence of Answer to QQZ 12.27 to the next
>>
>>  bib/swtools.bib       |  33 +++++++
>>  formal/dyntickrcu.tex |   2 +-
>>  formal/ppcmem.tex     | 210 +++++++++++++++++++++++-------------------
>>  3 files changed, 149 insertions(+), 96 deletions(-)
>>
>> -- 
>> 2.17.1
>>