RVWMO Memory Consistency Model, Version 2.0
This chapter defines the RISC-V memory consistency model. A memory consistency model is a set of rules specifying the values that can be returned by loads of memory. RISC-V uses a memory model called "RVWMO" (RISC-V Weak Memory Ordering) which is designed to provide flexibility for architects to build high-performance scalable designs while simultaneously supporting a tractable programming model.
Under RVWMO, code running on a single hart appears to execute in order from the perspective of other memory instructions in the same hart, but memory instructions from another hart may observe the memory instructions from the first hart being executed in a different order. Therefore, multithreaded code may require explicit synchronization to guarantee ordering between memory instructions from different harts. The base RISC-V ISA provides a FENCE instruction for this purpose, described in [fence], while the atomics extension "A" additionally defines load-reserved/store-conditional and atomic read-modify-write instructions.
The standard ISA extension for total store ordering "Ztso" ([ztso]) augments RVWMO with additional rules specific to those extensions.
The appendices to this specification provide both axiomatic and operational formalizations of the memory consistency model as well as additional explanatory material.
|
This chapter defines the memory model for regular main memory operations. The interaction of the memory model with I/O memory, instruction fetches, FENCE.I, page table walks, and SFENCE.VMA is not (yet) formalized. Some or all of the above may be formalized in a future revision of this specification. The RV128 base ISA and future ISA extensions such as the V vector and J JIT extensions will need to be incorporated into a future revision as well. Memory consistency models supporting overlapping memory accesses of different widths simultaneously remain an active area of academic research and are not yet fully understood. The specifics of how memory accesses of different sizes interact under RVWMO are specified to the best of our current abilities, but they are subject to revision should new issues be uncovered. |
Definition of the RVWMO Memory Model
The RVWMO memory model is defined in terms of the global memory order, a total ordering of the memory operations produced by all harts. In general, a multithreaded program has many different possible executions, with each execution having its own corresponding global memory order.
The global memory order is defined over the primitive load and store operations generated by memory instructions. It is then subject to the constraints defined in the rest of this chapter. Any execution satisfying all of the memory model constraints is a legal execution (as far as the memory model is concerned).
Memory Model Primitives
The program order over memory operations reflects the order in which the instructions that generate each load and store are logically laid out in that hart’s dynamic instruction stream; i.e., the order in which a simple in-order processor would execute the instructions of that hart.
Memory-accessing instructions give rise to memory operations. A memory operation can be either a load operation, a store operation, or both simultaneously. All memory operations are single-copy atomic: they can never be observed in a partially complete state.
Among instructions in RV32GC and RV64GC, each aligned memory instruction gives rise to exactly one memory operation, with two exceptions. First, an unsuccessful SC instruction does not give rise to any memory operations. Second, FLD and FSD instructions may each give rise to multiple memory operations if XLEN<64, as stated in [fld_fsd] and clarified below. An aligned AMO gives rise to a single memory operation that is both a load operation and a store operation simultaneously.
|
Instructions in the RV128 base instruction set and in future ISA extensions such as V (vector) and P (SIMD) may give rise to multiple memory operations. However, the memory model for these extensions has not yet been formalized. |
A misaligned load or store instruction may be decomposed into a set of component memory operations of any granularity. An FLD or FSD instruction for which XLEN<64 may also be decomposed into a set of component memory operations of any granularity. The memory operations generated by such instructions are not ordered with respect to each other in program order, but they are ordered normally with respect to the memory operations generated by preceding and subsequent instructions in program order. The atomics extension "A" does not require execution environments to support misaligned atomic instructions at all. However, if misaligned atomics are supported via the misaligned atomicity granule PMA, then AMOs within an atomicity granule are not decomposed, nor are loads and stores defined in the base ISAs, nor are loads and stores of no more than XLEN bits defined in the F, D, and Q extensions.
|
The decomposition of misaligned memory operations down to byte granularity facilitates emulation on implementations that do not natively support misaligned accesses. Such implementations might, for example, simply iterate over the bytes of a misaligned access one by one. |
An LR instruction and an SC instruction are said to be paired if the LR precedes the SC in program order and if there are no other LR or SC instructions in between; the corresponding memory operations are said to be paired as well (except in case of a failed SC, where no store operation is generated). The complete list of conditions determining whether an SC must succeed, may succeed, or must fail is defined in [sec:lrsc].
Load and store operations may also carry one or more ordering annotations from the following set: "acquire-RCpc", "acquire-RCsc", "release-RCpc", and "release-RCsc". An AMO or LR instruction with aq set has an "acquire-RCsc" annotation. An AMO or SC instruction with rl set has a "release-RCsc" annotation. An AMO, LR, or SC instruction with both aq and rl set has both "acquire-RCsc" and "release-RCsc" annotations.
For convenience, we use the term "acquire annotation" to refer to an acquire-RCpc annotation or an acquire-RCsc annotation. Likewise, a "release annotation" refers to a release-RCpc annotation or a release-RCsc annotation. An "RCpc annotation" refers to an acquire-RCpc annotation or a release-RCpc annotation. An RCsc annotation refers to an acquire-RCsc annotation or a release-RCsc annotation.
|
In the memory model literature, the term "RCpc" stands for release consistency with processor-consistent synchronization operations, and the term "RCsc" stands for release consistency with sequentially consistent synchronization operations. While there are many different definitions for acquire and release annotations in the literature, in the context of RVWMO these terms are concisely and completely defined by Preserved Program Order rules 5-7. "RCpc" annotations are currently only used when implicitly assigned to every memory access per the standard extension "Ztso" ([ztso]). Furthermore, although the ISA does not currently contain native load-acquire or store-release instructions, nor RCpc variants thereof, the RVWMO model itself is designed to be forwards-compatible with the potential addition of any or all of the above into the ISA in a future extension. |
Syntactic Dependencies
The definition of the RVWMO memory model depends in part on the notion of a syntactic dependency, defined as follows.
In the context of defining dependencies, a register refers either to an entire general-purpose register, some portion of a CSR, or an entire CSR. The granularity at which dependencies are tracked through CSRs is specific to each CSR and is defined in CSR Dependency Tracking Granularity.
Syntactic dependencies are defined in terms of instructions' source registers, instructions' destination registers, and the way instructions carry a dependency from their source registers to their destination registers. This section provides a general definition of all of these terms; however, Source and Destination Register Listings provides a complete listing of the specifics for each instruction.
In general, a register r other than x0 is a source
register for an instruction i if any of the following
hold:
-
In the opcode of i, rs1, rs2, or rs3 is set to r
-
i is a CSR instruction, and in the opcode of i, csr is set to r, unless i is CSRRW or CSRRWI and rd is set to
x0 -
r is a CSR and an implicit source register for i, as defined in Source and Destination Register Listings
-
r is a CSR that aliases with another source register for i
Memory instructions also further specify which source registers are address source registers and which are data source registers.
In general, a register r other than x0 is a destination
register for an instruction i if any of the following
hold:
-
In the opcode of i, rd is set to r
-
i is a CSR instruction, and in the opcode of i, csr is set to r, unless i is CSRRS or CSRRC and rs1 is set to
x0or i is CSRRSI or CSRRCI and uimm[4:0] is set to zero. -
r is a CSR and an implicit destination register for i, as defined in Source and Destination Register Listings
-
r is a CSR that aliases with another destination register for i
Most non-memory instructions carry a dependency from each of their source registers to each of their destination registers. However, there are exceptions to this rule; see Source and Destination Register Listings.
Instruction j has a syntactic dependency on instruction i via destination register s of i and source register r of j if either of the following hold:
-
s is the same as r, and no instruction program-ordered between i and j has r as a destination register
-
There is an instruction m program-ordered between i and j such that all of the following hold:
-
j has a syntactic dependency on m via destination register q and source register r
-
m has a syntactic dependency on i via destination register s and source register p
-
m carries a dependency from p to q
-
Finally, in the definitions that follow, let a and b be two memory operations, and let i and j be the instructions that generate a and b, respectively.
b has a syntactic address dependency on a if r is an address source register for j and j has a syntactic dependency on i via source register r
b has a syntactic data dependency on a if b is a store operation, r is a data source register for j, and j has a syntactic dependency on i via source register r
b has a syntactic control dependency on a if there is an instruction m program-ordered between i and j such that m is a branch or indirect jump and m has a syntactic dependency on i.
|
Generally speaking, non-AMO load instructions do not have data source registers, and unconditional non-AMO store instructions do not have destination registers. However, a successful SC instruction is considered to have the register specified in rd as a destination register, and hence it is possible for an instruction to have a syntactic dependency on a successful SC instruction that precedes it in program order. |
Preserved Program Order
The global memory order for any given execution of a program respects some but not all of each hart’s program order. The subset of program order that must be respected by the global memory order is known as preserved program order.
The complete definition of preserved program order is as follows (and note that AMOs are simultaneously both loads and stores): memory operation a precedes memory operation b in preserved program order (and hence also in the global memory order) if a precedes b in program order, a and b both access regular main memory (rather than I/O regions), and any of the following hold:
-
Overlapping-Address Orderings:
-
b is a store, and a and b access overlapping memory addresses
-
a and b are loads, x is a byte read by both a and b, there is no store to x between a and b in program order, and a and b return values for x written by different memory operations
-
a is generated by an AMO or SC instruction, b is a load, and b returns a value written by a
-
-
Explicit Synchronization
-
There is a FENCE instruction that orders a before b
-
a has an acquire annotation
-
b has a release annotation
-
a and b both have RCsc annotations
-
a is paired with b
-
-
Syntactic Dependencies
-
b has a syntactic address dependency on a
-
b has a syntactic data dependency on a
-
b is a store, and b has a syntactic control dependency on a
-
-
Pipeline Dependencies
-
b is a load, and there exists some store m between a and b in program order such that m has an address or data dependency on a, and b returns a value written by m
-
b is a store, and there exists some instruction m between a and b in program order such that m has an address dependency on a
-
Memory Model Axioms
An execution of a RISC-V program obeys the RVWMO memory consistency model only if there exists a global memory order conforming to preserved program order and satisfying the load value axiom, the atomicity axiom, and the progress axiom.
Load Value Axiom
Each byte of each load i returns the value written to that byte by the store that is the latest in global memory order among the following stores:
-
Stores that write that byte and that precede i in the global memory order
-
Stores that write that byte and that precede i in program order
Atomicity Axiom
If r and w are paired load and store operations generated by aligned LR and SC instructions in a hart h, s is a store to byte x, and r returns a value written by s, then s must precede w in the global memory order, and there can be no store from a hart other than h to byte x following s and preceding w in the global memory order.
|
The Atomicity Axiom theoretically supports LR/SC pairs of different widths and to mismatched addresses, since implementations are permitted to allow SC operations to succeed in such cases. However, in practice, we expect such patterns to be rare, and their use is discouraged. |
CSR Dependency Tracking Granularity
| Name | Portions Tracked as Independent Units | Aliases |
|---|---|---|
fflags |
Bits 4, 3, 2, 1, 0 |
fcsr |
frm |
entire CSR |
fcsr |
fcsr |
Bits 7-5, 4, 3, 2, 1, 0 |
fflags, frm |
Note: read-only CSRs are not listed, as they do not participate in the definition of syntactic dependencies.
Source and Destination Register Listings
This section provides a concrete listing of the source and destination registers for each instruction. These listings are used in the definition of syntactic dependencies in Syntactic Dependencies.
The term "accumulating CSR" is used to describe a CSR that is both a source and a destination register, but which carries a dependency only from itself to itself.
Instructions carry a dependency from each source register in the "Source Registers" column to each destination register in the "Destination Registers" column, from each source register in the "Source Registers" column to each CSR in the "Accumulating CSRs" column, and from each CSR in the "Accumulating CSRs" column to itself, except where annotated otherwise.
Key:
-
AAddress source register
-
DData source register
-
† The instruction does not carry a dependency from any source register to any destination register
-
‡ The instruction carries dependencies from source register(s) to destination register(s) as specified
| Source Registers | Destination Registers | Accumulating CSRs | ||
|---|---|---|---|---|
LUI |
rd |
|||
AUIPC |
rd |
|||
JAL |
rd |
|||
JALR† |
rs1 |
rd |
||
BEQ |
rs1, rs2 |
|||
BNE |
rs1, rs2 |
|||
BLT |
rs1, rs2 |
|||
BGE |
rs1, rs2 |
|||
BLTU |
rs1, rs2 |
|||
BGEU |
rs1, rs2 |
|||
LB † |
rs1 A |
rd |
||
LH † |
rs1 A |
rd |
||
LW † |
rs1 A |
rd |
||
LBU † |
rs1 A |
rd |
||
LHU † |
rs1 A |
rd |
||
SB |
rs1 A, rs2 D |
|||
SH |
rs1 A, rs2 D |
|||
SW |
rs1 A, rs2 D |
|||
ADDI |
rs1 |
rd |
||
SLTI |
rs1 |
rd |
||
SLTIU |
rs1 |
rd |
||
XORI |
rs1 |
rd |
||
ORI |
rs1 |
rd |
||
ANDI |
rs1 |
rd |
||
SLLI |
rs1 |
rd |
||
SRLI |
rs1 |
rd |
||
SRAI |
rs1 |
rd |
||
ADD |
rs1, rs2 |
rd |
||
SUB |
rs1, rs2 |
rd |
||
SLL |
rs1, rs2 |
rd |
||
SLT |
rs1, rs2 |
rd |
||
SLTU |
rs1, rs2 |
rd |
||
XOR |
rs1, rs2 |
rd |
||
SRL |
rs1, rs2 |
rd |
||
SRA |
rs1, rs2 |
rd |
||
OR |
rs1, rs2 |
rd |
||
AND |
rs1, rs2 |
rd |
||
FENCE |
||||
FENCE.I |
||||
ECALL |
||||
EBREAK |
||||
CSRRW‡ |
rs1, csr* |
rd, csr |
*unless rd= |
|
CSRRS‡ |
rs1, csr |
rd *, csr |
*unless rs1= |
|
CSRRC‡ |
rs1, csr |
rd *, csr |
*unless rs1= |
|
‡ carries a dependency from rs1 to csr and from csr to rd |
||||
CSRRWI ‡ |
csr * |
rd, csr |
*unless rd=x0 |
|
CSRRSI ‡ |
csr |
rd, csr* |
*unless uimm[4:0]=0 |
|
CSRRCI ‡ |
csr |
rd, csr* |
*unless uimm[4:0]=0 |
|
| Source Registers | Destination Registers | Accumulating CSRs | ||
|---|---|---|---|---|
LWU † |
rs1 A |
rd |
||
LD † |
rs1 A |
rd |
||
SD |
rs1 A, rs2 D |
|||
SLLI |
rs1 |
rd |
||
SRLI |
rs1 |
rd |
||
SRAI |
rs1 |
rd |
||
ADDIW |
rs1 |
rd |
||
SLLIW |
rs1 |
rd |
||
SRLIW |
rs1 |
rd |
||
SRAIW |
rs1 |
rd |
||
ADDW |
rs1, rs2 |
rd |
||
SUBW |
rs1, rs2 |
rd |
||
SLLW |
rs1, rs2 |
rd |
||
SRLW |
rs1, rs2 |
rd |
||
SRAW |
rs1, rs2 |
rd |
| Source Registers | Destination Registers | Accumulating CSRs | ||
|---|---|---|---|---|
MUL |
rs1, rs2 |
rd |
||
MULH |
rs1, rs2 |
rd |
||
MULHSU |
rs1, rs2 |
rd |
||
MULHU |
rs1, rs2 |
rd |
||
DIV |
rs1, rs2 |
rd |
||
DIVU |
rs1, rs2 |
rd |
||
REM |
rs1, rs2 |
rd |
||
REMU |
rs1, rs2 |
rd |
| Source Registers | Destination Registers | Accumulating CSRs | ||
|---|---|---|---|---|
MULW |
rs1, rs2 |
rd |
||
DIVW |
rs1, rs2 |
rd |
||
DIVUW |
rs1, rs2 |
rd |
||
REMW |
rs1, rs2 |
rd |
||
REMUW |
rs1, rs2 |
rd |
| Source Registers | Destination Registers | Accumulating CSRs | ||
|---|---|---|---|---|
LR.W† |
rs1 A |
rd |
||
SC.W† |
rs1 A, rs2 D |
rd * |
* if successful |
|
AMOSWAP.W† |
rs1 A, rs2 D |
rd |
||
AMOADD.W† |
rs1 A, rs2 D |
rd |
||
AMOXOR.W† |
rs1 A, rs2 D |
rd |
||
AMOAND.W† |
rs1 A, rs2 D |
rd |
||
AMOOR.W† |
rs1 A, rs2D |
rd |
||
AMOMIN.W† |
rs1 A, rs2 D |
rd |
||
AMOMAX.W† |
rs1 A, rs2 D |
rd |
||
AMOMINU.W† |
rs1 A, rs2 D |
rd |
||
AMOMAXU.W† |
rs1 A, rs2 D |
rd |
| Source Registers | Destination Registers | Accumulating CSRs | ||
|---|---|---|---|---|
LR.D† |
rs1 A |
rd |
||
SC.D† |
rs1 A, rs2 D |
rd * |
*if successful |
|
AMOSWAP.D† |
rs1 A, rs2 D |
rd |
||
AMOADD.D† |
rs1 A, rs2 D |
rd |
||
AMOXOR.D† |
rs1 A, rs2 D |
rd |
||
AMOAND.D† |
rs1 A, rs2D |
rd |
||
AMOOR.D† |
rs1 A, rs2D |
rd |
||
AMOMIN.D† |
rs1 A, rs2D |
rd |
||
AMOMAX.D† |
rs1 A, rs2D |
rd |
||
AMOMINU.D† |
rs1 A, rs2D |
rd |
||
AMOMAXU.D† |
rs1 A, rs2D |
rd |
| Source Registers | Destination Registers | Accumulating CSRs | ||
|---|---|---|---|---|
FLW† |
rs1 A |
rd |
||
FSW |
rs1 A, rs2D |
|||
FMADD.S |
rs1, rs2, rs3, frm* |
rd |
NV, OF, UF, NX |
*if rm=111 |
FMSUB.S |
rs1, rs2, rs3, frm* |
rd |
NV, OF, UF, NX |
*if rm=111 |
FNMSUB.S |
rs1, rs2, rs3, frm* |
rd |
NV, OF, UF, NX |
*if rm=111 |
FNMADD.S |
rs1, rs2, rs3, frm* |
rd |
NV, OF, UF, NX |
*if rm=111 |
FADD.S |
rs1, rs2, frm* |
rd |
NV, OF, NX |
*if rm=111 |
FSUB.S |
rs1, rs2, frm* |
rd |
NV, OF, NX |
*if rm=111 |
FMUL.S |
rs1, rs2, frm* |
rd |
NV, OF, UF, NX |
*if rm=111 |
FDIV.S |
rs1, rs2, frm* |
rd |
NV, DZ, OF, UF, NX |
*if rm=111 |
FSQRT.S |
rs1, frm* |
rd |
NV, NX |
*if rm=111 |
FSGNJ.S |
rs1, rs2 |
rd |
||
FSGNJN.S |
rs1, rs2 |
rd |
||
FSGNJX.S |
rs1, rs2 |
rd |
||
FMIN.S |
rs1, rs2 |
rd |
NV |
|
FMAX.S |
rs1, rs2 |
rd |
NV |
|
FCVT.W.S |
rs1, frm* |
rd |
NV, NX |
*if rm=111 |
FCVT.WU.S |
rs1, frm* |
rd |
NV, NX |
*if rm=111 |
FMV.X.W |
rs1 |
rd |
||
FEQ.S |
rs1, rs2 |
rd |
NV |
|
FLT.S |
rs1, rs2 |
rd |
NV |
|
FLE.S |
rs1, rs2 |
rd |
NV |
|
FCLASS.S |
rs1 |
rd |
||
FCVT.S.W |
rs1, frm* |
rd |
NX |
*if rm=111 |
FCVT.S.WU |
rs1, frm* |
rd |
NX |
*if rm=111 |
FMV.W.X |
rs1 |
rd |
| Source Registers | Destination Registers | Accumulating CSRs | ||
|---|---|---|---|---|
FCVT.L.S |
rs1, frm* |
rd |
NV, NX |
*if rm=111 |
FCVT.LU.S |
rs1, frm* |
rd |
NV, NX |
*if rm=111 |
FCVT.S.L |
rs1, frm* |
rd |
NX |
*if rm=111 |
FCVT.S.LU |
rs1, frm* |
rd |
NX |
*if rm=111 |
| Source Registers | Destination Registers | Accumulating CSRs | ||
|---|---|---|---|---|
FLD† |
rs1 A |
rd |
||
FSD |
rs1 A, rs2D |
|||
FMADD.D |
rs1, rs2, rs3, frm* |
rd |
NV, OF, UF, NX |
*if rm=111 |
FMSUB.D |
rs1, rs2, rs3, frm* |
rd |
NV, OF, UF, NX |
*if rm=111 |
FNMSUB.D |
rs1, rs2, rs3, frm* |
rd |
NV, OF, UF, NX |
*if rm=111 |
FNMADD.D |
rs1, rs2, rs3, frm* |
rd |
NV, OF, UF, NX |
*if rm=111 |
FADD.D |
rs1, rs2, frm* |
rd |
NV, OF, NX |
*if rm=111 |
FSUB.D |
rs1, rs2, frm* |
rd |
NV, OF, NX |
*if rm=111 |
FMUL.D |
rs1, rs2, frm* |
rd |
NV, OF, UF, NX |
*if rm=111 |
FDIV.D |
rs1, rs2, frm* |
rd |
NV, DZ, OF, UF, NX |
*if rm=111 |
FSQRT.D |
rs1, frm* |
rd |
NV, NX |
*if rm=111 |
FSGNJ.D |
rs1, rs2 |
rd |
||
FSGNJN.D |
rs1, rs2 |
rd |
||
FSGNJX.D |
rs1, rs2 |
rd |
||
FMIN.D |
rs1, rs2 |
rd |
NV |
|
FMAX.D |
rs1, rs2 |
rd |
NV |
|
FCVT.S.D |
rs1, frm* |
rd |
NV, OF, UF, NX |
*if rm=111 |
FCVT.D.S |
rs1 |
rd |
NV |
|
FEQ.D |
rs1, rs2 |
rd |
NV |
|
FLT.D |
rs1, rs2 |
rd |
NV |
|
FLE.D |
rs1, rs2 |
rd |
NV |
|
FCLASS.D |
rs1 |
rd |
||
FCVT.W.D |
rs1,* |
rd |
NV, NX |
*if rm=111 |
FCVT.WU.D |
rs1, frm* |
rd |
NV, NX |
*if rm=111 |
FCVT.D.W |
rs1 |
rd |
||
FCVT.D.WU |
rs1 |
rd |
| Source Registers | Destination Registers | Accumulating CSRs | ||
|---|---|---|---|---|
FCVT.L.D |
rs1, frm* |
rd |
NV, NX |
*if rm=111 |
FCVT.LU.D |
rs1, frm* |
rd |
NV, NX |
*if rm=111 |
FMV.X.D |
rs1 |
rd |
||
FCVT.D.L |
rs1, frm* |
rd |
NX |
*if rm=111 |
FCVT.D.LU |
rs1, frm* |
rd |
NX |
*if rm=111 |
FMV.D.X |
rs1 |
rd |