May 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

haskell on sel4
by Tim Newsham 05 Dec '15

05 Dec '15

I just noticed the web page says "we have Haskell sort-of running on seL4 (thanks or friends from Galois for their help), should be released in the near future" This is great news. Are you able to share any details such as when any of this will be public, what the porting strategy was (is this similar to HalVM?), what dependencies haskell compiled code requires, if there are sel4 bindings, etc? Tim

3 4

Wandboard Port
by Robert Kaiser 30 Jul '15

30 Jul '15

Hello, in an attempt to familiarize myself with the seL4 code, I am trying to "port" it to the Wandboard (see www.wandboard.org) This should be an easy task for a beginner (thought I) since the board is very similar to the SabeLite, and seL4 is already running well on that board. I have access to a SabreLite and a Wandboard Quad, both (according to U-boot) have the same revision of the iMX6 SoC installed. Differences between the Sabre and the Wand I have noticed so far are: - 2GB of RAM from (0x10000000 to 0x90000000) on the Wand (Sabrelite has 1GB) - Wand uses UART1 for debug output, Sabrelite: UART2 I compiled an sel4test project where I adapted the UART port in kernel/include/plat/imx6/plat/machine/devices.h and elfloader/src/arch-arm/plat-imx6/platform.h and the RAM size in kernel src/plat/imx6/machine/hardware.c. When I boot this system, I get: Jumping to kernel-image entry point... Bootstrapping kernel Caught cap fault in send phase at address 0x0 while trying to handle: vm fault on data at address 0x9f11c2e0 with status 0x1c06 in thread 0xffdfad00 at address 0x13294 (Needless to say, "all is well in the universe" on the SabreLite... ) What is not shown here are a ton of other debug messages which I have added to convince myself that kernel initialization completes as expected. The crash seems to happen upon entry into user code. The address 0x13294 is the virtual address of the entry point: $ nm build/arm/imx6/sel4test-driver/sel4test-driver.bin | grep 13294 00013294 T _sel4_start I suspect that this fault happens on opcode fetch, because the user code is not properly mapped when invoked. Does "status 0x1c06" confirm this? If so, *should* the code be mapped at this point or are these mappings expected to be installed "on demand", i.e. through page fault handling? Thanks for any help... Robert -- Robert Kaiser Computer Engineering RheinMain University of Applied Sciences

3 14

Hello world - simple example thread creation
by Piotr 31 May '15

31 May '15

I would like to start from scratch - simple thread or process creation helloworld in seL4. I saw there are some examples in "sel4test/app" of seL4 application, but I am looking for something smaller. I have found here on page 39 "Creating a Thread in Own AS and cspace_t" http://www.cse.unsw.edu.au/~cs9242/14/lectures/01-intro.pdf example of thread creation. Unfortunetly I cannot find header file with " cspace_ut_retype_addr" or "ut_alloc". Are they obsolete, any replacements? Are there any small and simple hello-world tutorials or examples avaliable?

1 0

why do there are some differences between camkes branch and master branch in lib seL4/libsel4muslcsys
by Pei.XiLong(裴喜龙) 29 May '15

29 May '15

Hi, Siwei Zhuang, Why do there are some differences between camkes branch and master branch in lib seL4/libsel4muslcsys? The lib seL4/libsel4muslcsys is the foundation of libmuslc, it shoud be a libc for any seL4 program, and there should be no diference among any branches. https://github.com/seL4/libsel4muslcsys/commits/camkes Xilong Pei Tongji University 2015/5/29

3 3

[sel4] Porting seL4 to RISC-V - Status Report 1
by Hesham ALMatary 26 May '15

26 May '15

Hi all, As a warm up, I've written a blog entry [1] of the project giving some introductory details for both RISC-V and seL4 microkernel and what has been done so far. Open to questions/suggestions. [1] http://heshamelmatary.blogspot.co.uk/2015/05/porting-sel4-to-risc-v-status-… Thanks, -- Hesham

2 3

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

Virtual address space (kernelBase) restriction
by Hesham ALMatary 23 May '15

23 May '15

Hi all, Is it a must that every platform/architecture mapped to virtual addresses higher than 0xF0000000? Thanks -- Hesham

1 0

lowRISC Google Summer of Code
by Stefan Wallentowitz 19 May '15

19 May '15

Hi all, I just wanted to take the chance to introduce Hesham ALMatary and myself. Hesham participates in Google's Summer of Code in the lowRISC organization and I am his mentor. During summer, Hesham will port seL4 to the RISC-V architecture, specifically for the lowRISC project. Please find more details here: http://www.lowrisc.org/blog/2015/05/summer-of-code-students-for-lowrisc/ Hesham and I will keep you updated about the progress, I believe he will also give updates in his blog: http://heshamelmatary.blogspot.it/. Best Regards, Stefan

2 1

sel4 example compilation - cygwin
by Piotr 12 May '15

12 May '15

Hi, I am trying to compile example from 'Download' tutorial under Cygwin. http://sel4.systems/Download/ What I get is: [KERNEL] [BF_GEN] arch/object/structures_gen.h [BF_GEN] plat/machine/hardware_gen.h [BF_GEN] api/types_gen.h [CPP] src/arch/ia32/machine_asm.s [AS] src/arch/ia32/machine_asm.o /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S: Assembler messages: /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:15: Warning: .type pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:15: Error: junk at end of line, first unrecognized character is `o' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:20: Warning: .size pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:20: Error: junk at end of line, first unrecognized character is `o' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:22: Warning: .type pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:22: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:26: Warning: .size pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:26: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:30: Warning: .type pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:30: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:34: Warning: .size pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:34: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:36: Warning: .type pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:36: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:41: Warning: .size pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:41: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:43: Warning: .type pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:43: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:49: Warning: .size pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:49: Error: junk at end of line, first unrecognized character is `i' .......... What to do with it?

4 3