seL4 what exactly is in the kernel

[Gernot Heiser]

On 12 Mar 2014, at 8:48 , Taylor Bioniks <zeitue at gmail.com> wrote:

>> 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? 

There is an address-space abstraction that allows userland to map frames. It’s essentially an abstraction of a page table: you can insert a mapping frame->page, which is like inserting an entry into a PT. That code is all the kernel does to help userland manage memory. (That part is common across L4 kernels.)

>> 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?

The kernel stack is in the kernel address space (kernel-only mappings, not different from other L4 kernels, or Linux etc). On kernel entry, the kernel mappings become active (effectively the kernel executes in the union of the current user AS plus the kernel-only AS, again, not different from Linux).

>> 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?

Nope. The kernel stack only contains stack frames of kernel functions, it is completely unwound at kernel exit. Kernel objects are global data (after all, they are provided to the kernel by userland retyping some Untyped). Each kernel object has a fixed, global address (it’s physical memory address, i.e. the address of the Untyped it was derived from). Pages 30-31 of http://www.cse.unsw.edu.au/~cs9242/13/lectures/01-introx4.pdf show diagrams of seL4 memory management.

> 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?

Of course it has a stack, that’s what the single the *kernel stack* is. As I said earlier, the stack gets allocated (like kernel static data) at boot time. It is a fixed size – there’s no recursion in the kernel, and a finite number of possible dynamic nestings, so we know how big the stack can grow worst-case.

> 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 

We use the same (much less than 1GiB though), see above.

> 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?

See above link. There’s no audio, though, not sure who said that. There were a few videos of my lectures done a few years ago, but then I talked about different kernels. I don’t think the videos are around anymore.

Gernot

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://os.inf.tu-dresden.de/pipermail/l4-hackers/attachments/20140312/de13d763/attachment.htm>