[llvm] [RFC][LangRef] Specify that the accessed bytes of concurrent atomics must be either disjoint or the same (PR #204329)

Ralf Jung via llvm-commits llvm-commits at lists.llvm.org
Tue Jun 30 04:11:41 PDT 2026


================
@@ -3968,13 +3968,20 @@ Given that definition, R\ :sub:`byte` is defined as follows:
    R\ :sub:`byte`, R\ :sub:`byte` returns ``undef`` for that byte.
 -  Otherwise, if R\ :sub:`byte` may see exactly one write,
    R\ :sub:`byte` returns the value written by that write.
--  Otherwise, if R is atomic, and all the writes R\ :sub:`byte` may
-   see are atomic, it chooses one of the values written. See the :ref:`Atomic
+-  Otherwise, if R is atomic, all the writes R\ :sub:`byte` may
+   see are atomic, and R and the writes all access the exact same set of
+   bytes, it chooses one of the values written. See the :ref:`Atomic
----------------
RalfJung wrote:

If the model is indeed meant to be in the style of the C++ model (as a consistency predicate on whole executions, hopefully in a way that it can be defined incrementally [which the C++ model can]), then I am fine -- I just think it'd be good to make that more explicit.

In C++, the data race UB is not part of the consistency predicate. It's a separate "catch-fire" term. I suppose those *can* be adjusted to LLVM's undef-returning semantics, but I don't think I have actually seen this done.

https://github.com/llvm/llvm-project/pull/204329


More information about the llvm-commits mailing list