WebAssembly Memory Model Wasm
The first formal relaxed-memory model for WebAssembly's shared-memory threads and atomics, and the basis of the model later folded into the Wasm specification. Built on the C/C++11 axiomatic model of Batty et al., it exposes only two access modes — unordered (unord) non-atomics and sequentially-consistent (seqcst) atomics — and, unlike C/C++11, carefully avoids undefined behaviour, giving racy accesses defined but weak (thin-air-permitting) semantics. It is deliberately not sequentially consistent (the authors argue no SC semantics can be given to memory growth) but is proven to guarantee Sequential Consistency for Data-Race-Free programs (SC-DRF), the same guarantee class as C11; the paper also shows the contemporary JavaScript model's SC-DRF claim was false and proposes two conditions, since adopted by TC39, that align JavaScript's SharedArrayBuffer semantics with Wasm's.
Properties
Property vector author-extrapolated — set only where the model’s definition pins the cell down (unknown cells are omitted); cells citing a specific source are marked.
- Reasoning guarantees
- yes No undefined behaviour
- no In-order execution
- no No out-of-thin-air
Ordering relationships
- Equivalent to
- JavaScript Memory Model (JSMM) — Watt et al. 2019 §6.3 (Prop. 6.2): dropping Wasm's two strengthening conditions (†,‡) yields exactly the consistency behaviours of the (uncorrected) JavaScript model on shared array buffers. The paper proposes adding (†,‡) to JavaScript as a strict strengthening; TC39 adopted them, and the repaired model is this dataset's JSMM — so full Wasm and JSMM agree on the shared-memory data-access (SharedArrayBuffer) fragment (excluding traps, memory growth, and mixed-size beyond the shared subset).
- Compiles correctly to
- Total Store Order (TSO) — Watt et al. 2019 Fig. 19 tabulates the compilation of Wasm memory accesses to x86 (whose ISA model is TSO), following the established C/C++11 SC-atomic schemes [Sewell & Sevcik 2016]; full mixed-size correctness is flagged as an open problem (§7.1.1).
- ARM Memory Model — Watt et al. 2019 Fig. 19 gives the compilation of Wasm memory accesses to ARMv7, following the established C/C++11 SC-atomic schemes [Sewell & Sevcik 2016]; full mixed-size correctness is flagged as an open problem (§7.1.1).
- ARMv8 / AArch64 Memory Model — Watt et al. 2019 Fig. 19 gives the compilation of Wasm memory accesses to AArch64/ARMv8 (LDR/STR, LDAR/STLR), following the established C/C++11 SC-atomic schemes [Sewell & Sevcik 2016]; full mixed-size correctness is flagged as an open problem (§7.1.1).
- Compilation target of
- C11/C++11 Memory Model — Watt et al. 2019 §7.2 / Fig. 20 give the compilation of C/C++11 accesses to Wasm memory accesses, mapping all C/C++ atomics (relaxed, acquire/release, seq_cst) onto Wasm seqcst atomics; the sketch shows the compiled program is SC-DRF and thus behaviourally correct at the level of memory accesses.
References
- Conrad Watt, Andreas Rossberg, Jean Pichon-Pharabod. Weakening WebAssembly. PACMPL 3(OOPSLA), Article 133 (SPLASH/OOPSLA 2019); corrigendum Dec 2020, 2019. doi:10.1145/3360559