Skip to content
This repository was archived by the owner on Nov 3, 2021. It is now read-only.

[spec] Document execution #19

Closed
wants to merge 8 commits into from
Closed

[spec] Document execution #19

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
1f65aa1
[spec] Document execution
binji May 22, 2018
6c73ce1
Capitalize some headings
binji May 22, 2018
94e91c4
Address some comments
binji Jun 7, 2018
9bbfe24
Add memory.{drop,copy} exec
binji Jun 13, 2018
af0622b
Add Table instructions
binji Jun 20, 2018
4fd2b5b
Init all segments, move initdata/initelem into instructions section
binji Jun 20, 2018
526575e
Some instruction fixes
binji Jun 20, 2018
d058cd0
Address some comments
binji Jul 9, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
371 changes: 371 additions & 0 deletions document/core/exec/instructions.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -618,6 +618,377 @@ Memory Instructions
In practice, the choice depends on the :ref:`resources <impl-exec>` available to the :ref:`embedder <embedder>`.


.. _exec-memory.init:

:math:`\MEMORYINIT~x`
.....................

1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.

2. Assert: due to :ref:`validation <valid-memory.init>`, :math:`F.\AMODULE.\MIMEMS[0]` exists.

3. Let :math:`ma` be the :ref:`memory address <syntax-memaddr>` :math:`F.\AMODULE.\MIMEMS[0]`.

4. Assert: due to :ref:`validation <valid-memory.init>`, :math:`S.\SMEMS[ma]` exists.

5. Let :math:`\X{mem}` be the :ref:`memory instance <syntax-meminst>` :math:`S.\SMEMS[ma]`.

6. Let :math:`msz` be the length of :math:`\X{mem}.\MIDATA`.

7. Assert: due to :ref:`validation <valid-memory.init>`, :math:`F.\AMODULE.\MIDATAS[x]` exists.

8. Let :math:`da` be the :ref:`data segment address <syntax-dataaddr>` :math:`F.\AMODULE.\MIDATAS[x]`.

9. If :math:`S.\SDATA[da]` is :math:`\epsilon`, then:

a. Trap.

10. Let :math:`\X{data}` be the :ref:`data segment instance <syntax-datainst>` :math:`S.\SDATA[da]`.

11. Assert: due to :ref:`validation <valid-memory.init>`, three values of :ref:`value type <syntax-valtype>` |I32| are on the top of the stack.

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

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

14. Pop the value :math:`\I32.\CONST~n` from the stack.

15. Let :math:`dsz` be the length of :math:`\X{data}.\DIINIT`.

16. If :math:`i + n > dsz`, then:

a. Trap.

17. If :math:`j + n > msz`, then:

a. Trap.

18. Let :math:`b^\ast` be the byte sequence :math:`\X{data}.\DIINIT[i \slice n]`.

19. :ref:`Initialize <initdata>` the memory instance at address :math:`ma` starting from offset :math:`j` with the byte sequence :math:`b^\ast`.

.. math::
~\\[-1ex]
\begin{array}{l}
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\MEMORYINIT~x) &\stepto& S; F; (\INITDATA~ma~j~b^\ast)
\end{array}
\\ \qquad
\begin{array}[j]{@{}r@{~}l@{}}
(\iff & F.\AMODULE.\MIMEMS[0] = ma \\
\wedge & F.\AMODULE.\MIDATAS[x] = da \\
\wedge & S.\SDATA[da] \neq \epsilon \\
\wedge & (i + n \leq |S.\SDATA[da].\DIINIT|) \\
\wedge & (j + n \leq |S.\SMEMS[ma].\MIDATA|) \\
\wedge & b^\ast = S.\SDATA[da].\DIINIT[i \slice n]) \\
\end{array}
\\[1ex]
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\MEMORYINIT~x) &\stepto& S; F; \TRAP
\end{array}
\\ \qquad
(\otherwise)
\end{array}


.. _exec-memory.drop:

:math:`\MEMORYDROP~x`
.....................

1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.

2. Assert: due to :ref:`validation <valid-memory.drop>`, :math:`F.\AMODULE.\MIDATAS[x]` exists.

3. Let :math:`da` be the :ref:`data segment address <syntax-dataaddr>` :math:`F.\AMODULE.\MIDATAS[x]`.

4. Replace :math:`S.\SDATA[da]` with :math:`\epsilon`.

.. math::
~\\[-1ex]
\begin{array}{l}
\begin{array}{lcl@{\qquad}l}
S; F; (\MEMORYDROP~x) &\stepto& S'; F; \epsilon
\end{array}
\\ \qquad
\begin{array}[j]{@{}r@{~}l@{}}
(\iff & F.\AMODULE.\MIDATAS[x] = da \\
\wedge & S' = S \with \SDATA[da] = \epsilon) \\
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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).

\end{array}
\end{array}


.. _exec-memory.copy:

:math:`\MEMORYCOPY`
...................

1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.

2. Assert: due to :ref:`validation <valid-memory.init>`, :math:`F.\AMODULE.\MIMEMS[0]` exists.

3. Let :math:`ma` be the :ref:`memory address <syntax-memaddr>` :math:`F.\AMODULE.\MIMEMS[0]`.

4. Assert: due to :ref:`validation <valid-memory.init>`, :math:`S.\SMEMS[ma]` exists.

5. Let :math:`\X{mem}` be the :ref:`memory instance <syntax-meminst>` :math:`S.\SMEMS[ma]`.

6. Let :math:`sz` be the length of :math:`\X{mem}.\MIDATA`.

7. Assert: due to :ref:`validation <valid-memory.init>`, three values of :ref:`value type <syntax-valtype>` |I32| are on the top of the stack.

8. Pop the value :math:`\I32.\CONST~i` from the stack.

9. Pop the value :math:`\I32.\CONST~j` from the stack.

10. Pop the value :math:`\I32.\CONST~n` from the stack.

11. If :math:`i + n > sz`, then:

a. Trap.

12. If :math:`j + n > sz`, then:

a. Trap.

13. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[i \slice n]`.

14. :ref:`Initialize <initdata>` the memory instance at address :math:`ma` starting from offset :math:`j` with the byte sequence :math:`b^\ast`.

.. math::
~\\[-1ex]
\begin{array}{l}
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\MEMORYCOPY) &\stepto& S; F; (\INITDATA~ma~j~b^\ast)
\end{array}
\\ \qquad
\begin{array}[j]{@{}r@{~}l@{}}
(\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]) \\
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

\end{array}
\\[1ex]
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\MEMORYCOPY) &\stepto& S; F; \TRAP
\end{array}
\\ \qquad
(\otherwise)
\end{array}

.. TODO: The semantics here describe making a copy of the source memory before
the writing begins. This is probably OK for now but will need to be updated
when threads are added.


.. index:: memory, memory instance, memory address, initialize memory
.. _initdata:

:math:`\INITDATA~\memaddr~o~b^\ast`
...................................

1. For each byte :math:`b_i` of :math:`b^\ast`:

a. Replace :math:`S.\SMEMS[\memaddr].\MIDATA[o + i]` with :math:`b_i`.

.. math::
~\\[-1ex]
\begin{array}{l}
\begin{array}{lcl@{\qquad}l}
S; F; \INITDATA~\memaddr~o~\epsilon &\stepto& S; F; \epsilon \\
S; F; \INITDATA~\memaddr~o~(b_0~b^\ast) &\stepto& S'; F; \INITDATA~\memaddr~(o+1)~b^\ast
\end{array}
\\ \qquad
(\iff S' = S \with \SMEMS[\memaddr].\MIDATA[o] = b_0) \\
\end{array}


Table Instructions
~~~~~~~~~~~~~~~~~~

.. _exec-table.init:

:math:`\TABLEINIT~x`
..................

1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.

2. Assert: due to :ref:`validation <valid-table.init>`, :math:`F.\AMODULE.\MITABLES[0]` exists.

3. Let :math:`ta` be the :ref:`table address <syntax-tableaddr>` :math:`F.\AMODULE.\MITABLES[0]`.

4. Assert: due to :ref:`validation <valid-table.init>`, :math:`S.\STABLES[ta]` exists.

5. Let :math:`\X{table}` be the :ref:`table instance <syntax-tableinst>` :math:`S.\STABLES[ta]`.

6. Let :math:`tsz` be the length of :math:`\X{table}.\TIELEM`.

7. Assert: due to :ref:`validation <valid-table.init>`, :math:`F.\AMODULE.\MIELEMS[x]` exists.

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

9. If :math:`S.\SELEM[ea]` is :math:`\epsilon`, then:

a. Trap.

10. Let :math:`\X{elem}` be the :ref:`element segment instance <syntax-eleminst>` :math:`S.\SELEM[ea]`.

11. Assert: due to :ref:`validation <valid-table.init>`, three values of :ref:`value type <syntax-valtype>` |I32| are on the top of the stack.

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

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

14. Pop the value :math:`\I32.\CONST~n` from the stack.

15. Let :math:`esz` be the length of :math:`\X{elem}.\EIINIT`.

16. If :math:`i + n > esz`, then:

a. Trap.

17. If :math:`j + n > tsz`, then:

a. Trap.

18. Let :math:`y^\ast` be the function address sequence :math:`\X{elem}.\EIINIT[i \slice n]`.

19. :ref:`Initialize <initelem>` the table instance at address :math:`ta` starting from offset :math:`j` with the function address sequence :math:`y^\ast`.

.. math::
~\\[-1ex]
\begin{array}{l}
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\TABLEINIT~x) &\stepto& S; F; (\INITELEM~ta~j~y^\ast)
\end{array}
\\ \qquad
\begin{array}[j]{@{}r@{~}l@{}}
(\iff & F.\AMODULE.\MITABLES[0] = ta \\
\wedge & F.\AMODULE.\MIELEMS[x] = ea \\
\wedge & S.\SELEM[ea] \neq \epsilon \\
\wedge & (i + n \leq |S.\SELEM[ea].\EIINIT|) \\
\wedge & (j + n \leq |S.\STABLES[ta].\TIELEM|) \\
\wedge & y^\ast = S.\SELEM[ea].\EIINIT[i \slice n]) \\
\end{array}
\\[1ex]
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\TABLEINIT~x) &\stepto& S; F; \TRAP
\end{array}
\\ \qquad
(\otherwise)
\end{array}


.. _exec-table.drop:

:math:`\TABLEDROP~x`
.....................

1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.

2. Assert: due to :ref:`validation <valid-table.drop>`, :math:`F.\AMODULE.\MIELEMS[x]` exists.

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

4. Replace :math:`S.\SELEM[ea]` with :math:`\epsilon`.

.. math::
~\\[-1ex]
\begin{array}{l}
\begin{array}{lcl@{\qquad}l}
S; F; (\TABLEDROP~x) &\stepto& S'; F; \epsilon
\end{array}
\\ \qquad
\begin{array}[j]{@{}r@{~}l@{}}
(\iff & F.\AMODULE.\MIELEMS[x] = ea \\
\wedge & S' = S \with \SELEM[ea] = \epsilon) \\
\end{array}
\end{array}


.. _exec-table.copy:

:math:`\TABLECOPY`
...................

1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.

2. Assert: due to :ref:`validation <valid-table.init>`, :math:`F.\AMODULE.\MITABLES[0]` exists.

3. Let :math:`ta` be the :ref:`table address <syntax-tableaddr>` :math:`F.\AMODULE.\MITABLES[0]`.

4. Assert: due to :ref:`validation <valid-table.init>`, :math:`S.\STABLES[ta]` exists.

5. Let :math:`\X{table}` be the :ref:`table instance <syntax-tableinst>` :math:`S.\STABLES[ta]`.

6. Let :math:`sz` be the length of :math:`\X{table}.\TIELEM`.

7. Assert: due to :ref:`validation <valid-table.init>`, three values of :ref:`value type <syntax-valtype>` |I32| are on the top of the stack.

8. Pop the value :math:`\I32.\CONST~i` from the stack.

9. Pop the value :math:`\I32.\CONST~j` from the stack.

10. Pop the value :math:`\I32.\CONST~n` from the stack.

11. If :math:`i + n > sz`, then:

a. Trap.

12. If :math:`j + n > sz`, then:

a. Trap.

13. Let :math:`y^\ast` be the function address sequence :math:`\X{table}.\TIELEM[i \slice n]`.

14. :ref:`Initialize <initelem>` the table instance at address :math:`ta` starting from offset :math:`j` with the function address sequence :math:`y^\ast`.

.. math::
~\\[-1ex]
\begin{array}{l}
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\TABLECOPY) &\stepto& S; F; (\INITELEM~ta~j~y^\ast)
\end{array}
\\ \qquad
\begin{array}[j]{@{}r@{~}l@{}}
(\iff & F.\AMODULE.\MITABLES[0] = ta \\
\wedge & (i + n \leq |S.\STABLES[ta].\TIELEM|) \\
\wedge & (j + n \leq |S.\STABLES[ta].\TIELEM|) \\
\wedge & y^\ast = S.\STABLES[ta].\TIELEM[i \slice n]) \\
\end{array}
\\[1ex]
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\TABLECOPY) &\stepto& S; F; \TRAP
\end{array}
\\ \qquad
(\otherwise)
\end{array}


.. index:: table, table instance, table address, initialize table
.. _initelem:

:math:`\INITELEM~\tableaddr~o~a^\ast`
.....................................

1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.

2. For each :ref:`function address <syntax-funcaddr>` :math:`x_i` of :math:`a^\ast`:

a. Replace :math:`S.\STABLES[\tableaddr].\TIELEM[o + i]` with :math:`x_i`.

.. math::
~\\[-1ex]
\begin{array}{l}
\begin{array}{lcl@{\qquad}l}
S; F; \INITELEM~\tableaddr~o~\epsilon &\stepto& S; F; \epsilon & \\
S; F; \INITELEM~\tableaddr~o~(a_0~a^\ast) &\stepto& S'; F; \INITELEM~\tableaddr~(o+1)~a^\ast
\end{array}
\\ \qquad
(\iff S' = S \with \STABLES[\tableaddr].\TIELEM[o] = a_0) \\
\end{array}


.. index:: control instructions, structured control, label, block, branch, result type, label index, function index, type index, vector, address, table address, table instance, store, frame
pair: execution; instruction
single: abstract syntax; instruction
Expand Down
Loading