[spec] Document execution #19

binji · 2018-05-22T00:55:14Z

Started to work on spec for execution. Still more work to do, but I thought it would be useful to get some early feedback.

binji · 2018-05-22T00:56:16Z

Rendered result: https://webassembly.github.io/bulk-memory-operations/core/bikeshed

binji · 2018-05-31T21:34:53Z

@rossberg PTAL if you have time!

rossberg

This looks mostly good, except for the correct indexing semantics.

One thing I was hoping for, though, is that with proper memory.init and table.init instructions we could get rid of the auxiliary init_data and init_elem ones, and replace their uses with the former. Is there a reason why that cannot work?

rossberg · 2018-06-01T10:30:41Z

document/core/exec/instructions.rst

+
+12. Pop the value :math:`\I32.\CONST~s` from the stack.
+
+13. Pop the value :math:`\I32.\CONST~t` from the stack.


Nit: the spec convention is to use t for value types, and i,j,k,m,n for integers, at least if they are single-letter. So either use those or somewhat longer names.

rossberg · 2018-06-01T10:31:12Z

document/core/exec/instructions.rst

+
+    a. Trap.
+
+18. Let :math:`y` be the byte sequence :math:`\X{mem}.\DSIINIT[s \slice n]`.


Nit: Use b^\ast instead of y.

rossberg · 2018-06-01T10:32:39Z

document/core/exec/instructions.rst

+     \end{array}
+   \\[1ex]
+   \begin{array}{lcl@{\qquad}l}
+   S; F; (\I32.\CONST~n)~(\I32.\CONST~t)~(\I32.\CONST~s)~(\MEMORYINIT~x) &\stepto& S; F; \TRAP


This needs an "otherwise" as a side conditione, else it would always be allowed non-deterministically.

rossberg · 2018-06-01T10:38:52Z

document/core/exec/modules.rst

+
+1. Let :math:`e` be the :ref:`element segment <syntax-elem>` to allocate.
+
+2. If :math:`e` is of the form :math:`\{ \EINIT~x^\ast \}`, then:


What does this algorithm return otherwise? Should it be epsilon, i.e., the algo returns an optional address?

rossberg · 2018-06-01T10:40:42Z

document/core/exec/modules.rst

+.. math::
+   \begin{array}{rlll@{\qquad}l}
+   \allocelem(S, e, \moduleinst) &=& S', \elemaddr & (\iff e = \{ \EINIT~x^\ast \}) \\[1ex]
+   \allocelem(S, e, \moduleinst) &=& S & (\otherwise) \\[1ex]


This only returns one thing, not a pair, which seems incoherent. I think it should be epsilon.

rossberg · 2018-06-01T10:44:43Z

document/core/exec/modules.rst

+
+1. Let :math:`d` be the :ref:`data segment <syntax-data>` to allocate.
+
+2. If :math:`d` is of the form :math:`\{ \DINIT~b^\ast \}`, then:


rossberg · 2018-06-01T10:48:52Z

document/core/exec/modules.rst

-6. Let :math:`\funcaddr^\ast` be the the concatenation of the :ref:`function addresses <syntax-funcaddr>` :math:`\funcaddr_i` in index order.
+6. For each :ref:`element segment <syntax-elem>` :math:`\elem_i` in :math:`\module.\MELEM`, do:
+
+   a. Let :math:`\elemaddr_i` be the :ref:`element address <syntax-elemaddr>` resulting from :ref:`allocating <alloc-elem>` :math:`\elem_i` for the :ref:`\module instance <syntax-moduleinst>` :math:`\moduleinst` defined below.


Here you assume that the vector of elemaddr_i corresponds to elem_i, which is not the case because you only get addresses for passive elements. So I think what the module instance needs to store is not am elemaddr^* but an (elemaddr^?)^*. Otherwise all the indexing will be off, too.

rossberg · 2018-06-01T10:55:03Z

document/core/exec/runtime.rst

@@ -158,6 +170,8 @@ and collects runtime representations of all entities that are imported, defined,
     \MITABLES & \tableaddr^\ast, \\
     \MIMEMS & \memaddr^\ast, \\
     \MIGLOBALS & \globaladdr^\ast, \\
+     \MIELEMS & \elemaddr^\ast, \\


As mentioned above, I think these need to be optional addresses to represent indices of active segments correctly.

rossberg · 2018-06-01T10:56:09Z

document/core/exec/runtime.rst

+.. math::
+   \begin{array}{llll}
+   \production{(element instance)} & \eleminst &::=&
+     \{ \ESIINIT~\vec(\funcaddr) \} \\


Nit: why not EIINIT?

rossberg · 2018-06-01T10:56:23Z

document/core/exec/runtime.rst

+.. math::
+   \begin{array}{llll}
+   \production{(data instance)} & \datainst &::=&
+     \{ \DSIINIT~\vec(\byte) \} \\


Same Q here.

binji · 2018-06-07T23:53:21Z

One thing I was hoping for, though, is that with proper memory.init and table.init instructions we could get rid of the auxiliary init_data and init_elem ones, and replace their uses with the former. Is there a reason why that cannot work?

I think it's possible, and I started to do this, but it's pretty ugly unless we go with option 2 here.

Here's what I was thinking:

Create element/data instances for all segments, even active ones
instantiate executes something like S;F; (i32.const |elem.data|) (i32.const 0) (elem.offset) (table.init x) (table.drop x) for each active segment
Similar for data segments

Without option 2, though, I guess you'd need to conditionally update the state only if none of the instructions trap. I started to write this, but wasn't quite sure how to define it, and thought we may need to change it for the threads proposal anyway.

rossberg · 2018-06-09T11:36:35Z

Yes, I like that makes. Look slike the preferable route.

For option 1, wouldn't the only difference be that we keep the bounds checks as pre-checks in the instantiation itself?

rossberg

Sorry, dropped the ball on this review.

rossberg · 2018-07-09T14:09:02Z

document/core/exec/instructions.rst

+   \end{array}
+   \\ \qquad
+     \begin{array}[j]{@{}r@{~}l@{}}
+     (\iff & F.\AMODULE.\MIMEMS[0] = ma \\


It seems like ma isn't needed (similarly in prose).

rossberg · 2018-07-09T14:13:05Z

document/core/exec/instructions.rst

+   ~\\[-1ex]
+   \begin{array}{l}
+   \begin{array}{lcl@{\qquad}l}
+   S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\MEMORYCOPY~x) &\stepto& S; F; (\INITDATA~ma~j~b^\ast)


The index x seems unused. I think in the future we will want two indices, for source and target memory, but for now we can probably drop both from the AST.

rossberg · 2018-07-09T14:19:07Z

document/core/exec/instructions.rst

+     (\iff & F.\AMODULE.\MIMEMS[0] = ma \\
+     \wedge & (i + n \leq |S.\SMEMS[ma].\MIDATA|) \\
+     \wedge & (j + n \leq |S.\SMEMS[ma].\MIDATA|) \\
+     \wedge & b^\ast = S.\SMEMS[ma].\MIDATA[i \slice n]) \\


Should we add a note that this semantics implies that overlapping ranges are handled correctly?

Also, this semantics essentially prescribes buffering of the copied memory before writing begins. That will be observable once we have threads and concurrent mutation. I think it's fine to leave this for now, but I suspect we will need to tweak it. Perhaps adda TODO note?

rossberg · 2018-07-09T16:44:43Z

document/core/exec/instructions.rst

+
+8. Let :math:`ea` be the :ref:`element segment address <syntax-elemaddr>` :math:`F.\AMODULE.\MIELEMS[x]`.
+
+9. If :math:`S.\SELEM[ea]` does not exist, then:


Nit: better say "is unset" or something like that (ea exists in the list, but its value is epsilon).

rossberg · 2018-07-09T16:46:21Z

document/core/exec/instructions.rst

+   \end{array}
+   \\ \qquad
+     \begin{array}[j]{@{}r@{~}l@{}}
+     (\iff & F.\AMODULE.\MITABLES[0] = ta \\


Same as above: ta is unused.

rossberg · 2018-07-09T16:48:10Z

document/core/exec/instructions.rst

+   ~\\[-1ex]
+   \begin{array}{l}
+   \begin{array}{lcl@{\qquad}l}
+   S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\TABLECOPY~x) &\stepto& S; F; (\INITELEM~ta~j~y^\ast)


Same as above: x unused.

rossberg · 2018-07-09T16:52:29Z

document/core/exec/instructions.rst

+.. index:: table, table instance, table address, initialize table
+.. _initelem:
+
+:math:`\INITELEM~\tableaddr~o~x^\ast`


Let's rename x* to a* here and below, since they're not function indices but function addresses.

rossberg · 2018-07-09T16:54:07Z

document/core/exec/modules.rst


-   b. For each :ref:`function index <syntax-funcidx>` :math:`x_i` in :math:`e.\EINIT`, do:
+   a. Let :math:`\funcaddr_i` be the :ref:`function address <syntax-funcaddr>` :math:`\moduleinst.\MIFUNCS[x_i]`.


First assert that this exists.

rossberg · 2018-07-09T17:06:49Z

document/core/exec/instructions.rst

+     \begin{array}[j]{@{}r@{~}l@{}}
+     (\iff & F.\AMODULE.\MIMEMS[0] = ma \\
+     \wedge & F.\AMODULE.\MIDATAS[x] = da \\
+     \wedge & S' = S \with \SDATA[da] = \epsilon) \\


Setting a SDATA slot to epsilon must allow for it in the definition of store, i.e., change the syntax to (\datainst^?)^* (same for element segments).

binji · 2018-07-09T18:52:38Z

Sorry, dropped the ball on this review.

It's OK, I still haven't fixed the instantiation to use MEMORYINIT/TABLEINIT instead of INITDATA/INITELEM. Got a bit sidetracked with other stuff.

binji · 2019-02-21T19:27:34Z

This is pretty out-of-date at this point, closing for now.

This is copied and modified from this closed PR: #19

[spec] Document execution

1f65aa1

binji requested a review from rossberg May 22, 2018 00:55

Capitalize some headings

6c73ce1

rossberg reviewed Jun 1, 2018

View reviewed changes

Address some comments

94e91c4

binji added 4 commits June 12, 2018 17:14

Add memory.{drop,copy} exec

9bbfe24

Add Table instructions

af0622b

Init all segments, move initdata/initelem into instructions section

4fd2b5b

Some instruction fixes

526575e

rossberg reviewed Jul 9, 2018

View reviewed changes

Address some comments

d058cd0

conrad-watt mentioned this pull request Aug 8, 2018

Data initialization synchronization WebAssembly/threads#96

Open

binji closed this Feb 21, 2019

binji added a commit that referenced this pull request May 24, 2019

[spec] Runtime format of element and data segments

2d16b84

This is copied and modified from this closed PR: #19

binji mentioned this pull request May 24, 2019

[spec] Runtime format of element and data segments #91

Merged

binji added a commit that referenced this pull request May 31, 2019

[spec] Runtime format of element and data segments (#91)

a976b82

This is copied and modified from this closed PR: #19

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[spec] Document execution #19

[spec] Document execution #19

binji commented May 22, 2018

binji commented May 22, 2018

binji commented May 31, 2018

rossberg left a comment

rossberg Jun 1, 2018

rossberg Jun 1, 2018

rossberg Jun 1, 2018

rossberg Jun 1, 2018

rossberg Jun 1, 2018

rossberg Jun 1, 2018

rossberg Jun 1, 2018

rossberg Jun 1, 2018

rossberg Jun 1, 2018

rossberg Jun 1, 2018

binji commented Jun 7, 2018

rossberg commented Jun 9, 2018

rossberg left a comment

rossberg Jul 9, 2018

rossberg Jul 9, 2018

rossberg Jul 9, 2018

rossberg Jul 9, 2018

rossberg Jul 9, 2018

rossberg Jul 9, 2018

rossberg Jul 9, 2018

rossberg Jul 9, 2018

rossberg Jul 9, 2018

binji commented Jul 9, 2018

binji commented Feb 21, 2019


		12. Pop the value :math:`\I32.\CONST~s` from the stack.

		13. Pop the value :math:`\I32.\CONST~t` from the stack.


		a. Trap.

		18. Let :math:`y` be the byte sequence :math:`\X{mem}.\DSIINIT[s \slice n]`.


		1. Let :math:`e` be the :ref:`element segment <syntax-elem>` to allocate.

		2. If :math:`e` is of the form :math:`\{ \EINIT~x^\ast \}`, then:


		1. Let :math:`d` be the :ref:`data segment <syntax-data>` to allocate.

		2. If :math:`d` is of the form :math:`\{ \DINIT~b^\ast \}`, then:


		8. Let :math:`ea` be the :ref:`element segment address <syntax-elemaddr>` :math:`F.\AMODULE.\MIELEMS[x]`.

		9. If :math:`S.\SELEM[ea]` does not exist, then:


		b. For each :ref:`function index <syntax-funcidx>` :math:`x_i` in :math:`e.\EINIT`, do:
		a. Let :math:`\funcaddr_i` be the :ref:`function address <syntax-funcaddr>` :math:`\moduleinst.\MIFUNCS[x_i]`.

[spec] Document execution #19

[spec] Document execution #19

Conversation

binji commented May 22, 2018

binji commented May 22, 2018

binji commented May 31, 2018

rossberg left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

binji commented Jun 7, 2018

rossberg commented Jun 9, 2018

rossberg left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

binji commented Jul 9, 2018

binji commented Feb 21, 2019