[RFC] Clarifying LLVM IR's concurrent memory model

Overview & Motivation

I’m proposing several adjustments to the Language Reference concerning the memory model for concurrent operations and atomic memory ordering constraints.
The intention is not to change the de-facto semantics of LLVM IR, it’s to make the LangRef more aligned with it.

Specifically:

  1. Currently, the behavior of operations with monotonic and sequentially consistent memory orderings are only specified relative to operations with the same memory ordering. For example, strictly read, the LangRef suggests that seq_cst loads can only read from seq_cst stores. PR #189014 aims to fix this.
  2. Usually in scoped memory models (like the hrf models, the HSA memory model, or the CUDA memory model), atomics without compatible syncscope (for a target-specific definition of “compatible”) cause data races. PR #189015 lets targets specify that this is possible (and specifies that that’s the case for AMDGPU).
  3. As a consequence of the previous point, if atomics without compatible syncscope can even cause data races, there is no point in requiring them to be ordered in a specific way by the monotonic modification order or the total order of sequentially consistent operations. PR #189017 aims to address this.

The motivation for fixing these problems is to make it easier to argue about the behavior of concurrent LLVM IR programs in a formal way.

Affected Components

  • Point 1 should only disallow optimizations and lowerings that rely on seq_cst and monotonic operations not being able to interact with weaker operations. Such optimizations would break the common programming strategy to start with a seq_cst implementation and relax individual operations as required for performance.
  • Point 2 means that frontends and optimizations can no longer assume that atomics never race (unless only compatible syncscopes are used). I’m not aware of a frontend that uses scopes non-trivially but relies on incompatibly-scoped atomics to not race (note that data races in LLVM IR are not immediate UB, racy loads only return undef).
  • I’m not aware of a case where the change in point 3 would affect the observable behavior.

Open Questions

I’m aware of a few more potential issues with this part of the LangRef that these PRs don’t address:

  • Should racing loads return poison instead of undef? There has been an inconclusive previous discussion on this topic.
  • Currently, a non-atomic load that “may see” only two atomic stores that happen-before it returns undef (see example below), which seems surprising to me. Is that intentional?
  • As far as I can see, there is no strong foundation in the LangRef to ensure that atomics actually behave atomically (i.e., if you have two atomic stores W1, W2 happening-before an atomic load R, R cannot read some bytes that W2 also writes from W1 and some bytes that W1 also writes from W2.)
    • There is “A value cannot be read unless some operation wrote it.” for unordered, but it’s not clear to me how this formally interacts with atomics with different access sizes and/or that overlap.
    • There is also “there is a single total order for modifications by monotonic operations on each address”, but it’s also not obvious how this interacts with partially overlapping operations: Are there separate modification orders for each addressable byte, and a pair of stores must be ordered the same way in every modification order they both participate in?

Example: Two atomic stores that happen-before a non-atomic load are currently a data race.

; thread 0:
  store atomic i32 1, ptr %p monotonic, align 4
  store atomic i32 1, ptr %flag_p release, align 4

; thread 1:
  store atomic i32 2, ptr %p monotonic, align 4
  %f = load atomic i32, ptr %flag_p acquire, align 4
  ; ... ensure that %f reads from the release store, which establishes a happens-before relation
  load i32, ptr %p  ; reads undef, because it is non-atomic and it may see two stores.

I’d appreciate feedback and reviews for the proposed changes and discussion on the open questions. Thanks!

CC @ssahasra @Pierre-vh @nhaehnle ; @jyknight @efriedma-quic for awareness

1 Like

Can you elaborate on how/where this relaxation helps? It does feel like it’s directionally the right thing to do, since different syncscope instances should really be separate from each other, and it’s weird if they become entangled by a per-address but global-for-all-scope-instances modification order. But it would be nice to have a slightly more concrete argument in favor.

4 years later I’d still vote “yes” :slight_smile:

This is an interesting corner case.

I spent a bit of time trying to think through this case in Vulkan’s memory model, and I suspect that that may be buggy as well. It seems that something like this case was considered, since there is a note in the section on Scoped Modification Order:

It is valid to have non-atomic operations or atomics in a different scope instance to the same set of memory locations, as long as they are synchronized against each other as if they were non-atomic (if they are not, it is treated as a data race). That means this definition of A’s scoped modification order could include atomic operations that occur much later, after intervening non-atomics. That is a bit non-intuitive, but it helps to keep this definition simple and non-circular.

Unfortunately, I don’t believe notes are meant to be normative, and it is not clear to me whether the particular corner case you highlighted becomes a data race or not:

; A, B, C are executed by different threads.
; A happens-before C
; B happens-before C
; A and B are mutually ordered atomics (they execute in each other's syncscopes)
; Assume no happens-before relation between A and B
; Assume availability/visible operations from A to C and from B to C, i.e. they're location-ordered.
(A) store atomic %p monotonic
(B) store atomic %p monotonic
(C) load %p

If we did treat all the instruction as non-atomic, then it’d be fairly natural to say that there is a data race.

However, in the Vulkan memory model:

  • The conditions for a Data Race (as defined in that section) don’t seem to be satisfied. A and B are mutually ordered, so the only source for a data race could be the pairs A/C and B/C. But those pairs are location-ordered, so there is no data race.
  • A is visible-to C (per the Visible-To section) because A is location-ordered before C and there is no other write that is location-ordered against A; but by the same argument, B is visible-to C, and so C reads the values written by both A and B, which is clearly not possible and so this seems like it may be a bug in that memory model?

It does seem intuitively plausible that a memory location could be used atomically and then later non-atomically, and that any atomic writes would “settle” to a well-defined final value that can be read non-atomically (based on modification order).

I wonder whether there are any architectures with weak memory models that would have difficulties implementing such a model. It would have to be an architecture that implements monotonic atomic loads differently from non-atomic loads.

cc @RalfJung

So far, I haven’t found a case where this would make an observable difference. My investigation was mostly limited to “compatible scopes = inclusive scopes”, like AMDGPU specifies it. For that, all my searches for examples ended like this:

  • Assume we have two monotonic stores W1 and W2 to the same location that are not required to be modification-ordered because their scopes are not compatible.
  • Further assume that there are two pairs of monotonic reads R1A, R2A (program-ordered like that in a thread A) and R1B, R2B (program-ordered like that in a thread B) and that they “may see” both W1 and W2, so that they could observe them in different orders.
  • That means that every read may see writes with incompatible scopes, so all of them return undef due to data races anyway.

The same should apply for the order of sequentially consistent operations.
So I don’t have a better argument than “different syncscope instances should really be separate from each other, and it’s weird if they become entangled by a per-address but global-for-all-scope-instances modification order”, as you put it.

I can add one more data point on why I don’t think this is a problem if you’re only looking at C/C++ code: There, atomic operations happen (pretty much [1]) if and only if you are working with an atomic type; so if you are mixing atomic and non-atomic operations to the same memory object, you are accessing it with incompatible types, which is a violation of strict aliasing, i.e., UB. In my opinion, that shouldn’t hold as a justification for the LLVM IR semantics, though.


[1] C++'s std::atomic_ref is a strange exception to that

For which part exactly? :slight_smile:
I know nothing about GPU memory models, so I will refrain from commenting on them.

For a compiler-friendly semantics of the various ordering modes, the by-far best-understood model is the C++ memory model. It is the only model I am aware of that admits the kinds of optimizations a backend like LLVM performs. See this paper for a modern presentation of a model in that style – however, there are subtle differences between that model and what is written in the C++ standard, some of which are mistakes in the standard and some (specifically the out-of-thin-air problem) are unresolved issues where no model has been found yet that serves both the interests of programmers (who want to have basic guarantees like causality, ensuring the compiler does not just make up values “out of thin air”) and compilers (who want to generate efficient code without fences for architectures like ARM that allow load buffering, which quickly defies basic reasoning principles).

The LLVM Model in its current form is way too underspecified so it cannot be rigorously studied the way the C++ memory model is being studied. My recommendation would be to take something like https://plv.mpi-sws.org/scfix/paper.pdf without the “NO-THIN-AIR” rule as starting point.

The main departure from that model in LLVM that I am aware of is the desire to make data races not UB. For read-write races, that seems to be complicated but possible (though I am not aware of work framing this in a C++-style graph-based model). For write-write races, the documentation is unclear. I have previously been told that the intent is for that to cause the affected memory to become poison/undef. To my knowledge, nobody ever rigorously defined any model with that property, let alone checked even basic consistency and correctness properties for such a model.

Memory doesn’t actually have a state in those memory models though, does it? Instead, it’s all expressed in terms of “which store does a load read from (if any)”. So that sentence isn’t exactly meaningful.

In LLVM (under-specified as it is), my understanding is that store-store races are not UB, but they may lead to loads returning undef.

And, now that I’m thinking this through, are we really okay with that? My intuitive understanding of the memory model has always been that if we see a non-atomic store to a location L, we could (as an optimization that avoids spilling to stack) safely re-materialize the stored value by loading from L in the region of code after the store but before any other potentially synchronizing instruction.

Is that not actually true? Is that not an optimization we’d like to have? Actually, I do have a use case where I want this optimization, though it’s not currently in upstream LLVM…

Edit: FWIW, the Vulkan memory model does explicitly make this a Data Race and therefore allows this optimization.

Indeed. I was just rephrasing what I was told a while ago in some LLVM issue. It should be rephrased in terms of which values can be returned by which loads, as you suggested.

Good point! That is indeed not a valid optimization under the sketched LLVM semantics. Does LLVM not do this optimization?

TBH this makes me lean rather strongly towards saying LLVM should use a more standard model and make store-store races UB.

Doesn’t this mean it is illegal to compile LLVM IR to Vulkan since well-defined LLVM IR programs may compile to Vulkan programs with UB? Is that a problem for the SPIR-V backend?

EDIT: Though for this even read-write races of being UB is a problem.

cc @efriedma-quic

For context, LLVM’s “atomic memory model” description was initially submitted by me, with some help (I think someone else wrote the original draft, but I forget who). At the time, I did not appreciate the full complexity of the C++ memory model. So it’s unintentionally inconsistent with the C++ memory model in some of the finer details.

The intended semantics are basically just the C++ memory model, translated into a context where C++ objects don’t exist. The one significant intentional deviation is speculated loads: we need such loads to return undef/poison, instead of being instant UB, to justify hoisting loads based on dereferenceability. Any other deviations are unintentional, as far as I know.

I haven’t thought through the implications of changing racing loads from undef to poison.

I don’t recall any discussion of non-atomic write-write races which aren’t observed by a read in the past. I don’t think we intentionally made it defined, we just didn’t take the time to specify anything about it. I don’t think there are really any practical effects for transforms LLVM currently implements.

4 Likes

On the question of store-store races, I’ll point out that there is strong interest from the WebGPU community to be able to translate shaders in a way that guarantees the absence of UB (for security).

There’s some leeway in how we achieve this goal. For example, it may be sufficient if unordered atomics are always defined and we steer the WebGPU frontends down that path. (I haven’t had the chance to think through the implications for performance.) The point is to allow frontends to choose what behavior they require.

IMO much like arithmatic, the burden of choosing semantics needs to be on the front end. There is no single set of semantics that all languages can or should be expected to agree upon. Always choosing atomic (relaxed) stores is a totally reasonable choice for a front end to make.

Interesting, thanks for the clarification. I was under the impression that the deviation on stores was also intentional.