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

Mon Apr 4 02:55:06 PDT 2016

On 04/02, Tobias Grosser wrote:
> On 04/01/2016 03:04 PM, Michael Kruse wrote:
> >Sorry for my absence in the discussion.
> >
> >
> >Thanks Tobias for his analysis. In some details it can be improved.
> >Lets give the changes to the test case a letter:
> >
> >
> >A: Make %count and %0/%count2 independent by removing the zext.
I will assume you now have two independent inputs/arguments. If that is
wrong my comments might be too.

> >B1: Remove nuw in induction variable increment
This should not make a difference in Polly except if ScalarEvolution
can use nuw somehow to provide an nsw flag for SCEVs.

> >B2: Remove nsw in induction variable increment

> >C: Use sge instead of eq in loop exit condition
> >
> >In plain loop-succ-cond.ll (and wtih/without any B,C), there is
> >neither undefined behaviour nor an infinite loop.
And I still think there is no problem [for us].

> > ScEv might know, but
> >not Polly. This can cause another set of problems.
If ScalarEvolution knows that there is no infinite loop we should to :)
We check all SCEVAddRec expressions for a given loop before we try to
come up with the unbounded assumptions. If there is an SCEVAddRec marked
as nsw we know the loop will not be infinite [assuming the step is not
equal to 0].

> >With A and count2<0 (>= 2^61 as unsigned) we have undefined behaviour.
> >indvar will eventually hit the nsw limit (2^61-1). One possible effect
> >of undefined behaviour is an infinite loop.
With the nsw flag for the induction variable, two independent inputs (A)
and signed(count2) < 0, I agree that the behaviour is undefined. Thus,
there is no problem here either.

> >With A+B1 and count2<0 as before, because we hit the nsw first.
True.

> >With A+B2, we have completely defined behaviour. indvar will iterate
> >through 0..2^61-1 and eventually be equal to count to in the range
> >2^61..2^62-1
The behaviour is different but so is our invalid context:
    Invalid Context:
        [count, count2] -> {  : count > 0 and count2 <= 0 }
Which precisely captures what should not happen as it is defined but not
represented this way in the SCoP.

> >With A+C (with/without any B) and count2<0  the loop body is executed
> >exactly once because 0 (+1) is greater than any negative count2.
This is fine and modeled correctly or am I missing something?

> >In summary, we have no infinite loop in any case. Any analysis
> >including ScalarEvolution and Polly can assume that undefined
> >behaviour does not occur. ScEv can give us a trip count when it sees
> >the nsw flag.
Actually, for all version I tried now [basically the variations of
loop-succ-cond you describe] I only saw finite loop restrictions (or any
assumptions for that matter) in the case where the induction variable
can actually wrap around. While we call it "finite loop restriction" it
is actually more of a "indvar does not wrap" restriction, thus it seems
to do exactly what it was designed to do.

> >For the cases that trigger undefined behaviour (A [+B1]), we might
> >want to add count2>=1 to the assumption context.  Not sure why this
> >isn't done yet.
> 
> Right. This could be added. I suggest to keep this in mind and to look again
> into this after having resolved the actual bug we see.
I don't see the need for such an assumption, the behaviour is [as you
said] undefined. We actually had those assumptions initially and they
caused a lot of unnecessary runtime checks. That was the reason we
started to look for SCEVAddRec with nsw flags [see above].

> >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?
I tried all variations of the test case and I followed the analyses of
both of you, however I never encountered a SCoP that was not
representing the semantics of the underlying IR.

> > Shouldn't Polly reject loops without nsw
> >flag?
> 
> No, we do not need to reject them. Polly assumes that all loops are finite
> (do not wrap) and generates constraints (and as a result run-time checks),
> that verify this assumption dynamically. For loop-succ-cond-3.ll we would
> get a wrapping loop in case 'count > 0 and count2 <= 0'. This condition is
> added by Polly to the 'Invalid Context',
> and is verified to not hold before entering the scop at run-time.
True.

> >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[] };
> 
> 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.
That sounds like a good plan.

> >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.
There are different things here.
  1) Adding lower and upper bounds only together is not as simple as
     there is no single "lower" and "upper" bound but only pieces which
     cannot be looked up somewhere.
  2) I agree that we might not want to keep constraints from inside a
     loop but I am not even sure about it. Since I don't think we have
     a correctness issue either way I would like to go forward only with
     a motivating example that profits from this.

> 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?
> 
> > D18450 cannot help when the loop
> >has multiple exits.
> 
> Agreed. And for whatever reason it also did not fix the bug we see on LNT.
That statement is not helping. AFAIK, there is little evidence that the
additional constraints cause the lnt failure. From what I understand,
the additional constrains prevent us from statically dropping the SCoP,
thus it mainly will hide bugs in all parts after the ScopInfo.

Cheers,
  Johannes

-- 

Johannes Doerfert
Researcher / PhD Student

Compiler Design Lab (Prof. Hack)
Saarland University, Computer Science
Building E1.3, Room 4.31

Tel. +49 (0)681 302-57521 : doerfert at cs.uni-saarland.de
Fax. +49 (0)681 302-3065  : http://www.cdl.uni-saarland.de/people/doerfert
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 213 bytes
Desc: Digital signature
URL: <http://lists.llvm.org/pipermail/llvm-commits/attachments/20160404/0fdb8ee6/attachment.sig>