diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index ba8c3436..f96df09a 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -440,8 +440,6 @@ Atomic Memory Instructions * Let :math:`\limits~\share` be the :ref:`memory type ` :math:`C.\CMEMS[0]`. -* The sharedness :math:`\share` must be |MSHARED|. - * The alignment :math:`2^{\memarg.\ALIGN}` must be equal to :math:`4`. * Then the instruction is valid with type :math:`[\I32~\I64] \to [\I64]`. @@ -464,8 +462,6 @@ Atomic Memory Instructions * Let :math:`\limits~\share` be the :ref:`memory type ` :math:`C.\CMEMS[0]`. -* The sharedness :math:`\share` must be |MSHARED|. - * The alignment :math:`2^{\memarg.\ALIGN}` must be equal to the :ref:`width ` of :math:`t` divided by :math:`8`. * Then the instruction is valid with type :math:`[\I32~t~\I64] \to [\I32]`. @@ -488,8 +484,6 @@ Atomic Memory Instructions * Let :math:`\limits~\share` be the :ref:`memory type ` :math:`C.\CMEMS[0]`. -* The sharedness :math:`\share` must be |MSHARED|. - * The alignment :math:`2^{\memarg.\ALIGN}` must be equal to the :ref:`width ` of :math:`t` divided by :math:`8`. * Then the instruction is valid with type :math:`[\I32] \to [t]`. @@ -513,8 +507,6 @@ Atomic Memory Instructions * Let :math:`\limits~\share` be the :ref:`memory type ` :math:`C.\CMEMS[0]`. -* The sharedness :math:`\share` must be |MSHARED|. - * The alignment :math:`2^{\memarg.\ALIGN}` must be equal to :math:`N/8`. * Then the instruction is valid with type :math:`[\I32] \to [t]`. @@ -538,8 +530,6 @@ Atomic Memory Instructions * Let :math:`\limits~\share` be the :ref:`memory type ` :math:`C.\CMEMS[0]`. -* The sharedness :math:`\share` must be |MSHARED|. - * The alignment :math:`2^{\memarg.\ALIGN}` must be equal to the :ref:`width ` of :math:`t` divided by :math:`8`. * Then the instruction is valid with type :math:`[\I32~t] \to []`. @@ -563,8 +553,6 @@ Atomic Memory Instructions * Let :math:`\limits~\share` be the :ref:`memory type ` :math:`C.\CMEMS[0]`. -* The sharedness :math:`\share` must be |MSHARED|. - * The alignment :math:`2^{\memarg.\ALIGN}` must be equal to :math:`N/8`. * Then the instruction is valid with type :math:`[\I32~t] \to []`. @@ -588,8 +576,6 @@ Atomic Memory Instructions * Let :math:`\limits~\share` be the :ref:`memory type ` :math:`C.\CMEMS[0]`. -* The sharedness :math:`\share` must be |MSHARED|. - * The alignment :math:`2^{\memarg.\ALIGN}` must be equal to the :ref:`width ` of :math:`t` divided by :math:`8`. * Then the instruction is valid with type :math:`[\I32~t] \to [t]`. @@ -612,8 +598,6 @@ Atomic Memory Instructions * Let :math:`\limits~\share` be the :ref:`memory type ` :math:`C.\CMEMS[0]`. -* The sharedness :math:`\share` must be |MSHARED|. - * The alignment :math:`2^{\memarg.\ALIGN}` must be equal to :math:`N/8`. * Then the instruction is valid with type :math:`[\I32~t] \to [t]`. @@ -636,8 +620,6 @@ Atomic Memory Instructions * Let :math:`\limits~\share` be the :ref:`memory type ` :math:`C.\CMEMS[0]`. -* The sharedness :math:`\share` must be |MSHARED|. - * The alignment :math:`2^{\memarg.\ALIGN}` must be equal to the :ref:`width ` of :math:`t` divided by :math:`8`. * Then the instruction is valid with type :math:`[\I32~t~t] \to [t]`. @@ -660,8 +642,6 @@ Atomic Memory Instructions * Let :math:`\limits~\share` be the :ref:`memory type ` :math:`C.\CMEMS[0]`. -* The sharedness :math:`\share` must be |MSHARED|. - * The alignment :math:`2^{\memarg.\ALIGN}` must be equal to :math:`N/8`. * Then the instruction is valid with type :math:`[\I32~t~t] \to [t]`. diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index bce1441b..2420e177 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -277,6 +277,7 @@ let rec step (c : config) : config = with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at]); | AtomicWait {offset; ty; sz; _}, I64 timeout :: ve :: I32 i :: vs' -> + (* TODO: Trap if memory is not shared *) let mem = memory frame.inst (0l @@ e.at) in let addr = I64_convert.extend_i32_u i in (try diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index 0cc8504e..a62149c8 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -137,6 +137,7 @@ let type_cvtop at = function (* Expressions *) +(* TODO: Remove sharability requirements *) let check_memop (c : context) (memop : 'a memop) (sh: sharability option) get_sz at = let MemoryType (_, shared) = memory c (0l @@ at) in diff --git a/proposals/threads/Overview.md b/proposals/threads/Overview.md index 7690b633..57451c88 100644 --- a/proposals/threads/Overview.md +++ b/proposals/threads/Overview.md @@ -228,9 +228,8 @@ This has been separated into ## Atomic Memory Accesses Atomic memory accesses are separated into three categories, load/store, -read-modify-write, and compare-exchange. All atomic memory accesses require a -shared linear memory. Attempting to use atomic access operators on non-shared -linear memory is a validation error. +read-modify-write, and compare-exchange. All atomic memory accesses can be +performed on both shared and unshared linear memories. Currently all atomic memory access instructions are [sequentially consistent][]. Instructions with other memory orderings may be provided in the future. @@ -340,12 +339,12 @@ has any other value than the natural alignment for that access size. ## Wait and Notify operators The notify and wait operators are optimizations over busy-waiting for a value -to change. It is a validation error to use these operators on non-shared linear -memory. The operators have sequentially consistent ordering. +to change. The operators have sequentially consistent ordering. Both notify and wait operators trap if the effective address of either operator -is misaligned or out-of-bounds. The wait operators require an alignment of -their memory access size. The notify operator requires an alignment of 32 bits. +is misaligned or out-of-bounds. Wait operators additionally trap if used on an +unshared linear memory. The wait operators require an alignment of their memory +access size. The notify operator requires an alignment of 32 bits. For the web embedding, the agent can also be suspended or woken via the [`Atomics.wait`][] and [`Atomics.notify`][] functions respectively. An agent @@ -373,14 +372,15 @@ and a relative timeout in nanoseconds as an `i64`. The return value is `0`, | `1` | "not-equal", the loaded value did not match the expected value | | `2` | "timed-out", not woken before timeout expired | -The wait operation begins by performing an atomic load from the given address. -If the loaded value is not equal to the expected value, the operator returns 1 -("not-equal"). If the values are equal, the agent is suspended. If the agent -is woken, the wait operator returns 0 ("ok"). If the timeout expires before -another agent notifies this one, this operator returns 2 ("timed-out"). Note that -when the agent is suspended, it will not be [spuriously woken](https://en.wikipedia.org/wiki/Spurious_wakeup). -The agent is only woken by `atomic.notify` (or [`Atomics.notify`][] in the web -embedding). +If the linear memory is unshared, the wait operation traps. Otherwise, the wait +operation begins by performing an atomic load from the given address. If the +loaded value is not equal to the expected value, the operator returns 1 +("not-equal"). If the values are equal, the agent is suspended. If the agent is +woken, the wait operator returns 0 ("ok"). If the timeout expires before another +agent notifies this one, this operator returns 2 ("timed-out"). Note that when +the agent is suspended, it will not be [spuriously +woken](https://en.wikipedia.org/wiki/Spurious_wakeup). The agent is only woken +by `atomic.notify` (or [`Atomics.notify`][] in the web embedding). When an agent is suspended, if the number of waiters (including this one) is equal to 232, then trap. @@ -424,7 +424,9 @@ no `Int64Array` type, and an ECMAScript `Number` cannot represent all values of The notify operator takes two operands: an address operand and a count as an unsigned `i32`. The operation will notify as many waiters as are waiting on the same effective address, up to the maximum as specified by `count`. The operator -returns the number of waiters that were woken as an unsigned `i32`. +returns the number of waiters that were woken as an unsigned `i32`. Note that if +the notify operator is used with an unshared linear memory, the number of +waiters will always be zero. * `atomic.notify`: notify `count` threads waiting on the given address via `i32.atomic.wait` or `i64.atomic.wait` @@ -441,7 +443,7 @@ For the web embedding, `atomic.notify` is equivalent in behavior to executing th The fence operator, `atomic.fence`, takes no operands, and returns nothing. It is intended to preserve the synchronization guarantees of the [fence operators of higher-level languages](https://en.cppreference.com/w/cpp/atomic/atomic_thread_fence). -Unlike other atomic operators, `atomic.fence` does not target a particular linear memory. It may occur in modules which declare no memory, or a non-shared memory, without causing a validation error. +Unlike other atomic operators, `atomic.fence` does not target a particular linear memory. It may occur in modules which declare no memory without causing a validation error. ## [JavaScript API][] changes