- Devel - lists.sel4.systems

How are capabilities assigned
by Sebastian Lau 16 Feb '15

16 Feb '15

I have a question, how are capabilities assigned or given to processes? Is it through the kernel or can the root process (like init etc.) assign capabilities as well? Also is IPC managed by calls to the kernel? I have in mind to base something off of seL4 in the future but I'm not quite ready to start though and just want to get an understanding of how things work.

2 3

am335x patches
by Tim Newsham 16 Feb '15

16 Feb '15

This set of fixes pushes AM335x support closer to working. With these patches and the previously submitted bootloader fix (https://github.com/seL4/elfloader-tool/issues/2) sel4 can boot and the sel4test project can run through some of the test cases. There are still some notable ommissions like missing timer and uart features and lack of uart IRQ support. - sel4 kernel - fix up sel4 kernel support for the am335x timer - note: this still receives lots of spurious interrupts - libplatsupport - bring code into line with conventions used by other ports - bring the uart code to life. PIO only for now - support multiple timers - libsel4platsupport - bring code into line with conventions used by other ports -- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com

2 2

am335x test PREEMPT_REVOKE hanging
by Tim Newsham 16 Feb '15

16 Feb '15

while running the am335x port through the sel4 test suite I'm getting a hang in the PREEMPT_REVOKE test. It appears the revoke_thread is getting created but it is never getting executed and hence the wait_for_helper on the revoke thread is hanging indefinitely.. Any idea what would cause this behavior? Tim

2 1

am335x and question
by Tim Newsham 13 Feb '15

13 Feb '15

I'm playing around with the am335x code now and have the sel4 test building but not working properly. If anyone else is interested in playing with this, let me know. I have a question about the boot loader, I'm seeing: if (UART_PPTR < kernel_info.virt_region_start) { printf("Jumping to kernel-image entry point...\n\n"); } else { /* Our serial port is no longer accessible */ } is this necessary? It looks like init_boot_pd established a 1:1 mapping for all addresses lower than the kernel vaddr (which for me is 0xf0000000). Shouldnt the UART be accesible here? I'm seeing the bootloader run up to mmu is turned on but nothing after that and trying to track down where the failure is happening. printf's after arm_enable_mmu are not working for me, and I don't understand if this is due to mmu bringup problems or something else. By the way, I started a "#seL4" channel on freenode IRC. -- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com

2 2

Capability unwrapping
by Norman Feske 13 Feb '15

13 Feb '15

Hello, after a rather long break, I picked up my work with porting Genode to seL4. More specifically, I try to find a good way to realize Genode's RPC mechanism with seL4 IPC. But admittedly, I am struggling a bit. Ideally, each Genode RPC should be realized as a seL4 IPC call. Unfortunately, however, I find the kernel interface too restrictive to do that. There are two issues. 1. Delegation of multiple capabilities at once According to Chapter 4.2.2 of the manual, the kernel allows the delegation of merely a single capability for each IPC whereas the Genode API does not have such a restriction. It effectively renders my idea for working around the capability re-identification problem [1] by representing each Genode capability by a tuple (or triple) of seL4 endpoint capabilities moot. [1] http://sel4.systems/pipermail/devel/2014-November/000112.html Is there a fundamental reason for this restriction? If not, would you be open to make the kernel more flexible with regard to the maximum number of delegations per IPC? 2. Aliasing of unwrapped capabilities with delegated capabilities I understand that the kernel will automatically "unwrap" capabilities if the receiver imprinted a badge into the received capability. In my experiments, the mechanism works as expected. However, how can the receiver determine, which capability got unwrapped if multiple capabilities were transferred? For example, if the sender specifies three capabilities, two of them "unwrappable" and one delegated, the receiver will see 3 capabilities. The delegated cap is written to the specified 'ReceivePath' whereas the badges of the two unwrapped caps can be read from the message buffer. But I see no way for the receiver to decide, which of the three capability arguments got unwrapped and which got delegated. How could the receiver determine this information? 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

8 18

Network stack support
by Andy Helten 13 Feb '15

13 Feb '15

1 0

Status of supporting Beaglebone?
by Kun Cheng 06 Feb '15

06 Feb '15

Hi guys, I happened to find out that beaglebone was listed in the menuconfig. After that I immediately bought a Beaglebone black (Yeah I know beaglebone is different from bb black, but it might succeed. LOL.) and tried to build a image for my bb black . But I found code errors during compilation. I use arm-none-eabi tool chains and the gcc version is 4.8. Errors occurred in sel4test/libs/libplatsupport/src/clock.c which includes platsupport/plat/clock.h but it doesn't exist sel4test/libs/libplatsupport/src/plat/am335x/dm.c has several coding mistakes, like: in function dm_stop_timer() the 'timer' is undeclared in function dm_periodic() dm is undeclared in function dm_get_timer() timer->properties.upcounter = false; but 'false' is undeclared timer->properties.bitwidth = 32; should probably be timer->properties.bit_width = 32; and timer->start = dm_timer_start; timer->stop = dm_timer_stop; should probably be: timer->start = dm_start_timer; timer->stop = dm_stop_timer; also I got a redundant redeclaration of 'ki_end' in sel4test/kernel/src/plat/am335x/machine/hardware.c which the compiler thought the previous declaration of ki_end was in : sel4test/kernel/src/arch/arm/kernel/boot.c So I am just wandering if beaglebone support is still under development? If any of you run sel4 successfully on beaglebone black, please give me some instructions. Currently I removed building platform independent libraries from menuconfig and the compilation went well. But I don't think it's a good idea. And I also find the cross tool chains which is recommend for Debian Wheezy on the http://sel4.systems/Download/DebianToolChain.pml seems to be not working well for compiling beagle configs. I got cc1 options error during compiling which is due to that some of the options are supported by gcc 4.5 or later while the recommended one is based on gcc 4.4. Best regards, Kun Cheng

2 4

Optimizations?
by Raoul Duke 30 Jan '15

30 Jan '15

> Easier to keep the generator simple and let the compiler do the optimisations it already understands. Based on things like the experiences of Tahoe LAFS with compiler optimizations vs. security - let alone plain bugs - I am scared if anybody uses any optimizations at all, especially for serious business. I have not researched the position se4L takes on this. Are the proofs about the before-optimization code, or do they consider the after-optimization assembly output? thanks.

4 4

curious design pattern
by David Greve 28 Jan '15

28 Jan '15

One more and then I'll stop .. I promise. There appear to be numerous instances of the following design pattern: struct message_info { uint32_t words[1]; }; Where the above structure is then allocated locally, initialized and returned by a procedure. Seems like a lot of work to return a uint32_t. I originally assumed that all/much of this code was generated automatically from Haskell .. so I figured it was some odd corner case in the translator. Subsequent discussions, however, have suggested that this assumption is false and that the code was actually written by hand. I could understand using structures to present a unique, statically checkable procedure type signature .. but I can't rationalize the use of the single element array. So .. is there a reason for this curious design pattern? Thanks, Dave

3 2

Haskell error comments
by David Greve 28 Jan '15

28 Jan '15

What is the significance of the various "Haskell error:" comments found throughout the kernel code?

3 6