artifact tweaks

.gitignore

@@ -11,3 +11,6 @@ gnu-mcu-eclipse
 *.dyn_o
 *.dyn_hi
 src/verilog/
+/riscv-memory-model/alloy4.2_2015-02-22.jar
+/test/litmus/*.log
+/execution*.als

make-circuit.sh

@@ -3,3 +3,4 @@ cd src
 sed Spec/Decode.hs -i -e 's/.*if supports. iset then result. else.*/-- REDACTED to make clash work/g' \
                       -e 's/.*if bitwidth iset == 64.*/-- REDACTED to make clash work/g'
 stack exec --package clash-ghc -- clash --verilog Platform/Clash.hs
+git checkout -- Spec/Decode.hs

riscv-memory-model/README.md

@@ -1,5 +1,6 @@
-====== IMPORTED FROM https://github.com/daniellustig/riscv-memory-model 
-This repo presents a formalization of the RISC-V memory consistency model.  
+IMPORTED FROM https://github.com/daniellustig/riscv-memory-model
+
+This repo presents a formalization of the RISC-V memory consistency model.
 
 This repo is meant to serve as an upstream for the official RVWMO specification at <https://github.com/riscv/riscv-isa-manual>.
 
@@ -8,3 +9,60 @@ This version of the model is specified in [Alloy](http://alloy.mit.edu).  The IS
 Note: this version of the model does not support mixed-size or misaligned accesses.
 
 More updates likely to follow over time...
+
+-------------
+
+### Documentation for the RiscvMachine instance running RISC-V litmus tests through the HMC model-checking
+
+The following documentation was copied from PR 33:
+
+This PR adds support for running [RISC-V litmus tests](https://github.com/litmus-tests/litmus-tests-riscv) through the HMC model-checking backend. Currently, **only tests with two threads** and **postconditions of the form "exists (X /\ Y /\ ... /\ Z)"** are supported, and it is known to work with all of the [BASIC_2_THREAD](https://github.com/litmus-tests/litmus-tests-riscv/tree/master/tests/non-mixed-size/BASIC_2_THREAD) tests. To run a test, execute the following:
+```
+stack run riscv-mm </path/to/litmus/file>
+```
+The BASIC_2_THREAD tests have been added to the directory `test/litmus/`. This will call my simple compiler (implemented in `LitmusToRiscv.hs`) to translate the litmus specification into a RISC-V assembly file and extract the condition to check, then use `riscv-none-embed-gcc` to compile the assembly file into an ELF file, then run the HMC interpreter over that ELF file. For every valid full execution of a file, it will check whether all of the conditions specified in the litmus file postcondition are met; if so, it will print the alloy file generated by that execution for manual inspection. I also added a script `run_riscv_mm_litmus.sh` to run all the tests and store their output in log files.
+
+The following table summarizes performance and results:
+
+| Test file | Wallclock time | Conditions met? | Expect conditions to be met? |
+|-----------|----------------|-----------------|------------------------------|
+| 2+2W.litmus | 2:52.43 | Yes | Yes |
+| 2+2W+fence.rw.rws.litmus | 3:03.12 | No | No |
+| 2+2W+fence.rw.rw+po.litmus | 2:57.30 | Yes | Yes |
+| LB.litmus | 2:39.31 | Yes | Yes |
+| LB+ctrls.litmus | 2:20.20 | No | No |
+| LB+ctrl+po.litmus | 2:39.62 | Yes | Yes |
+| LB+datas.litmus | 2:22.97 | No | No |
+| LB+data+ctrl.litmus | 2:18.99 | No | No |
+| LB+data+po.litmus | 2:38.70 | Yes | Yes |
+| LB+fence.rw.rws.litmus | 2:40.91 | No | No |
+| LB+fence.rw.rw+ctrl.litmus | 2:12.61 | No | No |
+| LB+fence.rw.rw+data.litmus | 2:25.57 | No | No |
+| LB+fence.rw.rw+po.litmus | 2:44.65 | Yes | Yes |
+| MP.litmus | 0:22.19 | Yes | Yes |
+| MP+fence.rw.rws.litmus | 0:20.80 | No | No |
+| MP+fence.rw.rw+addr.litmus | 0:21.07 | No | No |
+| MP+fence.rw.rw+ctrl.litmus | 0:24.52 | Yes | Yes |
+| MP+fence.rw.rw+po.litmus | 0:24.56 | Yes | Yes |
+| MP+po+addr.litmus | 0:22.40 | Yes | Yes |
+| MP+po+ctrl.litmus | 0:22.42 | Yes | Yes |
+| MP+po+fence.rw.rw.litmus | 0:21.90 | Yes | Yes |
+| R.litmus | 0:50.24 | Yes | Yes |
+| R+fence.rw.rws.litmus | 0:51.41 | No | No |
+| R+fence.rw.rw+po.litmus | 0:48.89 | Yes | Yes |
+| R+po+fence.rw.rw.litmus | 0:51.20 | Yes | Yes |
+| S.litmus | 1:13.26 | Yes | Yes |
+| SB.litmus | 0:22.53 | Yes | Yes |
+| SB+fence.rw.rws.litmus | 0:24.89 | No | No |
+| SB+fence.rw.rw+po.litmus | 0:25.35 | Yes | Yes |
+| S+fence.rw.rws.litmus | 1:13.46 | No | No |
+| S+fence.rw.rw+ctrl.litmus | 0:45.92 | No | No |
+| S+fence.rw.rw+data.litmus | 0:46.18 | No | No |
+| S+fence.rw.rw+po.litmus | 1:11.26 | Yes | Yes |
+| S+po+ctrl.litmus | 0:45.26 | Yes | Yes |
+| S+po+data.litmus | 0:45.40 | Yes | Yes |
+| S+po+fence.rw.rw.litmus | 1:15.50 | Yes | Yes |
+
+Performance is currently limited by the use of SAT4J in the alloy solver, the time taken to start up the JVM for each separate alloy run (can be dozens of alloy runs per litmus test), and the fact that I increased the alloy search depth to 20. One can imagine ways to improve all of these.
+
+The third column indicates whether HMC found an execution satisfying the litmus test postcondition; the fourth column indicates whether the `rmem` (operational) and `herd` (axiomatic) models find an execution satisfying the litmus test postcondition (generated by manual inspection of the [test log files](https://github.com/litmus-tests/litmus-tests-riscv/tree/master/model-results)).

riscv-memory-model/download_alloy.sh

@@ -0,0 +1,3 @@
+#!/bin/sh
+
+curl -# -L -O https://alloytools.org/download/alloy4.2_2015-02-22.jar