RMEM is a tool for exploring the relaxed-memory concurrency behaviour allowed by the ARM, IBM POWER, and RISC-V architectures; it also has experimental support for a mixed-size version of x86-TSO.

It lets one take small test programs, either concurrency litmus tests or standalone ELF binaries, and explore the envelope of all their architecturally allowed behaviour -- interactively, randomly, or exhaustively.

There is a web version for convenient use, compiled to JavaScript and running in the browser (best used in chrome/chromium), and a command-line version (not included here) for better performance and batch use.

Getting Started

To use the web version:

For ARM, POWER, and RISC-V, 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 and exclusives, isb, dmb sy, dmb ld, and dmb st; and POWER load-reserve/store-conditional, sync, lwsync, and isync. They do not cover load-store pair/multiple, read-modify-writes, exceptions, interrupts, floating-point, vector instructions, MMU aspects, or self-modifying code.

Bugs and Workarounds



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).


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.


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


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.


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.

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.


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 "Hide finished instructions but last..." 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.

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).

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 interface 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, in 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.

Full console help

RMEM console help

The command line indicates in [square brackets] the default command to be taken

if enter is pressed on an empty command line. Multiple commands may be

semicolon-separated on one line. Note that a trailing semicolon has an empty

command on the right hand side, which is interpreted as the default command.


(...|...) Represents alternatives

[...] Represents an optional section

<N[n]> Represents a positive integer (including

zero) in either decimal or (0x prefixed)


<ioid> Represents instruction instance ID. This can

be entered as two integers, separated by

colon or space, where the first one is the

thread number and the second one is the

instruction number within the thread (e.g.

'0:1' or '0 1' both represent the first

instruction of thread 0).

<string[n]> Represents an arbitrary string containing no


<bool[n]> Represents a boolean. Accepted values:

true = 'true', 'on', '1', 't', 'yes', 'y'

false = 'false', 'off', '0', 'f', 'no', 'n'

Stepping commands

<N> Take the transition with the given number,

and all the enabled eager transitions that

follow (see 'help eager').

<N1>e<N2> Take transition <N1>, and then another <N2>

enabled eager transitions (see 'help


s|step [<N>] Take the default transition <N> times,

default once.

b|back [<N>] Step back <N> previously taken transitions,

default one.

a|auto Repeatedly take the default transition until

no more enabled transitions exist.

Analogous to 'holding down enter'.

set follow_list "[<N>[;<N>[...]]]"

Set the list of upcoming transitions.

Note 1: 'set follow_list "4;2"' is a single

command that sets the follow-list to 4

followed by 2, and 'set follow_list 4;2'

(without the double quotes) is two

commands: set the follow-list to 4 and take

transition 2 (which has the side effect of

clearing the follow-list because it does

not match the next transition in the

follow-list, 4).

Note 2: 'set follow_list ""' clears the


fo|follow Repeatedly take all the transitions from the


set follow_list "[<N>[;<N>[...]]]"

Set the list of upcoming transitions.

Note 1: 'set follow_list "4;2"' is a single

command that sets the follow-list to 4

followed by 2, and 'set follow_list 4;2'

(without the double quotes) is two

commands: set the follow-list to 4 and take

transition 2 (which has the side effect of

clearing the follow-list because it does

not match the next transition in the

follow-list, 4).

Note 2: 'set follow_list ""' clears the


fo|follow Repeatedly take all the transitions from the


fetch Take all fetch transitions. Note, this may

not terminate if the test has loops.

set random <bool> Enable or disable the default transition

being pseudorandomly chosen.

set storage_first <bool> Enable or disable whether storage transitions

are preferentially taken first when


focus thread (<N>|off) Enable only transitions for the given thread

id, or 'off' for all threads.

focus instruction (<ioid>|off) Enable only transitions for the given

instruction ioid, or 'off' for all


si|stepi [<N>|<ioid>] Take transitions of the specified instruction

until it is finished, if possible. The

specified instruction is either <ioid>, the

first instruction of <N> that has enabled

transitions, or the first instruction with

enabled transitions of the first thread

with such instruction.

peeki <ioid> Show all the states instruction <ioid> can

reach by taking only <ioid> transitions.

Each state of <ioid> will be printed with

the sequence of transitions that leads to

it below.

Searching commands

search (exhaustive|random <N>) [final|final_ok|final_not_ok]

Run an exhaustive search, or <N> pseudorandom

linear searches, through the graph of

possible states, looking for final states

in which no more transitions are possible,

and print a histogram of the reachable

final states. If a breakpoint is hit during

the search, it will stop and jump to the

breakpoint-matching state.

set hash_prune <bool> Enable or disable using hashing of states to

avoid visiting a state's subtree more than

once in a search.

set prune_restarts <bool> Enable or disable discounting traces with

instruction restarts when searching

(believed to be safe).

set prune_discards <bool> Enable or disable discounting traces with

instruction discards when searching

(believed to be safe; requires '-model


set partial_order_reduction <bool>

Enable or disable restricting searches

according to the partial order reduction

set priority_reduction <bool> Enable or disable taking certain kinds of

transition preferentially by disabling all

others when they exist. Currently:

exclusives, multiple-successor fetches.

set allow_partial <bool> Enable or disable setting a signal handler to

allow interrupting a search and returning

partial results.

set compare_analyses <bool> Enable or disable comparing the handwritten

and exhaustive analyses.

set transition_limit (<N>|none) Set the transition limit on searches.

set trace_limit (<N>|none) Set the trace limit on searches.

set time_limit (<N>|none) Set the time limit on searches in seconds.

set branch-targets "<bt-map>" EXPERIMENTAL. Sets the initial approximation

of branch targets for branch-register

instructions (will be extended by the

search until a fixed-point is reached).

In the 'set foo_limit ...' commands, 'none' means no limit (the default).

Breakpoint commands

break <N> Insert a breakpoint that will fire when the

given address can be fetched.

break <string>

break <string>+<N>

break <string>-<N> Insert a breakpoint that will fire when the

address of the given symbol, optionally

plus or minus an offset, can be fetched.

break <string>:<N> Insert a break-point that will fire when the

given source line can be fetched.

[a|r]watch <N> Insert a watch-point of size one byte at the

given address.

[a|r]watch <N1>/<N2> Insert a watch-point of size <N2> at address


[a|r]watch <string>

[a|r]watch <string>+<N>

[a|r]watch <string>-<N> Insert a watchpoint of size one byte at the

given symbol, optionally plus or minus an


[a|r]watch shared Insert a watchpoint that triggers on all

locations which have been recorded as


info break Print all the currently active breakpoints.

delete [break] <N> Delete the breakpoint with the given number.

For all watchpoint commands, the type of watchpoint inserted

is determined by the prefix of the command:

if no prefix is given, a write watchpoint;

or if 'r' is prefixed, a read watchpoint;

or if 'a' is prefixed, an access watchpoint (either read or write.)

Eager options

set eager <bool> Shortcut to enable/disable all the eager

options at once, except that 'set eager on'

does not enable eager_fetch_multi (as that

can cause infinite loops) and


set eager_fetch_single <bool> Fetch transitions with a single successor

set eager_fetch_multi <bool> Fetch transitions with multiple successors

(i.e., branches. Can cause infinite loops)

set eager_pseudocode_internal <bool>

Pseudocode-internal transitions

set eager_constant_reg_read <bool>

Constant register reads (e.g. pseudo-regs.)

set eager_reg_rw <bool> Register reads and writes

set eager_memory_aux <bool> Memory auxiliary transitions (e.g. flowing

events, barriers, commits)

set eager_finish <bool> Instruction finish transitions

set eager_fp_recalc <bool> PLDI11 footprint recalculation transitions

set eager_thread_start <bool> Thread start transitions

set eager_local_mem <bool> EXPERIMENTAL. Affects searching only. Eagerly

take thread-local memory access transitions

using an approximation of the shared memory

footprint. The approximation is refined at

the end of the search, and another search

is started, until a fixed-point is reached.

set shared-memory "<footprints>" EXPERIMENTAL. Sets the initial approximation

of the shared memory footprint for

eager_local_mem (will be extended by the

search until a fixed-point is reached).

set eager_fetch_unmodified <bool> EXPERIMENTAL. Affects searching only. Eagerly

take fetch transitions using an

approximation of the set of modified

locations. The approximation is refined at

the end of the search, and another search

is started, until a fixed-point is reached.

set memory-writes "<footprints>" EXPERIMENTAL. Overwrites the approximation of

the modified code locations for


When exploring interactively, these options control which transitions are

considered 'uninteresting' and eagerly taken, which should not affect the set

of observable behaviours because these are all (believed to be...)

confluent with each other.

Interface options

set pp_style (full|compact|screenshot)

Set the printing style

set condense_finished_instructions <bool>

Enable or disable condensing finished

instructions in printed states.

set max_finished (<N>|none) Set the maximum number of finished

instructions printed at the start of each


set pp_sail <bool> Enable or disable showing the Sail

interpreter state and code for instructions

(if interpreter enabled).

set verbosity (quiet|normal|verbose|very|debug)

Set the verbosity of command line output.

set choice_history_limit (<N>|none)

Set the maximum number of 'choices so far'

printed with the current state, 'none' for

no limit.

set always_print <bool> Enable or disable printing the current state

after every command.

set prefer_symbolic_values <bool> Enable or disable preferring symbolic values

to hex in output.

set pp_hex <bool> Enable/disable printing histogram values in


set hide_pseudoregister_reads <bool>

Hide or show pseudoregister reads in output

set pp_colours <bool> Enable or disable colourised output

set dwarf_show_all_variable_locations <bool>

Enable or disable showing all DWARF variable

location data at each instruction

set state_output <file> Print the current state, every time it

changes, to <file>.

set trace_output <file> Print the current trace, every time it

changes, to <file>.

Graph options

set always_graph <bool> Enable/disable generate a .dot or onscreen

transition graph after every command

set graph_backend (dot|tikz) Set the backend used for generating graphs

set ppg_shared <bool> Enable/disable showing *only* shared-memory

instructions in graph output

set ppg_rf <bool> Enable/disable showing read-from (rf) edges

set ppg_fr <bool> Enable/disable showing from-read (fr) edges

set ppg_co <bool> Enable/disable showing coherence (co) edges

set ppg_addr <bool> Enable/disable showing address dependency

(addr) edges

set ppg_data <bool> Enable/disable showing data dependency (data)


set ppg_ctrl <bool> Enable/disable showing control dependency

(ctrl) edges

set ppg_regs <bool> Enable/disable showing registers in graph


set ppg_reg_rf <bool> Enable/disable showing rf edges in graph


set ppg_trans <bool> Enable/disable showing transitions in graph


Miscellaneous commands


q|quit Quit rmem

?|h|help Show a help message for all the commands.

h|help <command> [<args>] Show a help message for <command>.

h|help <category> Show all the commands related to <category>.

The following categories are available:

stepping, searching, breakpoints, eager,

interface, graphs, misc

typeset Write LaTeX of the current state to


graph Write a graphviz/TikZ graph of state and

transitions to out.dot/out.tikz

p|print Print the current state

his|history Print the history of previously entered


o|options Print the current configuration of options

set <key> [<arg> [<arg>[...]]] Set <key> according to <arg>s