- l4-hackers - example.com Site

Question about handshake_receiver in IPC
by Yuxin Ren 02 Jul '14

02 Jul '14

Hi, I find before handle IPC, we always call handshake_receiver function. A basic question is why do we need to handshake receiver? What do we do when we handshake_receiver? Another thing I note is we have separate handshake_receiver (remote_handshake_receiver) if the receiver is on the other core. What is the difference between those two handshake_receiver functions? Thank you very much. Best, Yuixn

2 1

real time application example in l4re
by cem akpolat 01 Jul '14

01 Jul '14

Dear all, is there any example for a real-time applications running on l4re? I see in the slides prepared by TU Dresden that there is always a separation between realtime and non-realtime, but I couldn't find any example for that. If there is an example, could you refer it? Cheers, Cem Akpolat

2 1

IO configuration language
by Martin Schröder 25 Jun '14

25 Jun '14

IO supports two configuration formats. The (legacy format ?) "IO configuration language" and a (newer ?) lua based one. Except for some examples and the syntax file ioconfig.vim I could not find much documentation. But anyway I am running into trouble when using the lua based one instead of my existing (so far working) old one. I have something like this (two network cards with each dmamem): === (old one) hw-root { NIC0 => new Device() { .hid = "foodevice"; new-res Mmio(0x111 ... 0x222); } NIC1 => new Device() { .hid = "foodevice"; new-res Mmio(0x333 ... 0x444); } DMAMEM0 => new Device() { .hid = "dmamem"; new-res Mmio_ram(0x80000, 0); } DMAMEM1 => new Device() { .hid = "dmamem"; new-res Mmio_ram(0x80000, 0); } } client0 => new System_bus() { "foo.dev0" => wrap(hw-root.NIC0); "dmamem" => wrap(hw-root.DMAMEM0); } client1 => new System_bus() { "foo.dev1" => wrap(hw-root.NIC1); "dmamem" => wrap(hw-root.DMAMEM1); } === and want to convert it into something like this: === (new one) Io.hw_add_devices { NIC0 = Io.Hw.Device { hid = "foodevice" Io.Res.mmio(0x111, 0x222) }, NIC1 = Io.Hw.Device { hid = "foodevice" Io.Res.mmio(0x333, 0x444) }, DMAMEM0 = Io.Hw.Device { hid = "dmamem"; Io.Mmio_data_space(0x80000, 0x80000); }, DMAMEM1 = Io.Hw.Device { hid = "dmamem"; Io.Mmio_data_space(0x80000, 0x80000); } } local hw = Io.Hw Io.add_vbusses { client0 = Io.Vi.System_bus(function () dev0 = wrap(hw:match(NIC0)); dev1 = wrap(hw:match(DMAMEM0)); end), client1 = Io.Vi.System_bus(function () dev0 = wrap(hw:match(NIC1)); dev1 = wrap(hw:match(DMAMEM1)); end) } === So dev0 = wrap(hw:match(NIC0)); seems to be wrong. In all the examples I fould the hid-string dev0 = wrap(hw:match("foodevice")) is always used. So three questions: 1) How can I use the device in the example if the hid is not unique? I even tried wrap(hw:device(NIC0)) but this does not work eiher. 2) How can I set the device name for client0/client1 into "foo.dev0" for dev0 as in the (old) example above? dev0.set_name("foo.dev0"); seems not to be the right one. 3) Is Io.mio_data_space(0x80000, 0x80000) the right replacement for "new-res Mmio_ram(0x80000, 0);" ? Best regards, Martin

2 7

A conceptual question about IPC
by Jorge Ventura 24 Jun '14

24 Jun '14

I have been reading several papers about micro kernel and they explain how critical the IPC design is for kernel performance, most of them point to use of register, incomplete context switch and so on. Here is my question: Is not possible to use the MMU and just execute a page swap between address spaces ? Make changes in the page table is not something fast ?

2 1

Setting task priority in loader configuration script
by Peter Howard 24 Jun '14

24 Jun '14

Dear all, I've looked through the documentation, but it doesn't seem clear how you set the priority of a task as you create it from a .cfg script. I've tried: loader:start({caps = { ... }, l4re_dbg = L4.Dbg.Warn, log = {"foo", "red" }, priority = 100}, "rom/foo"); But I'm not seeing any difference from that, with priority < 0x10, > 0x10, or unset. (I got the 0x10 value from http://os.inf.tu-dresden.de/l4env/doc/html/loader/p_script.html) So, is that the correct way? If now, what is the correct way to specify priority? Thanks, -- Peter Howard <pjh(a)northern-ridge.com.au>

2 3

Fwd: l4shmnet and its structure
by cem akpolat 22 Jun '14

22 Jun '14

Hi, "So I understand that you configured one L4Linux with two l4shmnet network interfaces and one of those two did not work? Hard to tell for me what's wrong without more info." I added printf lines to shmc.c file and the output I get the following output while a connection is created btw. the server and the first client. //*************************************// client1 | l4shmc_create : starting client1 | l4shmc_create : l4re_ns_register_obj_srv returned error client1 | l4shmc_attach_to : starting client1 | l4shmc_attach_to : no problem, returning L4_OK client1 | l4shmc_add_chunk : starting client1 | l4shmc_add_chunk : executing chunk_get client1 | l4shmc_add_chunk : in the else side due to offs client1 | l4shmc_add_chunk : returning L4_OK client1 | l4shmc_add_signal : starting client1 | l4shmc_add_signal : returning L4_EOK client1 | l4shmc_get_chunk_to :starting server | l4shmc_get_chunk_to :starting net shm0: shm0: L4ShmNet established, with 54:42:00:00:ff:01, IRQ 66 client1 net shm0: shm0: L4ShmNet established, with 54:42:00:00:ff:02, IRQ 65 And the following output between the server and the second client: //*************************************// client2 | l4shmc_create : starting client2 | l4shmc_create : l4re_ns_register_obj_srv returned error client2 | l4shmc_attach_to : starting client2 | l4shmc_attach_to : no problem, returning L4_OK client2 | l4shmc_add_chunk : starting client2 | l4shmc_add_chunk : executing chunk_get client2 | l4shmc_add_chunk : in the else side due to offs client2 | l4shmc_add_chunk : returning L4_OK client2 | l4shmc_add_signal : starting client2 | l4shmc_add_signal : returning L4_EOK client2 | l4shmc_get_chunk_to :starting server | l4shmc_get_chunk_to :starting net shm1: shm1: L4ShmNet established, with 54:42:00:00:ff:04, IRQ 67 //*************************************// As you can see, the second client does not respond after the connection established message from the server. I have two questions regarding this problem: 1) Is the message "l4re_ns_register_obj_srv returned error" the source of the problem? If so, then what might be the reason for this error? And also, why does the connection work properly between the first server and the client if that is the source of the problem? 2) Could it be the case that the second client obtains the same IRQ number with the first client(IRQ 65) or the server (IRQ66 or 67), and therefore the trigger signal is not received by the second client? How can I detect this problem? Which function is responsible for the IRQ numbering? As you can see, the second client does not respond after the connection established message from the server. I have two questions regarding this problem: 1) Is the message "l4re_ns_register_obj_srv returned error" the source of the problem? If so, then what might be the reason for this error? And also, why does the connection work properly between the first server and the client if that is the source of the problem? 2) Could it be the case that the second client obtains the same IRQ number with the first client(IRQ 65) or the server (IRQ66 or 67), and therefore the trigger signal is not received by the second client? How can I detect this problem? Which function is responsible for the IRQ numbering? Thank you very much for your time, Cem

2 3

RCU period
by Yuxin Ren 22 Jun '14

22 Jun '14

Hi I do not understand the period in Rcu class. How do we use it? Now it is 10ms, how is it calculated? Thanks a lot.

2 3

How does Fiasco implement printf
by Yuxin Ren 22 Jun '14

22 Jun '14

Hi, I think printf usually invoke system call. But in Fiasco only one system call is capability invocation. So what capability is invoked by printf? Or Fiasco implements printf in user level, so printf triggers a normal IPC? Thank you. Best

3 2

Question about seL4 on July 29th
by Jorge Ventura 21 Jun '14

21 Jun '14

Anybody knows what kind of Open Source License is expected to be deployed with seL4 on July 29th ?

3 2

Istream beginner help
by ba_f 17 Jun '14

17 Jun '14

Hallo Hackers, for design reason i would like to use separate Istream & Ostream instead of IOstream with call(). ostream.send() does work, but i cant manage istream.receive(). It keeps waiting for ever. I did edit the client from pkg/examples/clntsrv, the server sends the result, so there should be something to receive. What am i missing? // pkg/examples/clntsrv/myClient.cc static L4::Cap<void> server; static int func_neg_transmit() { L4::Ipc::Ostream oStream(l4_utcb()); l4_uint32_t val = 8; s << l4_umword_t(Opcode::func_neg) << val; int r = l4_error(s.send(server.cap(), Protocol::Calc)); } static int getResult() { L4::Ipc::Istream iStream(l4_utcb()); l4_uint32_t val; // while ( iStream.has_more<l4_uint32_t>()) { // doesnt work neither int r = l4_error(iStream.receive(server.cap())); printf("receive success\n"); // doesnt pass here iStream >> val; } int main() { server = L4Re::Env::env()->get_cap<void>("calc_server"); func_neg_transmit(); getResult(); return 0; } THANK YOU

2 1

Multiple IPC_Gate channels per task
by professor xavier 13 Jun '14

13 Jun '14

Hi, I am a newbie to L4 and have a simple question about the IPC_Gate feature. Can a single task support multiple IPC_Gates? If so, can you please provide an example of a *.cfg script that shows this? Thank you. px

2 1

l4shmnet and its structure
by cem akpolat 13 Jun '14

13 Jun '14

Dear all, As far as I tested, l4smnet.c file establishes a communication channel between client ann server l4linux and I asked couple of weeks ago about the posibility of multiple clients and one server example and Adam recommended me to use one of the l4linux, in this case server, as a router. That is exactly the way that I am following. For this reason, I tried first of all a simple example: one server two clients with two different shm. Interestingly, I couldn't see the second client. I couldn't evaluate whether this trial was logical or not, but if this works for one of the clients why not for the second? Apart from this case, I attempt to convert l4shmnet from two l4linux to multiple case, but this is really not easy. I tried one shared memory first of all, modifying some parts of the code is quite difficult, you can easily encounter a failure such as page_fault. That's why I did two shared memory as mentioned above. My simple question, which way is really more logical, 1- using one shared memory for all clients and server or 2- multiple shared memory for each separate client. Is there any document or source snippet that I can to use a similar structure in l4re. shm code is already here, but it doesn't really give insight into this part. Thanks, Best Regards, Cem Akpolat

2 1

Trouble building l4linux
by Sören Jonsson 10 Jun '14

10 Jun '14

Hello, I have successfully built L4Fiasco and L4Re, and tested it by running the hello test program under quemu. After that I attempted to build L4linux, using instructions from this site: http://wiki.tudos.org/L4Linux/build . Unfortunately, when I came to the stage of "make O=/home/osj/l4linux_bld/" I get an error message "make[2]: *** [/home/osj/l4/l4linux_bld/Makeconf.l4conf] Error 1 make[1]: *** No rule for creating the target "/home/osj/l4/l4linux_bld/Makeconf.l4conf" Is there another web page I should get my instructions from, or is there anything I have missed in my attempt to build l4linux? Best regards, Sören Jonsson Sweden

2 1

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

l4re compilation
by Ramya Masti 04 Jun '14

04 Jun '14

Hi all, I am trying to compile l4re run time from the snapshot (l4re-snapshot- 2014053111) using GCC 4.9 on an x86-64 machine with multilib. The compilation fails with not being able to find cstdio header file. I followed the instructions in http://os.inf.tu-dresden.de/L4Re/build.html. I note that the fiasco kernel itself builds fine from the same snapshot. Some debug information: -------------------------------------------- Output of gcc -v Using built-in specs. COLLECT_GCC=gcc COLLECT_LTO_WRAPPER=/usr/lib/gcc/x86_64-unknown-linux-gnu/4.9.0/lto-wrapper Target: x86_64-unknown-linux-gnu Configured with: /build/gcc-multilib/src/gcc-4.9-20140507/configure -- prefix=/usr --libdir=/usr/lib --libexecdir=/usr/lib --mandir=/usr/share/man --infodir=/usr/share/info --with-bugurl=https://bugs.archlinux.org/ -- enable-languages=c,c++,ada,fortran,go,lto,objc,obj-c++ --enable-shared -- enable-threads=posix --with-system-zlib --enable-__cxa_atexit --disable- libunwind-exceptions --enable-clocale=gnu --disable-libstdcxx-pch --disable- libssp --enable-gnu-unique-object --enable-linker-build-id --enable-cloog- backend=isl --disable-cloog-version-check --enable-lto --enable-plugin -- enable-install-libiberty --with-linker-hash-style=gnu --enable-multilib -- disable-werror --enable-checking=release Thread model: posix gcc version 4.9.0 20140507 (prerelease) (GCC) ---------------------------------------------- Output of make O=build in the src/l4 directory (of what I think maybe relevant parts) === Building package "libstdc++-headers" === bash: line 0: cd: /home/ramya/Downloads/fiasco/l4re-snapshot- 2014053111/src/l4/pkg/libstdc++-headers/../libstdc++-v3/contrib/libstdc++- v3-/include: No such file or directory ....... ....... ....... ....... ....... ....... === Building package "cxx_libc_io" === ... Compiling io_backend.o /home/ramya/Downloads/fiasco/l4re-snapshot- 2014053111/src/l4/pkg/cxx_libc_io/lib/src/io_backend.cc:9:18: fatal error: cstdio: No such file or directory #include <cstdio> ^ compilation terminated. Is this a problem with the GCC version? Any help is much appreciated. Best, Ramya

2 2

Documentation of Sched_context
by Valentin Hauner 03 Jun '14

03 Jun '14

Hi, what exactly is represented by a Sched_context? 'sched_context-fixed_prio.cpp', for example, contains members called '_prio' and '_quantum'. That would suggest that a Sched_context is a schedulable object like a task or a thread. However, the file mentioned above defines some sort of ready queue, too. That would indicate that a Sched_context is some part of the scheduler that organizes the schedulable objects in a data structure? Where are all those classes documentated? Using the search box, the official documentation (http://os.inf.tu-dresden.de/L4Re/doc/index.html) does not offer any information about these. Best regards, Valentin Hauner

2 1