ECMAScript® 2024 Language Specification

Draft ECMA-262 / December 6, 2023

29.7 Properties of Valid Executions

29.7.1 Valid Chosen Reads

A candidate execution execution has valid chosen reads if the following algorithm returns true.

  1. For each ReadSharedMemory or ReadModifyWriteSharedMemory event R of SharedDataBlockEventSet(execution), do
    1. Let chosenValueRecord be the element of execution.[[ChosenValues]] whose [[Event]] field is R.
    2. Let chosenValue be chosenValueRecord.[[ChosenValue]].
    3. Let readValue be ValueOfReadEvent(execution, R).
    4. Let chosenLen be the number of elements in chosenValue.
    5. Let readLen be the number of elements in readValue.
    6. If chosenLen ≠ readLen, then
      1. Return false.
    7. If chosenValue[i] ≠ readValue[i] for some integer i in the interval from 0 (inclusive) to chosenLen (exclusive), then
      1. Return false.
  2. Return true.

29.7.2 Coherent Reads

A candidate execution execution has coherent reads if the following algorithm returns true.

  1. For each ReadSharedMemory or ReadModifyWriteSharedMemory event R of SharedDataBlockEventSet(execution), do
    1. Let Ws be execution.[[ReadsBytesFrom]](R).
    2. Let byteLocation be R.[[ByteIndex]].
    3. For each element W of Ws, do
      1. If execution.[[HappensBefore]] contains (R, W), then
        1. Return false.
      2. If there exists a WriteSharedMemory or ReadModifyWriteSharedMemory event V that has byteLocation in its range such that the pairs (W, V) and (V, R) are in execution.[[HappensBefore]], then
        1. Return false.
      3. Set byteLocation to byteLocation + 1.
  2. Return true.

29.7.3 Tear Free Reads

A candidate execution execution has tear free reads if the following algorithm returns true.

  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.
      2. For each event W such that execution.[[ReadsFrom]] contains (R, W) 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 is not V, and execution.[[ReadsFrom]] contains (R, V), then
          1. Return false.
  2. Return true.
 Note

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.

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.

29.7.4 Sequentially Consistent Atomics

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

  • For each pair (E, D) in execution.[[HappensBefore]], (E, D) is in memory-order.

  • For each pair (R, W) in execution.[[ReadsFrom]], there is no WriteSharedMemory or ReadModifyWriteSharedMemory event V in SharedDataBlockEventSet(execution) such that V.[[Order]] is seq-cst, the pairs (W, V) and (V, R) are in memory-order, and any of the following conditions are true.

    • execution.[[SynchronizesWith]] contains the pair (W, R), and V and R have equal ranges.
    • The pairs (W, R) and (V, R) are in execution.[[HappensBefore]], W.[[Order]] is seq-cst, and W and V have equal ranges.
    • The pairs (W, R) and (W, V) are in execution.[[HappensBefore]], R.[[Order]] is seq-cst, and V and R have equal ranges.
    Note 1

    This clause additionally constrains seq-cst events on equal 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.

    Note 2

    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.

A candidate execution has sequentially consistent atomics if a memory-order exists.

Note 3

While memory-order includes all events in EventSet(execution), those that are not constrained by happens-before or synchronizes-with are allowed to occur anywhere in the order.

29.7.5 Valid Executions

A candidate execution execution is a valid execution (or simply an execution) if all of the following are true.

  • The host provides a host-synchronizes-with Relation for execution.[[HostSynchronizesWith]].
  • execution.[[HappensBefore]] is a strict partial order.
  • execution has valid chosen reads.
  • execution has coherent reads.
  • execution has tear free reads.
  • execution has sequentially consistent atomics.

All programs have at least one valid execution.