The rmem tool comprises executable operational models for the relaxed-memory concurrency semantics of the Power, ARMv8, RISC-V, and x86 (TSO) processor architectures, as well as machinery for executing the models on litmus tests and ELF binaries: allowing one to interactively step through the legal concurrency behaviours, pseudorandomly find legal outcomes, and exhaustively enumerate all architecturally allowed outcomes of small bounded concurrent programs. For ARM, it supports both the current ARMv8-A multicopy atomic model and the earlier ARMv8-A non-multicopy-atomic model.
The tool provides both a stand-alone web-interface version (compiled to JavaScript), which can be tried at http://www.cl.cam.ac.uk/users/pes20/rmem, and a command-line version.
rmem was developed as part of the REMS project, partly funded by ERC Advanced grant "ELVER" (2018-2023, ERC AdG 789108), the EPSRC Programme Grant "REMS: Rigorous Engineering for Mainstream Systems" (EP/K008528/1), EPSRC grant "C3: Scalable & Verified Shared Memory via Consistency-directed Cache Coherence" (EP/M027317/1), an ARM iCASE award (Pulte), an EPSRC IAA KTF (Gray), EPSRC Leadership Fellowship "Semantic Foundations for Real-World Systems" (EP/H005633/1, 2009-2014, Sewell), an Arm iCASE Award (Simner), and EPSRC grant "Reasoning with Relaxed Memory Models" (EP/F036345, 2008-2012).
rmem relies on a number of dependencies, including:
The dependencies can be installed automatically as part of the rmem build process, as detailed below.
In addition, a debian based Linux system also need the following packages:
sudo apt install findutils libgmp-dev m4 perl pkg-config zlib1g-dev # add the REMS opam repository containing some of rmem's dependencies:
opam repository add rems https://github.com/rems-project/opam-repository.git#opam2
opam install rmem # clone the repo:
git clone git@github.com:rems-project/rmem.git
cd rmem
# add the REMS opam repository containing some of rmem's dependencies:
opam repository add rems https://github.com/rems-project/opam-repository.git#opam2
opam install .To rebuild and reinstall after local changes, run opam upgrade --working-dir rmem (or opam upgrade -w rmem).
makeAlternatively, rmem can be built using make as follows:
# clone the repo:
git clone git@github.com:rems-project/rmem.git
cd rmem
# get rmem's opam dependencies
opam repository add rems https://github.com/rems-project/opam-repository.git#opam2
opam install --deps-only .
# build rmem
make MODE=opt This will build a native rmem OCaml binary.
The invocation make MODE=debug builds an OCaml bytecode
version. To build rmem for only a specific ISA, for instance
AArch64, run make rmem MODE=opt ISA=AArch64. For additional
information and build options see make help.
Finally run rmem --help for information on how to run rmem and the
available options.
TODO.
(The web interface is built using JS_of_ocaml.)
The contributors to the rmem code are listed in the LICENCE.txt file
rmem is a successor to the ppcmem tool, originally developed to model the concurrency semantics of the IBM Power architecture in the "PLDI11" model, developed from 2009 onwards. It has since been substantially extended and re-engineered, and it currently includes several concurrency models:
The Flat model for ARMv8 and RISC-V, principally by Christopher Pulte and Shaked Flur, described in the paper and RISC-V architecture manual below, and co-developed with the revised ARMv8-A axiomatic model, principally by Will Deacon.
The PLDI11 Power model, principally by Susmit Sarkar and Peter Sewell, originally as described in the papers below, and adapted since.
The Flowing and POP models for ARMv8, principally by Shaked Flur, described in:
Originally all these models and the tool assumed all memory accesses were aligned and of the same size. Mixed-size support was added by Shaked Flur, Susmit Sarkar, Peter Sewell, and Kathryn E. Gray, as described in the paper:
The TSO model for x86, by Linden Ralph and Shaked Flur, adding mixed-size accesses and Sail ISA integration to the x86-TSO model described in:
The Promising model for ARMv8 and RISC-V, executable model principally by Christopher Pulte:
An extension to the Flat model for Arm to model instruction fetch and the required cache maintenance instructions, described in:
These models have been validated against observable hardware behaviour using the litmus tool of the herdtools tool suite of Jade Alglave and Luc Maranget; this validation has been done principally by Luc Maranget and Shaked Flur. Some models have also been compared or co-developed with axiomatic models expressed using the herd tool of that tool suite.
rmem integrates Sail models for the sequential aspects of the instruction semantics. The initial work, doing this for IBM POWER, is described in:
More recent work, integrating a newer version of Sail with rmem (currently only for RISC-V), is described in:
(2023/10/19 Note: rmem is currently lagging behind Sail development. rmem's integration of ISA models is based on the now-outdated Sail1, and all ISA models except RISC-V are Sail1 models. To accommodate the Sail2-based RISC-V model, rmem internally converts Sail2 types to Sail1 types. The parts of Sail1 rmem relies on are checked in as src_sail_legacy.)
rmem also includes extensive infrastructure for driving the models and providing user interfaces.
OCaml harness for driving the models, in exhaustive, pseudorandom, and interactive mode, infrastructure for connecting to the ELF model, pretty-printing the user interface, etc.: Shaked Flur, Susmit Sarkar, Jon French, Peter Sewell, Christopher Pulte, Luc Maranget, Pankaj Pawan, and Francesco Zappa Nardelli.
The current graphical Web interface is principally by Jon French; an earlier version was principally by Pankaj Pawan and Francesco Zappa Nardelli.
rmem integrates code from herdtools, in (src_top/herd_based), for parsing and pretty printing of litmus tests, maintaining compatibility with the herdtools tools. This code is due to Jade Alglave and Luc Maranget.
Integrating dwarf information for improved user-interface: Peter Sewell and Shaked Flur.
rmem
|
|---- pldi11, pldi11Opt, flat, etc. // shell scripts that run the corresponding
| // model in a suitable configuration. The
| // 'opt' version turns on the recommended
| // performance optimisations for exhaustive
| // execution
|
+---- src_top // OCaml code of the rmem tool
| |
| +---- herd_based // parsing litmus files (forked from herdtools)
| +---- text // CLI
| +---- web // web-interface
| +---- headless // CLI without interactive mode (does not depend on
| // lambda-term which does not build on Power)
|
+---- src_concurrency_model // Lem code of the concurrency models
|
+---- src_isa_defs // Lem code defining details of the ISA models
|
+---- src_isa_stubs/<ISA> // stubs for when the ISA is excluded from the build
|
+---- src_web_interface // non-OCaml code of the web-interface (and some
| // tests)
|
|
+---- gen_files // hand-written files helping with parsing/pretty-printing/etc.
|
+---- scripts // scripts for various things
|
|
+---- src_sail_legacy // temporary: a copy of the relevant bits of an old
| // version of Sail and surrounding infrastructure: for
| // models not ported to current Sail yet
|
| // THE FOLDERS BELOW ARE CONSTRUCTED DURING THE BUILD PROCESS AND ARE
| // NOT CHECKED IN
|
+---- _build // ocamlbuild workspace
|
+---- generated_ocaml // OCaml files generated from the concurrency and
// ISA model Lem definitions