June 2014 - l4-hackers - example.com Site

EFI boot fails
by Ayad Mostafa 10 Jun '14

10 Jun '14

hello l4-hackers, i'm trying to boot l4 on intel galileo board, but i'm getting error 13 from grub "Error 13: Invalid or unsupported executable format". the error is generated after issuing kernel /bootstrap -modaddr 0x01100000 here is my grub.conf title hw_test0 root (hd0,0) kernel /bootstrap -modaddr 0x01100000 module /fiasco -jdb_cmd=JS -serial_esc module /sigma0 module /moe rom/lwip.lua module /l4re module /ned module /io module /ankh module /ankh.vbus module /lwip.lua module /Aw.lua module /hw_test0 the same setup was tested successfully under qemu i appreciate any help thanks in advance

2 1

Dresden Microkernel Hackers Meet-up
by Julian Stecklina 08 Jun '14

08 Jun '14

Hey fellow microkernel hackers, a lot of us are still in Dresden, but are now scattered across several work places. Let's meet up and have some beer next week. Please vote for when[1] and where[2] until Sunday 18:00 CEST. I'll send one additional mail on Sunday evening to announce the results. Forward this mail as you like. The more the merrier. For all of you too far away: My apologies for the off-topic mail. Julian [1] https://dudle.inf.tu-dresden.de/ukernelbeerwhen/ [2] https://dudle.inf.tu-dresden.de/ukernelbeerwhat/

1 1

Adding hardware access to L4Linux, and killing serial console
by Peter Howard 07 Jun '14

07 Jun '14

Dear all, I'm currently trying to add extra hardware access to L4Linux on the da850. I'm having reasonable success (thanks Taueng!), but have hit a problem with interrupts. I have enabled: * GPIO access (working, with problem described below), * DMA access (working, I think), * Clock access (working, insomuch as the GPIO and DMA stop giving clock errors), * MMC/SD access (not working - and until it does I'm not 100% sure about DMA). (For anyone who knows the omapl138, the mux setup _is_ being handled; part of the bsp code in Fiasco). I hit my current problem when I got the Clock access working, and the GPIO driver started registering interrupts. At that point the serial console stops responding. It prints, but any attempts to type anything fail. Simply commenting out the second half of davinci_gpio_irq_setup() removes the problem. Of course then gpio interrupts can't work (not that I know if they are working yet). So clearly registering those interrupts is affecting the serial console being notified of data pending. I don't expect anyone here to have the answer. But to work out the problem I need to better understand how the virtual serial works in L4Linux. So can anyone give me/point me to a description of how it does work, along with the relevant driver code? Thanks, -- Peter Howard <pjh(a)northern-ridge.com.au>

2 2

Clans and chiefs
by teclis High Elf 07 Jun '14

07 Jun '14

Hi, I just started hacking on Fiasco. Could someone point me to the code where the clans and chiefs are implemented? Where is the code for adding a process to a clan and where is the code where I chief checks to see if a process from another clan is allowed to send a message to a process in its clan? thanks

2 1

error: ext2_lookup: deleted inode referenced
by cem akpolat 07 Jun '14

07 Jun '14

Dear all, I attempt to boot two l4linux instance (one from SATA Disk, the other from ramdisk) on l4re. Both instances boots normally and works fine. I create a file on a filesystem which has access to the SATA Disk. When I reboot the system, all created files permissions show ?????? and kernel message is: error: ext2_lookup: deleted inode referenced Any idea? Cem Akpolat

2 1

Question about cross core IPC
by Yuxin Ren 07 Jun '14

07 Jun '14

Hi I am learning the IPC code in the Fiasco kernel. I have some questions here. If the receiver is not ready, we will add the sender to the sender_list. But I did find any lock to protect the sender_list. So if two threads at different cores try to add themselves to the sender_list at the same time, how can we guarantee the we are safe to do so? When sender and receiver are at different cores, we have to use IPI to communicate. Where is the code on IPC path to use IPI? I imagine the code around IPI should be complex, so it is great if someone can tell me the logic about it, especially about how we protect data structures, using locks or any other lock-free algorithm. Thank you very much. Best

2 3

how to transfer capabilities from server to client
by Yuxin Ren 06 Jun '14

06 Jun '14

Hi, I want to write some code to transfer capabilities from server to client. But I have no idea how to do this as I am not familiar with L4Re and its interface. Could anyone give me some example code or some hints? Thank you very much. Best

3 6

A convenient makefile
by Sören Jonsson 06 Jun '14

06 Jun '14

Hello, I have recently made fiasco and the l4Re, and found that it can be a little tricky. It is a few Debian packages that can be easy to forget to install on your computer etc. In order to make it easier to remember all details I developed the attached Makefile. I have tested it fairly well, and it makes it easy to download and make both l4Fiasco and the l4Re on a Debian or Ubuntu machine. It should be easy to modify to work with Red Hat as well. Documentation: "make envesetup" will install all necessary packages except the "make" package. That has to be installed previously. "make downloads" will download l4Fiasco, the l4Re, and l4Linux to your computer "make kernelsetup" will create the directory fiasco_bld in your current directory and configure the build there. "make resetup" will create the directory l4Re_bld in your current directory and configure the build of l4Re in that directory. I have found the Makefile very convenient, and decided to post it to the l4-hackers mailing list in the case that it can help more people than me. I hope that you like it. Best regards, Sören Jonsson Sweden

1 0

L4-based microkernel on Intel SCC
by Masti Ramya Jayaram 05 Jun '14

05 Jun '14

Hi all, In fact, I am looking for a micro-kernel based hypervisor (like L4:pistachio or Fiasco) to run on the SCC. The only pointer I found was a port of Fiasco OS for Intel SCC recently (http://os.inf.tu-dresden.de/papers_ps/partheymueller-beleg.pdf) and would like to try this. I had a few questions though: a. Is the public version of fiasco compatible with the SCC? If not, is it possible to get it? b. Since SCC uses a different compiler set (much older than gcc 4.4), does the compilation work out of the box? c. Finally, has anyone run L4Linux on top of the SCC? Thanks in advance, Ramya

4 4

seL4 will go open source on 29 July
by Gernot Heiser 05 Jun '14

05 Jun '14

… via the portal http://sel4.systems. This site will start accumulating info through the next few weeks, please check there for updates (or subscribe to the mailing list). For those who haven’t heard about seL4: - it’s the latest L4 microkernel developed by NICTA. - according to the performance figures on http://l4hq.org, it’s the fastest L4 kernel around (let me know if you have performance data to contribute) - it’s the world’s first and only OS kernel with a formal security proof, extending from high-level statements of confidentiality and integrity enforcement all the way down to the binary - it’s proved functionally correct (i.e. bug-free implementation of the spec) - it’s the first and only protected-mode OS with a complete and sound timing analysis, and as such the only credible platform on which to do hard real-time in protected mode - it’s the foundation for DARPA’s high-assurance UAV project (http://trustworthy.systems/projects/TS/SMACCM/) … and it will soon be free! Gernot

2 2