Skip to content

Latest commit

 

History

History
269 lines (200 loc) · 13 KB

README.md

File metadata and controls

269 lines (200 loc) · 13 KB
Raw

rmem: Executable concurrency models for ARMv8, RISC-V, Power, and x86

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

Dependencies

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

Building and running rmem with command-line interface, with opam

  # 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

Building and running rmem with command-line interface, with opam, from a github checkout

  # clone the repo:
git clone [email protected]: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).

Building and running rmem with command-line interface, with make

Alternatively, rmem can be built using make as follows:

  # clone the repo:
git clone [email protected]: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.

Building rmem with web interface

TODO.

(The web interface is built using JS_of_ocaml.)

Authors

The contributors to the rmem code are listed in the LICENCE.txt file

The concurrency models and their contributors

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.

    • Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8. Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell. In POPL 2018.
      • The RISC-V Instruction Set Manual Volume I: Unprivileged ISA. Andrew Waterman and Krste Asanović, editors. December 2018. Document Version 20181221-Public-Review-draft. Contributors: Arvind, Krste Asanović, Rimas Avižienis, Jacob Bachmeyer, Christopher F. Batten, Allen J. Baum, Alex Bradbury, Scott Beamer, Preston Briggs, Christopher Celio, Chuanhua Chang, David Chisnall, Paul Clayton, Palmer Dabbelt, Roger Espasa, Shaked Flur, Stefan Freudenberger, Jan Gray, Michael Hamburg, John Hauser, David Horner, Bruce Hoult, Alexandre Joannou, Olof Johansson, Ben Keller, Yunsup Lee, Paul Loewenstein, Daniel Lustig, Yatin Manerkar, Luc Maranget, Margaret Martonosi, Joseph Myers, Vijayanand Nagarajan, Rishiyur Nikhil, Jonas Oberhauser, Stefan O'Rear, Albert Ou, John Ousterhout, David Patterson, Christopher Pulte, Jose Renau, Colin Schmidt, Peter Sewell, Susmit Sarkar, Michael Taylor, Wesley Terpstra, Matt Thomas, Tommy Thorn, Caroline Trippel, Ray VanDeWalker, Muralidaran Vijayaraghavan, Megan Wachs, Andrew Waterman, Robert Watson, Derek Williams, Andrew Wright, Reinoud Zandijk, and Sizhuo Zhang.

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

Model validation

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.

Sail integration

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:

  • ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS. Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell. In POPL 2019.

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

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.

Directory structure

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