- Devel - lists.sel4.systems

quesion about TK1 Linux irq
by PX 27 Sep '16

27 Sep '16

Hi, I have questions about the irqs defined for TK1 guest linux. 1. The linux_pt_irqs[] defined in tk1_vmlinux.h lists all the IRQs for I/O devices, but why they are different from TK1 manual? Does seL4 perform some mapping for guest Linux? 2. what 's the Physical address for Ethernet card on TK1 board? Thanks Peng

2 1

Fwd: [Fwd: quesion about TK1 Linux irq]
by Jason.Butler＠data61.csiro.au 27 Sep '16

27 Sep '16

The irq numbers are remapped in: kernel/include/plat/tk1/plat/machine.h Jason ? -------- Forwarded Message -------- From: PX <seawolf.peng(a)gmail.com> To: devel(a)sel4.systems Subject: [seL4] quesion about TK1 Linux irq Date: Mon, 26 Sep 2016 17:38:47 -0400 Hi, I have questions about the irqs defined for TK1 guest linux. 1. The linux_pt_irqs[] defined in tk1_vmlinux.h lists all the IRQs for I/O devices, but why they are different from TK1 manual? Does seL4 perform some mapping for guest Linux? 2. what 's the Physical address for Ethernet card on TK1 board? Thanks Peng _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel

1 0

Why send-only IPC doesn't and shouldn't return a success indicator
by Matt Rice 26 Sep '16

26 Sep '16

Gernot.Heiser wrote: > We have just received this comment on github, which I think merits some explanation: >> There are times when IPC needs to happen, but a sending process cannot wait around for another process to be receiving. seL4_NBSend is basically the system call for this, but it never provides any feedback whether or not IPC took place. ... >This gets me to (2): send-only IPC is the wrong way to solve the problem. > >The above use case is clearly one where info flow is inherently two-way: you send >something and need an acknowledgment of > receipt. This means call-type IPC is the right mechanism, it does exactly that. And on top of that it is more efficient than > separate send-receiver, and avoids (thanks to reply caps) the need to set up a separate reply channel. New to sel4 and the list (so sorry for stuffing up the threading) Couldn't at the expense of an extra notification send, use a notification where the receiver of the notification then should call the then do a non-blocking reply. I didn't see reply being non-blocking described in the manual so please correct me if i am wrong. This only works one party is willing to block correct, and there is no way to short circuit the call if an incoming message could be delivered to the call'ing process before the call can be completed? Although it would seem to take some amount of gymnastics to balance sending and receiving... so if really neither are willing to wait there is always notifications+shared memory?

3 4

Questions about Capability model
by Daniel Wang 21 Sep '16

21 Sep '16

Hi all, I’m new to the capability concept of seL4. Please correct me if I’m wrong. My understand of the capability is that it is a reference to a chunk of memory that allocated for specific purpose. Say if I want to do IPC between two threads A and B, I will need to apply an chunk of memory as endpoint, which give me a capability that I can pass from thread A to thread B is that correct? Also it is ok to assume the message passing mechanism in IPC is a producer-consumer model? The reason I ask it because I’m thinking is it possible for three (or more) threads that need to communicate with each other using the same endpoint, or it has to be paired for each two of those threads to use an endpoint? Thanks -Dan

3 4

developing a Ethernet card server for seL4
by PX 20 Sep '16

20 Sep '16

Hi, all, We want to develop a networking service on top of seL4, which works as a hypervisor, on Jetson TK1. We know that there is source code for lwip under /projects/util_libs/libethdrivers, but there is no support for TK1. We want to know how much effort needed to port the code to TK1 platform? Is it straightforward? Is there any TK1 ethernet driver source code available? Peng

3 3

How to run seL4 as a hypervisor?
by Daniel Wang 19 Sep '16

19 Sep '16

Hi all, Is there any document/tutorial about using seL4 as a hypervisor to running Linux on top? Appreciate for your help. Thanks -Dan

2 1

General Questions
by sixpackgurkenwasser＠use.startmail.com 15 Sep '16

15 Sep '16

Hello, I've got several questions. 1. Is there a simple way to relate a virtual address in the initial threads address space to the corresponding frame cap in the BootInfo? 2. In 8.2.2 of the manual it is stated in that "seL4 provides no way to obtain the physical address of a page from its capability". Isn't that exactly what the GetAddress method of a Page object does(10.4.14)? Cheers, Steve

3 2

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