TL;DR: Zig should adopt an official memory model. Some options are to use the C/C++ memory model (easy), or its own better memory model (very hard).
(Note that this issue is about the semantics of concurrent access, not other just-as-important things like pointer aliasing rules and provenance. That should also be specified, but it's the job of another issue.)
The problem
The memory model determines which concurrent programs are valid, and is important as the ground truth for what transformations the compiler is allowed to do. Currently, the Zig memory model is by default "whatever LLVM says". It would be nice to have a Zig memory model independent of LLVM. LLVM memory model
This is by no means urgent -- despite being the subject of significant formal verification efforts, Rust still lacks its own memory model, instead defaulting to the C11/C++11 spec.
Here are some reasons to not just stick with LLVM's model:
- The Zig language would be tied to the LLVM release schedule. If LLVM changes what it does in the future, Zig would be forced to either change with it, or implement some kind of backwards compatibility on top of it.
- Other Zig backends (Stage2, as well as any other future backend) are forced to have feature parity with LLVM
- The LLVM memory model is more docs than spec, so it lacks the formalisms that would unambiguously deal with all edge cases. This also has implications for other Stage2/other backends -- if LLVM starts compiling some code in a more conservative way than Stage2, that shouldn't retroactively make Stage2's behavior a bug.
The LLVM memory model also (somewhat necessarily) incorporates a lot of cruft, from C, Java, and probably more -- what could "starting over" with a memory model fix?
-
Reordering of dependent loads is allowed by C/C++ relaxed loads, and maybe by Java non-volatiles (this is unclear to me, maybe someone else can say for sure). LLVM never allows reordering of dependent loads, by simply not supporting the DEC Alpha processor. If Zig is to ever be run on the DEC Alpha, Zig will have to take a stance on this.
-
LLVM doesn't support C/C++ consume operations, which are arguably broken. Instead, Clang changes all consumes to acquires. Consume semantics were introduced for a reason though, so it's worth thinking about how Zig could succeed where the C/C++ standard failed.
-
LLVM has unordered for Java non-volatile, and monotonic for C/C++ relaxed. It also asserts that monotonic is strictly more ordered than unordered. However, C/C++ relaxed allows some things that Java non-volatile doesn't. This section of the Java memory model has an example:
Initially x = 0, y = 0.
| Thread 1 |
Thread 2 |
int tmp1 = x; |
int tmp2 = y; |
if (tmp1 == 1) y = 1; |
if (tmp2 == 1) x = 1; |
Assuming relaxed loads/stores to x and y, C/C++ allows this program to end with x = y = 1, but Java non-volatiles disallow this result. This is largely considered a bug in the C/C++ spec, but (afaik) all fixes are either too restrictive or require significant changes to how the memory model is specified.
Proposed solution
- Start off by officially adopting the C/C++ memory model, minus
consume. (This is what Rust has currently.)
- Introduce
AtomicOrder.Relaxed, which gets translated to LLVM's monotonic, and remove/deprecate AtomicOrder.Unordered and AtomicOrder.Monotonic.
- More importantly, improve the
AtomicOrder docs, including stating that Zig follows the C11/C++11 memory model.
- If
consume is deemed useful in the future, introduce something like consume in a way that fixes the poor C/C++ semantics. This could be implemented by LLVM with acquire, and in a more fine-grained way in Stage2.
- Zig might eventually wish to replace the C/C++ memory model with its own memory model, as it's currently doing with other C infrastructure like libc. This would be very hard, and I don't expect it to happen soon, if ever.
TL;DR: Zig should adopt an official memory model. Some options are to use the C/C++ memory model (easy), or its own better memory model (very hard).
(Note that this issue is about the semantics of concurrent access, not other just-as-important things like pointer aliasing rules and provenance. That should also be specified, but it's the job of another issue.)
The problem
The memory model determines which concurrent programs are valid, and is important as the ground truth for what transformations the compiler is allowed to do. Currently, the Zig memory model is by default "whatever LLVM says". It would be nice to have a Zig memory model independent of LLVM. LLVM memory model
This is by no means urgent -- despite being the subject of significant formal verification efforts, Rust still lacks its own memory model, instead defaulting to the C11/C++11 spec.
Here are some reasons to not just stick with LLVM's model:
The LLVM memory model also (somewhat necessarily) incorporates a lot of cruft, from C, Java, and probably more -- what could "starting over" with a memory model fix?
Reordering of dependent loads is allowed by C/C++
relaxedloads, and maybe by Java non-volatiles (this is unclear to me, maybe someone else can say for sure). LLVM never allows reordering of dependent loads, by simply not supporting the DEC Alpha processor. If Zig is to ever be run on the DEC Alpha, Zig will have to take a stance on this.LLVM doesn't support C/C++
consumeoperations, which are arguably broken. Instead, Clang changes allconsumes toacquires. Consume semantics were introduced for a reason though, so it's worth thinking about how Zig could succeed where the C/C++ standard failed.LLVM has
unorderedfor Java non-volatile, andmonotonicfor C/C++ relaxed. It also asserts thatmonotonicis strictly more ordered thanunordered. However, C/C++ relaxed allows some things that Java non-volatile doesn't. This section of the Java memory model has an example:Initially
x = 0,y = 0.int tmp1 = x;int tmp2 = y;if (tmp1 == 1) y = 1;if (tmp2 == 1) x = 1;Assuming relaxed loads/stores to
xandy, C/C++ allows this program to end withx = y = 1, but Java non-volatiles disallow this result. This is largely considered a bug in the C/C++ spec, but (afaik) all fixes are either too restrictive or require significant changes to how the memory model is specified.Proposed solution
consume. (This is what Rust has currently.)AtomicOrder.Relaxed, which gets translated to LLVM's monotonic, and remove/deprecateAtomicOrder.UnorderedandAtomicOrder.Monotonic.AtomicOrderdocs, including stating that Zig follows the C11/C++11 memory model.consumeis deemed useful in the future, introduce something likeconsumein a way that fixes the poor C/C++ semantics. This could be implemented by LLVM withacquire, and in a more fine-grained way in Stage2.