VMSA extensions are available in the head versions of our tools, see https://github.com/herd/herdtools7.git.
Our complete test base consists in 1332 tests, most of which have been written by hand during model design. Some of the tests have been selected from automatically generated large test bases, because they highlighted specific points of some models.
See here for a more information on what tests actually are, in the context of previous experiments on IBM Power and ARMv7 machines.
Log: Model.
Our model aarch64.cat i written in the specialised Cat language. It is part of head version of the herd7 simulation tool. All tests have been executed as follows:
% herd7 -variant vmsa,fatal ...
Where option -variant vmsa commands virtual-memory aware simulation, and fatal commands test thread stop in case of failing instruction (a.k.a. synchronous exception) — Other options are skip, for returning after the failing instruction, and handled for re-executing the failing instruction).
Setting a timeout of 10 minutes for each test, simulation terminates sucessfully for 1291 tests.
Log: Hardware
Tests are compiled into C source files by the litmus7 tool. Most of our experiments have been performed by using hypervisor support leveraging the existing kvm-unit-tests infrastructure. We have also performed bare-metal execution of those by extending kvm-unit-tests with Extensible Firmware Interface (EFI) support. Some of our extensions have been integrated upstream: configure translation granule and EFI support.
Tests are compiled into C files by using litmus7. For user convenience, we also provide litmus tests as C-files (i.e. the product of applying litmus7 to our test base). Ready-To-Compile tests (also as archive SHIP.tar). Distribution includes a small README file.
The documentation of litmus7 contains instructions on how to
compile and run tests in VMSA mode.
Briefly, given the then many necessary option settings,
configuration options -mach kvm-aarch64, -mach kvm-armv8.1 or -mach kvm-m1, depending upon target machine being ARMv8.0 or ARMv8.1. Moreover, compiled test must be placed into a sub-directory D of the kvm-litmus-tests installation. Tests are then run from the kvm-litmus-tests directory installation with command sh D/run.sh ….
We have run tests over a variety of ARMv8 systems, which we identify by convential machine names:
Our experiment reports mostly consist of tables of results. In such tables, rows correspond to test executions, while columns correspond to model or hardware output. Model output is given as Allow or Forbid, expressing that the executions are either allowed or forbidden by the model; while hardware output is given as counts of observed executions over the total number of runs.
See here for a thorough description of tables, in the context or our ARMv7 experiments