RMEM

RMEM is a tool for exploring the relaxed-memory concurrency behaviour allowed by the ARM and IBM POWER architectures. There are command-line and web versions, the latter compiled to JavaScript running in the browser (best used in chrome/chromium). It supports small test programs, in the form of litmus tests or standalone ELF binaries.

Getting Started

To use the web version: For both ARM and POWER, the models include essentially all the integer non-vector user-mode instructions, with instruction semantics based on or derived from the vendor pseudocode. They include mixed-size behaviour, ARM release/acquires, exclusives, isb, dmb sys, ld, and st, and POWER load-reserve/store-conditional, sync, lwsync, and isync. They do not cover load-store pair/multiple, RMWs, exceptions, interrupts, floating-point, vector instructions, MMU aspects, or self-modifying code.

Bugs and Workarounds

Papers

People

RMEM also builds on earlier work on tool and model development, for the ppcmem2, ppcmem, and memevents tools, including contributions from Jade Alglave, Ohad Kammar (ex-Cambridge), Pankaj Pawan (ex-IIT Kanpur and INRIA Paris), Ali Sezgin (ex-Cambridge), and Francesco Zappa Nardelli (INRIA Paris)

Disclaimer

Note that, while substantial confidence in the models has been established, by experiment, by discussion with the vendors, and (for the ARM Flat model) by an equivalence proof with the revised ARM architecture axiomatic model, they are not the vendor architecture documents of either IBM or ARM.

Funding

This work is funded by REMS: Rigorous Engineering for Mainstream Systems, by an EPSRC iCASE studentship, and by an EPSRC Impact Acceleration Account Knowledge Transfer Fellowship (with ARM).

User Guide

Tests

The menu-bar Load litmus test and Load ELF test buttons let one choose a test to run, either a litmus test or a standalone ELF binary.

One can choose tests from the built-in libraries, which include many tests mentioned in the literature, select files from the local filesystem, or paste tests into an editing window. The litmus library is subdivided into categories, shown on the left. If one starts to type a test name in the "Filter" box, it shows the categories and matching tests within the currently selected category.

Litmus tests are in essentially the same format as used by the litmus tool for running tests on hardware (see the TACAS 2011 paper) and the herd tool for axiomatic models, both part of the diy suite, except that the supported instructions may differ.

Standalone ELF binaries can be produced (for example) by compiling C programs with gcc or clang, e.g. using the gcc flags CFLAGS=-g -std=c11 -Wall -save-temps=obj -ffreestanding -nostdlib -Wl,--defsym,_start=main -Wa,-L -D__THREAD_START_H=\"thread_start_aarch64.h\" for ARM and CFLAGS= -g -std=c11 -mcpu=power7 -Wall -save-temps -msoft-float -ffreestanding -nostdlib -Wl,--defsym,_start=main -Wa,-L for POWER.

The models support a special "thread start" pseudo-instruction to start a new hardware thread; see the atomics_test_2.c example in the ELF test library for example usage and the appropriate ARM or POWER header file. The maximum number of threads must be configured in the "Load ELF test" dialogue.

Model options

The menu-bar Model Options lets one control which concurrency model to use (the available models and options differ for ARM and POWER tests). The models are: These are all operational models, defining model states and transitions.

For the intra-instruction semantics, one can choose either the Sail interpreter (allowing single-stepping through the Sail pseudocode for each instruction instance) or the "Shallow embedding" (computing the next outcome of each instruction instance directly).

The Out-of-order mode lets one choose whether to allow simultaneous exploration of multiple successors of conditional branches ("tree speculation" allowed) or restrict to exploration of a single path at a time ("tree speculation" forbidden). This should not affect the set of final allowed states. For performance, one often wants to forbid tree speculation.

In the Flowing model, one has to choose the desired topology.

Panes

The main UI consists of a menu bar and one or more panes. Each pane can display one of: Panes can be subdivided horizontally or vertically, or deleted, with the buttons at their top right corner. The boundaries between them can be dragged. The font size of each pane can be adjusted separately. The graph can be dragged within its pane.

Interactive exploration

The console, graph, and trace panes each show the enabled transitions of the current model state, underlined and highlighted in blue; one can just click on these to construct a possible (architecture/model-allowed) execution incrementally. The Undo and Restart menu-bar buttons undo transitions and restart the execution, respectively.

Eager transitions

Depending on what one wants to explore, one may want to make one or more kinds of transition "eager", using the Execution options drop-down in the menu-bar. For stepping through the pseudocode of a single instruction, one typically wants nothing eager, while for exploring the allowed concurrent execution of a litmus test, one might want all the below eager. Making transitions eager means they will be automatically taken whenever enabled, leaving only the non-eager transitions visible. Several kinds of transition can independently be made eager: One can also select all or none of those. Taking any of these eagerly should not eliminate any potential executions. For the Flat model, the transitions for satisfying a memory read and propagating a memory write cannot be made eager, as in general taking one such transition may exclude some other behaviour. For code with loops, making instruction fetch eager will not terminate, otherwise it can be eager. The console fetch command will also fetch all the instruction instances.

Additionally, if using the Sail interpreter, the "Suppress internal" option makes pseudocode internal steps be taken by the interpreter rather than be exposed as transitions.

In the web interface version, browsers without tail-call optimisation may hit stack overflow issues.

Default transitions

One of the enabled transitions is selected as the default, which can be taken just be pressing Enter; the default transition is highlighted in yellow. The Execution drop-down Random option makes the default be chosen randomly, otherwise it is normally chosen in a deterministic (but rather arbitrary) way.

Follow-mode

The enabled transitions in each state are numbered, and the list of choices made so far is displayed in the console window. To replay a trace interactively, one can set the "follow list" to such a list, with the console set follow_list command, which then makes the default transition that from the next step in the follow list.

Interface display options

The menu-bar Interface drop-down gives several options for controlling the amount of detail in the console output. Here the main options are "Show Sail state and code", controlling whether the detailed pseudocode state for each instruction instance is displayed, and the "PP Style" which can be "compact" or "full".

For larger tests, especially compiled ELF files, one often wants to suppress most of the prefix of finished instructions, by setting the "Finished insts limit" Interface option.

Graph display options

The menu-bar Graph drop-down gives several options for controlling the graph output: By default the graph is redrawn after every transition, but for large graphs this may be too slow, in which case "Update every step" can be turned off and one can use the manual "Refresh" button on the graph pane.

For searches, one can also choose whether to display a graph of a final state that satisfies the condition of a litmus test, "Final OK graph".

The "Download .dot" button on the graph pane title lets one download the GraphViz dot source for the displayed graph.

Random search

The Search menu-bar drop-down includes a "Search randomly" button, which explores some user-selectable number of random traces. For each trace, it start with the current state and takes a sequence of pseudo-randomly chosen transitions. The results are shown as a histogram of the values in the reachable final states, with (for each) a sample trace (expressed as a follow-mode list of transition numbers) that reached those values.

These histograms are in the same format as those produced by the litmus tool, to let one compare model results with experimental results from running tests on hardware (usually using model results from running the console version on batches of tests).

Exhaustive search

The Search menu-bar drop-down also includes a "Search exhaustively" button, which tries an exhaustive search from the current state. To reduce the state space, one usually wants: Exhaustive search also prints a histogram of the reachable final states on the console.

For both random-trace and exhaustive search, one can set limits, of the amount of time or number of transitions.

Stepping control

The console interfce provides additional control of stepping:

ELF/DWARF Debug information output

When running an ELF file that was compiled with debugging information, rmem will by default use that information in the output: using the source-code names for global and local variables, and showing the C source code lines associated with assembly instructions. This can be toggled with "Enable DWARF support" in the "Load ELF test" dialogue. The tool does not currently use DWARF type information, e.g. for displaying values of C struct types.

Debugger-style breakpoints and watchpoints

For larger tests (especially ELF files compiled from non-trivial C code), one may want to automatically execute up to some condition, i n the same way as one might use a debugger such as gdb, rather than single-step.

The console break and watch commands let one set breakpoints at particular addresses (numeric or a symbol with a numeric offset) and for particular source lines, and watchpoints for particular addresses (numeric or a symbol with a numeric offset), of a specified size (in bytes). Watchpoints can be for reads, writes, or both. These apply to exhaustive and random search.

Along with this, one sometimes wants to turn off the automatic redisplay of the model state in the console, with the Interface dropdown "Always print" option. One can also toggle "Scroll on output" and "Suppress newpage".

Linking to model/tool states

When discussing some particular example, it is often useful to communicate particular executions. This can be done in two ways: one can either just manually paste the follow-mode list of transition numbers (note that this will only be valid for the same eager-mode options), but one can also use the menu-bar Link to this state dropdown to construct a URL that includes that, and optionally also includes other information.