[PATCH] advsync: Fix control-dependency no-transitivity example

[PATCH] advsync: Fix control-dependency no-transitivity example

[Akira Yokosawa]

From 8740c546fbb6988c2fcf4a88c4314df972d0b9b7 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Fri, 14 Jul 2017 22:48:37 +0900
Subject: [PATCH] advsync: Fix control-dependency no-transitivity example

The corresponding assert condition in memory-barriers.txt was
fixed in commit 5646f7acc95f ("memory-barriers: Fix control-
ordering no-transitivity example") of Linux kernel repository.
Somehow it was imported to perfbook in a wrong form and has
survived since.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 advsync/memorybarriers.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/advsync/memorybarriers.tex b/advsync/memorybarriers.tex
index c9c975c..25a90b2 100644
--- a/advsync/memorybarriers.tex
+++ b/advsync/memorybarriers.tex
@@ -3036,9 +3036,9 @@ not), then adding the following CPU would guarantee a related assertion:
 \begin{tabular}{l}
 	\nf{CPU 2} \\
 	\hline
-	\tco{WRITE_ONCE(y, 1);} \\
+	\tco{WRITE_ONCE(x, 2);} \\
 	\multicolumn{1}{l}{~} \\
-	\multicolumn{1}{l}{\tco{assert(!(r1 == 1 && r2 == 1 && x == 1));}} \\
+	\multicolumn{1}{l}{\tco{assert(!(r1 == 2 && r2 == 1 && x == 2));}} \\
 \end{tabular}
 \end{minipage}
 \vspace{5pt}
-- 
2.7.4

[PATCH] advsync: Fix two-CPU control-dependency example

[Akira Yokosawa]

From 8996357b6bd21245ef6545fca0c282fb4a31349e Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Sun, 16 Jul 2017 20:33:14 +0900
Subject: [PATCH] advsync: Fix two-CPU control-dependency example

The two-CPU example always results in r1==0 && r2==0 when the
operator ">" is used in the "if" statement.
The point of this example is to use control dependency for ordering,
and the WRITE_ONCE() should always be executed.

So the corresponding example in memory-barriers.txt was correct
before commit 5646f7acc95f in Linux kernel repository.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
Hi Paul,

So sounds like you didn't like the previous patch in this thread.
I tried to convert the examples to litmus test format,
and found out the two-CPU example results in a single outcome.

If you prefer these examples to be converted to litmus test format,
I can respin these patches and add the tests to CodeSamples.
But I need to know what names to use for the tests.
Do "C-SB+o-c-o+o-c-o" and "C-WWC+o-c-o+o-c-o+o" work?

Or if these changes conflict with your ongoing work, I'll back off.

FWIW I've not seen the three-CPU litmus test results in "sometimes",
even on PPC. 

      Thanks, Akira
--
 advsync/memorybarriers.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/advsync/memorybarriers.tex b/advsync/memorybarriers.tex
index 894de6d..f0ca79d 100644
--- a/advsync/memorybarriers.tex
+++ b/advsync/memorybarriers.tex
@@ -3015,8 +3015,8 @@ of~\co{x} and~\co{y} both being zero:
 	\hline
 	\tco{r1 = READ_ONCE(x);} &
 		\tco{r2 = READ_ONCE(y);} \\
-	if (r1 > 0) &
-		if (r2 > 0) \\
+	if (r1 >= 0) &
+		if (r2 >= 0) \\
 	~~~\tco{WRITE_ONCE(y, 1);} &
 		~~~\tco{WRITE_ONCE(x, 1);} \\
 	\multicolumn{2}{l}{~} \\
-- 
2.7.4

Re: [PATCH] advsync: Fix two-CPU control-dependency example

[Paul E. McKenney]

On Sun, Jul 16, 2017 at 11:27:58PM +0900, Akira Yokosawa wrote:
> >From 8996357b6bd21245ef6545fca0c282fb4a31349e Mon Sep 17 00:00:00 2001
> From: Akira Yokosawa <akiyks@gmail.com>
> Date: Sun, 16 Jul 2017 20:33:14 +0900
> Subject: [PATCH] advsync: Fix two-CPU control-dependency example
> 
> The two-CPU example always results in r1==0 && r2==0 when the
> operator ">" is used in the "if" statement.
> The point of this example is to use control dependency for ordering,
> and the WRITE_ONCE() should always be executed.
> 
> So the corresponding example in memory-barriers.txt was correct
> before commit 5646f7acc95f in Linux kernel repository.
> 
> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> ---
> Hi Paul,
> 
> So sounds like you didn't like the previous patch in this thread.
> I tried to convert the examples to litmus test format,
> and found out the two-CPU example results in a single outcome.
> 
> If you prefer these examples to be converted to litmus test format,
> I can respin these patches and add the tests to CodeSamples.
> But I need to know what names to use for the tests.
> Do "C-SB+o-c-o+o-c-o" and "C-WWC+o-c-o+o-c-o+o" work?
> 
> Or if these changes conflict with your ongoing work, I'll back off.
> 
> FWIW I've not seen the three-CPU litmus test results in "sometimes",
> even on PPC. 

Sorry, I was distracted with C++ standards-committee work, and got
behind on my email.  No opinion at all on them yet.

If these two patches are either-or, I would take the one that matches
memory-barriers.txt.  Please advise.  ;-)

This part of the file is likely to be overwritten at some point, but
it would be good to remove confusion in the meantime.

On the PPC end of things, the hardware often has stronger ordering
than does the architecture.  For example, Power hardware is reluctant
to reorder later writes wiht earlier reads, despite the fact that
the architecture allows this.  So it would be good to get some
tests that actually show reordering on PPC.

Your names look good, and I would welcome help in converting things
to litmus tests.  To that end, I have a github archive with lots
of litmus tests, some manually generated and some automatically
generated:

	https://github.com/paulmckrcu/litmus

Which reminds me...  Do you have access to a Linux system on which
you can install kernel modules?  There is a klitmus7 that does that.

							Thanx, Paul

>       Thanks, Akira
> --
>  advsync/memorybarriers.tex | 4 ++--
>  1 file changed, 2 insertions(+), 2 deletions(-)
> 
> diff --git a/advsync/memorybarriers.tex b/advsync/memorybarriers.tex
> index 894de6d..f0ca79d 100644
> --- a/advsync/memorybarriers.tex
> +++ b/advsync/memorybarriers.tex
> @@ -3015,8 +3015,8 @@ of~\co{x} and~\co{y} both being zero:
>  	\hline
>  	\tco{r1 = READ_ONCE(x);} &
>  		\tco{r2 = READ_ONCE(y);} \\
> -	if (r1 > 0) &
> -		if (r2 > 0) \\
> +	if (r1 >= 0) &
> +		if (r2 >= 0) \\
>  	~~~\tco{WRITE_ONCE(y, 1);} &
>  		~~~\tco{WRITE_ONCE(x, 1);} \\
>  	\multicolumn{2}{l}{~} \\
> -- 
> 2.7.4
> 
> 

Re: [PATCH] advsync: Fix two-CPU control-dependency example

[Akira Yokosawa]

On 2017/07/16 16:40:28 -0700, Paul E. McKenney wrote:
> On Sun, Jul 16, 2017 at 11:27:58PM +0900, Akira Yokosawa wrote:
>> >From 8996357b6bd21245ef6545fca0c282fb4a31349e Mon Sep 17 00:00:00 2001
>> From: Akira Yokosawa <akiyks@gmail.com>
>> Date: Sun, 16 Jul 2017 20:33:14 +0900
>> Subject: [PATCH] advsync: Fix two-CPU control-dependency example
>>
>> The two-CPU example always results in r1==0 && r2==0 when the
>> operator ">" is used in the "if" statement.
>> The point of this example is to use control dependency for ordering,
>> and the WRITE_ONCE() should always be executed.
>>
>> So the corresponding example in memory-barriers.txt was correct
>> before commit 5646f7acc95f in Linux kernel repository.
>>
>> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
>> ---
>> Hi Paul,
>>
>> So sounds like you didn't like the previous patch in this thread.
>> I tried to convert the examples to litmus test format,
>> and found out the two-CPU example results in a single outcome.
>>
>> If you prefer these examples to be converted to litmus test format,
>> I can respin these patches and add the tests to CodeSamples.
>> But I need to know what names to use for the tests.
>> Do "C-SB+o-c-o+o-c-o" and "C-WWC+o-c-o+o-c-o+o" work?
>>
>> Or if these changes conflict with your ongoing work, I'll back off.
>>
>> FWIW I've not seen the three-CPU litmus test results in "sometimes",
>> even on PPC. 
> 
> Sorry, I was distracted with C++ standards-committee work, and got
> behind on my email.  No opinion at all on them yet.

I see.

> 
> If these two patches are either-or, I would take the one that matches
> memory-barriers.txt.  Please advise.  ;-)

The 1st one ("advsync: Fix control-dependency no-transitivity example")
is the catchup to memroy-barriers.txt.

As for the 2nd one, would it be better to fix memory-barriers.txt first
if the two-CPU example actually neesd the partial revert? 

> 
> This part of the file is likely to be overwritten at some point, but
> it would be good to remove confusion in the meantime.
> 
> On the PPC end of things, the hardware often has stronger ordering
> than does the architecture.  For example, Power hardware is reluctant
> to reorder later writes wiht earlier reads, despite the fact that
> the architecture allows this.  So it would be good to get some
> tests that actually show reordering on PPC.
> 
> Your names look good, and I would welcome help in converting things
> to litmus tests.  To that end, I have a github archive with lots
> of litmus tests, some manually generated and some automatically
> generated:
> 
> 	https://github.com/paulmckrcu/litmus
> 
> Which reminds me...  Do you have access to a Linux system on which
> you can install kernel modules?

If a virtual guest machine on x86, I should be able to. Does that
suffice?

           Thanks, Akira

>                                 There is a klitmus7 that does that.
> 
> 							Thanx, Paul
> 
>>       Thanks, Akira
>> --
>>  advsync/memorybarriers.tex | 4 ++--
>>  1 file changed, 2 insertions(+), 2 deletions(-)
>>
>> diff --git a/advsync/memorybarriers.tex b/advsync/memorybarriers.tex
>> index 894de6d..f0ca79d 100644
>> --- a/advsync/memorybarriers.tex
>> +++ b/advsync/memorybarriers.tex
>> @@ -3015,8 +3015,8 @@ of~\co{x} and~\co{y} both being zero:
>>  	\hline
>>  	\tco{r1 = READ_ONCE(x);} &
>>  		\tco{r2 = READ_ONCE(y);} \\
>> -	if (r1 > 0) &
>> -		if (r2 > 0) \\
>> +	if (r1 >= 0) &
>> +		if (r2 >= 0) \\
>>  	~~~\tco{WRITE_ONCE(y, 1);} &
>>  		~~~\tco{WRITE_ONCE(x, 1);} \\
>>  	\multicolumn{2}{l}{~} \\
>> -- 
>> 2.7.4
>>
>>
> 
> 

Re: [PATCH] advsync: Fix control-dependency no-transitivity example

[Paul E. McKenney]

On Fri, Jul 14, 2017 at 11:34:45PM +0900, Akira Yokosawa wrote:
> >From 8740c546fbb6988c2fcf4a88c4314df972d0b9b7 Mon Sep 17 00:00:00 2001
> From: Akira Yokosawa <akiyks@gmail.com>
> Date: Fri, 14 Jul 2017 22:48:37 +0900
> Subject: [PATCH] advsync: Fix control-dependency no-transitivity example
> 
> The corresponding assert condition in memory-barriers.txt was
> fixed in commit 5646f7acc95f ("memory-barriers: Fix control-
> ordering no-transitivity example") of Linux kernel repository.
> Somehow it was imported to perfbook in a wrong form and has
> survived since.
> 
> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>

And I did take this, thank you very much, and please accept my apologies
for the delay.

If I understand correctly, I should leave your second patch alone.
If I am confused, please let me know!

							Thanx, Paul

> ---
>  advsync/memorybarriers.tex | 4 ++--
>  1 file changed, 2 insertions(+), 2 deletions(-)
> 
> diff --git a/advsync/memorybarriers.tex b/advsync/memorybarriers.tex
> index c9c975c..25a90b2 100644
> --- a/advsync/memorybarriers.tex
> +++ b/advsync/memorybarriers.tex
> @@ -3036,9 +3036,9 @@ not), then adding the following CPU would guarantee a related assertion:
>  \begin{tabular}{l}
>  	\nf{CPU 2} \\
>  	\hline
> -	\tco{WRITE_ONCE(y, 1);} \\
> +	\tco{WRITE_ONCE(x, 2);} \\
>  	\multicolumn{1}{l}{~} \\
> -	\multicolumn{1}{l}{\tco{assert(!(r1 == 1 && r2 == 1 && x == 1));}} \\
> +	\multicolumn{1}{l}{\tco{assert(!(r1 == 2 && r2 == 1 && x == 2));}} \\
>  \end{tabular}
>  \end{minipage}
>  \vspace{5pt}
> -- 
> 2.7.4
> 

Re: [PATCH] advsync: Fix two-CPU control-dependency example

[Paul E. McKenney]

On Mon, Jul 17, 2017 at 09:45:26AM +0900, Akira Yokosawa wrote:
> On 2017/07/16 16:40:28 -0700, Paul E. McKenney wrote:
> > On Sun, Jul 16, 2017 at 11:27:58PM +0900, Akira Yokosawa wrote:
> >> >From 8996357b6bd21245ef6545fca0c282fb4a31349e Mon Sep 17 00:00:00 2001
> >> From: Akira Yokosawa <akiyks@gmail.com>
> >> Date: Sun, 16 Jul 2017 20:33:14 +0900
> >> Subject: [PATCH] advsync: Fix two-CPU control-dependency example
> >>
> >> The two-CPU example always results in r1==0 && r2==0 when the
> >> operator ">" is used in the "if" statement.
> >> The point of this example is to use control dependency for ordering,
> >> and the WRITE_ONCE() should always be executed.
> >>
> >> So the corresponding example in memory-barriers.txt was correct
> >> before commit 5646f7acc95f in Linux kernel repository.
> >>
> >> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> >> ---
> >> Hi Paul,
> >>
> >> So sounds like you didn't like the previous patch in this thread.
> >> I tried to convert the examples to litmus test format,
> >> and found out the two-CPU example results in a single outcome.
> >>
> >> If you prefer these examples to be converted to litmus test format,
> >> I can respin these patches and add the tests to CodeSamples.
> >> But I need to know what names to use for the tests.
> >> Do "C-SB+o-c-o+o-c-o" and "C-WWC+o-c-o+o-c-o+o" work?
> >>
> >> Or if these changes conflict with your ongoing work, I'll back off.
> >>
> >> FWIW I've not seen the three-CPU litmus test results in "sometimes",
> >> even on PPC. 
> > 
> > Sorry, I was distracted with C++ standards-committee work, and got
> > behind on my email.  No opinion at all on them yet.
> 
> I see.
> 
> > If these two patches are either-or, I would take the one that matches
> > memory-barriers.txt.  Please advise.  ;-)
> 
> The 1st one ("advsync: Fix control-dependency no-transitivity example")
> is the catchup to memroy-barriers.txt.

As noted in my other email, applied!

> As for the 2nd one, would it be better to fix memory-barriers.txt first
> if the two-CPU example actually neesd the partial revert? 

This is the one below that changes the ">" to ">=" in the "if"
conditions, correct?  (If not please point me in the right direction.)

If so, the change would be correct in theory, but I would like to
keep the ">" because with the change to ">=" an enthusiastic
compiler could potentially figure out that the values of "x" and "y"
are never negative, and thus leave out the "if" statement completely,
resulting in the following optimized program:

	CPU 0                     CPU 1
	=======================   =======================
	r1 = READ_ONCE(x);        r2 = READ_ONCE(y);
	WRITE_ONCE(y, 1);         WRITE_ONCE(x, 1);

	assert(!(r1 == 1 && r2 == 1));

Both the compiler and many CPUs would be within their rights to
reorder either CPU's read with its write, which could cause the
assertion to trigger.

So again, let's please keep the ">".

> > This part of the file is likely to be overwritten at some point, but
> > it would be good to remove confusion in the meantime.
> > 
> > On the PPC end of things, the hardware often has stronger ordering
> > than does the architecture.  For example, Power hardware is reluctant
> > to reorder later writes wiht earlier reads, despite the fact that
> > the architecture allows this.  So it would be good to get some
> > tests that actually show reordering on PPC.
> > 
> > Your names look good, and I would welcome help in converting things
> > to litmus tests.  To that end, I have a github archive with lots
> > of litmus tests, some manually generated and some automatically
> > generated:
> > 
> > 	https://github.com/paulmckrcu/litmus
> > 
> > Which reminds me...  Do you have access to a Linux system on which
> > you can install kernel modules?
> 
> If a virtual guest machine on x86, I should be able to. Does that
> suffice?

It does!

							Thanx, Paul

>            Thanks, Akira
> 
> >                                 There is a klitmus7 that does that.
> > 
> > 							Thanx, Paul
> > 
> >>       Thanks, Akira
> >> --
> >>  advsync/memorybarriers.tex | 4 ++--
> >>  1 file changed, 2 insertions(+), 2 deletions(-)
> >>
> >> diff --git a/advsync/memorybarriers.tex b/advsync/memorybarriers.tex
> >> index 894de6d..f0ca79d 100644
> >> --- a/advsync/memorybarriers.tex
> >> +++ b/advsync/memorybarriers.tex
> >> @@ -3015,8 +3015,8 @@ of~\co{x} and~\co{y} both being zero:
> >>  	\hline
> >>  	\tco{r1 = READ_ONCE(x);} &
> >>  		\tco{r2 = READ_ONCE(y);} \\
> >> -	if (r1 > 0) &
> >> -		if (r2 > 0) \\
> >> +	if (r1 >= 0) &
> >> +		if (r2 >= 0) \\
> >>  	~~~\tco{WRITE_ONCE(y, 1);} &
> >>  		~~~\tco{WRITE_ONCE(x, 1);} \\
> >>  	\multicolumn{2}{l}{~} \\
> >> -- 
> >> 2.7.4
> >>
> >>
> > 
> > 
> 
> --
> To unsubscribe from this list: send the line "unsubscribe perfbook" in
> the body of a message to majordomo@vger.kernel.org
> More majordomo info at  http://vger.kernel.org/majordomo-info.html
> 

Re: [PATCH] advsync: Fix control-dependency no-transitivity example

[Akira Yokosawa]

On 2017/07/20 2:30, Paul E. McKenney wrote:
> On Fri, Jul 14, 2017 at 11:34:45PM +0900, Akira Yokosawa wrote:
>> >From 8740c546fbb6988c2fcf4a88c4314df972d0b9b7 Mon Sep 17 00:00:00 2001
>> From: Akira Yokosawa <akiyks@gmail.com>
>> Date: Fri, 14 Jul 2017 22:48:37 +0900
>> Subject: [PATCH] advsync: Fix control-dependency no-transitivity example
>>
>> The corresponding assert condition in memory-barriers.txt was
>> fixed in commit 5646f7acc95f ("memory-barriers: Fix control-
>> ordering no-transitivity example") of Linux kernel repository.
>> Somehow it was imported to perfbook in a wrong form and has
>> survived since.
>>
>> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> 
> And I did take this, thank you very much, and please accept my apologies
> for the delay.
> 
> If I understand correctly, I should leave your second patch alone.

For the moment, yes!

But as I said in the other thread, I'm beginning to think of
rewriting these examples in pseudo-asm form.

          Thanks, Akira

> If I am confused, please let me know!
> 
> 							Thanx, Paul
> 
>> ---
>>  advsync/memorybarriers.tex | 4 ++--
>>  1 file changed, 2 insertions(+), 2 deletions(-)
>>
>> diff --git a/advsync/memorybarriers.tex b/advsync/memorybarriers.tex
>> index c9c975c..25a90b2 100644
>> --- a/advsync/memorybarriers.tex
>> +++ b/advsync/memorybarriers.tex
>> @@ -3036,9 +3036,9 @@ not), then adding the following CPU would guarantee a related assertion:
>>  \begin{tabular}{l}
>>  	\nf{CPU 2} \\
>>  	\hline
>> -	\tco{WRITE_ONCE(y, 1);} \\
>> +	\tco{WRITE_ONCE(x, 2);} \\
>>  	\multicolumn{1}{l}{~} \\
>> -	\multicolumn{1}{l}{\tco{assert(!(r1 == 1 && r2 == 1 && x == 1));}} \\
>> +	\multicolumn{1}{l}{\tco{assert(!(r1 == 2 && r2 == 1 && x == 2));}} \\
>>  \end{tabular}
>>  \end{minipage}
>>  \vspace{5pt}
>> -- 
>> 2.7.4
>>
> 
>