Zig: Adopt a Zig Memory Model

Created on 23 Sep 2020  路  2Comments  路  Source: ziglang/zig

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.
proposal

Most helpful comment

I've also extensively tried to wrap my head around memory models, so I'll try to partake in the discussion when it eventually happens.
Just a couple of quick notes for the interested:

  • Different memory orders (or "AtomicOrder") are a high-level way of reasoning which CPU instructions to use; a more-strictly-defined order means you get more guarantees ("sane behaviour"), but need stronger fencing (and less optimizations through reordering). Consume wasn't "broken" conceptually (IIUC), but it didn't end up mapping to the set of instructions (on older-generation ARM targets I think?) it was designed for - compilers incorrectly assuming so had a broken implementation.
  • The C/C++11 model is sort of the 'best attempt' at an efficient abstraction so far, but it is not (yet?) bullet-proof due to "out-of-thin-air" behaviour. Since its inception, dozens of papers have been published trying to rectify this, most of them incur stronger ordering/costs. The newest most promising one seems to address all issues without penalty, and hasn't been disproved for now. Summary, Presentation, Paper
  • The C/C++11 model turns programs with race conditions wholly-undefined. One sweeping solution is to "localize" their effects, which is done by the "Multicore OCaml" memory model (Paper, Implementation with doc comment); they essentially have to disallow certain optimizations, and use fencing store instructions where concurrent access can occur (or might have occured).
  • (race conditions cont.) While undefined behaviour is a bad fit for Zig, ReleaseFast will probably not want to forfeit optimizations, and I think it's generally difficult to transition from a "safer" model, unless we can provide some runtime detection (for Debug / ReleaseSafe, which I've read is a non-trivial task) and guarantee it doesn't interfer with any of the optimization passes (which may be the source of race conditions themselves).

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.

As long as clang supports C/C++11 - 20+, adopting their memory model puts us in the same boat, which seems reasonably stable to me (though maybe only on their target platforms).
I agree that it's a difficult topic, which shouldn't (and needn't) be rushed. IMO 1.0 can probably do with picking the stable sections of the state-of-the-art C/C++ model that we're interested in supporting.

All 2 comments

Note that in the language specification (#75) the memory model will be specified without referencing an external definition (even if it happens to match C11).

I've also extensively tried to wrap my head around memory models, so I'll try to partake in the discussion when it eventually happens.
Just a couple of quick notes for the interested:

  • Different memory orders (or "AtomicOrder") are a high-level way of reasoning which CPU instructions to use; a more-strictly-defined order means you get more guarantees ("sane behaviour"), but need stronger fencing (and less optimizations through reordering). Consume wasn't "broken" conceptually (IIUC), but it didn't end up mapping to the set of instructions (on older-generation ARM targets I think?) it was designed for - compilers incorrectly assuming so had a broken implementation.
  • The C/C++11 model is sort of the 'best attempt' at an efficient abstraction so far, but it is not (yet?) bullet-proof due to "out-of-thin-air" behaviour. Since its inception, dozens of papers have been published trying to rectify this, most of them incur stronger ordering/costs. The newest most promising one seems to address all issues without penalty, and hasn't been disproved for now. Summary, Presentation, Paper
  • The C/C++11 model turns programs with race conditions wholly-undefined. One sweeping solution is to "localize" their effects, which is done by the "Multicore OCaml" memory model (Paper, Implementation with doc comment); they essentially have to disallow certain optimizations, and use fencing store instructions where concurrent access can occur (or might have occured).
  • (race conditions cont.) While undefined behaviour is a bad fit for Zig, ReleaseFast will probably not want to forfeit optimizations, and I think it's generally difficult to transition from a "safer" model, unless we can provide some runtime detection (for Debug / ReleaseSafe, which I've read is a non-trivial task) and guarantee it doesn't interfer with any of the optimization passes (which may be the source of race conditions themselves).

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.

As long as clang supports C/C++11 - 20+, adopting their memory model puts us in the same boat, which seems reasonably stable to me (though maybe only on their target platforms).
I agree that it's a difficult topic, which shouldn't (and needn't) be rushed. IMO 1.0 can probably do with picking the stable sections of the state-of-the-art C/C++ model that we're interested in supporting.

Was this page helpful?
0 / 5 - 0 ratings

Related issues

andrewrk picture andrewrk  路  3Comments

andersfr picture andersfr  路  3Comments

jorangreef picture jorangreef  路  3Comments

andrewrk picture andrewrk  路  3Comments

zimmi picture zimmi  路  3Comments