29 Memory Model
The memory consistency model, or memory model, specifies the possible orderings of
The memory model is defined as relational constraints on
This section provides an axiomatic model on
29.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
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 Name | Value | Meaning |
|---|---|---|
| [[Order]] | The weakest ordering guaranteed by the |
|
| [[NoTear]] | a Boolean | Whether this event is allowed to read from multiple write events with equal memory range as this event. |
| [[Block]] | a |
The block the event operates on. |
| [[ByteIndex]] | a non-negative |
The byte address of the read in [[Block]]. |
| [[ElementSize]] | a non-negative |
The size of the read. |
| Field Name | Value | Meaning |
|---|---|---|
| [[Order]] | The weakest ordering guaranteed by the |
|
| [[NoTear]] | a Boolean | Whether this event is allowed to be read from multiple read events with equal memory range as this event. |
| [[Block]] | a |
The block the event operates on. |
| [[ByteIndex]] | a non-negative |
The byte address of the write in [[Block]]. |
| [[ElementSize]] | a non-negative |
The size of the write. |
| [[Payload]] | a |
The |
| Field Name | Value | Meaning |
|---|---|---|
| [[Order]] | 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 non-negative |
The byte address of the read-modify-write in [[Block]]. |
| [[ElementSize]] | a non-negative |
The size of the read-modify-write. |
| [[Payload]] | a |
The |
| [[ModifyOp]] | a |
An |
Shared Data Block events are introduced to
Let the memory range of a Shared Data Block event e be the Set of all
Examples of postMessage in a browser), starting and stopping
Events are ordered within
29.2 Agent Events Records
An Agent Events Record is a
| Field Name | Value | Meaning |
|---|---|---|
| [[AgentSignifier]] | an |
The |
| [[EventList]] | a |
Events are appended to the list during evaluation. |
| [[AgentSynchronizesWith]] | a |
29.3 Chosen Value Records
A Chosen Value Record is a
| Field Name | Value | Meaning |
|---|---|---|
| [[Event]] | a |
The |
| [[ChosenValue]] | a |
The bytes that were nondeterministically chosen during evaluation. |
29.4 Candidate Executions
A candidate execution of the evaluation of an
| Field Name | Value | Meaning |
|---|---|---|
| [[EventsRecords]] | a |
Maps an |
| [[ChosenValues]] | a |
Maps |
An empty candidate execution is a candidate execution
29.5 Abstract Operations for the Memory Model
29.5.1 EventSet ( execution )
The abstract operation EventSet takes argument execution (a
- Let events be an empty Set.
- For each
Agent Events Record aer of execution.[[EventsRecords]], do- For each
Memory event event of aer.[[EventList]], do- Add event to events.
- For each
- Return events.
29.5.2 SharedDataBlockEventSet ( execution )
The abstract operation SharedDataBlockEventSet takes argument execution (a
- Let events be an empty Set.
- For each
Memory event event ofEventSet (execution), do- If event is a
Shared Data Block event , add event to events.
- If event is a
- Return events.
29.5.3 HostEventSet ( execution )
The abstract operation HostEventSet takes argument execution (a
- Return a new Set containing all elements of
EventSet (execution) that are not inSharedDataBlockEventSet (execution).
29.5.4 ComposeWriteEventBytes ( execution, byteIndex, writes )
The abstract operation ComposeWriteEventBytes takes arguments execution (a
- Let byteLocation be byteIndex.
- Let bytesRead be a new empty
List . - For each element writeEvent of writes, do
Assert : writeEvent has byteLocation in itsmemory range .- Let payloadIndex be byteLocation - writeEvent.[[ByteIndex]].
- If writeEvent is a
WriteSharedMemory event, then- Let byte be writeEvent.[[Payload]][payloadIndex].
- Else,
Assert : writeEvent is aReadModifyWriteSharedMemory event.- Let bytes be
ValueOfReadEvent (execution, writeEvent). - Let bytesModified be writeEvent.[[ModifyOp]](bytes, writeEvent.[[Payload]]).
- Let byte be bytesModified[payloadIndex].
- Append byte to bytesRead.
- Set byteLocation to byteLocation + 1.
- Return bytesRead.
The read-modify-write modification [[ModifyOp]] is given by the function properties on the Atomics object that introduce
This abstract operation composes a
29.5.5 ValueOfReadEvent ( execution, readEvent )
The abstract operation ValueOfReadEvent takes arguments execution (a
- Let writes be
reads-bytes-from (readEvent) in execution. Assert : writes is aList ofWriteSharedMemory orReadModifyWriteSharedMemory events with length equal to readEvent.[[ElementSize]].- Return
ComposeWriteEventBytes (execution, readEvent.[[ByteIndex]], writes).
29.6 Relations of Candidate Executions
The following relations and mathematical functions are parameterized over a particular
29.6.1 is-agent-order-before
For a
- For events eventA and eventB, eventA is-agent-order-before eventB in execution if there is some
Agent Events Record aer in execution.[[EventsRecords]] such that aer.[[EventList]] contains both eventA and eventB and eventA is before eventB inList order of aer.[[EventList]].
Each
29.6.2 reads-bytes-from
For a
-
For each
ReadSharedMemory orReadModifyWriteSharedMemory event readEvent inSharedDataBlockEventSet (execution), reads-bytes-from(readEvent) in execution is aList of length readEvent.[[ElementSize]] whose elements areWriteSharedMemory orReadModifyWriteSharedMemory events writes such that all of the following are true.- Each event writeEvent with index i in writes has readEvent.[[ByteIndex]] + i in its
memory range . - result is not in writes.
- Each event writeEvent with index i in writes has readEvent.[[ByteIndex]] + i in its
A
29.6.3 reads-from
For a
- For events readEvent and writeEvent, readEvent reads-from writeEvent in execution if
SharedDataBlockEventSet (execution) contains both readEvent and writeEvent, andreads-bytes-from (readEvent) in execution contains writeEvent.
29.6.4 host-synchronizes-with
For a
- If eventA host-synchronizes-with eventB in execution,
HostEventSet (execution) contains eventA and eventB. - There is no cycle in the union of host-synchronizes-with and
is-agent-order-before in execution.
For two
29.6.5 synchronizes-with
For a
-
For events readEvent and writeEvent, writeEvent synchronizes-with readEvent in execution if readEvent
reads-from writeEvent in execution, readEvent.[[Order]] isseq-cst , writeEvent.[[Order]] isseq-cst , and readEvent and writeEvent have equalmemory ranges . -
For each element eventsRecord of execution.[[EventsRecords]], the following is true.
- For events eventA and eventB, eventA synchronizes-with eventB in execution if eventsRecord.[[AgentSynchronizesWith]] contains (eventA, eventB).
- For events eventA and eventB, eventA synchronizes-with eventB in execution if eventA
host-synchronizes-with eventB in execution.
Owing to convention in
In a
In a
For
29.6.6 happens-before
For a
-
For events eventA and eventB, eventA happens-before eventB in execution if any of the following conditions are true.
- eventA
is-agent-order-before eventB in execution. - eventA
synchronizes-with eventB in execution. SharedDataBlockEventSet (execution) contains both eventA and eventB, eventA.[[Order]] isinit , and eventA and eventB have overlappingmemory ranges .- There is an event eventC such that eventA happens-before eventC and eventC happens-before eventB in execution.
- eventA
Because happens-before is a superset of
29.7 Properties of Valid Executions
29.7.1 Valid Chosen Reads
A
- For each
ReadSharedMemory orReadModifyWriteSharedMemory event readEvent ofSharedDataBlockEventSet (execution), do- Let chosenValueRecord be the element of execution.[[ChosenValues]] whose [[Event]] field is readEvent.
- Let chosenValue be chosenValueRecord.[[ChosenValue]].
- Let readValue be
ValueOfReadEvent (execution, readEvent). - Let chosenLength be the number of elements in chosenValue.
- Let readLength be the number of elements in readValue.
- If chosenLength ≠ readLength, then
- Return
false .
- Return
- If chosenValue[i] ≠ readValue[i] for some
integer i in theinterval from 0 (inclusive) to chosenLength (exclusive), then- Return
false .
- Return
- Return
true .
29.7.2 Coherent Reads
A
- For each
ReadSharedMemory orReadModifyWriteSharedMemory event readEvent ofSharedDataBlockEventSet (execution), do- Let writes be
reads-bytes-from (readEvent) in execution. - Let byteLocation be readEvent.[[ByteIndex]].
- For each element writeEvent of writes, do
- If readEvent
happens-before writeEvent in execution, then- Return
false .
- Return
- If there exists a
WriteSharedMemory orReadModifyWriteSharedMemory event value that has byteLocation in itsmemory range such that writeEventhappens-before value in execution and valuehappens-before readEvent in execution, then- Return
false .
- Return
- Set byteLocation to byteLocation + 1.
- If readEvent
- Let writes be
- Return
true .
29.7.3 Tear Free Reads
A
- For each
ReadSharedMemory orReadModifyWriteSharedMemory event readEvent ofSharedDataBlockEventSet (execution), do- If readEvent.[[NoTear]] is
true , thenAssert : The remainder of dividing readEvent.[[ByteIndex]] by readEvent.[[ElementSize]] is 0.- For each
Memory event writeEvent such that readEventreads-from writeEvent in execution and writeEvent.[[NoTear]] istrue , do- If readEvent and writeEvent have equal
memory ranges and there exists aMemory event value such that value and writeEvent have equalmemory ranges , value.[[NoTear]] istrue , writeEvent and value are not the sameShared Data Block event , and readEventreads-from value in execution, then- Return
false .
- Return
- If readEvent and writeEvent have equal
- If readEvent.[[NoTear]] is
- Return
true .
A
Intuitively, this requirement says when a
29.7.4 Sequentially Consistent Atomics
For a
- For events eventA and eventB, eventA is-memory-order-before eventB in execution if eventA
happens-before eventB in execution. -
For events readEvent and writeEvent such that readEvent
reads-from writeEvent in execution, there is noWriteSharedMemory orReadModifyWriteSharedMemory event value inSharedDataBlockEventSet (execution) such that value.[[Order]] isseq-cst , writeEvent is-memory-order-before value in execution, value is-memory-order-before readEvent in execution, and any of the following conditions are true.- writeEvent
synchronizes-with readEvent in execution, and value and readEvent have equalmemory ranges . - writeEvent
happens-before readEvent and valuehappens-before readEvent in execution, writeEvent.[[Order]] isseq-cst , and writeEvent and value have equalmemory ranges . - writeEvent
happens-before readEvent and writeEventhappens-before value in execution, readEvent.[[Order]] isseq-cst , and value and readEvent have equalmemory ranges .
Note 1 This clause additionally constrains
seq-cst events on equalmemory ranges . - writeEvent
-
For each
WriteSharedMemory orReadModifyWriteSharedMemory event writeEvent inSharedDataBlockEventSet (execution), if writeEvent.[[Order]] isseq-cst , then it is not the case that there is an infinite number ofReadSharedMemory orReadModifyWriteSharedMemory events inSharedDataBlockEventSet (execution) with equalmemory range that is memory-order before writeEvent.Note 2 This clause together with the forward progress guarantee on
agents ensure the liveness condition thatseq-cst writes become visible toseq-cst reads with equalmemory range infinite time.
A
While is-memory-order-before includes all events in
29.7.5 Valid Executions
A
- The
host provides ahost-synchronizes-with Relation for execution. - execution admits a
happens-before Relation that is astrict 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.
29.8 Races
For an execution execution and events eventA and eventB that are contained in
- If eventA and eventB are not the same
Shared Data Block event , then- If it is not the case that both eventA
happens-before eventB in execution and eventBhappens-before eventA in execution, then- If eventA is either a
WriteSharedMemory orReadModifyWriteSharedMemory event, eventB is either aWriteSharedMemory orReadModifyWriteSharedMemory event, and eventA and eventB do not have disjointmemory ranges , then- Return
true .
- Return
- If eventA
reads-from eventB in execution or eventBreads-from eventA in execution, then- Return
true .
- Return
- If eventA is either a
- If it is not the case that both eventA
- Return
false .
29.9 Data Races
For an execution execution and events eventA and eventB that are contained in
- If eventA and eventB are in a
race in execution, then- If eventA.[[Order]] is not
seq-cst or eventB.[[Order]] is notseq-cst , then- Return
true .
- Return
- If eventA and eventB have overlapping
memory ranges , then- Return
true .
- Return
- If eventA.[[Order]] is not
- Return
false .
29.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
29.11 Shared Memory Guidelines
The following are guidelines for ECMAScript programmers working with shared memory.
We recommend programs be kept
More generally, even if a program is not
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
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 whose [[Order]] isseq-cst to be removed from theis-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]] isunordered .(In practice, the prohibition on reorderings forces a compiler to assume that every
seq-cst operation is a synchronization and included in the finalis-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 containseq-cst 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 non-empty: 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 byread events . For example, writes may be moved and coalesced and sometimes reordered between twoseq-cst 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
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 architecture, 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 a
Local improvements to those basic patterns are also allowed, subject to the constraints of the
- 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.