seL4 what exactly is in the kernel

[Taylor Bioniks]

Like all L4 kernels, it provides basic mechanisms which must be in the
kernel for security reasons. These include low-level interrupt and
exception handlers (which essentially convert these events into IPC
messages to user-level handlers), a notion of address spaces into which you
can map frames (basically an abstraction of page tables), a notion of
kernel-scheduled (and context-switched) threads, a notion of a protection
domain (capability tree) and a communication and synchronisation mechanism
(IPC endpoints). Other L4 kernels have similar abstractions.


Please explain what you mean by notion? Do you mean that it has code to
deal with the user mode memory management and such?


What is different in seL4 is that all memory management is done at user
level. After booting up and allocating and initialising its static data
structures (scheduling queues, the kernel stack and a few globals) the
kernel sets up an initial user address space with a single thread, and
hands it the rights to all remaining memory (in the form of "Untyped"
capabilities). When performing an operation that requires kernel data
structures (eg creating a thread requires creating a thread control block,
TCB) the user has to provide these, by "retyping" some Untyped memory into
a kernel object type. This makes it kernel memory (inaccessible to
userland), but the owner of that memory can always revoke it (revert it to
Untuped, thus nuking the kernel object).

so is the single kernel stack in it's own address space or is it somehow
mapped or shared with other address spaces?



There's a single kernel stack, which is in use whenever kernel code
executes. The terms "kernel mode" or "user mode" make no sense for data -
they refer to the processor mode that is active when particular code is
executing. However, the kernel stack is, of course, a kernel object, only
accessible in kernel mode. While the kernel stack (like the scheduler
queues) is somewhat special, in that it is allocated by the kernel at boot
time, in terms of accessibility it's no different from other "kernel
objects", such as PTs or TCBs, that are allocated by userland.

so kernel objects are stored in this user mode kernel stack?

Okay, so the kernel never actually has a stack in kernel mode, and it never
allocates space for itself does this mean that the kernel does not grow?

And if so does that eliminate the requirement that I've seen on X86
machines where they have 1GB for the kernel and 3GB for the user programs



Final thing is I've been pointed to the university site a few times and
I've been told there are slides with audio on there, however, I can never
find them even after mirroring the site and looking through it. Where might
I find these?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://os.inf.tu-dresden.de/pipermail/l4-hackers/attachments/20140311/2a49fbca/attachment.htm>