sel4test is a test suite for seL4.
First make sure you have set up your machine.
Getting the Code
mkdir sel4test cd sel4test repo init -u https://github.com/seL4/sel4test-manifest.git repo sync ls # kernel/ libs/ projects/ tools/ apps configs Kbuild Kconfig Makefile
This clones the seL4 kernel, the test suite, some libraries used by the tests, and some tools used in the build process. By default, the current master branch of the kernel is cloned. To clone a specific version of the kernel and compatible libraries and tools, replace the
line above with:
repo init -u https://github.com/seL4/sel4test-manifest.git -b refs/tags/9.0.1
In this example we clone version 9.0.1 of the kernel. For more information on version numbers, see ReleaseProcess.
Default make configurations are provided for a number of platforms:
$ ls configs arndale_debug_xml_defconfig inforce_release_xml_defconfig arndale_release_xml_defconfig kzm_debug_xml_clang_defconfig bbone_debug_xml_defconfig kzm_debug_xml_defconfig bbone_release_xml_defconfig kzm_debug_xml_goanna_defconfig beagle_debug_xml_defconfig kzm_release_xml_clang_defconfig beagle_release_xml_defconfig kzm_release_xml_defconfig beagle_simulation_debug_xml_defconfig kzm_release_xml_goanna_defconfig beagle_simulation_release_xml_defconfig kzm_simulation_debug_xml_defconfig goanna-arm-gcc.profile kzm_simulation_release_xml_defconfig ...
To use a specific config:
./.config, and sets up various header files.
You can look at the configuration options using
Alternatively you can use any text editor to change
you change anything you need to rebuild header files with
. It’s advisable also to make clean to clear out anything
already built — the build system does not track as many dependencies as
it ought to.
Useful configuration options
For cross compilation (targeting ARM), you can set the cross compiler triple. This will
typically be arm-linux-gnueabi- or arm-none-eabi-. Do
make menuconfig and look for toolchain-options
Some of the default configurations specify a particular x86 compiler. It is usually safe to set the triple to the empty string when building for x86, if you have a multilib gcc installed.
Fiddling with most of the other configuration options will lead to systems that will either not compile, or not run.
When you’ve configured the system, you can build by doing
make -j libmuslc && make
Currently parallel builds do not work for the whole build, but it is worth using for the C library. The build system does however support ccache if you have it installed.
A more comprehensive overview of the build system is available at BuildSystemAnatomy
We will now build seL4test for ia32, to run on the QEMU simulator.
The makefile provides a target to simulate ia32. Running the following command will run qemu and point it towards the image we just built.
make ia32_simulation_release_xml_defconfig make -j libmuslc && make make simulate-ia32
To exit qemu after the All is well in the universe message that
indicates the test suite has passed, type
ARM - kzm11
Let’s build the test suite for kzm_simulation_debug_xml_defconfig:
make kzm_simulation_debug_xml_defconfig make ls images # sel4test-driver-image-arm-imx31
Run it in qemu:
qemu-system-arm -nographic -M kzm -kernel images/sel4test-driver-image-arm-imx31 ELF-loader started on CPU: ARM Ltd. ARMv6 Part: 0xb36 r1p3 paddr=[82000000..8223001f] ELF-loading image 'kernel' paddr=[80000000..80035fff] vaddr=[f0000000..f0035fff] virt_entry=f0000000 ELF-loading image 'sel4test-driver' ... <testsuite> <testcase classname="sel4test" name="TEST_BIND0001"> Running test BIND0001 (Test that a bound tcb waiting on a sync endpoint receives normal sync ipc and notification notifications.) Test BIND0001 passed <system-out> TEST_BIND0001 </system-out> </testcase> ...
The test suite prints out JUnit-style XML which can be parsed by various tools.
Testing a Customised Kernel
Suppose you’ve got seL4 checked out in
\~/projects/seL4, and sel4test in
\~/tests/sel4test, and you have been making changes on a feature branch of seL4 named
awesome-new-feature. You want to test if your modified kernel
still passes all the tests in sel4test.
cd ~/tests/sel4tests/kernel git remote add feature ~/projects/seL4 git fetch feature git checkout feature/awesome-new-feature cd ..
Now the kernel in sel4test has been changed to your custom kernel. Now just build and run the test suite as above.
Running a subset of the tests
You can use a regular expression to select a subset of
tests. This can be set using Kconfig, or the build shortcut
make select-test TEST=SCHED.*. By default the test suite runs all tests.