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.
Hi Julien,
I've answered the questions I can, I know more about seL4 than CAmkES though:
- 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?
Experimental support for real-time, periodic threads will be released in the coming months for seL4 and CAmkES (we are working on it now). Currently periodic threads can be achieved by using a timer component which threads communicate with in order to sleep.
- 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
This will come with the above real-time extensions.
- About scheduling, what are the policies actually supported?
Currently fixed priority round-robin is the only scheduling policy supported. Other policies can be achieved with a scheduler component. There is also a domain scheduler which allows threads to be placed in isolated domains with fixed length domain timeslices.
- 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).
- is it possible for the OS to load and launch multiple elf at the same time or other processes must be manually started?
Manually, but CAmkES + the capDL loader can also do this for you using user level infrastructure.
- 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.
- Is there any efforts to support standards such as ARINC653 or MILS? (even experimental)
ARINC can be achieved with the domain scheduler in master seL4, however we haven't actually built user level support for it.
- Is there any significant/big projects that are available online and you would recommend to learn the OS and its associated libraries?
To get familiar with the code base, you can do the advanced operating systems project: http://www.cse.unsw.edu.au/~cs9242/15/project/index.shtml I recommend you use sel4test as a guide for use of our libraries: https://github.com/seL4/sel4test-manifest
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? - 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.
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.systemsmailto: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.
On 4 Jan 2016, at 8:18 am, Anna Lyons Anna.Lyons@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/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
Dear Ihor and Anna,
Thanks you so much for your detailed answers. This explains a lot.
Happy new year! On Jan 3, 2016 6:22 PM, "Ihor Kuz" ihor.kuz@nicta.com.au wrote:
On 4 Jan 2016, at 8:18 am, Anna Lyons Anna.Lyons@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/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
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
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.kuz@nicta.com.au wrote:
On 4 Jan 2016, at 8:18 am, Anna Lyons Anna.Lyons@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/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
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
-
Anna Lyons -
Ihor Kuz -
Julien Delange -
Julien Delange