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

[Akira Yokosawa <akiyks@gmail.com>]

On 2017/07/20 2:43, Paul E. McKenney wrote:
> On Mon, Jul 17, 2017 at 05:24:42PM +0900, Akira Yokosawa wrote:
>> >From b798b9b631e237d285aa8699da00bfb8ced33bea Mon Sep 17 00:00:00 2001
>> From: Akira Yokosawa <akiyks@gmail.com>
>> Date: Mon, 17 Jul 2017 16:25:33 +0900
>> Subject: [PATCH] documentation: Fix two-CPU control-dependency example
>>
>> In commit 5646f7acc95f ("memory-barriers: Fix control-ordering
>> no-transitivity example"), the operator in "if" statement of
>> the two-CPU example was modified from ">=" to ">".
>> Now the example misses the point because there is no party
>> who will modify "x" nor "y". So each CPU performs only the
>> READ_ONCE().
>>
>> The point of this example is to use control dependency for ordering,
>> and the WRITE_ONCE() should always be executed.
>>
>> So it was correct prior to the above mentioned commit. Partial
>> revert of the commit (with context adjustments regarding other
>> changes thereafter) restores the point.
>>
>> Note that the three-CPU example demonstrating the lack of
>> transitivity stands regardless of this partial revert.
>>
>> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> 
> Hello, Akira,
> 
> You are quite right that many compilers would generate straightforward
> code for the code fragment below, and in that case, the assertion could
> never trigger due to either TSO or control dependencies, depending on
> the architecture this was running on.
> 
> However, if the compiler was too smart for our good, it could figure
> out that "x" and "y" only take on the values zero and one, so that
> the "if" would always be taken.  At that point, the compiler could
> simply ignore the "if" with the result shown below.
> 
>> ---
>>  Documentation/memory-barriers.txt | 2 +-
>>  1 file changed, 1 insertion(+), 1 deletion(-)
>>
>> diff --git a/Documentation/memory-barriers.txt b/Documentation/memory-barriers.txt
>> index c4ddfcd..c1ebe99 100644
>> --- a/Documentation/memory-barriers.txt
>> +++ b/Documentation/memory-barriers.txt
>> @@ -851,7 +851,7 @@ demonstrated by two related examples, with the initial values of
>>  	CPU 0                     CPU 1
>>  	=======================   =======================
>>  	r1 = READ_ONCE(x);        r2 = READ_ONCE(y);
>> -	if (r1 > 0)               if (r2 > 0)
>> +	if (r1 >= 0)              if (r2 >= 0)
>>  	  WRITE_ONCE(y, 1);         WRITE_ONCE(x, 1);
>>
>>  	assert(!(r1 == 1 && r2 == 1));
> 
> Original program:
> 
>  	CPU 0                     CPU 1
>  	=======================   =======================
>  	r1 = READ_ONCE(x);        r2 = READ_ONCE(y);
> 	if (r1 >= 0)              if (r2 >= 0)
>  	  WRITE_ONCE(y, 1);         WRITE_ONCE(x, 1);
> 
>  	assert(!(r1 == 1 && r2 == 1));
> 
> Enthusiastically 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));
> 
> This optimized version could trigger the assertion.
> 
> So we do need to stick with the ">" comparison.

Well but,

Current example:

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

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

Such a clever compiler might be able to prove that "x" and "y"
are never modified and end up in the following:

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

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

This means it is impossible to describe this example in C,
doesn't it?

What am I missing here?

            Thanks, Akira

> That said, I very much welcome critical reviews of memory-barriers.txt,
> so please do feel free to continue doing that!
> 
> 							Thanx, Paul
> 
>