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
I would like to start from scratch - simple thread or process creation
helloworld in seL4. I saw there are some examples in "sel4test/app" of seL4
application, but I am looking for something smaller.
I have found here on page 39 "Creating a Thread in Own AS and cspace_t"
http://www.cse.unsw.edu.au/~cs9242/14/lectures/01-intro.pdf
example of thread creation. Unfortunetly I cannot find header file with "
cspace_ut_retype_addr" or "ut_alloc". Are they obsolete, any replacements?
Are there any small and simple hello-world tutorials or examples avaliable?
Hi, Siwei Zhuang,
Why do there are some differences between camkes branch and master
branch in lib seL4/libsel4muslcsys? The lib seL4/libsel4muslcsys is the
foundation of libmuslc, it shoud be a libc for any seL4 program, and there
should be no diference among any branches.
https://github.com/seL4/libsel4muslcsys/commits/camkes
Xilong Pei
Tongji University
2015/5/29
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 all,
I just wanted to take the chance to introduce Hesham ALMatary and myself.
Hesham participates in Google's Summer of Code in the lowRISC
organization and I am his mentor. During summer, Hesham will port seL4
to the RISC-V architecture, specifically for the lowRISC project.
Please find more details here:
http://www.lowrisc.org/blog/2015/05/summer-of-code-students-for-lowrisc/
Hesham and I will keep you updated about the progress, I believe he will
also give updates in his blog: http://heshamelmatary.blogspot.it/.
Best Regards,
Stefan
Hi,
I am trying to compile example from 'Download' tutorial under Cygwin.
http://sel4.systems/Download/
What I get is:
[KERNEL]
[BF_GEN] arch/object/structures_gen.h
[BF_GEN] plat/machine/hardware_gen.h
[BF_GEN] api/types_gen.h
[CPP] src/arch/ia32/machine_asm.s
[AS] src/arch/ia32/machine_asm.o
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S: Assembler messages:
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:15: Warning: .type
pseudo-op used outside of .def/.endef ignored.
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:15: Error: junk at
end of line, first unrecognized character is `o'
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:20: Warning: .size
pseudo-op used outside of .def/.endef ignored.
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:20: Error: junk at
end of line, first unrecognized character is `o'
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:22: Warning: .type
pseudo-op used outside of .def/.endef ignored.
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:22: Error: junk at
end of line, first unrecognized character is `i'
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:26: Warning: .size
pseudo-op used outside of .def/.endef ignored.
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:26: Error: junk at
end of line, first unrecognized character is `i'
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:30: Warning: .type
pseudo-op used outside of .def/.endef ignored.
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:30: Error: junk at
end of line, first unrecognized character is `i'
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:34: Warning: .size
pseudo-op used outside of .def/.endef ignored.
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:34: Error: junk at
end of line, first unrecognized character is `i'
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:36: Warning: .type
pseudo-op used outside of .def/.endef ignored.
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:36: Error: junk at
end of line, first unrecognized character is `i'
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:41: Warning: .size
pseudo-op used outside of .def/.endef ignored.
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:41: Error: junk at
end of line, first unrecognized character is `i'
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:43: Warning: .type
pseudo-op used outside of .def/.endef ignored.
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:43: Error: junk at
end of line, first unrecognized character is `i'
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:49: Warning: .size
pseudo-op used outside of .def/.endef ignored.
/home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:49: Error: junk at
end of line, first unrecognized character is `i'
..........
What to do with it?