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

[Tobias Grosser via llvm-commits]

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