On Sun, Nov 12, 2017 at 08:26:21AM +0900, Akira Yokosawa wrote:
> On 2017/11/11 08:57:23 -0800, Paul E. McKenney wrote:
> > 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. ;-)
>
> ;-) ;-)
>
> Please see inline (nitpicking) comments below.
>
> Thanks, Akira
>
> >
> > 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"
> > +}
>
> 2nd parentheses should be removed in code snippets.
>
> > +
> > +P0(int *x0, int *x1)
> > +{
> > + WRITE_ONCE(*x0, 1);
> > + smp_wmb();
> > + WRITE_ONCE(*x1, 2);
> > +}
>
> Need to convert "tab" -> " ".
Good catches, fixed.
> > +
> > +
> > +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}.
>
> And the exists clause triggers by herd7 verification. (Redundant???)
Good point, added.
> > +
> > +\begin{listing}[tbp]
> > +{ \scriptsize
> > +\begin{verbbox}[\LstLineNo]
> > +C C-2+2W+o-o+o-o
> > +{
> > +}
> > +
> > +{
> > +#include "api.h"
> > +}
>
> Ditto.
>
> > +
> > +P0(int *x0, int *x1)
> > +{
> > + WRITE_ONCE(*x0, 1);
> > + WRITE_ONCE(*x1, 2);
>
> Ditto.
And these.
> > +}
> > +
> > +
> > +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}%
> > +%
>
> These "%"s have no effect because of the blank line above the
> "listing" environment. You can remove them if you are OK with
> the following sentence starting a new paragraph.
OK, I removed them. So we only need the "%"s if we want the figure
in the middle of a paragraph?
Thanx, Paul
> > + 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
