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 sc to fail, either a spontaneous fail or because it is not paired with a program-order-previous lr.

• : This transition indicates the sc is paired with an lr and might succeed.

• : This is an atomic execution of the transitions and , it is enabled only if the stores from which the lr read from have not been overwritten.

• : 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:

• : 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:

3. 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.

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:

1. i is finished; or

2. 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.

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.

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:

1. 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

2. 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.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.

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:

1. 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.

2. set mem_loads of i to mlos; and

3. update the state of i to Pending_mem_loads(load_continuation).

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:

1. all program-order-previous fence instructions with .sr and .pw set are finished;

2. 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;

3. 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;

4. if i is a load-acquire-RCsc, all program-order-previous store-releases-RCsc are finished;

5. if i is a load-acquire-release, all program-order-previous instructions are finished;

6. all non-finished program-order-previous load-acquire instructions are entirely satisfied; and

7. 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:

1. update i.mem_loads to indicate that mlo was satisfied by msoss; and

2. 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.

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 .

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:

1. 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.

2. set i.mem_stores to msos; and

3. update the state of i to Plain(next_state).

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:

1. split mem_value between the memory store operations i.mem_stores; and

2. 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:

1. i has fully determined data;

2. all program-order-previous conditional branch and indirect jump instructions are finished;

3. all program-order-previous fence instructions with .sw set are finished;

4. all program-order-previous fence.tso instructions are finished;

5. all program-order-previous load-acquire instructions are finished;

6. all program-order-previous store-acquire-release instructions are finished;

7. if i is a store-release, all program-order-previous instructions are finished;

8. [omm:commit_store:prev_addrs] all program-order-previous memory access instructions have a fully determined memory footprint;

9. [omm:commit_store:prev_stores] all program-order-previous store instructions, except for sc that failed, have initiated and so have non-empty mem_stores; and

10. [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.

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:

1. all memory store operations of program-order-previous store instructions that overlap with mso have already propagated;

2. 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

3. all memory load operations that were satisfied by forwarding mso are entirely satisfied.

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

1. 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

2. 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:

1. update the shared memory state with mso;

2. update i.mem_stores to indicate that mso was propagated; and

3. 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:

1. i′ is finished;

2. every memory store operation that has been forwarded to i′ is propagated;

3. the conditions of is satisfied;

4. the conditions of is satisfied (notice that an sc instruction can only have one memory store operation); and

5. 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:

1. apply the actions of ; and

2. 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:

1. clear i.mem_stores; and

2. update the state of i to Plain(store_continuation(false)).

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:

3. (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.

Commit fence

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

1. if i is a normal fence and it has .pr set, all program-order-previous load instructions are finished;

2. if i is a normal fence and it has .pw set, all program-order-previous store instructions are finished; and

3. if i is a fence.tso, all program-order-previous load and store instructions are finished.

Action:

1. record that i is committed; and

2. 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:

1. add reg_name to i.reg_reads with read_sources and reg_value; and

2. 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:

1. add reg_name to i.reg_writes with deps and reg_value; and

2. 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:

1. 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 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:

      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 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.

2. i has a fully determined data; and

3. if i is not a fence, all program-order-previous conditional branch and indirect jump instructions are finished.

Action:

1. 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

2. 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.