The operational model re-presents RVWMO as an abstract machine with explicit out-of-order and speculative execution — no renaming, store buffers, or caches, but recognizably pipeline-shaped. It’s intended to admit exactly the executions the axiomatic model admits, covers mixed-size accesses (misaligned → single-byte operations), and lives in the rmem rmem and sail rmem (github.com/rems-project/rmem): the exploration tool embedding the operational model with Sail-defined RV64IA instruction semantics; runs litmus tests and small ELFs exhaustively, pseudorandomly, or interactively (web + CLI). Sail is the ISA-description language; sail-riscv is the golden ISA model. defined in ch. I·B — open in glossary tool with Sail-defined RV64IA instruction semantics. One terminology shift: here every memory operation is either a load or a store — an AMO contributes one of each (re-fused later by an atomic transition).
Model state anatomy
- Shared memory: simply the list of store operations that have propagated, in propagation order.
- Per-hart state: a tree of instruction instances. Conditional branches and indirect jumps may have several fetched successors — speculation as tree branches; when the transfer finishes, untaken subtrees are discarded. Non-finished instances can be restarted if a speculative load they depended on proves unsound.
- Per-instance state: the execution state of its Sail pseudocode (control point, call stack, locals) plus footprints, register reads/writes, memory operations, finished flag.
The pseudocode interface
Each instruction runs as a little state machine whose states name the next thing the memory model must do:
| Meaning | |
|---|---|
| Load_mem(kind, addr, size, k) | Pending memory load |
| Store_ea(kind, addr, size, next) | Store effective address known — footprint fixed before the value |
| Store_memv(value, k) | Store value available; k learns success (always true except failed SC) |
| Early_sc_fail(k) | Offer the SC a spontaneous early failure |
| Fence(kind, next) | Fence request (normal with pred/succ bits, or TSO) |
| Read_reg(name, k) / Write_reg(name, v, next) | Register traffic |
| Internal(next) / Done | Pure computation step / pseudocode finished |
The spec’s own walkthrough: lw x1,0(x2) begins in
Read_reg(x2, k); feeding it 0x4000 yields
Load_mem(plain_load, 0x4000, 4, k′); feeding the loaded bytes yields
Write_reg(x1, value, Done) — with Internal steps sprinkled anywhere.
Hardware Designer Notes
The tree-of-instances view is the cleanest mental model of what speculation is ALLOWED to do architecturally: anything, as long as discard/restart happens before finishing. The transitions that police that boundary are the next page.
Minimal Linux-boot hart MUST
- Nothing directly — this is a reference model, not an implementation mandate
MAY simplify / trap-and-emulate
- Read your pipeline against the state anatomy: ROB ≈ the instruction tree, replay ≈ restart, store queue ≈ unpropagated stores
- Use rmem interactively to produce step-by-step witnesses when herd/RTL outcome diffs need explaining
Check yourself — operational model states
1.In the operational model, what is a hart's state?
2.Why do AMOs become TWO memory operations (a load and a store) in the operational model when the axiomatic model treats them as one load-store operation?
3.How does the model handle instruction fetch and self-modifying code?