genode/repos/base-sel4/doc/notes.txt

              ==========================================
              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 two things: This notes
document at _doc/_ and the port-description file for downloading the seL4
kernel _(ports/sel4.port)_ accompanied with the corresponding hash file
_(ports/sel4.hash)_.

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
###############################################

At this point, there are two options. We could either start with a very
minimalistic hello-world program that is completely unrelated to Genode. Such
a root-task from scratch could be used to explore the individual system calls
before jumping into Genode. The second option would be to go directly for
a Genode program, which includes a proper C++ runtime and Genode's generic
linker script.

I went for the latter option and created a simple test program at
_base-sel4/src/test/sel4/_. The _target.mk_ file looks as follows:

! TARGET = test-sel4
! SRC_CC = main.cc
! LIBS   = cxx startup

The 'main' function of the _main.cc_ file does no much except for writing
at an illegal (yet known) address:

! int main()
! {
! 	*(int *)0x1122 = 0;
! 	return 0;
! }

When attempting to build the program by issuing 'make test/sel4' from within
our build directory, the build system will attempt to compile the C++ runtime,
which, in turn, depends on a few Genode headers. Some headers are readily
provided by the _base/_ repository but others are expected to be supplied
by the _base-<kernel>_ repository. The compile errors look like this:

!     COMPILE  malloc_free.o
! In file included from repos/base/include/parent/capability.h:17:0,
!                  from repos/base/include/base/env.h:20,
!                  from repos/base/src/base/cxx/malloc_free.cc:17:
! repos/base/include/base/capability.h:21:31:
!   fatal error: base/native_types.h: No such file or directory

For now, we can supply a dummy version of this header, which contain
preliminary type definitions. To see, which types are expected from which
header file, we can take cues from the other _base-<kernel>_ platforms.

At link time, we will observe plenty of undefined references originating
from the startup code. Most of those references concern basic data
structures such as the AVL tree. Normally, those symbols are provided by
the so-called _base-common_ library, which is used both core and non-core
programs. We can take a copy of a _base-common.mk_ file from one of the
other base platforms as a starting point. I decided to go for the version
provided by _base-nova_. With the base-common library present, we can
replace the 'cxx' and 'startup' libs by the base-common library in the
'LIBS' declaration of our test-sel4 program. Because base-common already
depends on both 'cxx' and 'startup', there is no need to specify those
libraries twice.

On the attempt to compile the base-common library, we will stumble over
further missing headers such as _ipc_msgbuf.h_. Here the _base-linux_
version of this file becomes handy because it is free-standing.

When compiling _lock.cc_, the compiler complaints about the missing
_lock_helper.h_ file. This platform-specific file that is internally used by
the lock implementation is normally expected
at _base-<kernel>/src/base/lock/_. For now, just for getting the binary
linked, we provide empty dummies:

! static inline void thread_yield() { }
! static inline void thread_switch_to(Genode::Thread_base *thread_base) { }
! static inline void thread_stop_myself() { }
! 
! static inline bool thread_check_stopped_and_restart(Genode::Thread_base *)
! {
! 	return false;
! }

The next missing piece is the platform-specific implementation of the IPC
API _(ipc/ipc.cc and ipc/pager.cc)_, which are expected to reside at
_base-sel4/src/base/ipc/_. We just take the simplest version of the other
base platforms (in this case _base-codezero/src/base/ipc/) and strip it down
to become mere dummy.

By adding the base-common library, the number of unresolved references
decreased by a great amount. Some functions are still unresolved.
There are many references to 'printf', which is not part of the base-common
library because core uses a different back end (typically a kernel debugger)
than non-core processes (using a session to core's LOG service). Because
our test plays the role of a root task, we can include core's version by
adding 'base/src/base/console/core_printf.cc' as source to our target
description file.

! SRC_CC += base/console/core_printf.cc
! vpath %.cc $(BASE_DIR)/src

The back end of 'core_printf.cc' has to be provided by a header at
_base-sel4/src/base/console/core_console.h_. For now, we just provide
an empty implementation of '_out_char'. To let the compiler find the
header, we need to add the extend the include search path as follows:

! INC_DIR += $(REP_DIR)/src/base/console

For the unresolved references for 'env_context_area_ram_session' and
'env_context_area_rm_session', the following dummy will do:

! #include <ram_session/ram_session.h>
! #include <rm_session/rm_session.h>
!
! namespace Genode {
! 	Rm_session  *env_context_area_rm_session()  { return nullptr; }
! 	Ram_session *env_context_area_ram_session() { return nullptr; }
! }

The remaining pieces of the puzzle is the 'Genode::env()' function, which
is an accessor to the Genode environment. Because the Genode environment does
not exist yet, we provide a dummy 'env' called _mini_env_. Initially, this
implementation of the 'Genode::Env' interface merely returns dummy values
(null pointers and invalid capabilies).

After this step, the test-sel4 target links successfully. To use it as
roottask, we have to modify our _test.run_ script by

# Adding a build step
  ! build { test/sel4 }
# Specifying the test-sel4 binary as boot module so that the our run
  environment includes it in the boot image and appends the file as module
  to the boot-loader configuration.
  ! build_boot_image "test-sel4"

When issuing 'make run/test' now, we get the following messages from the
kernel:

! Detected 1 boot module(s):
!   module #0: start=0x169000 end=0x186754 size=0x1d754
!              name='/genode/test-sel4'
! ELF-loading userland images from boot modules:
!   module #0 for node #0: size=0x27000 v_entry=0x136cc
!                          v_start=0x0 v_end=0x27000
!                          p_start=0x187000 p_end=0x1ae000
! Moving loaded userland images to final location:
!                          from=0x187000 to=0x15e000 size=0x27000
!
! Starting node #0
! Caught cap fault in send phase at address 0x0
! while trying to handle:
! vm fault on data at address 0x9090c3fb with status 0x4
! in thread 0xe0189880 at address 0x314a

Assuming that 'v_start' and 'v_end' stand for the virtual address range
if the loaded binary, those numbers look weird. Normally, Genode binaries
are linked at a much higher address, e.g., 0x1000000. By inspecting the
binary via the readelf commend, it turns out that we haven't yet declared the
link address for the seL4 platform. So its time to introduce a so-called spec
file for the "sel4" build-spec value. The new file _base-sel4/mk/spec-sel4.mk_
will be incorporated into the build process whenever the 'SPEC' declaration of
the build directory has the value "sel4" listed. To define the default link
address for the platform, the file has the following content:

! LD_TEXT_ADDR ?= 0x01000000

When issuing 'make test/sel4 VERBOSE=', we can see the link address specified
at the linker command line. Another look at the binary via readelf confirms
that the location of the text segment looks good now. Re-executing the run
script produces the same result as before though. But the last message is
quite helpful:

! vm fault on data at address 0x0 with status 0x4
! in thread 0xe0189880 at address 0x100312b

The last address lies well within the text segment of our binary. It seems
that the kernel has kicked off the execution of our root task (presumably
at the entry point address as found in the ELF binary). At some point, our
"root task" de-references a null pointer. Given that several of the dummy
functions that we just created, return null pointers, this is hardly a
surprise. So let us have a look how far we have come by inspecting the
fault address 0x100312b using
! objdump -lSd bin/test-sel4 | less
In less, we search for the pattern "100312b". We see that the surrounding
code belongs to the heap implementation ('Heap::_allocate_dataspace'). It
seems that someone is trying to use 'Genode::env()->heap()'. To confirm
this assumption, we can use Qemu's GDB stub to obtain a backtrace. We have
to take the following steps:

# We want to halt the execution at the point where the fault would happen
  instead of triggering a page fault. The easiest way to accomplish that
  is to insert an infinite loop at the right spot. The infinite loop serve
  us as a poor man's break point. In our case, we add a 'for (;;);' statement
  right at the beginning of the '_allocate_dataspace' function in
  _repos/base/src/base/heap/heap.cc_. When re-executing the run script after
  this change, we can see that the fault message won't appear.

# We cancel the execution of the run script and start Qemu manually using
  the command-line arguments that are found in the log output (the message
  "spawn qemu ...". To enable Qemu's GDB stub, we have to append "-s" as
  argument.
  ! qemu-system-i386 -nographic -m 64 -cdrom var/run/test.iso -s

# When qemu is running, we start GDB from another shell (changing to
  our build directory) as follows:
  ! gdb bin/test-sel4 -ex "target remote :1234"

# Listing the backtrace via the 'bt' command is quite revealing (output
  slightly edited for brevity):

  ! (gdb) bt
  ! #0  Genode::Heap::_allocate_dataspace
  !     at genode/repos/base/src/base/heap/heap.cc:57
  ! #1  0x010030b9 in Genode::Heap::_unsynchronized_alloc
  !     at genode/repos/base/src/base/heap/heap.cc:181
  ! #2  0x01003155 in Genode::Heap::alloc
  !     at genode/repos/base/src/base/heap/heap.cc:199
  ! #3  0x01010732 in malloc
  ! #4  0x0100f539 in start_fde_sort
  ! #5  init_object
  !     at ../../../../../../contrib/gcc-4.7.2/libgcc/unwind-dw2-fde.c:768
  ! #6  search_object
  !     at ../../../../../../contrib/gcc-4.7.2/libgcc/unwind-dw2-fde.c:958
  ! #7  0x01010375 in _Unwind_Find_registered_FDE
  !     at ../../../../../../contrib/gcc-4.7.2/libgcc/unwind-dw2-fde.c:1022
  ! #8  _Unwind_Find_FDE
  !     at ../../../../../../contrib/gcc-4.7.2/libgcc/unwind-dw2-fde-dip.c:440
  ! #9  0x0100d4c3 in uw_frame_state_for
  ! #10 0x0100dff8 in uw_init_context_1
  !     at ../../../../../../contrib/gcc-4.7.2/libgcc/unwind-dw2.c:1500
  ! #11 0x0100e3ea in _Unwind_RaiseException
  ! #12 0x01011f51 in __cxa_throw ()
  ! #13 0x01013751 in init_main_thread ()
  !     at genode/repos/base/src/platform/init_main_thread.cc:119
  ! #14 0x010134fe in _start ()
  !     at genode/repos/base/src/platform/x86_32/crt0.s:47

We can see that Genode's startup code tries to throw the first C++ exception.
There is a lengthy comment at the corresponding code portion that explains
the rationale behind throwing an exception right from the startup code.
The exception handling, in particular the stack unwinding) is done by the
GCC support library, which eventually calls 'malloc' to allocate some
backing store for metadata. Genode has no 'malloc' function. But for making
the GCC support library happy (which expects a C runtime to be present), our
Genode-specific C++ support code in the form of the 'cxx' library comes with
a library-local version of malloc _(base/src/base/cxx/malloc_free.cc)_. This
malloc implementation uses a separate 'Genode::Heap' instance. The instance
has an initial capacity of 512 bytes. If the allocations exceed this capacity,
this heap will try to expand using 'env()->ram_session()' as backing store.
This is why the '_allocate_dataspace' function was called. At the current
stage, we don't have an implementation of 'env()->ram_session()'. To work
around this early allocation issue, we can simply increase the capacity of
the 'initial_block', let's say by factor 10. When re-executing the run script
now, '_allocate_dataspace' won't be called. Hence, we execution won't get
stuck in our infinite loop (we can remove the loop either way now). Instead,
we get another null-pointer dereference:

! vm fault on data at address 0x0 with status 0x4
! in thread 0xe0189880 at address 0x1003ab7

The procedure to investigate the reason for this page fault is exactly the
same as for the first one, using objdump, infinite loops, and Qemu's GDB stub.

This time, the null-pointer dereference occurs in
_base/src/base/thread/thread.cc_ on the attempt to allocate so-called
thread context for the main thread. Such thread contexts contain the
stacks and meta data of threads. They are placed in a dedicated virtual
memory area that is manually managed by the process.

For our minimalistic root task, we don't have Genode's address-space
management facilities at our disposal yet. So we have to side-step the
'_alloc_context' function somehow. This can be accomplished by using
custom version of _thread.cc_ instead of the one provided by the _base/_
repository. So we remove _thread.cc_ from the base-common library for now
and add a new _thread.cc_ file to our test-sel4 target. The following
dummy stub will do for now:

! static Thread_base::Context *main_context()
! {
! 	enum { STACK_SIZE = sizeof(long)*4*1024 };
! 
! 	static long buffer[STACK_SIZE/sizeof(long)];
! 
! 	/* the context is located beyond the top of the stack */
! 	addr_t const context_addr = (addr_t)buffer + sizeof(buffer)
! 	                          - sizeof(Thread_base::Context);
! 
! 	Thread_base::Context *context = (Thread_base::Context *)context_addr;
! 	context->stack_base = (addr_t)buffer;
! 	return context;
! }
! 
! Thread_base *Thread_base::myself() { return nullptr; }
! 
! Thread_base::Thread_base(const char *name, size_t stack_size, Type type,
!                          Cpu_session *cpu_session)
! :
! 	_cpu_session(cpu_session), _context(main_context())
! {
! 	strncpy(_context->name, name, sizeof(_context->name));
! 	_context->thread_base = this;
! 
! 	_init_platform_thread(type);
! }
! 
! Thread_base::Thread_base(const char *name, size_t stack_size, Type type)
! : Thread_base(name, stack_size, type, nullptr) { }
! 
! Thread_base::~Thread_base() { _deinit_platform_thread(); }

Genode's startup code will change the stack of the main thread prior calling
the main function. This way, the stack can be placed at a dedicated area of
the virtual address space (thread-context area). By not placing the stack
close to the program image, stack overflows won't silently corrupt data but
trigger a page fault. The code above, however, allocates a dummy context for
the main thread in the BSS segment (the 'buffer' used as backing store for the
context is a static variable). This code above is intended as an interim
solution for the initialization of the main thread only.

When executing our run script again, we will get the following message:

! vm fault on data at address 0x1122 with status 0x6
! in thread 0xe0189880 at address 0x1000190

This message is caused by the main function of our test program! In this
function, we deliberately triggered a fault at the address 0x1122 via
the statement '*(int *)0x1122 = 0;'


Issuing the first system call
#############################

We have successfully started our custom root task but we have not interacted
with the kernel yet. So it is time to take a look at seL4's system-call
interface. The interfaces comes in the form of several header files within
sel4's _libsel4/_ directory. At the first glance, the directory layout looks
straight forward. The generic parts reside in _libsel4/include/_ whereas
the architecture-depending parts are located at _libsel4/arch_include/_.
However, when skimming over the headers, it becomes apparent that some of
them are generated from XML files. Also, some headers are including
a top-level header '<autoconf.h>'.

To make sel4's kernel interface visible to the Genode world, we use a pseudo
library called _platform.mk_. The platform library is built before all other
libraries and targets and thereby gives us a hook to populate the build
directory with a custom include-directory structure. Because the selection of
the kernel-interface header depends on the architecture, we place the
_platform.mk_ file at _lib/mk/x86_32_. To create the platform library, we can
take OKL4's version as a blue print. When the library gets built, the include
directory structure will be created as a side effect. However, we cannot
implement the removal of the _include/_ directory of a side effect of a clean
rule because library description files have no clean rule (the build system
just wipes the respective library directory when cleaning). To complement the
creation of the _include/_ directory structure with a corresponding clean
rule, the _base-sel4/mk/spec-sel4.mk_ file can be extended with such a rule,
which will be globally visible.

The platform library is used as a mere hook to create the include directory
structure within the build directory. To allow a program to actually use
those headers, we'd need to extend the include-search path accordingly.
One way would be to have each target specify the build-directory's local
include path via 'INC_DIR += $(BUILD_BASE_DIR)/include'. To too bad. However,
to make the use of the syscall headers more convenient, we introduce just
another library called _syscall_. The library is solely used for providing
a so-called library-import file to all targets that use the library. The
import file contains the extension of the include-search path. Additionally,
we extend the 'REP_INC_DIR' with the value "include/sel4". This way, we can
place custom headers (such as a version of _autoconf.h_) within one of the
Genode source repositories under _include/sel4/_. Those headers will appear
to be located at the inlude root scope for such targets. Speaking of
_autoconf.h_, this header is expected by some sel4 includes to distinguish
the debug mode from the non-debug mode. As we want to enable the debug
functionality, we supply our version of the _autoconf.h_ file at
_base-sel4/include/sel4/autoconf.h_ with the definition:

! #define SEL4_DEBUG_KERNEL 1

Besides the _autoconf.h_ file, the kernel-interface headers also require
an _stdint.h_ to be present at the include root scope. So we place a version
of this file at _base-sel4/include/sel4/stdint.h_.

! #include <base/fixed_stdint.h>
! 
! typedef genode_uint32_t uint32_t;
! 
! #ifndef NULL
! #define NULL ((void *)0)
! #endif

For trying out the access to the kernel-interface headers, we let our target
use the syscall library by extending the
_target.mk_ file with 'LIBS += syscall'. Then, we change the main program
as follows.

! /* Genode includes */
! #include <util/string.h>
! 
! /* seL4 includes */
! #include <sel4/arch/syscalls.h>
! 
! int main()
! {
! 	char const *string = "\nMessage printed via the kernel\n";
! 	for (unsigned i = 0; i < Genode::strlen(string); i++)
! 		seL4_DebugPutChar(string[i]);
! 
! 	*(int *)0x1122 = 0;
! 	return 0;
! }

Here we see three things. First, we can use Genode's usual utilities such as
the string functions, which is quite convenient. Second, we include one of
seL4 headers. And third, we try to invoke the 'seL4_DebugPutChar' system call
to print a string before triggering the page fault at address 0x1122. Before
we can run the program, through, we just have to overcome yet another problem.
On the attempt to build it, we get the following message:

!     COMPILE  main.o
! In file included from include/sel4/arch/syscalls.h:15:0,
!                  from genode/repos/base-sel4/src/test/sel4/main.cc:18:
! include/sel4/types.h:16:28: fatal error: sel4/types_gen.h: No such file or directory

A look at the top-level _Makefile_ of seL4 reveals that this file is generated
from a "types.bf" file using a python script called _tools/bitfield_gen.py_.
Se we have to add a rule for generating this file to our platform library.

! $(BUILD_BASE_DIR)/include/sel4/types_gen.h: $(LIBSEL4_DIR)/include/sel4/types.bf
! 	$(VERBOSE)python $(LIBSEL4_DIR)/tools/bitfield_gen.py \
! 	                 --environment libsel4 "$<" $@

The next missing header that we stumble over is _assert.h_. So we have to add
a simple version of _assert.h_ to _base-sel4/include/sel4/_. This version
uses Genode's PDBG facility to print error messages, which is, of course, not
expected to work yet.

On the next attempt to build the program, the compilation fails because
of a missing header again:

! In file included from include/sel4/arch/syscalls.h:15:0,
!                  from genode/repos/base-sel4/src/test/sel4/main.cc:18:
! include/sel4/types.h:17:26: fatal error: sel4/syscall.h: No such file or directory

The _libsel4/Makefile_ contains the rule to generate this file. At this point,
I am wondering whether to use this Makefile to add those rules to our
platform library. I decided for the latter because there are not too many
files to generate, I will need to look behind the scenes sooner or later
anyway, and I would need to supply some some additional environment (such
as providing a _common.mk_ file in order to invoke the original Makefile.
The rules for generating headers like _syscall.h_ look similar to the rule
for _types_gen.h_ above.

With _sel4/syscall.h_ in place, we get confronted with another problem:

! include/sel4/arch/syscalls.h: In function ‘void seL4_Send(seL4_CPtr, seL4_MessageInfo_t)’:
! include/sel4/arch/syscalls.h:32:26: error: ‘seL4_GetMR’ was not declared in this scope

Fortunately, this error is simply caused by a missing include directive of
_syscalls.h_. The 'seL4_GetMR' function is provided by _sel4/arch/functions.h_
but this file is never included except for _sel4/sel4.h_. I assume that seL4
users are expected to always include the _sel4/sel4.h_ file instead of
including individual kernel headers. By prepending the include of
'<sel4/arch/functions.h>' to the include of '<sel4/arch/syscalls.h>, the
problem goes away and clears the path for the next one:

! include/sel4/arch/syscalls.h: In function ‘void seL4_DebugPutChar(char)’:
! include/sel4/arch/syscalls.h:478:16: error: ‘seL4_SysDebugPutChar’ was not declared in this scope

This message is accompanied with similar errors for "seL4_SysDebugHalt",
"seL4_SysDebugSnapshot", and "seL4_SysDebugCapIdentify".
A look in the generated _include/sel4/syscall.h_ reveals that those
declarations exists only when building in DEBUG mode. Hence, we need
to add the following line to our _autoconf.h_ file:

! #define DEBUG 1

The next problem is more tricky:

! include/sel4/arch/syscalls.h: In function ‘int main()’:
! include/sel4/arch/syscalls.h:481:6: error: impossible register constraint in ‘asm’

The error refers to the system-call binding for 'seL4_DebugPutChar'. After
twiddling with the asm constraints, it turns out that the error is caused by
the use of an enum value as input argument. The C++ compiler is free to pick
any integer type that it sees fit for representing an enum value. Even though
the seL4 developers use a helper macro (SEL4_FORCE_LONG_ENUM) to force a
certain minimum bit width for the used type, the C++ compiler complains. By
explicitly casting the input argument to 'int', this ambiguity can be resolved
and the compiler becomes happy. Unfortunately, this means that I will have to
patch the system-call bindings to make them fit for the use with C++. But
looking at the bindings, I think that a patch won't be avoidable anyway
because the bindings clobber the EBX register. This means that we won't be
able to use the headers for compiling position-independent code (as is the
case for Genode). For now, we have are not compiling with '-fPIC' enabled but
this issue is clear in front of us.

Patches for the seL4 code will be reside at _base-sel4/src/kernel/_. E.g.,
we just added the current modification of the _syscalls.h_ header by
copying a git diff to the file _base-sel4/src/kernel/syscalls.patch_.
To apply the patch automatically when preparing the seL4 port, we need
to modify the _base-sel4/ports/sel4.port_ file by adding the following
lines:

! PATCHES   := src/kernel/syscalls.patch
! PATCH_OPT := -p1 -d src/kernel/sel4

Since we modified the port-description file, we need to update the
accompanied hash via './tool/ports/update_hash sel4'.

_Edit: After consulting the seL4 mailing list, Adrian Danis pointed out that_
_the actual issue is an off-by-one bug in the SEL4_FORCE_LONG_ENUM macro._
_So instead of explicitly casting all opcodes to integers, the macro_
_can be fixed at one place. Hence, I replaced the syscalls.patch by a_
_macros.patch until the fix appears upstream._

Anyway, after all the steps, our test-sel4 program can be successfully
built. Executing the run script produces the result that we longed for:

! Message printed via the kernel
! Caught cap fault in send phase at address 0x0
! while trying to handle:
! vm fault on data at address 0x1122 with status 0x6
! in thread 0xe0189880 at address 0x10001d8

The first line is produced by our test program. Knowing how to print
characters using the kernel's debug interface, filling out the empty
stub function 'Genode::Core_console::_out_char' in _core_console.h_
is easy. We can replace the main program with this version:

! #include <base/printf.h>
! 
! int main()
! {
! 	PDBG("a message printed via Genode's PDBG");
! 
! 	*(int *)0x1122 = 0;
! 	return 0;
! }

When running it via 'make run/test', it produces the expected result:

! int main(): a message printed via Genode's PDBG


Exploration of the kernel interface
###################################

Now that we have a nice playground in place, it is time to explore the
actual kernel interface step by step. The goal is to get a tangible
feeling for the kernel and to exercise the functionality that is needed
by Genode. Those functionalities are:

* Access to boot information such as the memory layout and the boot modules
* Multi-threading
* Process-local synchronization
* Synchronous inter-process communication between threads
* Address-space creation
* Page-fault handling

At this point, it is useful to take a look at the excellent seL4 reference
manual to learn the concepts behind the kernel interface:

:[http://sel4.systems/Docs/seL4-manual.pdf]:

  seL4 reference manual


Obtaining boot information
==========================

The manual mentions the function 'seL4_GetBootInfo' to obtain a pointer to
a boot-info structure. The function implementation, however, requires a
prior all of 'seL4_InitBootInfo' from the startup code. According to the
manual, the startup code gets the pointer passed in a CPU register. It
presumably registers this pointer via 'seL4_InitBootInfo'. Of course, we
don't want to change Genode's kernel-agnostic startup code by inserting
a call to the 'seL4_InitBootInfo' function. Fortunately, this is not the
first time, Genode has to pick up a register value passed by the kernel to
root task via a CPU register. The startup code already saves the initial
stack pointer, EAX and EDI. The seL4 manual does not state, which register
is used. In the kernel code ('create_initial_thread'), the register is denoted
at "capRegister". A look into _ia32/arch/machine/registerset.h_ reveals that
this register is actually EBX on the x86 architecture. Since EBX is not
saved by Genode's startup code yet, we need to enhance the startup code
a bit to save the initial EBX value in the variable '_initial_bx'.

The boot-info type is declared in _sel4/bootinfo.h_. When including the
header, we have to expand our _sel4/stdint.h_ version by a definition
of 'uint8_t'. Also, the header expects CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS
to be defined. We are just using the kernel's default config value, which
we copy to our _sel4/autoconf.h_ file.

! #define CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS 800

With those changes in place, we can access the boot info with a utility like
this:

! #include <sel4/bootinfo.h>
! 
! static seL4_BootInfo const *boot_info()
! {
! 	extern Genode::addr_t __initial_bx;
! 	return (seL4_BootInfo const *)__initial_bx;
! }

While writing a simple 'dump_boot_info' function, I noticed that some boot-info
fields mentioned in the manual and present on the master branch, have
disappeared in the experimental branch, i.e., 'numDeviceRegions'.

Anyway, the output of 'dump_boot_info' function looks like this:

! --- boot info at 102c000 ---
! ipcBuffer:               102b000
! initThreadCNodeSizeBits: 12
! untyped:                 [38,4d)
!                          [38] [00100000,00107fff]
!                          [39] [00108000,00109fff]
!                          [3a] [001a0000,001bffff]
!                          [3b] [001c0000,001fffff]
!                          [3c] [00200000,003fffff]
!                          [3d] [00400000,007fffff]
!                          [3e] [00800000,00ffffff]
!                          [3f] [01000000,01ffffff]
!                          [40] [02000000,02ffffff]
!                          [41] [03000000,037fffff]
!                          [42] [03800000,03bfffff]
!                          [43] [03c00000,03dfffff]
!                          [44] [03e00000,03efffff]
!                          [45] [03f00000,03f7ffff]
!                          [46] [03f80000,03fbffff]
!                          [47] [03fc0000,03fdffff]
!                          [48] [03fe0000,03feffff]
!                          [49] [03ff0000,03ff7fff]
!                          [4a] [03ff8000,03ffbfff]
!                          [4b] [03ffc000,03ffdfff]
!                          [4c] [00189000,001897ff]


Creating a thread
=================

On seL4, kernel objects are created by turning untyped memory into kernel
memory using the 'seL4_Untype_Retype' function. As a first test. I am going to
manually define the parameters for this function using the information from
the boot info.

But before I can start using this function, we first need to generate some
stub code. We need to generate _sel4/invocation.h_ and its corresponding
_sel4/arch/invocation.h_. The rules in the platform library are quickly added,
taking the seL4 Makefile as inspiration. We also need to generate the
_interfaces/sel4_client.h_ stub code. In the stub code, we find the function
'seL4_Untyped_RetypeAtOffset', which pretty much matches the signature of
'seL4_Untype_Retype' explained in the manual. This is just another difference
from the master branch.