[llvm] [LangRef] State that the memory model is an axiomatic one (PR #208710)

Fabian Ritter via llvm-commits llvm-commits at lists.llvm.org
Mon Jul 13 06:51:43 PDT 2026


================
@@ -4014,6 +4014,8 @@ The LLVM IR does not define any way to start parallel threads of
 execution or to register signal handlers. Nonetheless, there are
 platform-specific ways to create them, and we define LLVM IR's behavior
 in their presence. This model is inspired by the C++ memory model.
+The memory model is defined axiomatically: it provides constraints that valid
+executions of multi-threaded LLVM IR programs must satisfy.
----------------
ritter-x2a wrote:

> This might be a bit too general. The so called "candidate executions" still require that reads and write access the same memory location. This is not imposed by the memory model constraints, but rather by the semantics of the read-from relation.

We do provide a constraint for that later in the section, though: "For each byte of a read R, Rbyte may see any write to the same byte[...]"

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


More information about the llvm-commits mailing list