Hi
Thanks a lot for the responses. It is much clearer now. I will delve a little bit more into this.
Regards Andrew Mine
On Mon, Sep 12, 2016 at 2:07 AM, Kofidoku.Atuah@data61.csiro.au wrote:
Hey, welcome:
- Once the kernel boots, the control is given to a root task which we
define. Does this root task have all permissions and capabilities or do we still need to assign it capabilities?
The root task is given capabilities to all kernel objects , and it has full permissions (Read-write-grant) on all of them -- you needn't do any work to cause the root task to have permissions/control over the initial objects. Just need to read and parse the BootInfo struct that describes how they are laid out in your CSpace.
- Who is in-charge of scheduling or thread suspend (We can start new
threads from root task), is it also responsibility in root task to manage and schedule it? Who is in charge of migrating the tasks, flushing CPUs loading new stack etc?
The kernel handles scheduling in the main, but threads can be suspended as needed by any other thread that has a capability to the TCB of the thread that you want to manage. Mainline seL4 currently doesn't support multicore, so there is no thread migration, and I do not know what form the multicore extensions will take, with regards to CPU affinity configuration as yet. It's not easy to speculate either, since the entire scheduler is going to undergo intrusive changes when the Real Time extensions are released.
- While spawning a new thread? Who allocates virtual memory to it? And
is the virtual memory allocated equal to 4 GB like in linux kernel where all applications get same Virtual Memory size but different mappings?
A new thread is initially a blank TCB -- to associate a virtual address space (VSpace) with it, you'd need to create a VSpace (seL4_Untyped_Retype), and then pass that to the kernel while configuring the TCB (seL4_TCB_Configure). The VSpace is also just a blank page directory, so you have to then create the page tables for the address space, and then create frames to map into the page tables, etc. The VSpace object is a light wrapper around hardware page tables, so yes, they cover a 4GiB address range, but like Linux, seL4 takes up some of that 4GiB for itself.
- What are the default things loaded into Virtual Memory of a thread?
Only the Cspace maybe made available via CNode_mutates? or something else?
Nothing -- the day that comes after the darkest night has the greatest number of possibilities -- or something like that: what I'm trying to say is that because no policy is enforced by the kernel (not even executable format) you have the greatest range of flexibility to do what you want with the new thread's VSpace. When you create a new VSpace there is nothing in it at all.
The only exception is that when the kernel creates the root task's VSpace, it also then goes on to put the bootinfo struct into it, and in addition it allocates a stack and IPC buffer, and expands the root task's ELF image -- this is a special case because the root task is special.
Kofi Doku Atuah Kernel engineer DATA61 | CSIRO E kofidoku.atuah@data61.csiro.au www.data61.csiro.au
CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61