A Tool for Exploring the POWER and ARM Memory Models

PPCMEM (also known as ARMMEM) is a tool with a web interface for exploring our formal architectural model of the Power and ARM memory models, as described here and in the paper:

This work is associated with a broader project on Relaxed-Memory Concurrency.

Usage To use the web version of the tool:


Disclaimer Note that, while some confidence in the models has been established by experiment and discussion (as described in the associated papers), they are not officially sanctioned by either IBM or ARM.


The model code was built using Lem, and js_of_ocaml was used to compile OCaml bytecode to Javascript.