一句话：为 Wasm 3.0 的 struct 提出并发语义，证明编译方案与优化正确，建立 DRF 性质并提供模型检测工具。
WebAssembly 3.0 引入了由运行时自动管理生命周期的动态分配类型化 struct，以便将带 GC 的源语言编译到 Wasm；但受 web 平台遗留技术约束影响，这些 struct 无法与 Wasm 既有并发特性共用，并被类型系统禁止跨线程共享。本文为 Wasm 3.0 struct 给出并发语义，旨在为 Wasm 社区正在推进的 shared-everything threads 项目提供依据，并证明三类正确性：(a) 到 x86 与 Arm 的预期编译方案；(b) 从 C/C++ 与 OCaml 并发原语到 Wasm 的编译；(c) 预期编译器优化。文章还建立了 DRF（data-race freedom）性质，并提供用于验证并发 Wasm 程序的模型检测工具；此外批判性审视 Wasm 1.0 内存模型，指出若干可使其实践与放松内存研究前沿更一致的修改。
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.
@article{paperbot12091,
title = {A Formal Account of the Wasm 3.0 Concurrency Model},
author = {Azalea Raad and Michalis Kokologiannakis and Viktor Vafeiadis and Conrad Watt},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839465}
}