The memory model team for the AMDGPU backend has started an attempt to formalize LLVM’s Memory Model for Concurrent Operations in Alloy: GitHub - ROCm/formal-models · GitHub
The idea is to have a general model encoding the target-independent memory model constraints of the LangRef as well as variants with target-specific extensions (e.g., with additional constraints on syncscopes, or supporting relevant target intrinsics).
The formalization is executable in the sense that it allows exploring the possible behaviors of small litmus tests (usually no more than 10-20 instructions, no control flow) in a simplified pseudo-LLVM-IR language (see the README in the repo for how to do that). It also supports proving model properties for bounded settings.
Notable aspects the model does cover:
loads, stores, RMWs, and fence instructions
all atomic memory orderings: unordered, monotonic, acquire, release, acq_rel, seq_cst
syncscope, with simple or complex scope hierarchies
data races that don’t cause immediate UB
Notable aspects the model does not cover (some of these may change in the future):
uninitialized memory
mixed-size, misaligned, or partially overlapping accesses
volatile accesses
aliasing
value computations
control flow
infinite executions and liveness properties
The goal is to have a clear, testable understanding of the memory model, to make it easier to reason about the memory model, to find errors in it, and to extend the LLVM IR language without breaking the model.
The formalization is still a WIP, and the expectation is that it will evolve as LLVM IR evolves. There is certainly also potential for more tooling around it.
Questions for the Community:
Is there community interest in upstreaming this (e.g., to an incubator project), so that the community can develop it together towards an official formal LLVM memory model?
Any feedback regarding the project and the model is welcome.
During the semantics WG call we discussed whether this does anything about out-of-thin-air (the answer is no) and I was asked for some references explaining that issue. I am not sure where to best put those so I will put them here. (I might edit this to add more)
My colleague also pointed me towards https://people.mpi-sws.org/~viktor/papers/oopsla2026-wasm.pdf which has wasm-style “unordered” accesses, which may or may not be the same as LLVM “unordered”. (That paper also uses the simple out-of-thin air fix of saying that po ∪ rf must be acyclic, which rules out load buffering.)
It would be interesting to understand what your model says the possible outcomes are for these two examples from the paper:
All accesses are non-atomic, and let’s say the if(x) are actually if(freeze(x)) to avoid any risk of the program having UB.
The program on the left (CYC) should only have one outcome: a = b = 0. The stores are in dead code and can never execute. It is generally an expected property of these models (known as “DRF theorem”) that if a program is race-free under an SC semantics, then the weaker semantics does not add any new behavior; from that theorem it directly follows that a = b = 0 is the only possible outcome. With my Rust hat on, we definitely don’t want to see any other outcomes for this program.
The program on the right (LB) can actually exhibit a = b = 1 on ARM; that’s classical load buffering. The justification for this in the LLVM world would be that the read in b = Y is racy, so it returns undef/poison, so the program is allowed to enter the if, and then the left thread can read-from the X = 1 on the right.
However, under the usual event-graph-based C++-style memory model, that execution for the right program looks entirely like a valid execution for the left program. I can build a seemingly-valid graph for the left program where a = X reads-from X = 1 and b = Y reads-from Y = 1. This is the classical out-of-thin-air example, except now in a program that doesn’t use any atomics at all! The C++ model satisfies the DRF theorem at least for programs without relaxed accesses because out-of-thin-air only affects relaxed accesses; a model that allows a = b = 1 on this example violates DRF and therefore is significantly less well-behaved than the already problematic C++ model. To avoid this, the LLVM semantics paper uses heavy machinery (event structures). I wonder if your model also somehow avoids this, or if your model allows a = b = 1 on the left program?
tl;dr: The bad outcome for CYC, a = b = 1, is currently allowed in the model.
Conditionals are not represented in the model, it only talks about linear sequences of instruction instances per thread. The way to check this with the model would be to enumerate the possible instruction instance sequence sets according to the sequential semantics and check each if it is allowed by the memory model. For the CYC example, we’d therefore (among others) run this through the memory model:
#thread 0
L1: load X
S1: store Y
#thread 1
L2: load Y
S2: store X
For this, the the memory model says that L1 and L2 must both read undef, because they are part of a data race. Without freeze in the condition, that would mean that the execution triggers immediate UB. With freeze, it means that the a = b = 1 outcome is allowed.
I’d say that this is not only a problem of this formulation of LLVM’s memory model, but of LLVM’s memory model in general. I have some vague ideas how this might be addressed in the Alloy model, but I’ll have to think some more about it. The spec text will need to mirror such changes as well, though.
When you say that “The C++ model satisfies the DRF theorem at least for programs without relaxed accesses because out-of-thin-air only affects relaxed accesses[…]”, you refer to C++'s “visible side effect” rule (intro.races-9 and Note 10), right?
It’s somewhat counter-intuitive, that turning non-atomic accesses into atomic ones would allow more behaviors in the program.
Given that the equivalent C++ code does not allow this outcome, this means we cannot make the model official. (If we did, we’d say that clang is buggy for generating the “obvious” LLVM IR from the equivalent C++ code.)
I don’t know what you mean by “LLVM’s memory model in general”. There is no agreement on what exactly that model is, that’s the entire problem.
But let me go over which models I am aware of that give the desired semantics to CYC:
The simplest approach is to say that po+rf must be acyclic. However, that disallows a = b = 1 on LB, which is bad news as we certainly don’t want to change how that program compiles. That program has no atomic operations! We’d be pessimizing regular non-atomic loads or stores, which is clearly not acceptable. So while maybe on can defend “po+rf must be acyclic” as a possible approach on the C++/Rust level (that’s the RC11 memory model, essentially), it’s clearly not a practical approach for LLVM. Bummer.
The paper mentioned above presents an approach based on event structures. They can compile to PowerPC in the expected way, so chances are the same is true for ARM as both architectures have load buffering. However, event structures didn’t really catch on due to how complicated they are. Also that paper does not have relaxed accesses (let alone unordered) so it’s unclear how well it would extend to all of LLM.
And finally there is the latest iteration on the line of work on Promising Semantics. Their IR semantics has LLVM-style data races and it fully avoids out-of-thin-air (it even lets source languages use RC11). However, they don’t have SC accesses nor unordered accesses. (Earlier iterations of their work had “plain” accesses which are very close to LLVM “unordered” accesses, so it’s possible those could be added back. But SC accesses are surprisingly tricky to deal with once you allow mixing SC and non-SC atomic operations on the same locations.) Also, their model does require backend lowering changes – much less than “po+rf must be acyclic”, but without better hardware support, relaxed stores would get a lot more expensive.
No, I did not talk about visible side-effects at all. I don’t understand what you mean.
All I said is that if you take a C++ program that does not use relaxed accesses, and you run it under SC semantics (i.e. you just interleave individual steps of each thread while everyone works on a global view of memory), and in all SC executions the program has no race conditions (not just no data races, but no races at all), then the program will have the same behavior under the SC semantics and the full weak C++ semantics.
There’s a variant of this where, if you take a C++ program where all atomic accesses are SC, then it doesn’t matter whether you use simple SC semantics or the full weak memory model. You get the same behaviors either way. That’s also an important theorem, it means people can fully “opt-out” of all the weak memory nonsense if they are willing to make all atomic accesses SC.
Both of those are properties Rust and C++ want to hold, and both are violated by the proposed LLVM model.
It’s somewhat counter-intuitive, that turning non-atomic accesses into atomic ones would allow more behaviors in the program.
I don’t think that is the case in any of the academic models (as in, they all allow turning non-atomic into atomic). C++ generally does not allow just changing a non-atomic access into an atomic one, you have to use atomic_ref and then that has special and strange rules (it is UB if one thread reads via atomic_ref and another thread does a normal read at the same time). I think that’s just a C++ idiosyncrasy caused by their very typed view of memory. In Rust, it is always fine to replace a non-atomic access by an atomic one.
(I might edit this to add more)
