Relaxed Memory Model

The execution of a WebAssembly program gives rise to a trace of events. WebAssembly’s relaxed memory model constrains the observable behaviours of the program’s execution by defining a consistency condition on the trace of events.

Note

A relaxed memory model is necessary to describe the behaviour of programs exhibiting shared memory concurrency. WebAssembly’s relaxed memory model is heavily based on those of C/C++11 and JavaScript. The relaxed memory model described here is derived from the following article: 1.

Preliminary Definitions

$$\begin{array}{r}\begin{array}{rcl}\mathrm{time}({\mathit{act}}^{\ast }\mathsf{at}{\mathit{time}}_p\mathit{time})& =& \mathit{time}\\ {\mathrm{time}}_p({\mathit{act}}^{\ast }\mathsf{at}{\mathit{time}}_p\mathit{time})& =& {\mathit{time}}_p\\ & & \\ \mathrm{loc}({\mathsf{rd}}_{\mathit{ord}}\mathit{loc}{\mathit{byte}}^{\ast }{\mathsf{notears}}^{?})& =& \mathit{loc}\\ \mathrm{loc}({\mathsf{wr}}_{\mathit{ord}}\mathit{loc}{\mathit{byte}}^{\ast }{\mathsf{notears}}^{?})& =& \mathit{loc}\\ \mathrm{loc}(\mathsf{rmw}\mathit{loc}{{\mathit{byte}}_1}^{\ast }{{\mathit{byte}}_2}^{\ast })& =& \mathit{loc}\\ \mathrm{loc}(\mathsf{wait}\mathit{loc}\mathit{s}\mathit{64})& =& \mathit{loc}\\ \mathrm{loc}(\mathsf{woken}\mathit{loc})& =& \mathit{loc}\\ \mathrm{loc}(\mathsf{timeout}\mathit{loc})& =& \mathit{loc}\\ \mathrm{loc}(\mathsf{notify}\mathit{loc}\mathit{u}\mathit{32}\mathit{u}\mathit{32})& =& \mathit{loc}\\ & & \\ \mathrm{ord}({\mathsf{rd}}_{\mathit{ord}}\mathit{loc}{\mathit{byte}}^{\ast }{\mathsf{notears}}^{?})& =& \mathit{ord}\\ \mathrm{ord}({\mathsf{wr}}_{\mathit{ord}}\mathit{loc}{\mathit{byte}}^{\ast }{\mathsf{notears}}^{?})& =& \mathit{ord}\\ \mathrm{ord}(\mathsf{rmw}\mathit{loc}{{\mathit{byte}}_1}^{\ast }{{\mathit{byte}}_2}^{\ast })& =& \mathsf{seqcst}\\ & & \\ \mathrm{overlap}({\mathit{act}}_1,{\mathit{act}}_2)& =& (\mathrm{range}({\mathit{act}}_1)\cup \mathrm{range}({\mathit{act}}_2)\ne ϵ)\\ \mathrm{same}({\mathit{act}}_1,{\mathit{act}}_2)& =& (\mathrm{range}({\mathit{act}}_1)=\mathrm{range}({\mathit{act}}_2))\\ & & \\ \mathrm{reading}(\mathit{act})& =& (\mathrm{read}(\mathit{act})\ne ϵ)\\ \mathrm{writing}(\mathit{act})& =& (\mathrm{write}(\mathit{act})\ne ϵ)\\ \mathrm{susp}(\mathit{u}\mathit{32},\mathsf{wait}\mathit{reg}[\mathit{u}\mathit{32}]\mathit{s}\mathit{64})& =& \mathsf{wait}\mathit{reg}[\mathit{u}\mathit{32}]\mathit{s}\mathit{64}\\ \mathrm{susp}(\mathit{u}\mathit{32},\mathsf{woken}\mathit{reg}[\mathit{u}\mathit{32}])& =& \mathsf{woken}\mathit{reg}[\mathit{u}\mathit{32}]\\ \mathrm{susp}(\mathit{u}\mathit{32},\mathsf{timeout}\mathit{reg}[\mathit{u}\mathit{32}])& =& \mathsf{timeout}\mathit{reg}[\mathit{u}\mathit{32}]\\ \mathrm{susp}(\mathit{u}\mathit{32},\mathsf{notify}\mathit{reg}[\mathit{u}\mathit{32}]{\mathit{u}\mathit{32}}^{\prime }{\mathit{u}\mathit{32}}^{″})& =& \mathsf{notify}\mathit{reg}[\mathit{u}\mathit{32}]{\mathit{u}\mathit{32}}^{\prime }{\mathit{u}\mathit{32}}^{″}\\ \mathrm{susp}(\mathit{u}\mathit{32},\mathit{act})& =& ϵ(\text{otherwise})\\ & & \\ \mathrm{read}({\mathsf{rd}}_{\mathit{ord}}\mathit{loc}{\mathit{byte}}^{\ast }{\mathsf{notears}}^{?})& =& {\mathit{byte}}^{\ast }\\ \mathrm{read}(\mathsf{rmw}\mathit{loc}{{\mathit{byte}}_1}^{\ast }{{\mathit{byte}}_2}^{\ast })& =& {{\mathit{byte}}_1}^{\ast }\\ \mathrm{read}(\mathit{act})& =& ϵ(\text{otherwise})\\ & & \\ \mathrm{write}({\mathsf{wr}}_{\mathit{ord}}\mathit{loc}{\mathit{byte}}^{\ast }{\mathsf{notears}}^{?})& =& {\mathit{byte}}^{\ast }\\ \mathrm{write}(\mathsf{rmw}\mathit{loc}{{\mathit{byte}}_1}^{\ast }{{\mathit{byte}}_2}^{\ast })& =& {{\mathit{byte}}_2}^{\ast }\\ \mathrm{write}(\mathit{act})& =& ϵ(\text{otherwise})\\ & & \\ \mathrm{offset}(\mathit{act})& =& \mathit{u}\mathit{32}(\text{if}\mathrm{loc}(\mathit{act})=\mathit{reg}[\mathit{u}\mathit{32}])\\ & & \\ \mathrm{sync}({\mathit{act}}_1,{\mathit{act}}_2)& =& (\mathrm{same}({\mathit{act}}_1,{\mathit{act}}_2)\wedge \\ & & \mathrm{ord}({\mathit{act}}_1)=\mathrm{ord}({\mathit{act}}_2)=\mathsf{seqcst})\\ \mathrm{range}(\mathit{act})& =& [\mathit{u}\mathit{32}\dots \mathit{u}\mathit{32}+n-1]\\ & & (\text{if}\mathrm{loc}(\mathit{act})=\mathit{reg}[\mathit{u}\mathit{32}]\wedge \\ & & n=\max (|\mathrm{read}(\mathit{act})|,|\mathrm{write}(\mathit{act})|))\\ & & \\ \mathrm{tearfree}({\mathsf{rd}}_{\mathit{ord}}\mathit{loc}{\mathit{byte}}^{\ast })& =& \mathrm{\perp }(\text{if}\mathit{ord}=\mathsf{unord}\vee \mathit{ord}=\mathsf{init})\\ \mathrm{tearfree}({\mathsf{wr}}_{\mathit{ord}}\mathit{loc}{\mathit{byte}}^{\ast })& =& \mathrm{\perp }(\text{if}\mathit{ord}=\mathsf{unord}\vee \mathit{ord}=\mathsf{init})\\ \mathrm{tearfree}(\mathit{act})& =& \mathrm{\top }(\text{otherwise})\\ & & \\ \mathrm{id}(\mathit{act})& =& \mathit{act}\end{array}\end{array}$$

The above operations on actions are raised to operations on events, indexed by region.

$$\begin{array}{r}\begin{array}{rcl}{\mathit{func}}_{\mathit{reg}}({\mathit{act}}_1^{\ast }\mathit{act}{\mathit{act}}_2^{\ast }\mathsf{at}{\mathit{time}}_p\mathit{time})& =& \mathit{func}(\mathit{act})\\ & & (\text{if}\mathrm{loc}(\mathit{act})=\mathit{reg}[\mathit{u}\mathit{32}])\\ {\mathit{func}}_{\mathit{reg}}({\mathit{act}}_1^{\ast }\mathit{act}{\mathit{act}}_2^{\ast }\mathsf{at}{\mathit{time}}_p\mathit{time},& & \\ {\mathit{act}}_3^{\ast }{\mathit{act}}^{\prime }{\mathit{act}}_4^{\ast }\mathsf{at}{\mathit{time}}_p^{\prime }{\mathit{time}}^{\prime })& =& \mathit{func}(\mathit{act},{\mathit{act}}^{\prime })\\ & & (\text{if}\mathrm{loc}(\mathit{act})=\mathrm{loc}({\mathit{act}}^{\prime })=\mathit{reg}[\mathit{u}\mathit{32}])\end{array}\end{array}$$

Traces

Todo

novel notation here?

A trace is a coinductive list of events. A trace is considered to be a pre-execution of a given global configuration if it represents the events emitted by the coinductive closure of the global reduction relation on that configuration, such that all of the trace’s consituent events have unique time stamps that are totally ordered according to the reduction order.

$$\begin{array}{r}\begin{array}{c}\begin{array}{c}\mathit{config}{\hookrightarrow }^{\mathit{evt}}{\mathit{config}}^{\prime }⊢{\mathit{config}}^{\prime }:\mathit{tr}\\ \mathrm{\forall }{\mathit{evt}}^{\prime }\in \mathit{tr},\mathrm{time}({\mathit{evt}}^{\prime }){\prec }_{\mathsf{tot}}\mathrm{time}(\mathit{evt})\end{array}\begin{array}{l}\mathrm{time}(\mathit{evt})\notin {\mathrm{time}}^{\ast }(\mathit{tr})\\ {\mathrm{time}}_p(\mathit{evt})\notin {\mathrm{time}}_p^{\ast }(\mathit{tr})\end{array}\\ \\ \\ ⊢\mathit{config}:\mathit{evt}\mathit{tr}\end{array}\end{array}$$

When a WebAssembly program is executed, all behaviours observed during that execution must correspond to a single consistent pre-execution of that execution’s starting configuration.

Consistency

$$\frac{\mathrm{\forall }\mathit{reg},{⊢}_{\mathit{reg}}\mathit{tr}\text{consistent-with}}{⊢\mathit{tr}\text{consistent}}$$

$$\begin{array}{r}\frac{\begin{array}{c}\mathrm{\forall }i,{⊢}_{\mathit{reg}}^i\mathit{tr}\text{suspensions-consistent}\\ \mathrm{\forall }{\mathit{evt}}_R\in {\mathrm{reading}}_{\mathit{reg}}(\mathit{tr}),\mathrm{\exists }{\mathit{evt}}_W^{\ast },\mathit{tr}{⊢}_{\mathit{reg}}{\mathit{evt}}_R\text{reads-each-from}{\mathit{evt}}_W^{\ast }\\ \mathrm{\forall }{\mathit{evt}}_I,\mathit{evt}\in \mathit{tr},{\mathrm{ord}}_{\mathit{reg}}({\mathit{evt}}_I)=\mathsf{init}\wedge {\mathit{evt}}_I\ne \mathit{evt}\wedge \mathrm{overlap}({\mathit{evt}}_I,\mathit{evt})\Rightarrow {\mathit{evt}}_I{\prec }_{\mathsf{hb}}\mathit{evt}\end{array}}{{⊢}_{\mathit{reg}}\mathit{tr}\text{consistent-with}}\end{array}$$

$$\begin{array}{r}\frac{\begin{array}{c}\left|{\mathit{evt}}_W^{\ast }\right|=|{\mathrm{read}}_{\mathit{reg}}({\mathit{evt}}_R)|\\ \mathrm{\forall }i<|{\mathit{evt}}_W^{\ast }|,\mathit{tr}{⊢}_{\mathit{reg}}^i{\mathit{evt}}_R\text{reads-from}({\mathit{evt}}_W^{\ast }[i])\\ {⊢}_{\mathit{reg}}{\mathit{evt}}_R\text{no-tear}{\mathit{evt}}_W^{\ast }\end{array}}{\mathit{tr}{⊢}_{\mathit{reg}}{\mathit{evt}}_R\text{reads-each-from}{\mathit{evt}}_W^{\ast }}\end{array}$$

$$\begin{array}{r}\frac{\begin{array}{c}{\mathit{evt}}_R\ne {\mathit{evt}}_W\\ {\mathit{evt}}_W\in {\mathrm{writing}}_{\mathit{reg}}(\mathit{tr})\\ \mathit{tr}{⊢}_{\mathit{reg}}^{i,k}{\mathit{evt}}_R\text{value-consistent}{\mathit{evt}}_W\\ \mathit{tr}{⊢}_{\mathit{reg}}^k{\mathit{evt}}_R\text{hb-consistent}{\mathit{evt}}_W\\ \mathit{tr}{⊢}_{\mathit{reg}}{\mathit{evt}}_R\text{sc-last-visible}{\mathit{evt}}_W^{\ast }\end{array}}{\mathit{tr}{⊢}_{\mathit{reg}}^i{\mathit{evt}}_R\text{reads-from}{\mathit{evt}}_W}\end{array}$$

$$\begin{array}{r}\frac{\begin{array}{rcl}{\mathrm{read}}_{\mathit{reg}}({\mathit{evt}}_R)[i]& =& {\mathrm{write}}_{\mathit{reg}}({\mathit{evt}}_W)[j]\\ k={\mathrm{offset}}_{\mathit{reg}}({\mathit{evt}}_R)+i& =& {\mathrm{offset}}_{\mathit{reg}}({\mathit{evt}}_W)+j\end{array}}{\mathit{tr}{⊢}_{\mathit{reg}}^{i,k}{\mathit{evt}}_R\text{value-consistent}{\mathit{evt}}_W}\end{array}$$

$$\begin{array}{r}\frac{\begin{array}{c}\mathrm{\neg }({\mathit{evt}}_R{\prec }_{\mathsf{hb}}{\mathit{evt}}_W)\\ {\mathrm{sync}}_{\mathit{reg}}({\mathit{evt}}_W,{\mathit{evt}}_R)\Rightarrow {\mathit{evt}}_W{\prec }_{\mathsf{hb}}{\mathit{evt}}_R\\ \mathrm{\forall }{\mathit{evt}}_W^{\prime }\in {\mathrm{writing}}_{\mathit{reg}}(\mathit{tr}),{\mathit{evt}}_W{\prec }_{\mathsf{hb}}{\mathit{evt}}_W^{\prime }{\prec }_{\mathsf{hb}}{\mathit{evt}}_R\Rightarrow k\notin {\mathrm{range}}_{\mathit{reg}}({\mathit{evt}}_W^{\prime })\end{array}}{\mathit{tr}{⊢}_{\mathit{reg}}^k{\mathit{evt}}_R\text{hb-consistent}{\mathit{evt}}_W}\end{array}$$

$$\begin{array}{r}\frac{\begin{array}{l}\mathrm{\forall }{\mathit{evt}}_W^{\prime }\in {\mathrm{writing}}_{\mathit{reg}}(\mathit{tr}),{\mathit{evt}}_W{\prec }_{\mathsf{hb}}{\mathit{evt}}_R\Rightarrow \\ {\mathit{evt}}_W{\prec }_{\mathsf{tot}}{\mathit{evt}}_W^{\prime }{\prec }_{\mathsf{tot}}{\mathit{evt}}_R\wedge {\mathrm{sync}}_{\mathit{reg}}({\mathit{evt}}_W,{\mathit{evt}}_R)\Rightarrow \mathrm{\neg }{\mathrm{sync}}_{\mathit{reg}}({\mathit{evt}}_W^{\prime },{\mathit{evt}}_R)\\ {\mathit{evt}}_W{\prec }_{\mathsf{hb}}{\mathit{evt}}_W^{\prime }{\prec }_{\mathsf{tot}}{\mathit{evt}}_R\Rightarrow \mathrm{\neg }{\mathrm{sync}}_{\mathit{reg}}({\mathit{evt}}_W^{\prime },{\mathit{evt}}_R)\\ {\mathit{evt}}_W{\prec }_{\mathsf{tot}}{\mathit{evt}}_W^{\prime }{\prec }_{\mathsf{hb}}{\mathit{evt}}_R\Rightarrow \mathrm{\neg }{\mathrm{sync}}_{\mathit{reg}}({\mathit{evt}}_W,{\mathit{evt}}_W^{\prime })\end{array}}{\mathit{tr}{⊢}_{\mathit{reg}}{\mathit{evt}}_R\text{sc-last-visible}{\mathit{evt}}_W}\end{array}$$

$$\begin{array}{r}\frac{\begin{array}{l}{\mathrm{tearfree}}_{\mathit{reg}}({\mathit{evt}}_R)\Rightarrow \\ |\{{\mathit{evt}}_W\in {\mathit{evt}}_W^{\ast }|{\mathrm{same}}_{\mathit{reg}}({\mathit{evt}}_R,{\mathit{evt}}_W)\wedge {\mathrm{tearfree}}_{\mathit{reg}}({\mathit{evt}}_W)\}|\le 1\end{array}}{{⊢}_{\mathit{reg}}{\mathit{evt}}_R\text{no-tear}{\mathit{evt}}_W^{\ast }}\end{array}$$

$$\begin{array}{r}\frac{\begin{array}{c}{\mathrm{susp}}_{\mathit{reg}}^{\ast }(i,\mathit{tr})={\mathit{tr}}^{\prime }{⊢}_{\mathit{reg}}^i{\mathit{tr}}^{\prime }\text{suspensions-consistent-with}(ϵ)\\ \mathrm{\forall }\mathit{evt},{\mathit{evt}}^{\prime }\in {\mathit{tr}}^{\prime },\mathit{evt}{\prec }_{\mathsf{tot}}{\mathit{evt}}^{\prime }⟹\mathit{evt}{\prec }_{\mathsf{hb}}{\mathit{evt}}^{\prime }\end{array}}{{⊢}_{\mathit{reg}}^i\mathit{tr}\text{suspensions-consistent}}\end{array}$$

$$\frac{}{{⊢}_{\mathit{reg}}^iϵ\text{suspensions-consistent-with}({\mathit{time}}^{\ast })}$$

$$\frac{{\mathrm{id}}_{\mathit{reg}}(\mathit{evt})=(\mathsf{wait}\mathit{reg}[i]\mathit{s}\mathit{64}){⊢}_{\mathit{reg}}^i\mathit{tr}\text{suspensions-consistent-with}(\mathrm{time}(\mathit{evt}){\mathit{time}}^{\ast })}{{⊢}_{\mathit{reg}}^i\mathit{evt}\mathit{tr}\text{suspensions-consistent-with}({\mathit{time}}^{\ast })}$$

$$\frac{{\mathrm{id}}_{\mathit{reg}}(\mathit{evt})=(\mathsf{timeout}\mathit{reg}[i]){⊢}_{\mathit{reg}}^i\mathit{tr}\text{suspensions-consistent-with}({\mathit{time}}^{\ast }{\mathit{time}}^{\prime \ast })}{{⊢}_{\mathit{reg}}^i\mathit{evt}\mathit{tr}\text{suspensions-consistent-with}({\mathit{time}}^{\ast }{\mathrm{time}}_p(\mathit{evt}){\mathit{time}}^{\prime \ast })}$$

$$\begin{array}{r}\frac{\begin{array}{c}{\mathrm{id}}_{\mathit{reg}}^n({\mathit{evt}}^n)=(\mathsf{woken}\mathit{reg}[i]){\mathrm{id}}_{\mathit{reg}}({\mathit{evt}}_N)=(\mathsf{notify}\mathit{reg}[i]nk)\\ n<k⟹m=0{⊢}_{\mathit{reg}}^i\mathit{tr}\text{suspensions-consistent-with}({\mathit{time}}^m)\end{array}}{{⊢}_{\mathit{reg}}^i{\mathit{evt}}_N{\mathit{evt}}^n\mathit{tr}\text{suspensions-consistent-with}({\mathit{time}}^m{\mathrm{time}}_p^n({\mathit{evt}}^n))}\end{array}$$

Note

The following is a non-normative and non-exhaustive explanation of WebAssembly’s relaxed memory model in plain English. Note that the definition of Consistency is the sole normative definition of the relaxed memory model.

When a WebAssembly operation reads from shared mutable state, the WebAssembly relaxed memory model determines the value that this read access observes, in terms of the write access to the same location(s) that have occurred in the execution.

The WebAssembly memory model is built around the concept of a happens-before transitive partial order between accesses of shared mutable state, ${\prec }_{\mathsf{hb}}$, which captures a strong notion of causality. All sequential accesses in the same thread are related by ${\prec }_{\mathsf{hb}}$ according to execution order. Certain operations also establish a ${\prec }_{\mathsf{hb}}$ relation between operations of different threads (see atomic accesses below). A read access may never take its value from a write access that comes later in ${\prec }_{\mathsf{hb}}$. Moreover, if two write accesses ordered by ${\prec }_{\mathsf{hb}}$ come before a read access in ${\prec }_{\mathsf{hb}}$, the read access must take its value from the later of the two write accesses according to ${\prec }_{\mathsf{hb}}$. In the case that ${\prec }_{\mathsf{hb}}$ does not uniquely determine a write access that a given read access must take its value from, the read access may non-deterministically take its value from any permitted write.

In the case that a read operation is a multi-byte memory access, the value of each byte may in certain circumstances be determined by a different write event. If this happens, we describe the read operation as tearing. In general, naturally aligned multi-byte reads are not allowed to tear, unless they race with a partially overlapping write or are greater than four bytes in width.

Most WebAssembly accesses of shared mutable state are classified as non-atomic. However a number of operations are classified as performing atomic accesses. Atomic accesses must always be naturally aligned. If an atomic read takes its value from an atomic write of the same width, the write access is fixed as coming before the read access in ${\prec }_{\mathsf{hb}}$. This is the main mechanism by which a ${\prec }_{\mathsf{hb}}$ relation is established between threads.

WebAssembly’s atomic operations are also required to be sequentially consistent. The relaxed memory model defines a toal order on all events of the execution, ${\prec }_{\mathsf{tot}}$, and sequentially consistent operations to identical ranges must respect this ordering - i.e. sequentially consistent reads cannot read from any sequentially consistent write of idential range other than the most recent preceding one according to ${\prec }_{\mathsf{tot}}$.

Some operations such as memory accesses must perform a bounds check in addition to accessing data. The relaxed memory model treats these accesses as additionally accessing a distinguished length location, with the observed value respecting the constraints of the relaxed memory model. Most bounds checks are non-atomic, but bounds checks peformed during instantiation are atomic, and changes to the length (e.g. $\mathsf{memory}\mathsf{.}\mathsf{grow}$) are modelled as atomic read-modify-write accesses.

In some circumstances, two accesses to overlapping locations may occur in an execution without any relation in ${\prec }_{\mathsf{hb}}$. This situation is known as a race. If at least one of these accesses is a non-atomic write, we describe this situation as a data race. Unlike some other relaxed memory models, WebAssembly does not declare data races to be undefined behaviour. However, the allowed execution behaviours may still be highly non-deterministic as the lack of ${\prec }_{\mathsf{hb}}$ relations means that reads participating in or overlapping with the location of the data race may non-deterministically observe a number of different values.

The relaxed memory model also describes the concurrent behaviour of WebAssembly’s wait ($\mathsf{memory}\mathsf{.}\mathsf{atomic}\mathsf{.}\mathsf{wait}$) and notify ($\mathsf{memory}\mathsf{.}\mathsf{atomic}\mathsf{.}\mathsf{notify}$) operations. Each memory location is associated with a queue of waiting threads. A thread suspending as the result of a wait operation enters the queue, and a notify operation to that location will attempt to wake up as many threads as possible from the head of the associated queue, up to the maximum specified by the arguments of the notify operation. All operations on the same location which change the state of that location’s wait queue are sequentially consistent and totally ordered by ${\prec }_{\mathsf{hb}}$.

1

The semantics of the relaxed memory model is derived from the following article: Conrad Watt, Andreas Rossberg, Jean Pichon-Pharabod. Weakening WebAssembly. Proceedings of the ACM on Programming Languages (OOPSLA 2019). ACM 2019.