- Devel - lists.sel4.systems

handling timer with camkes
by Julien Delange 16 Feb '16

16 Feb '16

Dear all, I would like to build a scheduler on top of camkes. I figure that I have to get access to the timer irq and start from there (e.g. then, dispatch other tasks according to the number of elapsed ticks). I did find some relevant examples, especially in the camkes-vm ( https://github.com/seL4/camkes-vm) but nothing I can try. Is there any information about such materials? I tried to reuse the component but always got build error. I was wondering if there was an existing tutorial or an example I could try that will help me. Thanks. Julien.

2 3

Allocation of untyped memory
by Norman Feske 09 Feb '16

09 Feb '16

Hello, while moving Genode's seL4 support to seL4 version 2, I stumbled over the dynamic allocation within untyped memory regions. In the old experimental branch that I used previously, the retype-untyped operation allowed me to manually specify an offset where the new kernel object should be placed within the untyped memory region. So I was able to manage the allocation of untyped memory manually. In short, I added each initial untyped memory region to a roottask-local "phys-mem" allocator. Each time when creating a kernel object, I asked this allocator for a region of the required size and alignment, determined the untyped-memory capability that belongs to the found region, and used this capability to create the kernel object(s) at the calculated offset within the untyped-memory region. This worked very well. After switching to version 2, I found the retype-untyped operation to lack the offset argument (which admittedly was never present in the non-experimental version). Instead of accepting an offset parameter, the kernel maintains a built-in allocator per untyped-memory region. (please correct me if my understanding is wrong) The allocator is basically a simple offset value ("FreeIndex") that is increased with each allocation. Since I no longer have the chance to specify the offset explicitly, I have to rely on the allocation policy of the kernel and hit the following problem: There exists an untyped memory region of size 0x2000. Initially, the FreeIndex is 0. Now, I am creating the following kernel objects within the untyped-memory region: 1. CNode with totalObjectSize 0x400: -> The allocation increases FreeIndex to 0x400. 2. CNode with totalObjectSize 0x800: -> The FreeIndex gets aligned to 0x800 (natural alignment of the to-be-created CNode). This creates a gap between 0x400 and 0x800. -> The allocation increases FreeIndex to 0x1000. 3. seL4_IA32_4K with a totalObjectSize 0x1000: -> The allocation increases FreeIndex to 0x2000. 4. CNode with totalObjectSize 0x400: <<seL4 [decodeUntypedInvocation/209 T0xe3fc9900 "rootserver" @2013228]: Untyped Retype: Insufficient memory (1 * 1024 bytes needed, 0 bytes available).>> Since FreeIndex equals the size of the untyped memory region, the kernel concludes that untypedFreeBytes is 0. Even though there exists a gap of 0x400 within the untyped memory region that satisfies the alignment of the to-be-created kernel object, the kernel won't allow me to use it. In contrast, with the retype-untyped-at-offset operation, such a situation never occurred. Right now, I am a bit puzzled about how to proceed and have the following questions in the back of me head: * What is the rationale behind fixing the allocation policy within untyped memory regions in the kernel. Doesn't this design contradict with the principle of avoiding policy in the kernel? In my specific case, this policy seemingly makes my life much more difficult. To use the kernel in a deterministic way, I would need to model the kernel's allocation behavior in the user land. * From what I gather from the kernel's source code, the built-in allocator would not allow me to reuse parts of untyped memory regions because 'FreeIndex' is always increasing. E.g., after revoking the CNodes of steps 1 and 2, I still cannot create any new kernel objects within the untyped memory region because FreeIndex remains equal the size of the untyped memory region. Is this correct? * Is it possible to give me the retyped-untyped-at-offset operation back? ;-) e.g., in the form of a patch? Or alternatively, are there any best practices that I could follow wrt managing untyped memory? Maybe I'm just approaching the problem from the wrong angle? Best regards Norman -- Dr.-Ing. Norman Feske Genode Labs http://www.genode-labs.com · http://genode.org Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

3 5

Upgrading to Camkes 2.0
by Jeff Hieb 25 Jan '16

25 Jan '16

I was looking to upgrade to CAmkES release 2.0. but can't get an example arm configuration to compile. I did a a fresh clone using https://github.com/seL4/camkes-manifest.git and found the ia32_simple_defconfig compiles fine, but not arm_simple_defconfig make arm_simple_defconfig make [libs/libsel4] building... make[1]: *** No rule to make target `/home/sysjeff/Camkes2/libs/libsel4/sel4_arch_include/arm/interfaces/sel4arch.xml', needed by `include/interfaces/sel4_client.h'. Stop. make: *** [libsel4] Error 2 looks like the arm directory got renamed to aarch32 and part of the build system doesn't know? $ ls /home/sysjeff/Camkes2/libs/libsel4/sel4_arch_include/ aarch32/ ia32/ Is there something simple I am missing? Thanks, Jeff -- Jeffrey L. Hieb Department of Engineering Fundamentals University of Louisville Louisville Kentucky 40292 (502) 852 0465

2 2

Issue with CAmkES tutorial
by James Hasner 21 Jan '16

21 Jan '16

All, Noticed an issue with the tutorial for creating a dataport application with CAmkES components. This issue is on https://wiki.sel4.systems/CAmkES%20Tutorial within the Makefile and Kbuild section. You titled the application "helloevent" instead of hellodataport, causing the newly created application to not be able to access the header files needed. Thanks, James

2 1

Announcing Robigalia, make seL4 applications with Rust!
by Corey Richardson 06 Jan '16

06 Jan '16

Hi all, On behalf of the Robigalia project I am pleased to announce our first public release of the core libraries for using Rust on seL4. Currently, this consists of a raw interface akin to libsel4 and a higher-level "Rustic" interface. Currently, only x86 is supported. An ARM port is in progress. We have a website: https://robigalia.org/ And a mailing list: https://lists.robigalia.org/listinfo/robigalia-dev The goal of the Robigalia project is to promote Rust as a robust choice for application development on seL4 and has the long-term goal of producing Robigo, a POSIX-compatible personality on seL4. We're in the initial stages of development. We are primarily a group of students from Clarkson University, though other contributors are starting to trickle in. Currently in-progress is a port of the tutorial from the sel4-tutorials repositories and examples of doing various things using the libraries we've created. Beyond those, we're also working on x86 platform support, right now virtio and PCI bus management. (I didn't intend on posting this for another week, to finish the tutorial and high-level library, but it was scooped on HN, so I figured I might as well) -- cmr +16032392210 http://octayn.net/

2 1

Hardware Platform for sel4 and running linux as guest os
by Julien Delange 06 Jan '16

06 Jan '16

Dear all, I am looking to purchase a board for a project that will use sel4. I have the following hardware requirements: - serial port - ethernet - potentially usb Then, I want to run linux on top of sel4 and have also some native components. In the linux partition, I would like to control the usb and potentially the ethernet. In the native components, I am planning to use the serial port (communication with other components). I thought the beagleboard black would be a good match. Does anyone tried to run linux as a guest os on this platform? If yes, is there any tutorial/example to set it up? Also, any information about how to use the serial ports and other hardware components? Also, if you have an experience with any other board (x86 or ARM - the platform does not really matter), is it possible to indicate what you would recommend? Thanks for any help or suggestion, Julien.

6 6

CAmkES 2.0.0
by Ihor Kuz 06 Jan '16

06 Jan '16

The Trustworthy Systems Team at Data61 (formerly NICTA) is pleased to announce CAmkES release 2.0.0 The new release updates CAmkES to be compatible with seL4 version 2.0.0. It also marks the transition to more frequent and regular releases, as well as switching our release process to semantic versioning, so it's easy to tell which CAmkES releases are source-compatible, or will require updates to user-level code, and also with which seL4 versions they will be compatible. You can find it at: https://github.com/seL4/camkes-tool/tree/2.0.0 And a manifest for the 2.0.0 compatible versions of the CAmkES test and example apps: https://github.com/seL4/camkes-manifest/blob/master/default-2.0.x.xml Enjoy! ________________________________ 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.

1 0

Extending errors to always include argument numbers
by Corey Richardson 04 Jan '16

04 Jan '16

For consistency, it seems like it'd beneficial if: seL4_RangeError seL4_AlignmentError seL4_DeleteFirst seL4_FailedLookup seL4_RevokeFirst included an indication of which argument the error applies to. For some of these errors, not every call has a unique argument which can cause the erorr. This seems like a relatively straightforward change for me to get acquainted with the full process of modifying and re-verifying the kernel. Are there tradeoffs hidden here that would make this undesirable? -- cmr +16032392210 http://octayn.net/

3 2

seL4 & camkes questions
by Julien Delange 04 Jan '16

04 Jan '16

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.

4 4

DMA
by Raymond Jennings 03 Jan '16

03 Jan '16

Is it ever possible for seL4 to run on a conventional machine without an IOMMU if any code that manipulates a DMA capable device is included as trusted or does DMA automatically void any assurance? Reason for question: Running seL4 on a system without an IOMMU.

4 8