llvm dev - Jun 2021 - [RFC] Introducing a byte type to LLVM

On Tue, Jun 22, 2021 at 11:59 AM Ralf Jung via llvm-dev <
llvm-dev at lists.llvm.org> wrote:
> I don't think it makes sense for LLVM to adopt an explicit
"exposed" flag
> in its
> semantics. Reasoning based on non-determinism works fine, and has the
> advantage
> of keeping ptr-to-int casts a pure, side-effect-free operation. This is
> the
> model we explored in
<https://people.mpi-sws.org/~jung/twinsem/twinsem.pdf>,
> and
> we were able to show quite a few of LLVM's standard optimizations
correct
> formally. Some changes are still needed as you noted, but those changes
> will be
> required anyway even if LLVM were to adopt PNVI-ae:
> - No removal of ptr-int-ptr roundtrips.
> (https://bugs.llvm.org/show_bug.cgi?id=34548)
> - No GVN replacement of pointer-typed values.
> (https://bugs.llvm.org/show_bug.cgi?id=35229)
>
I've read this paper now, and it makes good sense to me as something to
adopt in LLVM.

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.

Has the alternative of allowing type punning through memory at the cost of
removing that optimization been studied sufficiently elsewhere?

Cheers,
Nicolai

-- 
Lerne, wie die Welt wirklich ist,
aber vergiss niemals, wie sie sein sollte.
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20210623/fbd41df9/attachment.html>

On Wed, Jun 23, 2021 at 2:27 PM Nicolai Hähnle <nhaehnle at gmail.com>
wrote:
> On Tue, Jun 22, 2021 at 11:59 AM Ralf Jung via llvm-dev <
> llvm-dev at lists.llvm.org> wrote:
>
>> I don't think it makes sense for LLVM to adopt an explicit
"exposed" flag
>> in its
>> semantics. Reasoning based on non-determinism works fine, and has the
>> advantage
>> of keeping ptr-to-int casts a pure, side-effect-free operation. This is
>> the
>> model we explored in <
>> https://people.mpi-sws.org/~jung/twinsem/twinsem.pdf>, and
>> we were able to show quite a few of LLVM's standard optimizations
correct
>> formally. Some changes are still needed as you noted, but those changes
>> will be
>> required anyway even if LLVM were to adopt PNVI-ae:
>> - No removal of ptr-int-ptr roundtrips.
>> (https://bugs.llvm.org/show_bug.cgi?id=34548)
>> - No GVN replacement of pointer-typed values.
>> (https://bugs.llvm.org/show_bug.cgi?id=35229)
>>
>
> I've read this paper now, and it makes good sense to me as something to
> adopt in LLVM.
>
> 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.
>
> Has the alternative of allowing type punning through memory at the cost of
> removing that optimization been studied sufficiently elsewhere?
>
The transformation is analogous to removing memcpy-like code with the same
dst and src.
Such code might not be written by humans frequently, but I believe C++'s
template instantiation or optimizations like inlining can expose such a
case.

Juneyoung

> Cheers,
> Nicolai
>
> --
> Lerne, wie die Welt wirklich ist,
> aber vergiss niemals, wie sie sein sollte.
>

-- 

Juneyoung Lee
Software Foundation Lab, Seoul National University
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20210623/bab60d49/attachment.html>