Genode on the Codezero microkernel

Codezero is a microkernel primarily targeted at ARM-based embedded systems. It is developed by the British company B-Labs.

The Codezero kernel was first made publicly available in summer 2009. The latest version, documentation, and community resources are available at the project website:

As highlighted by the name of the project website, the design of the kernel is closely related to the family of L4 microkernels. In short, the kernel provides a minimalistic set of functionality for managing address spaces, threads, and communication between threads, but leaves complicated policy and device access to user-level components.

Using Genode with Codezero

For using Codezero, please ensure to have Git, SCons, and Python installed as these tools are required for downloading and building the kernel. Furthermore, you will need to install the tool chain for ARM. For instructions on how to download and install the tool chain, please refer to:

To download the Codezero kernel and integrate it with Genode, issue

 make prepare

from the base-codezero/ directory. The Codezero kernel is fully supported by Genode's run mechanism. Therefore, you can run Genode scenarios using Qemu directly from the build directory. For a quick test, let's create a build directory for Codezero on the VersatilePB926 platform using Genode's create_builddir tool:

 <genode-dir>/tool/create_builddir codezero_vpb926 BUILD_DIR=<build_dir>

To execute the graphical Genode demo, change to the new created build directory and issue:

 make run/demo

Characteristics of the kernel

To put Codezero in relation to other L4 kernels, here is a quick summary on the most important design aspects as implemented with the version 0.3, and on how our port of Genode relates to them:

• In the line of the original L4 interface, the kernel uses global name spaces for kernel objects such as threads and address spaces.

• For the interaction between a user thread and the kernel, the concept of user-level thread-control blocks (UTCB) is used. A UTCB is a small thread-specific region in the thread's virtual address space, which is always mapped. Hence the access to the UTCB can never raise a page fault, which makes it perfect for the kernel to access system-call arguments, in particular IPC payload copied from/to user threads. In contrast to other L4 kernels, the location of UTCBs within the virtual address space is managed by the user land.

  On Genode, core keeps track of the UTCB locations for all user threads. This way, the physical backing store for the UTCB can be properly accounted to the corresponding protection domain.

• The kernel provides three kinds of synchronous inter-process communication (IPC): Short IPC carries payload in CPU registers only. Full IPC copies message payload via the UTCBs of the communicating parties. Extended IPC transfers a variable-sized message from/to arbitrary locations of the sender/receiver address spaces. During an extended IPC, page fault may occur.

  Genode solely relies on extended IPC, leaving the other IPC mechanisms to future optimizations.

• The scheduling of threads is based on hard priorities. Threads with the same priority are executed in a round-robin fashion. The kernel supports time-slice-based preemption.

  Genode does not support Codezero priorities yet.

• The original L4 interface leaves open the question on how to manage and account kernel resources such as the memory used for page tables. Codezero makes the accounting of such resources explicit, enables the user-land to manage them in a responsible way, and prevent kernel-resource denial-of-service problems.

• In contrast to the original L4.v2 and L4.x0 interfaces, the kernel provides no time source in the form of IPC timeouts to the user land. A time source must be provided by a user-space timer driver. Genode employs such a timer services on all platforms so that it is not effected by this limitation.

In several ways, Codezero goes beyond the known L4 interfaces. The most noticeable addition is the support for so-called containers. A container is similar to a virtual machine. It is an execution environment that holds a set of physical resources such as RAM and devices. The number of containers and the physical resources assigned to them is static and is to be defined at build time. The code executed inside a container can be roughly classified into two cases. First, there are static programs that require strong isolation from the rest of the system but no classical operating-system infrastructure, for example special-purpose telecommunication stacks or cryptographic functionality of an embedded device. Second, there a kernel-like workload, which use the L4 interface to substructure the container into address spaces, for example a paravirtualized Linux kernel that uses Codezero address spaces to protect Linux processes. Genode runs inside a container and facilitates Codezero's L4 interface to implement its multi-server architecture.

Behind the scenes

The make prepare mechanism checks out the kernel source code from the upstream Git repository to base-codezero/contrib. When building the kernel from within a Genode build directory via make kernel, this directory won't be touched by the Genode build system. Instead, a snapshot of the contrib directory is taken to <build-dir>/kernel/codezero. This is the place where the Codezero configuration and build processes are executed. By working with a build-directory-local snapshot, we ensure that the source tree remains untouched at all times. After having taken the snapshot, the Codezero kernel is configured using a configuration template specific for the hardware platform. The configuration comes in the form of a CML file located at base-codezero/config/. There is one CML file per supported platform named <platform>.cml. The configured Codezero build directory will reside at <build-dir>/kernel/codezero/build/. Finally, the Codezero build system is invoked to build the kernel.

The two stages of building Codezero

The Codezero build system always performs the compilation of the kernel and the so-called containers as well as the integration of all these components into a final ELF image as one operation. When building just the kernel via 'make kernel', the final image will contain the default container0 that comes with the Codezero distribution. For integrating Genode into the final image, the content of the container0 must be replaced by the Genode binaries followed by another execution of kernel/codezero/build.py. Now, the single-image will be re-created, including the Genode binaries. When using Genode's run mechanism, these steps are automated for you. For reference, please review the Codezero run environment at base-codezero/run/env.

By first building the kernel with Codezero's default container (make kernel) and later replacing the container's content with Genode binaries, we optimize the work flow for building Genode components. The kernel is compiled only once, but the (quick) re-linking of the final image is done every time a run script is executed.

In the run environment, you will see that we forcefully remove a file called cinfo.c from the build-directory-local snapshot of the Codezero source tree. This file is generated automatically by the Codezero build system and linked against the kernel. It contains the parameters of the containers executed on the kernel. Because we change the content of container0 each time when executing a run script, those parameter change. So we have to enforce to re-generation of the cinfo.c file.

How Genode ROM modules are passed into the final image

The Codezero build system picks up any ELF files residing the container's directory wheres the file called main.elf is considered to be the roottask (in Codezero speak called pager) of the container. For Genode, main.elf corresponds to the core executable. All other boot modules are merged into an ELF file, which we merely use as a container for these binary data. This ELF file is linked such that it gets loaded directly after the core image (this is how core finds the boot modules). The process of archiving all boot modules into the single ELF file is automated via the base-codezero/tool/gen_romfs tool. In the container's directory, the merged file is called modules.elf.

Adapting the source code of the kernel

For debugging and development you might desire to change the kernel code at times. You can safely do so within the base-codezero/contrib/ directory. When issuing the next make kernel from the Genode build directory, your changes will be picked up. However, when working with run scripts, the kernel is not revisited each time. The kernel gets built only once if the <build-dir>/kernel directory does not exist, yet. If you work on the kernel source tree and wish to conveniently test the kernel with a run script, use

 make kernel run/<run-script>

This way, you make sure to rebuild the kernel prior executing the steps described in the run script.

Tweaking the kernel configuration

The kernel configuration can be tweaked within <build-dir>/kernel/codezero. Just change to this directory and issue ./build.py -C. The next time you build the kernel via make kernel your configuration will be applied. If you want to conserve your custom configuration, just copy the file <build-dir>/kernel/codezero/build/config.cml.

Parameters of vpb926.cml explained

The default configuration for the VersatilePB926 platform as found at base-codzero/config/vpb926.cml is paramaterized as follows:

 0x41000  Pager LMA
 0x100000 Pager VMA

These values are important because they are currently hard-wired in the linker script used by Genode. If you need to adopt these values, make sure to also update the Genode linker script located at base-codezero/src/platform/genode.ld.

 1         Number of Physical Regions
 0x41000   Physical Region 0 Start Address
 0x4000000 Physical Region 0 End Address

We only use 64MB of memory. The physical memory between 0 and 0x41000 is used by the kernel.

 1          Number of Virtual Regions
 0x0        Virtual Region 0 Start Address
 0x50000000 Virtual Region 0 End Address

It is important to choose the end address such that the virtual memory covers the thread context area. The context area is defined at base/include/base/thread.h.

Limitations

At the current stage, the Genode version for Codezero is primarily geared towards the developers of Codezero as a workload to stress their kernel. It still has a number of limitations that would affect the real-world use:

• Because the only platform supported out of the box by the official Codezero source tree is the ARM-based Versatilebp board, Genode is currently tied to this hardware platform.

• The current timer driver at os/src/drivers/timer/codezero/ is a dummy driver that just yields the CPU time instead of blocking. Is is not suitable as time source.

• The PL110 framebuffer driver at os/src/drivers/framebuffer/pl110/ does only support the LCD display as provided by Qemu but it is not tested on real hardware.

• Even though Codezero provides priority-based scheduling, Genode does not allow assigning priorities to Codezero processes, yet.

As always, these limitations will be addressed as needed.

Thanks

We want to thank the main developer of Codezero Bahadir Balban for his great responsiveness to our feature requests and questions. Without his help, the porting effort would have taken much more effort. We hope that our framework will be of value to the Codezero community.