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 …
[View More]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
[View Less]
Hi,
I'm trying to port sel4 into ODROID-XU4 by following the wiki (
https://wiki.sel4.systems/Hardware/odriod-XU)
So far I can successfully enable HYP mode as indicated by
[ 0.198398] [c0] CPU: All CPU(s) started in HYP mode.
[ 0.198433] [c0] CPU: Virtualization extensions available.
as well as generate sel4test-driver-image-arm-exynos5 image.
However, we cant do fastboot in XU4 since it doesnt have usb otg.
Thus, I followed booting from sd card from
https://wiki.sel4.systems/Hardware/…
[View More]General-ARM and copied the image into
the first partition of sd card and do the following:
Exynos5422 # fatload mmc 0 0x48000000 sel4test-driver-image-arm-exynos5
Exynos5422 # bootelf 0x48000000
and here's the output:
## Starting application at 0x41000000 ...
ELF-loader started on CPU: ARM Ltd. Cortex-A7 r0p3
Switching CPU...
ELF-loader started on CPU: ARM Ltd. Cortex-A15 r2p3
paddr=[41000000..4126401f]
ELF-loading image 'kernel'
paddr=[40000000..4002dfff]
vaddr=[e0000000..e002dfff]
virt_entry=e0000000
ELF-loading image 'sel4test-driver'
paddr=[4002e000..40388fff]
vaddr=[8000..362fff]
virt_entry=13868
Enabling hypervisor MMU and paging
Enabling MMU and paging
Jumping to kernel-image entry point...
�⧹I�AIq9Fy6 1)�a&I99)�6� Yq��摦P�^б��F��^/A�yyyyyyyyy�Y
�)aay���XY�ǡyQ)�q��O�a@ Ia)!Fyaay
�)��XY��������.6I�)&FvF�6fF�����VƑ�y��P�)aay���XY�ǡyQ)�q��O�a@ Ia
Is it expected? or am I doing something wrong? Any help would be
appreciated.
Best,
--
Norrathep (Oak) Rattanavipanon
M.S. in Computer Science
University of California - Irvine
[View Less]
Dear all,
I have some questions about building VMM on top of seL4. I know there is a
sel4-based VMM on github (https://github.com/smaccm/sel4arm-vmm-manifest)
Gernot also told me that this version of VMM does not support multi core.
My questions are:
1) Can this single core version of VMM be run on top of multi-core sel4
just using one core without modification?
2) If not, what supports are missed in the multi-core version of sel4? I
assume single-core version applications should be compatible …
[View More]with
multi-core micro kernel.
3) If my assumption is wrong, what do we (as VMM developer) need to add to
the VMM code to make it workable on the multi-core seL4?
thanks
Peng
[View Less]
On 11 Apr 2016, at 8:09 , fresheneesz <notifications(a)github.com<mailto:notifications@github.com>> wrote:
I imagine this isn't the right place for this, but i can't find a better one.
The correct one is this (devel(a)sel4.systems<mailto:devel@sel4.systems>)
I see the performance comparisons at http://l4hq.org/docs/performance.php are run on all different processors. In its current form, the performance numbers here are completely useless. It would be very informative to …
[View More]have real performance benchmarks where the exact same processor is used for every OS in comparison. Otherwise, what am I supposed to do with those number?
You’re right that comparisons across different processors are of limited power, but they aren’t useless either, especially when expressed in cycles (and ideally coupled with an understanding of the underlying hardware, eg the insane pipeline depth and speculation of the Pentium 4).
However, given that these are different implementations spanning 20 years (some written in assembler), it isn’t possible to run them on the same hardware.
The key observation is that no-one has ever done better on any of those processors.
Gernot
________________________________
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.
[View Less]
Hi, all
first, I do not speak English well. please answer to me easily.
i'm studying seL4 kernel source code.
i have some questions.
1. What is domain? i read manual but i don't understand well.
I hope that you explain to me in detail about the domain.
2. What is the maximum number of threads that can be created in one domain?
3. Usually there is a function to create a new thread in kernel source code.
but i can't find the function in seL4 kernel source code.
What is the way to create a …
[View More]new user thread in seL4? also, what is the way to exit user thread in seL4?
thanks.
[View Less]
Hi all,
I’m trying to understand the seL4 kernel source code. I think the memory mapping between physical memory and virtual memory is a key point since it is directly related to how kernel functions and manage badges. I noticed that the kernel turns on the paging very early. Can someone help me or point out some resources how kernel memory is allocated? Especially how during and after the booting what the kernel memory snapshot looks like and things like that.
For example, I traced to …
[View More]map_kernel_window() function and even before that there is some pptr to paddr conversion. I would really appreciate the help.
Thanks
-Dan
[View Less]
