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

Akira Yokosawa
2017-07-19T21:33:34Z

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
>
>