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
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
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
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
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
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
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
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
> ***********************************
