This directory contains patches for the OKL4 kernel version 2.1.1-patch.9.
:'syscall_pic.patch':
The original distribution of the OKL4 kernel comes with x86 syscall bindings
that use absolute addressing modes. Therefore, code using L4 syscalls
cannot be compiled as position-independent code (gcc option '-fPIC').
Unfortunately, shared libraries must be compiled as position independent
because the location of such a library's text segment is not known at
compile time. Consequently, L4 syscalls cannot be issued by shared
libraries, which is a severe limitation. The patch fixes the problem
by changing all L4 syscall bindings by removing PIC-incompatible
addressing modes. It does not affect the functionality of the kernel.
:'eabi_build.patch':
The build system of the orignal OKL4 distribution is not prepared to
compile ARM EABI binaries as generated by modern tool chains such as the
Codesourcery GCC. The patch applies the needed changes to the OKL4 build
infrastructure.
:'reply_tid.patch':
The original OKL4 kernel does not report the global thread ID of the
sender to the receiver of an IPC. Instead, the so called "threadhandle"
of the sender thread is provided. This value is the KTCB index of the
thread. It can be used as IPC destination when sending the reply but
is otherwise meaningless to the userland. However, this becomes a
problem when handing page faults because the page-fault handler is not
able to identify the faulting thread - only the faulting space. There
is no way for the pager to lookup the thread context of the faulting
thread with the information of the page-fault message. The patch changes
OKL4 such that the global thread ID of the sender is provided to the
receiver.
:'kdb_reboot.patch':
This patch enables machine reboot from the kernel debugger.
:'char_bit.patch':
This patch resolves the conflict of definitions of 'CHAR_BIT' between
libc and the OKL4 headers. 'CHAR_BIT' is normally defined by the libc
('limits.h') but it also appears in OKL4's 'types.h'. The patch relaxes
the conflict by making 'CHAR_BIT' an enum value rather then a '#define'.
This way, OKL4's headers included into a dedicated 'Okl4' C++ namespace
(as done by Genode) will result in a 'Okl4::CHAR_BIT' name, not causing
trouble with libc headers included by the same compilation unit.
:'gdt_init.patch':
This patch fixes a off-by-one bug that prevents OKL4 from running on
VirtualBox with VT-x disabled. The original kernel calculates the
last segment address in a wrong way, causing a conflict between
GDT and TSS. As a result, VirtualBox stops with a 'GURU_MEDITATION'
error.
:'invalid_opcode_exception_ipc.patch':
When an invalid opcode gets executed, OKL4 switches to the kernel debugger
console instead of sending an exception IPC to the userland. This patch
fixes the problem by removing the code that invokes the debugger console.
:'bda.patch':
This patch reads out the I/O port of the serial device from the BIOS data
area (on x86).
Applying the patches
--------------------
To apply a patch to the OKL4 kernel, use the 'patch' command. First check
the directory given at the header of the patch. It may contain a directory
prefix (such as 'a/'), which does not actually exist. This prefix is usually
generated by the tool used to create the patch. In this case, use the '-p'
option of the patch command. To apply the patch with the first part of the
path stripped, issue the following command (make sure that you changed to
the base directory of the OKL4 kernel):
! patch -p1 < /path/to/syscall_pic.patch
ac6c4682f3