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 \textit{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 \textit{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.