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

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

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 “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
===============================================================================

Multiple commands may be semicolon-separated on one line.
The command line indicates in [square brackets] the default
command to be taken if enter is pressed on an empty command line.

Notation
-------------------------------------------------------------------------------
(... | ...)    represents alternatives
[...]          represents an optional section
<N[n]>         represents a positive integer (including zero)
                 in either decimal or (0x prefixed) hex
<string[n]>    represents an arbitrary string containing no spaces
<bool[n]>      represents a boolean. Accepted values:
                 true = 'true', 'on', '1', 't', 'yes', 'y'
                 false = 'false', 'off', '0', 'f', 'yes', 'y'

Stepping commands
-------------------------------------------------------------------------------
<N>                              Take the transition with the given number.
step | s | step <N>              Take the default transition <N> times,
                                   default once.
back | b | undo | u | back <N>   Undo <N> previously taken transitions,
                                   default one.
stepi <N1> <N2> | si <N1> <N2>   'Step instruction', specifically, search for
                                   and take the shortest path of transitions
                                   to a state in which instruction <N2> of
                                   thread <N1> is finished
follow | f                       Repeatedly take transitions from the
                                   follow-list until either the follow-list is
                                   empty, or it specifies a non-existent
                                   transition number
auto | a                         Repeatedly take the default transition until
                                   no more enabled transitions exist.
                                   Analogous to 'holding down enter'
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 stepping

focus thread (<N>|off)           Enable only transitions for the given
                                   thread id, or 'off' for all threads
focus instruction (<N>|off)      Enable only transitions for the given
                                   instruction ioid, or 'off' for all
                                   instructions

Searching commands
--------------------------------------------------------------------------------
search exhaustive | search random <N>
                                 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.
                                   For exhaustive search, one usually wants
                                   hash_prune, eager, eager_fetch,
                                   and forbid_tree_speculation.

set check_inf_loop <bool>  Enable or disable terminating a search if an
                             infinite loop is detected (Not guaranteed)
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 partial_order_reduction <bool>  Enable or disable restricting searches
                                      according to the partial order reduction
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 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 prune_restarts <bool>  Enable or disable discounting traces with
                             instruction restarts when searching (this
                             is safe for searching because of the proven
                             axiomatic/operational equivalence)
set prune_discards <bool>  Enable or disable discounting traces with
                             instruction discards when searching (same.
                             Requires forbid_tree_speculation)

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

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

Breakpoint commands
-------------------------------------------------------------------------------
break <N>             Insert a breakpoint when the given address is fetched
break <string> | break <string>+<N> | break <string>-<N>
                      Insert a breakpoint when the address of the given symbol,
                        optionally plus or minus an offset, is fetched
break <string>:<N>    Insert a breakpoint when the given source line is fetched

[a|r]watch <N>        Insert a watchpoint of size one byte at the given address
[a|r]watch <N1>/<N2>  Insert a watchpoint of size <N2> at address <N1>
[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 offset
[a|r]watch shared     Insert a watchpoint that triggers on all locations which
                        have been recorded as 'shared'
                        (see also 'set record_writes')

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

info break            Print all the currently active breakpoints
delete [break] <N>    Delete the breakpoint with the given number

Global options
-------------------------------------------------------------------------------
set suppress_internal <bool>  Enable or disable whether Sail micro-steps
                                (exposed as 'Internal' transitions) are suppressed
set record_writes <bool>  Enable or disable written-to memory locations being
                            recorded for the shared-memory approximation
set follow_list <N>[,<N>,...] Set the list of upcoming transitions.
                                (Note, comma separated.)

Eager options
-------------------------------------------------------------------------------
When both searching and 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.

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 <bool>          Shortcut to enable/disable all of the above at once,
                            except that 'set eager on' does not enable
                            eager_fetch_multi (as that can cause infinite loops)

set eager_up_to_shared <bool>         EXPERIMENTAL. Eagerly take even effectful memory
                                        transitions of instructions not in the
                                        shared-memory approximation. May not do what
                                        you expect if enabled at the start of an execution!
                                        Requires record_writes on.


Interface options
--------------------------------------------------------------------------------
set pp_style (full|compact|screenshot)  Set the printing style
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 suppress_newpage <bool>  Enable or disable not clearing the screen before
                               every prompt
set buffer_messages <bool>   Enable or disable holding messages until the
                               next prompt is displayed, for easy reading
set announce_options <bool>  Enable or disable printing the current
                               configuration of options before each prompt
set prefer_symbolic_values <bool>  Enable or disable preferring symbolic
                                     values to hex in output
set hide_pseudoregister_reads <bool>  Hide or show pseudoregister reads in output
set max_finished (<N>|none)  Set the maximum number of finished instructions
                               printed at the start of each thread
set pp_colours <bool>      Enable or disable colourised output
set condense_finished_instructions <bool> Enable or disable condensing
                                            finished instructions in printed states
set pp_hex <bool>          Enable or disable printing histogram values in hex
set dwarf_show_all_variable_locations <bool>  Enable or disable showing all DWARF
                                                variable location data at each
                                                instruction
set pp_sail <bool>         Enable or disable showing the Sail interpreter state
                             and code for instructions (if interpreter enabled)

Graph options
--------------------------------------------------------------------------------
set always_graph  <bool>  Enable or disable generate a .dot or onscreen
                            transition graph after every command
set dot_final_ok <bool>    Enable or disable generating a .dot or onscreen
                             transition graph for the first
                             final-constraint-satisfying execution of searches
set ppg_shared <bool>     Enable or disable showing *only* shared-memory
                            instructions in graph output
set ppg_rf <bool>         Enable or disable showing read-from (rf) edges
set ppg_fr <bool>         Enable or disable showing from-read (fr) edges
set ppg_co <bool>         Enable or disable showing coherence (co) edges
set ppg_addr <bool>       Enable or disable showing address dependency (addr) edges
set ppg_data <bool>       Enable or disable showing data dependency (data) edges
set ppg_ctrl <bool>       Enable or disable showing control dependency (ctrl) edges
set ppg_regs <bool>       Enable or disable showing registers in graph output
set ppg_reg_rf <bool>     Enable or disable showing rf edges in graph output
set ppg_trans <bool>      Enable or disable showing transitions in graph output
set graph_backend (dot|tikz)  Set the backend used for generating graphs

Miscellaneous commands
-------------------------------------------------------------------------------
quit | q | exit | x  Quit ppcmem
help | h | ?         Show this help message
typeset              Write LaTeX of the current state to ui_snapshot.tex
graph                Write a graphviz graph of state and transitions to out.dot
print | p            Print the current state
history | his        Print the history of previously entered commands

===============================================================================