<div dir="ltr"><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Jun 22, 2021 at 11:59 AM Ralf Jung via llvm-dev <<a href="mailto:llvm-dev@lists.llvm.org">llvm-dev@lists.llvm.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">I don't think it makes sense for LLVM to adopt an explicit "exposed" flag in its <br>
semantics. Reasoning based on non-determinism works fine, and has the advantage <br>
of keeping ptr-to-int casts a pure, side-effect-free operation. This is the <br>
model we explored in <<a href="https://people.mpi-sws.org/~jung/twinsem/twinsem.pdf" rel="noreferrer" target="_blank">https://people.mpi-sws.org/~jung/twinsem/twinsem.pdf</a>>, and <br>
we were able to show quite a few of LLVM's standard optimizations correct <br>
formally. Some changes are still needed as you noted, but those changes will be <br>
required anyway even if LLVM were to adopt PNVI-ae:<br>
- No removal of ptr-int-ptr roundtrips. <br>
(<a href="https://bugs.llvm.org/show_bug.cgi?id=34548" rel="noreferrer" target="_blank">https://bugs.llvm.org/show_bug.cgi?id=34548</a>)<br>
- No GVN replacement of pointer-typed values. <br>
(<a href="https://bugs.llvm.org/show_bug.cgi?id=35229" rel="noreferrer" target="_blank">https://bugs.llvm.org/show_bug.cgi?id=35229</a>)<br></blockquote><div><br></div><div>I've read this paper now, and it makes good sense to me as something to adopt in LLVM.</div><div><br></div><div>I do have one question about a point that doesn't seem sufficiently justified, though. In the semantics of the paper, store-pointer-then-load-as-integer results in poison. This seems to be the root cause for being forced to introduce a "byte" type for correctness, but it is only really justified by an optimization that eliminates a store that writes back a previously loaded value. That optimization doesn't seem all that important (but feel free to point out why it is...), while introducing a "byte" type is a massive change. On the face of it, that doesn't seem like a good trade-off to me.<br></div><div><br></div><div>Has the alternative of allowing type punning through memory at the cost of removing that optimization been studied sufficiently elsewhere?</div><div><br></div><div>Cheers,</div><div>Nicolai<br></div></div><br>-- <br><div dir="ltr" class="gmail_signature">Lerne, wie die Welt wirklich ist,<br>aber vergiss niemals, wie sie sein sollte.</div></div>