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
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
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
Here <https://github.com/winksaville/sel4-min-sel4/tree/new-libs> is a
different approach for removing the libc dependency, it seemed like people
thought libsel4 was to big and that as part of the effort of breaking the
dependency it should be made smaller. Basically libsel4 does nothing expect
satisfy dependency needed for the kernel for some xml files. And I've
broken libsel4 into basically 8 other libraries. see here
<https://github.com/winksaville/sel4-min-sel4/tree/new-libs/libs>.
This maybe taking things to far, but it does mean people can use only what
they need, which I like. The smallest example is app/min-hw which only uses
libsel4_gen, libsel4_startup. libsel4_bootinfo and libsel4_putchar. At the
other extreme apps/test-newlibs uses everything. Anyway other organizations
are certainly possible.
Currently there is at least one known problem, I modified bitfield_gen.py
so types_gen.h has no asserts since at the moment the kernel uses assert
and userspace is libsel4_assert. We could either do something like I've
done and remove them or change the kernel to use libsel4_assert or
something else.
Anyway, before creating a pull request I'd like to know what people think.
-- Wink
I noticed that seL4/libsel4 was dependent upon libc and so I created a
patch (
https://github.com/winksaville/seL4/commit/fc91a1f68c054fdb41aaa42a7b56a80f…)
which removes the dependency. If there is interest I can submit a pull
request, and of course will make any changes deemed necessary to make it
suitable for acceptance.
Please advise,
Wink
Hi,
I am using RefOS to develop a small applicaiton(interprocess comunicaion).I need to edit some c files in RefOS/libs/librefos directory,But comments say that do not edit these files,these files were generated by CIDL.CIDL is a simple C IDL compiler which is made to save the trouble of manually implementing RPC interface stubs to marshal C style arguments and return value. It uses a simple XML-based IDL language. I search on the google，but just got some introduction. So where can I got some useful infomation about CIDL? Can you recommend some books or websites?
------------------ Original ------------------
From: "devel-request";<devel-request(a)sel4.systems>;
Date: Sun, Jun 21, 2015 10:00 AM
To: "devel"<devel(a)sel4.systems>;
Subject: Devel Digest, Vol 13, Issue 11
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. Re: Devel Digest, Vol 13, Issue 10_Bare Metal support for GCC
(da Tyga)
----------------------------------------------------------------------
Message: 1
Date: Sat, 20 Jun 2015 16:26:46 +1000
From: da Tyga <cyberfonic(a)gmail.com>
To: devel(a)sel4.systems
Subject: Re: [seL4] Devel Digest, Vol 13, Issue 10_Bare Metal support
for GCC
Message-ID:
<CALj3Nd3+CFFQF41BOwW+-bwFNOEZS9HyVLHDwVssTyMAcsU3ig(a)mail.gmail.com>
Content-Type: text/plain; charset="utf-8"
>
>
> Hi Yuxin,
I don't think you need to modify GCC, it is the compiler that you can use
to generate required executables. Making changes to it is a massive
undertaking.
Instead of trying to reinvent stuff that has already been done, you really
should read the Genode documentation and download and read the source code
referenced by Norman Feske's suggestions.
>From my reading of the Genode documents and source code, I would expect
that you would find a considerable amount of code that you could you
re-purpose for your specific requirements.
Cheers,
Tyga
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Fri, 19 Jun 2015 22:46:40 +0800
> From: Yuxin Ren <ryx(a)gwmail.gwu.edu>
> To: Norman Feske <norman.feske(a)genode-labs.com>
> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems>
> Subject: Re: [seL4] Does sel4 support c++
> Message-ID:
> <CAAKbDrcbyh0YV+nHzhziiiXavn-=
> P_tW5bS2LUfPzHcBF-iMKg(a)mail.gmail.com>
> Content-Type: text/plain; charset="utf-8"
>
> Thank you all!
>
> If modifying the tool chain is the easiest way, I want to try it.
> But I definitely want to avoid creating the tool chain from "bare metal".
> I still prefer to reuse the existing tool chain like gcc
> with minimal modification.
>
> Could you give me some guidance how to create a custom tool chain, which
> part I need to modify?
> I am not familiar with gcc. So if I have to modify gcc, where can I get
> more information or documentation?
>
> Thanks a lot!!
> Yuxin
>
> On Thu, Jun 18, 2015 at 9:50 PM, Norman Feske <
> norman.feske(a)genode-labs.com>
> wrote:
>
> > Hello,
> >
> > > The easiest approach is possibly to create a custom tool chain, and
> port
> > > the GCC C++ library that way. I know the people behind Genode did some
> > > of this (http://genode.org/download/tool-chain), although I'm not sure
> > > how much of the C++ standard library they actually support.
> >
> > more in-depth information about Genode's tool chain are provided by
> > Section 7.2 of the documentation [1]. In short, the tool chain is a
> > "bare metal" tool chain that does not depend on a C library, yet it
> > still supports C++ (including exceptions and runtime type information).
> >
> > On Genode, the libc and STL (aka stdcxx) can be used optionally whereas
> > the STL depends on the libc. The libc is based on FreeBSD's libc. The
> > STL is GCC's version. Both libraries are available via Genode's ports
> > mechanism.
> >
> > That said, as both the libc and stdcxx are shared libraries, they cannot
> > be used on the seL4 version of Genode as of now. Shared libraries don't
> > work on seL4 (at least on x86_32) because the system-call bindings
> > cannot be compiled with -fPIC.
> >
> > [1] http://genode.org/documentation/genode-foundations-15-05.pdf
> >
> > 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
> >
> > _______________________________________________
> > Devel mailing list
> > Devel(a)sel4.systems
> > https://sel4.systems/lists/listinfo/devel
> >
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: <
> http://sel4.systems/pipermail/devel/attachments/20150619/5b4ce704/attachmen…
> >
>
> ------------------------------
>
> Subject: Digest Footer
>
> _______________________________________________
> Devel mailing list
> Devel(a)sel4.systems
> https://sel4.systems/lists/listinfo/devel
>
>
> ------------------------------
>
> End of Devel Digest, Vol 13, Issue 10
> *************************************
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://sel4.systems/pipermail/devel/attachments/20150620/c72cfc07/attachmen…>
------------------------------
Subject: Digest Footer
_______________________________________________
Devel mailing list
Devel(a)sel4.systems
https://sel4.systems/lists/listinfo/devel
------------------------------
End of Devel Digest, Vol 13, Issue 11
*************************************
>
>
> Hi Yuxin,
I don't think you need to modify GCC, it is the compiler that you can use
to generate required executables. Making changes to it is a massive
undertaking.
Instead of trying to reinvent stuff that has already been done, you really
should read the Genode documentation and download and read the source code
referenced by Norman Feske's suggestions.
>From my reading of the Genode documents and source code, I would expect
that you would find a considerable amount of code that you could you
re-purpose for your specific requirements.
Cheers,
Tyga
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Fri, 19 Jun 2015 22:46:40 +0800
> From: Yuxin Ren <ryx(a)gwmail.gwu.edu>
> To: Norman Feske <norman.feske(a)genode-labs.com>
> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems>
> Subject: Re: [seL4] Does sel4 support c++
> Message-ID:
> <CAAKbDrcbyh0YV+nHzhziiiXavn-=
> P_tW5bS2LUfPzHcBF-iMKg(a)mail.gmail.com>
> Content-Type: text/plain; charset="utf-8"
>
> Thank you all!
>
> If modifying the tool chain is the easiest way, I want to try it.
> But I definitely want to avoid creating the tool chain from "bare metal".
> I still prefer to reuse the existing tool chain like gcc
> with minimal modification.
>
> Could you give me some guidance how to create a custom tool chain, which
> part I need to modify?
> I am not familiar with gcc. So if I have to modify gcc, where can I get
> more information or documentation?
>
> Thanks a lot!!
> Yuxin
>
> On Thu, Jun 18, 2015 at 9:50 PM, Norman Feske <
> norman.feske(a)genode-labs.com>
> wrote:
>
> > Hello,
> >
> > > The easiest approach is possibly to create a custom tool chain, and
> port
> > > the GCC C++ library that way. I know the people behind Genode did some
> > > of this (http://genode.org/download/tool-chain), although I'm not sure
> > > how much of the C++ standard library they actually support.
> >
> > more in-depth information about Genode's tool chain are provided by
> > Section 7.2 of the documentation [1]. In short, the tool chain is a
> > "bare metal" tool chain that does not depend on a C library, yet it
> > still supports C++ (including exceptions and runtime type information).
> >
> > On Genode, the libc and STL (aka stdcxx) can be used optionally whereas
> > the STL depends on the libc. The libc is based on FreeBSD's libc. The
> > STL is GCC's version. Both libraries are available via Genode's ports
> > mechanism.
> >
> > That said, as both the libc and stdcxx are shared libraries, they cannot
> > be used on the seL4 version of Genode as of now. Shared libraries don't
> > work on seL4 (at least on x86_32) because the system-call bindings
> > cannot be compiled with -fPIC.
> >
> > [1] http://genode.org/documentation/genode-foundations-15-05.pdf
> >
> > 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
> >
> > _______________________________________________
> > Devel mailing list
> > Devel(a)sel4.systems
> > https://sel4.systems/lists/listinfo/devel
> >
>
Hi,
Can I run C++ programs on sel4?
I am not familiar with programming language.
I do not know the relationship between the OS and the C++ language.
In order to run C++, does the OS need to provide some support or what user
level library are needed?
Thanks a lot.
Yuxin
Hi
I'm very interested in working with the virtualization extensions on sel4 - is there any rough timeline for when these will be available.
Thanks
Nick
Hi,
In general, a high-availability system should have the following
software services
http://electronicdesign.com/boards/high-availability-rtoss-deliver-five-nine
s-reliability :
- Heartbeat support for each server and each application.
- Event management capability for change notification.
- Alarm management for error handling.
- Transactions capability for check-pointing and
rollback/restart.
- Clustering for server management and applications links.
- Reliable storage support for RAIDs and for journaling file
systems.
I want to develop a high-availability system on seL4, can anyone
give me some suggestions? QNX has high availability support
http://www.qnx.com/developers/docs/6.3.0SP3/neutrino/sys_arch/ham.html , can
we learn something from them?
Xilong Pei
Tongji University
2015/6/11
