Appendix B is RVWMO three more times, in executable form. Prose rules settle arguments slowly; these models settle them mechanically — and they are the reference artifacts a memory-model verification flow runs against.
| What it is | Use it to… | |
|---|---|---|
| B.1 · Alloy | Relational-logic model for the Alloy analyzer (alloytools.org) | Bounded model checking |
| B.2 · herd | riscv.cat — the same axioms in herd7’s cat language (diy.inria.fr) | Run the 7000+-test litmus suite; the day-to-day axiomatic reference |
| B.3 · operational | Abstract state machine in rmem, with Sail ISA semantics | Incremental/interactive exploration; the model that “feels like a pipeline” (next pages) |
The Alloy model’s anatomy
The model builds RVWMO from a handful of signatures and relations — recognizable one-for-one from ch. 18:
- Events:
MemoryEventsplits into loads (normal / reserve), stores (normal / conditional) and AMOs;Fenceevents carry pr/pw/sr/sw bits; annotations mark Acq/Rel and RCsc/RCpc strength. - Relations: program order
po, the three syntactic dependency relations (addrdep,ctrldep,datadep), LR→SC pairing (rmw), reads-fromrf, coherenceco— and from them a derived global memory order. - Constraints: the load-value axiom, atomicity axiom, and progress axiom, plus the thirteen PPO rules, each a short relational predicate.
An execution is RVWMO-legal iff the constraints are satisfiable over it; the analyzer explores every candidate up to a size bound.
Hardware Designer Notes
Practical setup for a core team: (1) run the litmus suite on RTL simulation with random perturbation, (2) collect outcome sets, (3) diff against herd’s allowed outcomes — any RTL outcome herd forbids is a silicon-grade bug. The operational model (next page) adds the interactive debugging angle when a diff needs a step-by-step witness.
Minimal Linux-boot hart MUST
- Adopt an executable-model diff flow: herd7 verdicts vs RTL outcomes over the litmus suite is the memory-model signoff gate
MAY simplify / trap-and-emulate
- Use Alloy when debating micro-architecture-motivated model questions — it finds distinguishing programs mechanically
- Skip reading the Alloy source line-by-line: its structure IS ch. 18, one predicate per rule
Check yourself — Alloy & herd
1.What does the Alloy formalization buy you that prose rules don't?
2.Which tool + input pair is the standard axiomatic reference flow for litmus testing a RISC-V core?