On 8 Mar 2014, at 6:16 , Taylor Bioniks zeitue@gmail.com wrote:
What does the seL4 kernel actually provide in the kernel itself?
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.
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).
I've read through documentation and it seems they just stop before they state exactly what the seL4 kernel does.
The manual actually fairly precisely describes what the kernel does ;-) But I agree, it could do with a somewhat more gentle intro and overview.
I’m happy to take suggestions as to what should go in there, and will try to find some time (or a volunteer) to add it.
So what I'd like to know is what features and components are in the kernel and what is outside of it?
What’s in the kernel is the implementation of the above abstractions. Among others, this requires low-level exception/interrupt/syscall handlers, context-switching code, maintaining kernel data structures (page tables, cap storage, TCBs, IPC message queues, scheduler queues).
Does the kernel have a single kernel stack or multiple kernel stacks and is/are it/they in kernel mode or user mode?
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.
The only way userland can access any memory is by having it mapped into an address space. And the only memory that can be mapped into an address space is memory of type “frame” (i.e. Untyped memory that has been re-typed into Frames).
Are there any good diagrams that show how seL4 works with its user space components?
Have a look at the Week-1 slides of Advanced OS (http://www.cse.unsw.edu.au/~cs9242). They don’t contain the full story, and are meant to come with my audio ;-)
Gernot