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

[Michael Kruse via llvm-commits]

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
>