On Tue, Nov 14, 2017 at 09:07:06PM +0900, Akira Yokosawa wrote:
> >From 9b53814671df7e54b294599959b739f592196258 Mon Sep 17 00:00:00 2001
> From: Akira Yokosawa <akiyks@xxxxxxxxx>
> Date: Tue, 14 Nov 2017 20:57:08 +0900
> Subject: [PATCH] memorder: Use litmus test in section 'control dependency calamity'
>
> Also substitute "cumulativity" for "transitivity".
Applied and pushed, good catch, thank you!
Thanx, Paul
> Signed-off-by: Akira Yokosawa <akiyks@xxxxxxxxx>
> ---
> memorder/memorder.tex | 139 ++++++++++++++++++++++++++++++++++----------------
> 1 file changed, 94 insertions(+), 45 deletions(-)
>
> diff --git a/memorder/memorder.tex b/memorder/memorder.tex
> index f028789..180a721 100644
> --- a/memorder/memorder.tex
> +++ b/memorder/memorder.tex
> @@ -3957,54 +3957,103 @@ invoked by those two clauses), not to code following that ``\co{if}''.
> Finally, control dependencies do \emph{not} provide cumulativity.\footnote{
> Refer to Section~\ref{sec:memorder:Cumulativity} for
> the meaning of cumulativity.}
> -This is demonstrated by two related examples, with the initial values
> -of~\co{x} and~\co{y} both being zero:
> +This is demonstrated by two related litmus tests, namely
> +Listings~\ref{lst:memorder:LB Litmus Test With Control Dependency}
> +and~\ref{lst:memorder:WWC Litmus Test With Control Dependency (Cumulativity?)}
> +with the initial values
> +of~\co{x} and~\co{y} both being zero.
>
> -\vspace{5pt}
> -\begin{minipage}[t]{\columnwidth}
> -\tt
> -\scriptsize
> -\begin{tabular}{l|p{1.5in}}
> - \nf{CPU 0} & \nf{CPU 1} \\
> - \hline
> - \tco{r1 = READ_ONCE(x);} &
> - \tco{r2 = READ_ONCE(y);} \\
> - if (r1 > 0) &
> - if (r2 > 0) \\
> - ~~~\tco{WRITE_ONCE(y, 1);} &
> - ~~~\tco{WRITE_ONCE(x, 1);} \\
> - \multicolumn{2}{l}{~} \\
> - \multicolumn{2}{l}{\tco{assert(!(r1 == 1 && r2 == 1));}} \\
> -\end{tabular}
> -\end{minipage}
> -\vspace{5pt}
> +\begin{listing}
> +{ \scriptsize
> +\begin{verbbox}[\LstLineNo]
> +C C-LB+o-cgt-o+o-cgt-o
> +{
> +}
>
> -The above two-CPU example will never trigger the \co{assert()}.
> -However, if control dependencies guaranteed transitivity (which they do
> -not), then adding the following CPU would guarantee a related assertion:
> +P0(int *x, int *y)
> +{
> + int r1;
>
> -\vspace{5pt}
> -\begin{minipage}[t]{\columnwidth}
> -\tt
> -\scriptsize
> -\begin{tabular}{l}
> - \nf{CPU 2} \\
> - \hline
> - \tco{WRITE_ONCE(x, 2);} \\
> - \multicolumn{1}{l}{~} \\
> - \multicolumn{1}{l}{\tco{assert(!(r1 == 2 && r2 == 1 && x == 2));}} \\
> -\end{tabular}
> -\end{minipage}
> -\vspace{5pt}
> + r1 = READ_ONCE(*x);
> + if (r1 > 0)
> + WRITE_ONCE(*y, 1);
> +}
> +
> +P1(int *x, int *y)
> +{
> + int r2;
> +
> + r2 = READ_ONCE(*y);
> + if (r2 > 0)
> + WRITE_ONCE(*x, 1);
> +}
> +
> +exists (0:r1=1 /\ 1:r2=1)
> +\end{verbbox}
> +}
> +\centering
> +\theverbbox
> +\caption{LB Litmus Test With Control Dependency}
> +\label{lst:memorder:LB Litmus Test With Control Dependency}
> +\end{listing}
> +
> +The \co{exists} clause in the two-thread example of
> +Listing~\ref{lst:memorder:LB Litmus Test With Control Dependency}
> +(\path{C-LB+o-cgt-o+o-cgt-o.litmus})
> +will never trigger.
> +If control dependencies guaranteed cumulativity (which they do
> +not), then adding a thread to the example as in
> +Listing~\ref{lst:memorder:WWC Litmus Test With Control Dependency (Cumulativity?)}
> +(\path{C-WWC+o-cgt-o+o-cgt-o+o.litmus})
> +would guarantee the related \co{exists} clause never to trigger.
> +
> +\begin{listing}
> +{ \scriptsize
> +\begin{verbbox}[\LstLineNo]
> +C C-WWC+o-cgt-o+o-cgt-o+o
> +{
> +}
> +
> +P0(int *x, int *y)
> +{
> + int r1;
> +
> + r1 = READ_ONCE(*x);
> + if (r1 > 0)
> + WRITE_ONCE(*y, 1);
> +}
> +
> +P1(int *x, int *y)
> +{
> + int r2;
> +
> + r2 = READ_ONCE(*y);
> + if (r2 > 0)
> + WRITE_ONCE(*x, 1);
> +}
> +
> +P2(int *x)
> +{
> + WRITE_ONCE(*x, 2);
> +}
> +
> +exists (0:r1=2 /\ 1:r2=1 /\ x=2)
> +\end{verbbox}
> +}
> +\centering
> +\theverbbox
> +\caption{WWC Litmus Test With Control Dependency (Cumulativity?)}
> +\label{lst:memorder:WWC Litmus Test With Control Dependency (Cumulativity?)}
> +\end{listing}
>
> -But because control dependencies do \emph{not} provide transitivity, the above
> -assertion can fail after the combined three-CPU example completes.
> -If you need the three-CPU example to provide ordering, you will need
> -\co{smp_mb()} between the loads and stores in the CPU~0 and CPU~1 code
> -fragments, that is, just before or just after the ``\co{if}'' statements.
> -Furthermore, the original two-CPU example is very fragile and should be avoided.
> +But because control dependencies do \emph{not} provide cumulativity, the
> +\co{exists} clause in the three-thread litmus test can trigger.
> +If you need the three-thread example to provide ordering, you will need
> +\co{smp_mb()} between the loads and stores in threads \co{P0()} and \co{P1()},
> +that is, just before or just after the ``\co{if}'' statements.
> +Furthermore, the original two-thread example is very fragile and should be avoided.
>
> -The two-CPU example is known as LB (load buffering) and the three-CPU
> +The two-thread example is known as LB (load buffering) and the three-thread
> example as WWC~\cite{Maranget2012TutorialARMPower}.
>
> The following list of rules summarizes the lessons of this section:
> @@ -4053,8 +4102,8 @@ The following list of rules summarizes the lessons of this section:
> \item Control dependencies pair normally with other types of
> memory-ordering operations.
>
> -\item Control dependencies do \emph{not} provide transitivity.
> - If you need transitivity, use \co{smp_mb()}.
> +\item Control dependencies do \emph{not} provide cumulativity.
> + If you need cumulativity, use \co{smp_mb()}.
> \end{enumerate}
>
> In short, many popular languages were designed primarily with
> --
> 2.7.4
>
--
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
