December 2014 - 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

simple_default_cap_count doesn't contain seL4_CapDomain
by Pei.XiLong(裴喜龙) 05 Jan '15

05 Jan '15

Hi PM, The logic in these 2 functions doesn’t contain capability seL4_CapDomain int simple_default_cap_count(void *data) seL4_CPtr simple_default_nth_cap(void *data, int n) So, these sentense cause error: // ……/sel4tes-drivers/src/main.c env.init->domain = copy_cap_to_process(&test_process, simple_get_init_cap(&env.simple, seL4_CapDomain)); Xilong Pei Tongji University 2014/12/31

2 4

Day-to-day usability of seL4
by Marc Hans 31 Dec '14

31 Dec '14

seL4 as a kernel is complete, as far as I can tell, but what about the userspace and hardware support? As soon as this formally verified OS boots into a graphical interface and one can get a simple web browser and media player working, it will be pretty much ready for day-to-day use for most users. I normally wouldn't expect such a thing, but since NICTA has showed excellence in the past and is so intensively powered, I got my hopes up. Will users soon be able to use a completely formally verified OS (kernel, userspace and everything)? Or is that something too far fetched to dream about? Best wishes, Marc Collin

4 3

i.MX6 quad booting problems
by Will Korteland 25 Dec '14

25 Dec '14

Hi everyone, I hope I'm using the correct list for this type of thing... I've bought my own Sabre Lite (identical to the AOS boards), and I've been trying for a few days now to get it to boot from tftp. I've downloaded the prebuilt u-boot.bin from the Sabre Lite hardware page, but it still doesn't seem to be working - it keeps timing out when trying to do the transfer. I think my tftp server is set up correctly, since it is the same as it was during AOS last semester. Could someone please boot a Sabre Lite set up for TFTP, interrupt the default boot process, type "printenv" into the U-Boot prompt and paste the results? Sorry if this is the wrong place to ask. Thanks, - Will

2 4

page permissions - execute?
by Tim Newsham 24 Dec '14

24 Dec '14

Is there no "execute" permission that can be set (or not set) on mapped pages in sel4?

4 3

(no subject)
by Jensen Zhang 24 Dec '14

24 Dec '14

Hi Will, About the message, "Unknown command 'bootelf'", it seems that this command wasn't configured and compiled. You'd better recompile th u-boot image. You can modify the source code to config this command. Add a macro define "#define CONFIG_CMD_ELF" in the file "include/config_cmd_default.h" to enable the command "bootelf". This link can help you, http://elastos.org/redmine/issues/17472#change-34139. Lucky! -- Jensen Zhang Tongji University

1 0

Run seL4 on OMAP4
by 张静轩 22 Dec '14

22 Dec '14

Hi, We have run the seL4 on pandaboard[1] (omap4 platform). It seems that the kernel works well, excpet for some tests about timer. Is there anyone interested in it or helping us? The source code can be got from the following link[2] now. (We will upload to github latter.) btw. I think the devices and platforms supported by seL4 are too few. How to make it easy to let seL4 support more devices? Can anyone give me some suggestion? I suggest to write a document to port seL4 easier. :) --- Jensen Zhang Tongji University 2014/12/22 [1] http://pandaboard.org/ [2] http://elastos.org/review/#/admin/projects/HD-Elastos

2 1

Re: [seL4] Devel Digest, Vol 7, Issue 3
by Kenneth 20 Dec '14

20 Dec '14

Hi Pei, Maybe you could make it happen on cmkes. As far as I know it's a set of OS' services for sel4, just like Iguana for OKL4. FS should be a service, so I think it's better ported into cmkes. This email is typed on my iPhone. I'd like to apologize for any mistake in it. > 在 2014年12月20日，9:00，devel-request@sel4.systems 写道： > > Send Devel mailing list submissions to > devel(a)sel4.systems > > To subscribe or unsubscribe via the World Wide Web, visit > https://sel4.systems/lists/listinfo/devel > or, via email, send a message with subject or body 'help' to > devel-request(a)sel4.systems > > You can reach the person managing the list at > devel-owner(a)sel4.systems > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Devel digest..." > > > Today's Topics: > > 1. I want to port a filesystem onto seL4 (XilongPei (???)) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Fri, 19 Dec 2014 14:20:22 +0800 > From: XilongPei(???) <pei_xilong(a)tongji.edu.cn> > To: <devel(a)sel4.systems> > Subject: [seL4] I want to port a filesystem onto seL4 > Message-ID: <01c401d01b53$e054be30$a0fe3a90$(a)tongji.edu.cn> > Content-Type: text/plain; charset="gb2312" > > Hi, > I want to port a filesystem onto seL4, the source code is here: > https://github.com/RT-Thread/rt-thread/tree/master/components/dfs Can anyone > give me some suggestion? > > > Xilong Pei > Tongji University > 2014/12/19 > > > > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > > ------------------------------ > > End of Devel Digest, Vol 7, Issue 3 > ***********************************

3 2

I want to port a filesystem onto seL4
by XilongPei(裴喜龙) 19 Dec '14

19 Dec '14

Hi, I want to port a filesystem onto seL4, the source code is here: https://github.com/RT-Thread/rt-thread/tree/master/components/dfs Can anyone give me some suggestion? Xilong Pei Tongji University 2014/12/19

1 0