<div dir="ltr"><div class="gmail_quote"><div dir="ltr">On Wed, Jun 28, 2017 at 12:42 PM Peter Lawrence <<a href="mailto:peterl95124@sbcglobal.net">peterl95124@sbcglobal.net</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word">Hal,<div>Chandler,</div><div>               Can we get back on topic, IE if you’ve actually read the paper I’d like to </div><div>hear some feedback on its technical content</div></div></blockquote><div><br></div><div>Sure, I was mostly mentioning prior discussion because I don't think this is going to add a lot to the discussion around `nsw` and the `llvm.assume` intrinsic back when Hal and I started discussing modeling assumptions as first class entities in the IR.</div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><div><div><blockquote type="cite"><div><blockquote type="cite" style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255)"><div dir="ltr"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div style="word-wrap:break-word"><div><div><blockquote type="cite"><div><div dir="ltr"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div style="word-wrap:break-word"><div dir="auto" style="word-wrap:break-word"><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><div style="margin:0px;line-height:normal;min-height:16px"><br></div></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">I have been re-reading Dan Gohman's original post "the nsw story" [1]</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">and have come to the conclusion that Dan got it wrong in some respects.</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">He came up with "no signed wrap" ("nsw") which in his words means</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">"The purpose of the nsw flag is to indicate instructions which are</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">known to have no overflow".  The key operative word here is "known".</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">This means literally an operation with an additional "llvm.assume".</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">For example    (a +nsw b)    when a and b are i32   is really</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures"> <span class="m_-2105736059564455628Apple-converted-space"> </span>((llvm.assume((INT_MIN <= ((i64)a+(i64)b) <= INT_MAX) , (a + b))</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">It is this "assume" that justifies the transformation that Dan does</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">to optimize sign-extension of i32 induction variables out of loops</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">on LP64 targets.  So far so good.</span></div></div></div></blockquote></div></div></div></blockquote></div></div></div></blockquote></div></div></blockquote></div></blockquote></div></div></div></blockquote><div><br></div><div>I just want to point out that this isn't complete.</div><div><br></div><div>*Before* an `add nsw` instruction is hoisted, it could be thought of as a normal `add` plus `llvm.assume`. But the `llvm.assume` cannot be hoisted above predicates. So what this would end up doing is allowing the hoisting of the `add` by separating the invariant and keeping the invariant below the predicate. This is a fairly minor point, but I didn't want it to be unstated.</div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><div><blockquote type="cite"><blockquote type="cite" style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255)"><div dir="ltr"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div style="word-wrap:break-word"><div><blockquote type="cite"><div dir="ltr"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div style="word-wrap:break-word"><div dir="auto" style="word-wrap:break-word"><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">Where Dan goes wrong is in thinking that "+nsw" is an operation</span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">rather than an operation with an assume, and therefore he feels</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">the need to define what the result of this operation is when it</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">overflows, which then seems to require a new "poison" instruction</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">because "undef" isn't good enough.</span></div></div></div></blockquote></div></div></blockquote></div></div></blockquote></div></div></blockquote></blockquote></div></div></blockquote><div><br></div><div>A meta comment. I think it would be helpful for you to phrase your discussion in a less personalized way. Rather than talking about "So-and-so went wrong when they thought ...", I would instead merely discuss the situation as it is today. This helps keep the discussion from sliding into inappropriate areas, which has already been a concern, so it seems worth pointing out as a suggestion for future emails.</div><div><br></div><div>To the actual point, it seems backwards to say that we made a mistake in specifying `nsw` as an operation rather than an `assume`. At the time we specified `nsw` there was no such construct as `llvm.assume`. Perhaps introducing `llvm.assume` would have been better than introducing `nsw`, perhaps not. But it doesn't actually matter. This kind of historical critique doesn't seem like a useful way to frame the discussion.</div><div><br></div><div>The point is, we have `llvm.assume` now, and we can and should consider whether it is a better tool for the job. Hopefully I have understood the point you are trying to make?</div><div><br></div><div>My response is that I don't think this is clearly a superior tool for the job. We did actually discuss things like `nsw` when designing `llvm.assume`. One serious issue with `llvm.assume` is that it *cannot be speculated*. Even though we gain the ability to speculate the `add` by decoupling the invariant, we would retain a large amount of IR that could not be speculated and would cause us to retain control flow and be a significant barrier to optimization.</div><div><br></div><div>In fact, `llvm.assume` is *incredibly* expensive already. We talked at length when introducing it about how it should be relatively sparingly used and used with care to provide the most impactful hints to the optimizer rather than trying to encode everything that might possibly be assumed to be true.</div><div><br></div><div>On the flip side, `add nsw` is extremely common in the IR produced by many frontends. So it would seem like a poor fit to use a very expensive and heavyweight tool to represent something that is very common.</div><div><br></div><div>I'm happy to view `add nsw` as an `add` with an implicit `llvm.assume` inside of control flow where the result is "used" (for a complex definition of "used" that should be discussed on the `undef` thread and not here) if that is a useful notional or theoretical model. But the *representation optimization* of `add nsw` still seems quite useful.</div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><div><blockquote type="cite"><blockquote type="cite" style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255)"><div dir="ltr"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div style="word-wrap:break-word"><div><blockquote type="cite"><div dir="ltr"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div style="word-wrap:break-word"><div dir="auto" style="word-wrap:break-word"><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures">It therefore makes no sense to discuss the result of "+nsw" as</span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">ever being either "undef" or "poison", and so the need for "poison"</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">is gone.</span></div></div></div></blockquote></div></div></blockquote></div></div></blockquote></div></div></blockquote></blockquote></div></div></blockquote><div>Note that there have been examples which show that the `undef` semantics alone as used to model reading from uninitialized memory are effectively equivalent to `poison`. So I don't believe that removing `nsw` would necessarily be sufficient here. I think it would also require other changes. And in your emails about `undef` you seem to agree that we would have to change `undef` itself.</div><div><br></div><div>I think it would be more productive to focus on that thread. If we decide to get rid of poison entirely (including changing `undef`), *then* we can have a discussion about how to model `nsw`.</div></div></div>