[polly] r264118 - [ScopInfo] Fix domains after loops.

Mon Apr 4 15:50:59 PDT 2016

Still crashing test case with multiple loop exits at:

llvm.org/PR27207

Michael

2016-04-04 16:18 GMT+02:00 Michael Kruse <llvm at meinersbur.de>:
> After a phone discussion will Tobias, we agreed that
>
> Context \cap dom(EntryBB) == Context \cap \bigcup_{E \in LoopExits} dom(E)
>
> is a desirable invariant, even for loop with multiple exits. Since
> r265285 the loop_unroll loop has been fixed and the case not urgent
> anymore. I will try to create a testcase with the same behaviour but
> multiple loop exits that is not handled by r265285 that we can use as
> a basis for another discussion.
>
> Michael
>
>
>
>
> 2016-04-04 14:07 GMT+02:00 Tobias Grosser <tobias at grosser.es>:
>> On 04/04/2016 01:03 PM, Michael Kruse wrote:
>>>
>>> 2016-04-02 0:48 GMT+02:00 Tobias Grosser <tobias at grosser.es>:
>>>>>
>>>>> For the others, count<0 && count2<0 should still be possible, but
>>>>> maybe not supported by Polly.
>>>>
>>>>
>>>>
>>>> I am not sure to understand this sentence. Are you saying our current
>>>> modeling is incorrect for some of the test cases I attached in my last
>>>> email?
>>>
>>>
>>> With "not supported by Polly" I meant some constraints count>=0
>>> count2>0 added to the assumed and checked context.
>>
>>
>> Sorry, I still have issues to parse this sentence. (I understood something,
>> but at this point it seems even details are important).
>>
>> Does this sentence mean you believe some constraints in either the different
>> context sets or the domain are wrong or missing and consequently affect the
>> model of the SCoP in a way that would result in incorrect results to be
>> computed by the program we generate. I believe this is what you are saying,
>> but can you confirm this explicitly?
>>
>>>>> Case A+C remains to be handled even if we add proper assumed context
>>>>> and enforce nsw/nuw flags.
>>>>
>>>>
>>>>
>>>> A+C corresponds to /tmp/loop-succ-cond-4.ll, right? The domain we obtain
>>>> today (without your patch) is:
>>>>
>>>>          [count, count2] -> { Stmt_if_end12[] };
>>>
>>>
>>> loop-succ-cond-4.ll also has B1+B2.
>>
>>
>> So you are saying loop-succ-cond-4.ll is modeled correctly?
>>
>>>> To me this seems correct. It seems you believe that some of the modeling
>>>> is
>>>> currently still incorrect. Could you name the example file I added and
>>>> the
>>>> constraints/conditions that are required to changed to ensure
>>>> _correctness_.
>>>> I am currently not seen where this would be necessary.
>>>
>>>
>>> I think that for each loop
>>>    Context \cap dom(EntryBB) == Context \cap \bigcup_{E \in LoopExits}
>>> dom(E)
>>> is a necessary condition for correctness. Currently Polly does not
>>> have this, as show in unroll_loop.
>>
>>
>> This equality should also include "Assumed Context" and "Invalid Context",
>> which are both used to derive run-time conditions that validate additional
>> context conditions. So the actual context is now
>> something like:
>>
>> Actual Context = Context \cup Assumed Context \cup \complement{Invalid
>> Context}
>>
>> You can see this with:
>>
>> opt -polly-scops -analyze loop-succ-cond-3.ll  -polly-process-unprofitable
>>
>> Here the context is empty, but we have:
>>
>> Invalid Context:
>>     [count, count2] -> {  : count > 0 and count2 <= 0 }
>>
>> which ensures that overall the modeling is still correct (AFAIU).
>>
>>> We can either ensure
>>> 1) dom(EntryBB) == \bigcup_{E \in LoopExits} dom(E)
>>> - or -
>>> 2) that Context excludes all cases where 1) is false.
>>>
>>> My patch tried 1). 2) Is also a viable solution but harder to ensure.
>>
>>
>> I am unsure if you talk about Context or the "Actual Context" I introduced
>> above for this discussion. If you talk about the actual context, then I
>> agree with your two options.
>>
>>> We don't even agree yet what domain/context are supposed to be. Hence
>>> IMHO, maybe even just for robustness, we should do 1) and maybe 2) as
>>> well.
>>
>>
>> I still think we currently don't understand each other fully. We probably
>> should first get a common understanding of the problem, before we decide on
>> the actual solution.
>>
>> As suggested above: can you point to a single .ll file and give a set of
>> input parameter values that are not excluded by the different contexts, for
>> which the polyhedral model is incorrect?
>>
>>>>> In all cases, I think we should add domain lower and upper bound only
>>>>> together and we shouldn't allow ISL to add new contraints when leaving
>>>>> the loop. It might find other contraints in  [p] -> { [i0] : i0 > 0
>>>>> and <contraints found in the loop> }.
>>>>
>>>>
>>>>
>>>> I think it might be good to do what you did in your patch, but before
>>>> moving
>>>> ahead I would like to understand if this is a correctness issue
>>>> or just constraints that we can make simpler.
>>>
>>>
>>> It fixes loop_unroll, so it obviously has to do with correctness ?!?
>>
>>
>> loop_unroll broke because we crash in the code generation as a basic block
>> was removed from the modeling which was required to build exit
>> PHI nodes during code generation. This codegen crash can be prevented by
>> ensuring the relevant ScopArrayInfo object is always generated. (I showed
>> you such patches in Barcelona).
>>
>> Now, to understand if our modeling is correct or not, we need to understand
>> if the generated code results in incorrect execution or not.
>> Specifically, if the set of constraints in Context, Assumed Context and
>> Invalid Context are sufficient to prevent any well-defined execution of
>> the SCoP -- you call this solution 2) above.
>>
>>>> Your example above suggests that you have a correctness issue in mind. As
>>>> said above, do we already have (or can we draft) such a test case?
>>>
>>>
>>> This happens in loop-succ-cond.ll
>>>
>>> Do you have another issue in mind?
>>
>>
>> I think we agreed, loop-succ-cond.ll is correctly modeled just because the
>> zext that is visible. I am currently still under the impression that all
>> other loop-succ-cond-*.ll files are also correctly modeled. I am still
>> looking for a concrete example to convince me otherwise. Is any of these
>> other loop-succ-cond-*.ll incorrectly modeled from your perspective.
>>
>> After this discussion has concluded, I think we should still discuss
>> solution 1), but it is good to understand first if this is a 'correctness'
>> discussion or a modeling improvement not affecting correctness.
>>
>> * By 'incorrect' I always mean here 'modeled in a way that results in
>> incorrect output from the generated program'. This does not mean that
>> the modeling is efficient or should not be improved for other reasons.
>>
>> Best,
>> Tobias
>>