Flowing and POP (ARMv8) Web-interface

A Tool for Exploring the ARMv8 ISA and Memory Models

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

Usage

To use the web interface click on the Flowing or POP link. 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:

Examples

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: