29.7 Properties of Valid Executions

29.7.1 Valid Chosen Reads

A candidate execution execution has valid chosen reads if the following abstract operation 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 of chosenValue.
    5. Let readLen be the number of elements of readValue.
    6. If chosenLenreadLen, then
      1. Return false.
    7. If chosenValue[i] ≠ readValue[i] for any integer value i in the range 0 through chosenLen, exclusive, then
      1. Return false.
  2. Return true.

29.7.2 Coherent Reads

A candidate execution execution has coherent reads if the following abstract operation 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 (R, W) is in execution.[[HappensBefore]], then
        1. Return false.
      2. If there is 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 abstract operation 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 (R, W) is in execution.[[ReadsFrom]] and W.[[NoTear]] is true, do
        1. If R and W have equal ranges, and there is an event V such that V and W have equal ranges, V.[[NoTear]] is true, W is not V, and (R, V) is in execution.[[ReadsFrom]], 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 SeqCst, the pairs (W, V) and (V, R) are in memory-order, and any of the following conditions are true.

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

    This clause additionally constrains SeqCst events on equal ranges.

  • For each WriteSharedMemory or ReadModifyWriteSharedMemory event W in SharedDataBlockEventSet(execution), if W.[[Order]] is SeqCst, 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 SeqCst writes become visible to SeqCst 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.