In a previous post, we used litmus7 to generate source code and run litmus tests on hardware. However, in certain cases, a user might need to control more than just that the instructions that execute within a standalone application.
litmus7
In addition to generating application-level source code as before, we can use litmus7 to control several aspects of the system software. For example, of particular interest to the memory model are the implications of address translation to execution of applications. In such cases, litmus7 can generate tests with full control of the translation tables and how the Memory Management Unit handles virtual addresses translation and protection. Such functionality requires access to instructions and memory that are typically available to the operating system that runs in a higher Exception Level (EL1).
The litmus7 tool can also generate the sources for a binary that runs as a Virtual Machine (VM). As a result, litmus7 can control the code that executes EL0 as well as in EL1 and control services such as memory allocation and therefore virtual address translation.
To run litmus tests in a VM, litmus7 builds on kvm-unit-tests [1]. The kvm-unit-tests project was originally intended to test the Kernel-based Virtual Machine (KVM) [2] features, and litmus7 uses its basic functionality to encapsulate litmus tests into small operating systems. By doing that, we can control and make changes to functionality that typically would be provided by an operating system running in EL1. For example, the test sets up and control translation tables, the Memory Management Unit (MMU) and any device that we make available to the VM.
The following instructions have been tested on Ubuntu 18.04. However, the concepts are similar for other Linux distributions and operating systems with support for Virtual Machines.
https://github.com/herd/herdtools7/tree/KVM
You need to have essential build tools installed as well as QEMU. In Ubuntu 18.04 you can install these dependencies by executing:
sudo apt install build-essential qemu-system-arm
Also your user needs to have permissions to run VMs using KVM and typically that can be achieved by making sure that your user is a member of the kvm Unix group:
kvm
sudo usermod -a -G kvm ${USER}
First, we first need to download a copy of the kvm-unit-tests and configure it in our system. We can fetch the latest copy of kvm-unit-tests using the following link:https://gitlab.com/kvm-unit-tests/kvm-unit-tests/-/archive/master/kvm-unit-tests-master.tar.gz
And extract the files from the compressed tarball:
tar xzvf kvm-unit-tests-master.tar.gz && cd kvm-unit-tests-master
Finally, we need to build the source code in kvm-unit-tests:
./configure && make
To test that kvm-unit-tests work in our system, we can simply run:
./run_tests.sh
Which will run the tests which are included by default in kvm-unit-tests. If at least one of them was run successfully we know that our setup is working correctly, and we can move on to next part which is running litmus tests using KVM.
To begin with, we take our traditional MP litmus test and run it inside a VM. We use litmus7 to generate the sources for MP inside a folder in kvm-unit-tests:
mkdir litmus-tests ~/bin/litmus7 -mach kvm-aarch64 -variant precise -o litmus-tests mp.litmus
The litmus7 tool has now produced the sources for the litmus test inside the folder “litmus-tests”. We will then use make and the generated Makefile to produce a binary that we can then run inside a VM:
cd litmus-tests && make && cd ..
In this example, this binary is stored in the file “MP.flat” and resides inside the folder “litmus-tests”. Then we can run the MP inside a VM using the command:
sh ./litmus-tests/run.sh
Which gives the output:
Wed 21 Oct 11:56:20 UTC 2020 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for MP.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% AArch64 MP "PodWW Rfe PodRR Fre" {0:X1=x; 0:X3=y; 1:X1=y; 1:X3=x;} P0 | P1 ; MOV W0,#1 | LDR W0,[X1] ; STR W0,[X1] | LDR W2,[X3] ; MOV W2,#1 | ; STR W2,[X3] | ; exists (1:X0=1 /\ 1:X2=0) Generated assembler #START _litmus_P0 nop mov w3,#1 str w3,[x0] mov w2,#1 str w2,[x1] nop #START _litmus_P1 nop ldr w4,[x1] ldr w5,[x0] nop /usr/bin/qemu-system-aarch64 -nodefaults -machine virt,gic-version=host,accel=kvm -cpu host -device virtio-serial-device -device virtconsole,chardev=ctd -chardev testdev,id=ctd -device pci-testdev -display none -serial stdio -kernel MP/MP.flat -smp 4 -append -q # -initrd /tmp/tmp.g5R4XsS1BN Test MP Allowed Histogram (4 states) 910548:>1:X0=0; 1:X2=0; 56482 :>1:X0=0; 1:X2=1; 38531 *>1:X0=1; 1:X2=0; 994439:>1:X0=1; 1:X2=1; Ok Witnesses Positive: 38531, Negative: 1961469 Condition exists (1:X0=1 /\ 1:X2=0) is validated Hash=211d5b298572012a0869d4ded6a40b7f Cycle=Rfe PodRR Fre PodWW Generator=diycross7 (version 7.54+01(dev)) Com=Rf Fr Orig=PodWW Rfe PodRR Fre Observation MP Sometimes 38531 1961469 Time MP 3.75 Revision 8a99be9348124b52f116a26453a3cf3da5c5fb59, version 7.56+02~dev Command line: /home/niknik01/workspace/mm/herdtools7/_build/litmus/litmus.native -mach kvm-aarch64 -variant precise -o mp mp.litmus Parameters #define SIZE_OF_TEST 5000 #define NUMBER_OF_RUN 200 #define AVAIL 4 /* gcc options: -Wall -std=gnu99 -std=gnu99 -ffreestanding -I $(SRCDIR)/lib -I $(SRCDIR)/libfdt -Wall -Werror -fomit-frame-pointer -Wno-frame-address -fno-pic -no-pie -Wmissing-parameter-type -Wold-style-declaration -Woverride-init -O2 $(call optional-ccopt, -mno-outline-atomics) -pthread */ /* barrier: userfence */ /* launch: changing */ /* affinity: none */ /* alloc: dynamic */ /* memory: direct */ /* stride: 1 */ /* safer: write */ /* preload: random */ /* speedcheck: no */ /* proc used: 4 */ LITMUSOPTS= Wed 21 Oct 11:56:24 UTC 2020
As previously, the generated output, includes the test itself, the generated assembly code, followed by the command used to run the VM:
/usr/bin/qemu-system-aarch64 -nodefaults -machine virt,gic-version=host,accel=kvm -cpu host -device virtio-serial-device -device virtconsole,chardev=ctd -chardev testdev,id=ctd -device pci-testdev -display none -serial stdio -kernel ./litmus-tests/MP.flat -smp 4 -append -q # -initrd /tmp/tmp.yjTA8uEN6k
And the final states of all executions of the MP litmus test as before:
Test MP Allowed Histogram (4 states) 1023984:>1:X0=0; 1:X2=0; 8226 :>1:X0=0; 1:X2=1; 6604 *>1:X0=1; 1:X2=0; 961186:>1:X0=1; 1:X2=1; Ok Witnesses Positive: 6604, Negative: 1993396 Condition exists (1:X0=1 /\ 1:X2=0) is validated
So far, we have only run the MP test again, using a different litmus7 mode. But now we can move on to running tests which do make interesting use of our new capability to run code in EL1. We will first look at how the litmus test syntax is extended to ask questions about scenarios relative to address translation and page tables.
Consider the following variant of the message passing idiom:
AArch64 MP-pte { pte_x=(valid:0,oa:phy_x); 0:X2=pte_x; 0:X1=(valid:1,oa:phy_y); 1:X3=x; y=1; 0:X8=z; 1:X8=z; } P0 | P1; STR X1,[X2] | LDR W7,[X8] ; MOV W7,#1 | L0:LDR W4,[X3]; STR W7,[X8] | ; locations [1:X4;] exists(1:X7=1 /\ fault(P1:L0,x))
There are several new points worth noting:
pte_x =
valid:0,oa:phy_x
phy_x
L0
P1
fault
P1:L0,x
x
In summary, the test MP-pte is describing the following scenario:
pte_x
phy_y
What is P1 to see? In particular, can it be that P1 reads the initial value for pte_x? If that is the case, then the access at L0 on P1 will fault, because the initial value for pte_x is invalid.
We can now run our MP-pte litmus test using the previous instructions, or by calling litmus7 directly. Assuming this test is in the file MP-pte.litmus:
~/bin/litmus7 -mach kvm-aarch64 -variant precise MP-pte.litmus
After executing the test in a VM, we will again see a summary of the final states that were observed.
Wed Oct 21 10:19:09 UTC 2020 %%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for MP-pte.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%% AArch64 MP-pte {pteval_t pte_x=(oa:phy_x, af:1, db:1, dbm:0, valid:0); 0:X2=pte_x; pteval_t 0:X1=(oa:phy_y, af:1, db:1, dbm:0, valid:1); 1:X3=x; y=1; 0:X8=z; 1:X8=z;} P0 | P1 ; STR X1,[X2] | LDR W7,[X8] ; MOV W7,#1 | L0: LDR W4,[X3] ; STR W7,[X8] | ; locations [1:X4;] exists (1:X7=1 /\ fault(P1:L0,x)) Generated assembler #START _litmus_P0 nop str x2,[x1] mov w3,#1 str w3,[x0] nop #START _litmus_P1 nop ldr w5,[x1] 0: ldr w4,[x0] nop /usr/bin/qemu-system-aarch64 -nodefaults -machine virt,gic-version=host,accel=kvm -cpu host -device virtio-serial-device -device virtconsole,chardev=ctd -chardev testdev,id=ctd -device pci-testdev -display none -serial stdio -kernel J/./MP-pte.flat -smp 4 -append -q -r 20k -s 500 # -initrd /tmp/tmp.OCQCGXnK5v Test MP-pte Allowed Histogram (4 states) 332 *>1:X4=0; 1:X7=1; fault(P1:L0,x); 13634195:>1:X4=1; 1:X7=0; 2172395:>1:X4=0; 1:X7=0; fault(P1:L0,x); 4193078:>1:X4=1; 1:X7=1; Ok Witnesses Positive: 332, Negative: 19999668 Condition exists (1:X7=1 /\ fault(P1:L0,x)) is validated Hash=0effe3c5c9512116cdc3770032f132fd Observation MP-pte Sometimes 332 19999668 Faults MP-pte 2172727 P1:2172727 Time MP-pte 57.45 Revision 8a99be9348124b52f116a26453a3cf3da5c5fb59, version 7.56+02~dev Command line: /opt/KVM/bin/litmus7 -mach kvm-aarch64 -variant precise -o J.tar MP-pte.litmus Parameters #define SIZE_OF_TEST 5000 #define NUMBER_OF_RUN 200 #define AVAIL 4 /* gcc options: -Wall -std=gnu99 -std=gnu99 -ffreestanding -I $(SRCDIR)/lib -I $(SRCDIR)/libfdt -Wall -Werror -fomit-frame-pointer -Wno-frame-address -fno-pic -no-pie -Wmissing-parameter-type -Wold-style-declaration -Woverride-init -O2 $(call optional-ccopt, -mno-outline-atomics) -pthread */ /* barrier: userfence */ /* launch: changing */ /* affinity: none */ /* alloc: dynamic */ /* memory: direct */ /* stride: 1 */ /* safer: write */ /* preload: random */ /* speedcheck: no */ /* proc used: 4 */ LITMUSOPTS=-r 20k -s 500 Wed Oct 21 10:20:08 UTC 2020
In general a page table entry value such as pte_x is a tuple (oa, valid, af, db, dbm), where:
oa
valid
af
db
dbm
Those af, db and dbm bits behave as follows.
TCR_ELx.{HA,HD} == {0,0}):
TCR_ELx.HA = 1:
TCR_ELx.{HA,HD} == {1,1}:
The dirty bit corresponds to hardware-level write permissions in page table entries. Hence in the simpler stage 1 case, we have AP[2] == 0b1 for clean, and AP[2] == 0b0 for dirty. The default value for pte_x is (oa:phy_x, valid:1, af:1, db:1, dbm:0). If certain fields are omitted (for example in the initial state or the exists clause), they are assumed to have their default values. We can now specify whether ARMv8.1-TTHM is implemented, and whether TCR_ELx.{HA, HD} are equal to 1, with metadata at the top of the test. By default, none of those are equal to 1.
oa:phy_x
valid:1
af:1
db:1
dbm:0
TCR_ELx.{HA, HD}
For example, consider the following test:
AArch64 LDR-AF TTHM=HA { int x=1; pte_x = (af:0); 0:X2=x; } P0 ; L0: LDR W0,[X2] ; forall 0:X0=1 /\ pte_x=(af:1) /\ ~fault(P0:L0,x)
Here we have a test which assumes that ARMv8.1-TTHM is implemented, and states that TCR_ELx.HA is equal to 1. The initial value for x is 1, and initially the page table entry for x has the Access Flag af set to 0 (since the other values are omitted, this entails that pte_x is valid and points to phy_x).
TCR_ELx.HA
At line L0 the thread P0 does a load of x.
In the final clause, we state that it must always be the case (see keyword “forall”) that:
“forall”
X0
We can also manage attributes that determine Cacheability for memory locations in litmus tests.
In VMSAv8-64 a memory location can be mapped as normal memory or device memory. A memory location in normal memory can have the following attributes:
Write-back
Write-through
Non-cacheable
Which are specified separately for caches in the inner-shareability domain of the PE and the outer Shareability domain of the PE. As an example, a location in normal memory can be Inner Write-through and Outer Write-back.
Inner Write-through
Outer Write-back
A memory location in device memory is always Non-cacheable but in addition it can have the following attributes:
nGnRnE:
nGnRE:
nGRE:
GRE:
Please note this is not an exhaustive and detailed explanation of the Cacheability attributes. For further details, please refer to the ARMv8-A Architecture Reference Manual [4].
By default, litmus7 uses Normal, Inner write-back and Outer write-back for all memory locations. However, we can alter the Cacheability attributes for each location at will. For example, we can change the Cacheability attributes for the locations x and y in the MP litmus test:
Normal
Inner write-back
Outer write-back
AArch64 mp-xWB-yWT { 0 :X1=x ; 0 :X3=y ; 1 :X1=y ; 1 :X3=x ; } P0 | P1 ; MOV W0,#1 | LDR W0,[X1] ; STR W0,[X1] | LDR W2,[X3] ; MOV W2,#1 | ; STR W2,[X3] | ; regions: x: normal inner-write-back outer-write-back, y: normal inner-write-through outer-write-through exists (1:X0=1 /\ 1:X2=0)
The previous litmus test is similar to the traditional MP litmus with the addition of the regions section:
regions
regions: x: normal inner-write-back outer-write-back, y: normal inner-write-through outer-write-through
In the regions section, we have specified memory attributes for x and y. In this example, x is mapped as Normal Memory, Inner Write-back and Outer Write-back and y is mapped as Normal Memory, Inner Write-through and Outer-Write-through.
y
Normal Memory
Inner Write-back
Outer-Write-through
The litmus7 tool generates the code to set these Cacheability attributes before executing the test. We can use the same flow to run the MP-xWB-yWT test:
Wed 21 Oct 12:25:50 BST 2020 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for mp-xWB-yWT.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% AArch64 mp-xWB-yWT {0:X1=x; 0:X3=y; 1:X1=y; 1:X3=x;} P0 | P1 ; MOV W0,#1 | LDR W0,[X1] ; STR W0,[X1] | LDR W2,[X3] ; MOV W2,#1 | ; STR W2,[X3] | ; exists (1:X0=1 /\ 1:X2=0) Generated assembler #START _litmus_P0 nop mov w3,#1 str w3,[x0] mov w2,#1 str w2,[x1] nop #START _litmus_P1 nop ldr w4,[x1] ldr w5,[x0] nop /usr/bin/qemu-system-aarch64 -nodefaults -machine virt,gic-version=host,accel=kvm -cpu host -device virtio-serial-device -device virtconsole,chardev=ctd -chardev testdev,id=ctd -device pci-testdev -display none -serial stdio -kernel ./mp-xWB-yWT/mp-xWB-yWT.flat -smp 4 -append -q # -initrd /tmp/tmp.Df13ZMOkLP Test mp-xWB-yWT Allowed Histogram (4 states) 972907:>1:X0=0; 1:X2=0; 7 :>1:X0=0; 1:X2=1; 673912*>1:X0=1; 1:X2=0; 353174:>1:X0=1; 1:X2=1; Ok Witnesses Positive: 673912, Negative: 1326088 Condition exists (1:X0=1 /\ 1:X2=0) is validated Hash=211d5b298572012a0869d4ded6a40b7f Observation mp-xWB-yWT Sometimes 673912 1326088 Time mp-xWB-yWT 10.18 Revision 2e1f66a892506e3027ac381048928efe3020e120, version 7.56+02~dev Command line: /home/niknik01/workspace/mm/herdtools7/_build/litmus/litmus.native -mach kvm-aarch64 -variant precise -o mp-xWB-yWT mp-xWB-yWT.litmus Parameters #define SIZE_OF_TEST 5000 #define NUMBER_OF_RUN 200 #define AVAIL 4 /* gcc options: -Wall -std=gnu99 -std=gnu99 -ffreestanding -I $(SRCDIR)/lib -I $(SRCDIR)/libfdt -Wall -Werror -fomit-frame-pointer -Wno-frame-address -fno-pic -no-pie -Wmissing-parameter-type -Wold-style-declaration -Woverride-init -O2 $(call optional-ccopt, -mno-outline-atomics) -pthread */ /* barrier: userfence */ /* launch: changing */ /* affinity: none */ /* alloc: dynamic */ /* memory: direct */ /* stride: 1 */ /* safer: write */ /* preload: random */ /* speedcheck: no */ /* proc used: 4 */ LITMUSOPTS= Wed 21 Oct 12:26:02 BST 2020
We thank Mark Rutland for the description of TTHM.
[1] https://github.com/herd/herdtools7/tree/KVM
[2] https://www.linux-kvm.org/page/KVM-unit-tests
[3] https://www.linux-kvm.org/page/Main_Page
[4] https://developer.arm.com/documentation/ddi0487/latest/