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
<p>The <em>Set</em> type is used to explain a collection of unordered elements for use in the memory model. It is distinct from the ECMAScript collection type of the same name. To disambiguate, instances of the ECMAScript collection are consistently referred to as "Set objects" within this specification. Values of the Set type are simple collections of elements, where no element appears more than once. Elements may be added to and removed from Sets. Sets may be unioned, intersected, or subtracted from each other.</p>
4196
-
<p>The <dfn variants="Relations">Relation</dfn> type is used to explain constraints on Sets. Values of the Relation type are Sets of ordered pairs of values from its value domain. For example, a Relation on events is a set of ordered pairs of events. For a Relation _R_ and two values _a_ and _b_ in the value domain of _R_, _a_ _R_ _b_ is shorthand for saying the ordered pair (_a_, _b_) is a member of _R_. A Relation is the <dfn id="least-relation">least Relation</dfn> with respect to some conditions when it is the smallest Relation that satisfies those conditions.</p>
4196
+
<p>The <dfn variants="Relations">Relation</dfn> type is used to explain constraints on Sets. Values of the Relation type are Sets of ordered pairs of values from its value domain. For example, a Relation on Memory events is a set of ordered pairs of Memory events. For a Relation _R_ and two values _a_ and _b_ in the value domain of _R_, _a_ _R_ _b_ is shorthand for saying the ordered pair (_a_, _b_) is a member of _R_. A Relation is the <dfn id="least-relation">least Relation</dfn> with respect to some conditions when it is the smallest Relation that satisfies those conditions.</p>
4197
4197
<p>A <dfn variants="strict partial orders">strict partial order</dfn> is a Relation value _R_ that satisfies the following.</p>
<p>The memory consistency model, or <dfn>memory model</dfn>, specifies the possible orderings of Shared Data Block events, arising via accessing TypedArray instances backed by a SharedArrayBuffer and via methods on the Atomics object. When the program has no data races (defined below), the ordering of events appears as sequentially consistent, i.e., as an interleaving of actions from each agent. When the program has data races, shared memory operations may appear sequentially inconsistent. For example, programs may exhibit causality-violating behaviour and other astonishments. These astonishments arise from compiler transforms and the design of CPUs (e.g., out-of-order execution and speculation). The memory model defines both the precise conditions under which a program exhibits sequentially consistent behaviour as well as the possible values read from data races. To wit, there is no undefined behaviour.</p>
51211
-
<p>The memory model is defined as relational constraints on events introduced by abstract operations on SharedArrayBuffer or by methods on the Atomics object during an evaluation.</p>
51211
+
<p>The memory model is defined as relational constraints on Memory events introduced by abstract operations on SharedArrayBuffer or by methods on the Atomics object during an evaluation.</p>
51212
51212
<emu-note>
51213
-
<p>This section provides an axiomatic model on events introduced by the abstract operations on SharedArrayBuffers. It bears stressing that the model is not expressible algorithmically, unlike the rest of this specification. The nondeterministic introduction of events by abstract operations is the interface between the operational semantics of ECMAScript evaluation and the axiomatic semantics of the memory model. The semantics of these events is defined by considering graphs of all events in an evaluation. These are neither Static Semantics nor Runtime Semantics. There is no demonstrated algorithmic implementation, but instead a set of constraints that determine if a particular event graph is allowed or disallowed.</p>
51213
+
<p>This section provides an axiomatic model on Memory events introduced by the abstract operations on SharedArrayBuffers. It bears stressing that the model is not expressible algorithmically, unlike the rest of this specification. The nondeterministic introduction of events by abstract operations is the interface between the operational semantics of ECMAScript evaluation and the axiomatic semantics of the memory model. The semantics of these events is defined by considering graphs of all events in an evaluation. These are neither Static Semantics nor Runtime Semantics. There is no demonstrated algorithmic implementation, but instead a set of constraints that determine if a particular event graph is allowed or disallowed.</p>
51214
51214
</emu-note>
51215
51215
51216
51216
<emu-clause id="sec-memory-model-fundamentals">
@@ -51347,7 +51347,7 @@ <h1>Memory Model Fundamentals</h1>
51347
51347
</table>
51348
51348
</emu-table>
51349
51349
51350
-
<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.</p>
51350
+
<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>
51351
51351
<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>
51352
51352
<emu-note>
51353
51353
<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>
<p>The following relations and mathematical functions are parameterized over a particular candidate execution and order its events.</p>
51547
+
<p>The following relations and mathematical functions are parameterized over a particular candidate execution and order its Memory events.</p>
51548
51548
51549
51549
<emu-clause id="sec-agent-order">
51550
51550
<h1>is-agent-order-before</h1>
51551
-
<p>For a candidate execution _execution_, its <dfn>is-agent-order-before</dfn> Relation is the least Relation on events that satisfies the following.</p>
51551
+
<p>For a candidate execution _execution_, its <dfn>is-agent-order-before</dfn> Relation is the least Relation on Memory events that satisfies the following.</p>
51552
51552
<ul>
51553
51553
<li>For events _E_ and _D_, _E_ is-agent-order-before _D_ in _execution_ if there is some Agent Events Record _aer_ in _execution_.[[EventsRecords]] such that _aer_.[[EventList]] contains both _E_ and _D_ and _E_ is before _D_ in List order of _aer_.[[EventList]].</li>
<p>For a candidate execution _execution_, its <em>reads-bytes-from</em> function is a mathematical function mapping events in SharedDataBlockEventSet(_execution_) to Lists of events in SharedDataBlockEventSet(_execution_) that satisfies the following conditions.</p>
51563
+
<p>For a candidate execution _execution_, its <em>reads-bytes-from</em> function is a mathematical function mapping Memory events in SharedDataBlockEventSet(_execution_) to Lists of events in SharedDataBlockEventSet(_execution_) that satisfies the following conditions.</p>
51564
51564
<ul>
51565
51565
<li>
51566
51566
<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>
<p>For a candidate execution _execution_, its <dfn>reads-from</dfn> Relation is the least Relation on events that satisfies the following.</p>
51578
+
<p>For a candidate execution _execution_, its <dfn>reads-from</dfn> Relation is the least Relation on Memory events that satisfies the following.</p>
51579
51579
<ul>
51580
51580
<li>For events _R_ and _W_, _R_ reads-from _W_ in _execution_ if SharedDataBlockEventSet(_execution_) contains both _R_ and _W_, and reads-bytes-from(_R_) in _execution_ contains _W_.</li>
51581
51581
</ul>
51582
51582
</emu-clause>
51583
51583
51584
51584
<emu-clause id="sec-host-synchronizes-with">
51585
51585
<h1>host-synchronizes-with</h1>
51586
-
<p>For a candidate execution _execution_, its <dfn>host-synchronizes-with</dfn> Relation is a host-provided strict partial order on host-specific events that satisfies at least the following.</p>
51586
+
<p>For a candidate execution _execution_, its <dfn>host-synchronizes-with</dfn> Relation is a host-provided strict partial order on host-specific Memory events that satisfies at least the following.</p>
51587
51587
<ul>
51588
51588
<li>If _E_ host-synchronizes-with _D_ in _execution_, HostEventSet(_execution_) contains _E_ and _D_.</li>
51589
51589
<li>There is no cycle in the union of host-synchronizes-with and is-agent-order-before in _execution_.</li>
<p>For a candidate execution _execution_, its <dfn>synchronizes-with</dfn> Relation is the least Relation on events that satisfies the following.</p>
51602
+
<p>For a candidate execution _execution_, its <dfn>synchronizes-with</dfn> Relation is the least Relation on Memory events that satisfies the following.</p>
51603
51603
<ul>
51604
51604
<li>
51605
51605
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.
<p>For a candidate execution _execution_, its <dfn>happens-before</dfn> Relation is the least Relation on events that satisfies the following.</p>
51635
+
<p>For a candidate execution _execution_, its <dfn>happens-before</dfn> Relation is the least Relation on Memory events that satisfies the following.</p>
51636
51636
51637
51637
<ul>
51638
51638
<li>
@@ -51697,8 +51697,8 @@ <h1>Tear Free Reads</h1>
51697
51697
1. For each ReadSharedMemory or ReadModifyWriteSharedMemory event _R_ of SharedDataBlockEventSet(_execution_), do
51698
51698
1. If _R_.[[NoTear]] is *true*, then
51699
51699
1. Assert: The remainder of dividing _R_.[[ByteIndex]] by _R_.[[ElementSize]] is 0.
51700
-
1. For each event _W_ such that _R_ reads-from _W_ in _execution_ and _W_.[[NoTear]] is *true*, do
51701
-
1. If _R_ and _W_ have equal ranges and there exists an 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
51700
+
1. For each Memory event _W_ such that _R_ reads-from _W_ in _execution_ and _W_.[[NoTear]] is *true*, do
51701
+
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
51702
51702
1. Return *false*.
51703
51703
1. Return *true*.
51704
51704
</emu-alg>
@@ -51711,7 +51711,7 @@ <h1>Tear Free Reads</h1>
51711
51711
51712
51712
<emu-clause id="sec-memory-order">
51713
51713
<h1>Sequentially Consistent Atomics</h1>
51714
-
<p>For a candidate execution _execution_, <dfn>is-memory-order-before</dfn> is a strict total order of all events in EventSet(_execution_) that satisfies the following.</p>
51714
+
<p>For a candidate execution _execution_, <dfn>is-memory-order-before</dfn> is a strict total order of all Memory events in EventSet(_execution_) that satisfies the following.</p>
51715
51715
<ul>
51716
51716
<li>For events _E_ and _D_, _E_ is-memory-order-before _D_ in _execution_ if _E_ happens-before _D_ in _execution_.</li>
<p>The following are guidelines for ECMAScript implementers writing compiler transformations for programs using shared memory.</p>
51801
-
<p>It is desirable to allow most program transformations that are valid in a single-agent setting in a multi-agent setting, to ensure that the performance of each agent in a multi-agent program is as good as it would be in a single-agent setting. Frequently these transformations are hard to judge. We outline some rules about program transformations that are intended to be taken as normative (in that they are implied by the memory model or stronger than what the memory model implies) but which are likely not exhaustive. These rules are intended to apply to program transformations that precede the introductions of the events that make up the is-agent-order-before Relation.</p>
51801
+
<p>It is desirable to allow most program transformations that are valid in a single-agent setting in a multi-agent setting, to ensure that the performance of each agent in a multi-agent program is as good as it would be in a single-agent setting. Frequently these transformations are hard to judge. We outline some rules about program transformations that are intended to be taken as normative (in that they are implied by the memory model or stronger than what the memory model implies) but which are likely not exhaustive. These rules are intended to apply to program transformations that precede the introductions of the Memory events that make up the is-agent-order-before Relation.</p>
51802
51802
<p>Let an <dfn variants="agent-order slices">agent-order slice</dfn> be the subset of the is-agent-order-before Relation pertaining to a single agent.</p>
51803
51803
<p>Let <dfn>possible read values</dfn> of a read event be the set of all values of ValueOfReadEvent for that event across all valid executions.</p>
51804
51804
<p>Any transformation of an agent-order slice that is valid in the absence of shared memory is valid in the presence of shared memory, with the following exceptions.</p>
0 commit comments