27 Memory Model
The memory consistency model, or memory model, specifies the possible orderings of
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.
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.
27.1 Memory Model Fundamentals
Shared memory accesses (reads and writes) are divided into two groups, atomic accesses and data accesses, defined below. Atomic accesses are sequentially consistent, i.e., there is a strict total ordering of events agreed upon by all agents in an
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
| Field | Value | Meaning |
|---|---|---|
| [[Order]] | "SeqCst" or "Unordered" |
The weakest ordering guaranteed by the |
| [[NoTear]] | A Boolean | Whether this event is allowed to read from multiple write events on equal range as this event. |
| [[Block]] | A |
The block the event operates on. |
| [[ByteIndex]] | A nonnegative integer | The byte address of the read in [[Block]]. |
| [[ElementSize]] | A nonnegative integer | The size of the read. |
| Field | Value | Meaning |
|---|---|---|
| [[Order]] | "SeqCst", "Unordered", or "Init" |
The weakest ordering guaranteed by the |
| [[NoTear]] | A Boolean | Whether this event is allowed to be read from multiple read events with equal range as this event. |
| [[Block]] | A |
The block the event operates on. |
| [[ByteIndex]] | A nonnegative integer | The byte address of the write in [[Block]]. |
| [[ElementSize]] | A nonnegative integer | The size of the write. |
| [[Payload]] | A |
The |
| Field | Value | Meaning |
|---|---|---|
| [[Order]] | "SeqCst" |
Read-modify-write events are always sequentially consistent. |
| [[NoTear]] | Read-modify-write events cannot tear. | |
| [[Block]] | A |
The block the event operates on. |
| [[ByteIndex]] | A nonnegative integer | The byte address of the read-modify-write in [[Block]]. |
| [[ElementSize]] | A nonnegative integer | The size of the read-modify-write. |
| [[Payload]] | A |
The |
| [[ModifyOp]] | A semantic function | A pure semantic function that returns a modified |
These events are introduced by abstract operations or by methods on the Atomics object.
In addition to
Let the range of a ReadSharedMemory, WriteSharedMemory, or ReadModifyWriteSharedMemory event be the
Examples of host-specific synchronizing events that should be accounted for are: sending a SharedArrayBuffer from one postMessage in a browser), starting and stopping agents, and communicating within the
27.2 Agent Events Records
27.3 Chosen Value Records
A Chosen Value Record is a
| Field | Value | Meaning |
|---|---|---|
| [[Event]] | A |
The |
| [[ChosenValue]] | A |
The bytes that were nondeterministically chosen during evaluation. |
27.4 Candidate Executions
A candidate execution of the evaluation of an
| Field | Value | Meaning |
|---|---|---|
| [[EventLists]] | A |
Maps an |
| [[ChosenValues]] | A |
Maps |
| [[AgentOrder]] | An |
Defined below. |
| [[ReadsBytesFrom]] | A |
Defined below. |
| [[ReadsFrom]] | A |
Defined below. |
| [[HostSynchronizesWith]] | A |
Defined below. |
| [[SynchronizesWith]] | A |
Defined below. |
| [[HappensBefore]] | A |
Defined below. |
An empty candidate execution is a candidate execution
27.5 Abstract Operations for the Memory Model
27.5.1 EventSet( execution )
The abstract operation EventSet takes one argument, a
- Let events be an empty
Set . - For each
Agent Events Record aer in execution.[[EventLists]], do- For each event E in aer.[[EventList]], do
- Add E to events.
- For each event E in aer.[[EventList]], do
- Return events.
27.5.2 SharedDataBlockEventSet( execution )
The abstract operation SharedDataBlockEventSet takes one argument, a
- Let events be an empty
Set . - For each event E in
EventSet (execution), do- If E is a
ReadSharedMemory ,WriteSharedMemory , orReadModifyWriteSharedMemory event, add E to events.
- If E is a
- Return events.
27.5.3 HostEventSet( execution )
The abstract operation HostEventSet takes one argument, a
- Let events be an empty
Set . - For each event E in
EventSet (execution), do- If E is not in
SharedDataBlockEventSet (execution), add E to events.
- If E is not in
- Return events.
27.5.4 ComposeWriteEventBytes( execution, byteIndex, Ws )
The abstract operation ComposeWriteEventBytes takes four arguments, a
- Let byteLocation be byteIndex.
- Let bytesRead be a new empty
List . - For each element W of Ws in
List order, doAssert : W has byteLocation in its range.- Let payloadIndex be byteLocation - W.[[ByteIndex]].
- If W is a
WriteSharedMemory event, then- Let byte be W.[[Payload]][payloadIndex].
- Else,
Assert : W is aReadModifyWriteSharedMemory event.- Let bytes be
ValueOfReadEvent (execution, W). - Let bytesModified be W.[[ModifyOp]](bytes, W.[[Payload]]).
- Let byte be bytesModified[payloadIndex].
- Append byte to bytesRead.
- Increment byteLocation by 1.
- Return bytesRead.
The semantic function [[ModifyOp]] is given by the function properties on the Atomics object that introduce
This abstract operation composes a
27.5.5 ValueOfReadEvent( execution, R )
The abstract operation ValueOfReadEvent takes two arguments, a
Assert : R is aReadSharedMemory orReadModifyWriteSharedMemory event.- Let
reads-bytes-from be execution.[[ReadsBytesFrom]]. - Let Ws be
reads-bytes-from (R). Assert : Ws is aList ofWriteSharedMemory orReadModifyWriteSharedMemory events with length equal to R.[[ElementSize]].- Return
ComposeWriteEventBytes (execution, R.[[ByteIndex]], Ws).
27.6 Relations of Candidate Executions
27.6.1 agent-order
For a
- Let
agent -order be execution.[[AgentOrder]]. - For each pair of events E and D in
EventSet (execution), do- For each
Agent Events Record aer in execution.[[EventLists]], do
- For each
Each
27.6.2 reads-bytes-from
For a
- Let reads-bytes-from be execution.[[ReadsBytesFrom]].
- For each
ReadSharedMemory orReadModifyWriteSharedMemory event R inSharedDataBlockEventSet (execution), do- There is a
List of length equal to R.[[ElementSize]] ofWriteSharedMemory orReadModifyWriteSharedMemory events Ws such that reads-bytes-from(R) is Ws. - Let byteLocation be R.[[ByteIndex]].
- For each element W of Ws in
List order, do- W has byteLocation in its range.
- W is not R.
- Increment byteLocation by 1.
- There is a
27.6.3 reads-from
For a
- Let reads-from be execution.[[ReadsFrom]].
- Let
reads-bytes-from be execution.[[ReadsBytesFrom]]. - For each pair of events R and W in
SharedDataBlockEventSet (execution), do- Let Ws be
reads-bytes-from (R). Assert : Ws is aList ofWriteSharedMemory orReadModifyWriteSharedMemory events.- If Ws contains W, then R reads-from W.
- Let Ws be
27.6.4 host-synchronizes-with
For a
For two host-specific events E and D, E host-synchronizes-with D implies E
The host-synchronizes-with relation allows the host to provide additional synchronization mechanisms, such as postMessage between HTML workers.
27.6.5 synchronizes-with
For a
- Let synchronizes-with be execution.[[SynchronizesWith]].
- Let
reads-from be execution.[[ReadsFrom]]. - Let
host-synchronizes-with be execution.[[HostSynchronizesWith]]. - For each pair of events R and W in
SharedDataBlockEventSet (execution) such that R.[[Order]] is"SeqCst"and Rreads-from W, doAssert : R is aReadSharedMemory orReadModifyWriteSharedMemory event.Assert : W is aWriteSharedMemory orReadModifyWriteSharedMemory event.- If W.[[Order]] is
"SeqCst"and R and W have equal ranges, then W synchronizes-with R. - Else if W has order
"Init", then- Let allInitReads be
true . - For each event V such that R
reads-from V, do- If V.[[Order]] is not
"Init", set allInitReads tofalse .
- If V.[[Order]] is not
- If allInitReads is
true , then W synchronizes-with R.
- Let allInitReads be
- For each pair of events E and D in
HostEventSet (execution), do- If E
host-synchronizes-with D, then E synchronizes-with D.
- If E
Owing to convention, write events synchronizes-with read events, instead of read events synchronizes-with write events.
Not all "SeqCst" events related by
For an event R and an event W such that W synchronizes-with R, R may
27.6.6 happens-before
For a
- Let happens-before be execution.[[HappensBefore]].
- Let
agent -order be execution.[[AgentOrder]]. - Let
synchronizes-with be execution.[[SynchronizesWith]]. - For each pair of events E and D in
EventSet (execution), do- If E is
agent -order before D, then E happens-before D. - If E
synchronizes-with D, then E happens-before D. - If E and D are in
SharedDataBlockEventSet (execution), E.[[Order]] is"Init", and E and D have overlapping ranges, thenAssert : D.[[Order]] is not"Init".- E happens-before D.
- If there is an event F such that E happens-before F and F happens-before D, then E happens-before D.
- If E is
Because happens-before is a superset of
27.7 Properties of Valid Executions
27.7.1 Valid Chosen Reads
A
- For each
ReadSharedMemory orReadModifyWriteSharedMemory event R inSharedDataBlockEventSet (execution), do- Let chosenValue be the element of execution.[[ChosenValues]] whose [[Event]] field is R.
- Let readValue be
ValueOfReadEvent (execution, R). - Let chosenLen be the number of elements of chosenValue.
- Let readLen be the number of elements of readValue.
- chosenLen is equal to readLen and chosenValue[i] is equal to readValue[i] for all integer values i in the range 0 through chosenLen, exclusive.
27.7.2 Coherent Reads
A
- Let
happens-before be execution.[[HappensBefore]]. - Let
reads-bytes-from be execution.[[ReadsBytesFrom]]. - For each
ReadSharedMemory orReadModifyWriteSharedMemory event R inSharedDataBlockEventSet (execution), do- Let Ws be the
List of eventsreads-bytes-from (R). - Let byteLocation be R.[[ByteIndex]].
- For each element W of Ws in
List order, do- It is not the case that R
happens-before W, and - There is no
WriteSharedMemory orReadModifyWriteSharedMemory event V that has byteLocation in its range such that Whappens-before V and Vhappens-before R. - Increment byteLocation by 1.
- It is not the case that R
- Let Ws be the
27.7.3 Tear Free Reads
A
- Let
reads-from be execution.[[ReadsFrom]]. - For each
ReadSharedMemory orReadModifyWriteSharedMemory event R inSharedDataBlockEventSet (execution), do- If R.[[NoTear]] is
true , thenAssert : The remainder of dividing R.[[ByteIndex]] by R.[[ElementSize]] is 0.- For each event W such that R
reads-from W and W.[[NoTear]] istrue , do- If R and W have equal ranges, then there is no V such that V and W have equal range, V.[[NoTear]] is
true , W is not V, and Rreads-from V.
- If R and W have equal ranges, then there is no V such that V and W have equal range, V.[[NoTear]] is
- If R.[[NoTear]] is
An event's [[NoTear]] field is
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.
27.7.4 Sequentially Consistent Atomics
For a
- Let
happens-before be execution.[[HappensBefore]]. - Let
synchronizes-with be execution.[[SynchronizesWith]]. - For each pair of events E and D in
EventSet (execution), do- If E
happens-before D, then E is memory-order before D. - If E and D are in
SharedDataBlockEventSet (execution) and Esynchronizes-with D, thenAssert : D.[[Order]] is"SeqCst".- There is no
WriteSharedMemory orReadModifyWriteSharedMemory event W inSharedDataBlockEventSet (execution) with equal range as D such that W is not E, E is memory-order before W, and W is memory-order before D. - NOTE: This clause additionally constrains
"SeqCst"events on equal ranges.
- If E
- For each
WriteSharedMemory orReadModifyWriteSharedMemory event W inSharedDataBlockEventSet (execution), do- If W.[[Order]] is
"SeqCst", then it is not the case that there is an infinite number ofReadSharedMemory orReadModifyWriteSharedMemory events inSharedDataBlockEventSet (execution) with equal range that is memory-order before W. - NOTE: 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.
- If W.[[Order]] is
A
While memory-order includes all events in
27.7.5 Valid Executions
A
- The host provides a
host-synchronizes-with Relation for execution.[[HostSynchronizesWith]], and - execution.[[HappensBefore]] is a
strict partial order , and - execution has valid chosen reads, and
- execution has coherent reads, and
- execution has tear free reads, and
- execution has sequentially consistent atomics.
All programs have at least one valid execution.
27.8 Races
For an execution execution, two events E and D in
- Let
happens-before be execution.[[HappensBefore]]. - Let
reads-from be execution.[[ReadsFrom]]. - E is not D, and
- It is not the case that E
happens-before D or Dhappens-before E, and - If E and D are both
WriteSharedMemory orReadModifyWriteSharedMemory events, then- E and D do not have disjoint ranges.
- Else,
- E
reads-from D or Dreads-from E.
- E
27.9 Data Races
For an execution execution, two events E and D in
- E and D are in a race in execution, and
- At least one of E or D does not have [[Order]]
"SeqCst"or E and D have overlapping ranges.
27.10 Data Race Freedom
An execution execution is data race free if there are no two events in
A program is data race free if all its executions are data race free.
The
27.11 Shared Memory Guidelines
The following are guidelines for ECMAScript programmers working with shared memory.
We recommend programs be kept data race free, i.e., make it so that it is impossible for there to be concurrent non-atomic operations on the same memory location. Data race free programs have interleaving semantics where each step in the evaluation semantics of each
More generally, even if a program is not data race free it may have predictable behaviour, so long as atomic operations are not involved in any data races and the operations that race all have the same access size. The simplest way to arrange for atomics not to be involved in races is to ensure that different memory cells are used by atomic and non-atomic operations and that atomic accesses of different sizes are not used to access the same cells at the same time. Effectively, the program should treat shared memory as strongly typed as much as possible. One still cannot depend on the ordering and timing of non-atomic accesses that race, but if memory is treated as strongly typed the racing accesses will not "tear" (bits of their values will not be mixed).
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-
Let an agent-order slice be the subset of the
Let possible read values of a read event be the set of all values of
Any transformation of an
-
Atomics are carved in stone: Program transformations must not cause the
"SeqCst"events in anagent-order slice to be reordered with its"Unordered"operations, nor its"SeqCst"operations to be reordered with each other, nor may a program transformation remove a"SeqCst"operation from theagent -order.(In practice, the prohibition on reorderings forces a compiler to assume that every
"SeqCst"operation is a synchronization and included in the finalmemory-order , 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 thememory-order are unknown may contain"SeqCst"operations.) -
Reads must be stable: Any given shared memory read must only observe a single value in an execution.
(For example, if what is semantically a single read in the program is executed multiple times then the program is subsequently allowed to observe only one of the values read. A transformation known as rematerialization can violate this rule.)
-
Writes must be stable: All observable writes to shared memory must follow from program semantics in an execution.
(For example, a transformation may not introduce certain observable writes, such as by using read-modify-write operations on a larger location to write a smaller datum, writing a value to memory that the program could not have written, or writing a just-read value back to the location it was read from, if that location could have been overwritten by another
agent after the read.) -
Possible read values must be nonempty: Program transformations cannot cause the possible read values of a shared memory read to become empty.
(Counterintuitively, this rule in effect restricts transformations on writes, because writes have force in
memory model insofar as to be read by read events. For example, writes may be moved and coalesced and sometimes reordered between two"SeqCst"operations, but the transformation may not remove every write that updates a location; some write must be preserved.)
Examples of transformations that remain valid are: merging multiple non-atomic reads from the same location, reordering non-atomic reads, introducing speculative non-atomic reads, merging multiple non-atomic writes to the same location, reordering non-atomic writes to different locations, and hoisting non-atomic reads out of loops even if that affects termination. Note in general that aliased TypedArrays make it hard to prove that locations are different.
The following are guidelines for ECMAScript implementers generating machine code for shared memory accesses.
For architectures with memory models no weaker than those of ARM or Power, non-atomic stores and loads may be compiled to bare stores and loads on the target architecture. Atomic stores and loads may be compiled down to instructions that guarantee sequential consistency. If no such instructions exist, memory barriers are to be employed, such as placing barriers on both sides of a bare store or load. Read-modify-write operations may be compiled to read-modify-write instructions on the target architectrue, such as LOCK-prefixed instructions on x86, load-exclusive/store-exclusive instructions on ARM, and load-link/store-conditional instructions on Power.
Specifically, the
- Every atomic operation in the program is assumed to be necessary.
- Atomic operations are never rearranged with each other or with non-atomic operations.
- Functions are always assumed to perform atomic operations.
- Atomic operations are never implemented as read-modify-write operations on larger data, but as non-lock-free atomics if the platform does not have atomic operations of the appropriate size. (We already assume that every platform has normal memory access operations of every interesting size.)
Naive code generation uses these patterns:
- Regular loads and stores compile to single load and store instructions.
- Lock-free atomic loads and stores compile to a full (sequentially consistent) fence, a regular load or store, and a full fence.
- 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
A number of local improvements to those basic patterns are also intended to be legal:
- 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.
- Most modern platforms support lock-free atomics for all the data sizes required by ECMAScript atomics. Should non-lock-free atomics be needed, the fences surrounding the body of the atomic operation can usually be folded into the lock and unlock steps. The simplest solution for non-lock-free atomics is to have a single lock word per SharedArrayBuffer.
- There are also more complicated platform-dependent local improvements, requiring some code analysis. For example, two back-to-back fences often have the same effect as a single fence, so if code is generated for two atomic operations in sequence, only a single fence need separate them. On x86, even a single fence separating atomic stores can be omitted, as the fence following a store is only needed to separate the store from a subsequent load.