A Formal Account of the Wasm 3.0 Concurrency Model

Abstract

WebAssembly (Wasm) is a platform-independent language that serves as a target for web applications and provides rudimentary support for untyped concurrent programming. The Wasm 1.0 memory model was a simple buffer of raw bytes, while the recently finalised Wasm 3.0 adds a new instruction set for dynamically allocated typed structs whose lifetime is managed automatically by the Wasm runtime. However, Wasm structs cannot be used with existing concurrency features of Wasm, and the Wasm type system prevents them from being shared between threads. This means that languages such as Java, OCaml and Kotlin, whose compilers use Wasm 3.0 features, must currently completely forbid the use of source-level shared-memory concurrency features when compiling to Wasm.

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 3.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 in close collaboration with members of WebAssembly's industrial standards community, 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 . Notably prototypes based on our Wasm 3.0 model are under active implementation by major industrial stakeholders. 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.

Paper

People