January 2015 - Devel - lists.sel4.systems

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

Progress of bringing Genode to seL4
by Norman Feske 26 May '15

26 May '15

Hello, I have written up the first of a series of articles about using seL4 as base platform for the Genode OS framework: http://genode.org/documentation/articles/sel4_part_1 I hope that it contains useful bits of information for novices of seL4 and Genode alike. Even though the article outlines a few hurdles, the overall experience of using the kernel had been overly positive so far. For those of you interested in tracking the progress of the ongoing work, here is the corresponding topic branch: https://github.com/nfeske/genode/commits/sel4 Cheers 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

Optimizations?
by Raoul Duke 30 Jan '15

30 Jan '15

> Easier to keep the generator simple and let the compiler do the optimisations it already understands. Based on things like the experiences of Tahoe LAFS with compiler optimizations vs. security - let alone plain bugs - I am scared if anybody uses any optimizations at all, especially for serious business. I have not researched the position se4L takes on this. Are the proofs about the before-optimization code, or do they consider the after-optimization assembly output? thanks.

4 4

curious design pattern
by David Greve 29 Jan '15

29 Jan '15

One more and then I'll stop .. I promise. There appear to be numerous instances of the following design pattern: struct message_info { uint32_t words[1]; }; Where the above structure is then allocated locally, initialized and returned by a procedure. Seems like a lot of work to return a uint32_t. I originally assumed that all/much of this code was generated automatically from Haskell .. so I figured it was some odd corner case in the translator. Subsequent discussions, however, have suggested that this assumption is false and that the code was actually written by hand. I could understand using structures to present a unique, statically checkable procedure type signature .. but I can't rationalize the use of the single element array. So .. is there a reason for this curious design pattern? Thanks, Dave

3 2

Haskell error comments
by David Greve 28 Jan '15

28 Jan '15

What is the significance of the various "Haskell error:" comments found throughout the kernel code?

3 6

fall-through procedures
by David Greve 27 Jan '15

27 Jan '15

I ran the sel4 kernel source through the CIL infrastructure front end: http://kerneis.github.io/cil/ CIL reported two warnings: ../../../../seL4/src/object/cnode.c:867: Warning: Body of function isMDBParentOf falls-through. Adding a return statement ../../../../seL4/src/object/objecttype.c:261: Warning: Body of function recycleCap falls-through and cannot find an appropriate return value The first warning looks like a weakness in CIL code analysis .. every branch of the condition has a return so the procedure doesn't need a fall-through return. The same is not true for the second .. the first branch halt()'s but it doesn't return .. thus the procedure is not "obviously" type safe. I'm curious about the this from a reasoning perspective. Perhaps the argument is that halt() never terminates (or it "exits"), thus it is OK if the procedure doesn't return a value in that case. But that argument only works if the logic somehow captures the semantics of halt(). Are halt() semantics baked into the correctness proofs? If not, how is this procedure justified? Thanks, Dave

2 2

Elfloader faults when MMU activated
by Jordan Woehr 24 Jan '15

24 Jan '15

Hello, I am attempting to boot the seL4 kernel (only the kernel, not the platform library) on an AM335x chip and am running into difficulties when the elfloader enables the MMU. Debug statements indicate that the enable_mmu function is not returned from, thus I believe a fault is occuring when the processor attempts to execute the first instruction following the MMU being enable. Unfortunately I do not have access to a JTAG debugger at the moment, so I will relay what information I can. I should also mention that I have made no changes to the elfloader source code except where noted for debugging purposes. I have verified that the page table is being setup for supervisor access (access protection bit 10 set, bit 11 clear) and that the domain is set to 0 for all pages. As I understand it, this means that the permissions set in the domain access control register are checked. I am booting the elfloader through uboot and since the co-processor registers are accessible, I believe I am already in supervisor mode. Thus it would seem the elfloader code should work without modification. However, the only way I have found to get the kernel to boot is by setting access control for domain 0 to manager (write 3 instead of 1 at https://github.com/seL4/elfloader-tool/blob/803b92c7a3c9b48bd474b3de7ac9b8c…) >From my examination of the code, I don't believe this should be necessary, so I think I have probably configured the project incorrectly or am loading the image with uboot somehow incorrectly (for the record, I objcopy the elfloader elf to a bin and load the image through uboot to memory address 0x82000000 and perform a go command). What confuses me is that if I leave access to the domain set as client (no change from what is on the master branch) and instead set the permission on the page to bit 10 and bit 11 both set, the processor still faults. I would expect this configuration to not produce a fault since these permissions should allow supervisor and non-supervisor read/write access. Finally, the code is executing in a region that is 1:1 mapped after the MMU is enabled, so I don't think this is a problem. With all that said, does anyone have any idea why the elfloader isn't working out of the box for me? As I understand things, using the elfloader is the standard way to boot the kernel on an arm processor. I have included the options of my build configuration at the end of this message. Thank you for your time, Jordan CONFIG_ARCH_ARM_V7A=y CONFIG_ARCH_ARM=y CONFIG_ARM_CORTEX_A8=y CONFIG_PLAT_AM335X=y CONFIG_ROOT_CNODE_SIZE_BITS=16 CONFIG_TIMER_TICK_MS=2 CONFIG_TIME_SLICE=5 CONFIG_RETYPE_FAN_OUT_LIMIT=256 CONFIG_MAX_NUM_WORK_UNITS_PER_PREEMPTION=100 CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS=199 CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS=167 CONFIG_FASTPATH=y CONFIG_NUM_DOMAINS=1 CONFIG_DOMAIN_SCHEDULE="" CONFIG_NUM_PRIORITIES=256 CONFIG_DEBUG_BUILD=y CONFIG_IRQ_REPORTING=y CONFIG_OPTIMISATION_O2=y CONFIG_LIB_SEL4=y CONFIG_LIB_MUSL_C=y CONFIG_HAVE_LIBC=y CONFIG_HAVE_CRT=y CONFIG_LIB_CPIO=y CONFIG_LIB_ELFLOADER=y CONFIG_ARM_ERRATA_764369=y CONFIG_CROSS_COMPILER_PREFIX="arm-none-eabi-" CONFIG_KERNEL_COMPILER="" CONFIG_KERNEL_CFLAGS="" CONFIG_KERNEL_EXTRA_CPPFLAGS="" CONFIG_USER_EXTRA_CFLAGS="" CONFIG_USER_CFLAGS="" CONFIG_USER_OPTIMISATION_O2=y CONFIG_USER_DEBUG_BUILD=y

2 2

Re: [seL4] run_test failures
by David Greve 22 Jan '15

22 Jan '15

Gerwin, On Tue, Jan 20, 2015 at 3:02 PM, Gerwin Klein <Gerwin.Klein(a)nicta.com.au> wrote: > Hi David, > > yes, it seems the Isabelle installation step failed already. The command > ./isabelle/bin/isabelle components -a should print the list of missing > components as it did, but should then start downloading them. Instead it > printed an error message about dirname. > Isabelle did go on to download and install the components (sorry: the ellipsis was supposed to suggest that). I did not see any other warnings or errors after the message about dirname. Is there any way I could test to make sure this installation succeeded? > It's possible that it is picking up the wrong kind of shell to run the > script. Do you have bash installed? The script is trying to run bash using > "#!/usr/bin/env bash" > Bash is installed. When I type /usr/bin/env bash at my prompt I get a new bash shell prompt. > The wrong path out of run_tests also seems to be related to dirname. It's > this line that seems to be going wrong: > > DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" > > in this case DIR should just become ".", but it seems to return the empty > string instead. > I added a line to echo DIR in the run_scripts and it prints out my current working directory, as I would expect. The nature of the failure makes me think there might some environment variable that I am supposed to set .. could that be? It looks like the test failure was generated by "make" .. can you tell me where (the directory in which) make is run and/or tell me where to find the Makefile it is using? > Cheers, > Gerwin > > > On 21.01.2015, at 05:41, David Greve <david.greve(a)rockwellcollins.com> > wrote: > > > > > > I am attempting to run the sel4 proofs on linux Mint 17.1 (64-bit). > > > > I have a copy of the "verification" project and have walked through > all of the setup steps up to the point of running run_test. When I do, I > encounter numerous failures, the first of which says: > > > > ------------------------------------------------------------------------ > > TEST FAILURE: CamkesAdlSpec > > > > /isabelle/bin/isabelle build -b -v -d "" CamkesAdlSpec > > make: /isabelle/bin/isabelle: Command not found > > /bin/sh: /isabelle/bin/isabelle: No such file or directory > > make: *** [CamkesAdlSpec] Error 127 > > > > ------------------------------------------------------------------------ > > > > Note that the isabelle command appears to be missing a leading path. > > > > I think the script is somehow failing to pick up my working directory. > > > > Now, when I was setting up isabelle, I did see the following message: > > > > $ ./isabelle/bin/isabelle components -a > > ### Missing Isabelle component: > "/home/dagreve/.isabelle/contrib/cvc3-2.4.1" > > ... > > ### Missing Isabelle component: > "/home/dagreve/.isabelle/contrib/xz-java-1.2-1" > > dirname: missing operand > > Try 'dirname --help' for more information. > > ... > > > > The setup completed without further errors, but I wonder if this is a > contributing factor? > > > > Thanks, > > Dave > > > > _______________________________________________ > > Devel mailing list > > Devel(a)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. >

3 8

run_test failures
by David Greve 21 Jan '15

21 Jan '15

I am attempting to run the sel4 proofs on linux Mint 17.1 (64-bit). I have a copy of the "verification" project and have walked through all of the setup steps up to the point of running run_test. When I do, I encounter numerous failures, the first of which says: ------------------------------------------------------------------------ TEST FAILURE: CamkesAdlSpec /isabelle/bin/isabelle build -b -v -d "" CamkesAdlSpec make: /isabelle/bin/isabelle: Command not found /bin/sh: /isabelle/bin/isabelle: No such file or directory make: *** [CamkesAdlSpec] Error 127 ------------------------------------------------------------------------ Note that the isabelle command appears to be missing a leading path. I think the script is somehow failing to pick up my working directory. Now, when I was setting up isabelle, I did see the following message: $ ./isabelle/bin/isabelle components -a ### Missing Isabelle component: "/home/dagreve/.isabelle/contrib/cvc3-2.4.1" ... ### Missing Isabelle component: "/home/dagreve/.isabelle/contrib/xz-java-1.2-1" dirname: missing operand Try 'dirname --help' for more information. ... The setup completed without further errors, but I wonder if this is a contributing factor? Thanks, Dave

2 1

Support for Intel x86-64?
by Yes Man 13 Jan '15

13 Jan '15

2 1