Hurd, seL4, thoughts

In the past 30 years, GNU Hurd has been the official kernel of GNU operating system. The term "kernel" may not be precise here. "The kernel" is the classical concept of the monolithic OS design; in microkernel, there's still the concept "kernel", but it's smaller than monolithic. However, GNU Hurd is not following the simple "kernel + userland" design. GNU Hurd is a collection of servers, which can interact with its microkernel GNU Mach by IPC (Inter Process Communication) for system level requesting. Sounds a little familiar? Try to imagine you're running bunch of dockers on the cloud, and there's a centralized node for scheduling.

Alright, alright, I know you're thinking about Kubernetes, please stop it, really.

Linux is a kernel of the complete OS: GNU or Android. The popular Linux distros are mostly GNU OS, although unnecessary a fullfilled GNU, like Debian/Arch/Ubuntu/SUSE...we call them GNU/Linux distro. Android is not a GNU/Linux distro, because it doesn't abide to GNU's system design. Android OS is independent of GNU OS.

Now we know GNU Hurd is "microkernel + servers + applications" pattern, and the "servers + applications" are in the userland. If we still think "microkernel + servers" a generic kernel concept, then what it will be if we replace this generic kernel with another one?

The battle of microkernels

Since 1970s, there're several microkernels:

Amoeba. Authored by Andrew Tanenbaum who is also known as the author of Minux. The interesting point is that Python programming language was designed for this operating system. Well, I do think we can't anticipate the future, so many interesting changes in our history.

Minix. Well, no need to introduce, huh?

Chorus. It's one of the earliest microkenels (another is Mach), and a real-time distributed OS. In 1997, Sun Microsystems had aquired it for their JavaOS dream. Discontinued, unlucky.

Mach is the microkernel of GNU Hurd, GNU hackers are maintaining a modified version named GNU Mach. Nowadays, L4 is the believerable better one. Microkernel has no traditional system call, so the efficiency of IPC becomes the critical factor for evaluating a microkernel design. Mach is the first generation of microkernels, its IPC was too slow. In the early 1990s, microkernels have received bad reputation for its efficiency, so people had tried a lot of efforts to change the situation. In 1987, German computer scientist Jochen Liedtke had started his 3rd OS design named after him (Liedtke 3rd system, aka L3), but he still found his microkernel too slow. Then he realized that the IPC is the critical factor, then he started his 4th OS design (yes, L4) , and concentrated on IPC optimizing with the hardware specific features. Finally, L4 become the new game changer, it's the second generation of microkernel. L4 brings unbelievable high speed IPC, only costs 0.04us on PentiumIII 500Mhz.

Unfortunately, Jochen Liedtke passed away suddenly on June 10th, 2001. His legacy is still shining in this world.

It's hardly to say the choice of Mach for GNU Hurd by Richard Stallman was wrong. Because Mach has proved itself in the industry, MacOS and WinNT are both based on Mach, and their Mach has been greatly improved, WinNT even re-implemented its microkernel following Mach design. There're two main developers of the original Mach, Avie Tevanian who was Apple's software CTO, and Richard Rashid who was top-level researcher in Microsoft Research. Given this background, we can hardly say Mach design is not powerful enough for an ambitious OS like GNU Hurd, however, GNU Mach is an older version that maybe not to compare to the Mach used by MacOS and WinNT. GNU Hurd hasn't been maintained by its original maintainer for decades. Anyway, today we do have other better alternative.

In 2014, seL4 was released with GPL2, it's a big news to the free-and-opensource OS world. Because seL4 is the only known OS that can full pass the formal verification (so far, full passed for ARM, x86 is still not full passed). seL4 is so extrodinary that we can't ingore it anymore, if we need to enhance or create new GNU Hurd, then I don't think there's other microkernel can be chosen other than seL4.

What if we replace Mach with seL4 for GNU Hurd?

Before answer this question, we have a story to tell, a story about the struggling against L4 in Hurd community in past decades.

There were many efforts that try to port Hurd from Mach to L4, unfortunately, all of the known efforts are failed. However, previous experiments already yielded a lot of experience, which will be very useful for future Hurd development.

In the beginning, Hurd people tried to write a Mach-on-L4 layer to get the ball rolling. Then gradually move the Hurd servers to use L4 intefaces rather than Mach ones. As you may imagine, this approach makes Hurd run slower, but we may expect its future performance when L4 porting is completely done. I have to say this approach looks promising, but sadly, Hurd people finally came to a conclusion that L4 maybe not suitable for a general-purpose operating system design. But I don't think it's a reasonable understand today, because Genode can prove that L4 is suitable from embedded system to general-purpose operating system.

The Hurd/L4 development stopped in 2004. It provided several important experiences and docs about L4 on Hurd.

Hurd people also tried Coyotos and Viengoos which are different microkernels to L4, and these projects are also not proved successful so far. They are out of this article since I only want to focus on L4.

Today, the Hurd-NG (next generation) plan is more focusing on an independent design from the current Hurd. Another effort is x15 which is an alternative to Mach but a brand new microkernel, it's believed to be the more reasonable plan since it can reuse all exiting Hurd components. Mach is the only part will be replaced.

Now let's back to seL4.

First, it's GPLv2, not as good as GPLv3 but still very good in my opinion.

seL4 can pass formal verification because it's so small (but still powerful) around 10,000 loc. Mach on x86 has 90,000 loc. Linux? More than 2.7 Million lines. It's OK if a kernel is small, but if it's too small, then we need to add more necessary features for general-purpose OS. But if we add more features, we can hardly make it pass formal verification. So there has to be compromised. We can just make sure seL4 pass the verification in a certain level. If we can control the granularity for necessary requirements, then seL4's verification is still meaningful. But what extra features we need? It's another suspended topic.

If we replace Mach with L4, then we have to support L4 in glibc. For example, implementing c standard library with L4 APIs. It's never a small work plus necessary testing! Fortunately, microkernel is different from Linux. Linux has many system calls, but in a microkernel, in theory, there could be only 2 APIs, message-send and message-receive, please don't forget you're passing messages rather than function calling to require resources from the kernel. You may ask, how does other microkernel OS support C/C++ languages? Well, they may not choose glibc. For example, zircon which is the microkernel of Google's brand new OS Fuchsia chooses musl. However, I'm a GNU hacker and I want to see a complete better GNU OS so that glibc is necessary for GNU tools/applications.

I've discussed the seL4 plan on Hurd-L4 mailing-list. So far, there's no any coding work for it. I think it's better to share more of my ideas on my blogs to get more advice, or potential contributors. Personally, I have many projects on the way, if I have a good scheduling and sufficient ideas and information, then I think it could happen.

BTW, if we really have L4 on Hurd someday, we may have to call an operating system "Debian GNU/Hurd/L4" and "Debian GNU/Hurd/Mach" to distinct. I'm kidding, if that day come, we'll have special codenames for them. ;-)

Why GNU Hurd is so hard to develop that it's still not ready in 2019?!

There're many explainations and rumors around this question, but the answer IMHO is no so complex: there're no sufficient contributors. But let me ask it deeper: why less people are intested in it? Well, I think there're many people have interest, but they lack of sufficient knowladge to help GNU Hurd technically. After all, the research and application of monolithic kernel is prominent in the industry. But the microkernel, usually, you may learn about it only if you're a serious CS student. That's not cool, because the success of Linux is based on massive contributors without serious CS background.

I believe there should be more blogs or YouTube channels to help people to learn about GNU Hurd. And I guess most people never know GNU Hurd can work as a Debian or Arch distro, say, Debian/Hurd or Arch/Hurd. It works fine as a command line server. Few people know GNU Hurd had released working versions for years. But I would like to suggest you try a qemu image which won't harm your current system.

Some people may ask, I'm familiar with Linux, how can I start Hurd? Does it mean I have to learn new command and tools from scratch?

However, most of Linux people neither use Linux nor familiar with Linux, because Linux is a kernel. You only use Linux when you're a kernel developer. What you're using is GNU tools and other applications which is compatible with POSIX. Please don't forget that you're actually using GNU operating system. That is to say, if you switch to Debian/Hurd, you may use it just like a Debian/Linux, if you don't run "uname -r", you may not even realize it's Debian/Hurd. Of course, if there's no any differences, then we don't need Hurd, right? The difference appears when you're trying to do system level programming, and more complex software system development, it's out of this article.

"But why Hurd? There's Linux, right?"

Well, yes, there was Minix, why Linus wrote Linux? If you want to ask, there could be some technical reasons for you. But the only true reason, the intrisic one, is always "because I like and it's no harm".

Cattelan’s Banana

In Dec 8th 2019, Italian artist Maurizio Cattelan had made a new sculpture in the Art Basel Miami Beach. It is a banana duct-taped to the wall, and it was priced $120,000. The orgnizer hope the visitors to think about how to confirm the value of a thing. Some people like this idea, some are not. Well, it's trivial in my article. I don't care how people think about it.

The title of this artwork is "Comedian". So who is the comedian?

GNU Hurd looks like the banana on the GNU wall. It can not move because it's taped as the offical GNU generic kernel. So far, we've spent more than million dollars on its development. Of course, Hurd contributors rarely get money from writing Hurd, but please think about the deserved income of the hardcore contributors for so many years. It's claimed to be valuable, or even priceless to somebody (like me), but it's never used in the senario that equals to its claimed value.

Huh, sounds like us Hurd contributors are the comedians, who is yearly blindly arduously pushing a rock to the top.

Sometimes when we look back to the history, old efforts had revealed the future to us, however, we never realized because it's too early to open it up. We may only realize the future when we're in the future. When we see something like Kubernetes or else, we may suddenly realize the value of the effort of GNU Hurd. If I can see those mocking face laughing at GNU Hurd decade ago, I guess I would see the real comedian. It's the fearless of ignorance facing the unknown future.

Yes, I know Kubernetes is never GNU Hurd, I heard you. They're different thing, I know.

GNU Hurd is not the banana too, fortunately.