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 <ihor....@nicta.com.au> wrote: > > > On 4 Jan 2016, at 8:18 am, Anna Lyons <anna.ly...@nicta.com.au> 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/platsupport/timer.h#L165 > 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....@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 > 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. > >> > >> I still do have some questions regarding sel4 and camkes. > >> - 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? > >> - 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. > >> - 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 > the example and more information about how time is handled? > >> - 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);), > there is no use of the capability. So, how the kernel can check that the > thread can effectively send a message? > >> - 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 > 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 >
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
