July 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

Some questions about seL4 operating system
by Qing Wei 22 Aug '15

22 Aug '15

Hi, I am a beginner to seL4 as well as microkernel, and very interested in it. I think it is great in terms of its minimality and formally verified security. However, I have some questions about it, (1) How is its performance compared to other monolithic kernel, say, Linux. Could it make use of multicore, multiprocessor to enjoy the performance scalability? (2) How is its ecosystem, fox example, how to support new hardware, does it need write the driver from scratch or could it make use of Linux driver? And how to write application on it, or, could it run Linux application without modification? (3) How is its virtualization support, could it run Linux vm, and does it need any modification to the guest os? Cheers, Qing Wei

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

Happy Birthday, Developers!
by Gernot Heiser 29 Jul '15

29 Jul '15

Hi everyone, Today is the anniversary of the open-sourcing of seL4. At NICTA we’re celebrating, I hope you’ll virtually join us ;-) Let me add that I quite enjoy this mailing list. Traffic has a high signal-noise ratio (apologies for degrading it with this message ;-) people generally seem to know what they are doing, and the community is clearly growing. Presently there are over 300 addresses on the list. Many thanks from all of us at NICTA, and keep it up! Gernot [cid:1374281D-B193-431C-AA3F-D6EE049C461A@keg.ertos.in.nicta.com.au] ________________________________ 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.

2 1

CMake and seL4
by Wink Saville 29 Jul '15

29 Jul '15

In my opinion the edit/compile/test loop with the standard build system seeed slow, so I thought I'd try to see if CMake might be any better. Here <https://github.com/winksaville/sel4-newlibs-manifest> is repo manifest which uses CMake for building my sel4-newlibs helloworld application and I'm happy to report there is some improvement. For a "clean" build it is about 2x faster, 8 seconds as compared to 14 seconds. And for a small change to apps/helloworld/src/main.c it is 20x faster, 0.3 seconds as compared to 7 seconds. Is there any interest in using CMake or other build system to reduce the builds times for seL4? -- Wink

2 2

seL4 runs on Rocket Chip (RISCV/FPGA)
by Hesham ALMatary 18 Jul '15

18 Jul '15

Hi all, This is a status update of the seL4/RISC-V project. It can run now on Rocket Chip (FPGA) and jor1k (online emulator), for more details have a look at this link [1]. [1] http://heshamelmatary.blogspot.co.uk/2015/07/sel4-runs-on-rocket-chip-riscv… Thanks, -- Hesham

1 0

Some questions about seL4 operating system
by Qing Wei 16 Jul '15

16 Jul '15

Hi, I am a beginner to seL4 as well as microkernel, and very interested in it. I think it is great in terms of its minimality and formally verified security. However, I have some questions about it, (1) How is its performance compared to other monolithic kernel, say, Linux. Could it make use of multicore, multiprocessor to enjoy the performance scalability? (2) How is its ecosystem, fox example, how to support new hardware, does it need write the driver from scratch or could it make use of Linux driver? And how to write application on it, or, could it run Linux application without modification? (3) How is its virtualization support, could it run Linux vm, and does it need any modification to the guest os? Cheers, Qing Wei

1 0

what are these comments meaning
by Pei.XiLong(裴喜龙) 15 Jul '15

15 Jul '15

Hi, In recent seL4 commit https://github.com/seL4/seL4/commit/67d8d041de0c435a1cc59ef8c237be6e39beb1c6 , A lot of comments like these: /** AUXUPD: "(True, ptr_retyps (2 ^ (unat \<acute>userSize)) (Ptr (ptr_val \<acute>regionBase) :: cte_C ptr))" */ /** GHOSTUPD: "(True, gs_new_cnodes (unat \<acute>userSize) (ptr_val \<acute>regionBase) (4 + unat \<acute>userSize))" */ have been added into source code, What is their meaning? I don't know isablle, and just know a little about haskell. thanks! Xilong Pei Tongji University 2015/7/14

2 1

Raspberry Pi version for learning about seL4
by Simon Apperley 14 Jul '15

14 Jul '15

Hi, I wondered if there was any news on the Raspberry Pi 2 port of seL4 which I saw mentioned when I did a search? I am interested in using the Raspberry Pi to learn about seL4 - not as a target for a full system (as I know there is an issue with trusting the boot mechanism). I just thought it would be a nice platform to use to get my head around seL4 and experiment with virtualising Linux and maybe Android? Simon Sent from my iPad

2 1