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

[via llvm-commits]

Author: Fabian Ritter
Date: 2026-07-16T09:58:44+02:00
New Revision: ca6fe413daa538440cf47d4734051e3be7293600

URL: https://github.com/llvm/llvm-project/commit/ca6fe413daa538440cf47d4734051e3be7293600
DIFF: https://github.com/llvm/llvm-project/commit/ca6fe413daa538440cf47d4734051e3be7293600.diff

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

Currently, one could read large parts of the memory model without learning for
sure whether it is meant as an operational model that describes how individual
operations change some notion of state or if it is an axiomatic model (like the
C++ memory model) that lists constraints that a candidate execution must
satisfy to be allowed.

While the description of what a read returns sounds somewhat operational,
aspects like the definition of fence instructions, the monotonic modification
order, and the total order of sequentially consistent operations place it in
the realm of axiomatic models.

This is an attempt to make the nature of the model more explicit (and maybe a
place to discuss the nature of the model), as suggested by RalfJung in the
reviews for #204329.

Added: 
    

Modified: 
    llvm/docs/LangRef.md

Removed: 
    


################################################################################
diff  --git a/llvm/docs/LangRef.md b/llvm/docs/LangRef.md
index f555ca543ffdc..cc3668c95159e 100644
--- a/llvm/docs/LangRef.md
+++ b/llvm/docs/LangRef.md
@@ -4014,6 +4014,10 @@ 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: we consider a set of candidate
+executions where every read can (in principle) read from every write
+to the same location (including "later" writes), and provide constraints that
+reduce this candidate set to the set of actually valid executions.
 
 For a more informal introduction to this model, see the {doc}`Atomics`.