From 70130a2c02da3ed8b9d7932e737d65a93e64923f Mon Sep 17 00:00:00 2001 From: Richard Gibson Date: Thu, 15 Aug 2024 22:21:22 -0400 Subject: [PATCH 01/13] Editorial: Clean up TypedArray/DataView bounds checking --- spec.html | 26 ++++++++++++++++---------- 1 file changed, 16 insertions(+), 10 deletions(-) diff --git a/spec.html b/spec.html index 3f95b6d214..7ff3962da0 100644 --- a/spec.html +++ b/spec.html @@ -14831,12 +14831,12 @@

- 1. If IsTypedArrayOutOfBounds(_taRecord_) is *true*, return 0. - 1. Let _length_ be TypedArrayLength(_taRecord_). - 1. If _length_ = 0, return 0. + 1. Assert: IsTypedArrayOutOfBounds(_taRecord_) is *false*. 1. Let _O_ be _taRecord_.[[Object]]. 1. If _O_.[[ByteLength]] is not ~auto~, return _O_.[[ByteLength]]. + 1. Let _length_ be TypedArrayLength(_taRecord_). 1. Let _elementSize_ be TypedArrayElementSize(_O_). + 1. NOTE: The returned byte length is always an integer multiple of _elementSize_, even when the underlying buffer has been resized to a non-integer multiple. 1. Return _length_ × _elementSize_. @@ -14875,16 +14875,19 @@

1. Let _O_ be _taRecord_.[[Object]]. 1. Let _bufferByteLength_ be _taRecord_.[[CachedBufferByteLength]]. - 1. Assert: IsDetachedBuffer(_O_.[[ViewedArrayBuffer]]) is *true* if and only if _bufferByteLength_ is ~detached~. - 1. If _bufferByteLength_ is ~detached~, return *true*. + 1. If IsDetachedBuffer(_O_.[[ViewedArrayBuffer]]) is *true*, then + 1. Assert: _bufferByteLength_ is ~detached~. + 1. Return *true*. + 1. Assert: _bufferByteLength_ is a non-negative integer. 1. Let _byteOffsetStart_ be _O_.[[ByteOffset]]. 1. If _O_.[[ArrayLength]] is ~auto~, then 1. Let _byteOffsetEnd_ be _bufferByteLength_. 1. Else, 1. Let _elementSize_ be TypedArrayElementSize(_O_). - 1. Let _byteOffsetEnd_ be _byteOffsetStart_ + _O_.[[ArrayLength]] × _elementSize_. + 1. Let _arrayByteLength_ be _O_.[[ArrayLength]] × _elementSize_. + 1. Let _byteOffsetEnd_ be _byteOffsetStart_ + _arrayByteLength_. + 1. NOTE: A 0-length TypedArray with [[ByteOffset]] equal to _bufferByteLength_ is not considered out-of-bounds. 1. If _byteOffsetStart_ > _bufferByteLength_ or _byteOffsetEnd_ > _bufferByteLength_, return *true*. - 1. NOTE: 0-length TypedArrays are not considered out-of-bounds. 1. Return *false*. @@ -40577,6 +40580,7 @@

get %TypedArray%.prototype.byteLength

1. Perform ? RequireInternalSlot(_O_, [[TypedArrayName]]). 1. Assert: _O_ has a [[ViewedArrayBuffer]] internal slot. 1. Let _taRecord_ be MakeTypedArrayWithBufferWitnessRecord(_O_, ~seq-cst~). + 1. If IsTypedArrayOutOfBounds(_taRecord_) is *true*, return *+0*𝔽. 1. Let _size_ be TypedArrayByteLength(_taRecord_). 1. Return 𝔽(_size_). @@ -44218,15 +44222,17 @@

1. Let _view_ be _viewRecord_.[[Object]]. 1. Let _bufferByteLength_ be _viewRecord_.[[CachedBufferByteLength]]. - 1. Assert: IsDetachedBuffer(_view_.[[ViewedArrayBuffer]]) is *true* if and only if _bufferByteLength_ is ~detached~. - 1. If _bufferByteLength_ is ~detached~, return *true*. + 1. If IsDetachedBuffer(_view_.[[ViewedArrayBuffer]]) is *true*, then + 1. Assert: _bufferByteLength_ is ~detached~. + 1. Return *true*. + 1. Assert: _bufferByteLength_ is a non-negative integer. 1. Let _byteOffsetStart_ be _view_.[[ByteOffset]]. 1. If _view_.[[ByteLength]] is ~auto~, then 1. Let _byteOffsetEnd_ be _bufferByteLength_. 1. Else, 1. Let _byteOffsetEnd_ be _byteOffsetStart_ + _view_.[[ByteLength]]. + 1. NOTE: A 0-length DataView with [[ByteOffset]] equal to _bufferByteLength_ is not considered out-of-bounds. 1. If _byteOffsetStart_ > _bufferByteLength_ or _byteOffsetEnd_ > _bufferByteLength_, return *true*. - 1. NOTE: 0-length DataViews are not considered out-of-bounds. 1. Return *false*. From 7d55cb81041f5e9cc4846e1ba49b2585130d2f11 Mon Sep 17 00:00:00 2001 From: Richard Gibson Date: Thu, 15 Aug 2024 23:14:33 -0400 Subject: [PATCH 02/13] Editorial: Clean up IsSharedArrayBuffer --- spec.html | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/spec.html b/spec.html index 7ff3962da0..84472c611c 100644 --- a/spec.html +++ b/spec.html @@ -43879,14 +43879,11 @@

description
-
It tests whether an object is an ArrayBuffer, a SharedArrayBuffer, or a subtype of either.
+
It tests whether an object is a SharedArrayBuffer.
- 1. Let _bufferData_ be _obj_.[[ArrayBufferData]]. - 1. If _bufferData_ is *null*, return *false*. - 1. If _bufferData_ is a Data Block, return *false*. - 1. Assert: _bufferData_ is a Shared Data Block. - 1. Return *true*. + 1. If _obj_.[[ArrayBufferData]] is a Shared Data Block, return *true*. + 1. Return *false*. From 31c095e0eb908eb07cbc1fc7dd1658a169b26f54 Mon Sep 17 00:00:00 2001 From: Richard Gibson Date: Thu, 15 Aug 2024 23:16:04 -0400 Subject: [PATCH 03/13] Editorial: Add IsGrowableSharedArrayBuffer for clarity --- spec.html | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/spec.html b/spec.html index 84472c611c..041e481fa7 100644 --- a/spec.html +++ b/spec.html @@ -43184,7 +43184,7 @@

- 1. If IsSharedArrayBuffer(_arrayBuffer_) is *true* and _arrayBuffer_ has an [[ArrayBufferByteLengthData]] internal slot, then + 1. If IsGrowableSharedArrayBuffer(_arrayBuffer_) is *true*, then 1. Let _bufferByteLengthBlock_ be _arrayBuffer_.[[ArrayBufferByteLengthData]]. 1. Let _rawLength_ be GetRawBytesFromSharedBlock(_bufferByteLengthBlock_, 0, ~biguint64~, *true*, _order_). 1. Let _isLittleEndian_ be the value of the [[LittleEndian]] field of the surrounding agent's Agent Record. @@ -43887,6 +43887,22 @@

+ +

+ IsGrowableSharedArrayBuffer ( + _obj_: an ArrayBuffer or a SharedArrayBuffer, + ): a Boolean +

+
+
description
+
It tests whether an object is a growable SharedArrayBuffer.
+
+ + 1. If IsSharedArrayBuffer(_obj_) is *true* and _obj_ has an [[ArrayBufferByteLengthData]] internal slot, return *true*. + 1. Return *false*. + +
+

HostGrowSharedArrayBuffer ( From 513a5b8b6e21d87455ab5228d45b6b65d8931d78 Mon Sep 17 00:00:00 2001 From: Richard Gibson Date: Thu, 15 Aug 2024 23:18:06 -0400 Subject: [PATCH 04/13] Editorial: Improve formatting in HostGrowSharedArrayBuffer --- spec.html | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/spec.html b/spec.html index 041e481fa7..ee80ea5fb8 100644 --- a/spec.html +++ b/spec.html @@ -43917,12 +43917,12 @@

The implementation of HostGrowSharedArrayBuffer must conform to the following requirements:

  • If the abstract operation does not complete normally with ~unhandled~, and _newByteLength_ < the current byte length of the _buffer_ or _newByteLength_ > _buffer_.[[ArrayBufferMaxByteLength]], throw a *RangeError* exception.
  • -
  • Let _isLittleEndian_ be the value of the [[LittleEndian]] field of the surrounding agent's Agent Record. If the abstract operation completes normally with ~handled~, a WriteSharedMemory or ReadModifyWriteSharedMemory event whose [[Order]] is ~seq-cst~, [[Payload]] is NumericToRawBytes(~biguint64~, _newByteLength_, _isLittleEndian_), [[Block]] is _buffer_.[[ArrayBufferByteLengthData]], [[ByteIndex]] is 0, and [[ElementSize]] is 8 is added to the surrounding agent's candidate execution such that racing calls to `SharedArrayBuffer.prototype.grow` are not "lost", i.e. silently do nothing.
  • +
  • Let _isLittleEndian_ be the value of the [[LittleEndian]] field of the surrounding agent's Agent Record. If the abstract operation completes normally with ~handled~, a WriteSharedMemory or ReadModifyWriteSharedMemory event whose [[Order]] is ~seq-cst~, [[Payload]] is NumericToRawBytes(~biguint64~, _newByteLength_, _isLittleEndian_), [[Block]] is _buffer_.[[ArrayBufferByteLengthData]], [[ByteIndex]] is 0, and [[ElementSize]] is 8 is added to the surrounding agent's candidate execution such that racing calls to are not "lost", i.e. silently do nothing.
-

The second requirement above is intentionally vague about how or when the current byte length of _buffer_ is read. Because the byte length must be updated via an atomic read-modify-write operation on the underlying hardware, architectures that use load-link/store-conditional or load-exclusive/store-exclusive instruction pairs may wish to keep the paired instructions close in the instruction stream. As such, SharedArrayBuffer.prototype.grow itself does not perform bounds checking on _newByteLength_ before calling HostGrowSharedArrayBuffer, nor is there a requirement on when the current byte length is read.

-

This is in contrast with HostResizeArrayBuffer, which is guaranteed that the value of _newByteLength_ is ≥ 0 and ≤ _buffer_.[[ArrayBufferMaxByteLength]].

+

The second requirement above is intentionally vague about how or when the current byte length of _buffer_ is read. Because the byte length must be updated via an atomic read-modify-write operation on the underlying hardware, architectures that use load-link/store-conditional or load-exclusive/store-exclusive instruction pairs may wish to keep the paired instructions close in the instruction stream. As such, itself does not perform bounds checking on _newByteLength_ before calling HostGrowSharedArrayBuffer, nor is there a requirement on when the current byte length is read.

+

This is in contrast with HostResizeArrayBuffer, which is guaranteed that 0 ≤ _newByteLength_ ≤ _buffer_.[[ArrayBufferMaxByteLength]].

The default implementation of HostGrowSharedArrayBuffer is to return NormalCompletion(~unhandled~).

From 307d44fd8bfcbdb1d637742df14931b88bc8995e Mon Sep 17 00:00:00 2001 From: Richard Gibson Date: Thu, 15 Aug 2024 23:30:45 -0400 Subject: [PATCH 05/13] Editorial: Make better use of the "Shared Data Block event" term --- spec.html | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/spec.html b/spec.html index ee80ea5fb8..6338290106 100644 --- a/spec.html +++ b/spec.html @@ -49305,10 +49305,8 @@

Memory Model Fundamentals

-

These events are introduced by abstract operations or by methods on the Atomics object.

-

Some operations may also introduce Synchronize events. A Synchronize event has no fields, and exists purely to directly constrain the permitted orderings of other events.

-

In addition to Shared Data Block and Synchronize events, there are host-specific events.

-

Let the range of a ReadSharedMemory, WriteSharedMemory, or ReadModifyWriteSharedMemory 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]], and the ranges are element-wise equal. 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.

+

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 Synchronize events, which have no fields and exist purely to directly constrain the permitted orderings of other events. And finally, there are host-specific events.

+

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.

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.

@@ -49424,14 +49422,14 @@

SharedDataBlockEventSet ( _execution_: a candidate execution, - ): a Set of events + ): a Set of Shared Data Block events

1. Let _events_ be an empty Set. 1. For each event _E_ of EventSet(_execution_), do - 1. If _E_ is a ReadSharedMemory, WriteSharedMemory, or ReadModifyWriteSharedMemory event, add _E_ to _events_. + 1. If _E_ is a Shared Data Block event, add _E_ to _events_. 1. Return _events_. @@ -49667,7 +49665,7 @@

Tear Free Reads

-

An event's [[NoTear]] field is *true* when that event was introduced via accessing an integer TypedArray, and *false* when introduced via accessing a floating point TypedArray or DataView.

+

A Shared Data Block event's [[NoTear]] field is *true* when that event was introduced via accessing an integer TypedArray, and *false* when introduced via accessing a floating point TypedArray or DataView.

Intuitively, this requirement says when a memory range is accessed in an aligned fashion via an integer TypedArray, a single write event on that range must "win" when in a data race with other write events with equal ranges. More precisely, this requirement says an aligned read event cannot read a value composed of bytes from multiple, different write events all with equal ranges. It is possible, however, for an aligned read event to read from multiple write events with overlapping ranges.

@@ -49767,7 +49765,7 @@

Shared Memory Guidelines

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.

  • -

    Atomics are carved in stone: Program transformations must not cause the ~seq-cst~ events in an agent-order slice to be reordered with its ~unordered~ operations, nor its ~seq-cst~ operations to be reordered with each other, nor may a program transformation remove a ~seq-cst~ operation from the is-agent-order-before Relation.

    +

    Atomics are carved in stone: Program transformations must not cause any Shared Data Block events having [[Order]] ~seq-cst~ to be removed from the is-agent-order-before Relation, nor to be reordered with respect to each other, nor to be reordered inside an agent-order slice with respect to events having [[Order]] ~unordered~.

    (In practice, the prohibition on reorderings forces a compiler to assume that every ~seq-cst~ operation is a synchronization and included in the final is-memory-order-before Relation, which it would usually have to assume anyway in the absence of inter-agent program analysis. It also forces the compiler to assume that every call where the callee's effects on the memory-order are unknown may contain ~seq-cst~ operations.)

  • From 37c4decfe5550df07d00b32134d121c376b4bb1a Mon Sep 17 00:00:00 2001 From: Richard Gibson Date: Thu, 15 Aug 2024 23:32:37 -0400 Subject: [PATCH 06/13] Editorial: Make better use of the "Set" specification type --- spec.html | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/spec.html b/spec.html index 6338290106..b2bba0cd22 100644 --- a/spec.html +++ b/spec.html @@ -42190,7 +42190,7 @@

    %MapIteratorPrototype% [ %Symbol.toStringTag% ]

    Set Objects

    -

    Set objects are collections of ECMAScript language values. A distinct value may only occur once as an element of a Set's collection. Distinct values are discriminated using the SameValueZero comparison algorithm.

    +

    Set objects are collections of ECMAScript language values. A distinct value may only occur once as an element of a Set's collection. Distinct values are discriminated using the SameValueZero comparison algorithm.

    Set objects must be implemented using either hash tables or other mechanisms that, on average, provide access times that are sublinear on the number of elements in the collection. The data structure used in this specification is only intended to describe the required observable semantics of Set objects. It is not intended to be a viable implementation model.

    @@ -49443,10 +49443,7 @@

    - 1. Let _events_ be an empty Set. - 1. For each event _E_ of EventSet(_execution_), do - 1. If _E_ is not in SharedDataBlockEventSet(_execution_), add _E_ to _events_. - 1. Return _events_. + 1. Return the subtraction of SharedDataBlockEventSet(_execution_) from EventSet(_execution_). From 3f8dfa943655f3a8daa7030987aede84a61d047d Mon Sep 17 00:00:00 2001 From: Richard Gibson Date: Thu, 15 Aug 2024 23:35:43 -0400 Subject: [PATCH 07/13] Editorial: Link directly to ReadSharedMemory as appropriate --- spec.html | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec.html b/spec.html index b2bba0cd22..0f8433a1db 100644 --- a/spec.html +++ b/spec.html @@ -14735,7 +14735,7 @@

    [[OwnPropertyKeys]] ( ): a normal completion containing a List of property k

    TypedArray With Buffer Witness Records

    -

    An TypedArray With Buffer Witness Record is a Record value used to encapsulate a TypedArray along with a cached byte length of the viewed buffer. It is used to help ensure there is a single shared memory read event of the byte length data block when the viewed buffer is a growable SharedArrayBuffer.

    +

    An TypedArray With Buffer Witness Record is a Record value used to encapsulate a TypedArray along with a cached byte length of the viewed buffer. It is used to help ensure there is a single ReadSharedMemory event of the byte length data block when the viewed buffer is a growable SharedArrayBuffer.

    TypedArray With Buffer Witness Records have the fields listed in .

    @@ -44142,7 +44142,7 @@

    Abstract Operations For DataView Objects

    DataView With Buffer Witness Records

    -

    A DataView With Buffer Witness Record is a Record value used to encapsulate a DataView along with a cached byte length of the viewed buffer. It is used to help ensure there is a single shared memory read event of the byte length data block when the viewed buffer is a growable SharedArrayBuffers.

    +

    A DataView With Buffer Witness Record is a Record value used to encapsulate a DataView along with a cached byte length of the viewed buffer. It is used to help ensure there is a single ReadSharedMemory event of the byte length data block when the viewed buffer is a growable SharedArrayBuffer.

    DataView With Buffer Witness Records have the fields listed in .

    From 15b811d134a019a45e1d7c5fc42e5bc05664ff90 Mon Sep 17 00:00:00 2001 From: Richard Gibson Date: Thu, 15 Aug 2024 23:41:44 -0400 Subject: [PATCH 08/13] Editorial: Introduce term "Memory event" to describe Agent Events Record [[EventList]] contents (Shared Data Block events, Synchronize events, and a host-specific events) --- spec.html | 42 +++++++++++++++++++++--------------------- 1 file changed, 21 insertions(+), 21 deletions(-) diff --git a/spec.html b/spec.html index 0f8433a1db..5d18f3249f 100644 --- a/spec.html +++ b/spec.html @@ -4058,7 +4058,7 @@

    The List and Record Specification Types

    The Set and Relation Specification Types

    The Set 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.

    -

    The Relation 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 least Relation with respect to some conditions when it is the smallest Relation that satisfies those conditions.

    +

    The Relation 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 least Relation with respect to some conditions when it is the smallest Relation that satisfies those conditions.

    A strict partial order is a Relation value _R_ that satisfies the following.

    • @@ -49166,9 +49166,9 @@

      %Symbol.toStringTag%

      Memory Model

      The memory consistency model, or memory model, 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.

      -

      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.

      +

      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.

      -

      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.

      +

      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.

      @@ -49305,7 +49305,7 @@

      Memory Model Fundamentals

    -

    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 Synchronize events, which have no fields and exist purely to directly constrain the permitted orderings of other events. And finally, there are host-specific events.

    +

    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 Synchronize events, which have no fields and exist purely to directly constrain the permitted orderings of other events. And finally, there are host-specific events. A Memory event is either a Shared Data Block event, Synchronize event, or such a host-specific event.

    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.

    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.

    @@ -49332,7 +49332,7 @@

    Agent Events Records

    [[EventList]] - a List of events + a List of Memory events Events are appended to the list during evaluation. @@ -49385,7 +49385,7 @@

    Candidate Executions

    [[EventsRecords]] a List of Agent Events Records - Maps an agent to Lists of events appended during the evaluation. + Maps an agent to Lists of Memory events appended during the evaluation. [[ChosenValues]] @@ -49405,14 +49405,14 @@

    Abstract Operations for the Memory Model

    EventSet ( _execution_: a candidate execution, - ): a Set of events + ): a Set of Memory events

    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_. @@ -49428,7 +49428,7 @@

    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_. @@ -49438,7 +49438,7 @@

    HostEventSet ( _execution_: a candidate execution, - ): a Set of events + ): a Set of Memory events

    @@ -49502,11 +49502,11 @@

    Relations of Candidate Executions

    -

    The following relations and mathematical functions are parameterized over a particular candidate execution and order its events.

    +

    The following relations and mathematical functions are parameterized over a particular candidate execution and order its Memory events.

    is-agent-order-before

    -

    For a candidate execution _execution_, its is-agent-order-before Relation is the least Relation on events that satisfies the following.

    +

    For a candidate execution _execution_, its is-agent-order-before Relation is the least Relation on Memory events that satisfies the following.

    • 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]].
    @@ -49518,7 +49518,7 @@

    is-agent-order-before

    reads-bytes-from

    -

    For a candidate execution _execution_, its reads-bytes-from function is a mathematical function mapping events in SharedDataBlockEventSet(_execution_) to Lists of events in SharedDataBlockEventSet(_execution_) that satisfies the following conditions.

    +

    For a candidate execution _execution_, its reads-bytes-from function is a mathematical function mapping Memory events in SharedDataBlockEventSet(_execution_) to Lists of events in SharedDataBlockEventSet(_execution_) that satisfies the following conditions.

    • 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.

      @@ -49533,7 +49533,7 @@

      reads-bytes-from

      reads-from

      -

      For a candidate execution _execution_, its reads-from Relation is the least Relation on events that satisfies the following.

      +

      For a candidate execution _execution_, its reads-from Relation is the least Relation on Memory events that satisfies the following.

      • 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_.
      @@ -49541,7 +49541,7 @@

      reads-from

      host-synchronizes-with

      -

      For a candidate execution _execution_, its host-synchronizes-with Relation is a host-provided strict partial order on host-specific events that satisfies at least the following.

      +

      For a candidate execution _execution_, its host-synchronizes-with Relation is a host-provided strict partial order on host-specific Memory events that satisfies at least the following.

      • If _E_ host-synchronizes-with _D_ in _execution_, HostEventSet(_execution_) contains _E_ and _D_.
      • There is no cycle in the union of host-synchronizes-with and is-agent-order-before in _execution_.
      • @@ -49557,7 +49557,7 @@

        host-synchronizes-with

        synchronizes-with

        -

        For a candidate execution _execution_, its synchronizes-with Relation is the least Relation on events that satisfies the following.

        +

        For a candidate execution _execution_, its synchronizes-with Relation is the least Relation on Memory events that satisfies the following.

        • 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. @@ -49590,7 +49590,7 @@

          synchronizes-with

          happens-before

          -

          For a candidate execution _execution_, its happens-before Relation is the least Relation on events that satisfies the following.

          +

          For a candidate execution _execution_, its happens-before Relation is the least Relation on Memory events that satisfies the following.

          • @@ -49655,8 +49655,8 @@

            Tear Free Reads

            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*. @@ -49669,7 +49669,7 @@

            Tear Free Reads

            Sequentially Consistent Atomics

            -

            For a candidate execution _execution_, is-memory-order-before is a strict total order of all events in EventSet(_execution_) that satisfies the following.

            +

            For a candidate execution _execution_, is-memory-order-before is a strict total order of all Memory events in EventSet(_execution_) that satisfies the following.

            • For events _E_ and _D_, _E_ is-memory-order-before _D_ in _execution_ if _E_ happens-before _D_ in _execution_.
            • @@ -49756,7 +49756,7 @@

              Shared Memory Guidelines

              The following are guidelines for ECMAScript implementers writing compiler transformations for programs using shared memory.

              -

              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.

              +

              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.

              Let an agent-order slice be the subset of the is-agent-order-before Relation pertaining to a single agent.

              Let possible read values of a read event be the set of all values of ValueOfReadEvent for that event across all valid executions.

              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.

              From b01c73cff8d89d2b8d2af76980ac56fbdccd5a13 Mon Sep 17 00:00:00 2001 From: Richard Gibson Date: Thu, 15 Aug 2024 23:46:02 -0400 Subject: [PATCH 09/13] Editorial: Introduce term "memory range" to provide links for Shared Data Block event comparison --- spec.html | 38 +++++++++++++++++++------------------- 1 file changed, 19 insertions(+), 19 deletions(-) diff --git a/spec.html b/spec.html index 5d18f3249f..deb402ec49 100644 --- a/spec.html +++ b/spec.html @@ -49196,7 +49196,7 @@

              Memory Model Fundamentals

              [[NoTear]] a Boolean - Whether this event is allowed to read from multiple write events with equal range as this event. + Whether this event is allowed to read from multiple write events with equal memory range as this event. [[Block]] @@ -49233,7 +49233,7 @@

              Memory Model Fundamentals

              [[NoTear]] a Boolean - Whether this event is allowed to be read from multiple read events with equal range as this event. + Whether this event is allowed to be read from multiple read events with equal memory range as this event. [[Block]] @@ -49306,7 +49306,7 @@

              Memory Model Fundamentals

              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 Synchronize events, which have no fields and exist purely to directly constrain the permitted orderings of other events. And finally, there are host-specific events. A Memory event is either a Shared Data Block event, Synchronize event, or such a host-specific event.

              -

              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.

              +

              Let the memory range 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.

              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.

              @@ -49461,7 +49461,7 @@

              1. Let _byteLocation_ be _byteIndex_. 1. Let _bytesRead_ be a new empty List. 1. For each element _W_ of _Ws_, do - 1. Assert: _W_ has _byteLocation_ in its range. + 1. Assert: _W_ has _byteLocation_ in its memory range. 1. Let _payloadIndex_ be _byteLocation_ - _W_.[[ByteIndex]]. 1. If _W_ is a WriteSharedMemory event, then 1. Let _byte_ be _W_.[[Payload]][_payloadIndex_]. @@ -49523,7 +49523,7 @@

              reads-bytes-from

            • 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.

                -
              • Each event _W_ with index _i_ in _Ws_ has _R_.[[ByteIndex]] + _i_ in its range.
              • +
              • Each event _W_ with index _i_ in _Ws_ has _R_.[[ByteIndex]] + _i_ in its memory range.
              • _R_ is not in _Ws_.
            • @@ -49560,7 +49560,7 @@

              synchronizes-with

              For a candidate execution _execution_, its synchronizes-with Relation is the least Relation on Memory events that satisfies the following.

              • - 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. + 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.
              • For each element _eventsRecord_ of _execution_.[[EventsRecords]], the following is true. @@ -49580,7 +49580,7 @@

                synchronizes-with

                -

                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.

                +

                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.

                @@ -49598,7 +49598,7 @@

                happens-before

                • _E_ is-agent-order-before _D_ in _execution_.
                • _E_ synchronizes-with _D_ in _execution_.
                • -
                • SharedDataBlockEventSet(_execution_) contains both _E_ and _D_, _E_.[[Order]] is ~init~, and _E_ and _D_ have overlapping ranges.
                • +
                • SharedDataBlockEventSet(_execution_) contains both _E_ and _D_, _E_.[[Order]] is ~init~, and _E_ and _D_ have overlapping memory ranges.
                • There is an event _F_ such that _E_ happens-before _F_ and _F_ happens-before _D_ in _execution_.
              • @@ -49641,7 +49641,7 @@

                Coherent Reads

                1. For each element _W_ of _Ws_, do 1. If _R_ happens-before _W_ in _execution_, then 1. Return *false*. - 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 + 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 1. Return *false*. 1. Set _byteLocation_ to _byteLocation_ + 1. 1. Return *true*. @@ -49656,7 +49656,7 @@

                Tear Free Reads

                1. If _R_.[[NoTear]] is *true*, then 1. Assert: The remainder of dividing _R_.[[ByteIndex]] by _R_.[[ElementSize]] is 0. 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. 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 1. Return *false*. 1. Return *true*. @@ -49675,18 +49675,18 @@

                Sequentially Consistent Atomics

              • 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.

                  -
                • _W_ synchronizes-with _R_ in _execution_, and _V_ and _R_ have equal ranges.
                • -
                • _W_ happens-before _R_ and _V_ happens-before _R_ in _execution_, _W_.[[Order]] is ~seq-cst~, and _W_ and _V_ have equal ranges.
                • -
                • _W_ happens-before _R_ and _W_ happens-before _V_ in _execution_, _R_.[[Order]] is ~seq-cst~, and _V_ and _R_ have equal ranges.
                • +
                • _W_ synchronizes-with _R_ in _execution_, and _V_ and _R_ have equal memory ranges.
                • +
                • _W_ happens-before _R_ and _V_ happens-before _R_ in _execution_, _W_.[[Order]] is ~seq-cst~, and _W_ and _V_ have equal memory ranges.
                • +
                • _W_ happens-before _R_ and _W_ happens-before _V_ in _execution_, _R_.[[Order]] is ~seq-cst~, and _V_ and _R_ have equal memory ranges.
                -

                This clause additionally constrains ~seq-cst~ events on equal ranges.

                +

                This clause additionally constrains ~seq-cst~ events on equal memory ranges.

              • -

                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_.

                +

                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_.

                -

                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.

                +

                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.

              @@ -49718,7 +49718,7 @@

              Races

              1. If _E_ and _D_ are not the same Shared Data Block event, then 1. If it is not the case that both _E_ happens-before _D_ in _execution_ and _D_ happens-before _E_ in _execution_, then - 1. If _E_ and _D_ are both WriteSharedMemory or ReadModifyWriteSharedMemory events and _E_ and _D_ do not have disjoint ranges, then + 1. If _E_ and _D_ are both WriteSharedMemory or ReadModifyWriteSharedMemory events and _E_ and _D_ do not have disjoint memory ranges, then 1. Return *true*. 1. If _E_ reads-from _D_ in _execution_ or _D_ reads-from _E_ in _execution_, then 1. Return *true*. @@ -49733,7 +49733,7 @@

              Data Races

              1. If _E_ and _D_ are in a race in _execution_, then 1. If _E_.[[Order]] is not ~seq-cst~ or _D_.[[Order]] is not ~seq-cst~, then 1. Return *true*. - 1. If _E_ and _D_ have overlapping ranges, then + 1. If _E_ and _D_ have overlapping memory ranges, then 1. Return *true*. 1. Return *false*.
              @@ -49798,7 +49798,7 @@

              Shared Memory Guidelines

            • Lock-free atomic read-modify-write accesses compile to a full fence, an atomic read-modify-write instruction sequence, and a full fence.
            • 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.
            -

            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.

            +

            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.

            Local improvements to those basic patterns are also allowed, subject to the constraints of the memory model. For example:

            • 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 LOCK-prefixed instructions. On many platforms there are fences of several strengths, and weaker fences can be used in certain contexts without destroying sequential consistency.
            • From 9c8d921ffa7cd1b4967eebfbaa5c3ccbd6ac2d6e Mon Sep 17 00:00:00 2001 From: Richard Gibson Date: Thu, 15 Aug 2024 23:47:24 -0400 Subject: [PATCH 10/13] Editorial: Make auto-linking "read event" and "write event" specializations --- spec.html | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec.html b/spec.html index deb402ec49..f89247f455 100644 --- a/spec.html +++ b/spec.html @@ -49177,7 +49177,7 @@

              Memory Model Fundamentals

              No orderings weaker than sequentially consistent and stronger than unordered, such as release-acquire, are supported.

              -

              A Shared Data Block event is either a ReadSharedMemory, WriteSharedMemory, or ReadModifyWriteSharedMemory Record.

              +

              A Shared Data Block event is either a ReadSharedMemory, WriteSharedMemory, or ReadModifyWriteSharedMemory Record. A read event is either a ReadSharedMemory or a ReadModifyWriteSharedMemory. A write event is either a WriteSharedMemory or a ReadModifyWriteSharedMemory.

              @@ -49686,7 +49686,7 @@

              Sequentially Consistent Atomics

            • 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_.

              -

              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.

              +

              This clause together with the forward progress guarantee on agents ensure the liveness condition that ~seq-cst~ write events become visible to ~seq-cst~ read events with equal memory range in finite time.

            • From a3b78dd9f4c13958956a27a7d6271b6dbe55f289 Mon Sep 17 00:00:00 2001 From: Richard Gibson Date: Wed, 21 Aug 2024 18:25:09 -0400 Subject: [PATCH 11/13] Editorial: Replace auto-linked "{read,write} events" with explicitly linked "{reads,writes}" --- spec.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec.html b/spec.html index f89247f455..b1b6c36c7b 100644 --- a/spec.html +++ b/spec.html @@ -49686,7 +49686,7 @@

              Sequentially Consistent Atomics

            • 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_.

              -

              This clause together with the forward progress guarantee on agents ensure the liveness condition that ~seq-cst~ write events become visible to ~seq-cst~ read events with equal memory range in finite time.

              +

              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.

            • From 077d5c6e43078ac66172e2744b0a1c0850351c42 Mon Sep 17 00:00:00 2001 From: Richard Gibson Date: Sat, 31 Aug 2024 14:27:47 -0400 Subject: [PATCH 12/13] Editorial: Apply suggestions --- spec.html | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/spec.html b/spec.html index b1b6c36c7b..689da9ccef 100644 --- a/spec.html +++ b/spec.html @@ -14886,7 +14886,7 @@

              1. Let _elementSize_ be TypedArrayElementSize(_O_). 1. Let _arrayByteLength_ be _O_.[[ArrayLength]] × _elementSize_. 1. Let _byteOffsetEnd_ be _byteOffsetStart_ + _arrayByteLength_. - 1. NOTE: A 0-length TypedArray with [[ByteOffset]] equal to _bufferByteLength_ is not considered out-of-bounds. + 1. NOTE: A 0-length TypedArray with [[ByteOffset]] of _bufferByteLength_ is not considered out-of-bounds. 1. If _byteOffsetStart_ > _bufferByteLength_ or _byteOffsetEnd_ > _bufferByteLength_, return *true*. 1. Return *false*. @@ -42190,7 +42190,7 @@

              %MapIteratorPrototype% [ %Symbol.toStringTag% ]

              Set Objects

              -

              Set objects are collections of ECMAScript language values. A distinct value may only occur once as an element of a Set's collection. Distinct values are discriminated using the SameValueZero comparison algorithm.

              +

              Set objects are collections of ECMAScript language values. A Set may contain each distinct value at most once. Distinct values are discriminated using the SameValueZero comparison algorithm.

              Set objects must be implemented using either hash tables or other mechanisms that, on average, provide access times that are sublinear on the number of elements in the collection. The data structure used in this specification is only intended to describe the required observable semantics of Set objects. It is not intended to be a viable implementation model.

              @@ -44244,7 +44244,7 @@

              1. Let _byteOffsetEnd_ be _bufferByteLength_. 1. Else, 1. Let _byteOffsetEnd_ be _byteOffsetStart_ + _view_.[[ByteLength]]. - 1. NOTE: A 0-length DataView with [[ByteOffset]] equal to _bufferByteLength_ is not considered out-of-bounds. + 1. NOTE: A 0-length DataView with [[ByteOffset]] of _bufferByteLength_ is not considered out-of-bounds. 1. If _byteOffsetStart_ > _bufferByteLength_ or _byteOffsetEnd_ > _bufferByteLength_, return *true*. 1. Return *false*. @@ -49306,7 +49306,7 @@

              Memory Model Fundamentals

              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 Synchronize events, which have no fields and exist purely to directly constrain the permitted orderings of other events. And finally, there are host-specific events. A Memory event is either a Shared Data Block event, Synchronize event, or such a host-specific event.

              -

              Let the memory range 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.

              +

              Let the memory range of a Shared Data Block event _e_ be the Set of all integers in the interval from _e_.[[ByteIndex]] (inclusive) to _e_.[[ByteIndex]] + _e_.[[ElementSize]] (exclusive). 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.

              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.

              @@ -49443,7 +49443,7 @@

              - 1. Return the subtraction of SharedDataBlockEventSet(_execution_) from EventSet(_execution_). + 1. Return a new Set containing all elements of EventSet(_execution_) that are not in SharedDataBlockEventSet(_execution_). @@ -49762,7 +49762,7 @@

              Shared Memory Guidelines

              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.

              • -

                Atomics are carved in stone: Program transformations must not cause any Shared Data Block events having [[Order]] ~seq-cst~ to be removed from the is-agent-order-before Relation, nor to be reordered with respect to each other, nor to be reordered inside an agent-order slice with respect to events having [[Order]] ~unordered~.

                +

                Atomics are carved in stone: Program transformations must not cause any Shared Data Block events whose [[Order]] is ~seq-cst~ to be removed from the is-agent-order-before Relation, nor to be reordered with respect to each other, nor to be reordered inside an agent-order slice with respect to events whose [[Order]] is ~unordered~.

                (In practice, the prohibition on reorderings forces a compiler to assume that every ~seq-cst~ operation is a synchronization and included in the final is-memory-order-before Relation, which it would usually have to assume anyway in the absence of inter-agent program analysis. It also forces the compiler to assume that every call where the callee's effects on the memory-order are unknown may contain ~seq-cst~ operations.)

              • From 504834b2b9adb6f91a48d7a0df5a1ced63db5700 Mon Sep 17 00:00:00 2001 From: Richard Gibson Date: Tue, 3 Sep 2024 15:52:54 -0400 Subject: [PATCH 13/13] Editorial: Apply suggestions --- spec.html | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec.html b/spec.html index 689da9ccef..844c3ba08f 100644 --- a/spec.html +++ b/spec.html @@ -14886,7 +14886,7 @@

                1. Let _elementSize_ be TypedArrayElementSize(_O_). 1. Let _arrayByteLength_ be _O_.[[ArrayLength]] × _elementSize_. 1. Let _byteOffsetEnd_ be _byteOffsetStart_ + _arrayByteLength_. - 1. NOTE: A 0-length TypedArray with [[ByteOffset]] of _bufferByteLength_ is not considered out-of-bounds. + 1. NOTE: A 0-length TypedArray whose [[ByteOffset]] is _bufferByteLength_ is not considered out-of-bounds. 1. If _byteOffsetStart_ > _bufferByteLength_ or _byteOffsetEnd_ > _bufferByteLength_, return *true*. 1. Return *false*. @@ -44244,7 +44244,7 @@

                1. Let _byteOffsetEnd_ be _bufferByteLength_. 1. Else, 1. Let _byteOffsetEnd_ be _byteOffsetStart_ + _view_.[[ByteLength]]. - 1. NOTE: A 0-length DataView with [[ByteOffset]] of _bufferByteLength_ is not considered out-of-bounds. + 1. NOTE: A 0-length DataView whose [[ByteOffset]] is _bufferByteLength_ is not considered out-of-bounds. 1. If _byteOffsetStart_ > _bufferByteLength_ or _byteOffsetEnd_ > _bufferByteLength_, return *true*. 1. Return *false*.