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...