[PATCH RFC] tools/memory-model: Adjust ctrl dependency definition

[PATCH RFC] tools/memory-model: Adjust ctrl dependency definition

[Paul Heidekrüger]

Hi all,

I have been confused by explanation.txt's definition of control
dependencies:

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

I'll go into the following:

====
1. "At all", to me, is misleading
  1.1 The code which confused me
  1.2 The traditional definition via post-dominance doesn't work either
2. Solution
====

1. "At all", to me, is misleading:

"At all" to me suggests a question for which we require a definitive
"yes" or "no" answer: given a programme and an input, can a certain
piece of code be executed? Can we always answer this this question?
Doesn't this sound similar to the halting problem?

1.1 The Example which confused me:

For the dependency checker project [1], I've been thinking about
tracking dependency chains in code, and I stumbled upon the following
edge case, which made me question the "at all" part of the current
definition. The below C-code is derived from some optimised kernel code
in LLVM intermediate representation (IR) I encountered:

> int *x, *y;
>
> int foo()
> {
> /* More code */
>
> 	 loop:
> 		/* More code */
>
> 	 	if(READ_ONCE(x)) {
> 	 		WRITE_ONCE(y, 42);
> 	 		return 0;
> 	 	}
>
> 		/* More code */
>
> 	 	goto loop;
>
>       /* More code */
> }

Assuming that foo() will return, the READ_ONCE() does not determine
whether the WRITE_ONCE() will be executed __at all__, as it will be
executed exactly when the function returns, instead, it determines
__when__ the WRITE_ONCE() will be executed.

1.2. The definition via post-dominance doesn't work either:

I have seen control dependencies being defined in terms of the first
basic block that post-dominates the basic block of the if-condition,
that is the first basic block control flow must take to reach the
function return regardless of what the if condition returned.

E.g. [2] defines control dependencies as follows:

> A statement y is said to be control dependent on another statement x
> if (1) there exists a nontrivial path from x to y such that every
> statement z != x in the path is post-dominated by y, and (2) x is not
> post-dominated by y.

Again, this definition doesn't work for the example above. As the basic
block of the if branch trivially post-dominates any other basic block,
because it contains the function return.

2. Solution:

The definition I came up with instead is the following:

> A basic block B is control-dependent on a basic block A if
> B is reachable from A, but control flow can take a path through A
> which avoids B. The scope of a control dependency ends at the first
> basic block where all control flow paths running through A meet.

Note that this allows control dependencies to remain "unresolved".

I'm happy to submit a patch which covers more of what I mentioned above
as part of explanation.txt, but figured that in the spirit of keeping
things simple, leaving out "at all" might be enough?

What do you think?

Many thanks,
Paul

[1]: https://lore.kernel.org/all/Yk7%2FT8BJITwz+Og1@Pauls-MacBook-Pro.local/T/#u
[2]: Optimizing Compilers for Modern Architectures: A Dependence-Based
Approach, Randy Allen, Ken Kennedy, 2002, p. 350

Signed-off-by: Paul Heidekrüger <paul.heidekrueger@in.tum.de>
Cc: Marco Elver <elver@google.com>
Cc: Charalampos Mainas <charalampos.mainas@gmail.com>
Cc: Pramod Bhatotia <pramod.bhatotia@in.tum.de>
Cc: Soham Chakraborty <s.s.chakraborty@tudelft.nl>
Cc: Martin Fink <martin.fink@in.tum.de>
---
 tools/memory-model/Documentation/explanation.txt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
index ee819a402b69..42af7ed91313 100644
--- a/tools/memory-model/Documentation/explanation.txt
+++ b/tools/memory-model/Documentation/explanation.txt
@@ -466,7 +466,7 @@ 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:
+the second event is executed.  Simple example:
 
 	int x, y;
 
-- 
2.35.1

Re: [PATCH RFC] tools/memory-model: Adjust ctrl dependency definition

[Alan Stern]

On Wed, Jun 15, 2022 at 11:43:29AM +0000, Paul Heidekrüger wrote:
> Hi all,
> 
> I have been confused by explanation.txt's definition of control
> dependencies:
> 
> > 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.
> 
> I'll go into the following:
> 
> ====
> 1. "At all", to me, is misleading
>   1.1 The code which confused me
>   1.2 The traditional definition via post-dominance doesn't work either
> 2. Solution
> ====
> 
> 1. "At all", to me, is misleading:
> 
> "At all" to me suggests a question for which we require a definitive
> "yes" or "no" answer: given a programme and an input, can a certain
> piece of code be executed? Can we always answer this this question?
> Doesn't this sound similar to the halting problem?

No.  You're not thinking about this the right way.

The point of view we take in this document and in the LKMM is not like 
the view in a static analysis of a program.  It is a dynamic analysis of 
one particular execution of a program.  The halting problem does not 
apply.  Note for instance that explanation.txt talks about "events" 
rather than instructions or pieces of code.

(The single-execution-at-a-time point of view has its own limitations, 
which do have some adverse affects on the LKMM.  But we don't want to 
exceed the capabilities of the herd7 tool.)

> 1.1 The Example which confused me:
> 
> For the dependency checker project [1], I've been thinking about
> tracking dependency chains in code, and I stumbled upon the following
> edge case, which made me question the "at all" part of the current
> definition. The below C-code is derived from some optimised kernel code
> in LLVM intermediate representation (IR) I encountered:
> 
> > int *x, *y;
> >
> > int foo()
> > {
> > /* More code */
> >
> > 	 loop:
> > 		/* More code */
> >
> > 	 	if(READ_ONCE(x)) {
> > 	 		WRITE_ONCE(y, 42);
> > 	 		return 0;
> > 	 	}
> >
> > 		/* More code */
> >
> > 	 	goto loop;
> >
> >       /* More code */
> > }
> 
> Assuming that foo() will return, the READ_ONCE() does not determine
> whether the WRITE_ONCE() will be executed __at all__, as it will be
> executed exactly when the function returns, instead, it determines
> __when__ the WRITE_ONCE() will be executed.

But what if your assumption is wrong?

In any case, your question displays an incorrect viewpoint.  For 
instance, the READ_ONCE() does not count as a single event.  Rather, 
each iteration through the loop executes a separate instance of the 
READ_ONCE(), and each instance counts as its own event.  Think of events 
not as static entities in the program source but instead as the items in 
the queue that gets fed into the CPU's execution unit at run time.

Strictly speaking, one could say there is a control dependency from each 
of these READ_ONCE() events to the final WRITE_ONCE().  However the LKMM 
takes a more limited viewpoint, saying that a dependency from a load to 
the controlling expression of an "if" statement only affects the 
execution of the events corresponding to statements lying statically in 
the two arms of the "if".  In your example the "if" has a single arm, 
and so only the access in that arm is considered to have a control 
dependency from the preceding instance of the READ_ONCE().  And it 
doesn't have a control dependency from any of the earlier iterations of 
the READ_ONCE(), because it doesn't lie in any of the arms of the 
earlier iterations of the "if".

> 1.2. The definition via post-dominance doesn't work either:
> 
> I have seen control dependencies being defined in terms of the first
> basic block that post-dominates the basic block of the if-condition,
> that is the first basic block control flow must take to reach the
> function return regardless of what the if condition returned.
> 
> E.g. [2] defines control dependencies as follows:
> 
> > A statement y is said to be control dependent on another statement x
> > if (1) there exists a nontrivial path from x to y such that every
> > statement z != x in the path is post-dominated by y, and (2) x is not
> > post-dominated by y.
> 
> Again, this definition doesn't work for the example above. As the basic
> block of the if branch trivially post-dominates any other basic block,
> because it contains the function return.

Again, not applicable as basic blocks, multiple paths, and so on belong 
to static analysis.

> 2. Solution:
> 
> The definition I came up with instead is the following:
> 
> > A basic block B is control-dependent on a basic block A if
> > B is reachable from A, but control flow can take a path through A
> > which avoids B. The scope of a control dependency ends at the first
> > basic block where all control flow paths running through A meet.
> 
> Note that this allows control dependencies to remain "unresolved".
> 
> I'm happy to submit a patch which covers more of what I mentioned above
> as part of explanation.txt, but figured that in the spirit of keeping
> things simple, leaving out "at all" might be enough?
> 
> What do you think?

Not so good.  A better description would be that there is a control 
dependency from a read event X to a memory access event Y if there is a 
dependency (data or address) from X to the conditional branch event of 
an "if" statement which contains Y in one of its arms.  And similarly 
for "switch" statements.

Alan

> Many thanks,
> Paul
> 
> [1]: https://lore.kernel.org/all/Yk7%2FT8BJITwz+Og1@Pauls-MacBook-Pro.local/T/#u
> [2]: Optimizing Compilers for Modern Architectures: A Dependence-Based
> Approach, Randy Allen, Ken Kennedy, 2002, p. 350
> 
> Signed-off-by: Paul Heidekrüger <paul.heidekrueger@in.tum.de>
> Cc: Marco Elver <elver@google.com>
> Cc: Charalampos Mainas <charalampos.mainas@gmail.com>
> Cc: Pramod Bhatotia <pramod.bhatotia@in.tum.de>
> Cc: Soham Chakraborty <s.s.chakraborty@tudelft.nl>
> Cc: Martin Fink <martin.fink@in.tum.de>
> ---
>  tools/memory-model/Documentation/explanation.txt | 2 +-
>  1 file changed, 1 insertion(+), 1 deletion(-)
> 
> diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
> index ee819a402b69..42af7ed91313 100644
> --- a/tools/memory-model/Documentation/explanation.txt
> +++ b/tools/memory-model/Documentation/explanation.txt
> @@ -466,7 +466,7 @@ 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:
> +the second event is executed.  Simple example:
>  
>  	int x, y;
>  
> -- 
> 2.35.1
> 

Re: [PATCH RFC] tools/memory-model: Adjust ctrl dependency definition

[Paul Heidekrüger]

Thanks for taking the time to read and provide feedback - much appreciated!

> On 15. Jun 2022, at 16:16, Alan Stern <stern@rowland.harvard.edu> wrote:
> 
> On Wed, Jun 15, 2022 at 11:43:29AM +0000, Paul Heidekrüger wrote:
>> Hi all,
>> 
>> I have been confused by explanation.txt's definition of control
>> dependencies:
>> 
>>> 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.
>> 
>> I'll go into the following:
>> 
>> ====
>> 1. "At all", to me, is misleading
>> 1.1 The code which confused me
>> 1.2 The traditional definition via post-dominance doesn't work either
>> 2. Solution
>> ====
>> 
>> 1. "At all", to me, is misleading:
>> 
>> "At all" to me suggests a question for which we require a definitive
>> "yes" or "no" answer: given a programme and an input, can a certain
>> piece of code be executed? Can we always answer this this question?
>> Doesn't this sound similar to the halting problem?
> 
> No. You're not thinking about this the right way.
> 
> The point of view we take in this document and in the LKMM is not like 
> the view in a static analysis of a program. It is a dynamic analysis of 
> one particular execution of a program. The halting problem does not 
> apply. Note for instance that explanation.txt talks about "events" 
> rather than instructions or pieces of code.
> 
> (The single-execution-at-a-time point of view has its own limitations, 
> which do have some adverse affects on the LKMM. But we don't want to 
> exceed the capabilities of the herd7 tool.)
> 
>> 1.1 The Example which confused me:
>> 
>> For the dependency checker project [1], I've been thinking about
>> tracking dependency chains in code, and I stumbled upon the following
>> edge case, which made me question the "at all" part of the current
>> definition. The below C-code is derived from some optimised kernel code
>> in LLVM intermediate representation (IR) I encountered:
>> 
>>> int *x, *y;
>>> 
>>> int foo()
>>> {
>>> /* More code */
>>> 
>>> 	 loop:
>>> 		/* More code */
>>> 
>>> 	 	if(READ_ONCE(x)) {
>>> 	 		WRITE_ONCE(y, 42);
>>> 	 		return 0;
>>> 	 	}
>>> 
>>> 		/* More code */
>>> 
>>> 	 	goto loop;
>>> 
>>> /* More code */
>>> }
>> 
>> Assuming that foo() will return, the READ_ONCE() does not determine
>> whether the WRITE_ONCE() will be executed __at all__, as it will be
>> executed exactly when the function returns, instead, it determines
>> __when__ the WRITE_ONCE() will be executed.
> 
> But what if your assumption is wrong?
> 
> In any case, your question displays an incorrect viewpoint. For 
> instance, the READ_ONCE() does not count as a single event. Rather, 
> each iteration through the loop executes a separate instance of the 
> READ_ONCE(), and each instance counts as its own event. Think of events 
> not as static entities in the program source but instead as the items in 
> the queue that gets fed into the CPU's execution unit at run time.
> 
> Strictly speaking, one could say there is a control dependency from each 
> of these READ_ONCE() events to the final WRITE_ONCE(). However the LKMM 
> takes a more limited viewpoint, saying that a dependency from a load to 
> the controlling expression of an "if" statement only affects the 
> execution of the events corresponding to statements lying statically in 
> the two arms of the "if". In your example the "if" has a single arm, 
> and so only the access in that arm is considered to have a control 
> dependency from the preceding instance of the READ_ONCE(). And it 
> doesn't have a control dependency from any of the earlier iterations of 
> the READ_ONCE(), because it doesn't lie in any of the arms of the 
> earlier iterations of the "if".

OK. So, LKMM limits the scope of control dependencies to its arm(s), hence
there is a control dependency from the last READ_ONCE() before the loop
exists to the WRITE_ONCE().

But then what about the following:

> int *x, *y;
> 
> int foo()
> {
> 	/* More code */
> 
> 	if(READ_ONCE(x))
> 		return 42;
> 
> 	/* More code */
> 
> 	WRITE_ONCE(y, 42);
> 
> 	/* More code */
> 
> 	return 0;
> }

The READ_ONCE() determines whether the WRITE_ONCE() will be executed at all,
but the WRITE_ONCE() doesn't lie in the if condition's arm. However, by
"inverting" the if, we get the following equivalent code:

> if(!READ_ONCE(x)) {
> 	/* More code */
> 
> 	WRITE_ONCE(y, 42);
> 
> 	/* More code */
> 
> 	return 0;
> }
> 
> return 42;

Now, the WRITE_ONCE() is in the if's arm, and there is clearly a control
dependency.

Similar cases:

> if(READ_ONCE())
> 	foo(); /* WRITE_ONCE() in foo() */
> return 42;

or

> if(READ_ONCE())
>     goto foo; /* WRITE_ONCE() after foo */
> return 42;

In both cases, the WRITE_ONCE() again isn't in the if's arm syntactically
speaking, but again, with rewriting, you can end up with a control
dependency; in the first case via inlining, in the second case by simply
copying the code after the "foo" marker.

>> 1.2. The definition via post-dominance doesn't work either:
>> 
>> I have seen control dependencies being defined in terms of the first
>> basic block that post-dominates the basic block of the if-condition,
>> that is the first basic block control flow must take to reach the
>> function return regardless of what the if condition returned.
>> 
>> E.g. [2] defines control dependencies as follows:
>> 
>>> A statement y is said to be control dependent on another statement x
>>> if (1) there exists a nontrivial path from x to y such that every
>>> statement z != x in the path is post-dominated by y, and (2) x is not
>>> post-dominated by y.
>> 
>> Again, this definition doesn't work for the example above. As the basic
>> block of the if branch trivially post-dominates any other basic block,
>> because it contains the function return.
> 
> Again, not applicable as basic blocks, multiple paths, and so on belong 
> to static analysis.
> 
>> 2. Solution:
>> 
>> The definition I came up with instead is the following:
>> 
>>> A basic block B is control-dependent on a basic block A if
>>> B is reachable from A, but control flow can take a path through A
>>> which avoids B. The scope of a control dependency ends at the first
>>> basic block where all control flow paths running through A meet.
>> 
>> Note that this allows control dependencies to remain "unresolved".

The "unresolved" part in my initial definition was inspired by cases such as
the ones above and the loop example from my previous email, where the
"paths" could be somewhat thought of as executions. But yes, as you said,
that's static analysis and not the position LKMM takes.

Many thanks,
Paul

--
PS replacing "Palmer Dabbelt <palmerdabbelt@google.com>" with "Palmer
Dabbelt <palmer@dabbelt.com>" in recipients - my maintainers file was
outdated.

>> I'm happy to submit a patch which covers more of what I mentioned above
>> as part of explanation.txt, but figured that in the spirit of keeping
>> things simple, leaving out "at all" might be enough?
>> 
>> What do you think?
> 
> Not so good. A better description would be that there is a control 
> dependency from a read event X to a memory access event Y if there is a 
> dependency (data or address) from X to the conditional branch event of 
> an "if" statement which contains Y in one of its arms. And similarly 
> for "switch" statements.
> 
> Alan
> 
>> Many thanks,
>> Paul
>> 
>> [1]: https://lore.kernel.org/all/Yk7%2FT8BJITwz+Og1@Pauls-MacBook-Pro.local/T/#u
>> [2]: Optimizing Compilers for Modern Architectures: A Dependence-Based
>> Approach, Randy Allen, Ken Kennedy, 2002, p. 350
>> 
>> Signed-off-by: Paul Heidekrüger <paul.heidekrueger@in.tum.de>
>> Cc: Marco Elver <elver@google.com>
>> Cc: Charalampos Mainas <charalampos.mainas@gmail.com>
>> Cc: Pramod Bhatotia <pramod.bhatotia@in.tum.de>
>> Cc: Soham Chakraborty <s.s.chakraborty@tudelft.nl>
>> Cc: Martin Fink <martin.fink@in.tum.de>
>> ---
>> tools/memory-model/Documentation/explanation.txt | 2 +-
>> 1 file changed, 1 insertion(+), 1 deletion(-)
>> 
>> diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
>> index ee819a402b69..42af7ed91313 100644
>> --- a/tools/memory-model/Documentation/explanation.txt
>> +++ b/tools/memory-model/Documentation/explanation.txt
>> @@ -466,7 +466,7 @@ 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:
>> +the second event is executed. Simple example:
>> 
>> 	int x, y;
>> 
>> -- 
>> 2.35.1

Re: [PATCH RFC] tools/memory-model: Adjust ctrl dependency definition

[Alan Stern]

On Tue, Jun 21, 2022 at 01:59:27PM +0200, Paul Heidekrüger wrote:
> OK. So, LKMM limits the scope of control dependencies to its arm(s), hence
> there is a control dependency from the last READ_ONCE() before the loop
> exists to the WRITE_ONCE().
> 
> But then what about the following:
> 
> > int *x, *y;
> > 
> > int foo()
> > {
> > 	/* More code */
> > 
> > 	if(READ_ONCE(x))
> > 		return 42;
> > 
> > 	/* More code */
> > 
> > 	WRITE_ONCE(y, 42);
> > 
> > 	/* More code */
> > 
> > 	return 0;
> > }
> 
> The READ_ONCE() determines whether the WRITE_ONCE() will be executed at all,
> but the WRITE_ONCE() doesn't lie in the if condition's arm.

So in this case the LKMM would not recognize that there's a control 
dependency, even though it clearly exists.

>   However, by
> "inverting" the if, we get the following equivalent code:
> 
> > if(!READ_ONCE(x)) {
> > 	/* More code */
> > 
> > 	WRITE_ONCE(y, 42);
> > 
> > 	/* More code */
> > 
> > 	return 0;
> > }
> > 
> > return 42;
> 
> Now, the WRITE_ONCE() is in the if's arm, and there is clearly a control
> dependency.

Correct.

> Similar cases:
> 
> > if(READ_ONCE())
> > 	foo(); /* WRITE_ONCE() in foo() */
> > return 42;
> 
> or
> 
> > if(READ_ONCE())
> >     goto foo; /* WRITE_ONCE() after foo */
> > return 42;
> 
> In both cases, the WRITE_ONCE() again isn't in the if's arm syntactically
> speaking, but again, with rewriting, you can end up with a control
> dependency; in the first case via inlining, in the second case by simply
> copying the code after the "foo" marker.

Again, correct.  The LKMM isn't always consistent, and it behaves this 
way to try to avoid presuming too much about the optimizations that 
compilers may apply.

Alan

Re: [PATCH RFC] tools/memory-model: Adjust ctrl dependency definition

[Paul Heidekrüger]

[-- Attachment #1: Type: text/plain, Size: 2395 bytes --]


> On 21. Jun 2022, at 16:24, Alan Stern <stern@rowland.harvard.edu> wrote:
> 
> On Tue, Jun 21, 2022 at 01:59:27PM +0200, Paul Heidekrüger wrote:
>> OK. So, LKMM limits the scope of control dependencies to its arm(s), hence
>> there is a control dependency from the last READ_ONCE() before the loop
>> exists to the WRITE_ONCE().
>> 
>> But then what about the following:
>> 
>>> int *x, *y;
>>> 
>>> int foo()
>>> {
>>> 	/* More code */
>>> 
>>> 	if(READ_ONCE(x))
>>> 		return 42;
>>> 
>>> 	/* More code */
>>> 
>>> 	WRITE_ONCE(y, 42);
>>> 
>>> 	/* More code */
>>> 
>>> 	return 0;
>>> }
>> 
>> The READ_ONCE() determines whether the WRITE_ONCE() will be executed at all,
>> but the WRITE_ONCE() doesn't lie in the if condition's arm.
> 
> So in this case the LKMM would not recognize that there's a control 
> dependency, even though it clearly exists.

Oh, that's unfortunate.

Then I would still argue that the "at all" definition is misleading. This
time in the other direction as I had initially proposed though, as the above
example is a case where "at all" holds true, but LKMM doesn't cover it. Or
do you think that caveating this in litmus-tests.txt, e.g. via the patch we
had recently worked out [1], is enough?

>>  However, by
>> "inverting" the if, we get the following equivalent code:
>> 
>>> if(!READ_ONCE(x)) {
>>> 	/* More code */
>>> 
>>> 	WRITE_ONCE(y, 42);
>>> 
>>> 	/* More code */
>>> 
>>> 	return 0;
>>> }
>>> 
>>> return 42;
>> 
>> Now, the WRITE_ONCE() is in the if's arm, and there is clearly a control
>> dependency.
> 
> Correct.
> 
>> Similar cases:
>> 
>>> if(READ_ONCE())
>>> 	foo(); /* WRITE_ONCE() in foo() */
>>> return 42;
>> 
>> or
>> 
>>> if(READ_ONCE())
>>>    goto foo; /* WRITE_ONCE() after foo */
>>> return 42;
>> 
>> In both cases, the WRITE_ONCE() again isn't in the if's arm syntactically
>> speaking, but again, with rewriting, you can end up with a control
>> dependency; in the first case via inlining, in the second case by simply
>> copying the code after the "foo" marker.
> 
> Again, correct.  The LKMM isn't always consistent, and it behaves this 
> way to try to avoid presuming too much about the optimizations that 
> compilers may apply.

Many thanks,
Paul

--
[1]: https://lore.kernel.org/all/20220614154812.1870099-1-paul.heidekrueger@in.tum.de/

[-- Attachment #2: smime.p7s --]
[-- Type: application/pkcs7-signature, Size: 5449 bytes --]

Re: [PATCH RFC] tools/memory-model: Adjust ctrl dependency definition

[Alan Stern]

On Mon, Jun 27, 2022 at 11:47:43AM +0200, Paul Heidekrüger wrote:
> 
> > On 21. Jun 2022, at 16:24, Alan Stern <stern@rowland.harvard.edu> wrote:
> > 
> > On Tue, Jun 21, 2022 at 01:59:27PM +0200, Paul Heidekrüger wrote:
> >> OK. So, LKMM limits the scope of control dependencies to its arm(s), hence
> >> there is a control dependency from the last READ_ONCE() before the loop
> >> exists to the WRITE_ONCE().
> >> 
> >> But then what about the following:
> >> 
> >>> int *x, *y;
> >>> 
> >>> int foo()
> >>> {
> >>> 	/* More code */
> >>> 
> >>> 	if(READ_ONCE(x))
> >>> 		return 42;
> >>> 
> >>> 	/* More code */
> >>> 
> >>> 	WRITE_ONCE(y, 42);
> >>> 
> >>> 	/* More code */
> >>> 
> >>> 	return 0;
> >>> }
> >> 
> >> The READ_ONCE() determines whether the WRITE_ONCE() will be executed at all,
> >> but the WRITE_ONCE() doesn't lie in the if condition's arm.
> > 
> > So in this case the LKMM would not recognize that there's a control 
> > dependency, even though it clearly exists.
> 
> Oh, that's unfortunate.
> 
> Then I would still argue that the "at all" definition is misleading. This

I agree, and I would welcome a patch improving the definition.  Perhaps 
something along the lines of what I wrote earlier in this email thread.

> time in the other direction as I had initially proposed though, as the above
> example is a case where "at all" holds true, but LKMM doesn't cover it. Or
> do you think that caveating this in litmus-tests.txt, e.g. via the patch we
> had recently worked out [1], is enough?

No, the explanation should be improved.

Alan

Re: [PATCH RFC] tools/memory-model: Adjust ctrl dependency definition

[Paul Heidekrüger]

Alan Stern <stern@rowland.harvard.edu> wrote:

> On Mon, Jun 27, 2022 at 11:47:43AM +0200, Paul Heidekrüger wrote:
>>> On 21. Jun 2022, at 16:24, Alan Stern <stern@rowland.harvard.edu> wrote:
>>> 
>>> On Tue, Jun 21, 2022 at 01:59:27PM +0200, Paul Heidekrüger wrote:
>>>> OK. So, LKMM limits the scope of control dependencies to its arm(s), hence
>>>> there is a control dependency from the last READ_ONCE() before the loop
>>>> exists to the WRITE_ONCE().
>>>> 
>>>> But then what about the following:
>>>> 
>>>>> int *x, *y;
>>>>> 
>>>>> int foo()
>>>>> {
>>>>> 	/* More code */
>>>>> 
>>>>> 	if(READ_ONCE(x))
>>>>> 		return 42;
>>>>> 
>>>>> 	/* More code */
>>>>> 
>>>>> 	WRITE_ONCE(y, 42);
>>>>> 
>>>>> 	/* More code */
>>>>> 
>>>>> 	return 0;
>>>>> }
>>>> 
>>>> The READ_ONCE() determines whether the WRITE_ONCE() will be executed at all,
>>>> but the WRITE_ONCE() doesn't lie in the if condition's arm.
>>> 
>>> So in this case the LKMM would not recognize that there's a control 
>>> dependency, even though it clearly exists.
>> 
>> Oh, that's unfortunate.
>> 
>> Then I would still argue that the "at all" definition is misleading. This
> 
> I agree, and I would welcome a patch improving the definition. Perhaps 
> something along the lines of what I wrote earlier in this email thread.

I have just been thinking about how to word this patch; am I correct in
assuming that the LKMM does not deal with loop conditions? Or in other
words, there is no way for a loop condition to impose a ctrl dependency on
any WRITE_ONCE's in the loop body? It are only if and switch statements the
LKMM is concerned with in the case of ctrl dependencies?

Many thanks,
Paul

>> time in the other direction as I had initially proposed though, as the above
>> example is a case where "at all" holds true, but LKMM doesn't cover it. Or
>> do you think that caveating this in litmus-tests.txt, e.g. via the patch we
>> had recently worked out [1], is enough?
> 
> No, the explanation should be improved.
> 
> Alan

Re: [PATCH RFC] tools/memory-model: Adjust ctrl dependency definition

[Alan Stern]

On Fri, Jul 15, 2022 at 02:27:28PM +0200, Paul Heidekrüger wrote:
> I have just been thinking about how to word this patch; am I correct in
> assuming that the LKMM does not deal with loop conditions? Or in other
> words, there is no way for a loop condition to impose a ctrl dependency on
> any WRITE_ONCE's in the loop body? It are only if and switch statements the
> LKMM is concerned with in the case of ctrl dependencies?

In theory, the LKMM does say that a loop condition imposes a control 
dependency on any memory accesses within the loop body.  However, the 
herd7 tool has only very limited support for looping constructs, so in 
practice it's not possible to create suitable litmus tests with loops.

Alan

Re: [PATCH RFC] tools/memory-model: Adjust ctrl dependency definition

[Paul E. McKenney]

On Fri, Jul 15, 2022 at 09:27:26AM -0400, Alan Stern wrote:
> On Fri, Jul 15, 2022 at 02:27:28PM +0200, Paul Heidekrüger wrote:
> > I have just been thinking about how to word this patch; am I correct in
> > assuming that the LKMM does not deal with loop conditions? Or in other
> > words, there is no way for a loop condition to impose a ctrl dependency on
> > any WRITE_ONCE's in the loop body? It are only if and switch statements the
> > LKMM is concerned with in the case of ctrl dependencies?
> 
> In theory, the LKMM does say that a loop condition imposes a control 
> dependency on any memory accesses within the loop body.  However, the 
> herd7 tool has only very limited support for looping constructs, so in 
> practice it's not possible to create suitable litmus tests with loops.

And Alan isn't joking.  The closest simulation that I know of is to
combine limited loop unrolling with the "filter" clause.  The point of
the filter clause is to eliminate from consideration executions that
need the more iterations of the loop to be unrolled.

And that means that as far as LKMM is concerned, loop-based control
dependencies are similar to those for nested "if" statements.

							Thanx, Paul

Re: [PATCH RFC] tools/memory-model: Adjust ctrl dependency definition

[Paul Heidekrüger]

Paul E. McKenney <paulmck@kernel.org> wrote:

> On Fri, Jul 15, 2022 at 09:27:26AM -0400, Alan Stern wrote:
>> On Fri, Jul 15, 2022 at 02:27:28PM +0200, Paul Heidekrüger wrote:
>>> I have just been thinking about how to word this patch; am I correct in
>>> assuming that the LKMM does not deal with loop conditions? Or in other
>>> words, there is no way for a loop condition to impose a ctrl dependency on
>>> any WRITE_ONCE's in the loop body? It are only if and switch statements the
>>> LKMM is concerned with in the case of ctrl dependencies?
>> 
>> In theory, the LKMM does say that a loop condition imposes a control 
>> dependency on any memory accesses within the loop body.  However, the 
>> herd7 tool has only very limited support for looping constructs, so in 
>> practice it's not possible to create suitable litmus tests with loops.
> 
> And Alan isn't joking.  The closest simulation that I know of is to
> combine limited loop unrolling with the "filter" clause.  The point of
> the filter clause is to eliminate from consideration executions that
> need the more iterations of the loop to be unrolled.
> 
> And that means that as far as LKMM is concerned, loop-based control
> dependencies are similar to those for nested "if" statements.
> 
> 							Thanx, Paul

Makes sense, thank you both!

Paul