|
|
|
|
@ -0,0 +1,296 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
==========================================
|
|
|
|
|
Notes on porting Genode to the seL4 kernel
|
|
|
|
|
==========================================
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Norman Feske
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This document is a loose collection of notes about the exploration of the
|
|
|
|
|
seL4 and the port of the Genode system to this kernel. The seL4 kernel is
|
|
|
|
|
a modern microkernel jointly developed by NICTA and General Dynamics.
|
|
|
|
|
|
|
|
|
|
:[http://sel4.systems]:
|
|
|
|
|
|
|
|
|
|
Website of the seL4 project
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
A fresh Genode source-code repository
|
|
|
|
|
=====================================
|
|
|
|
|
|
|
|
|
|
Following the convention to host each kernel in its dedicated _base-<kernel>_
|
|
|
|
|
source repository, the seL4-specific code will go to _base-sel4_. This way,
|
|
|
|
|
we can cleanly hold the seL4-specific code apart from generic Genode code.
|
|
|
|
|
|
|
|
|
|
For the start, the new repository will contain three things: This notes
|
|
|
|
|
document at _doc/_, the port-description file for downloading the seL4
|
|
|
|
|
kernel _(ports/sel4.port)_ accompanied with the corresponding hash file
|
|
|
|
|
_(ports/sel4.hash)_, and a bunch of small tests _(src/test/sel4/)_
|
|
|
|
|
|
|
|
|
|
Since seL4 is hosted on GitHub, writing a port-description file is easy.
|
|
|
|
|
We can simply use _base-nova/ports/nova.port_ as a template and adapt it:
|
|
|
|
|
|
|
|
|
|
! LICENSE := GPLv2
|
|
|
|
|
! VERSION := git
|
|
|
|
|
! DOWNLOADS := sel4.git
|
|
|
|
|
!
|
|
|
|
|
! URL(sel4) := https://github.com/seL4/seL4.git
|
|
|
|
|
! # experimental branch
|
|
|
|
|
! REV(sel4) := b6fbb78cb1233aa8549ea3acb90524306f49a8d2
|
|
|
|
|
! DIR(sel4) := src/kernel/sel4
|
|
|
|
|
|
|
|
|
|
There are two branches of seL4. The master branch is the stable branch
|
|
|
|
|
that contains the formally verified version of the kernel. The experimental
|
|
|
|
|
branch contains features that are not yet ready to be included in the
|
|
|
|
|
master branch. Among those features are the support for virtualization.
|
|
|
|
|
To anticipate current developments of the seL4 community, I am going with
|
|
|
|
|
the experimental branch. For the ports file, I pick the commit ID of the
|
|
|
|
|
most recent commit of the experimental branch at the time of porting. Once,
|
|
|
|
|
the _ports/sel4.port_ file is in place, we can generate the matching
|
|
|
|
|
port hash as follows (from the base directory of the Genode source tree):
|
|
|
|
|
|
|
|
|
|
! # create an empty hash file
|
|
|
|
|
! touch repos/base-sel4/ports/sel4.hash
|
|
|
|
|
!
|
|
|
|
|
! # update the hash for the current version of the sel4.port file
|
|
|
|
|
! ./tool/ports/update_hash sel4
|
|
|
|
|
|
|
|
|
|
With the _sel4.port_ file in place, we can download the seL4 kernel via:
|
|
|
|
|
! ./tool/ports/prepare_port sel4
|
|
|
|
|
|
|
|
|
|
After invoking this command, the kernel source will be located at
|
|
|
|
|
_contrib/sel4-<hash>/src/kernel/sel4_.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Building the kernel for the first time
|
|
|
|
|
======================================
|
|
|
|
|
|
|
|
|
|
For getting acquainted with the code base, the README.md file provides a
|
|
|
|
|
good starting point. It seems to contain exactly the information that I need
|
|
|
|
|
at this point. As a first test, I am going to build the kernel for the pc99
|
|
|
|
|
platform using the Genode tool chain. According to the README, the following
|
|
|
|
|
command should work
|
|
|
|
|
|
|
|
|
|
! make TOOLPREFIX=/usr/local/genode-gcc/bin/genode-x86- \
|
|
|
|
|
! ARCH=ia32 PLAT=pc99
|
|
|
|
|
|
|
|
|
|
On the first attempt, the following error occurs:
|
|
|
|
|
|
|
|
|
|
! Traceback (most recent call last):
|
|
|
|
|
! File "./tools/invocation_header_gen.py", line 18, in <module>
|
|
|
|
|
! import tempita
|
|
|
|
|
! ImportError: No module named tempita
|
|
|
|
|
! make: *** [arch/api/invocation.h] Error 1
|
|
|
|
|
|
|
|
|
|
This problem could be easily solved by installing the 'python-tempita'
|
|
|
|
|
package. However, further down the road, the build process stops with
|
|
|
|
|
the following message:
|
|
|
|
|
|
|
|
|
|
! src/arch/ia32/kernel/boot_sys.c:75:26: error: ‘CONFIG_MAX_NUM_IOAPIC’ undeclared here (not in a function)
|
|
|
|
|
! src/plat/pc99/machine/hardware.c: In function ‘maskInterrupt’:
|
|
|
|
|
! src/plat/pc99/machine/hardware.c:36:9: error: implicit declaration of function ‘pic_mask_irq’ [-Werror=implicit-function-declaration]
|
|
|
|
|
! src/plat/pc99/machine/hardware.c:36:9: error: nested extern declaration of ‘pic_mask_irq’ [-Werror=nested-externs]
|
|
|
|
|
|
|
|
|
|
A 'grep' for 'MAX_NUM_IOAPIC' reveals that this definition is normally
|
|
|
|
|
generated by the kernel configuration program as there is a match in
|
|
|
|
|
_src/plat/pc99/Kconfig_. At this point, I am wondering if I am on the wrong
|
|
|
|
|
track altogether. On the seL4 download page, the kernel is mentioned as just
|
|
|
|
|
one of several "projects". But since it is the only one of the list of
|
|
|
|
|
projects that I am actually interested in, I wanted to focus on only this one.
|
|
|
|
|
But apparently, attempts to configure the kernel via 'make menuconfig' are not
|
|
|
|
|
supposed to work if checking out the repository in a free-standing fashion.
|
|
|
|
|
|
|
|
|
|
Sooner or later, I would have to look behind the curtain of the seL4 build
|
|
|
|
|
system. So why not now? Passing 'BUILD_VERBOSE=1 V=1' to 'make' is quite
|
|
|
|
|
helpful in this situation. A look into _include/config.h_ reveals that the
|
|
|
|
|
use of the autoconf-generated header _autoconf.h_ is optional. This is
|
|
|
|
|
nice. So I can leave the kernel-configuration magic out of the loop and just
|
|
|
|
|
manually specify the config definitions at the build command line. After
|
|
|
|
|
a few iterations, I came up with the following command-line arguments:
|
|
|
|
|
|
|
|
|
|
! make TOOLPREFIX=/usr/local/genode-gcc/bin/genode-x86- \
|
|
|
|
|
! ARCH=ia32 PLAT=pc99 BUILD_VERBOSE=1 V=1 \
|
|
|
|
|
! LDFLAGS+=-Wl,-melf_i386 \
|
|
|
|
|
! LDFLAGS+=-nostdlib \
|
|
|
|
|
! LDFLAGS+=-Wl,-nostdlib \
|
|
|
|
|
! CFLAGS+=-m32 \
|
|
|
|
|
! CONFIG_KERNEL_EXTRA_CPPFLAGS+=-DCONFIG_MAX_NUM_IOAPIC=1 \
|
|
|
|
|
! CONFIG_KERNEL_EXTRA_CPPFLAGS+=-DCONFIG_IRQ_IOAPIC=1
|
|
|
|
|
|
|
|
|
|
The 'CONFIG_IRQ_IOAPIC' flag is needed to specify whether the legacy PIC
|
|
|
|
|
or the IOPIC should be used. It is picked up by for conditionally compiling
|
|
|
|
|
the code of _src/plat/pc99/machine/hardware.c_.
|
|
|
|
|
|
|
|
|
|
As the result of the build process, we get a freshly baked 'kernel.elf'
|
|
|
|
|
file.
|
|
|
|
|
|
|
|
|
|
Of course, we don't want Genode users to manually build the kernel in this
|
|
|
|
|
way. So we add a "kernel" target to our _base-sel4_ repository. The kernel
|
|
|
|
|
target comes in the form of a _src/kernel/target.mk_ file and a library
|
|
|
|
|
_lib/mk/x86_32/kernel.mk_. The _target.mk_ file is just a pseudo target
|
|
|
|
|
with a dependency on the _kernel.mk_ library. There may be multiple versions
|
|
|
|
|
of the _kernel.mk_ library. The build-system configuration determines the
|
|
|
|
|
version that is used. E.g., when we set up the build directory for x86_32,
|
|
|
|
|
the _lib/mk/x86_32/kernel.mk_ one will be used. The _kernel.mk_ file looks
|
|
|
|
|
as follows:
|
|
|
|
|
|
|
|
|
|
! SEL4_DIR = $(call select_from_ports,sel4)/src/kernel/sel4
|
|
|
|
|
!
|
|
|
|
|
! ifeq ($(called_from_lib_mk),yes)
|
|
|
|
|
! all: build_kernel
|
|
|
|
|
! endif
|
|
|
|
|
!
|
|
|
|
|
! LINKER_OPT_PREFIX := -Wl,
|
|
|
|
|
!
|
|
|
|
|
! build_kernel:
|
|
|
|
|
! $(VERBOSE)$(MAKE) TOOLPREFIX=$(CROSS_DEV_PREFIX) \
|
|
|
|
|
! ARCH=ia32 PLAT=pc99 \
|
|
|
|
|
! LDFLAGS+=-nostdlib LDFLAGS+=-Wl,-nostdlib \
|
|
|
|
|
! $(addprefix LDFLAGS+=$(LINKER_OPT_PREFIX),$(LD_MARCH)) \
|
|
|
|
|
! $(addprefix CFLAGS+=,$(CC_MARCH)) \
|
|
|
|
|
! CONFIG_KERNEL_EXTRA_CPPFLAGS+=-DCONFIG_MAX_NUM_IOAPIC=1 \
|
|
|
|
|
! CONFIG_KERNEL_EXTRA_CPPFLAGS+=-DCONFIG_IRQ_IOAPIC=1 \
|
|
|
|
|
! SOURCE_ROOT=$(SEL4_DIR) -f$(SEL4_DIR)/Makefile
|
|
|
|
|
|
|
|
|
|
The pseudo target _base-sel4/src/kernel/target.mk_ exists merely for making
|
|
|
|
|
the result from the seL4 build directory visible in the install directory
|
|
|
|
|
_(bin/)_.
|
|
|
|
|
|
|
|
|
|
! TARGET = sel4
|
|
|
|
|
! LIBS = kernel
|
|
|
|
|
!
|
|
|
|
|
! $(INSTALL_DIR)/$(TARGET):
|
|
|
|
|
! $(VERBOSE)ln -sf $(LIB_CACHE_DIR)/kernel/kernel.elf $@
|
|
|
|
|
|
|
|
|
|
Genode's build system works in two stages. At the first (light-weight) stage,
|
|
|
|
|
it merely determines library dependencies. At the second stage, the actual
|
|
|
|
|
build steps are performed. The condition around the 'all' target ensures that
|
|
|
|
|
the 'build_kernel' target will be visited only at the second build stage with
|
|
|
|
|
the current working directory set to the library location and all build
|
|
|
|
|
variables (such as CROSS_DEV_PREFIX) defined. Fortunately, the seL4 build
|
|
|
|
|
system supports out-of-tree builds by defining the SOURCE_ROOT variable.
|
|
|
|
|
|
|
|
|
|
To test drive the kernel target, we first need to create Genode build
|
|
|
|
|
directory prepared for seL4. Later, we will add seL4 support to the regular
|
|
|
|
|
'create_builddir' tool. But for now, it suffices to create one manually:
|
|
|
|
|
|
|
|
|
|
# Create a new directory with an _etc/_ subdirectory.
|
|
|
|
|
|
|
|
|
|
# Add an _etc/specs.conf_ file with the following content:
|
|
|
|
|
! SPECS = sel4 x86_32
|
|
|
|
|
This tells the build system the so-called build specification.
|
|
|
|
|
|
|
|
|
|
# Add an _etc/build.conf_ file with the following content:
|
|
|
|
|
! GENODE_DIR := /path/to/your/genode.git
|
|
|
|
|
! BASE_DIR := $(GENODE_DIR)/repos/base
|
|
|
|
|
! REPOSITORIES := $(GENODE_DIR)/repos/base-sel4 \
|
|
|
|
|
! $(GENODE_DIR)/repos/base
|
|
|
|
|
! CONTRIB_DIR := $(GENODE_DIR)/contrib
|
|
|
|
|
|
|
|
|
|
GENODE_DIR must point to the root of Genode's source tree.
|
|
|
|
|
BASE_DIR is used by the build system to find the build-system scripts.
|
|
|
|
|
The CONTRIB_DIR is needed to enable the build system to find the location
|
|
|
|
|
of the seL4 source code. The 'REPOSITORIES' declaration lists all source
|
|
|
|
|
repositories that should be included in the build. Note that the order
|
|
|
|
|
is important. By listing 'base-sel4' before 'base', we allow 'base-sel4'
|
|
|
|
|
to override the content of the 'base' repository.
|
|
|
|
|
|
|
|
|
|
# Symlink the _<genode-dir>/too/builddir/build.mk_ file to a _Makefile_.
|
|
|
|
|
! ln -s <genode-dir>/tool/builddir/build.mk Makefile
|
|
|
|
|
|
|
|
|
|
With the build directory, we can trigger the kernel build via 'make kernel'.
|
|
|
|
|
The seL4 build process will be invoked from within the kernel library. Hence,
|
|
|
|
|
the library's directory _var/libcache/kernel_ will be used as the build
|
|
|
|
|
directory of the kernel.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Starting the kernel in Qemu
|
|
|
|
|
===========================
|
|
|
|
|
|
|
|
|
|
To test-drive the kernel, we need to create a bootable image including a boot
|
|
|
|
|
loader, the boot-loader configuration, and the kernel. To spare us the
|
|
|
|
|
manual work, Genode comes with a so-called run tool that automates this
|
|
|
|
|
procedure. We merely need to create run environment for seL4 to tweak the
|
|
|
|
|
run tool for this particular platform. The run environment for seL4 resides at
|
|
|
|
|
_base-sel4/run/env_. To create it, we can take inspiration from the run
|
|
|
|
|
environments of the other platforms such as NOVA. It comes down to
|
|
|
|
|
implementing the functions 'build_boot_image' and 'run_genode_until' according
|
|
|
|
|
to our needs. The former function contains the generation of the boot-loader
|
|
|
|
|
configuration, i.e., GRUB's _menu.lst_ file. At the current stage, we merely
|
|
|
|
|
load the seL4 ELF image as multi-boot kernel. For using the run tool for the
|
|
|
|
|
initial test, the following small run script at _base-sel4/run/test.run_ does
|
|
|
|
|
the trick:
|
|
|
|
|
|
|
|
|
|
! create_boot_directory
|
|
|
|
|
! build_boot_image ""
|
|
|
|
|
! append qemu_args " -nographic -m 64 "
|
|
|
|
|
! run_genode_until forever
|
|
|
|
|
|
|
|
|
|
To invoke it, all we have to do is issuing 'make run/test' from the build
|
|
|
|
|
directory. All we see, however, is, well, nothing.
|
|
|
|
|
|
|
|
|
|
Normally we would expect from the kernel to print a life sign when booting
|
|
|
|
|
up. This is suggested by a 'printf' in _arch/arm/kernel/boot.c_. So the lack
|
|
|
|
|
of output is most certainly a configuration issue. A look in
|
|
|
|
|
_include/plat/pc99/plat/machine/io.h_ indicates that 'kernel_putchar', which
|
|
|
|
|
is used as the back end of 'printf' _(src/machine/io.c)_ is compiled in only
|
|
|
|
|
if DEBUG mode is enabled. Adding 'DEBUG=1' to the sel4 build command (in our
|
|
|
|
|
_lib/mk/x86_32/kernel.mk_ file) enables this mode.
|
|
|
|
|
|
|
|
|
|
But enabling the DEBUG option comes with a strange surprise. The kernel build
|
|
|
|
|
would fail with the following error:
|
|
|
|
|
|
|
|
|
|
! kernel.o: In function `insert_dev_p_reg':
|
|
|
|
|
! kernel_final.c:(.boot.text+0x131a): undefined reference to `putchar'
|
|
|
|
|
|
|
|
|
|
The message is strange because the seL4 source code is void of any call to
|
|
|
|
|
'putchar'. It turned out that the compiler automatically turned a 'printf'
|
|
|
|
|
with a one-character string ("/n") into a call of 'putchar'. Fortunately,
|
|
|
|
|
this built-in heuristic can be disabled by passing '-fno-builtin-printf'
|
|
|
|
|
to the CFLAGS when compiling seL4. With this fix, we can successfully compile
|
|
|
|
|
the kernel in debug mode, boot it in Qemu, and observe the first life sign:
|
|
|
|
|
|
|
|
|
|
! Boot config: parsing cmdline '/sel4'
|
|
|
|
|
! Boot config: console_port of node #0 = 0x3f8
|
|
|
|
|
! Boot config: debug_port of node #0 = 0x3f8
|
|
|
|
|
! Boot config: max_num_nodes = 1
|
|
|
|
|
! Boot config: num_sh_frames = 0x0
|
|
|
|
|
! seL4 failed assertion '_ndks_end - _ndks_start <= NDKS_SIZE'
|
|
|
|
|
! at src/arch/ia32/kernel/boot_sys.c:424 in function try_boot_sys
|
|
|
|
|
|
|
|
|
|
The NDKS section apparently contains those parts of the image that should
|
|
|
|
|
always be mapped at the upper part of the virtual address space. The assertion
|
|
|
|
|
triggers because the section of the binary is larger (40900 bytes) than the
|
|
|
|
|
assumed limit NDKS_SIZE (12288 bytes). According to the linker script
|
|
|
|
|
_(src/plat/pc99/linker.lds)_, the section includes the kernel stack, the BSS,
|
|
|
|
|
and "COMMON" symbols. When looking at the list of those symbols using 'nm |
|
|
|
|
|
sort -n', the 'ksReadyQueues' symbol raises my eyebrows because it is quite
|
|
|
|
|
large (32768 bytes) compared to all others. This symbol belongs to an array,
|
|
|
|
|
which is dimensioned as CONFIG_NUM_DOMAINS * CONFIG_NUM_PRIORITIES. As we are
|
|
|
|
|
using the default configuration values of _include/config.h_,
|
|
|
|
|
CONFIG_NUM_DOMAINS is 16 and CONFIG_NUM_PRIORITIES is 256. Hence, the array
|
|
|
|
|
has 4096 entries with 8 bytes for each entry ('tcb_queue_t' with two
|
|
|
|
|
pointers). Interestingly, the default value of NUM_DOMAINS in the _Kconfig_ is
|
|
|
|
|
1, which would result in a much smaller 'ksReadyQueues' array. In fact,
|
|
|
|
|
passing the following argument to the kernel build fixes the assertion:
|
|
|
|
|
|
|
|
|
|
! CONFIG_KERNEL_EXTRA_CPPFLAGS+=-DCONFIG_NUM_DOMAINS=1
|
|
|
|
|
|
|
|
|
|
Now, the kernel bootstraps successfully, detects one CPU and tries to
|
|
|
|
|
obtain information about the boot modules, which we don't have provided yet.
|
|
|
|
|
Hence, the kernel backs out with the following message:
|
|
|
|
|
|
|
|
|
|
! Boot loader did not provide information about boot modules
|
|
|
|
|
! seL4 called fail at src/arch/ia32/kernel/boot_sys.c:711
|
|
|
|
|
! in function boot_sys, saying "boot_sys failed for some reason :(
|
|
|
|
|
|
|
|
|
|
Well, this is expected. So it is time to take the first baby step of providing
|
|
|
|
|
a root task to the system.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
A root task for exercising the kernel interface
|
|
|
|
|
===============================================
|
|
|
|
|
|
|
|
|
|
|
Norman Feske
Christian Helmuth