Overview of the different kernels supported by Genode

Linux is used as the default kernel during development. Hence, documentation about using Genode on Linux is provided with the "Getting started" section of the Genode Foundations book.

NOVA is a so called microhypervisor - a modern high-performance capability-based microkernel for the x86 architecture with special support for hardware-based virtualization and IOMMUs. It is the go-to kernel for Genode on PC platforms. It is covered in detail in the "Getting started" and "Under the hood" chapters of the Genode Foundations book.

The so-called hw base platform allows for the execution of Genode directly on ARM and 64-bit x86 hardware platforms without relying on a separate kernel. It is covered in detail in the "Under the hood" chapter of the Genode Founations book.

The seL4 kernel is a modern open-source microkernel developed by Data61 in Sydney. Its biggest appeal stems from the fact that there exists a formal proof of correctness of the kernel code. But besides this assuring attribute, with solid kernel resource management, support for capability-based security, and good performance, it is attractive on technical merits too. Genode supports seL4 on the x86 (32 and 64 bit) and ARM (32 bit) architectures.

Fiasco.OC is a modernized version of the L4/Fiasco kernel as it emerged from the L4/Fiasco code base. However, its kernel interface diverged entirely from the classical L4 API, towards a modern capability-based object-oriented model. Fiasco.OC supports x86_32, x86_64 alongside many ARM-based platforms, facilitates the use of hardware-based virtualization, supports SMP, accounts kernel resources, and implements capability-based security.

L4ka::Pistachio is a BSD-licensed L4 microkernel developed in joint work of the University of Karlsruhe and the DiSy Group of the University of New South Wales. It is the reference implementation of the L4 API version x.2, which is also referred to as L4 version 4. L4ka::Pistachio supports the IA32 and PowerPC CPU architectures. Genode supports L4ka::Pistachio on the 32-bit x86 architecture only.

OKL4 is an abandoned microkernel that used to be available as commercial and Sleepycat-style licensed version. It was developed by Open Kernel Labs and deployed on mobile phones and other embedded devices. Genode supports OKL4 on the 32-bit x86 architecture only.

L4/Fiasco is a GPL-licensed L4 microkernel developed at the University of Technology Dresden. This kernel is optimized for low interrupt latencies. It implements the L4v2 API and supports IA32, AMD64, and ARM. Genode supports L4/Fiasco on the 32-bit x86 architecture only.