diff --git a/repos/base-sel4/doc/notes.txt b/repos/base-sel4/doc/notes.txt new file mode 100644 index 000000000..b7ea36e3f --- /dev/null +++ b/repos/base-sel4/doc/notes.txt @@ -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-_ +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-/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 +! 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 _/too/builddir/build.mk_ file to a _Makefile_. + ! ln -s /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 +=============================================== + + diff --git a/repos/base-sel4/lib/mk/x86_32/kernel.mk b/repos/base-sel4/lib/mk/x86_32/kernel.mk new file mode 100644 index 000000000..df1e85b78 --- /dev/null +++ b/repos/base-sel4/lib/mk/x86_32/kernel.mk @@ -0,0 +1,28 @@ +SEL4_DIR = $(call select_from_ports,sel4)/src/kernel/sel4 + +# +# Execute the kernel build only at the second build stage when we know +# about the complete build settings (e.g., the 'CROSS_DEV_PREFIX') and the +# current working directory is the library location. +# +ifeq ($(called_from_lib_mk),yes) +all: build_kernel +else +all: +endif + +LINKER_OPT_PREFIX := -Wl, + +build_kernel: + $(VERBOSE)$(MAKE) \ + TOOLPREFIX=$(CROSS_DEV_PREFIX) \ + ARCH=ia32 PLAT=pc99 DEBUG=1 V=1 \ + LDFLAGS+=-nostdlib LDFLAGS+=-Wl,-nostdlib \ + $(addprefix LDFLAGS+=$(LINKER_OPT_PREFIX),$(LD_MARCH)) \ + CFLAGS+=-fno-builtin-printf \ + $(addprefix CFLAGS+=,$(CC_MARCH)) \ + CONFIG_KERNEL_EXTRA_CPPFLAGS+=-DCONFIG_MAX_NUM_IOAPIC=1 \ + CONFIG_KERNEL_EXTRA_CPPFLAGS+=-DCONFIG_IRQ_IOAPIC=1 \ + CONFIG_KERNEL_EXTRA_CPPFLAGS+=-DCONFIG_NUM_DOMAINS=1 \ + SOURCE_ROOT=$(SEL4_DIR) -f$(SEL4_DIR)/Makefile + diff --git a/repos/base-sel4/ports/sel4.hash b/repos/base-sel4/ports/sel4.hash new file mode 100644 index 000000000..7c2d6b1ea --- /dev/null +++ b/repos/base-sel4/ports/sel4.hash @@ -0,0 +1 @@ +c538b91d215024f21be14837192141004c9e3561 diff --git a/repos/base-sel4/ports/sel4.port b/repos/base-sel4/ports/sel4.port new file mode 100644 index 000000000..06269f12d --- /dev/null +++ b/repos/base-sel4/ports/sel4.port @@ -0,0 +1,8 @@ +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 diff --git a/repos/base-sel4/run/test.run b/repos/base-sel4/run/test.run new file mode 100644 index 000000000..ff08409cd --- /dev/null +++ b/repos/base-sel4/run/test.run @@ -0,0 +1,7 @@ +create_boot_directory + +build_boot_image "" + +append qemu_args " -nographic -m 64 " + +run_genode_until forever diff --git a/repos/base-sel4/src/kernel/target.mk b/repos/base-sel4/src/kernel/target.mk new file mode 100644 index 000000000..9954b678b --- /dev/null +++ b/repos/base-sel4/src/kernel/target.mk @@ -0,0 +1,5 @@ +TARGET = sel4 +LIBS = kernel + +$(INSTALL_DIR)/$(TARGET): + $(VERBOSE)ln -sf $(LIB_CACHE_DIR)/kernel/kernel.elf $@ diff --git a/tool/run/boot_dir/sel4 b/tool/run/boot_dir/sel4 new file mode 100644 index 000000000..4f08a842b --- /dev/null +++ b/tool/run/boot_dir/sel4 @@ -0,0 +1,37 @@ +## +# Populate directory with binaries on seL4 +# +proc run_boot_dir {binaries} { + # + # Collect contents of the ISO image + # + copy_and_strip_genode_binaries_to_run_dir $binaries + + build { kernel } + exec cp bin/sel4 [run_dir]/sel4 + + if {[have_include "image/iso"] || [have_include "image/disk"]} { + # + # Install isolinux/GRUB files and bender + # + install_iso_bootloader_to_run_dir + + # + # Generate GRUB config file + # + set fh [open "[run_dir]/boot/grub/menu.lst" "WRONLY CREAT TRUNC"] + puts $fh "timeout 0" + puts $fh "default 0" + puts $fh "\ntitle Genode on seL4" + puts $fh " kernel /sel4" + foreach binary $binaries { + if {$binary != "core"} { + puts $fh " module /genode/$binary" } } + close $fh + } + + # + # Build image + # + run_image +}