Spec basic instructions #170

rossberg · 2020-11-18T15:57:46Z

This updates the spec for load, store, rmw, memory.size & .grow instructions.

Refactor and extend formal rules to allow atomic instructions on unshared memory.
Complete redo of rmw rules.
Update prose spec everywhere.
Various fixes and clean-ups.

rossberg · 2020-11-18T16:26:57Z

Unfortunately, it looks like MathJax is messing up the notation pretty badly. I tried a few quick hacks, but to no avail. Leaving that problem for later.

rossberg · 2020-11-19T17:28:12Z

@conrad-watt, PTAL.

conrad-watt

Main issue currently is the behaviour of cmpxchg.

After this PR, I believe the next steps are to add fence and flesh out the semantics of wait/notify?

conrad-watt · 2020-11-21T13:39:20Z

document/core/appendix/index-instructions.rst

@@ -215,70 +215,70 @@ Instruction                                                  Binary Opcode
 :math:`\I64.\TRUNC\K{\_sat}\_\F64\K{\_s}`                    :math:`\hex{FC}~~6`        :math:`[\F64] \to [\I64]`                      :ref:`validation <valid-cvtop>`                :ref:`execution <exec-cvtop>`, :ref:`operator <op-trunc_sat_s>`
 :math:`\I64.\TRUNC\K{\_sat\_}\F64\K{\_u}`                    :math:`\hex{FC}~~7`        :math:`[\F64] \to [\I64]`                      :ref:`validation <valid-cvtop>`                :ref:`execution <exec-cvtop>`, :ref:`operator <op-trunc_sat_u>`
 (reserved)                                                   :math:`\hex{FD}`                                                                                                                                                                        
-:math:`\MEMORYATOMICNOTIFY~\memarg`                          :math:`\hex{FE}~\hex{00}`  :math:`[\I32~\I64] \to [\I64]`                 :ref:`validation <valid-atomic-notify>`                                                                       


When I try to build this page, I get

<path>/index-instructions.rst: WARNING: Malformed table. Text in column margin in table line 210.

It shows up as blank in the built web document.

Oops, forgot to rerun the generator script (this ought to be automatic once we rebase on the main spec repo).

conrad-watt · 2020-11-21T13:45:15Z

document/core/exec/runtime.rst

@@ -174,7 +174,7 @@ Syntactically, a local store is defined as a :ref:`map <notation-map>` from know
     \globalinst \\
   \end{array}

-It is an invariant of the semantics that none of the memory instances :math:`\meminst` in a store is :math:`shared <syntax-shared>`.
+It is an invariant of the semantics that none of the memory instances :math:`\meminst` in a store is :ref:`shared <syntax-shared>`.


maybe clarify "none of the memory instances in a local store..."

conrad-watt · 2020-11-21T13:46:19Z

document/core/exec/runtime.rst

@@ -780,7 +780,7 @@ The following structural rule for global reduction delegates to local reduction
       \begin{array}[t]{@{}r@{~}l@{}}


A few lines up (missed earlier) "Formally, glboal reduction is a relation"

conrad-watt · 2020-11-21T13:51:22Z

document/core/valid/instructions.rst

@@ -431,228 +431,212 @@ Memory Instructions
 Atomic Memory Instructions
 ~~~~~~~~~~~~~~~~~~~~~~~~~~



Maybe add an explanatory note that atomic ops don't need to be on shared memory.

Hm, decided not to, since it should be pretty clear from the rules and the spec generally avoids design discussions beyond clarifications.

conrad-watt · 2020-11-21T13:58:08Z

document/core/valid/instructions.rst

   }{
-     C \vdash t\K{.}\ATOMICRMW\K{.}\ATOMICCMPXCHG~\memarg : [\I32~t~t] \to [t]
+     C \vdash \MEMORYATOMICNOTIFY~\memarg : [\I32~\I64] \to [\I64]


I should have caught this earlier, but I'm almost certain that the type of notify should be i32 i32 -> i32. This is what's specified in the overvew. I checked that Binaryen also expects this.

Yes, the current reduction rules also match that, fixed.

However, the reduction rule for wait seem to have the operand order reversed relative to both validation and overview. Added a todo.

conrad-watt · 2020-11-21T14:26:29Z

document/core/exec/instructions.rst


-    b. Let :math:`b^\ast_w` be the byte sequence :math:`\bytes_{\iN}(n)`.
+    c. Perform the atomic :ref:`action <syntax-act>` :math:`(\ARMW_{\ord}~a.\LDATA[\X{ea}]~b_{\F{r}}^\ast~b_{\F{r}}^\ast)` to read the bytes :math:`b_{\F{r}}^\ast` from data offset :math:`\X{ea}` of the shared :ref:`memory instance <syntax-meminst>` at :ref:`memory address <syntax-memaddr>` :math:`a` and replace them with bytes :math:`b_{\F{w}}^\ast` (which are defined below).


The ord subscript is never defined (should just be atomic/sc).

Also, b_r* seems to be repeated twice when the second component should be b_w* (copy-paste nit).

Both fixed.

conrad-watt · 2020-11-21T14:29:30Z

document/core/exec/instructions.rst


-17. Let :math:`c_1` be the integer for which :math:`bytes_{\iN}(m) = b^\ast_r`.
+    c. Perform the atomic :ref:`action <syntax-act>` :math:`(\ARMW_{\ord}~a.\LDATA[\X{ea}]~b_{\F{r}}^\ast~b_{\F{r}}^\ast)` to read the bytes :math:`b_{\F{r}}^\ast` from data offset :math:`\X{ea}` of the shared :ref:`memory instance <syntax-meminst>` at :ref:`memory address <syntax-memaddr>` :math:`a` and replace them with bytes :math:`b_{\F{w}}^\ast` (which are defined below).


rmw copy-paste nit replicated here (although as described above this section needs to change).

conrad-watt · 2020-11-21T14:31:18Z

document/core/exec/instructions.rst


-:math:`t\K{.}\ATOMICRMW{.}\ATOMICCMPXCHG~\memarg` and :math:`t\K{.}\ATOMICRMW{N}\K{\_u.}\ATOMICCMPXCHG~\memarg`
-...............................................................................................................
+:math:`t\K{.}\ATOMICRMW({N}\K{\_u})^?\K{.}\ATCMPXCHG~\memarg`


High-level:

cmpxchg should only perform an rmw action if the comparison succeeds. This means that at the operational level, the instruction non-deterministically either emits an atomic read action where the observed value is != the argument, or an rmw action where the read value is == the argument. The difference is observable unfortunately (due to the total ordering on atomics) so it's not enough to write back the same value.

EDIT: also noticed that the text format doesn't seem to pop the right number of arguments?

Huh, the JS spec also models compareExchange as an rmw even if the comparison fails. I'll double check, but I'm pretty sure that's not correct.

C++11 models it as just a load in the failure case, so I think this is also a JS spec bug.

Fixed the missing pop and added a todo for changing the semantics of the RMW (awaiting resolution?).

currently under discussion tc39/ecma262#2231

conrad-watt · 2020-11-21T14:34:31Z

document/core/exec/instructions.rst

+
+    c. Perform the :ref:`action <syntax-act>` :math:`(\ARD_{\ord}~a.\LDATA[\X{ea}]~b^\ast)` to read the bytes :math:`b^\ast` from data offset :math:`\X{ea}` of the shared :ref:`memory instance <syntax-meminst>` at :ref:`memory address <syntax-memaddr>` :math:`a`.
+
+11. If :math:`N` and :math:`\sx` are part of the instruction, then:


can conditionals like this be factored more like the formal semantics?

i.e. have a few preamble lines that state
"1. N = |t| if N is not part of the instruction"

some of the RMWs especially have a lot of case-splitting in the text on this

Done. Also extended numerics section to actually have bytes_iN and friends defined.

conrad-watt · 2020-11-21T14:38:18Z

document/core/exec/instructions.rst


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


the "try growing memory" text in the non-shared case above was always informal language. Could some of that flavour be added to this case too? i.e.

a. Either: memory growth succeeds. ... let bla bla bla b. Or: memory growth fails. ... bla bla bla

rossberg

Thanks for the thorough review! Yes, I think the next steps will be wait/notify/fence. Do you want to proceed with those?

rossberg · 2020-11-23T12:46:27Z

document/core/appendix/index-instructions.rst

@@ -215,70 +215,70 @@ Instruction                                                  Binary Opcode
 :math:`\I64.\TRUNC\K{\_sat}\_\F64\K{\_s}`                    :math:`\hex{FC}~~6`        :math:`[\F64] \to [\I64]`                      :ref:`validation <valid-cvtop>`                :ref:`execution <exec-cvtop>`, :ref:`operator <op-trunc_sat_s>`
 :math:`\I64.\TRUNC\K{\_sat\_}\F64\K{\_u}`                    :math:`\hex{FC}~~7`        :math:`[\F64] \to [\I64]`                      :ref:`validation <valid-cvtop>`                :ref:`execution <exec-cvtop>`, :ref:`operator <op-trunc_sat_u>`
 (reserved)                                                   :math:`\hex{FD}`                                                                                                                                                                        
-:math:`\MEMORYATOMICNOTIFY~\memarg`                          :math:`\hex{FE}~\hex{00}`  :math:`[\I32~\I64] \to [\I64]`                 :ref:`validation <valid-atomic-notify>`                                                                       


Oops, forgot to rerun the generator script (this ought to be automatic once we rebase on the main spec repo).

rossberg · 2020-11-23T12:48:10Z

document/core/exec/instructions.rst

@@ -381,7 +381,7 @@ Memory Instructions
 ~~~~~~~~~~~~~~~~~~~

 .. note::
-   The alignment :math:`\memarg.\ALIGN` in load and store instructions does not affect the semantics.
+   The alignment :math:`\memarg.\ALIGN` in load and store instructions does not affect the semantics of accesses to :ref:`unshared <syntax-unshared>` :ref:`memories <syntax-mem>`.


Yes, fixed.

rossberg · 2020-11-23T12:48:26Z

document/core/exec/instructions.rst


-:math:`t\K{.}\ATOMIC^?.\LOAD~\memarg` and :math:`t\K{.}\ATOMIC^?.\LOAD{N}\K{\_}\sx~\memarg`
-...........................................................................................
+:math:`t\K{.}\LOAD{N}(\K{\_}\sx)^?~\memarg`


rossberg · 2020-11-23T13:26:46Z

document/core/exec/instructions.rst

+
+    c. Perform the :ref:`action <syntax-act>` :math:`(\ARD_{\ord}~a.\LDATA[\X{ea}]~b^\ast)` to read the bytes :math:`b^\ast` from data offset :math:`\X{ea}` of the shared :ref:`memory instance <syntax-meminst>` at :ref:`memory address <syntax-memaddr>` :math:`a`.
+
+11. If :math:`N` and :math:`\sx` are part of the instruction, then:


Done. Also extended numerics section to actually have bytes_iN and friends defined.

rossberg · 2020-11-23T13:40:18Z

document/core/exec/instructions.rst

+
+5. Else:
+
+   a. Perform the :ref:`action <syntax-act>` :math:`(\ARD~a.\LLEN~n)` to read the length :math:`n` of the shared :ref:`memory instance <syntax-meminst>` at :ref:`memory address <syntax-memaddr>` :math:`a`.


rossberg · 2020-11-23T13:50:35Z

document/core/exec/instructions.rst


-:math:`t\K{.}\ATOMICRMW{.}\ATOMICCMPXCHG~\memarg` and :math:`t\K{.}\ATOMICRMW{N}\K{\_u.}\ATOMICCMPXCHG~\memarg`
-...............................................................................................................
+:math:`t\K{.}\ATOMICRMW({N}\K{\_u})^?\K{.}\ATCMPXCHG~\memarg`


Fixed the missing pop and added a todo for changing the semantics of the RMW (awaiting resolution?).

rossberg · 2020-11-23T13:51:22Z

document/core/exec/runtime.rst

@@ -174,7 +174,7 @@ Syntactically, a local store is defined as a :ref:`map <notation-map>` from know
     \globalinst \\
   \end{array}

-It is an invariant of the semantics that none of the memory instances :math:`\meminst` in a store is :math:`shared <syntax-shared>`.
+It is an invariant of the semantics that none of the memory instances :math:`\meminst` in a store is :ref:`shared <syntax-shared>`.


rossberg · 2020-11-23T13:52:04Z

document/core/exec/runtime.rst

@@ -780,7 +780,7 @@ The following structural rule for global reduction delegates to local reduction
       \begin{array}[t]{@{}r@{~}l@{}}


rossberg · 2020-11-23T13:56:52Z

document/core/valid/instructions.rst

@@ -431,228 +431,212 @@ Memory Instructions
 Atomic Memory Instructions
 ~~~~~~~~~~~~~~~~~~~~~~~~~~



Hm, decided not to, since it should be pretty clear from the rules and the spec generally avoids design discussions beyond clarifications.

rossberg · 2020-11-23T14:03:27Z

document/core/valid/instructions.rst

   }{
-     C \vdash t\K{.}\ATOMICRMW\K{.}\ATOMICCMPXCHG~\memarg : [\I32~t~t] \to [t]
+     C \vdash \MEMORYATOMICNOTIFY~\memarg : [\I32~\I64] \to [\I64]


Yes, the current reduction rules also match that, fixed.

However, the reduction rule for wait seem to have the operand order reversed relative to both validation and overview. Added a todo.

conrad-watt

Just a few nits.

I can look at fence/wait/notify in the next couple of weeks, but I really need to submit my thesis so I'm finding it hard to manage my time.

conrad-watt · 2020-11-25T15:25:13Z

document/core/appendix/index-instructions.rst

+:math:`\I64.\TRUNC\K{\_sat}\_\F64\K{\_s}`                :math:`\hex{FC}~~6`        :math:`[\F64] \to [\I64]`                      :ref:`validation <valid-cvtop>`                 :ref:`execution <exec-cvtop>`, :ref:`operator <op-trunc_sat_s>`
+:math:`\I64.\TRUNC\K{\_sat\_}\F64\K{\_u}`                :math:`\hex{FC}~~7`        :math:`[\F64] \to [\I64]`                      :ref:`validation <valid-cvtop>`                 :ref:`execution <exec-cvtop>`, :ref:`operator <op-trunc_sat_u>`
+(reserved)                                               :math:`\hex{FD}`                                                                                                                                                                         
+:math:`\MEMORYATOMICNOTIFY~\memarg`                      :math:`\hex{FE}~\hex{00}`  :math:`[\I32~\I64] \to [\I64]`                 :ref:`validation <valid-memory.atomic.notify>`                                                                 


Notify still has the incorrect type here.

conrad-watt · 2020-11-25T15:39:26Z

document/core/exec/instructions.rst


-2. Assert: due to :ref:`validation <valid-loadn>`, :math:`F.\AMODULE.\MIMEMS[0]` exists.
+   a. Let :math:`\X{st}` be the :ref:`pro forma type <aux-bytes>` :math:`\iN`.


Is the <aux-bytes> link association correct? I'd have expected this to link to the definition of storage types in numerics but it seems to jump me to a different section.

Also, it might be clearer to call this a "storage type" rather than a "pro forma type".

conrad-watt · 2020-11-25T15:44:03Z

document/core/exec/instructions.rst

-13. Else:
+11. Else:
+
+    a. Perform the :ref:`action <syntax-act>` :math:`(\ARD~a.\LLEN~n)` to read the length :math:`n` of the shared :ref:`memory instance <syntax-meminst>` at :ref:`memory address <syntax-memaddr>` :math:`a`.


Need to make sure that the length of b* matches the width of the load (same in formal semantics).

sorry, this comment should have been at line 439 just below

Made explicit in the prose. In the formal semantics that's implicit by the side conditions, particularly, its use as an argument to bytes^-1.

conrad-watt · 2020-11-25T15:46:17Z

document/core/exec/instructions.rst


-2. Assert: due to :ref:`validation <valid-storen>`, :math:`F.\AMODULE.\MIMEMS[0]` exists.
+   a. Let :math:`\X{st}` be the :ref:`pro forma type <aux-bytes>` :math:`\iN`.


same as above

conrad-watt · 2020-11-25T15:47:57Z

document/core/exec/instructions.rst


-2. Assert: due to :ref:`validation <valid-atomic-rmwn>`, :math:`F.\AMODULE.\MIMEMS[0]` exists.
+   a. Let :math:`\X{st}` be the :ref:`pro forma type <aux-bytes>` :math:`\iN`.


conrad-watt · 2020-11-25T15:48:58Z

document/core/exec/instructions.rst


-19. Replace the bytes :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]` with :math:`b^\ast_w`.
+    c. Perform the atomic :ref:`action <syntax-act>` :math:`(\ARMW_{\SEQCST}~a.\LDATA[\X{ea}]~b_{\F{r}}^\ast~b_{\F{w}}^\ast)` to read the bytes :math:`b_{\F{r}}^\ast` from data offset :math:`\X{ea}` of the shared :ref:`memory instance <syntax-meminst>` at :ref:`memory address <syntax-memaddr>` :math:`a` and replace them with bytes :math:`b_{\F{w}}^\ast` (which are defined below).


again, need to ensure that b_r* has the right length (does length of b_w* follow as numeric invariant?)

Fixed as above. (Yes, for b*_w this follows from the definition of bytes_st.)

conrad-watt · 2020-11-25T15:49:48Z

document/core/exec/instructions.rst

+     \wedge & \X{ea} + N/8 \leq n \\
+     \wedge & \X{ea} \mod N/8 = 0 \\
+     \wedge & c_1 = \extendtu_{\X{st},t}(\bytes^{-1}_{\X{st}}(b_{\F{r}}^\ast)) \\
+     \wedge & b_{\F{r}}^\ast = \bytes_{\X{st}}(\wrapt_{t,\X{st}}(\atop_t(c_1, c_2)))) \\


think this should be b_w*

conrad-watt · 2020-11-25T15:50:20Z

document/core/exec/instructions.rst


-:math:`t\K{.}\ATOMICRMW{.}\ATOMICCMPXCHG~\memarg` and :math:`t\K{.}\ATOMICRMW{N}\K{\_u.}\ATOMICCMPXCHG~\memarg`
-...............................................................................................................
+:math:`t\K{.}\ATOMICRMW({N}\K{\_u})^?\K{.}\ATCMPXCHG~\memarg`


currently under discussion tc39/ecma262#2231

conrad-watt · 2020-11-25T15:50:32Z

document/core/exec/instructions.rst


-2. Assert: due to :ref:`validation <valid-atomic-rmwn-cmpxchg>`, :math:`F.\AMODULE.\MIMEMS[0]` exists.
+   a. Let :math:`\X{st}` be the :ref:`pro forma type <aux-bytes>` :math:`\iN`.


same as above

conrad-watt · 2020-11-25T15:50:54Z

document/core/exec/instructions.rst

+
+       i. Trap.
+
+    c. Perform the atomic :ref:`action <syntax-act>` :math:`(\ARMW_{\SEQCST}~a.\LDATA[\X{ea}]~b_{\F{r}}^\ast~b_{\F{w}}^\ast)` to read the bytes :math:`b_{\F{r}}^\ast` from data offset :math:`\X{ea}` of the shared :ref:`memory instance <syntax-meminst>` at :ref:`memory address <syntax-memaddr>` :math:`a` and replace them with bytes :math:`b_{\F{w}}^\ast` (which are defined below).


same as above

rossberg

Thanks! No stress, I thought your thesis was already due in September.

rossberg · 2020-11-26T07:57:04Z

document/core/appendix/index-instructions.rst

+:math:`\I64.\TRUNC\K{\_sat}\_\F64\K{\_s}`                :math:`\hex{FC}~~6`        :math:`[\F64] \to [\I64]`                      :ref:`validation <valid-cvtop>`                 :ref:`execution <exec-cvtop>`, :ref:`operator <op-trunc_sat_s>`
+:math:`\I64.\TRUNC\K{\_sat\_}\F64\K{\_u}`                :math:`\hex{FC}~~7`        :math:`[\F64] \to [\I64]`                      :ref:`validation <valid-cvtop>`                 :ref:`execution <exec-cvtop>`, :ref:`operator <op-trunc_sat_u>`
+(reserved)                                               :math:`\hex{FD}`                                                                                                                                                                         
+:math:`\MEMORYATOMICNOTIFY~\memarg`                      :math:`\hex{FE}~\hex{00}`  :math:`[\I32~\I64] \to [\I64]`                 :ref:`validation <valid-memory.atomic.notify>`                                                                 


rossberg · 2020-11-26T08:01:04Z

document/core/exec/instructions.rst


-2. Assert: due to :ref:`validation <valid-loadn>`, :math:`F.\AMODULE.\MIMEMS[0]` exists.
+   a. Let :math:`\X{st}` be the :ref:`pro forma type <aux-bytes>` :math:`\iN`.


rossberg · 2020-11-26T08:06:07Z

document/core/exec/instructions.rst

-13. Else:
+11. Else:
+
+    a. Perform the :ref:`action <syntax-act>` :math:`(\ARD~a.\LLEN~n)` to read the length :math:`n` of the shared :ref:`memory instance <syntax-meminst>` at :ref:`memory address <syntax-memaddr>` :math:`a`.


Made explicit in the prose. In the formal semantics that's implicit by the side conditions, particularly, its use as an argument to bytes^-1.

rossberg · 2020-11-26T08:06:44Z

document/core/exec/instructions.rst


-2. Assert: due to :ref:`validation <valid-storen>`, :math:`F.\AMODULE.\MIMEMS[0]` exists.
+   a. Let :math:`\X{st}` be the :ref:`pro forma type <aux-bytes>` :math:`\iN`.


rossberg · 2020-11-26T08:08:47Z

document/core/exec/instructions.rst


-2. Assert: due to :ref:`validation <valid-atomic-rmwn>`, :math:`F.\AMODULE.\MIMEMS[0]` exists.
+   a. Let :math:`\X{st}` be the :ref:`pro forma type <aux-bytes>` :math:`\iN`.


rossberg · 2020-11-26T08:11:26Z

document/core/exec/instructions.rst


-19. Replace the bytes :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]` with :math:`b^\ast_w`.
+    c. Perform the atomic :ref:`action <syntax-act>` :math:`(\ARMW_{\SEQCST}~a.\LDATA[\X{ea}]~b_{\F{r}}^\ast~b_{\F{w}}^\ast)` to read the bytes :math:`b_{\F{r}}^\ast` from data offset :math:`\X{ea}` of the shared :ref:`memory instance <syntax-meminst>` at :ref:`memory address <syntax-memaddr>` :math:`a` and replace them with bytes :math:`b_{\F{w}}^\ast` (which are defined below).


Fixed as above. (Yes, for b*_w this follows from the definition of bytes_st.)

rossberg · 2020-11-26T08:12:08Z

document/core/exec/instructions.rst

+     \wedge & \X{ea} + N/8 \leq n \\
+     \wedge & \X{ea} \mod N/8 = 0 \\
+     \wedge & c_1 = \extendtu_{\X{st},t}(\bytes^{-1}_{\X{st}}(b_{\F{r}}^\ast)) \\
+     \wedge & b_{\F{r}}^\ast = \bytes_{\X{st}}(\wrapt_{t,\X{st}}(\atop_t(c_1, c_2)))) \\


rossberg · 2020-11-26T08:12:37Z

document/core/exec/instructions.rst


-2. Assert: due to :ref:`validation <valid-atomic-rmwn-cmpxchg>`, :math:`F.\AMODULE.\MIMEMS[0]` exists.
+   a. Let :math:`\X{st}` be the :ref:`pro forma type <aux-bytes>` :math:`\iN`.


rossberg · 2020-11-26T08:13:16Z

document/core/exec/instructions.rst

+
+       i. Trap.
+
+    c. Perform the atomic :ref:`action <syntax-act>` :math:`(\ARMW_{\SEQCST}~a.\LDATA[\X{ea}]~b_{\F{r}}^\ast~b_{\F{w}}^\ast)` to read the bytes :math:`b_{\F{r}}^\ast` from data offset :math:`\X{ea}` of the shared :ref:`memory instance <syntax-meminst>` at :ref:`memory address <syntax-memaddr>` :math:`a` and replace them with bytes :math:`b_{\F{w}}^\ast` (which are defined below).


conrad-watt · 2020-11-26T10:40:20Z

Thanks! No stress, I thought your thesis was already due in September.

yes

conrad-watt

LGTM

Spec basic instructions

eaff5c8

rossberg requested a review from conrad-watt November 18, 2020 15:57

rossberg added 2 commits November 18, 2020 17:49

Forgot atomic stores

1c21d70

Keep sections consistent

4f03457

rossberg force-pushed the instr.basic branch from a4e0fc2 to 4f03457 Compare November 19, 2020 12:45

Redo RMW spec; rule refactorings; various cleanups

43bd60d

conrad-watt requested changes Nov 21, 2020

View reviewed changes

Address comments

8cef096

rossberg commented Nov 23, 2020

View reviewed changes

conrad-watt reviewed Nov 25, 2020

View reviewed changes

More comments

ee78d29

rossberg commented Nov 26, 2020

View reviewed changes

conrad-watt approved these changes Nov 27, 2020

View reviewed changes

rossberg merged commit 3b7a4e9 into master Nov 30, 2020

rossberg deleted the instr.basic branch November 30, 2020 07:58

jakobkummerow mentioned this pull request Jun 11, 2022

atomic.fence is mentioned in the Overview but not in the spec #188

Open

		@@ -780,7 +780,7 @@ The following structural rule for global reduction delegates to local reduction
		\begin{array}[t]{@{}r@{~}l@{}}

		@@ -431,228 +431,212 @@ Memory Instructions
		Atomic Memory Instructions
		~~~~~~~~~~~~~~~~~~~~~~~~~~


		b. Let :math:`b^\ast_w` be the byte sequence :math:`\bytes_{\iN}(n)`.
		c. Perform the atomic :ref:`action <syntax-act>` :math:`(\ARMW_{\ord}~a.\LDATA[\X{ea}]~b_{\F{r}}^\ast~b_{\F{r}}^\ast)` to read the bytes :math:`b_{\F{r}}^\ast` from data offset :math:`\X{ea}` of the shared :ref:`memory instance <syntax-meminst>` at :ref:`memory address <syntax-memaddr>` :math:`a` and replace them with bytes :math:`b_{\F{w}}^\ast` (which are defined below).


		17. Let :math:`c_1` be the integer for which :math:`bytes_{\iN}(m) = b^\ast_r`.
		c. Perform the atomic :ref:`action <syntax-act>` :math:`(\ARMW_{\ord}~a.\LDATA[\X{ea}]~b_{\F{r}}^\ast~b_{\F{r}}^\ast)` to read the bytes :math:`b_{\F{r}}^\ast` from data offset :math:`\X{ea}` of the shared :ref:`memory instance <syntax-meminst>` at :ref:`memory address <syntax-memaddr>` :math:`a` and replace them with bytes :math:`b_{\F{w}}^\ast` (which are defined below).


		c. Perform the :ref:`action <syntax-act>` :math:`(\ARD_{\ord}~a.\LDATA[\X{ea}]~b^\ast)` to read the bytes :math:`b^\ast` from data offset :math:`\X{ea}` of the shared :ref:`memory instance <syntax-meminst>` at :ref:`memory address <syntax-memaddr>` :math:`a`.

		11. If :math:`N` and :math:`\sx` are part of the instruction, then:


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


		5. Else:

		a. Perform the :ref:`action <syntax-act>` :math:`(\ARD~a.\LLEN~n)` to read the length :math:`n` of the shared :ref:`memory instance <syntax-meminst>` at :ref:`memory address <syntax-memaddr>` :math:`a`.


		2. Assert: due to :ref:`validation <valid-loadn>`, :math:`F.\AMODULE.\MIMEMS[0]` exists.
		a. Let :math:`\X{st}` be the :ref:`pro forma type <aux-bytes>` :math:`\iN`.


		19. Replace the bytes :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]` with :math:`b^\ast_w`.
		c. Perform the atomic :ref:`action <syntax-act>` :math:`(\ARMW_{\SEQCST}~a.\LDATA[\X{ea}]~b_{\F{r}}^\ast~b_{\F{w}}^\ast)` to read the bytes :math:`b_{\F{r}}^\ast` from data offset :math:`\X{ea}` of the shared :ref:`memory instance <syntax-meminst>` at :ref:`memory address <syntax-memaddr>` :math:`a` and replace them with bytes :math:`b_{\F{w}}^\ast` (which are defined below).


		i. Trap.

		c. Perform the atomic :ref:`action <syntax-act>` :math:`(\ARMW_{\SEQCST}~a.\LDATA[\X{ea}]~b_{\F{r}}^\ast~b_{\F{w}}^\ast)` to read the bytes :math:`b_{\F{r}}^\ast` from data offset :math:`\X{ea}` of the shared :ref:`memory instance <syntax-meminst>` at :ref:`memory address <syntax-memaddr>` :math:`a` and replace them with bytes :math:`b_{\F{w}}^\ast` (which are defined below).

Spec basic instructions #170

Spec basic instructions #170

Conversation

rossberg commented Nov 18, 2020 • edited Loading

rossberg commented Nov 18, 2020

rossberg commented Nov 19, 2020

conrad-watt 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

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

conrad-watt Nov 21, 2020 • edited Loading

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

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

conrad-watt 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

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

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

conrad-watt commented Nov 26, 2020

conrad-watt left a comment

rossberg commented Nov 18, 2020 •

edited

Loading

conrad-watt Nov 21, 2020 •

edited

Loading