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@xxxxxxxxx>
> > > 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@xxxxxxxxx>
> > > ---
> > > 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@xxxxxxxxxxxxxxxxxx>
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@xxxxxxxxx>
Signed-off-by: Paul E. McKenney <paulmck@xxxxxxxxxxxxxxxxxx>
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}
--
To unsubscribe from this list: send the line "unsubscribe perfbook" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at http://vger.kernel.org/majordomo-info.html
