Devel September 2016

devel@sel4.systems

19 participants
16 discussions

Re: [seL4] General seL4 Kernel Questions
by Kofidoku.Atuah＠data61.csiro.au 13 Sep '16

13 Sep '16

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 kofidoku.atuah(a)data61.csiro.au www.data61.csiro.au CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61 ________________________________

3 2

Re: [seL4] General seL4 Kernel Questions
by Andrew Mine 13 Sep '16

13 Sep '16

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(a)data61.csiro.au> 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 kofidoku.atuah(a)data61.csiro.au > www.data61.csiro.au > > CSIRO's Digital Productivity business unit and NICTA have joined forces to > create digital powerhouse Data61 > ------------------------------ > > >

1 0

General seL4 Kernel Questions
by Andrew Mine 12 Sep '16

12 Sep '16

Hi I need help with some basic questions which I am getting confused of how seL4 is working. I am currently using the tutorials-seL4 branch. 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? 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? 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? 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? I am sorry if the questions are silly, but I am getting confused. Thanks and Regards Andrew Mine

1 0

seL4 GDB
by Chris Guikema 09 Sep '16

09 Sep '16

Hello everyone, DornerWorks has developed a GDB-stub system for the ARMv7 platform (specifically Zynq 7000) that can be found at the following repos: https://github.com/dornerworks/gdbstub-app https://github.com/dornerworks/gdbstub-app-manifest If you have any questions, feel free to ask.

1 0

CAmkES Question
by Chris Guikema 02 Sep '16

02 Sep '16

Hello Ihor, My name is Chris Guikema, and I am an embedded systems engineer at DornerWorks, located in Grand Rapids Michigan. I am currently working on a project that requires the use of the CAmkES system, and I would like some help, if you are willing to. The project is to allow for debugging using CAmkES. The debugging process was successfully implemented in a simple seL4 program by using the init thread to set up an exception thread and setting up the exception endpoint, which was mapped to the init thread. The init thread was then used to implement a bad assembly code, which fired an exception. The exception handler thread was waiting on something to appear at the endpoint, and then grabbed the program counter and the stack of the init thread and sent it to a GDB function, which allowed debugging. My job is to replicate the debugging using CAmkES. However, CAmkES doesn't seem to want the application to utilize any of the seL4 system calls, and I don't believe the application knows its root cspace and vspace, so any attempt to initialize a debug thread and setup an exception endpoint just don't work. What steps do I need to take to 1, set up an endpoint that I could map to the exception endpoint (the simple libraries cause a vm fault), and 2, set up a thread that waits on the application to throw an exception and allow the debugging to occur. Any help you could send me would be appreciated. I look forward to hearing from you. Thanks Chris Guikema

2 1

sel4 as hypervisor
by Horace Blanc 01 Sep '16

01 Sep '16

Hi, I would like to have more information concerning the design of the hypervisor functionality in the sel4 project on ARMv7 architectures. >From what I read (FAQ/announcement from Adrian Danis in this mailing list), sel4 can run an application called VMM which adds that functionality. Here are my questions: 1) Did the design of this functionality require any change in the sel4 microkernel or is it just the VMM in userland that permits it? (what was in the arm_hyp branch that is now in master?) 2) Does this mean that it is a type-2 hypervisor? Do the guest OS run on top of the VMM? 3) How are the virtualization extentions of ARM used? More precisely what runs on the different protection levels (PL0, PL1 and PL2)? 4) To what extent is this hypervisor design pure? Do the guest OS know that it is running on top of seL4? Best, Horace BLANC

2 1

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel September 2016