Message-Id: <935D3930-C369-4B0E-ACDC-5BFDFA85AA72@in.tum.de>
Date:   Wed, 31 Aug 2022 18:42:05 +0200
From:   Paul Heidekrüger <Paul.Heidekrueger@...tum.de>
To:     Alan Stern <stern@...land.harvard.edu>
Cc:     Joel Fernandes <joel@...lfernandes.org>,
        Andrea Parri <parri.andrea@...il.com>,
        Will Deacon <will@...nel.org>,
        Peter Zijlstra <peterz@...radead.org>,
        Boqun Feng <boqun.feng@...il.com>,
        Nicholas Piggin <npiggin@...il.com>,
        David Howells <dhowells@...hat.com>,
        Jade Alglave <j.alglave@....ac.uk>,
        Luc Maranget <luc.maranget@...ia.fr>,
        "Paul E. McKenney" <paulmck@...nel.org>,
        Akira Yokosawa <akiyks@...il.com>,
        Daniel Lustig <dlustig@...dia.com>,
        LKML <linux-kernel@...r.kernel.org>,
        linux-arch <linux-arch@...r.kernel.org>,
        Marco Elver <elver@...gle.com>,
        Charalampos Mainas <charalampos.mainas@...il.com>,
        Pramod Bhatotia <pramod.bhatotia@...tum.de>,
        Soham Chakraborty <s.s.chakraborty@...elft.nl>,
        Martin Fink <martin.fink@...tum.de>
Subject: Re: [PATCH] tools/memory-model: Weaken ctrl dependency definition in
 explanation.txt

On 31. Aug 2022, at 03:57, Alan Stern <stern@...land.harvard.edu> wrote:

> On Tue, Aug 30, 2022 at 05:12:33PM -0400, Joel Fernandes wrote:
>> On 8/30/2022 5:08 PM, Joel Fernandes wrote:
>>> On 8/30/2022 4:44 PM, Paul Heidekrüger wrote:
>>>> The current informal control dependency definition in explanation.txt is
>>>> too broad and, as dicsussed, needs to be updated.
>>>> 
>>>> Consider the following example:
>>>> 
>>>>> if(READ_ONCE(x))
>>>>> 	return 42;
>>>>> 
>>>>> 	WRITE_ONCE(y, 42);
>>>>> 
>>>>> 	return 21;
>>>> 
>>>> The read event determines whether the write event will be executed "at
>>>> all" - as per the current definition - but the formal LKMM does not
>>>> recognize this as a control dependency.
>>>> 
>>>> Introduce a new defintion which includes the requirement for the second
>>>> memory access event to syntactically lie within the arm of a non-loop
>>>> conditional.
>>>> 
>>>> Link: https://lore.kernel.org/all/20220615114330.2573952-1-paul.heidekrueger@in.tum.de/
>>>> Cc: Marco Elver <elver@...gle.com>
>>>> Cc: Charalampos Mainas <charalampos.mainas@...il.com>
>>>> Cc: Pramod Bhatotia <pramod.bhatotia@...tum.de>
>>>> Cc: Soham Chakraborty <s.s.chakraborty@...elft.nl>
>>>> Cc: Martin Fink <martin.fink@...tum.de>
>>>> Signed-off-by: Paul Heidekrüger <paul.heidekrueger@...tum.de>
>>>> Co-developed-by: Alan Stern <stern@...land.harvard.edu>
>>>> ---
>>>> 
>>>> @Alan:
>>>> 
>>>> Since I got it wrong the last time, I'm adding you as a co-developer after my
>>>> SOB. I'm sorry if this creates extra work on your side due to you having to
>>>> resubmit the patch now with your SOB if I understand correctly, but since it's
>>>> based on your wording from the other thread, I definitely wanted to give you
>>>> credit.
>>>> 
>>>> tools/memory-model/Documentation/explanation.txt | 7 ++++---
>>>> 1 file changed, 4 insertions(+), 3 deletions(-)
>>>> 
>>>> diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
>>>> index ee819a402b69..0bca50cac5f4 100644
>>>> --- a/tools/memory-model/Documentation/explanation.txt
>>>> +++ b/tools/memory-model/Documentation/explanation.txt
>>>> @@ -464,9 +464,10 @@ to address dependencies, since the address of a location accessed
>>>> through a pointer will depend on the value read earlier from that
>>>> pointer.
>>>> 
>>>> -Finally, a read event and another memory access event are linked by a
>>>> -control dependency if the value obtained by the read affects whether
>>>> -the second event is executed at all.  Simple example:
>>>> +Finally, a read event X and another memory access event Y are linked by
>>>> +a control dependency if Y syntactically lies within an arm of an if,
>>>> +else or switch statement and the condition guarding Y is either data or
>>>> +address-dependent on X.  Simple example:

Thank you both for commenting!

> "if, else or switch" should be just "if or switch".  In C there is no 
> such thing as an "else" statement; an "else" clause is merely part of 
> an "if" statement.  In fact, maybe "body" would be more appropriate than 
> "arm", because "switch" statements don't have arms -- they have cases.

Right. What do you think of "branch"? "Body" to me suggests that there's
only one and therefore that the else clause isn't included.

Would it be fair to say that switch statements have branches? I guess
because switch statements are a convenient way of writing goto's, i.e.
jumps, it's a stretch and basically the same as saying "arm"?

Maybe we can avoid the arm / case clash by just having a definition for if
statements and appending something like "similarly for switch statements"?

>>> 'conditioning guarding Y' sounds confusing to me as it implies to me that the
>>> condition's evaluation depends on Y. I much prefer Alan's wording from the
>>> linked post saying something like 'the branch condition is data or address
>>> dependent on X, and Y lies in one of the arms'.
>>> 
>>> I have to ask though, why doesn't this imply that the second instruction never
>>> executes at all? I believe that would break the MP-pattern if it were not true.
>> 
>> About my last statement, I believe your patch does not disagree with the
>> correctness of the earlier text but just wants to improve it. If that's case
>> then that's fine.
> 
> The biggest difference between the original text and Paul's suggested 
> update is that the new text makes clear that Y has to lie within the 
> body of the "if" or "switch" statement.  If Y follows the end of the 
> if/else, as in the example at the top of this email, then it does have 
> not a control dependency on X (at least, not via that if/else), even 
> though the value read by X does determine whether or not Y will execute.
> 
> [It has to be said that this illustrates a big weakness of the LKMM: It 
> isn't cognizant of "goto"s or "return"s.  This naturally derives from 
> limitations of the herd tool, but the situation could be improved.  So 
> for instance, I don't think it would cause trouble to say that in:
> 
> 	if (READ_ONCE(x) == 0)
> 		return;
> 	WRITE_ONCE(y, 5);
> 
> there really is a control dependence from x to y, even though the 
> WRITE_ONCE is outside the body of the "if" statement.  Certainly the 
> compiler can't reorder the write before the read.  But AFAIK there's no 
> way to include a "return" statement in a litmus test for herd.  Or a 
> subroutine definition, for that matter.]
> 
> I agree that "condition guarding Y" is somewhat awkward.  "the 
> condition of the if (or the expression of the switch)" might be better, 
> even though it is somewhat awkward as well.  At least it's more 
> explicit.

Maybe we can reuse the wording from the data and address dependency
definition here and say "affects"?

Putting it all together:

> Finally, a read event X and another memory access event Y are linked by a
> control dependency if Y syntactically lies within a branch of an if or
> switch statement and X affects the evaluation of that statement's
> condition via a data or address dependency.

Alternatively without the arm / case clash:

> Finally, a read event X and another memory access event Y are linked by a
> control dependency if Y syntactically lies within an arm of an if
> statement and X affects the evaluation of the if condition via a data or
> address dependency.  Similarly for switch statements.

What do you think?

Paul



Download attachment "smime.p7s" of type "application/pkcs7-signature" (5449 bytes)

Powered by blists - more mailing lists