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
Dear all,
I follow the official step (https://github.com/seL4/refos-manifest) to
build RefOS and it occurs the following error message.
In file included from
/home/chi-wai/Workspaces/microkernel/RefOS/libs/librefos/src/sync.c:16:0:
~/Workspaces/RefOS/stage/arm/imx31/include/refos/refos.h:73:1: *error:
unknown type name ‘uint32_t’*
~/Workspaces/RefOS/stage/arm/imx31/include/refos/refos.h:73:23: *error:
unknown type name ‘uint32_t’*
In file included from
/home/chi-wai/Workspaces/microkernel/RefOS/libs/librefos/src/sync.c:18:0:
~/Workspaces/RefOS/stage/arm/imx31/include/refos-util/cspace.h:44:72: *error:
unknown type name ‘uint32_t’*
~/Workspaces/RefOS/libs/librefos/src/sync.c: In function
‘sync_create_mutex’:
~/Workspaces/RefOS/libs/librefos/src/sync.c:49:5: *warning*: ‘seL4_Notify’
is deprecated (declared at
/home/chi-wai/Workspaces/microkernel/RefOS/stage/arm/imx31/include/sel4/deprecated.h:23):
use seL4_Signal [-Wdeprecated-declarations]
~/Workspaces/RefOS/libs/librefos/src/sync.c: In function ‘sync_acquire’:
~/Workspaces/RefOS/libs/librefos/src/sync.c:65:5: *error: invalid
initializer*
~/Workspaces/RefOS/libs/librefos/src/sync.c: In function ‘sync_release’:
~/Workspaces/RefOS/libs/librefos/src/sync.c:74:5: *warning*: ‘seL4_Notify’
is deprecated (declared at
/home/chi-wai/Workspaces/microkernel/RefOS/stage/arm/imx31/include/sel4/deprecated.h:23):
use seL4_Signal [-Wdeprecated-declarations]
make[1]: *** [src/sync.o] Error 1
make: *** [librefos] Error 2
Does RefOS use the old seL4 API ? If it is, which version I need to
downgrade?
Thanks for any help or suggestion,
Gapry.
https://gapry.wordpress.com/
I was looking to upgrade to CAmkES release 2.0. but can't get an example
arm configuration to compile.
I did a a fresh clone using https://github.com/seL4/camkes-manifest.git
and found the ia32_simple_defconfig compiles fine, but not
arm_simple_defconfig
make arm_simple_defconfig
make
[libs/libsel4] building...
make[1]: *** No rule to make target
`/home/sysjeff/Camkes2/libs/libsel4/sel4_arch_include/arm/interfaces/sel4arch.xml',
needed by `include/interfaces/sel4_client.h'. Stop.
make: *** [libsel4] Error 2
looks like the arm directory got renamed to aarch32 and part of the
build system doesn't know?
$ ls /home/sysjeff/Camkes2/libs/libsel4/sel4_arch_include/
aarch32/ ia32/
Is there something simple I am missing?
Thanks,
Jeff
--
Jeffrey L. Hieb
Department of Engineering Fundamentals
University of Louisville
Louisville Kentucky 40292
(502) 852 0465
All,
Noticed an issue with the tutorial for creating a dataport application with CAmkES components. This issue is on https://wiki.sel4.systems/CAmkES%20Tutorial within the Makefile and Kbuild section. You titled the application "helloevent" instead of hellodataport, causing the newly created application to not be able to access the header files needed.
Thanks,
James
Hi all,
On behalf of the Robigalia project I am pleased to announce our first public
release of the core libraries for using Rust on seL4. Currently, this consists
of a raw interface akin to libsel4 and a higher-level "Rustic" interface.
Currently, only x86 is supported. An ARM port is in progress.
We have a website: https://robigalia.org/
And a mailing list: https://lists.robigalia.org/listinfo/robigalia-dev
The goal of the Robigalia project is to promote Rust as a robust choice for
application development on seL4 and has the long-term goal of producing
Robigo, a POSIX-compatible personality on seL4. We're in the initial stages of
development. We are primarily a group of students from Clarkson University,
though other contributors are starting to trickle in.
Currently in-progress is a port of the tutorial from the sel4-tutorials
repositories and examples of doing various things using the libraries we've
created. Beyond those, we're also working on x86 platform support, right now
virtio and PCI bus management.
(I didn't intend on posting this for another week, to finish the tutorial and
high-level library, but it was scooped on HN, so I figured I might as well)
--
cmr
+16032392210
http://octayn.net/
Dear all,
I am looking to purchase a board for a project that will use sel4.
I have the following hardware requirements:
- serial port
- ethernet
- potentially usb
Then, I want to run linux on top of sel4 and have also some native
components. In the linux partition, I would like to control the usb and
potentially the ethernet. In the native components, I am planning to use
the serial port (communication with other components).
I thought the beagleboard black would be a good match. Does anyone tried to
run linux as a guest os on this platform? If yes, is there any
tutorial/example to set it up? Also, any information about how to use the
serial ports and other hardware components?
Also, if you have an experience with any other board (x86 or ARM - the
platform does not really matter), is it possible to indicate what you would
recommend?
Thanks for any help or suggestion,
Julien.
The Trustworthy Systems Team at Data61 (formerly NICTA) is pleased to announce CAmkES release 2.0.0
The new release updates CAmkES to be compatible with seL4 version 2.0.0. It also marks the transition to more frequent and regular releases, as well as switching our release process to semantic versioning, so it's easy to tell which CAmkES releases are source-compatible, or will require updates to user-level code, and also with which seL4 versions they will be compatible.
You can find it at:
https://github.com/seL4/camkes-tool/tree/2.0.0
And a manifest for the 2.0.0 compatible versions of the CAmkES test and example apps:
https://github.com/seL4/camkes-manifest/blob/master/default-2.0.x.xml
Enjoy!
________________________________
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.
For consistency, it seems like it'd beneficial if:
seL4_RangeError
seL4_AlignmentError
seL4_DeleteFirst
seL4_FailedLookup
seL4_RevokeFirst
included an indication of which argument the error applies to. For some of
these errors, not every call has a unique argument which can cause the erorr.
This seems like a relatively straightforward change for me to get acquainted
with the full process of modifying and re-verifying the kernel. Are there
tradeoffs hidden here that would make this undesirable?
--
cmr
+16032392210
http://octayn.net/
Hello,
First of all, thanks for the help you provided previously. After
downloading the virtual machine, everything was fine and I was able to try
seL4 and camkes by using the tutorials. Thanks also for making this
documentation available publicly, it definitively helps a lot to learn the
principles of this operating system.
I still do have some questions regarding sel4 and camkes.
- About camkes, what are the thread mapping rules. How a component is
transformed into one (or several) sel4 threads? Is there a mapping 1
component = 1 thread or is it possible to have multiple threads per
component?
- How can I find the code generated by camkes? The idl/adl code is
ultimately transformed into C code and I was wondering where I could see
the code.
- How the real-time requirements are handled in camkes? For example, how
can I specify that a component is executed periodically every XXX ms. Does
the ADL supports that?
- How can we specify the scheduling constraints? Can we have an
ARINC653-like scheduling where every process has a fixed time slice to be
executed? Since the behavior of the system can be deduced from the
execution time, allocated a fixed time slice also avoid some attacks
- About scheduling, what are the policies actually supported?
- How timing is handled? I tried to use nanosleep() from the libc but it
seems the syscall/service is not implemented. I also tried the timer
example from the sel4 tutorial but when compiling, there is an error (the
function timer_handle_irq needs an IRQ as a parameter). Any idea how to fix
the example and more information about how time is handled?
- is it possible for the OS to load and launch multiple elf at the same
time or other processes must be manually started?
- How capabilities and services are associated? From the example hello-2 in
the sel4 tutorial, I see that a capability is declared (with
vka_alloc_endpoint(&vka, &ep_object)) but I do not understand how this is
associated with the message being sent between both tasks. In other words,
how is it possible to associated a capability with a service. When sending
or receiving a message (for example, by using seL4_SetMR(0, MSG_DATA);),
there is no use of the capability. So, how the kernel can check that the
thread can effectively send a message?
- Is there any efforts to support standards such as ARINC653 or MILS? (even
experimental)
- Is there any significant/big projects that are available online and you
would recommend to learn the OS and its associated libraries?
Hope you do not mind such a list of questions! I really enjoy digging into
the OS and it seems very interesting.
Thanks for any help/comment.
Is it ever possible for seL4 to run on a conventional machine without an
IOMMU if any code that manipulates a DMA capable device is included as
trusted or does DMA automatically void any assurance?
Reason for question: Running seL4 on a system without an IOMMU.
