Greetings. Microkernels rarely appear on Habré, but in the week there was a topic about GNU / Hurd , where various microkernels and famous projects were remembered. Many inaccuracies were said, so I decided to talk about how things are in the industry from our point of view. The fact is that we are actively involved in the development of the Fiasco.OC and Genode projects and are developing on their basis, so we have something to tell about.

A bit of history

      I think the core of Mach is well known, so I will touch on it quite casually. It was developed at Carnegie Mellon University in the late 80s - early 90s, after the project was closed at CMU, it was developed at Utah University and then, in my opinion, it was already called GNU / Mach. GNU / Mach is part of the GNU / Hurd OS. This is a pretty slow microkernel, it only supports x86.
Jochen Liedtke ( by Jochen Liedtke ) at the end of the 90th proposed a new, optimized microkernel architecture, first L3, L4 then. Unfortunately, in 2001 he had an accident and died. L4 is an ideology and is documented in the L4 eXperimental reference manual. Now the latest version of X.2 rev.7Anyone can read this document and program "their" microkernel architecture L4. As a result, quite a few different micronuclear projects appeared in the 00s.

The most famous projects.

      There were many projects, far from all have survived to this day, I will talk about the most famous of the existing ones
1. L4Ka :: Pistachio, Karlsruhe Institute of Technology
This is the team of Jochen Lidtke, they developed the microkernel and environment. Currently, this team does not develop the L4Ka project, but this project has spawned many others.
2. Projects of NICTA Group
      NICTA Group- Information and Communications Technology (ICT) Research Center of Excellence. This organization is engaged in projects in the field of system programming, pattern recognition, artificial intelligence, some kind of nano. In general, the most popular CS destinations, which are very popular in the 00s and in the future. At the same time, this organization does not just invest in reception projects, it conducts them from the idea and reception at the university right up to the products and sales of the company.
      The history of the development of the L4Ka microkernel is very indicative in this regard. First, there was a research project NICTA :: Pistachio-embedded (created on the basis of the L4Ka :: Pistachio microkernel from KIT), then OKL (Open Kernel Lab) was created inside NICTA, which was engaged in the development of products based on the Pistachio microkernel. Then they made their product - the OKL4 microkernel and in the region of 2007 signed a contract with Qualcomm, since then there has been a microkernel in smartphones based on Qualcomm chips. Qualcomm’s recently leaked datasheets include, for example, a description of the L4 api (although I'm not sure I saw it briefly). More recently, OKL4 was sold to General Dynamics.
        L4.verified is a formally verified core on the L4 architecture. This is a scientific development of the NICTA Group, it can be assumed that the track for this project will be like OKL4. The main idea of ​​this project is to mathematically prove the correctness of the kernel implementation. The fact is that microkernels, unlike monolithic-modular monsters like GNU / Linux, are small, and they can be formally verified, that is, a theorem is written on each line of code, and, proving all the theorems, something is proved to be consistent. The L4.verified microkernel proves the conformity of the model implementation, the absence of perpetual cycles, and some other things. The cost of this study was about $ 6 million, the project lasted 7 years. The volume of work is 25 person-years. This is a colossal and very interesting work. Its obvious application is war, security.
seL4 is a security-oriented operating system, I don’t know if the kernel is verified or not. On the NICTA website you can download binaries.
3. MINIX3
        This is a project of the Andrew Tanenbaum team. The main emphasis in the MINIX3 microkernel is fault tolerance and desktop application. I know little about this project, but at the last FOSDEM one of the developers was present, and in Russia there is a small community of enthusiasts.
4. HelenOS
This is a development of students at the Faculty of Mathematics and Physics at Charles University in Prague. This project has been developing for quite some time; the kernel supports modern hardware platforms. And in 2012, they participated in the GSoC. The kernel initially had architectural flaws, for example, the kernel was not completely micro - part of the device driver was still in the kernel. Now, as far as I know, this architectural flaw has been eliminated. I personally do not like the fact that, being positioned as general purpose OS, they do not support normal drivers.
5. TU Dresden Projects Dresden
        University of Technology has a research team from Professor Hermann Härtig. He published and worked together with Jochen Lidtke, and the students under his management developed many interesting projects in the field of operating systems. Old kernels - L4 / Fiasco (the first L4 kernel in TUD), VFiasco (attempt to verify Fiasco, 2005)
Modern kernels:
        Fiasco.OC - a micronucleus written in C ++, built on the concept of Everything Is Object. Supports ARM, x86, ppc, sparc v8. It starts on modern platforms such as pandas. We are actively involved in the development of this project. As far as I know, the authors of the kernel (Adam Lackorzynski and Alexander Warg) left TUD a couple of months ago and organized their startup to support and develop micronuclei.
        NOVA is a micro hypervisor. It was developed by Udo Steinberg, now he continues to develop this hypervisor at Intel.
As you can imagine, microkernels themselves are not functional, so TUD developed a microkernel environment: L4Re - L4 Runtime Environment. This is a set of libraries and application software that can be run on top of the Fiasco and Fiasco.OC microkernels. It includes the paravirtualized L4Linux, a wrapper for using Linux DDEKit drivers (by the way, there is such a DDEKit in GNU / Hurd). This makes it easy to use existing software and use the microkernel in commercial projects. This is a very fast "entrance" to the microkernels, which seems very important to me. The negative point is that TU Dresden extremely rarely uploads updates and there is practically no community work. So for example, we keep the developments and our version of l4Linux in github.
        Genode framwork- Project Norman Feske and Christian Helmuth. They are graduates of TU Dresden and previously worked on the development of a secure graphics subsystem and the development of micronuclei. Now they have their own startup, they are developing a framework for various microkernel (not only) operating systems. Genode, unlike TUD, has regular releases and a roadmap. The sources are on github and everyone can take part in its development. We are also developing this project, we are interested in the Fiasco.OC + Genode framework.
        In other words, micro-nuclear projects from TUD are now moving from the state of “experimental student projects” to a real product on which to build your products. So community growth and engagement is just what we need now.

6. Singularity

We already wrote about this project , I won’t touch

FOSDEM

      This year we took part in FOSDEM and I talked about our experience in using microkernel OS. I did not attend other sessions, as I attended our devroom the first day, and the next day we had a demo section for half a day, where we demonstrated the firmware for the trusted phone on the microkernel, l4linux and Genode. There were projects in the devroom:
    GNU / Hurd, Samuel Thibault talked about him, the most active developer of this project, I think. He was the first to speak, and attended a panel discussion.
Genode labs talked about their work over the past year. They portedGenode framework on pandaboard in 2012. I think this is very significant, and extremely useful for the development of the framework and microkernels, as it adds popularity. We did not participate in the port on pandaboard, although we were the first to launch Genode on real ARM based hardware.
    HelenOS employees were also present, they talked about their plans for the next year, about what is already supported in HelenOS.
    There was Udo and talked about NOVA, that the performance loss of this hypervisor is lower than that of Xen and eSXI, in addition, this hypervisor is supported in Genode, that is, virtual machines can be run in parallel with application software on top of the microkernel.
    There were some new guys who talked about DSL, but this weak relationship has to micronuclei.
From TUD was presentBjoern Doebel , he talked about his Open Source replication framework. This is his research project.
    The demo section was attended by one young man from TU Berlin. TU Berlin has a T Lab department that deals with RnD in the field of information security. In particular, they are developing a trusted phone on the para-virtualized L4Android for Deutsche Telecom.
I liked the reports, and by the way, we will organize Microkernels and Component-based OS devroom next year.

P / S / And also, last year we held a summer school of system programming, and now we are looking for students who want to find themselves in the field of Computer Science and system programming. In order to get to our team, you need to look at the first three lectures ( 1 ,2 , 3 ) and complete tasks from them. The solution needs to be posted on github and send me a link to the mail sartakov@ksyslabs.org.

P / P / S / If interested, I can tell you about the main trends and challenges in the field of system programming in recent years.

P / P / P / S This year we are preparing a new school, but more on that later