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

[Ralf Jung via llvm-commits]

================
@@ -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.
----------------
RalfJung wrote:

Happy do add "to the same location" to my suggestion. The main point I felt was worth mentioning explicitly is that there is no constraint of causality in this candidate selection phase.

(This has non-trivial ramifications since we also have UB, so one could use non-causal nonsense to read a bad value, have that cause UB, and then use that UB to justify the existence of a write that explains the initial read. But that's a fundamental problem of these kinds of models -- we actually *need* something kind of operational. Most models have a nice acyclic order one can use to build candidates incrementally, but the C++ model allows too many cycles. This relates to the out-of-thin-air problem and the fundamental brokenness of the C++ model.)

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