A Formal Account of the Wasm 3.0 Concurrency Model

WebAssembly (Wasm) is a platform-independent target for web applications that provides rudimentary support for untyped concurrent programming. While Wasm 1.0’s memory model was a simple buffer of raw bytes, the recently-finalised Wasm 3.0 feature set adds a new instruction set for dynamically allocated typed structs whose lifetime is managed automatically by the Wasm runtime. This feature was intended to facilitate the compilation of garbage-collected source languages to Wasm. However, due to legacy technical constraints inherited from the wider web platform, Wasm structs cannot be used with Wasm’s existing concurrency features and are prevented by the language’s type system from being shared between multiple threads. As of now, a broad industrial project within the Wasm community named shared-everything threads seeks to relax these restrictions and specify the concurrent behaviour of Wasm 2.0 structs. To inform these efforts, we formalise a concurrency semantics for Wasm 3.0 structs and prove the correctness of (a) the intended compilation scheme to x86 and Arm; (b) compilation from C/C++ and OCaml concurrency primitives to Wasm; and (c) intended compiler optimisations. We also establish a DRF property and provide a model checking tool for verifying concurrent Wasm programs. We have carried out our work with the aim that our semantics should be adopted as the official concurrency model for Wasm 3.0 as the shared-everything threads project progresses. Along the way, we critically appraise the existing Wasm 1.0 memory model, identifying several changes that could be made to better align it with the state of the art in relaxed memory research.