Metadata Table
Manual Type user
Spec Revision 20181106-Base-Ratification
Spec Release Date
Git Revision 20181106-Base-Ratification
Git URLhttps://github.com/riscv/riscv-isa-manual.git
Sourcesrc/memory-model-alloy.tex
Conversion Date2023/11/12
LicenseCC-by-4.0

Formal Axiomatic Specification in Alloy

We present a formal specification of the RVWMO memory model in Alloy (http://alloy.mit.edu). This model is available online at https://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 Section [sec:memory:porting].

The RVWMO memory model formalized in Alloy (1/5: PPO)
The RVWMO memory model formalized in Alloy (2/5: Axioms)
The RVWMO memory model formalized in Alloy (3/5: model of memory)
The RVWMO memory model formalized in Alloy (4/5: Basic model rules)
The RVWMO memory model formalized in Alloy (5/5: Auxiliaries)