Skip to content

Allow atomic operations on unshared memories #147

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Jan 30, 2020
Merged

Allow atomic operations on unshared memories #147

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f99ef27
Allow atomic operations on unshared memories
tlively Dec 18, 2019
743ebcf
Do not require shared memory in formal semantics
tlively Jan 23, 2020
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
40 changes: 10 additions & 30 deletions document/core/valid/instructions.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -440,15 +440,13 @@ 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|.
Copy link
Member

Choose a reason for hiding this comment

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

You'll also need to adjust the respective premise in the formal rule below to keep it in sync, e.g., by changing C.\CMEMS[0] = \limits~\MSHARED to C.\CMEMS[0] = \memtype (here and elsewhere).


* The alignment :math:`2^{\memarg.\ALIGN}` must be equal to :math:`4`.

* Then the instruction is valid with type :math:`[\I32~\I64] \to [\I64]`.

.. math::
\frac{
C.\CMEMS[0] = \limits~\MSHARED
C.\CMEMS[0] = \memtype
\qquad
2^{\memarg.\ALIGN} = 4
}{
Expand All @@ -464,15 +462,13 @@ 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]`.

.. math::
\frac{
C.\CMEMS[0] = \limits~\MSHARED
C.\CMEMS[0] = \memtype
\qquad
2^{\memarg.\ALIGN} = |t|/8
}{
Expand All @@ -488,15 +484,13 @@ 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]`.

.. math::
\frac{
C.\CMEMS[0] = \limits~\MSHARED
C.\CMEMS[0] = \memtype
\qquad
2^{\memarg.\ALIGN} = |t|/8
}{
Expand All @@ -513,15 +507,13 @@ 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]`.

.. math::
\frac{
C.\CMEMS[0] = \limits~\MSHARED
C.\CMEMS[0] = \memtype
\qquad
2^{\memarg.\ALIGN} = N/8
}{
Expand All @@ -538,15 +530,13 @@ 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 []`.

.. math::
\frac{
C.\CMEMS[0] = \limits~\MSHARED
C.\CMEMS[0] = \memtype
\qquad
2^{\memarg.\ALIGN} = |t|/8
}{
Expand All @@ -563,15 +553,13 @@ 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 []`.

.. math::
\frac{
C.\CMEMS[0] = \limits~\MSHARED
C.\CMEMS[0] = \memtype
\qquad
2^{\memarg.\ALIGN} = N/8
}{
Expand All @@ -588,15 +576,13 @@ 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]`.

.. math::
\frac{
C.\CMEMS[0] = \limits~\MSHARED
C.\CMEMS[0] = \memtype
\qquad
2^{\memarg.\ALIGN} = |t|/8
}{
Expand All @@ -612,15 +598,13 @@ 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]`.

.. math::
\frac{
C.\CMEMS[0] = \limits~\MSHARED
C.\CMEMS[0] = \memtype
\qquad
2^{\memarg.\ALIGN} = N/8
}{
Expand All @@ -636,15 +620,13 @@ 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]`.

.. math::
\frac{
C.\CMEMS[0] = \limits~\MSHARED
C.\CMEMS[0] = \memtype
\qquad
2^{\memarg.\ALIGN} = |t|/8
}{
Expand All @@ -660,15 +642,13 @@ 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]`.

.. math::
\frac{
C.\CMEMS[0] = \limits~\MSHARED
C.\CMEMS[0] = \memtype
\qquad
2^{\memarg.\ALIGN} = N/8
}{
Expand Down
1 change: 1 addition & 0 deletions interpreter/exec/eval.ml
View file
Open in desktop
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
Open in desktop
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
1 change: 1 addition & 0 deletions proposals/threads/Globals.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@

# Import/Export mutable globals proposal

This has been separated into
Expand Down
36 changes: 19 additions & 17 deletions proposals/threads/Overview.md
View file
Open in desktop
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