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;'