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

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

 



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?

							Thanx, Paul

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

commit 9b44286879769a0973982807c80b6e0a7821a1de
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..327b1ad254bf 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
+	Figure~\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
+	Figure~\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
+	Figure~\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



[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Index of Archives]     [Linux NFS]     [Linux NILFS]     [Linux USB Devel]     [Video for Linux]     [Linux Audio Users]     [Yosemite News]     [Linux Kernel]     [Linux SCSI]

  Powered by Linux