A formal account of the Wasm 3.0 concurrency model
File(s)
Published version
Author(s)
Raad, Azalea
Kokologiannakis, Michalis
Vafeiadis, Viktor
Watt, Conrad
Type
Journal Article
Abstract
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.
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.
Date Issued
2026-10-01
Date Acceptance
2026-06-10
Citation
Proceedings of the ACM on Programming Languages, 2026, 10 (OOPSLA2), pp.515-543
ISSN
2475-1421
Publisher
Association for Computing Machinery (ACM)
Start Page
515
End Page
543
Journal / Book Title
Proceedings of the ACM on Programming Languages
Volume
10
Issue
OOPSLA2
Copyright Statement
© 2026 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution International 4.0 License.
License URL
Publication Status
Published
Date Publish Online
2026-10-01