Devel December 2015

devel@sel4.systems

22 participants
18 discussions

IA32 syscall bindings
by Norman Feske 26 Aug '16

26 Aug '16

Dear seL4 developers, first, I'd like to thank you for publishing seL4 under GPL. I am very happy that I can finally get my hands dirty with working with the kernel of your group. :-) Currently, I am taking the first baby steps to bring the Genode OS framework (http://genode.org) to seL4. For reference, I am using the experimental branch. The first smallish issue I stumbled upon stems from the fact that Genode is written in C++. By compiling the seL4 syscall bindings with a C++ compiler, I got the following error: error: inconsistent operand constraints in an ‘asm’ It can be reproduced by putting the following code snippet into a cc file and compiling it with 'g++ -m32 -c' (tested with the Genode tool chain as well as with GCC 4.8.1): typedef enum { seL4_SysDebugPutChar = -9, _enum_pad_seL4_Syscall_ID = (1U << ((sizeof(int)*8) - 1)) } seL4_Syscall_ID; void seL4_DebugPutChar(char c) { asm volatile ( "pushl %%ebp \n" "movl %%esp, %%ecx \n" "leal 1f, %%edx \n" "1: \n" "sysenter \n" "popl %%ebp \n" : : "a" (seL4_SysDebugPutChar), "b" (c) : "%ecx", "%edx", "%esi", "%edi", "memory" ); } When compiling the same code snippet with 'gcc' instead of 'g++', everything is fine. It turns out that the C++ compiler does not like the enum value to be specified as input argument. I found the following ways to circumvent this problem: * Changing the enum value 'SysDebugPutChar' to a positive value, * Removing the definition of '_enum_pad_seL4_Syscall_ID', * Casting 'seL4_SysDebugPutChar' to an integer: : "a" ((int)seL4_SysDebugPutChar), In any case, I seem to have to change the bindings. Do you see a way around it? If not, would you consider one of the solutions above for the seL4 headers? On another note, I noticed that the bindings use the EBX register. Unfortunately, this makes it impossible to compile seL4 userland software as position-independent code (PIC). E.g., when compiling the above code snippet via 'g++ -m32 -fPIC -c', the following error occurs: error: inconsistent operand constraints in an ‘asm’ However, PIC is required in order to use shared libraries. The solution would be to not use EBX to pass arguments to the 'asm' statements, save EBX on the stack prior moving the respective kernel argument to the register, and, of course, restoring it after sysenter returns. Before I start changing the bindings, I'd like to know: is there anyone else working on the same problem? Would you be open to accept a change of the bindings to become PIC compliant on the costs of a few added instructions? Or do you have another suggestion how I should go about it? 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

4 7

seL4 & camkes questions
by Julien Delange 05 Jan '16

05 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 04 Jan '16

04 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

Tutorial error
by Julien Delange 24 Dec '15

24 Dec '15

Hello, I am trying to reproduce the tutorial. I followed the steps from the slides on https://github.com/seL4-projects/sel4-tutorials/blob/master/docs/seL4Tutori… When trying to compile, I got the following error in [1]. It seems to be a warning from the compiler, so, I edit the CFLAGS in the .config and tried to compile but then got the error in [2], which then avoid any potential compilation. Is there any special setup for the compiler? I am currently using gcc 5.2.1. Thanks for any suggestion, Julien. [1] /home/julien/tmp/sel4-tutorials/stage/x86/pc99/include/vka/object.h:286:5: warning: 'seL4_AsyncEndpointObject' is deprecated (declared at /home/julien/tmp/sel4-tutorials/stage/x86/pc99/include/sel4/objecttype.h:23): use seL4_NotificationObject [-Wdeprecated-declarations] [2] /home/julien/tmp/sel4-tutorials/kernel/src/plat/pc99/machine/acpi.c:38:13: error: size of array '__assert_failed_acpi_rsdp_packed' is negative

2 2

Camkes dependencies & development environment
by Julien Delange 23 Dec '15

23 Dec '15

Dear all, First of all, sorry if this question has been asked several times already. I am currently trying to use sel4 & camkes on a debian stable. I installed all the dependencies but I am facing an error message when trying to build the tool (see below). My version of cabal is 1.20, so, version should not be an issue. After searching, it seemed that the version of ghc might be the root cause so I upgraded to testing and/or unstable but faced other issues then. My question is then what is the best development environment to use sel4 and camkes? Any special recommendation? I would like to keep my existing debian/stable as much as possible. Thanks for any help or suggestion, Julien. [parse-capDL] building... export CONFIG_CAPDL_LOADER_MAX_IRQS=256 && cabal configure && cabal build && cp dist/build/parse-capDL/parse-capDL . Resolving dependencies... cabal: The package 'capDL-tool' requires Cabal library version -any && >=1.18 but no suitable version is installed. Makefile:45: recipe for target 'parse-capDL' failed make[1]: *** [parse-capDL] Error 1 Makefile:49: recipe for target '/home/julien/tmp/camkes/stage/arm/imx31/parse-capDL/parse-capDL' failed make: *** [/home/julien/tmp/camkes/stage/arm/imx31/parse-capDL/parse-capDL] Error 2

3 3

domain problems
by ぷ风过无痕?? 23 Dec '15

23 Dec '15

Hi everyone, I'm running the RefOS project on arm kzm board. The config file is kzm_debug_defconfig. I am tring to set two domains in the RefOS by changing the CONFIG_NUM_DOMAIN parameter from 1 to 2 in this file and rebuilt RefOS. When running RefOS it gets stucked and some servers cannot be initialized.How to resolve this bug?

1 0

domain problems
by ぷ风过无痕?? 23 Dec '15

23 Dec '15

1 0

RTEMS working with seL4
by Hesham Almatary 16 Dec '15

16 Dec '15

Hi all, I got an RTEMS port working for RISC-V architecture along with seL4. This depends on my earlier seL4 port for RISC-V. RTEMS runs with support of seL4 microkernel, and it runs in Supervisor mode (on another core). seL4 application would allocate and map memory for it from its untyped memory (userspace), before off-loading it to another core. seL4 application that loads/runs RTEMS is pretty much the same as SOS. For more details (and instructions) about how to build/run the project, see the github repo of the port [1], and/or this blog post [2] [1] https://github.com/heshamelmatary/rtems-riscv [2] http://heshamelmatary.blogspot.co.uk/2015/12/rtems-port-for-risc-v-withwith… Cheers, -- Hesham

2 2

VSpace translation?
by Ben Karel 14 Dec '15

14 Dec '15

Would any of seL4's guarantees be compromised if a Translate method were added to page directory objects (for mapping a virtual address to the underlying physical address, without exposing the intermediate page capabilities)?

4 4

Capability resolution depth mismatches
by Ben Karel 14 Dec '15

14 Dec '15

Hi all, Some capability resolution, such as for fault handling, winds up calling resolveAddressBits with n_bits = wordBits, and any remaining bits are ignored. In other cases, such as the destination slot for seL4_CNode_Copy, the user provides a resolution depth parameter, and the call to resolveAddressBits is mediated by lookupSlotForCNodeOp, which fails with a depth mismatch if there are any bits remaining. Individually these seem like reasonable choices, but it leads to code like this: seL4_CNode cspace_root = ...; // freshly allocated 256-slot CNode with no guard seL4_CPtr slot_for_copy = 0x23; // arbitrary slot we know is available seL4_CPtr slot_for_tcb = slot_for_copy << 24; seL4_CNode_Copy(cspace_root , endpoint_for_copy, 8, ...); seL4_TCB_Configure(..., endpoint_for_tcb, ...); I found it surprising that two different CPtrs are needed to describe the same slot! Is there a conceptual-model-explanation that doesn't involve appeal to the underlying implementation? Also: my current understanding is that the depth parameter is only needed to disambiguate indirections through CNode-containing slots. What goes wrong if the depth mismatch checks are relaxed?

2 2

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel December 2015