PPCMEM Web-interface

A Tool for Exploring the ARMv8 and POWER Memory Models

This is a web-interface for the tool described in this paper. It allows one to interactively explore all the behaviours the Flowing, POP and POWER models admit for a litmus test selected from a library or written by hand.


To use the web interface click on the ARM (Flowing and POP) or POWER model links. There is also this help page with introduction and guided examples. The interface has two main pages, the configuration page where the desired litmus test and options are selected, and the run page where the selected test is run interactively.

Configuration Page:

Run Page:

Thread subsystem legend:


Below we show three examples in detail. To keep them simple, the instructions explore only a tiny part of the reachable state space; to see more interesting concurrent behaviour, one should select one of the eager-transition options and explore more complex interactions between threads and between threads and the storage subsystem models. For each of the `Allowed' tests in the paper, it should be possible, with some understanding of the model from the paper, to find an execution that reaches the specified final state.

Guided Example 1 (POP with automatic transitions)

Guided Example 2 (Flowing with ISA transitions)

Guided Example 3 (Flowing with automatic ISA transitions and selecting topology)

Browser compatibility:

we have tested the interface on the following configurations: