llvm dev - Jul 2015 - [LLVMdev] Strong post-dominance in LLVM?

There is PostDominatorTree for determining post-dominance. Even if A
post-dominates B and B is executed, that doesn't guarantee that A will be
executed. For example, there could be an infinite loop in-between. Strong
post-dominance makes the stronger guarantee that there will be no infinite
loop from B to A. Do we have anything in LLVM for determining strong
post-dominance and in general for guaranteeing that if B is executed, then
A will also be executed?

Bjarke
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20150708/ac55c312/attachment.html>

Hi Bjarke,

Forgive my naivety, but wouldn't that involve solving the halting problem?

Cheers,

James

On Thu, 9 Jul 2015 at 02:21 Bjarke Roune <broune at google.com> wrote:
> There is PostDominatorTree for determining post-dominance. Even if A
> post-dominates B and B is executed, that doesn't guarantee that A will
be
> executed. For example, there could be an infinite loop in-between. Strong
> post-dominance makes the stronger guarantee that there will be no infinite
> loop from B to A. Do we have anything in LLVM for determining strong
> post-dominance and in general for guaranteeing that if B is executed, then
> A will also be executed?
>
> Bjarke
> _______________________________________________
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20150709/2b0e1461/attachment.html>

Hi James, Bjarke,
>
> Forgive my naivety, but wouldn't that involve solving the halting
problem?
>
> Strong post-dominance does not state anything about the termination of
loops. If A strongly post-dominates B, then A is executed iff B is
executed. The inverse is not true, however. So if A doesn't strongly
post-dominates B, A may or may not be executed after B. I.e., to prove
strong post-dominance between A and B, you need to prove termination of all
loops along the paths from B to A.

Do we have anything in LLVM for determining strong post-dominance and
in
>> general for guaranteeing that if B is executed, then A will also be
>> executed?
>>
>> To my knowledge, this feature is currently not available.
Best,
Philip
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20150709/b753c2a4/attachment.html>

On Thu, Jul 9, 2015 at 12:42 AM, James Molloy <james at jamesmolloy.co.uk>
 wrote:
> Forgive my naivety, but wouldn't that involve solving the halting
problem?
>
> If I had to have the exact right answer for every input, then yes. If you
allow a return value of "I don't know" for some inputs, then you
can solve
the halting problem trivially by always returning "I don't know".
Better
solutions return "I don't know" on a smaller subset of the inputs.
That the
halting problem is undecidable then just means that all correct solutions
must return "I don't know" for some inputs.

Bjarke

On Thu, Jul 9, 2015 at 12:42 AM, James Molloy <james at jamesmolloy.co.uk>
wrote:
> Hi Bjarke,
>
> Forgive my naivety, but wouldn't that involve solving the halting
problem?
>
> Cheers,
>
> James
>
> On Thu, 9 Jul 2015 at 02:21 Bjarke Roune <broune at google.com>
wrote:
>
>> There is PostDominatorTree for determining post-dominance. Even if A
>> post-dominates B and B is executed, that doesn't guarantee that A
will be
>> executed. For example, there could be an infinite loop in-between.
Strong
>> post-dominance makes the stronger guarantee that there will be no
infinite
>> loop from B to A. Do we have anything in LLVM for determining strong
>> post-dominance and in general for guaranteeing that if B is executed,
then
>> A will also be executed?
>>
>> Bjarke
>> _______________________________________________
>> LLVM Developers mailing list
>> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
>> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20150709/a393170c/attachment.html>

On Wed, Jul 8, 2015 at 6:01 PM, Bjarke Roune <broune at google.com>
wrote:
> There is PostDominatorTree for determining post-dominance. Even if A
> post-dominates B and B is executed, that doesn't guarantee that A will
be
> executed. For example, there could be an infinite loop in-between. Strong
> post-dominance makes the stronger guarantee that there will be no infinite
> loop from B to A. Do we have anything in LLVM for determining strong
> post-dominance and in general for guaranteeing that if B is executed, then
A
> will also be executed?
The closest thing to this I can think of is `isGuaranteedToExecute` in
LICM.cpp.  Perhaps that mechanism can be generalized?
>
> Bjarke
>
> _______________________________________________
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
>

On Thu, Jul 9, 2015 at 12:15 PM, Sanjoy Das <sanjoy at
playingwithpointers.com>
wrote:
> On Wed, Jul 8, 2015 at 6:01 PM, Bjarke Roune <broune at google.com>
wrote:
> > There is PostDominatorTree for determining post-dominance. Even if A
> > post-dominates B and B is executed, that doesn't guarantee that A
will be
> > executed. For example, there could be an infinite loop in-between.
Strong
> > post-dominance makes the stronger guarantee that there will be no
> infinite
> > loop from B to A. Do we have anything in LLVM for determining strong
> > post-dominance and in general for guaranteeing that if B is executed,
> then A
> > will also be executed?
>
> The closest thing to this I can think of is `isGuaranteedToExecute` in
> LICM.cpp.  Perhaps that mechanism can be generalized?
>
> Thanks. I took a look at it. It does not appear to take into account
nested infinite loops, yet it uses this function to hoist trapping
instructions. I also don't think that it works correctly if the loop itself
iterates infinitely but does have exit blocks in the CFG. I think this
function is based on the assumption that all loops terminate, but I don't
see where LICM checks that. I'm about to file a bug for that and see if I
can trigger it in an example, but feel free to save me the effort if you
know some reason that what it's doing is OK?

Bjarke
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20150709/205799ce/attachment.html>