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?