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,
I'm trying to follow the instructions for loading the test image for ifc6410 on this page:
http://sel4.systems/Hardware/IFC6410/
I'm not clear about the second instruction "> ramdisk". It looks to me like this is a redirection with some missing parts. Can you please help me fill in the blanks?
Thanks,
Joel
This is slightly tangential to sel4.. but.. sel4 uses
"repo" to tie together projects that span multiple github
repos. I'm really unclear on the proper workflow for
using repo. I would like to keep my local patches
(and be able to pull down updates from the master
repositories), and I would like to pick patches to
contribute back. What would the normal flow for these
be? Should I be forking each github project that I
work with and then fork a master "repo" project to
reference my versions, somehow?
Is there a good online guide that covers this?
Tim
I have a question, how are capabilities assigned or given to processes? Is
it through the kernel or can the root process (like init etc.) assign
capabilities as well? Also is IPC managed by calls to the kernel? I have in
mind to base something off of seL4 in the future but I'm not quite ready to
start though and just want to get an understanding of how things work.
This set of fixes pushes AM335x support closer to working.
With these patches and the previously submitted bootloader fix
(https://github.com/seL4/elfloader-tool/issues/2) sel4 can
boot and the sel4test project can run through some of
the test cases. There are still some notable ommissions
like missing timer and uart features and lack of uart IRQ
support.
- sel4 kernel
- fix up sel4 kernel support for the am335x timer
- note: this still receives lots of spurious interrupts
- libplatsupport
- bring code into line with conventions used by other ports
- bring the uart code to life. PIO only for now
- support multiple timers
- libsel4platsupport
- bring code into line with conventions used by other ports
--
Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com
while running the am335x port through the sel4 test suite
I'm getting a hang in the PREEMPT_REVOKE test. It
appears the revoke_thread is getting created but it is
never getting executed and hence the wait_for_helper
on the revoke thread is hanging indefinitely.. Any idea
what would cause this behavior?
Tim
I'm playing around with the am335x code now and have the
sel4 test building but not working properly. If anyone else is
interested in playing with this, let me know.
I have a question about the boot loader, I'm seeing:
if (UART_PPTR < kernel_info.virt_region_start) {
printf("Jumping to kernel-image entry point...\n\n");
} else {
/* Our serial port is no longer accessible */
}
is this necessary? It looks like init_boot_pd established a
1:1 mapping for all addresses lower than the kernel vaddr
(which for me is 0xf0000000). Shouldnt the UART be accesible
here?
I'm seeing the bootloader run up to mmu is turned on but nothing
after that and trying to track down where the failure is happening.
printf's after arm_enable_mmu are not working for me, and I don't
understand if this is due to mmu bringup problems or something else.
By the way, I started a "#seL4" channel on freenode IRC.
--
Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com
Hello,
after a rather long break, I picked up my work with porting Genode to
seL4. More specifically, I try to find a good way to realize Genode's
RPC mechanism with seL4 IPC. But admittedly, I am struggling a bit.
Ideally, each Genode RPC should be realized as a seL4 IPC call.
Unfortunately, however, I find the kernel interface too restrictive to
do that. There are two issues.
1. Delegation of multiple capabilities at once
According to Chapter 4.2.2 of the manual, the kernel allows the
delegation of merely a single capability for each IPC whereas the Genode
API does not have such a restriction. It effectively renders my idea for
working around the capability re-identification problem [1] by
representing each Genode capability by a tuple (or triple) of seL4
endpoint capabilities moot.
[1] http://sel4.systems/pipermail/devel/2014-November/000112.html
Is there a fundamental reason for this restriction? If not, would you be
open to make the kernel more flexible with regard to the maximum number
of delegations per IPC?
2. Aliasing of unwrapped capabilities with delegated capabilities
I understand that the kernel will automatically "unwrap" capabilities if
the receiver imprinted a badge into the received capability. In my
experiments, the mechanism works as expected. However, how can the
receiver determine, which capability got unwrapped if multiple
capabilities were transferred?
For example, if the sender specifies three capabilities, two of them
"unwrappable" and one delegated, the receiver will see 3 capabilities.
The delegated cap is written to the specified 'ReceivePath' whereas the
badges of the two unwrapped caps can be read from the message buffer.
But I see no way for the receiver to decide, which of the three
capability arguments got unwrapped and which got delegated. How could
the receiver determine this information?
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
