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 (https://github.com/rems-project/rmem). rmem can
explore litmus tests (see [sec:litmustests]) and small ELF
binaries exhaustively,
pseudo-randomly and interactively. In rmem, the ISA semantics
is expressed explicitly in Sail (see
https://github.com/rems-project/sail for the Sail language, and
https://github.com/rems-project/sail-riscv for the RISC-V ISA
model), and the concurrency semantics is expressed in Lem (see
https://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:
http://www.cl.cam.ac.uk/~pes20/rmem. 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
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 1.5, with a precondition and a construction of the post-transition model state for each.
Transitions for all instructions:
: 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 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.
: This is a write of a register value.
: This is a read of a register value from the most recent program-order-predecessor instruction instance that writes to that register.
: This covers pseudocode internal computation: arithmetic, function calls, etc.
: 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:
: 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.
: This partially or entirely satisfies a single memory load operation by forwarding, from program-order-previous memory store operations.
: This entirely satisfies the outstanding slices of a single memory load operation, from memory.
: 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:
: At this point the memory footprint of the store is provisionally known.
: At this point the memory store operations have their values and program-order-successor memory load operations can be satisfied by forwarding from them.
: 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.
: This propagates a single memory store operation to memory.
: 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:
: This causes the
scto fail, either a spontaneous fail or because it is not paired with a program-order-previouslr.: This transition indicates the
scis paired with anlrand might succeed.: This is an atomic execution of the transitions and , it is enabled only if the stores from which the
lrread from have not been overwritten.: This causes the
scto fail, either a spontaneous fail or because the stores from which thelrread from have been overwritten.
Transitions specific to AMO instructions:
: 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:
The transitions labeled ∘ can always be taken eagerly, as soon as their precondition is satisfied, without excluding other behavior; the • cannot. Although is marked with a •, 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:
and/or (as many as needed to satisfy all the load operations of the instance)
Before, between and after the transitions above, any number of transitions may appear. In addition, a 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.
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):
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).
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 and 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 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).
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_names (including system registers), as statically determined from the pseudocode of the instruction;
dst_regs, the destination reg_names (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):
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.
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.
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.
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; andfor any other instruction, i.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 address…address + size − 1.
set mem_loads of i to mlos; and
update the state of i to Pending_mem_loads(load_continuation).
In Section [sec: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.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
fenceinstructions with.srand.pwset are finished;for every program-order-previous
fenceinstruction, f, with.srand.prset, and.pwnot 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.tsoinstruction, 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.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 ), and will cause it to restart when that store operation is propagated (see ).
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 “” transition, any memory load operation mlo in i.mem_loads that has unsatisfied slices, can be satisfied from memory if all the conditions of are satisfied. Action: let msoss be the memory store operation slices from memory covering the unsatisfied slices of mlo, and apply the action of .
Note that might leave some slices of the memory load operation unsatisfied, those will have to be satisfied by taking the transition again, or taking . , 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.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.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 address…address + size − 1.
set i.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.mem_stores. Action:
split mem_value between the memory store operations i.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 “” 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
fenceinstructions with.swset are finished;all program-order-previous
fence.tsoinstructions 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;
[omm:commit_store:prev_addrs] all program-order-previous memory access instructions have a fully determined memory footprint;
[omm:commit_store:prev_stores] all program-order-previous store instructions, except for
scthat failed, have initiated and so have non-empty mem_stores; and[omm:commit_store:prev_loads] 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 [omm:commit_store:prev_addrs] is satisfied the conditions [omm:commit_store:prev_stores] and [omm:commit_store:prev_loads] 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.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 “” 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 “”/“” 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.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 ).
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 is satisfied;
the conditions of is satisfied (notice that an
scinstruction can only have one memory store operation); andfor 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 ; and
apply the action of .
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.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 transition.
This does not affect the set of allowed final states, but when explored interactively, if the sc should fail one should use the 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.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:
(zero or more times)
and in addition, the condition of , 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 ), 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 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
.prset, all program-order-previous load instructions are finished;if i is a normal fence and it has
.pwset, all program-order-previous store instructions are finished; andif 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.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.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.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:
all program-order-previous load-acquire instructions are finished;
all program-order-previous
fenceinstructions with.srset are finished;for every program-order-previous
fence.tsoinstruction, f, that is not finished, all load instructions that are program-order-before f are finished; andit 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 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 cfp in the memory footprint of i. If $\overline{\textit{cfp}}$ is not empty:
i′ has a fully determined memory footprint;
i′ has no unpropagated memory store operations that overlap with $\overline{\textit{cfp}}$; and
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 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.
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 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.
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 registerx2(the instruction semantics will be blocked if necessary until the register value is available), say0x4000, to read_continuation returns Load_mem(plain_load,0x4000,4, load_continuation). Feeding the 4-byte value loaded from memory location0x4000, say0x42, to load_continuation returns Write_reg(x1,0x42, Done). Many Internal(next_state) states may appear before and between the states above.