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
I was following the CAmkES "Getting Started" tutorial on the seL4 website
and followed all the instructions. Here is the link:
https://sel4.systems/Info/CAmkES/GettingStarted.pml
I managed to get the sample application to run in QEMU (Quick Emulator)
like the instructions said. I tried loading the sample application onto the
Sabre Lite Board through tftp booting using minicom. However, once I try to
boot the .elf file, it displays the memory address and nothing else happens.
Is there any configuration file that I need to change to make the sample
application run on my Sabre Lite Board? Or is there something else that I
am missing?
Thanks,
Bryan
Dear all,
I am forwarding the Call for Participation of the Microkernel devroom at
FOSDEM 2016. The original announcement did not pass the mailing list
gatekeeper for some reason.
Martin Decky
-------- Forwarded Message --------
Subject: FOSDEM 2016 - Microkernel devroom CfP
From: Jakub Jermar <jakub(a)jermar.eu>
FOSDEM 2016 - Microkernel devroom
CALL FOR PARTICIPATION
The developers of several free and open-source microkernel-based
operating systems will meet at FOSDEM 2016 [1] in Brussels, Belgium and
will share a developer room. The devroom is currently looking for
content in the form of talks and activities related to the area of
microkernel-based operating systems. Possible topics include, but are
not limited to:
* project introductory and status update talks, demos
* architecture, subsystem and components' design
* hardware and device drivers
* tools, languages and toolchains
* development, debugging, testing and release engineering
* best practices and learning from mistakes
* trends and challenges
* community and life with a microkernel project
Please use the Pentabarf [2] system to submit your proposals. You do
not need to create a new account if you already have one. When in doubt,
please use the devroom mailing list [3]. The deadline for your CfP
submissions is on 2015-12-13. Make sure to include the following in your
proposal:
* title of your talk
* abstract (one or two paragraphs)
* your full name
* your short bio
* a picture of yourself
* duration of your talk
The official devroom schedule (along with the accepted talks) will be
announced on 2015-12-18 in the devroom's mailing list and the speakers
will be notified via e-mail. The schedule will also be published on the
FOSDEM web and in the FOSDEM booklet.
The devroom will take place on Saturday of January 30, 2016 at ULB
Solbosch Campus in Brussels, Belgium [4].
About FOSDEM
FOSDEM is a two-day event organised by volunteers to promote the
widespread use of free and open source software. Taking place in the
beautiful city of Brussels (Belgium), FOSDEM is widely recognised as the
best such conference in Europe. FOSDEM covers a wide spectrum of free
and open source software projects, and offers a platform for people to
collaborate. To this end, FOSDEM has set up developer rooms (devrooms)
with network/internet connectivity and projectors where teams can meet
and showcase their projects. Devrooms are a place for teams to discuss,
hack and publicly present latest directions, lightning talks, news and
discussions. Besides developer rooms, FOSDEM also offers main tracks,
lightning talks, certification exams and project stands. Every year,
FOSDEM hosts more than 5000 developers at the ULB Solbosch campus.
Participation and attendance is totally free, though the organisers
gratefully accept donations and sponsorship. No registration necessary.
About the devroom
Since its inception in 2012 the Microkernel devroom has been part of
each FOSDEM conference. It has become a sort of an institutionalized
tradition since then. To this date over a dozen projects have
participated in one way or another, delivering forty talks and other
contributions in total. The goal of the Microkernel devroom has been to
bring the various projects together and let them share ideas,
cross-pollinate and socialize. Each year the devroom is organized by one
of the projects based on a system of rotating presidency from the pool
of projects that opt in. In 2016 it is HelenOS' turn again.
Social events
It has become a tradition that the microkernel projects dine together
somewhere in downtown Brussels after the devroom closes. The year 2016
will not be any different, so there is going to be a microkernel family
dinner on Saturday night. The exact location and time will be specified
later. Consult the FOSDEM web and other projects for additional social
events such as the famous FOSDEM-organized Friday Beer Event and the
FOSDEM-arranged free sightseeing tours for spouses.
Important dates
2015-10-23 CfP
2015-12-13 CfP deadline
2015-12-18 Devroom schedule published, speakers notified
2016-01-30 Microkernel devroom takes place
2016-01-30 Microkernel family dinner
Links
[1] http://fosdem.org/2016
[2] https://penta.fosdem.org/submission/FOSDEM16
[3] https://lists.fosdem.org/listinfo/microkernel-devroom
[4] https://fosdem.org/2016/practical/transportation/
I have a question about the way that derived capabilities are handled in seL4. I'm posting here in the hope that somebody might be able to share some insights about this part of the design.
As I understand it, early versions of seL4's Mint operation allowed multiple derived levels of capabilities. (I'm thinking, in particular, of the description of Capability Derivation Trees, or CDTs, on Pages 36-38 of Dhammika Elkaduwe's thesis.) This, for example, would make it possible to construct a system with multiple threads, A, B, and C, each holding a capability to the same object where the capability in C is a CDT child of the capability in B, which in turn is a CDT child of the capability in A. In this scenario, B would have authority to revoke the capability in C, including any further CDT children that C had created, but it wouldn't typically have authority over other children of the original capability in A.
So far as I can tell, this is not possible in the current version of seL4. Specifically, the reference manual (API version 1.3, Page 11) indicates that "Ordinary original capabilities can have one level of derived capabilities" and that "Further copies of these derived capabilities will create siblings". In the scenario above, this suggests that the capabilities in B and C would be siblings and that there would be no easy way for B to track any additional sibling copies that C might have created.
Can someone provide background about why this change was made? I've seen that Dhammika had a working implementation of the original design, and although it was still technically limited to 128 levels, this was not found to be an issue in practice. But perhaps there were security concerns or problems with verification? Or maybe people who worked with the original system found that it wasn't useful in practice, or that it was hard to use effectively? Or maybe I've just misunderstood some aspect of the above?
Thanks and best wishes,
Mark
Hello,
I have been experimenting on the SabreLite imx6 board and the network
driver provided by libethdrivers.
I've been successful in getting it to work "out of the box" and, testing
with a simple UDP echo client running on Linux, I've verified that I can
send and receive small UDP messages as long as they were not fragmented.
I immediately noticed that the fragmentation performed by Linux was
different than the one performed by lwip on seL4. Lwip was successfully
reassembling a message fragmented in two, but it wasn't fragmenting it when
sending it back out.
The driver reports an MTU of 1536 and this is likely the reason for lwip
not to perform output fragmentation. Hacking the driver slightly, I had it
report an MTU of 1500 to lwip, while using the 1536 value internally to
allocate buffers. This has allowed me to successfully receive and send UDP
messages of up to ~2950 bytes (ie. under 3 frames).
When size is increased above that amount, lwip starts behaving
"suspiciously" and I can only see the two first two fragments going out,
while the third one is never sent (causing the linux host to timeout on the
IP reassembly). Debugging the driver, it seems the third fragment is never
actually written
Has anybody had any experience in getting bigger UDP messages across?
Any suggestions on how to enable it if not?
Thanks,
-Andrea
tl;dr: Got UDP working on imx6 with libethdrivers+lwip, can only send up to
2950 bytes, would like to send more, help needed.
--
Andrea Sorbini
Software Engineer
asorbini(a)rti.com
+1.408.990.7475
www.rti.com
RTI - Your systems. Working as one.
I am working on a UART device driver in camkes for AM335x.
When I load the image on the board I get this error:
Creating object frame_drv_group_bin_42 in slot 596, from untyped 1f6...
device frame, paddr = 0x48022000, size = 12 bits
capDL-loader :: << Error: Failed to find device frame at paddr = 0x48022000
>>
I am reasonably confident the address is correct,
(https://github.com/seL4/libplatsupport/blob/master/plat_include/am335x/plat…)
Looking at the source It seems capDL-Loader wants to find this device
frame in bootinfo
https://github.com/seL4/capdl-loader-app/blob/master/src/main.c#L731
Any help on how capDL-loader builds bootinfo would be appreciated.
Jeff
--
Jeffrey L. Hieb
Department of Engineering Fundamentals
University of Louisville
Louisville Kentucky 40292
(502) 852 0465
