?
u
m
/
The memory consistency model, or memory model, specifies the possible orderings of
The memory model is defined as relational constraints on events introduced by
This section provides an axiomatic model on events introduced by the
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 on equal 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 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 abstract closure that returns a modified |
These events are introduced by
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
Let the range of a ReadSharedMemory, WriteSharedMemory, or ReadModifyWriteSharedMemory event be the Set of contiguous
Examples of postMessage
in a browser), starting and stopping
Events are ordered within
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 |
A Chosen Value Record is a
Field Name | Value | Meaning |
---|---|---|
[[Event]] | a |
The |
[[ChosenValue]] | a |
The bytes that were nondeterministically chosen during evaluation. |
A candidate execution of the evaluation of an
Field Name | Value | Meaning |
---|---|---|
[[EventsRecords]] | 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
The abstract operation EventSet takes argument execution (a
The abstract operation SharedDataBlockEventSet takes argument execution (a
The abstract operation HostEventSet takes argument execution (a
The abstract operation ComposeWriteEventBytes takes arguments execution (a
The read-modify-write modification [[ModifyOp]] is given by the function properties on the Atomics object that introduce
This abstract operation composes a
The abstract operation ValueOfReadEvent takes arguments execution (a
For a
Each
For a
For each
For a
For a
For two
The host-synchronizes-with relation allows the postMessage
between HTML workers.
For a
Owing to convention, write events synchronizes-with read events, instead of read events synchronizes-with write events.
Not all
For
For a
Because happens-before is a superset of
A
A
A
An event's [[NoTear]] field is
Intuitively, this requirement says when a memory range is accessed in an aligned fashion via an
For a
For each pair (R, W) in execution.[[ReadsFrom]], there is no
This clause additionally constrains
For each
This clause together with the forward progress guarantee on
A
While memory-order includes all events in
A
All programs have at least one valid execution.
For an execution execution, two events E and D in
For an execution execution, two events E and D in
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
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 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
(In practice, the prohibition on reorderings forces a compiler to assume that every
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
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
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 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
Naive code generation uses these patterns:
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:
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.