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 All,
I want to use musl lib c but I'm a little confused on the following two projects: libmuslc and musllibc. I went through their Kconfig and brief intros, so my question now is do I need them both to port/use musl lib c on sel4? It might be a dumb question but I'm stuck here, any help is appreciated.
Best regards,
Kenneth
Hi,
In the Makefile, a program beagle_run_elf is referred, Where can I
get it?
---------------------------------------
# This relies on a helper script to build a bootable image
simulate-beagle:
beagle_run_elf images/sel4test-driver-image-arm-omap3
---------------------------------------
Xilong Pei
Tongji University
2014/11/19
Hi,
I have built an image for my pandaboard, but I have no bootelf
u-boot command, I use go command instead, get the following error:
Panda # fatload mmc 0 0x82000000 sel4test-driver-image-arm-omap3
Panda # go 0x82008000
## Startting application at 0x82008000 ...
after this message, the system is dead. How to do next?
Xilong Pei
Tongji University
2014/11/14
Hello,
I hope you don't mind me spamming the list with my problems.
I have a question about the association of capabilities with
process-local meta data. As far as I understand, the "badging" of
capabilities is the recommended mechanism for servers to attach a
server-local meaningful value to a capability. After having handed out
the capability to a client, it gets this value reported each time the
client (or any other process to which the capability was delegated to)
invokes the capability or delegates the capability back to the server
(e.g., as RPC argument).
Now, I have the following scenario: There are three processes, a factory
(F), a mediator (M), and a client (C). The factory is responsible for
physically allocating objects (e.g., in Genode's case, one example would
be the core process that hands out dataspaces). The mediator is a
process that sits in-between the client and the factory (in the Genode
world, this could the the init process). It keeps records about the
allocation and may use this information to implement a policy. The
client is the designated user of the object. To create an object, C will
call M, which, in turn, will call F on behalf of C:
alloc create
F <-------- M <--------- C
F will create the actual object and a corresponding badged capability
and returns the badged capability as return value to M. Because M wants
to keep records about the lifetime and parameters of the created
objects, it needs to associate a process-local meta-data structure to
the capability.
badged
cap
F ---------> M C
:
(meta data <-> cap)
M stores the meta data in a process-local data base using the cap as
key. It then hands out the cap to the actual client. Sometime later, the
client decides to destroy the object (or perform another operation at M
that takes the cap as argument):
badged
cap
F M ---------> C
|
| uses object (e.g., invoking the cap)
destroy |
(cap arg) |
? <----------+
When M receives the destroy request with the cap of the to-be-destroyed
object as argument, it wants to look up the corresponding meta data from
its data base. But unfortunately, the cap argument of the destroy
function got assigned a new local name within M (some number within the
receive window of M).
How can M find the meta data associated with the allocated object?
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
Hi,
The OMAP3 Beagle board is too out of date, I buy a pandaboard
http://omappedia.org/wiki/PandaBoard , but the omap3 image can't run on this
board. The error information look like these:
-----------------------------------------------------------------
Panda #
Panda # fatls mmc 0
31644 mlo
208784 u-boot.img
4782336 uimage
208273 uinitrd
449 boot.scr
3092757 sel4test-driver-image-arm-omap3
9 file(s), 0 dir(s)
Panda # fatload mmc 0 0x81ff8000 omap3
reading sel4test-driver-image-arm-omap3
3092757 bytes read
Panda # go 0x82000000
## Starting application at 0x82000000 ...
data abort
MAYBE you should read doc/README.arm-unaligned-accesses
pc : [<820024bc>] lr : [<82002194>]
sp : 822d7f78 ip : 00000000 fp : 822d7f84
r10: 00000002 r9 : 00000000 r8 : bfefdf68
r7 : bffabd14 r6 : 82000000 r5 : bfeffd5c r4 : 00000002
r3 : 49020014 r2 : 00000001 r1 : 00000000 r0 : 0000000a
Flags: Nzcv IRQs off FIQs off Mode SVC_32
Resetting CPU ...
resetting ...
-----------------------------------------------------------------
Who can give me some help? thanks first!
Xilong Pei
Tongji University
Shanghai China
2014/11/13
Hi
I am trying to modify the seL4 scheduler as a part of my project. I was
wondering if there is any function present in the library OS like scanf
which can help me in writing an interactive process , to measure the
response time of the scheduler for interactive process.
I was also curious if there is any shell like framework for sel4, from
which multiple processes can be started concurrently and so that they run
in background.
Is there a benchmark suite for generation of performance metrics using the
data structures present in /kernel/src/arch/ia32/api/benchmark.
Please help.
Thanks and Regards
Yash
Hi !
There seems to be a general trend towards using Clang / LLVM in the ARM
area. AFAIK ARM are going LLVM for V8.
Is it viable to do seL4 work with that environment?
Cheers!
