Metadata Table
Manual Type	user
Spec Revision	20191214-
Spec Release Date	December 2019
Git Revision	Priv-v1.12
Git URL	https://github.com/riscv/riscv-isa-manual.git
Source	src/memory-model-alloy.tex
Conversion Date	2023/11/12
License	CC-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)