lkml.org 
[lkml]   [2022]   [Jun]   [15]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
Patch in this message
/
From
Subject[PATCH RFC] tools/memory-model: Adjust ctrl dependency definition
Date
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
\
 
 \ /
  Last update: 2022-06-15 13:46    [W:0.065 / U:0.516 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site