[PATCH] D56534: [Verifier] Add verification of unaligned atomic load/store

[Philip Reames via Phabricator via llvm-commits]

reames added a comment.

In D56534#1363586 <https://reviews.llvm.org/D56534#1363586>, @efriedma wrote:

> > I think what we're debating here is the meaning of "unsafe". If "unsafe" is interpreted as "has target defined behaviour", then I completely agree. If "unsafe" is defined as "result is undefined" (in the UB sense), then I strongly disagree.
>
> At the IR level, we often make operations undefined even when the underlying machine operations has some useful semantics, if we can't provide that across all platforms.  For example, float-to-int conversion produces poison on overflow, even though every target with a float-to-int instruction produces some well-defined result.  We don't want to introduce target-specific semantics unless we have to.  So the question is, what's the right tradeoff here?  And if we do decide to distinguish between locked and lock-free operations, how should we represent that?


Again, I would strongly resist any effort to define away overlapping atomics or unaligned atomics.  This works today in practice on common architectures.  We are reliant on this implementation working as it does today for overlapping atomics.  Specifying that away because we happen to not be able to guarantee anything on other platforms is not acceptable.

Now, to be clear, I'm not arguing we can't change *spelling*.  If you want to insist that overlapping atomics be done via intrinsics, I'll still argue with you because I think it's a bad design, but it's not a fundamental non starter like defining away existing target behaviour is.

> I haven't really thought it through completely, but I think if we want to distinguish them in IR, it might make sense to attach a "lockfree" bit to atomic operations where correctness depends on the lock-free semantics.
> 
>> We certainly have precedent for a number of target legality hooks in optimizations already.
> 
> Target hooks don't control the semantics of a given operation.  We use them to determine whether an transform is profitable, or sometimes whether the backend supports emitting a certain operation.  Semantic differences must be encoded directly into the IR; the power of LLVM IR for target-independent optimization is tied to this.  So adding a target hook to check whether a given target supports a certain lock-free operation is fine, but adding a target hook to control whether a certain sequence of atomic operations has defined behavior is not okay.

We certainly do this for library calls, and some intrinsics.  I can't think of an example in the base IR instruction set at the moment, but I really don't see it being that different.

I think this thread has moved beyond the original review and probably needs to be promoted to llvm-dev for a wider audience.  If there are no objections, I vote we close this review as abandoned, and then I'll send a summary email to llvm-dev.


CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D56534/new/

https://reviews.llvm.org/D56534