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
Is there an easy way for one task to share address space with another task
directly or does it have to go through the kernel/os and be emulated?
I noticed that support for mapping memory is mostly low level assignment of
physical frames to virtual frames via page tables, unlike Mach which uses
memory objects.
I noticed that unlike mach, L4 does not directly manage virtual memory, but
instead farms out address space, page directory, and page table
capabilities to userspace and lets userspace decide what pages to map and
where.
Does this imply that virtual memory abstraction is userspace responsibility?
Hi,
I'm experimenting with some x86 code that involves reading from I/O ports.
I noticed--much to my surprise--that I don't have to use seL4_IA32_IOPort_In8()
to read from a port; my program works just as fine using the "in" assembly
statement directly, without any caps.
The TSS segment limit is initialized with 0x67
https://github.com/seL4/seL4/blob/master/src/arch/x86/kernel/vspace.c#L158
and the "I/O Map base address" is initialized with 0 (zero)
https://github.com/seL4/seL4/blob/master/src/arch/x86/kernel/vspace.c#L43
I believe the result is that ring 3 programs can access I/O port addresses
below 0x388 (0x67 * 8) without triggering a protection violation.
So my question is: Shouldn't capabilities be required for all ports? Or what
what is the reason or motivation behind this?
Thanks,
Josef
On the sel4.systems website, it says that the site is served by the Apache
web server on Linux atop sel4. How does that work and could you operate the
Linux middleware just on top of sel4, maybe something like mer?
Hi,
I am a beginner to seL4 as well as microkernel, and very interested
in it. I think it is great in terms of its minimality and formally
verified security. However, I have some questions about it,
(1) How is its performance compared to other monolithic kernel,
say, Linux. Could it make use of multicore, multiprocessor to
enjoy the performance scalability?
(2) How is its ecosystem, fox example, how to support new hardware,
does it need write the driver from scratch or could it make use of
Linux driver? And how to write application on it, or, could it run
Linux application without modification?
(3) How is its virtualization support, could it run Linux vm, and
does it need any modification to the guest os?
Cheers,
Qing Wei
Hi,
Thank you for all your efforts and time. I believe the user community is
the main success key for all open source projects. Many users and
researchers, do not have enough time to read, download and evaluate all the
source code in order to investigate a system to see if it is suitable for
their research or usage. Usually they will go for clean systems which are
easy to use, simple to understand, well documented and have a strong
community beside the commercial support to ask and get help in case they
had a problem.
Here are some comments which may help to increase the number of users and
developers for seL4:
A) I suggest to add some howtos to the website. It's better to be a wiki
like system so other individuals, researchers and students can help in
writing some titles.
Some interesting topics (at least for me as a beginner in micro-kernel)
could be:
1- Running Linux/Android on top of seL4.
2- Writing a simple user application with a use case (not just the SOC).
3. Examples on real-time application.
4- Writing a service (could be a device driver, file-system, etc) for seL4.
5- Documents on using possible run-times like Genode.
6- Documents or case studies on porting an opensource software from Linux
or POSIX based system to directly run om seL4.
B) Providing ready to use download binary images for supported platforms
can also accelerate growth of community.
C) A research areas page which can suggest researchers some ideas to chose
a title and do their research to expand seL4 could also be useful. Ideas
like rump-kernels, lib-OS, visualization (x86/ARM), etc seems to be
possible research titles on seL4. I have seen the
https://sel4.systems/GettingStarted/ page and I think other than CAmkES,
ports and Qubes there could be many more titles.
D) I know the major development platform of seL4 has been the Arm
architecture, but optimizing the code to utilize the x86 architecture
including virtualization can also bring a lot of attention to this project
to use seL4 as a replacement for Linux-KVM and Xen in the cloud, IoT or
real time systems when stability and security is a matter.
Also please note, the archive of both development (
https://sel4.systems/pipermail/devel/) and announcements (
https://sel4.systems/pipermail/announce/) mailing lists are not accessible
trough the website.
I'm an OS researcher and a senior system engineer (mostly Linux) with a
limited time, but I can help in some parts if you think it may be useful.
Thank you again!
Best Regards,
Mehdi
Is there a mailinglist or forum anywhere for people interested in using
seL4? I realized this is a dev list and may not be the right place to ask
technical supportr questions.
