You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardexpand all lines: spec.html
+19-19
Original file line number
Diff line number
Diff line change
@@ -49193,7 +49193,7 @@ <h1>Memory Model Fundamentals</h1>
49193
49193
<tr>
49194
49194
<td>[[NoTear]]</td>
49195
49195
<td>a Boolean</td>
49196
-
<td>Whether this event is allowed to read from multiple write events with equal range as this event.</td>
49196
+
<td>Whether this event is allowed to read from multiple write events with equal memory range as this event.</td>
49197
49197
</tr>
49198
49198
<tr>
49199
49199
<td>[[Block]]</td>
@@ -49230,7 +49230,7 @@ <h1>Memory Model Fundamentals</h1>
49230
49230
<tr>
49231
49231
<td>[[NoTear]]</td>
49232
49232
<td>a Boolean</td>
49233
-
<td>Whether this event is allowed to be read from multiple read events with equal range as this event.</td>
49233
+
<td>Whether this event is allowed to be read from multiple read events with equal memory range as this event.</td>
49234
49234
</tr>
49235
49235
<tr>
49236
49236
<td>[[Block]]</td>
@@ -49303,7 +49303,7 @@ <h1>Memory Model Fundamentals</h1>
49303
49303
</emu-table>
49304
49304
49305
49305
<p>Shared Data Block events are introduced to candidate execution Agent Events Records by abstract operations or by methods on the Atomics object. Some operations also introduce <dfn variants="Synchronize,Synchronize event">Synchronize events</dfn>, which have no fields and exist purely to directly constrain the permitted orderings of other events. And finally, there are host-specific events. A <dfn variants="Memory events">Memory event</dfn> is either a Shared Data Block event, Synchronize event, or such a host-specific event.</p>
49306
-
<p>Let the range of a Shared Data Block event be the Set of contiguous integers from its [[ByteIndex]] to [[ByteIndex]] + [[ElementSize]] - 1. Two events' ranges are equal when the events have the same [[Block]], [[ByteIndex]], and [[ElementSize]]. Two events' ranges are overlapping when the events have the same [[Block]], the ranges are not equal, and their intersection is non-empty. Two events' ranges are disjoint when the events do not have the same [[Block]] or their ranges are neither equal nor overlapping.</p>
49306
+
<p>Let the <dfn variants="memory ranges">memory range</dfn> of a Shared Data Block event be the Set of contiguous integers from its [[ByteIndex]] to [[ByteIndex]] + [[ElementSize]] - 1. Two events' memory ranges are equal when the events have the same [[Block]], [[ByteIndex]], and [[ElementSize]]. Two events' memory ranges are overlapping when the events have the same [[Block]], the ranges are not equal, and their intersection is non-empty. Two events' memory ranges are disjoint when the events do not have the same [[Block]] or their ranges are neither equal nor overlapping.</p>
49307
49307
<emu-note>
49308
49308
<p>Examples of host-specific synchronizing events that should be accounted for are: sending a SharedArrayBuffer from one agent to another (e.g., by `postMessage` in a browser), starting and stopping agents, and communicating within the agent cluster via channels other than shared memory. For a particular execution _execution_, those events are provided by the host via the host-synchronizes-with strict partial order. Additionally, hosts can add host-specific synchronizing events to _execution_.[[EventList]] so as to participate in the is-agent-order-before Relation.</p>
49309
49309
</emu-note>
@@ -49458,7 +49458,7 @@ <h1>
49458
49458
1. Let _byteLocation_ be _byteIndex_.
49459
49459
1. Let _bytesRead_ be a new empty List.
49460
49460
1. For each element _W_ of _Ws_, do
49461
-
1. Assert: _W_ has _byteLocation_ in its range.
49461
+
1. Assert: _W_ has _byteLocation_ in its memory range.
49462
49462
1. Let _payloadIndex_ be _byteLocation_ - _W_.[[ByteIndex]].
49463
49463
1. If _W_ is a WriteSharedMemory event, then
49464
49464
1. Let _byte_ be _W_.[[Payload]][_payloadIndex_].
@@ -49520,7 +49520,7 @@ <h1>reads-bytes-from</h1>
49520
49520
<li>
49521
49521
<p>For each ReadSharedMemory or ReadModifyWriteSharedMemory event _R_ in SharedDataBlockEventSet(_execution_), reads-bytes-from(_R_) in _execution_ is a List of length _R_.[[ElementSize]] whose elements are WriteSharedMemory or ReadModifyWriteSharedMemory events _Ws_ such that all of the following are true.</p>
49522
49522
<ul>
49523
-
<li>Each event _W_ with index _i_ in _Ws_ has _R_.[[ByteIndex]] + _i_ in its range.</li>
49523
+
<li>Each event _W_ with index _i_ in _Ws_ has _R_.[[ByteIndex]] + _i_ in its memory range.</li>
<p>For a candidate execution _execution_, its <dfn>synchronizes-with</dfn> Relation is the least Relation on Memory events that satisfies the following.</p>
49558
49558
<ul>
49559
49559
<li>
49560
-
For events _R_ and _W_, _W_ synchronizes-with _R_ in _execution_ if _R_ reads-from _W_ in _execution_, _R_.[[Order]] is ~seq-cst~, _W_.[[Order]] is ~seq-cst~, and _R_ and _W_ have equal ranges.
49560
+
For events _R_ and _W_, _W_ synchronizes-with _R_ in _execution_ if _R_ reads-from _W_ in _execution_, _R_.[[Order]] is ~seq-cst~, _W_.[[Order]] is ~seq-cst~, and _R_ and _W_ have equal memory ranges.
49561
49561
</li>
49562
49562
<li>
49563
49563
For each element _eventsRecord_ of _execution_.[[EventsRecords]], the following is true.
<p>In a candidate execution _execution_, not all ~seq-cst~ events related by reads-from are related by synchronizes-with. Only events that also have equal ranges are related by synchronizes-with.</p>
49580
+
<p>In a candidate execution _execution_, not all ~seq-cst~ events related by reads-from are related by synchronizes-with. Only events that also have equal memory ranges are related by synchronizes-with.</p>
49581
49581
</emu-note>
49582
49582
49583
49583
<emu-note>
@@ -49595,7 +49595,7 @@ <h1>happens-before</h1>
49595
49595
<ul>
49596
49596
<li>_E_ is-agent-order-before _D_ in _execution_.</li>
49597
49597
<li>_E_ synchronizes-with _D_ in _execution_.</li>
49598
-
<li>SharedDataBlockEventSet(_execution_) contains both _E_ and _D_, _E_.[[Order]] is ~init~, and _E_ and _D_ have overlapping ranges.</li>
49598
+
<li>SharedDataBlockEventSet(_execution_) contains both _E_ and _D_, _E_.[[Order]] is ~init~, and _E_ and _D_ have overlapping memory ranges.</li>
49599
49599
<li>There is an event _F_ such that _E_ happens-before _F_ and _F_ happens-before _D_ in _execution_.</li>
49600
49600
</ul>
49601
49601
</li>
@@ -49638,7 +49638,7 @@ <h1>Coherent Reads</h1>
49638
49638
1. For each element _W_ of _Ws_, do
49639
49639
1. If _R_ happens-before _W_ in _execution_, then
49640
49640
1. Return *false*.
49641
-
1. If there exists a WriteSharedMemory or ReadModifyWriteSharedMemory event _V_ that has _byteLocation_ in its range such that _W_ happens-before _V_ in _execution_ and _V_ happens-before _R_ in _execution_, then
49641
+
1. If there exists a WriteSharedMemory or ReadModifyWriteSharedMemory event _V_ that has _byteLocation_ in its memory range such that _W_ happens-before _V_ in _execution_ and _V_ happens-before _R_ in _execution_, then
49642
49642
1. Return *false*.
49643
49643
1. Set _byteLocation_ to _byteLocation_ + 1.
49644
49644
1. Return *true*.
@@ -49653,7 +49653,7 @@ <h1>Tear Free Reads</h1>
49653
49653
1. If _R_.[[NoTear]] is *true*, then
49654
49654
1. Assert: The remainder of dividing _R_.[[ByteIndex]] by _R_.[[ElementSize]] is 0.
49655
49655
1. For each Memory event _W_ such that _R_ reads-from _W_ in _execution_ and _W_.[[NoTear]] is *true*, do
49656
-
1. If _R_ and _W_ have equal ranges and there exists a Memory event _V_ such that _V_ and _W_ have equal ranges, _V_.[[NoTear]] is *true*, _W_ and _V_ are not the same Shared Data Block event, and _R_ reads-from _V_ in _execution_, then
49656
+
1. If _R_ and _W_ have equal memory ranges and there exists a Memory event _V_ such that _V_ and _W_ have equal memory ranges, _V_.[[NoTear]] is *true*, _W_ and _V_ are not the same Shared Data Block event, and _R_ reads-from _V_ in _execution_, then
<p>For events _R_ and _W_ such that _R_ reads-from _W_ in _execution_, there is no WriteSharedMemory or ReadModifyWriteSharedMemory event _V_ in SharedDataBlockEventSet(_execution_) such that _V_.[[Order]] is ~seq-cst~, _W_ is-memory-order-before _V_ in _execution_, _V_ is-memory-order-before _R_ in _execution_, and any of the following conditions are true.</p>
49674
49674
<ul>
49675
-
<li>_W_ synchronizes-with _R_ in _execution_, and _V_ and _R_ have equal ranges.</li>
49676
-
<li>_W_ happens-before _R_ and _V_ happens-before _R_ in _execution_, _W_.[[Order]] is ~seq-cst~, and _W_ and _V_ have equal ranges.</li>
49677
-
<li>_W_ happens-before _R_ and _W_ happens-before _V_ in _execution_, _R_.[[Order]] is ~seq-cst~, and _V_ and _R_ have equal ranges.</li>
49675
+
<li>_W_ synchronizes-with _R_ in _execution_, and _V_ and _R_ have equal memory ranges.</li>
49676
+
<li>_W_ happens-before _R_ and _V_ happens-before _R_ in _execution_, _W_.[[Order]] is ~seq-cst~, and _W_ and _V_ have equal memory ranges.</li>
49677
+
<li>_W_ happens-before _R_ and _W_ happens-before _V_ in _execution_, _R_.[[Order]] is ~seq-cst~, and _V_ and _R_ have equal memory ranges.</li>
49678
49678
</ul>
49679
49679
<emu-note>
49680
-
<p>This clause additionally constrains ~seq-cst~ events on equal ranges.</p>
49680
+
<p>This clause additionally constrains ~seq-cst~ events on equal memory ranges.</p>
49681
49681
</emu-note>
49682
49682
</li>
49683
49683
<li>
49684
-
<p>For each WriteSharedMemory or ReadModifyWriteSharedMemory event _W_ in SharedDataBlockEventSet(_execution_), if _W_.[[Order]] is ~seq-cst~, then it is not the case that there is an infinite number of ReadSharedMemory or ReadModifyWriteSharedMemory events in SharedDataBlockEventSet(_execution_) with equal range that is memory-order before _W_.</p>
49684
+
<p>For each WriteSharedMemory or ReadModifyWriteSharedMemory event _W_ in SharedDataBlockEventSet(_execution_), if _W_.[[Order]] is ~seq-cst~, then it is not the case that there is an infinite number of ReadSharedMemory or ReadModifyWriteSharedMemory events in SharedDataBlockEventSet(_execution_) with equal memory range that is memory-order before _W_.</p>
49685
49685
<emu-note>
49686
-
<p>This clause together with the forward progress guarantee on agents ensure the liveness condition that ~seq-cst~ writes become visible to ~seq-cst~ reads with equal range in finite time.</p>
49686
+
<p>This clause together with the forward progress guarantee on agents ensure the liveness condition that ~seq-cst~ writes become visible to ~seq-cst~ reads with equal memory range in finite time.</p>
49687
49687
</emu-note>
49688
49688
</li>
49689
49689
</ul>
@@ -49715,7 +49715,7 @@ <h1>Races</h1>
49715
49715
<emu-alg>
49716
49716
1. If _E_ and _D_ are not the same Shared Data Block event, then
49717
49717
1. If it is not the case that both _E_ happens-before _D_ in _execution_ and _D_ happens-before _E_ in _execution_, then
49718
-
1. If _E_ and _D_ are both WriteSharedMemory or ReadModifyWriteSharedMemory events and _E_ and _D_ do not have disjoint ranges, then
49718
+
1. If _E_ and _D_ are both WriteSharedMemory or ReadModifyWriteSharedMemory events and _E_ and _D_ do not have disjoint memory ranges, then
49719
49719
1. Return *true*.
49720
49720
1. If _E_ reads-from _D_ in _execution_ or _D_ reads-from _E_ in _execution_, then
49721
49721
1. Return *true*.
@@ -49730,7 +49730,7 @@ <h1>Data Races</h1>
49730
49730
1. If _E_ and _D_ are in a <emu-xref href="#sec-races">race</emu-xref> in _execution_, then
49731
49731
1. If _E_.[[Order]] is not ~seq-cst~ or _D_.[[Order]] is not ~seq-cst~, then
49732
49732
1. Return *true*.
49733
-
1. If _E_ and _D_ have overlapping ranges, then
49733
+
1. If _E_ and _D_ have overlapping memory ranges, then
<li>Lock-free atomic read-modify-write accesses compile to a full fence, an atomic read-modify-write instruction sequence, and a full fence.</li>
49796
49796
<li>Non-lock-free atomics compile to a spinlock acquire, a full fence, a series of non-atomic load and store instructions, a full fence, and a spinlock release.</li>
49797
49797
</ul>
49798
-
<p>That mapping is correct so long as an atomic operation on an address range does not race with a non-atomic write or with an atomic operation of different size. However, that is all we need: the memory model effectively demotes the atomic operations involved in a race to non-atomic status. On the other hand, the naive mapping is quite strong: it allows atomic operations to be used as sequentially consistent fences, which the memory model does not actually guarantee.</p>
49798
+
<p>That mapping is correct so long as an atomic operation on a memory range does not race with a non-atomic write or with an atomic operation of different size. However, that is all we need: the memory model effectively demotes the atomic operations involved in a race to non-atomic status. On the other hand, the naive mapping is quite strong: it allows atomic operations to be used as sequentially consistent fences, which the memory model does not actually guarantee.</p>
49799
49799
<p>Local improvements to those basic patterns are also allowed, subject to the constraints of the memory model. For example:</p>
49800
49800
<ul>
49801
49801
<li>There are obvious platform-dependent improvements that remove redundant fences. For example, on x86 the fences around lock-free atomic loads and stores can always be omitted except for the fence following a store, and no fence is needed for lock-free read-modify-write instructions, as these all use <code>LOCK</code>-prefixed instructions. On many platforms there are fences of several strengths, and weaker fences can be used in certain contexts without destroying sequential consistency.</li>
0 commit comments