This repo presents a formalization of the RISC-V memory consistency model.

This repo is meant to serve as an upstream for the official RVWMO specification at https://github.com/riscv/riscv-isa-manual.

This version of the model is specified in Alloy. The ISA manual contains other presentations of the memory model as well.

Note: this version of the model does not support mixed-size or misaligned accesses.

More updates likely to follow over time...