Re: [PATCH 3/3] CodeSamples/formal: Get rid of warnings in cross compiling

["Paul E. McKenney" <paulmck@linux.vnet.ibm.com>]

On Sat, Nov 11, 2017 at 08:44:38AM -0800, Paul E. McKenney wrote:
> On Sat, Nov 11, 2017 at 08:56:01AM +0900, Akira Yokosawa wrote:
> > On 2017/11/11 08:41:54 +0900, Akira Yokosawa wrote:
> > >>From 6ecff66f2b5f95e914d90e29b6d0a2eb4d8901cc Mon Sep 17 00:00:00 2001
> > > From: Akira Yokosawa <akiyks@gmail.com>
> > > Date: Sat, 11 Nov 2017 08:25:34 +0900
> > > Subject: [PATCH 3/3] CodeSamples/formal: Get rid of warnings in cross compiling
> > > 
> > > Also fix corresponding code snippet.
> > > 
> > > Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> > > ---
> > >  CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus | 2 --
> > 
> > By the way Paul, didn't you have a plan to mention these "C-2+2W" litmus tests
> > somewhere in the memorder chapter?
> 
> Good point, it is an odd corner case that is worth at least a quick quiz.
> How about the following?

My fingers just keep automatically typing "Figure", so please see a
corrected patch below.  Presumably my fingers will get with the program
in a few months.  ;-)

							Thanx, Paul

------------------------------------------------------------------------

commit ac730edc868b6c8a9a71637fd205553e7ba88df2
Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Date:   Sat Nov 11 08:41:47 2017 -0800

    memorder: Add a quick quiz for the 2+2W litmus tests
    
    Reported-by: Akira Yokosawa <akiyks@gmail.com>
    Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>

diff --git a/memorder/memorder.tex b/memorder/memorder.tex
index 7d8e4978fa6d..2ef8363fba6a 100644
--- a/memorder/memorder.tex
+++ b/memorder/memorder.tex
@@ -2455,7 +2455,103 @@ same variable is not necessarily the store that started last.
 This should not come as a surprise to anyone who carefully examined
 Figure~\ref{fig:memorder:A Variable With More Simultaneous Values}.

-But sometimes time is on our side, as shown in the next section.
+\begin{listing}[tbp]
+{ \scriptsize
+\begin{verbbox}[\LstLineNo]
+C C-2+2W+o-wmb-o+o-wmb-o
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x0, int *x1)
+{
+	WRITE_ONCE(*x0, 1);
+	smp_wmb();
+	WRITE_ONCE(*x1, 2);
+}
+
+
+P1(int *x0, int *x1)
+{
+	WRITE_ONCE(*x1, 1);
+	smp_wmb();
+	WRITE_ONCE(*x0, 2);
+}
+
+exists (x0=1 /\ x1=1)
+\end{verbbox}
+}
+\centering
+\theverbbox
+\caption{2+2W Litmus Test With Write Barriers}
+\label{lst:memorder:2+2W Litmus Test With Write Barriers}
+\end{listing}
+
+\QuickQuiz{}
+	But for litmus tests having only ordered stores, as shown in
+	Listing~\ref{lst:memorder:2+2W Litmus Test With Write Barriers}
+	(\path{C-2+2W+o-wmb-o+o-wmb-o.litmus}),
+	research shows that the cycle is prohibited, even in weakly
+	ordered systems such as ARM and Power~\cite{test6-pdf}.
+	Given that, are store-to-store really \emph{always}
+	counter-temporal???
+\QuickQuizAnswer{
+	This litmus test is indeed a very interesting curiosity.
+	Its ordering apparently occurs naturally given typical
+	weakly ordered hardware design, which would normally be
+	considered a great gift from the relevant laws of physics
+	and cache-coherency-protocol mathematics.
+
+	Unfortunately, no one has been able to come up with a software use
+	case for this gift that does not have a much better alternative
+	implementation.
+	Therefore, neither the C11 nor the Linux kernel memory models
+	provide any guarantee corresponding to
+	Listing~\ref{lst:memorder:2+2W Litmus Test With Write Barriers}.
+
+\begin{listing}[tbp]
+{ \scriptsize
+\begin{verbbox}[\LstLineNo]
+C C-2+2W+o-o+o-o
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x0, int *x1)
+{
+	WRITE_ONCE(*x0, 1);
+	WRITE_ONCE(*x1, 2);
+}
+
+
+P1(int *x0, int *x1)
+{
+	WRITE_ONCE(*x1, 1);
+	WRITE_ONCE(*x0, 2);
+}
+
+exists (x0=1 /\ x1=1)
+\end{verbbox}
+}
+\centering
+\theverbbox
+\caption{2+2W Litmus Test Without Write Barriers}
+\label{lst:memorder:2+2W Litmus Test Without Write Barriers}
+\end{listing}%
+%
+	Of course, without the barrier, there are no ordering
+	guarantees, even on real weakly ordered hardware, as shown in
+	Listing~\ref{lst:memorder:2+2W Litmus Test Without Write Barriers}
+	(\path{C-2+2W+o-o+o-o.litmus}).
+} \QuickQuizEnd
+
+But sometimes time really is on our side.  Read on!

 \subsubsection{Happens-Before}
 \label{sec:memorder:Happens-Before}