Since our original plan to have the L4Re::Treat in june 2020 fell victim to a global pandemic, we gave it another try in mid september - with some care to enable distancing. This time our yearly trip into the nature led us not far from home to the Saxon Switzerland near Hohnstein where we stayed in an old renovated farmers building in the forest. The good weather allowed us to go hiking and on a boat trip on the Elbe river and to follow some self-chosen projects and ideas on the terrace. Let’s hear from some of our collegues:

At the campfire


I was working on supporting the gcc address sanitizer for L4Re. The address sanitizer is a powerful debugging tool helping to detect invalid memory accesses at runtime. There was previous work from SteffenL so I did not have to start from zero. My main work was to adapt the existing changes to a newer gcc version and to consider recent changes in the L4Re environment. I was not able to finish the project yet.

Working for 4 days on such a beautiful and quiet place was a pleasure for me! I enjoyed the events (hiking, boat trip), discussions and eating together with my colleagues.


Although I only attended one day, I started my investigation into a generic user mode tracing framework. There are numerous use cases for having such a framework which allows turning on certain actions at runtime. Function instrumentation, runtime statistics or even logging to name just a few. Beside being generic, the main objective is that it has to be really fast when those event points are turned off.

Similar to the Linux kernel ftrace framework, runtime code patching can be one possible solution. Also Fiasco itself is using runtime code patching for the Jdb trace buffers. To implement something similar for user mode, several tasks/problems had to be tackled:

  1. The places within the code which need to be patched have to be identified automatically.
  2. The memory pages for code are mapped read only. Somehow we need to be able to patch those memory locations anyway.
  3. Advanced use cases like multi-threaded applications have to work as well. Cache invalidation needs to be investigated.

I was able to solve 1. by using the asm directives pushsection/popsection together with a special linker script to create a list of patchable memory locations. Ignoring 1. and 2., a small proof of concept was implemented to see if this is feasible which turned out to be true. The next steps are to work on 2. and 3. and all the other problems which will show up along the way.


My retreat project was model checking on the IRQ lookup optimization. This splits the Irq array in the GIC (generic interrupt controller) implementation in uvmm in chunks, and assigns each chunk to a four-state cache. The algorithm speeds up the search for pending and enabled Irqs by shrinking the search space from the entire array to those chunks for which the cache indicates that a pending and enabled Irq might exist. The key property I was interested to check is that clients dont miss pending and enabled Irq due to concurrent updates to the cache. I used SPIN to model threads which set pending and enabled Irqs, and part of the algorithm that updates the cache. On a high-level, the cache update is split in three phases: enter, mark and leave. Time was not sufficient to model the entire algorithm, so I focused on the most complex of these phases: the enter phase. I chose to represent the cache abstractly as an array of bits instead of a single machine word, and made progress in modelling the atomic commands required to model the enter phase, such as atomic load, compare and swap and bitwise operators to manipulate the cache. Half of the verification project remains to be completed.

Personally, I enjoyed the retreat very much and I am glad that I took Hendrik’s suggestion on model checking the Irq lookup optimization. I really liked the boat trip, the visit to the Panoramarestaurant Bastei and enjoyed the nights around the fire with live music from Marius and Manuel! Many thanks to Andreas and Marius for their excellent organization of the event, and thanks to Matthias for the guided bike-tour to the retreat location! :-)


Taking Georg as an Example, I joined L4Re::Treat<2020> as an intern and first-timer. There was very little information about what exactly would await me and since “doing something that you do not have time for at daily work” is basically my everyday task, there was also no specific project for me beforehand. So I had to come up with something secondary of the secondary. Besides settling that, I got to enjoy the daily fireplace chats and learned a few cooking skills. All in all a major fest.


Because I joined Kernkonzept just before the Corona crisis the L4::Retreat<2020> was a welcome opportunity to get together with the team. I went to the location by bike which was a very nice trip along the Elbe to the Saxon Switzerland.

I picked my long running hobby project Bob to see if I could create a project that builds the L4Re hypervisor and a matching Linux guest together. Currently you have to compile L4Re, the Linux kernel and an initramfs manually. Bob together with the basement project provides all ingredients to make the build of such heterogeneous components a one-stop shop. The goal was to build a simple hypervisor demo in one go:

git clone ... demo
cd demo
bob build demo-amd64

Initially I had the idea to build all L4Re components separately in dedicated recipes. This turned out to be not really feasible after studying the L4Re build system in detail. So I got back to have just two L4Re recipes: one for the Fiasco micro kernel and one for L4Re. The Linux kernel and user space components are readily available in the basement recipes already.

Initial progress was quite fast. The kernel and L4Re did almost immediately compile in the recipes when using all tools from the host. Now came the part to reduce those host dependencies to maximize convenience and reproducability. Along the way I patched ham to accept local manifest files because it should be right in the recipes. The x86_64 toolchain in basement was not yet multilib-capable (-m32 was not supported). As this is required by bootstrap I had to spend a fair amount of time to get toolchain into shape. The changes have since landed upstream. Unfortunately the time was up before putting it all finally together.

All in all it was quite a fun time with a good mix of hacking and activities with the team.