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

[JF Bastien via Phabricator via llvm-commits]

jfb added a comment.

In D56534#1363988 <https://reviews.llvm.org/D56534#1363988>, @__simt__ wrote:

> With apologies, I would just like to tack a note into this thread that the entire *field* of formal memory model proofs involving partially-overlapping atomics is a single paper (last I knew, https://www.cl.cam.ac.uk/~pes20/popl17/mixed-size.pdf). The paper says mixed-size, but the key point is not-perfectly-overlapping.


Two papers https://arxiv.org/pdf/1801.10140.pdf 😆
Peter's group is doing further work from the JavaScript model for WebAssembly, so soon a whopping *3* papers.

> That one paper uncovered surprising new behaviors that don't exist in programs comprising only aligned atomics of matching sizes for all pairs that conflict. For example, because of this new behavior, the presence of misaligned atomics in a program can invalidate the proof that C++ programs with SC fences between every two atomic operations will admit only SC executions. Risking invalidating that proof supports the notion that they should be declared UB in C++ programs in the general sense (i.e. users definitely should not be writing this), though perhaps not UB on every imaginable back-end after optimizations (an argument you have made, I don't disagree with).
> 
> TL;DR: it's a bit early to declare that misaligned atomics are well-understood & just work, even where they usually fail to astonish.


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

https://reviews.llvm.org/D56534