Awesome

litmus-tests-riscv

This litmus-tests-riscv repository contains litmus tests for the RISC-V concurrency architecture, as used by members of the RISC-V Memory Model Task Group during the architecture development.

Most of the litmus tests have been automatically generated using the diy test generator from the diy tool suite http://diy.inria.fr; others are hand-written. The tests are in the form used both by that tool suite (which also includes the litmus tool for running tests on hardware and the herd tool for running tests in axiomatic models) and by the rmem tool http://www.cl.cam.ac.uk/users/pes20/rmem, for running tests in operational models.

The tests are distributed subject to the BSD 2-clause licence in LICENCE.

This work has been partly supported by the REMS "Rigorous Engineering of Mainstream Systems" EPSRC Programme Grant, EP/K008528/1, 2013-2020, and by the ERC Advanced Grant ELVER, 789108.

People

These tests were produced by Shaked Flur and Luc Maranget.

Files

LICENCE - Licence
Makefile - For running hardware tests and comparing results (see below)
riscv.cfg - A litmus configuration file (used by Makefile)
README.md - This file
model-results - Results from running the operational ("Flat", in rmem) and axiomatic ("Herd", in herd) models on the tests (see Makefile).
tests - Each test is in a separate .litmus file. Files in sub-folders with a build.sh script were generated by running the script. Files in sub-folders with an X.conf file (and no build.sh script) were generated by running 'diy7 -conf X.conf'.

Comparing the operational and axiomatic model results

To see a comparison, using the mcompare tool from the diy tool suite, of the operational (left) and axiomatic (right) models, do make compare-models.

At present seven tests show up as different between operational and axiomatic models. These tests involve load-reserve and store-conditional to two different locations. The herd tool assumes that different locations are on different cache lines, in which case the store-conditional must fail, while the rmem tool does not build in that assumption, so the store-conditional can either fail or succeed.

To see all the details of a specific test do make show-test TEST=<name> where <name> is a litmus test name (e.g. MP).

Running the tests on hardware

The litmus tool from the diy tool suite can generate a C program that runs each of the litmus tests (incorporated into the C program as embedded assembly) multiple times in an aggressive test harness, when executed on a target RISC-V machine. The program collects the results (the final state for each run of each test) and prints them in a format that can be processed by other tools from the diy tool suite.

To build the diy tool suite and the C program generated by litmus you will need a system with OCaml (4.02.0 or greater), GNU make (3.81 or greater, though this might also work with other versions of make) and gcc. If those are not available on the RISC-V machine on which you intend to run the tests (the target machine), you will need another machine, not necessarily RISC-V, on which they are available (the host machine).

The following sections explain how to run the litmus tests in three scenarios: (NOTE: we have only tested the instructions in the third scenario. If you need help please contact us.)

Building and running on the same (RISC-V) machine: the target RISC-V machine has the diy tool suite, gcc and make installed.
Generating the program on a host machine (compile on the target): the target RISC-V machine has gcc and make installed, but not the diy tool suite. Here you will need another machine that does have the diy tool suite installed.
Cross compilation: the target RISC-V machine does not have gcc or make installed. Here you will need another machine that does have the diy tool suite, make and gcc that can cross-compile for RISC-V.

In the first and third scenarios, for some RISC-V instructions (e.g. amoswap.w.aq.rl), make will check if your gcc supports those instructions. Litmus tests that include unsupported instructions will be excluded from the tests. After running make run-hw-tests ... or make hw-tests ... as described below, the file gcc.excl will list all the litmus test names that were excluded because gcc does not support them. The command grep "#" gcc.excl will show you which instructions were detected as unsupported by gcc.

In addition, if you are following the second scenario, or the target RISC-V machine does not support some instructions (even though gcc does), you can list instructions you want to exclude in the file exclude-instructions (one instruction in each line, lines starting with # are ignored). The command make exclude-instructions will generate the file, if it does not already exists, with all the instructions used by the litmus tests (commented out). After running the first make ... command below, the file instructions.excl will list all the litmus test names that were excluded because they included instructions from exclude-instructions.

Note that running the tests can take a few days and even weeks. The tests run in a few batches. Each batch includes the complete set of tests, but with different harness parameters which increase the chance of observing the full range of behaviours. The first batch is relatively quick (few minutes). The results from this batch will be saved in the file run.test.log. The following batches will take longer time to complete (a few hours each one). The results from each of those batches will be saved in run.<n>.log, where <n> is the batch number.

Building and running on the same (RISC-V) machine

Here we assume the litmus-tests-riscv repository is checked out on the RISC-V machine you intend to run the tests on and the machine has the diy tool suite, make and gcc installed.

To generate the C program, build it, and run it, do make run-hw-tests CORES=<n> [GCC=<gcc>] [-j <m>] where <n> is the number of hardware threads the machine can run (NOTE: this will probably take a few days to complete, though the first log file should be produced within a few minutes). The optional GCC=<gcc> allows you to specify a non-standard gcc path (the default is gcc). The optional -j <m> will use <m> concurrent processes to speed up the compilation (might take a few hours without this option).

After generating and compiling the tests program, make will run it. You should see the log files with the results in hw-tests/.

Generating the program on a host machine (compile on the target)

Here we assume the litmus-tests-riscv repository is checked out on a host machine that has the diy tool suite, and the target RISC-V machine has gcc and make installed.

To generate the C program do make hw-tests-src.tgz CORES=<n> where <n> is the number of hardware threads the target machine can run.

Copy hw-tests-src.tgz to the target RISC-V machine and then do (on the target machine):

$ tar -zxf hw-tests-src.tgz
$ cd hw-tests-src
$ make [GCC=<gcc>] [-j <m>]
...
$ ./run.sh

where <gcc> and <m> are as described in the previous section. (NOTE: run.sh will probably take a few days to complete!)

When the tests are finished run.sh will touch the file "done". Copy all the run.*.log files back to the host, to the directory litmus-tests-riscv/hw-tests (you will need to create it first), and do (on the host) make merge-hw-tests.

Cross compilation

Here we assume the litmus-tests-riscv repository is checked out on a host machine that has the diy tool suite, make and gcc, that can cross-compile for RISC-V, installed. On Ubuntu you can get gcc that is configured to cross-compile for RISC-V like this sudo apt install gcc-riscv64-linux-gnu and using GCC=riscv64-linux-gnu-gcc as explained below.

To generate the C program and build it do make hw-tests CORES=<n> [GCC=<gcc>] [-j <m>] where <n>, <gcc> and <m> are as in the previous sections. Note that <gcc> should cross-compile for RISC-V. If you installed the Ubuntu package gcc-riscv64-linux-gnu this will be riscv64-linux-gnu-gcc. This will produce the directory hw-tests with two files, run.exe and run.sh. Copy those files to the target machine, and run run.sh (on the target machine) (NOTE: run.sh will probably take a few days to complete). When the tests are finished run.sh will touch the file "done". Copy all the run.*.log files back to the host, to the directory hw-tests, and do (on the host) make merge-hw-tests.

Comparing hardware results with the models

After completing the instructions above you can compare the results with the models. But you do not have to wait for all the tests to complete. In the second and third scenarios above simply carry on with the instructions while run.sh is still running (i.e., copy whatever run.*.log files exist and run make merge-hw-tests as instructed above). In the first scenario just run make merge-hw-tests (while make run-hw-tests is still running).

To compare the hardware results with the Flat model do make compare-hw-flat, and to compare with the Herd model do make compare-hw-herd. This will show you the output of mcompare, from the diy tool suite, running on the hardware results (left) and model results (right).

If you see at the end of the output the line "!!! Warning negative differences in: [...]", the hardware has exhibited some behaviour that the model does not allow. This indicates that the hardware is inconsistent with the RISC-V RVWMO memory model.

You are most likely to see the line "!!! Warning positive differences in: [...]". This indicates that the model allows for more behaviour than was exhibited by the hardware. This is to be expected as implementations are unlikely to be as relaxed as the model permits them to be. In addition, it is possible that the test harness just did not trigger the right conditions for a certain behaviour to be exhibited by the hardware.