Reproduce some experiments

Reproduce some experiments

We have performed many experiments. We here suggest two experiments to be performed on a Linux system: reproducing our main experiment and running our tests on hardware. This will demonstrate tools from the herdtools7 toolbox at work.

Main experiment: comparing model and hardware logs

The shell used in the following instructions is bash.

Requirements

Experiments are reproducible completely on:

A multicore machine, running Linux, the more recent the better.
With opam (The OCaml package manager) installed. OCaml version should be at least 4.05.

Alternatively, we provide a VirtualBox machine with all software and files installed. The machine runs Ubuntu 20.04 and needs to be given at least 4 cores to run properly. The user is joe (password joe). User joe has been granted sudo access. Proceed to step below directly, having changed directory to ${HOME}/Artefact. However, performing the advanced experiment on the virtual machine will likely falsely invalidate our model. The blame is on the virtualisation technology, not on the model, as changing memory types has apparently no effect on the virtual machine.

Instructions

Install this version of the herdtools7 toolbox from its source deposit. Notice that it is important to install a recent version. Instructions for compiling and installing herdtools7 are as follows:
```
opam install dune menhir
tar zxmf herdtools7-7.57-rc2.tar.gz
cd herdtools7-75-rc2
make all install
cd ..
```
The above commands will install the herdtools7 tools in the user home directory, in sub-directories ${HOME}/bin/, ${HOME}/lib/, and ${HOME}/share, which are created if non-existent.
Download the new X86_64 memory model, litmus test sources and consolidated hardware log (Tests and tested hardware are described here.) Unpack the test archive as follows:
```
tar zxmf src.tgz
```
Execute the tests on top of the new memory model:
```
${HOME}/bin/herd7 -cat NEW.cat src/@all > Model
```
Running time should be about one minute.
A warning should appear:
```
Warning: File "src/SB+pontnts.litmus": X86_64Sem.ml: Instruction movntdqa (%rcx),xmm0 not implemented
```
The warning above is normal, as nor herd7, nor Linux kernels, can use the SSE extension of the Intel 64 architecture.
Compare the model log with the hardware log:
```
${HOME}/bin/mcompare7 -pos P -neg N Model Hardware
wc -l P
wc -l N
```
The file P contains “positive” differences, i.e. the names of the tests that exhibit more behaviours on hardware than predicted by model — or invalid behaviours.
```
 0 P
66 N
```
The file P is empty, demonstrating that our model is not invalidated by experiments. Additionally there are only 66 “negative” differences, i.e. only 66 tests some of which behaviours predicted by model are not observed on hardware.
See a more detailed account of the above comparison of model and hardware.

Advanced experiment: running tests on hardware

This advanced experiment consists in running tests on hardware. To that aim one needs (1) a Linux, X86_64 multicore machine, (2) root access, (3) linux headers installed. Linux kernel headers are available as a package (sudo apt install linux-headers on debian/Ubuntu).

One should first check whether the machine implements the clflushopt instruction or not. This is done easily by looking at the /proc/cpuinfo file. If the instruction is implemented, the word clflushopt is present in the file. The complete list of tests is in the file src/@all; while the file src/@noopt lists the tests that do not use the clflushopt instruction. In the following, we use a smaller list of files src/@small so as to eschew important compilation and running times.

We assume a 4 core machine. We shall run the experiment on all the cores. First compile the tests as the source of kernel modules by invoking the klitmus7 tool as follows:

mkdir -p Run
${HOME}/bin/klitmus7 -a 4 -size_of_test 500 -number_of_run 200 -stride 1 -o Run src/@small

(See klitmus7 description in herdtools7 documentation for details on command-line options). Then compile the kernel modules:

cd Run
make -j 16

And run the tests as root:

sudo sh run.sh > LOG.txt

During our experiments we ran tests varying runtime parameters, for instance:

cat <<'EOF' > runall.sh
for i in $(seq 1 8)
do
    sh run.sh size=500 nruns=200 stride=$i > 0$i.txt    
done
EOF

The above runall.sh shell script is to be run as root:

sudo sh runall.sh

The whole experiment should take about ten minutes on a typical machine.

Logs are then summed:

${HOME}/bin/msum7 0?.txt > 0X.txt

And compared with model:

${HOME}/bin/mcompare7 -pos P -neg N ../Model 0X.txt
wc -l P

One can for instance check the absence of invalid behaviour by checking the file P being empty. Such a successful experiment would reinforce our conviction that the model is valid by testing yet another machine.

If the experiment is run on the virtual machine, it may fail, as we have experienced discovering 48 tests that invalidate the model:

 48 P

Nevertheless our model is not to blame, the virtual mschine is: the failure can be explained by the virtual machine not implementing memory type changes. As a matter of facts, virtualization cannot emulate actual machines in every aspect.