Editorial: Introduce term "Memory event" to describe Agent Events Record [[EventList]] contents

gibson042 · gibson042 · commit 7b66465d82f0 · 2024-08-16T14:19:45.000-04:00
(Shared Data Block events, Synchronize events, and a host-specific events)
diff --git a/spec.html b/spec.html
@@ -4058,7 +4058,7 @@ <h1>The List and Record Specification Types</h1>
     <emu-clause id="sec-set-and-relation-specification-type">
       <h1>The Set and Relation Specification Types</h1>
       <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>
-      <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>
+      <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>
       <p>A <dfn variants="strict partial orders">strict partial order</dfn> is a Relation value _R_ that satisfies the following.</p>
       <ul>
         <li>
@@ -49163,9 +49163,9 @@ <h1>%Symbol.toStringTag%</h1>
 <emu-clause id="sec-memory-model">
   <h1>Memory Model</h1>
   <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>
-  <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>
+  <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>
   <emu-note>
-    <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>
+    <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>
   </emu-note>
 
   <emu-clause id="sec-memory-model-fundamentals">
@@ -49302,7 +49302,7 @@ <h1>Memory Model Fundamentals</h1>
       </table>
     </emu-table>
 
-    <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>
+    <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>
     <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>
     <emu-note>
       <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>
@@ -49329,7 +49329,7 @@ <h1>Agent Events Records</h1>
         </tr>
         <tr>
           <td>[[EventList]]</td>
-          <td>a List of events</td>
+          <td>a List of Memory events</td>
           <td>Events are appended to the list during evaluation.</td>
         </tr>
         <tr>
@@ -49382,7 +49382,7 @@ <h1>Candidate Executions</h1>
         <tr>
           <td>[[EventsRecords]]</td>
           <td>a List of Agent Events Records</td>
-          <td>Maps an agent to Lists of events appended during the evaluation.</td>
+          <td>Maps an agent to Lists of Memory events appended during the evaluation.</td>
         </tr>
         <tr>
           <td>[[ChosenValues]]</td>
@@ -49402,14 +49402,14 @@ <h1>Abstract Operations for the Memory Model</h1>
       <h1>
         EventSet (
           _execution_: a candidate execution,
-        ): a Set of events
+        ): a Set of Memory events
       </h1>
       <dl class="header">
       </dl>
       <emu-alg>
         1. Let _events_ be an empty Set.
         1. For each Agent Events Record _aer_ of _execution_.[[EventsRecords]], do
-          1. For each event _E_ of _aer_.[[EventList]], do
+          1. For each Memory event _E_ of _aer_.[[EventList]], do
             1. Add _E_ to _events_.
         1. Return _events_.
       </emu-alg>
@@ -49425,7 +49425,7 @@ <h1>
       </dl>
       <emu-alg>
         1. Let _events_ be an empty Set.
-        1. For each event _E_ of EventSet(_execution_), do
+        1. For each Memory event _E_ of EventSet(_execution_), do
           1. If _E_ is a Shared Data Block event, add _E_ to _events_.
         1. Return _events_.
       </emu-alg>
@@ -49435,7 +49435,7 @@ <h1>
       <h1>
         HostEventSet (
           _execution_: a candidate execution,
-        ): a Set of events
+        ): a Set of Memory events
       </h1>
       <dl class="header">
       </dl>
@@ -49499,11 +49499,11 @@ <h1>
   <emu-clause id="sec-relations-of-candidate-executions">
     <h1>Relations of Candidate Executions</h1>
 
-    <p>The following relations and mathematical functions are parameterized over a particular candidate execution and order its events.</p>
+    <p>The following relations and mathematical functions are parameterized over a particular candidate execution and order its Memory events.</p>
 
     <emu-clause id="sec-agent-order">
       <h1>is-agent-order-before</h1>
-      <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>
+      <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>
       <ul>
         <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>
       </ul>
@@ -49515,7 +49515,7 @@ <h1>is-agent-order-before</h1>
 
     <emu-clause id="sec-reads-bytes-from" aoid="reads-bytes-from">
       <h1>reads-bytes-from</h1>
-      <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>
+      <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>
       <ul>
         <li>
           <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>
@@ -49530,15 +49530,15 @@ <h1>reads-bytes-from</h1>
 
     <emu-clause id="sec-reads-from">
       <h1>reads-from</h1>
-      <p>For a candidate execution _execution_, its <dfn>reads-from</dfn> Relation is the least Relation on events that satisfies the following.</p>
+      <p>For a candidate execution _execution_, its <dfn>reads-from</dfn> Relation is the least Relation on Memory events that satisfies the following.</p>
       <ul>
         <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>
       </ul>
     </emu-clause>
 
     <emu-clause id="sec-host-synchronizes-with">
       <h1>host-synchronizes-with</h1>
-      <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>
+      <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>
       <ul>
         <li>If _E_ host-synchronizes-with _D_ in _execution_, HostEventSet(_execution_) contains _E_ and _D_.</li>
         <li>There is no cycle in the union of host-synchronizes-with and is-agent-order-before in _execution_.</li>
@@ -49554,7 +49554,7 @@ <h1>host-synchronizes-with</h1>
 
     <emu-clause id="sec-synchronizes-with">
       <h1>synchronizes-with</h1>
-      <p>For a candidate execution _execution_, its <dfn>synchronizes-with</dfn> Relation is the least Relation on events that satisfies the following.</p>
+      <p>For a candidate execution _execution_, its <dfn>synchronizes-with</dfn> Relation is the least Relation on Memory events that satisfies the following.</p>
       <ul>
         <li>
           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.
@@ -49587,7 +49587,7 @@ <h1>synchronizes-with</h1>
 
     <emu-clause id="sec-happens-before">
       <h1>happens-before</h1>
-      <p>For a candidate execution _execution_, its <dfn>happens-before</dfn> Relation is the least Relation on events that satisfies the following.</p>
+      <p>For a candidate execution _execution_, its <dfn>happens-before</dfn> Relation is the least Relation on Memory events that satisfies the following.</p>
 
       <ul>
         <li>
@@ -49652,8 +49652,8 @@ <h1>Tear Free Reads</h1>
         1. For each ReadSharedMemory or ReadModifyWriteSharedMemory event _R_ of SharedDataBlockEventSet(_execution_), do
           1. If _R_.[[NoTear]] is *true*, then
             1. Assert: The remainder of dividing _R_.[[ByteIndex]] by _R_.[[ElementSize]] is 0.
-            1. For each event _W_ such that _R_ reads-from _W_ in _execution_ and _W_.[[NoTear]] is *true*, do
-              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
+            1. For each Memory event _W_ such that _R_ reads-from _W_ in _execution_ and _W_.[[NoTear]] is *true*, do
+              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
                 1. Return *false*.
         1. Return *true*.
       </emu-alg>
@@ -49666,7 +49666,7 @@ <h1>Tear Free Reads</h1>
 
     <emu-clause id="sec-memory-order">
       <h1>Sequentially Consistent Atomics</h1>
-      <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>
+      <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>
       <ul>
         <li>For events _E_ and _D_, _E_ is-memory-order-before _D_ in _execution_ if _E_ happens-before _D_ in _execution_.</li>
         <li>
@@ -49753,7 +49753,7 @@ <h1>Shared Memory Guidelines</h1>
 
     <emu-note>
       <p>The following are guidelines for ECMAScript implementers writing compiler transformations for programs using shared memory.</p>
-      <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>
+      <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>
       <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>
       <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>
       <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>
