RISC-V Instruction Set Manual, Volume I: RISC-V User-Level ISA

Metadata Table
Manual Type	user
Spec Revision
Spec Release Date
Git Revision	riscv-isa-release-1239329-2023-05-23-96-g1ee25e1
Git URL	https://github.com/riscv/riscv-isa-manual.git
Source	src/mm-formal.adoc
Conversion Date	2023/11/12
License	CC-by-4.0

Metadata Table

Manual Type

user

Spec Revision

Spec Release Date

Git Revision

riscv-isa-release-1239329-2023-05-23-96-g1ee25e1

Git URL

https://github.com/riscv/riscv-isa-manual.git

Source

src/mm-formal.adoc

Conversion Date

2023/11/12

License

CC-by-4.0

Appendix A: Formal Memory Model Specifications, Version 0.1

To facilitate formal analysis of RVWMO, this chapter presents a set of formalizations using different tools and modeling approaches. Any discrepancies are unintended; the expectation is that the models describe exactly the same sets of legal behaviors.

This appendix should be treated as commentary; all normative material is provided in Chapter 17 and in the rest of the main body of the ISA specification. All currently known discrepancies are listed in Section A.7. Any other discrepancies are unintentional.

A.1. Formal Axiomatic Specification in Alloy

We present a formal specification of the RVWMO memory model in Alloy (alloy.mit.edu). This model is available online at github.com/daniellustig/riscv-memory-model.

The online material also contains some litmus tests and some examples of how Alloy can be used to model check some of the mappings in [memory_porting].

Example 1. The RVWMO memory model formalized in Alloy (1/5: PPO)

// =RVWMO PPO=

// Preserved Program Order
fun ppo : Event->Event {
  // same-address ordering
  po_loc :> Store
  + rdw
  + (AMO + StoreConditional) <: rfi

  // explicit synchronization
  + ppo_fence
  + Acquire <: ^po :> MemoryEvent
  + MemoryEvent <: ^po :> Release
  + RCsc <: ^po :> RCsc
  + pair

  // syntactic dependencies
  + addrdep
  + datadep
  + ctrldep :> Store

  // pipeline dependencies
  + (addrdep+datadep).rfi
  + addrdep.^po :> Store
}

// the global memory order respects preserved program order
fact { ppo in ^gmo }

The RVWMO memory model formalized in Alloy (2/5: Axioms)

// =RVWMO axioms=

// Load Value Axiom
fun candidates[r: MemoryEvent] : set MemoryEvent {
  (r.~^gmo & Store & same_addr[r]) // writes preceding r in gmo
  + (r.^~po & Store & same_addr[r]) // writes preceding r in po
}

fun latest_among[s: set Event] : Event { s - s.~^gmo }

pred LoadValue {
  all w: Store | all r: Load |
    w->r in rf <=> w = latest_among[candidates[r]]
}

// Atomicity Axiom
pred Atomicity {
  all r: Store.~pair |            // starting from the lr,
    no x: Store & same_addr[r] |  // there is no store x to the same addr
      x not in same_hart[r]       // such that x is from a different hart,
      and x in r.~rf.^gmo         // x follows (the store r reads from) in gmo,
      and r.pair in x.^gmo        // and r follows x in gmo
}

// Progress Axiom implicit: Alloy only considers finite executions

pred RISCV_mm { LoadValue and Atomicity /* and Progress */ }

Example 2. The RVWMO memory model formalized in Alloy (3/5: model of memory)

//Basic model of memory

sig Hart {  // hardware thread
  start : one Event
}
sig Address {}
abstract sig Event {
  po: lone Event // program order
}

abstract sig MemoryEvent extends Event {
  address: one Address,
  acquireRCpc: lone MemoryEvent,
  acquireRCsc: lone MemoryEvent,
  releaseRCpc: lone MemoryEvent,
  releaseRCsc: lone MemoryEvent,
  addrdep: set MemoryEvent,
  ctrldep: set Event,
  datadep: set MemoryEvent,
  gmo: set MemoryEvent,  // global memory order
  rf: set MemoryEvent
}
sig LoadNormal extends MemoryEvent {} // l{b|h|w|d}
sig LoadReserve extends MemoryEvent { // lr
  pair: lone StoreConditional
}
sig StoreNormal extends MemoryEvent {}       // s{b|h|w|d}
// all StoreConditionals in the model are assumed to be successful
sig StoreConditional extends MemoryEvent {}  // sc
sig AMO extends MemoryEvent {}               // amo
sig NOP extends Event {}

fun Load : Event { LoadNormal + LoadReserve + AMO }
fun Store : Event { StoreNormal + StoreConditional + AMO }

sig Fence extends Event {
  pr: lone Fence, // opcode bit
  pw: lone Fence, // opcode bit
  sr: lone Fence, // opcode bit
  sw: lone Fence  // opcode bit
}
sig FenceTSO extends Fence {}

/* Alloy encoding detail: opcode bits are either set (encoded, e.g.,
 * as f.pr in iden) or unset (f.pr not in iden).  The bits cannot be used for
 * anything else */
fact { pr + pw + sr + sw in iden }
// likewise for ordering annotations
fact { acquireRCpc + acquireRCsc + releaseRCpc + releaseRCsc in iden }
// don't try to encode FenceTSO via pr/pw/sr/sw; just use it as-is
fact { no FenceTSO.(pr + pw + sr + sw) }

Example 3. The RVWMO memory model formalized in Alloy (4/5: Basic model rules)

// =Basic model rules=

// Ordering annotation groups
fun Acquire : MemoryEvent { MemoryEvent.acquireRCpc + MemoryEvent.acquireRCsc }
fun Release : MemoryEvent { MemoryEvent.releaseRCpc + MemoryEvent.releaseRCsc }
fun RCpc : MemoryEvent { MemoryEvent.acquireRCpc + MemoryEvent.releaseRCpc }
fun RCsc : MemoryEvent { MemoryEvent.acquireRCsc + MemoryEvent.releaseRCsc }

// There is no such thing as store-acquire or load-release, unless it's both
fact { Load & Release in Acquire }
fact { Store & Acquire in Release }

// FENCE PPO
fun FencePRSR : Fence { Fence.(pr & sr) }
fun FencePRSW : Fence { Fence.(pr & sw) }
fun FencePWSR : Fence { Fence.(pw & sr) }
fun FencePWSW : Fence { Fence.(pw & sw) }

fun ppo_fence : MemoryEvent->MemoryEvent {
    (Load  <: ^po :> FencePRSR).(^po :> Load)
  + (Load  <: ^po :> FencePRSW).(^po :> Store)
  + (Store <: ^po :> FencePWSR).(^po :> Load)
  + (Store <: ^po :> FencePWSW).(^po :> Store)
  + (Load  <: ^po :> FenceTSO) .(^po :> MemoryEvent)
  + (Store <: ^po :> FenceTSO) .(^po :> Store)
}

// auxiliary definitions
fun po_loc : Event->Event { ^po & address.~address }
fun same_hart[e: Event] : set Event { e + e.^~po + e.^po }
fun same_addr[e: Event] : set Event { e.address.~address }

// initial stores
fun NonInit : set Event { Hart.start.*po }
fun Init : set Event { Event - NonInit }
fact { Init in StoreNormal }
fact { Init->(MemoryEvent & NonInit) in ^gmo }
fact { all e: NonInit | one e.*~po.~start }  // each event is in exactly one hart
fact { all a: Address | one Init & a.~address } // one init store per address
fact { no Init <: po and no po :> Init }

Example 4. The RVWMO memory model formalized in Alloy (5/5: Auxiliaries)

// po
fact { acyclic[po] }

// gmo
fact { total[^gmo, MemoryEvent] } // gmo is a total order over all MemoryEvents

//rf
fact { rf.~rf in iden } // each read returns the value of only one write
fact { rf in Store <: address.~address :> Load }
fun rfi : MemoryEvent->MemoryEvent { rf & (*po + *~po) }

//dep
fact { no StoreNormal <: (addrdep + ctrldep + datadep) }
fact { addrdep + ctrldep + datadep + pair in ^po }
fact { datadep in datadep :> Store }
fact { ctrldep.*po in ctrldep }
fact { no pair & (^po :> (LoadReserve + StoreConditional)).^po }
fact { StoreConditional in LoadReserve.pair } // assume all SCs succeed

// rdw
fun rdw : Event->Event {
  (Load <: po_loc :> Load)  // start with all same_address load-load pairs,
  - (~rf.rf)                // subtract pairs that read from the same store,
  - (po_loc.rfi)            // and subtract out "fri-rfi" patterns
}

// filter out redundant instances and/or visualizations
fact { no gmo & gmo.gmo } // keep the visualization uncluttered
fact { all a: Address | some a.~address }

// =Optional: opcode encoding restrictions=

// the list of blessed fences
fact { Fence in
  Fence.pr.sr
  + Fence.pw.sw
  + Fence.pr.pw.sw
  + Fence.pr.sr.sw
  + FenceTSO
  + Fence.pr.pw.sr.sw
}

pred restrict_to_current_encodings {
  no (LoadNormal + StoreNormal) & (Acquire + Release)
}

// =Alloy shortcuts=
pred acyclic[rel: Event->Event] { no iden & ^rel }
pred total[rel: Event->Event, bag: Event] {
  all disj e, e': bag | e->e' in rel + ~rel
  acyclic[rel]
}

A.2. Formal Axiomatic Specification in Herd

The tool herd takes a memory model and a litmus test as input and simulates the execution of the test on top of the memory model. Memory models are written in the domain specific language Cat. This section provides two Cat memory model of RVWMO. The first model, Example 6, follows the global memory order, Chapter [memorymodel], definition of RVWMO, as much as is possible for a Cat model. The second model, Example 7, is an equivalent, more efficient, partial order based RVWMO model.

The simulator herd is part of the diy tool suite — see diy.inria.fr for software and documentation. The models and more are available online at diy.inria.fr/cats7/riscv/.

Example 5. riscv-defs.cat, a herd definition of preserved program order (1/3)

(*************)
(* Utilities *)
(*************)

(* All fence relations *)
let fence.r.r = [R];fencerel(Fence.r.r);[R]
let fence.r.w = [R];fencerel(Fence.r.w);[W]
let fence.r.rw = [R];fencerel(Fence.r.rw);[M]
let fence.w.r = [W];fencerel(Fence.w.r);[R]
let fence.w.w = [W];fencerel(Fence.w.w);[W]
let fence.w.rw = [W];fencerel(Fence.w.rw);[M]
let fence.rw.r = [M];fencerel(Fence.rw.r);[R]
let fence.rw.w = [M];fencerel(Fence.rw.w);[W]
let fence.rw.rw = [M];fencerel(Fence.rw.rw);[M]
let fence.tso =
  let f = fencerel(Fence.tso) in
  ([W];f;[W]) | ([R];f;[M])

let fence =
  fence.r.r | fence.r.w | fence.r.rw |
  fence.w.r | fence.w.w | fence.w.rw |
  fence.rw.r | fence.rw.w | fence.rw.rw |
  fence.tso

(* Same address, no W to the same address in-between *)
let po-loc-no-w = po-loc \ (po-loc?;[W];po-loc)
(* Read same write *)
let rsw = rf^-1;rf
(* Acquire, or stronger  *)
let AQ = Acq|AcqRel
(* Release or stronger *)
and RL = RelAcqRel
(* All RCsc *)
let RCsc = Acq|Rel|AcqRel
(* Amo events are both R and W, relation rmw relates paired lr/sc *)
let AMO = R & W
let StCond = range(rmw)

(*************)
(* ppo rules *)
(*************)

(* Overlapping-Address Orderings *)
let r1 = [M];po-loc;[W]
and r2 = ([R];po-loc-no-w;[R]) \ rsw
and r3 = [AMO|StCond];rfi;[R]
(* Explicit Synchronization *)
and r4 = fence
and r5 = [AQ];po;[M]
and r6 = [M];po;[RL]
and r7 = [RCsc];po;[RCsc]
and r8 = rmw
(* Syntactic Dependencies *)
and r9 = [M];addr;[M]
and r10 = [M];data;[W]
and r11 = [M];ctrl;[W]
(* Pipeline Dependencies *)
and r12 = [R];(addr|data);[W];rfi;[R]
and r13 = [R];addr;[M];po;[W]

let ppo = r1 | r2 | r3 | r4 | r5 | r6 | r7 | r8 | r9 | r10 | r11 | r12 | r13

Example 6. riscv.cat, a herd version of the RVWMO memory model (2/3)

Total

(* Notice that herd has defined its own rf relation *)

(* Define ppo *)
include "riscv-defs.cat"

(********************************)
(* Generate global memory order *)
(********************************)

let gmo0 = (* precursor: ie build gmo as an total order that include gmo0 *)
  loc & (W\FW) * FW | # Final write after any write to the same location
  ppo |               # ppo compatible
  rfe                 # includes herd external rf (optimization)

(* Walk over all linear extensions of gmo0 *)
with  gmo from linearizations(M\IW,gmo0)

(* Add initial writes upfront -- convenient for computing rfGMO *)
let gmo = gmo | loc & IW * (M\IW)

(**********)
(* Axioms *)
(**********)

(* Compute rf according to the load value axiom, aka rfGMO *)
let WR = loc & ([W];(gmo|po);[R])
let rfGMO = WR \ (loc&([W];gmo);WR)

(* Check equality of herd rf and of rfGMO *)
empty (rf\rfGMO)|(rfGMO\rf) as RfCons

(* Atomicity axiom *)
let infloc = (gmo & loc)^-1
let inflocext = infloc & ext
let winside  = (infloc;rmw;inflocext) & (infloc;rf;rmw;inflocext) & [W]
empty winside as Atomic

Example 7. riscv.cat, an alternative herd presentation of the RVWMO memory model (3/3)

Partial

(***************)
(* Definitions *)
(***************)

(* Define ppo *)
include "riscv-defs.cat"

(* Compute coherence relation *)
include "cos-opt.cat"

(**********)
(* Axioms *)
(**********)

(* Sc per location *)
acyclic co|rf|fr|po-loc as Coherence

(* Main model axiom *)
acyclic co|rfe|fr|ppo as Model

(* Atomicity axiom *)
empty rmw & (fre;coe) as Atomic

A.3. An Operational Memory Model

This is an alternative presentation of the RVWMO memory model in operational style. It aims to admit exactly the same extensional behavior as the axiomatic presentation: for any given program, admitting an execution if and only if the axiomatic presentation allows it.

The axiomatic presentation is defined as a predicate on complete candidate executions. In contrast, this operational presentation has an abstract microarchitectural flavor: it is expressed as a state machine, with states that are an abstract representation of hardware machine states, and with explicit out-of-order and speculative execution (but abstracting from more implementation-specific microarchitectural details such as register renaming, store buffers, cache hierarchies, cache protocols, etc.). As such, it can provide useful intuition. It can also construct executions incrementally, making it possible to interactively and randomly explore the behavior of larger examples, while the axiomatic model requires complete candidate executions over which the axioms can be checked.

The operational presentation covers mixed-size execution, with potentially overlapping memory accesses of different power-of-two byte sizes. Misaligned accesses are broken up into single-byte accesses.

The operational model, together with a fragment of the RISC-V ISA semantics (RV64I and A), are integrated into the rmem exploration tool (github.com/rems-project/rmem). rmem can explore litmus tests (see [litmustests]) and small ELF binaries exhaustively, pseudo-randomly and interactively. In rmem, the ISA semantics is expressed explicitly in Sail (see github.com/rems-project/sail for the Sail language, and github.com/rems-project/sail-riscv for the RISC-V ISA model), and the concurrency semantics is expressed in Lem (see github.com/rems-project/lem for the Lem language).

rmem has a command-line interface and a web-interface. The web-interface runs entirely on the client side, and is provided online together with a library of litmus tests: www.cl.cam.ac.uk/. The command-line interface is faster than the web-interface, specially in exhaustive mode.

Below is an informal introduction of the model states and transitions. The description of the formal model starts in the next subsection.

Terminology: In contrast to the axiomatic presentation, here every memory operation is either a load or a store. Hence, AMOs give rise to two distinct memory operations, a load and a store. When used in conjunction with instruction, the terms load and store refer to instructions that give rise to such memory operations. As such, both include AMO instructions. The term acquire refers to an instruction (or its memory operation) with the acquire-RCpc or acquire-RCsc annotation. The term release refers to an instruction (or its memory operation) with the release-RCpc or release-RCsc annotation.

Model states

Model states: A model state consists of a shared memory and a tuple of hart states.

The shared memory state records all the memory store operations that have propagated so far, in the order they propagated (this can be made more efficient, but for simplicity of the presentation we keep it this way).

Each hart state consists principally of a tree of instruction instances, some of which have been finished, and some of which have not. Non-finished instruction instances can be subject to restart, e.g. if they depend on an out-of-order or speculative load that turns out to be unsound.

Conditional branch and indirect jump instructions may have multiple successors in the instruction tree. When such instruction is finished, any un-taken alternative paths are discarded.

Each instruction instance in the instruction tree has a state that includes an execution state of the intra-instruction semantics (the ISA pseudocode for this instruction). The model uses a formalization of the intra-instruction semantics in Sail. One can think of the execution state of an instruction as a representation of the pseudocode control state, pseudocode call stack, and local variable values. An instruction instance state also includes information about the instance’s memory and register footprints, its register reads and writes, its memory operations, whether it is finished, etc.

Model transitions

The model defines, for any model state, the set of allowed transitions, each of which is a single atomic step to a new abstract machine state. Execution of a single instruction will typically involve many transitions, and they may be interleaved in operational-model execution with transitions arising from other instructions. Each transition arises from a single instruction instance; it will change the state of that instance, and it may depend on or change the rest of its hart state and the shared memory state, but it does not depend on other hart states, and it will not change them. The transitions are introduced below and defined in Section A.3.5, with a precondition and a construction of the post-transition model state for each.

Transitions for all instructions:

\(\bullet\) Fetch instruction: This transition represents a fetch and decode of a new instruction instance, as a program order successor of a previously fetched instruction instance (or the initial fetch address).

The model assumes the instruction memory is fixed; it does not describe the behavior of self-modifying code. In particular, the Fetch instruction transition does not generate memory load operations, and the shared memory is not involved in the transition. Instead, the model depends on an external oracle that provides an opcode when given a memory location.

\(\circ\) Register write: This is a write of a register value.

\(\circ\) Register read: This is a read of a register value from the most recent program-order-predecessor instruction instance that writes to that register.

\(\circ\) Pseudocode internal step: This covers pseudocode internal computation: arithmetic, function calls, etc.

\(\circ\) Finish instruction: At this point the instruction pseudocode is done, the instruction cannot be restarted, memory accesses cannot be discarded, and all memory effects have taken place. For conditional branch and indirect jump instructions, any program order successors that were fetched from an address that is not the one that was written to the pc register are discarded, together with the sub-tree of instruction instances below them.

Transitions specific to load instructions:

\(\circ\) Initiate memory load operations: At this point the memory footprint of the load instruction is provisionally known (it could change if earlier instructions are restarted) and its individual memory load operations can start being satisfied. \(\bullet\) Satisfy memory load operation by forwarding from unpropogated stores: This partially or entirely satisfies a single memory load operation by forwarding, from program-order-previous memory store operations. \(\bullet\) Satisfy memory load operation from memory: This entirely satisfies the outstanding slices of a single memory load operation, from memory. \(\circ\) Complete load operations: At this point all the memory load operations of the instruction have been entirely satisfied and the instruction pseudocode can continue executing. A load instruction can be subject to being restarted until the transition. But, under some conditions, the model might treat a load instruction as non-restartable even before it is finished (e.g. see ).

Transitions specific to store instructions:

\(\circ\) Initiate memory store operation footprints: At this point the memory footprint of the store is provisionally known. \(\circ\) Instantiate memory store operation values: At this point the memory store operations have their values and program-order-successor memory load operations can be satisfied by forwarding from them. \(\circ\) Commit store instruction: At this point the store operations are guaranteed to happen (the instruction can no longer be restarted or discarded), and they can start being propagated to memory. \(\bullet\) Propagate store operation: This propagates a single memory store operation to memory. \(\circ\) Complete store operations: At this point all the memory store operations of the instruction have been propagated to memory, and the instruction pseudocode can continue executing.

Transitions specific to sc instructions:

\(\bullet\) Early sc fail: This causes the sc to fail, either a spontaneous fail or because it is not paired with a program-order-previous lr. \(\bullet\) Paired sc: This transition indicates the sc is paired with an lr and might succeed. \(\bullet\) Commit and propagate store operation of an sc: This is an atomic execution of the transitions Commit store instruction and Propagate store operation, it is enabled only if the stores from which the lr read from have not been overwritten. \(\bullet\) Late sc fail: This causes the sc to fail, either a spontaneous fail or because the stores from which the lr read from have been overwritten.

Transitions specific to AMO instructions:

\(\bullet\) Satisfy, commit and propagate operations of an AMO: This is an atomic execution of all the transitions needed to satisfy the load operation, do the required arithmetic, and propagate the store operation.

Transitions specific to fence instructions:

\(\circ\) Commit fence

The transitions labeled \(\circ\) can always be taken eagerly, as soon as their precondition is satisfied, without excluding other behavior; the \(\bullet\) cannot. Although is marked with a \(\bullet\), it can be taken eagerly as long as it is not taken infinitely many times.

An instance of a non-AMO load instruction, after being fetched, will typically experience the following transitions in this order:

Register read
Initiate memory load operations
Satisfy memory load operation by forwarding from unpropagated stores and/or Satisfy memory load operation from memory (as many as needed to satisfy all the load operations of the instance)
Complete load operations
Register write
Finish instruction

Before, between and after the transitions above, any number of Pseudocode internal step transitions may appear. In addition, a Fetch instruction transition for fetching the instruction in the next program location will be available until it is taken.

This concludes the informal description of the operational model. The following sections describe the formal operational model.

A.3.1. Intra-instruction Pseudocode Execution

The intra-instruction semantics for each instruction instance is expressed as a state machine, essentially running the instruction pseudocode. Given a pseudocode execution state, it computes the next state. Most states identify a pending memory or register operation, requested by the pseudocode, which the memory model has to do. The states are (this is a tagged union; tags in small-caps):

Load_mem(kind, address, size, load_continuation)

- memory load operation

Early_sc_fail(res_continuation)

- allow sc to fail early

Store_ea(kind, address, size, next_state)

- memory store effective address

Store_memv(mem_value, store_continuation)

- memory store value

Fence(kind, next_state)

- fence

Read_reg(reg_name, read_continuation)

- register read

Write_reg(reg_name, reg_value, next_state)

- register write

Internal(next_state)

- pseudocode internal step

Done

- end of pseudocode

Here:

mem_value and reg_value are lists of bytes;
address is an integer of XLEN bits;

for load/store, kind identifies whether it is lr/sc, acquire-RCpc/release-RCpc, acquire-RCsc/release-RCsc, acquire-release-RCsc; * for fence, kind identifies whether it is a normal or TSO, and (for normal fences) the predecessor and successor ordering bits; * reg_name identifies a register and a slice thereof (start and end bit indices); and the continuations describe how the instruction instance will continue for each value that might be provided by the surrounding memory model (the load_continuation and read_continuation take the value loaded from memory and read from the previous register write, the store_continuation takes false for an sc that failed and true in all other cases, and res_continuation takes false if the sc fails and true otherwise).

For example, given the load instruction lw x1,0(x2), an execution will typically go as follows. The initial execution state will be computed from the pseudocode for the given opcode. This can be expected to be Read_reg(x2, read_continuation). Feeding the most recently written value of register x2 (the instruction semantics will be blocked if necessary until the register value is available), say 0x4000, to read_continuation returns Load_mem(plain_load, 0x4000, 4, load_continuation). Feeding the 4-byte value loaded from memory location 0x4000, say 0x42, to load_continuation returns Write_reg(x1, 0x42, Done). Many Internal(next_state) states may appear before and between the states above.

Notice that writing to memory is split into two steps, Store_ea and Store_memv: the first one makes the memory footprint of the store provisionally known, and the second one adds the value to be stored. We ensure these are paired in the pseudocode (Store_ea followed by Store_memv), but there may be other steps between them.

It is observable that the Store_ea can occur before the value to be stored is determined. For example, for the litmus test LB+fence.r.rw+data-po to be allowed by the operational model (as it is by RVWMO), the first store in Hart 1 has to take the Store_ea step before its value is determined, so that the second store can see it is to a non-overlapping memory footprint, allowing the second store to be committed out of order without violating coherence.

The pseudocode of each instruction performs at most one store or one load, except for AMOs that perform exactly one load and one store. Those memory accesses are then split apart into the architecturally atomic units by the hart semantics (see Initiate memory load operations and Initiate memory store operation footprints below).

Informally, each bit of a register read should be satisfied from a register write by the most recent (in program order) instruction instance that can write that bit (or from the hart’s initial register state if there is no such write). Hence, it is essential to know the register write footprint of each instruction instance, which we calculate when the instruction instance is created (see the Festch instruction action of below). We ensure in the pseudocode that each instruction does at most one register write to each register bit, and also that it does not try to read a register value it just wrote.

Data-flow dependencies (address and data) in the model emerge from the fact that each register read has to wait for the appropriate register write to be executed (as described above).

A.3.2. Instruction Instance State

Each instruction instance _i has a state comprising:

program_loc, the memory address from which the instruction was fetched;
instruction_kind, identifying whether this is a load, store, AMO, fence, branch/jump or a simple instruction (this also includes a kind similar to the one described for the pseudocode execution states);
src_regs, the set of source _reg_name_s (including system registers), as statically determined from the pseudocode of the instruction;
dst_regs, the destination _reg_name_s (including system registers), as statically determined from the pseudocode of the instruction;
pseudocode_state (or sometimes just state for short), one of (this is a tagged union; tags in small-caps):

Plain(isa_state)	- ready to make a pseudocode transition
Pending_mem_loads(load_continuation)	- requesting memory load operation(s)
Pending_mem_stores(store_continuation)	- requesting memory store operation(s)

Plain(isa_state)

- ready to make a pseudocode transition

Pending_mem_loads(load_continuation)

- requesting memory load operation(s)

Pending_mem_stores(store_continuation)

- requesting memory store operation(s)

reg_reads, the register reads the instance has performed, including, for each one, the register write slices it read from;
reg_writes, the register writes the instance has performed;
mem_loads, a set of memory load operations, and for each one the as-yet-unsatisfied slices (the byte indices that have not been satisfied yet), and, for the satisfied slices, the store slices (each consisting of a memory store operation and subset of its byte indices) that satisfied it.
mem_stores, a set of memory store operations, and for each one a flag that indicates whether it has been propagated (passed to the shared memory) or not.
information recording whether the instance is committed, finished, etc.

Each memory load operation includes a memory footprint (address and size). Each memory store operations includes a memory footprint, and, when available, a value.

A load instruction instance with a non-empty mem_loads, for which all the load operations are satisfied (i.e. there are no unsatisfied load slices) is said to be entirely satisfied.

Informally, an instruction instance is said to have fully determined data if the load (and sc) instructions feeding its source registers are finished. Similarly, it is said to have a fully determined memory footprint if the load (and sc) instructions feeding its memory operation address register are finished. Formally, we first define the notion of fully determined register write: a register write \(w\) from reg_writes of instruction instance \(i\) is said to be fully determined if one of the following conditions hold:

\(i\) is finished; or
the value written by \(w\) is not affected by a memory operation that \(i\) has made (i.e. a value loaded from memory or the result of sc), and, for every register read that \(i\) has made, that affects \(w\), the register write from which \(i\) read is fully determined (or \(i\) read from the initial register state).

Now, an instruction instance \(i\) is said to have fully determined data if for every register read \(r\) from reg_reads, the register writes that \(r\) reads from are fully determined. An instruction instance \(i\) is said to have a fully determined memory footprint if for every register read \(r\) from reg_reads that feeds into \(i\)’s memory operation address, the register writes that \(r\) reads from are fully determined.

The rmem tool records, for every register write, the set of register writes from other instructions that have been read by this instruction at the point of performing the write. By carefully arranging the pseudocode of the instructions covered by the tool we were able to make it so that this is exactly the set of register writes on which the write depends on.

A.3.3. Hart State

The model state of a single hart comprises:

hart_id, a unique identifier of the hart;
initial_register_state, the initial register value for each register;
initial_fetch_address, the initial instruction fetch address;
instruction_tree, a tree of the instruction instances that have been fetched (and not discarded), in program order.

A.3.4. Shared Memory State

The model state of the shared memory comprises a list of memory store operations, in the order they propagated to the shared memory.

When a store operation is propagated to the shared memory it is simply added to the end of the list. When a load operation is satisfied from memory, for each byte of the load operation, the most recent corresponding store slice is returned.

For most purposes, it is simpler to think of the shared memory as an array, i.e., a map from memory locations to memory store operation slices, where each memory location is mapped to a one-byte slice of the most recent memory store operation to that location. However, this abstraction is not detailed enough to properly handle the sc instruction. The RVWMO allows store operations from the same hart as the sc to intervene between the store operation of the sc and the store operations the paired lr read from. To allow such store operations to intervene, and forbid others, the array abstraction must be extended to record more information. Here, we use a list as it is very simple, but a more efficient and scalable implementations should probably use something better.

A.3.5. Transitions

Each of the paragraphs below describes a single kind of system transition. The description starts with a condition over the current system state. The transition can be taken in the current state only if the condition is satisfied. The condition is followed by an action that is applied to that state when the transition is taken, in order to generate the new system state.

Fetch instruction

A possible program-order-successor of instruction instance \(i\) can be fetched from address loc if:

it has not already been fetched, i.e., none of the immediate successors of \(i\) in the hart’s instruction_tree are from loc; and
if \(i\)’s pseudocode has already written an address to pc, then loc must be that address, otherwise loc is:
- for a conditional branch, the successor address or the branch target address;
- for a (direct) jump and link instruction (jal), the target address;
- for an indirect jump instruction (jalr), any address; and
- for any other instruction, \(i.\textit{program\_loc}+4\).

Action: construct a freshly initialized instruction instance \(i'\) for the instruction in the program memory at loc, with state Plain(isa_state), computed from the instruction pseudocode, including the static information available from the pseudocode such as its instruction_kind, src_regs, and dst_regs, and add \(i'\) to the hart’s instruction_tree as a successor of \(i\).

The possible next fetch addresses (loc) are available immediately after fetching \(i\) and the model does not need to wait for the pseudocode to write to pc; this allows out-of-order execution, and speculation past conditional branches and jumps. For most instructions these addresses are easily obtained from the instruction pseudocode. The only exception to that is the indirect jump instruction (jalr), where the address depends on the value held in a register. In principle the mathematical model should allow speculation to arbitrary addresses here. The exhaustive search in the rmem tool handles this by running the exhaustive search multiple times with a growing set of possible next fetch addresses for each indirect jump. The initial search uses empty sets, hence there is no fetch after indirect jump instruction until the pseudocode of the instruction writes to pc, and then we use that value for fetching the next instruction. Before starting the next iteration of exhaustive search, we collect for each indirect jump (grouped by code location) the set of values it wrote to pc in all the executions in the previous search iteration, and use that as possible next fetch addresses of the instruction. This process terminates when no new fetch addresses are detected.

Initiate memory load operations

An instruction instance \(i\) in state Plain(Load_mem(kind, address, size, load_continuation)) can always initiate the corresponding memory load operations. Action:

Construct the appropriate memory load operations \(mlos\):
- if address is aligned to size then \(mlos\) is a single memory load operation of size bytes from address;
- otherwise, \(mlos\) is a set of size memory load operations, each of one byte, from the addresses \(\textit{address}\ldots\textit{address}+\textit{size}-1\).
set mem_loads of \(i\) to \(mlos\); and
update the state of \(i\) to Pending_mem_loads(load_continuation).

In [rvwmo-primitives] it is said that misaligned memory accesses may be decomposed at any granularity. Here we decompose them to one-byte accesses as this granularity subsumes all others.

Satisfy memory load operation by forwarding from unpropagated stores

For a non-AMO load instruction instance \(i\) in state Pending_mem_loads(load_continuation), and a memory load operation \(mlo\) in \(i.\textit{mem\_loads}\) that has unsatisfied slices, the memory load operation can be partially or entirely satisfied by forwarding from unpropagated memory store operations by store instruction instances that are program-order-before \(i\) if:

all program-order-previous fence instructions with .sr and .pw set are finished;
for every program-order-previous fence instruction, \(f\), with .sr and .pr set, and .pw not set, if \(f\) is not finished then all load instructions that are program-order-before \(f\) are entirely satisfied;
for every program-order-previous fence.tso instruction, \(f\), that is not finished, all load instructions that are program-order-before \(f\) are entirely satisfied;
if \(i\) is a load-acquire-RCsc, all program-order-previous store-releases-RCsc are finished;
if \(i\) is a load-acquire-release, all program-order-previous instructions are finished;
all non-finished program-order-previous load-acquire instructions are entirely satisfied; and
all program-order-previous store-acquire-release instructions are finished;

Let \(msoss\) be the set of all unpropagated memory store operation slices from non-sc store instruction instances that are program-order-before \(i\) and have already calculated the value to be stored, that overlap with the unsatisfied slices of \(mlo\), and which are not superseded by intervening store operations or store operations that are read from by an intervening load. The last condition requires, for each memory store operation slice \(msos\) in \(msoss\) from instruction \(i'\):

that there is no store instruction program-order-between \(i\) and \(i'\) with a memory store operation overlapping \(msos\); and
that there is no load instruction program-order-between \(i\) and \(i'\) that was satisfied from an overlapping memory store operation slice from a different hart.

Action:

update \(i.\textit{mem\_loads}\) to indicate that \(mlo\) was satisfied by \(msoss\); and
restart any speculative instructions which have violated coherence as a result of this, i.e., for every non-finished instruction \(i'\) that is a program-order-successor of \(i\), and every memory load operation \(mlo'\) of \(i'\) that was satisfied from \(msoss'\), if there exists a memory store operation slice \(msos'\) in \(msoss'\), and an overlapping memory store operation slice from a different memory store operation in \(msoss\), and \(msos'\) is not from an instruction that is a program-order-successor of \(i\), restart \(i'\) and its restart-dependents.

Where, the restart-dependents of instruction \(j\) are:

program-order-successors of \(j\) that have data-flow dependency on a register write of \(j\);
program-order-successors of \(j\) that have a memory load operation that reads from a memory store operation of \(j\) (by forwarding);
if \(j\) is a load-acquire, all the program-order-successors of \(j\);
if \(j\) is a load, for every fence, \(f\), with .sr and .pr set, and .pw not set, that is a program-order-successor of \(j\), all the load instructions that are program-order-successors of \(f\);
if \(j\) is a load, for every fence.tso, \(f\), that is a program-order-successor of \(j\), all the load instructions that are program-order-successors of \(f\); and
(recursively) all the restart-dependents of all the instruction instances above.

Forwarding memory store operations to a memory load might satisfy only some slices of the load, leaving other slices unsatisfied.

A program-order-previous store operation that was not available when taking the transition above might make \(msoss\) provisionally unsound (violating coherence) when it becomes available. That store will prevent the load from being finished (see Finish instruction), and will cause it to restart when that store operation is propagated (see Propagate store operation).

A consequence of the transition condition above is that store-release-RCsc memory store operations cannot be forwarded to load-acquire-RCsc instructions: \(msoss\) does not include memory store operations from finished stores (as those must be propagated memory store operations), and the condition above requires all program-order-previous store-releases-RCsc to be finished when the load is acquire-RCsc.

Satisfy memory load operation from memory

For an instruction instance \(i\) of a non-AMO load instruction or an AMO instruction in the context of the Saitsfy, commit and propagate operations of an AMO transition, any memory load operation \(mlo\) in \(i.\textit{mem\_loads}\) that has unsatisfied slices, can be satisfied from memory if all the conditions of <sat_by_forwarding, Saitsfy memory load operation by forwarding from unpropagated stores>> are satisfied. Action: let \(msoss\) be the memory store operation slices from memory covering the unsatisfied slices of \(mlo\), and apply the action of Satisfy memory operation by forwarding from unpropagates stores.

Note that Satisfy memory operation by forwarding from unpropagates stores might leave some slices of the memory load operation unsatisfied, those will have to be satisfied by taking the transition again, or taking Satisfy memory load operation from memory. Satisfy memory load operation from memory, on the other hand, will always satisfy all the unsatisfied slices of the memory load operation.

Complete load operations

A load instruction instance \(i\) in state Pending_mem_loads(load_continuation) can be completed (not to be confused with finished) if all the memory load operations \(i.\textit{mem\_loads}\) are entirely satisfied (i.e. there are no unsatisfied slices). Action: update the state of \(i\) to Plain(load_continuation(mem_value)), where mem_value is assembled from all the memory store operation slices that satisfied \(i.\textit{mem\_loads}\).

Early `sc` fail

An sc instruction instance \(i\) in state Plain(Early_sc_fail(res_continuation)) can always be made to fail. Action: update the state of \(i\) to Plain(res_continuation(false)).

Paired `sc`

An sc instruction instance \(i\) in state Plain(Early_sc_fail(res_continuation)) can continue its (potentially successful) execution if \(i\) is paired with an lr. Action: update the state of \(i\) to Plain(res_continuation(true)).

Initiate memory store operation footprints

An instruction instance \(i\) in state Plain(Store_ea(kind, address, size, next_state)) can always announce its pending memory store operation footprint. Action:

construct the appropriate memory store operations \(msos\) (without the store value):
- if address is aligned to size then \(msos\) is a single memory store operation of size bytes to address;
- otherwise, \(msos\) is a set of size memory store operations, each of one-byte size, to the addresses \(\textit{address}\ldots\textit{address}+\textit{size}-1\).
set \(i.\textit{mem\_stores}\) to \(msos\); and
update the state of \(i\) to Plain(next_state).

Note that after taking the transition above the memory store operations do not yet have their values. The importance of splitting this transition from the transition below is that it allows other program-order-successor store instructions to observe the memory footprint of this instruction, and if they don’t overlap, propagate out of order as early as possible (i.e. before the data register value becomes available).

Instantiate memory store operation values

An instruction instance \(i\) in state Plain(Store_memv(mem_value, store_continuation)) can always instantiate the values of the memory store operations \(i.\textit{mem\_stores}\). Action:

split mem_value between the memory store operations \(i.\textit{mem\_stores}\); and
update the state of \(i\) to Pending_mem_stores(store_continuation).

Commit store instruction

An uncommitted instruction instance \(i\) of a non-sc store instruction or an sc instruction in the context of the Commit and propagate store operation of an sc transition, in state Pending_mem_stores(store_continuation), can be committed (not to be confused with propagated) if:

\(i\) has fully determined data;
all program-order-previous conditional branch and indirect jump instructions are finished;
all program-order-previous fence instructions with .sw set are finished;
all program-order-previous fence.tso instructions are finished;
all program-order-previous load-acquire instructions are finished;
all program-order-previous store-acquire-release instructions are finished;
if \(i\) is a store-release, all program-order-previous instructions are finished;
all program-order-previous memory access instructions have a fully determined memory footprint;
all program-order-previous store instructions, except for sc that failed, have initiated and so have non-empty mem_stores; and
all program-order-previous load instructions have initiated and so have non-empty mem_loads.

Action: record that i is committed.

Notice that if condition 8 is satisfied the conditions 9 and 10 are also satisfied, or will be satisfied after taking some eager transitions. Hence, requiring them does not strengthen the model. By requiring them, we guarantee that previous memory access instructions have taken enough transitions to make their memory operations visible for the condition check of , which is the next transition the instruction will take, making that condition simpler.

Propagate store operation

For a committed instruction instance \(i\) in state Pending_mem_stores(store_continuation), and an unpropagated memory store operation \(mso\) in \(i.\textit{mem\_stores}\), \(mso\) can be propagated if:

all memory store operations of program-order-previous store instructions that overlap with \(mso\) have already propagated;
all memory load operations of program-order-previous load instructions that overlap with \(mso\) have already been satisfied, and (the load instructions) are non-restartable (see definition below); and
all memory load operations that were satisfied by forwarding \(mso\) are entirely satisfied.

Where a non-finished instruction instance \(j\) is non-restartable if:

there does not exist a store instruction \(s\) and an unpropagated memory store operation \(mso\) of \(s\) such that applying the action of the Propagate store operation transition to \(mso\) will result in the restart of \(j\); and
there does not exist a non-finished load instruction \(l\) and a memory load operation \(mlo\) of \(l\) such that applying the action of the Satisfy memory load operation by forwarding from unpropagated stores/Satisfy memory load operation from memory transition (even if \(mlo\) is already satisfied) to \(mlo\) will result in the restart of \(j\).

Action:

update the shared memory state with \(mso\);
update \(i.\textit{mem\_stores}\) to indicate that \(mso\) was propagated; and
restart any speculative instructions which have violated coherence as a result of this, i.e., for every non-finished instruction \(i'\) program-order-after \(i\) and every memory load operation \(mlo'\) of \(i'\) that was satisfied from \(msoss'\), if there exists a memory store operation slice \(msos'\) in \(msoss'\) that overlaps with \(mso\) and is not from \(mso\), and \(msos'\) is not from a program-order-successor of \(i\), restart \(i'\) and its restart-dependents (see Satisfy memory load operation by forwarding from unpropagated stores).

Commit and propagate store operation of an `sc`

An uncommitted sc instruction instance \(i\), from hart \(h\), in state Pending_mem_stores(store_continuation), with a paired lr \(i'\) that has been satisfied by some store slices \(msoss\), can be committed and propagated at the same time if:

\(i'\) is finished;
every memory store operation that has been forwarded to \(i'\) is propagated;
the conditions of Commit store instruction is satisfied;
the conditions of Commit store instruction is satisfied (notice that an sc instruction can only have one memory store operation); and
for every store slice \(msos\) from \(msoss\), \(msos\) has not been overwritten, in the shared memory, by a store that is from a hart that is not \(h\), at any point since \(msos\) was propagated to memory.

Action:

apply the actions of Commit store instruction; and
apply the action of Commit store instruction.

Late `sc` fail

An sc instruction instance \(i\) in state Pending_mem_stores(store_continuation), that has not propagated its memory store operation, can always be made to fail. Action:

clear \(i.\textit{mem\_stores}\); and
update the state of \(i\) to Plain(store_continuation(false)).

For efficiency, the rmem tool allows this transition only when it is not possible to take the Commit and propagate store operation of an sc transition. This does not affect the set of allowed final states, but when explored interactively, if the sc should fail one should use the Eaarly sc fail transition instead of waiting for this transition.

Complete store operations

A store instruction instance \(i\) in state Pending_mem_stores(store_continuation), for which all the memory store operations in \(i.\textit{mem\_stores}\) have been propagated, can always be completed (not to be confused with finished). Action: update the state of \(i\) to Plain(store_continuation(true)).

Satisfy, commit and propagate operations of an AMO

An AMO instruction instance \(i\) in state Pending_mem_loads(load_continuation) can perform its memory access if it is possible to perform the following sequence of transitions with no intervening transitions:

Satisfy memory load operation from memory
Complere load operations
Pseudocode internal step (zero or more times)
Instantiate memory store operation values
Commit store instruction
Propagate store operation
Complete store operations

and in addition, the condition of Finish instruction, with the exception of not requiring \(i\) to be in state Plain(Done), holds after those transitions. Action: perform the above sequence of transitions (this does not include Finish instruction), one after the other, with no intervening transitions.

Notice that program-order-previous stores cannot be forwarded to the load of an AMO. This is simply because the sequence of transitions above does not include the forwarding transition. But even if it did include it, the sequence will fail when trying to do the Propagate store operation transition, as this transition requires all program-order-previous store operations to overlapping memory footprints to be propagated, and forwarding requires the store operation to be unpropagated.

In addition, the store of an AMO cannot be forwarded to a program-order-successor load. Before taking the transition above, the store operation of the AMO does not have its value and therefore cannot be forwarded; after taking the transition above the store operation is propagated and therefore cannot be forwarded.

Commit fence

A fence instruction instance \(i\) in state Plain(Fence(kind, next_state)) can be committed if:

if \(i\) is a normal fence and it has .pr set, all program-order-previous load instructions are finished;
if \(i\) is a normal fence and it has .pw set, all program-order-previous store instructions are finished; and
if \(i\) is a fence.tso, all program-order-previous load and store instructions are finished.

Action:

record that \(i\) is committed; and
update the state of \(i\) to Plain(next_state).

Register read

An instruction instance \(i\) in state Plain(Read_reg(reg_name, read_cont)) can do a register read of reg_name if every instruction instance that it needs to read from has already performed the expected reg_name register write.

Let read_sources include, for each bit of reg_name, the write to that bit by the most recent (in program order) instruction instance that can write to that bit, if any. If there is no such instruction, the source is the initial register value from initial_register_state. Let reg_value be the value assembled from read_sources. Action:

add reg_name to \(i.\textit{reg\_reads}\) with read_sources and reg_value; and
update the state of \(i\) to Plain(read_cont(reg_value)).

Register write

An instruction instance \(i\) in state Plain(Write_reg(reg_name, reg_value, next_state)) can always do a reg_name register write. Action:

add reg_name to \(i.\textit{reg\_writes}\) with \(deps\) and reg_value; and
update the state of \(i\) to Plain(next_state).

where \(deps\) is a pair of the set of all read_sources from \(i.\textit{reg\_reads}\), and a flag that is true iff \(i\) is a load instruction instance that has already been entirely satisfied.

Pseudocode internal step

An instruction instance \(i\) in state Plain(Internal(next_state)) can always do that pseudocode-internal step. Action: update the state of \(i\) to Plain(next_state).

Finish instruction

A non-finished instruction instance \(i\) in state Plain(Done) can be finished if:

if \(i\) is a load instruction:
1. all program-order-previous load-acquire instructions are finished;
2. all program-order-previous fence instructions with .sr set are finished;
3. for every program-order-previous fence.tso instruction, \(f\), that is not finished, all load instructions that are program-order-before \(f\) are finished; and
4. it is guaranteed that the values read by the memory load operations of \(i\) will not cause coherence violations, i.e., for any program-order-previous instruction instance \(i'\), let \(\textit{cfp}\) be the combined footprint of propagated memory store operations from store instructions program-order-between \(i\) and \(i'\), and fixed memory store operations that were forwarded to \(i\) from store instructions program-order-between \(i\) and \(i'\) including \(i'\), and let \(\overline{\textit{cfp}}\) be the complement of \(\textit{cfp}\) in the memory footprint of \(i\). If \(\overline{\textit{cfp}}\) is not empty:
  1. \(i'\) has a fully determined memory footprint;
  2. \(i'\) has no unpropagated memory store operations that overlap with \(\overline{\textit{cfp}}\); and
  3. if \(i'\) is a load with a memory footprint that overlaps with \(\overline{\textit{cfp}}\), then all the memory load operations of \(i'\) that overlap with \(\overline{\textit{cfp}}\) are satisfied and \(i'\) is non-restartable (see the Propagate store operation transition for how to determined if an instruction is non-restartable).
    
    Here, a memory store operation is called fixed if the store instruction has fully determined data.
\(i\) has a fully determined data; and
if \(i\) is not a fence, all program-order-previous conditional branch and indirect jump instructions are finished.

Action:

if \(i\) is a conditional branch or indirect jump instruction, discard any untaken paths of execution, i.e., remove all instruction instances that are not reachable by the branch/jump taken in instruction_tree; and
record the instruction as finished, i.e., set finished to true.

A.3.6. Limitations

The model covers user-level RV64I and RV64A. In particular, it does not support the misaligned atomics extension "Zam" or the total store ordering extension "Ztso". It should be trivial to adapt the model to RV32I/A and to the G, Q and C extensions, but we have never tried it. This will involve, mostly, writing Sail code for the instructions, with minimal, if any, changes to the concurrency model.
The model covers only normal memory accesses (it does not handle I/O accesses).
The model does not cover TLB-related effects.
The model assumes the instruction memory is fixed. In particular, the Fetch instruction transition does not generate memory load operations, and the shared memory is not involved in the transition. Instead, the model depends on an external oracle that provides an opcode when given a memory location.
The model does not cover exceptions, traps and interrupts.