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:
- 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_cstloads can only read fromseq_cststores. PR #189014 aims to fix this. - 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).
- 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_cstandmonotonicoperations not being able to interact with weaker operations. Such optimizations would break the common programming strategy to start with aseq_cstimplementation 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
poisoninstead ofundef? 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
monotonicoperations 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?
- There is “A value cannot be read unless some operation wrote it.” for
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