Skip to content

Commit

Permalink
Allow atomic operations on unshared memories
Browse files Browse the repository at this point in the history 
As discussed in the CG on November 12, 2019 and in WebAssembly#144. Specifically,
all atomic accesses are now allowed to validate and execute normally
on unshared memories and wait operations trap when used with unshared
memories.

The PR updates Overview.md and makes a best-effort
attempt at updating the spec, making no changes when there is
already a TODO for updating spec text. It also adds new TODO comments
to the reference interpreter where changes will have to be made.
  • Loading branch information
@tlively
tlively committed Dec 18, 2019
1 parent 4cbecad commit f99ef27
Show file tree
Hide file tree
Showing 4 changed files with 21 additions and 37 deletions.
20 changes: 0 additions & 20 deletions document/core/valid/instructions.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -440,8 +440,6 @@ Atomic Memory Instructions

* Let :math:`\limits~\share` be the :ref:`memory type <syntax-memtype>` :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]`.
Expand All @@ -464,8 +462,6 @@ Atomic Memory Instructions

* Let :math:`\limits~\share` be the :ref:`memory type <syntax-memtype>` :math:`C.\CMEMS[0]`.

* The sharedness :math:`\share` must be |MSHARED|.

* The alignment :math:`2^{\memarg.\ALIGN}` must be equal to the :ref:`width <syntax-valtype>` of :math:`t` divided by :math:`8`.

* Then the instruction is valid with type :math:`[\I32~t~\I64] \to [\I32]`.
Expand All @@ -488,8 +484,6 @@ Atomic Memory Instructions

* Let :math:`\limits~\share` be the :ref:`memory type <syntax-memtype>` :math:`C.\CMEMS[0]`.

* The sharedness :math:`\share` must be |MSHARED|.

* The alignment :math:`2^{\memarg.\ALIGN}` must be equal to the :ref:`width <syntax-valtype>` of :math:`t` divided by :math:`8`.

* Then the instruction is valid with type :math:`[\I32] \to [t]`.
Expand All @@ -513,8 +507,6 @@ Atomic Memory Instructions

* Let :math:`\limits~\share` be the :ref:`memory type <syntax-memtype>` :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]`.
Expand All @@ -538,8 +530,6 @@ Atomic Memory Instructions

* Let :math:`\limits~\share` be the :ref:`memory type <syntax-memtype>` :math:`C.\CMEMS[0]`.

* The sharedness :math:`\share` must be |MSHARED|.

* The alignment :math:`2^{\memarg.\ALIGN}` must be equal to the :ref:`width <syntax-valtype>` of :math:`t` divided by :math:`8`.

* Then the instruction is valid with type :math:`[\I32~t] \to []`.
Expand All @@ -563,8 +553,6 @@ Atomic Memory Instructions

* Let :math:`\limits~\share` be the :ref:`memory type <syntax-memtype>` :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 []`.
Expand All @@ -588,8 +576,6 @@ Atomic Memory Instructions

* Let :math:`\limits~\share` be the :ref:`memory type <syntax-memtype>` :math:`C.\CMEMS[0]`.

* The sharedness :math:`\share` must be |MSHARED|.

* The alignment :math:`2^{\memarg.\ALIGN}` must be equal to the :ref:`width <syntax-valtype>` of :math:`t` divided by :math:`8`.

* Then the instruction is valid with type :math:`[\I32~t] \to [t]`.
Expand All @@ -612,8 +598,6 @@ Atomic Memory Instructions

* Let :math:`\limits~\share` be the :ref:`memory type <syntax-memtype>` :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]`.
Expand All @@ -636,8 +620,6 @@ Atomic Memory Instructions

* Let :math:`\limits~\share` be the :ref:`memory type <syntax-memtype>` :math:`C.\CMEMS[0]`.

* The sharedness :math:`\share` must be |MSHARED|.

* The alignment :math:`2^{\memarg.\ALIGN}` must be equal to the :ref:`width <syntax-valtype>` of :math:`t` divided by :math:`8`.

* Then the instruction is valid with type :math:`[\I32~t~t] \to [t]`.
Expand All @@ -660,8 +642,6 @@ Atomic Memory Instructions

* Let :math:`\limits~\share` be the :ref:`memory type <syntax-memtype>` :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]`.
Expand Down
1 change: 1 addition & 0 deletions interpreter/exec/eval.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions interpreter/valid/valid.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
36 changes: 19 additions & 17 deletions proposals/threads/Overview.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 2<sup>32</sup>, then trap.
Expand Down Expand Up @@ -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`

Expand All @@ -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

Expand Down

0 comments on commit f99ef27

Please sign in to comment.