ehmry/genode
ehmry/genode
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

sel4: print boot info

Browse Source
This commit is contained in:
Norman Feske 2014-10-16 20:29:41 +02:00 committed by Christian Helmuth
parent 6b9185ab34
commit 52c4dc8ec8
3 changed files with 189 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

122
repos/base-sel4/doc/notes.txt
View File

@ -18,7 +18,7 @@ a modern microkernel jointly developed by NICTA and General Dynamics.
A fresh Genode source-code repository A fresh Genode source-code repository
===================================== #####################################
Following the convention to host each kernel in its dedicated _base-<kernel>_ 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, source repository, the seL4-specific code will go to _base-sel4_. This way,
@ -65,7 +65,7 @@ _contrib/sel4-<hash>/src/kernel/sel4_.
Building the kernel for the first time Building the kernel for the first time
====================================== ######################################
For getting acquainted with the code base, the README.md file provides a 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 good starting point. It seems to contain exactly the information that I need
@ -207,7 +207,7 @@ directory of the kernel.
Starting the kernel in Qemu Starting the kernel in Qemu
=========================== ###########################
To test-drive the kernel, we need to create a bootable image including a boot 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 loader, the boot-loader configuration, and the kernel. To spare us the
@ -291,7 +291,7 @@ a root task to the system.
A root task for exercising the kernel interface A root task for exercising the kernel interface
=============================================== ###############################################
At this point, there are two options. We could either start with a very 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 minimalistic hello-world program that is completely unrelated to Genode. Such
@ -611,7 +611,7 @@ the statement '*(int *)0x1122 = 0;'
Issuing the first system call Issuing the first system call
============================= #############################
We have successfully started our custom root task but we have not interacted 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 with the kernel yet. So it is time to take a look at seL4's system-call
@ -818,3 +818,115 @@ When running it via 'make run/test', it produces the expected result:
! int main(): a message printed via Genode's PDBG ! 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.

22
repos/base-sel4/lib/mk/x86_32/platform.mk
View File

@ -21,14 +21,15 @@ LIBSEL4_DIR := $(call select_from_ports,sel4)/src/kernel/sel4/libsel4
# #
SEL4_ARCH_INCLUDES := objecttype.h types.h bootinfo.h constants.h functions.h \ SEL4_ARCH_INCLUDES := objecttype.h types.h bootinfo.h constants.h functions.h \
pfIPC.h syscalls.h exIPC.h pfIPC.h syscalls.h exIPC.h invocation.h
SEL4_INCLUDES := objecttype.h types.h bootinfo.h errors.h constants.h \ SEL4_INCLUDES := objecttype.h types.h bootinfo.h errors.h constants.h \
messages.h sel4.h benchmark.h types.bf macros.h \ messages.h sel4.h benchmark.h types.bf macros.h \
types_gen.h syscall.h types_gen.h syscall.h invocation.h
SEL4_INCLUDE_SYMLINKS += $(addprefix $(BUILD_BASE_DIR)/include/sel4/, $(SEL4_INCLUDES)) SEL4_INCLUDE_SYMLINKS += $(addprefix $(BUILD_BASE_DIR)/include/sel4/, $(SEL4_INCLUDES))
SEL4_INCLUDE_SYMLINKS += $(addprefix $(BUILD_BASE_DIR)/include/sel4/arch/,$(SEL4_ARCH_INCLUDES)) SEL4_INCLUDE_SYMLINKS += $(addprefix $(BUILD_BASE_DIR)/include/sel4/arch/,$(SEL4_ARCH_INCLUDES))
SEL4_INCLUDE_SYMLINKS += $(BUILD_BASE_DIR)/include/sel4/interfaces/sel4_client.h
SEL4_INCLUDE_DIRS = $(sort $(dir $(SEL4_INCLUDE_SYMLINKS))) SEL4_INCLUDE_DIRS = $(sort $(dir $(SEL4_INCLUDE_SYMLINKS)))
@ -61,5 +62,22 @@ $(BUILD_BASE_DIR)/include/sel4/syscall.h: $(LIBSEL4_DIR)/include/api/syscall.xml
$(VERBOSE)python $(LIBSEL4_DIR)/tools/syscall_header_gen.py \ $(VERBOSE)python $(LIBSEL4_DIR)/tools/syscall_header_gen.py \
--xml $< --libsel4_header $@ --xml $< --libsel4_header $@
$(BUILD_BASE_DIR)/include/sel4/invocation.h: $(LIBSEL4_DIR)/include/interfaces/sel4.xml
$(MSG_CONVERT)$(notdir $@)
$(VERBOSE)python $(LIBSEL4_DIR)/tools/invocation_header_gen.py \
--xml $< --libsel4 --dest $@
$(BUILD_BASE_DIR)/include/sel4/arch/invocation.h: $(LIBSEL4_DIR)/arch_include/ia32/interfaces/sel4arch.xml
$(MSG_CONVERT)arch/$(notdir $@)
$(VERBOSE)python $(LIBSEL4_DIR)/tools/invocation_header_gen.py \
--xml $< --libsel4 --arch --dest $@
SEL4_CLIENT_H_SRC := $(LIBSEL4_DIR)/include/interfaces/sel4.xml \
$(LIBSEL4_DIR)/arch_include/ia32/interfaces/sel4arch.xml
$(BUILD_BASE_DIR)/include/sel4/interfaces/sel4_client.h: $(SEL4_CLIENT_H_SRC)
$(MSG_CONVERT)$(notdir $@)
$(VERBOSE)python $(LIBSEL4_DIR)/tools/syscall_stub_gen.py \
-a ia32 -o $@ $(SEL4_CLIENT_H_SRC)
endif endif

53
repos/base-sel4/src/test/sel4/main.cc
View File

@ -13,10 +13,61 @@
/* Genode includes */ /* Genode includes */
#include <base/printf.h> #include <base/printf.h>
#include <base/stdint.h>
#include <util/string.h>
/* seL4 includes */
#include <sel4/bootinfo.h>
static seL4_BootInfo const *boot_info()
{
extern Genode::addr_t __initial_bx;
return (seL4_BootInfo const *)__initial_bx;
}
static void dump_untyped_ranges(seL4_BootInfo const &bi,
unsigned start, unsigned size)
{
for (unsigned i = start; i < start + size; i++) {
/* index into 'untypedPaddrList' */
unsigned const k = i - bi.untyped.start;
PINF(" [%02x] [%08lx,%08lx]",
i,
(long)bi.untypedPaddrList[k],
(long)bi.untypedPaddrList[k] + (1UL << bi.untypedSizeBitsList[k]) - 1);
}
}
static void dump_boot_info(seL4_BootInfo const &bi)
{
PINF("--- boot info at %p ---", &bi);
PINF("ipcBuffer: %p", bi.ipcBuffer);
PINF("initThreadCNodeSizeBits: %d", (int)bi.initThreadCNodeSizeBits);
PINF("untyped: [%x,%x)", bi.untyped.start, bi.untyped.end);
dump_untyped_ranges(bi, bi.untyped.start,
bi.untyped.end - bi.untyped.start);
PINF("deviceUntyped: [%x,%x)",
bi.deviceUntyped.start, bi.deviceUntyped.end);
dump_untyped_ranges(bi, bi.deviceUntyped.start,
bi.deviceUntyped.end - bi.deviceUntyped.start);
}
extern char _bss_start, _bss_end;
int main() int main()
{ {
PDBG("a message printed via Genode's PDBG"); seL4_BootInfo const *bi = boot_info();
dump_boot_info(*bi);
*(int *)0x1122 = 0; *(int *)0x1122 = 0;
return 0; return 0;