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, <[email protected]> wrote:

> Hey, welcome:
> ​
> > 1) 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.
>
> >2) 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.
>
> >3) 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.
>
> >4) 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 [email protected]
> www.data61.csiro.au
>
> CSIRO's Digital Productivity business unit and NICTA have joined forces to
> create digital powerhouse Data61
> ------------------------------
>
>
>
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel

Reply via email to