-
-

Todo

-

add index entries

-
-
+

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 decribed here is derived from the following article: 1.

+The relaxed memory model decribed here is derived from the following article: 1.

Preliminary Definitions

@@ -154,14 +150,14 @@

Quick search

\qquad \href{../exec/runtime.html#syntax-act}{\mathit{act}}_3^\ast~\href{../exec/runtime.html#syntax-act}{\mathit{act}}'~\href{../exec/runtime.html#syntax-act}{\mathit{act}}_4^\ast~\href{../exec/runtime.html#syntax-time}{\mathbin{\mathsf{at}}}~\href{../exec/runtime.html#syntax-time}{\mathit{time}}'_p~\href{../exec/runtime.html#syntax-time}{\mathit{time}}') & = & \mathit{func}(\href{../exec/runtime.html#syntax-act}{\mathit{act}},\href{../exec/runtime.html#syntax-act}{\mathit{act}}') \\ && (\mathrel{\mbox{if}}~\href{../exec/relaxed.html#relaxed-aux}{\mathrm{loc}}(\href{../exec/runtime.html#syntax-act}{\mathit{act}}) = \href{../exec/relaxed.html#relaxed-aux}{\mathrm{loc}}(\href{../exec/runtime.html#syntax-act}{\mathit{act}}') = \href{../exec/runtime.html#syntax-reg}{\mathit{reg}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}]) \\ \end{array}\end{split}\]