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

sel4: thread creation

This commit is contained in:
Norman Feske 2014-10-29 16:07:52 +01:00 committed by Christian Helmuth
parent 9bf7568909
commit 40c48c4538
3 changed files with 232 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -935,4 +935,165 @@ _interfaces/sel4_client.h_ stub code. In the stub code, we find the function
'seL4_Untype_Retype' explained in the manual. This is just another difference
from the master branch.
I decided to proceeed with invoking 'seL4_Untyped_RetypeAtOffset' by
manually specifying its parameters. At this point, I am having a hard time
with wrapping my head around seL4's kernel-resource management, in particular
the CNode addressing. My first attempt looked like this:
! {
! /* I don't really know what I am doing here */
! seL4_Untyped const service = 0x38; /* untyped */
! int const type = seL4_TCBObject;
! int const offset = 0;
! int const size_bits = 0;
! seL4_CNode const root = seL4_CapInitThreadCNode;
! int const node_index = 0;
! int const node_depth = 32;
! int const node_offset = 0x100;
! int const num_objects = 1;
!
! int const ret = seL4_Untyped_RetypeAtOffset(service,
! type,
! offset,
! size_bits,
! root,
! node_index,
! node_depth,
! node_offset,
! num_objects);
! PDBG("seL4_Untyped_RetypeAtOffset returned %d", ret);
! }
I put the individual arguments into named constants instead of directly
supplying them to the function to make their meaning easier to memorize. The
'service' argument refers to one of the untyped memory capabilities reported
by the boot info. This memory will be turned into a thread control block
(TCB). The 'node_offset' is a presumably free capability slot of the root
CScope that is supposed to be free. This is where we want to store the
capability for the newly created thread.
When executing the code, the kernel reports an error like this:
! vm fault on data at address 0x1e8 with status 0x6
! in thread 0xe0189880 at address 0x10002ed
The fault is triggered by the function 'seL4_SetCap', more precisely by the
instruction:
! mov %eax,%gs:0x1e8(,%ecx,4)
It appears that the seL4 bindings rely on a thread-local-storage facility
via GS-relative addressing. When the kernel switches thread contexts, it
loads a segment with a thread-specific memory location. Since, we have not
initialized the GS register with a particular value, we end up addressing
the first page, which is not mapped. The issue could be resolved by
initializing the GS register as follows:
! static inline void init_ipc_buffer()
! {
! asm volatile ("movl %0, %%gs" :: "r"(IPCBUF_GDT_SELECTOR) : "memory");
! }
The IPCBUF_GDT_SELECTOR is defined by the seL4 headers. On the next attempt
to execute the code, we get a much nicer kernel message:
! <<seL4 [decodeUntypedInvocation/136 Te0189880 @100035a]:
! Untyped Retype: Destination cap invalid or read-only.>>
In reality, the message even looks much better - it is in color!
The message tells us that the kernel has actually received our request
for retyping untyped memory but the arguments are still messed up.
The message comes from _src/object/untyped.c_:
! /* Lookup the destination CNode (where our caps will be placed in). */
! if (nodeDepth == 0) {
! nodeCap = extraCaps.excaprefs[0]->cap;
! } else {
! cap_t rootCap = extraCaps.excaprefs[0]->cap;
! lu_ret = lookupTargetSlot(rootCap, nodeIndex, nodeDepth);
! if (lu_ret.status != EXCEPTION_NONE) {
! userError("Untyped Retype: Invalid destination address.");
! return lu_ret.status;
! }
! nodeCap = lu_ret.slot->cap;
! }
Apparently, by specifying the value 32 for the depth argument, we entered
the code path for traversing a CNode tree instead of just inserting a
capability into the root CScope. By changing 'node_depth' to 0, system
call returns successfully:
! int main(): seL4_Untyped_RetypeAtOffset returned 0
Even though the new thread has no valid register set and no defined space,
let us see what happens when we try to start it anyway. This can be done
via the 'seL4_TCB_Resume' call with our just created TCB capability as
argument.
! seL4_TCB_Resume(0x100);
This results into the following exciting output:
! Caught cap fault in send phase at address 0x0
! while trying to handle:
! vm fault on data at address 0x1122 with status 0x6
! in thread 0xe0189880 at address 0x10003a5
! Caught cap fault in send phase at address 0x0
! while trying to handle:
! vm fault on data at address 0x0 with status 0x4
! in thread 0xe0100080 at address 0x0
We see two threads faulting! The main thread faults at our "breakpoint"
0x1122. But there is also another thread, which faults at 0x0. Apparently,
the TCB creation via 'seL4_Untyped_RetypeAtOffset' was successful!
Now, turning the situation into something useful seems like a walk in the
park: We need to allocate a stack for the new thread and set up the initial
program counter and stack pointer of the new thread. At this point, I decide
to give the number 0x100 a proper name SECOND_THREAD_CAP because it will be
repeatedly used.
! enum { SECOND_THREAD_CAP = 0x100 };
Following the manual, we have call 'seL4_TCB_WriteRegisters' and
'seL4_TCB_SetSpace'. The following code snippet allocates the stack for
the new thread on the stack of the main thread, initializes the stack
pointer and program counter of the new thread, assigns the new thread to
the same address space as the main thread, and kicks off the execution of
the new thread.
! long stack[0x1000];
! {
! seL4_UserContext regs;
! Genode::memset(&regs, 0, sizeof(regs));
!
! regs.eip = (uint32_t)&second_thread_entry;
! regs.esp = (uint32_t)&stack[0] + sizeof(stack);
! int const ret = seL4_TCB_WriteRegisters(SECOND_THREAD_CAP, false,
! 0, 2, &regs);
! PDBG("seL4_TCB_WriteRegisters returned %d", ret);
! }
!
! {
! seL4_CapData_t no_cap_data = { { 0 } };
! int const ret = seL4_TCB_SetSpace(SECOND_THREAD_CAP, 0,
! seL4_CapInitThreadCNode, no_cap_data,
! seL4_CapInitThreadPD, no_cap_data);
! PDBG("seL4_TCB_SetSpace returned %d", ret);
! }
!
! seL4_TCB_Resume(SECOND_THREAD_CAP);
The entry function of the new thread is supposed to produce a page fault at
the predefined address 0x2244:
! void second_thread_entry()
! {
! *(int *)0x2244 = 0;
! }
When executing the code, we get the desired result:
! vm fault on data at address 0x1122 with status 0x6
! ...
! vm fault on data at address 0x2244 with status 0x6
From these messages, we can see that both the main thread and the second
thread are faulting at their designated fault addresses.

2
repos/base-sel4/include/sel4/stdint.h
View File

@ -17,7 +17,9 @@
#include <base/fixed_stdint.h>
typedef genode_uint8_t uint8_t;
typedef genode_uint16_t uint16_t;
typedef genode_uint32_t uint32_t;
typedef genode_uint64_t uint64_t;
#ifndef NULL
#define NULL ((void *)0)

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

@ -18,6 +18,7 @@
/* seL4 includes */
#include <sel4/bootinfo.h>
#include <sel4/interfaces/sel4_client.h>
static seL4_BootInfo const *boot_info()
@ -61,6 +62,18 @@ static void dump_boot_info(seL4_BootInfo const &bi)
}
static inline void init_ipc_buffer()
{
asm volatile ("movl %0, %%gs" :: "r"(IPCBUF_GDT_SELECTOR) : "memory");
}
void second_thread_entry()
{
*(int *)0x2244 = 0;
}
extern char _bss_start, _bss_end;
int main()
@ -69,6 +82,62 @@ int main()
dump_boot_info(*bi);
PDBG("set_ipc_buffer");
init_ipc_buffer();
PDBG("seL4_SetUserData");
seL4_SetUserData((seL4_Word)bi->ipcBuffer);
enum { SECOND_THREAD_CAP = 0x100 };
{
seL4_Untyped const service = 0x38; /* untyped */
int const type = seL4_TCBObject;
int const offset = 0;
int const size_bits = 0;
seL4_CNode const root = seL4_CapInitThreadCNode;
int const node_index = 0;
int const node_depth = 0;
int const node_offset = SECOND_THREAD_CAP;
int const num_objects = 1;
int const ret = seL4_Untyped_RetypeAtOffset(service,
type,
offset,
size_bits,
root,
node_index,
node_depth,
node_offset,
num_objects);
PDBG("seL4_Untyped_RetypeAtOffset returned %d", ret);
}
long stack[0x1000];
{
seL4_UserContext regs;
Genode::memset(&regs, 0, sizeof(regs));
regs.eip = (uint32_t)&second_thread_entry;
regs.esp = (uint32_t)&stack[0] + sizeof(stack);
int const ret = seL4_TCB_WriteRegisters(SECOND_THREAD_CAP, false,
0, 2, &regs);
PDBG("seL4_TCB_WriteRegisters returned %d", ret);
}
{
seL4_CapData_t no_cap_data = { { 0 } };
int const ret = seL4_TCB_SetSpace(SECOND_THREAD_CAP, 0,
seL4_CapInitThreadCNode, no_cap_data,
seL4_CapInitThreadPD, no_cap_data);
PDBG("seL4_TCB_SetSpace returned %d", ret);
}
seL4_TCB_Resume(SECOND_THREAD_CAP);
*(int *)0x1122 = 0;
return 0;
}