PPCMEM/ARMMEM 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:
- Click on the PPCMEM
or ARMMEM link
- Select a test to run from the menu. The tests are divided into
families: for each of ARM and POWER, there are some hand-written
tests and several uniform families (MP, SB, WRC, IRIW etc.) with
different combinations of barriers and dependencies. Most of these
are discussed in
the paper
above, and there are experimental results and diagrams of the
relevant executions in
the supplementary material here (for
ARM) and here (for POWER).
- Click `Interactive' to explore the test interactively. The
screen will show the state of the memory model abstract machine,
with the allowable transitions highlighted in green. Click on any one of
those to follow that transition to its associated next state. After
doing so, the parts of the state that have changed will be
highlighted in red.
- Click on `Undo' to go back a transition, `Reset' to go back to
the start to choose a new test, or `Auto' to explore all
possible executions from this state and display their final values
(on some Javascript implementations, `Auto' will work only for
relatively small tests).
Download
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.
People
The model code was built
using Lem, and
js_of_ocaml was
used to compile OCaml bytecode to Javascript.