Re: [seL4] seL4 & camkes questions

About the timer example, the code you provided compiles fine and I can start the application. However, when starting with qemu, there is an error message: "Undelivered IRQ: 0" Is there any workout for it? Thanks! On Sun, Jan 3, 2016 at 6:04 PM, Ihor Kuz wrote:

...

On 4 Jan 2016, at 8:18 am, Anna Lyons wrote:

- How timing is handled? I tried to use nanosleep() from the libc but it seems the syscall/service is not implemented. I also tried the timer example from the sel4 tutorial but when compiling, there is an error (the function timer_handle_irq needs an IRQ as a parameter). Any idea how to fix the example and more information about how time is handled?

...

The kernel does not provide access to time, however we have some user level timers available. The tutorials are currently not up to date, but you can use the function here: https://github.com/seL4/util_libs/blob/master/libplatsupport/include/platsup... to get the irq number to handle (with n=0).

Some more info about this. The tutorial is being updated for the new version of the kernel and libraries. There are some API differences, and timer_handle_irq is one of those. In the meantime you can do one of two things: - use the tutorial with the older version of the kernel and libraries using a snapshot manifest. e.g.: repo init -u https://github.com/seL4-projects/sel4-tutorials-manifest.git -m snapshots/sel4-solutions.devday2.xml - As Anna said, update the call to timer_handle_irq, e.g.: sel4_timer_handle_irq(timer, timer_get_nth_irq(timer->timer, 0));

...

- How capabilities and services are associated? From the example hello-2 in the sel4 tutorial, I see that a capability is declared (with vka_alloc_endpoint(&vka, &ep_object)) but I do not understand how this is associated with the message being sent between both tasks. In other words, how is it possible to associated a capability with a service. When sending or receiving a message (for example, by using seL4_SetMR(0, MSG_DATA);), there is no use of the capability. So, how the kernel can check that the thread can effectively send a message?

seL4_SetMR just sets a message word in the IPC buffer, but does not perform the send. The kernel does this check when seL4_Call, seL4_Send or seL4_NBSend are used and the message will be received by the first thread that waits on the endpoint. For more details please see the manual.

More specifically, in the hello-3 tutorial the line "tag = seL4_Call(ep_cap_path.capPtr, tag);” is where the message is actually being sent, and it refers to the endpoint cap created.

...

I can't answer the following questions, but I'll point someone who can

to them:

...

- About camkes, what are the thread mapping rules. How a component is

transformed into one (or several) sel4 threads? Is there a mapping 1 component = 1 thread or is it possible to have multiple threads per component?

Currently CAmkES creates 1 thread per interface, and 1 thread for the ‘control’ thread (i.e. in a component that is declared with the ‘control’ keyword). What this means is that requests to different interfaces of the same component will be handled concurrently by different threads. Requests to the same interface of a component will be handled sequentially.

...

- How can I find the code generated by camkes? The idl/adl code is ultimately transformed into C code and I was wondering where I could see the code.

It’s in the build/ directory. For example, for hello-camkes-0 on x86 have a look in build/x86/pc99/hello-camkes-0/src/ and browse the various .c files

Ihor

-- Dr. Ihor Kuz Senior Research Engineer | Trustworthy Systems

DATA61 | CSIRO E ihor.kuz@nicta.com.au T + 61 2 8306 0582 Locked Bag 6016, UNSW, Sydney NSW 1466, Australia www.data61.csiro.au

CSIRO’s Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61

...

Cheers, Anna.

On 26/12/2015 10:14 am, Julien Delange wrote:

...

Hello,

First of all, thanks for the help you provided previously. After

...

...

I still do have some questions regarding sel4 and camkes. - About camkes, what are the thread mapping rules. How a component is

...

...

- How can I find the code generated by camkes? The idl/adl code is

...

...

- How the real-time requirements are handled in camkes? For example, how can I specify that a component is executed periodically every XXX ms. Does the ADL supports that? - How can we specify the scheduling constraints? Can we have an ARINC653-like scheduling where every process has a fixed time slice to be executed? Since the behavior of the system can be deduced from the execution time, allocated a fixed time slice also avoid some attacks - About scheduling, what are the policies actually supported? - How timing is handled? I tried to use nanosleep() from the libc but it seems the syscall/service is not implemented. I also tried the timer example from the sel4 tutorial but when compiling, there is an error (the function timer_handle_irq needs an IRQ as a parameter). Any idea how to fix

...

...

- is it possible for the OS to load and launch multiple elf at the same time or other processes must be manually started? - How capabilities and services are associated? From the example hello-2 in the sel4 tutorial, I see that a capability is declared (with vka_alloc_endpoint(&vka, &ep_object)) but I do not understand how this is associated with the message being sent between both tasks. In other words, how is it possible to associated a capability with a service. When sending or receiving a message (for example, by using seL4_SetMR(0, MSG_DATA);),

...

...

- Is there any efforts to support standards such as ARINC653 or MILS? (even experimental) - Is there any significant/big projects that are available online and you would recommend to learn the OS and its associated libraries?

Hope you do not mind such a list of questions! I really enjoy digging into the OS and it seems very interesting.

Thanks for any help/comment.

_______________________________________________ Devel mailing list

Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

The information in this e-mail may be confidential and subject to legal

downloading the virtual machine, everything was fine and I was able to try seL4 and camkes by using the tutorials. Thanks also for making this documentation available publicly, it definitively helps a lot to learn the principles of this operating system. transformed into one (or several) sel4 threads? Is there a mapping 1 component = 1 thread or is it possible to have multiple threads per component? ultimately transformed into C code and I was wondering where I could see the code. the example and more information about how time is handled? there is no use of the capability. So, how the kernel can check that the thread can effectively send a message? professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

...

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel