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