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 downloaded the latest repository of seL4 from GitHub. When I am trying to
build the kernel using make for ia32 architecture and pc99 platform I am
getting this error :
*yashward@macaroni-09:~/cs736-proj/seL4$ make ARCH=ia32 PLAT=pc99*
* [CC] kernel_final.s*
*src/arch/ia32/kernel/boot_sys.c:75:26: error: ‘CONFIG_MAX_NUM_IOAPIC’
undeclared here (not in a function)*
* paddr_t ioapic_paddr[CONFIG_MAX_NUM_IOAPIC];*
* ^*
*src/plat/pc99/machine/hardware.c: In function ‘maskInterrupt’:*
*src/plat/pc99/machine/hardware.c:54:9: error: implicit declaration of
function ‘pic_mask_irq’ [-Werror=implicit-function-declaration]*
* pic_mask_irq(mask, irq);*
* ^*
*src/plat/pc99/machine/hardware.c:54:9: error: nested extern declaration of
‘pic_mask_irq’ [-Werror=nested-externs]*
*cc1: all warnings being treated as errors*
*make: *** [kernel_final.s] Error 1*
I am trying to compile it on a 64 bit machine with red hat linux machine
operating system on it.
Please help me with this issue.
Regards
Yash
Hello everyone,
Currently I'm going through the source code of seL4. I find function in seL4\src\object\Tcb.c that I can't find it's definition.
In line 59, tcbSchedEnqueue calls a function 'thread_state_ptr_set_tcbQueued(&tcb->tcbState, true)'. However, even with the help of Source Insight I still can't locate the definition of 'thread_state_ptr_set_tcbQueued' . Does anyone know where it is ?
Thanks in advance.
Best regards,
Kenneth.
Hello Everyone,
I'm trying to implement interface which will accept similar syntax like
printf method in c is accepting.
syntax of function in c:
void printer(int i,char* format,...){
}
However I have problem to create valid syntax in idl4 interface definition
for CAmkES. Can somebody help me to create valid syntax for procedure
definition used in interface?
procedure Test {
void printer(in int i,in string format,in ...);
};
Or is this approach even supported?
Also If there is more complex reference guide for idl4 used by CAmkES which
I can use to find answers like this?
Thank you for help and if question is stupid please accept my apologize I'm
just starting to play with this project.
BR,
Casper
Hi All,
I think, on IA-32, sel4 supports multi-core machine.
But I do not how to use that. Here I have two specfic questions.
1. How to assign a specific core to a process/thread? And can I change this
affinity?
2. How to two process/threads communicate via IPC on different cores?
I want to know some implementation details in kernel to support cross-core
IPC.
Could anyone explain its logic or tell me the code for it in the kernel?
Thank you very much.
Best,
Yuxin
Hi All,
I find there have slow and fast path for IPC.
I want to know the performance difference between those two.
More accurate, on x86, how many cycles for slow path round-trip ipc between
two address space?(on single core)
And how many for fast path?
Thank you very much.
Yuxin
Hi All,
In sel4, how can a process/thread get the capability of its virtual address?
I know there is function
vspace_get_cap(vspace_t *vspace, void *vaddr)
But how can I know the current vspace the process/thread is in?
Thank you very much.
Yuxin
I'm new to seL4 (and L4 generally). I'd like to initially run my
application functionality in Linux on top of seL4 (x86) and then over time
migrate pieces of its functionality to run directly on seL4 to achieve
finer-grained confinement.
I'm having trouble finding any instructions on how to run a Linux
environment on top of seL4. Either paravirtualized or hardware virtualized
would be ok. So far I found pointers to L4Linux but it appears to need
L4Re. Can anyone point me in the right direction?
Thanks,
Rob
Hi All,
I am a very beginner for sel4, and I very little about its APIs.
Now I have a physical address of memory, I want to know if this address is
mapped into my virtual address space.
And if so, how can I know what virtual address t is mapped in?
Furthermore, how can I share this piece of memory with another
process/thread?
I find there is a function "simple_get_frame_mapping_f“ in
libsel4simple-default library. Its comment is "Request mapped address to a
region of physical memory.”
It is very similar to what I need, but its implementation just returns
NULL.(in sel4\libs\libsel4simple-stable\src\libsel4simple-stable.c)
Thank you very much.
Yuxin
