[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