[seL4][1] is a formally verified microKernel which is used by billions of smartphones as part of their baseband OS. The part which is completely separate from Android or iOS. [1]:http://sel4.systems/

L4 is a joy to use.

I haven't worked with seL4, but used an earlier branch of the L4 family (L4Ka::Pistachio) as a base for a toy OS (university project).

If I had the time to tinker with base OS design today, I'd definitely start with seL4.

Edited to add: the whitepaper here is a good intro to seL4: https://sel4.systems/About/seL4-whitepaper.pdf

That white paper is an incredible piece of technical documentation. Accessible to anyone with a basic background in computing and operating systems. I love hidden gems like this.

A favorite part of mine is the explanation of capabilities versus ACLs that it provides.

Fine y'all have convinced me to take a look

SEPOS, the OS that runs in the Secure Enclave in Apple devices, is actually fork of L4Ka::Pistachio. It's called L4-embedded, and was developed by National ICT Australia for their Darbat project, a port of Darwin/XNU to L4. Running macOS on L4 sounds cool, but that project didn't go anywhere, for whatever reason.

I wonder if seL4 could serve as the base layer for a new Smalltalk based system on something like a PineNote.

> which is used by billions of smartphones as part of their baseband OS

oooooh.

It's almost a lame/inane question when framed this broadly, but: where can I read more about similarly incredibly obscure yet Really Important™ applications of technology that have just about completely disappeared into the woodwork?

"Embedded systems" is probably the space where this happens the most and it's a super super broad category. Everything with a microcontroller in it is running someone's code.

For example, a quick google search of "how many microcontrollers in a car?" gives 50 as a common answer. For every system that people think about as a computer (entertainment, engine controller, airbags) there are another 10 systems that are also tiny computers that we kind of expect to mostly work together just about perfectly, forever.

Feels pretty obscure and somewhat important, but maybe not incredibly obscure and really important. :/

Minix and Intel

That is intriguing - which baseband OSes are using seL4? Where can we read more about how they are using it? Thank you.

Qualcomm is cited in

https://sel4.systems/About/seL4-whitepaper.pdf

Hubris is a microkernel-ish OS for embedded systems, and has a bunch of documentation about its design:

https://hubris.oxide.computer/reference/

It's all open-source on Github:

https://github.com/oxidecomputer/hubris

(I work at Oxide, mostly using Hubris)

Big Oxide fan, will look into it!

Xous [1][2] is an example of a microkernel written in Rust and inspired by QNX, that we are actively developing.

[1] https://betrusted.io/xous-book/ch00-00-introduction.html

[2] https://github.com/betrusted-io/xous-core

MINIX 3 is the goto, I believe? At least it was when I was researching them.

https://git.minix3.org/index.cgi?p=minix.git

Happy to be wrong though, I'd like new code to look at.

Yay, since noone else has mentioned it, I get to add :) that the standard "why is minix interesting" nowadays is "it runs the Intel ME in a gazillion CPUs".

That says something about what one bunch of Very Careful Engineers think about the implementation's uptime and reliability provenance...

(The ME-cleaner project has identified that if Intel ME does not initialize, the CPU resets a few minutes after power on - so this suggests that a hard-unrecoverable error would leave the CPU unusable.)

Also, there aren't many OSs that have books to teach you about them, but MINIX does. Operating Systems: Design and Implementation by Andrew Tanenbaum. I suppose the value you get for free in MINIX 3, you pay for if you want the book...

> Operating Systems: Design and Implementation by Andrew Tanenbaum

I had a student edition of that book, back in the late 1980s. It had a full listing of the Minix source code as an appendix: fascinating to be able to sit in a comfortable chair and read a large body of code. I referred to it a lot when i was learning C. I'm guessing Minix has got bigger since then though.

Yeah I believe Minix is actually a complete rewrite intended to be more useful in the real world than just a teaching toy (and at that it has been successful). I can't imagine enjoying reading the source code apendix from a book as much as you seemed to have done :D But I did learn a lot from the main text of the book. Pretty hard for me to dive into even a simple hobbyist OS and figure things out from scratch.

The long flamewar between Linus and Tannenbaum was interesting to read, at least briefly.

https://en.m.wikipedia.org/wiki/Tanenbaum%E2%80%93Torvalds_d...

I was very impressed by this https://youtu.be/jMkR9VF2GNY which also states minix 3 (from the author) is now a microkernel and hosts a modified netbsd like (service based) system.

Thank you very much! Really excited to dig into this.

Google Fuschia is a microkernel OS according to wikipedia https://en.wikipedia.org/wiki/Fuchsia_(operating_system)

https://cs.opensource.google/fuchsia

This is based on little kernel from recollection (noted somewhere in the docs)

https://github.com/littlekernel/lk

Nobody, and I mean literally NOBODY, can spell "Fuchsia".

Idea: "fuchs" is German for "fox".

This guy fuchs.

The OS Fuchsia is named after the colour Fuchsia named after the flower Fuchsia named after a Renaissance-era Bavarian botanist Leonhart Fuchs.

So, you're supposed to spell this guy's name with a capital F.

I was wondering how it went from "Fuks" to "Few-Sha" - and apparently that was via Latin:

> Leonhart Fuchs (German: [ˈleːɔnhaʁt ˈfʊks] ... sometimes spelled Leonhard Fuchs and cited in Latin as Leonhartus Fuchsius

TIL... that flower fews like Fuschius?

The Nintendo Switch runs a microkernel called "Horizon". It has been fully reverse-engineered, and a 1:1 open-source reimplementation exists: https://github.com/Atmosphere-NX/Atmosphere/tree/master/libr...

QNX's docs[1] are some of the easier ones to read. The neutrino kernel briefly had it's source code available.

[1] https://www.qnx.com/developers/docs/6.3.0SP3/neutrino/

I've always wanted to pin down a vaguely-normative idea of whether the "actually you can't have this anymore" applies retroactively, or whether it would be legally defensible to go run off with the kernel releases that were made openly available a while back.

I think it was even MIT or BSD or similar?

BSPs were a mix usually Apache or some more permissive license for common dev boards. They had something more limiting for the kernel. I'm kinda surprised I haven't seen a bootleg version of it floating around somewhere online.

They also had pretty liberal hobbyist/non-commercial license which let you learn the toolchain and develop with some of the middleware. That all went away when RIM (blackberry now) bought them.

Re: manuals - QNX Cookbook was also pretty good read. The documentation from that era were published as real books.

Plan 9 is a great example of a hybrid kernel that is very much in the spirit of a microkernel. It uses 9p as the foundation meaning the whole OS is based around a file-like message oriented RPC protocol. Every process has its own namespace and mount table so you implement security by limiting mounted resources to a child proc and its children. Since the 9p byte streams are processor agnostic you don't have endian or cross platform problems so you don't care about a remote machines architecture.

The source code is included by default so you can boot and jump right in. Code is very clean, minimal and approachable.

The reason why it is not a microkernel is because hardware drivers and some performance sensitive code such as ip, tls and graphics are in kernel. The rest, including on-disk file system (cwfs, fat, ext, etc), certain usb drivers, etc run in user space.

> I'm curious to see how userspace processes communicate to kernel processes to execute privileged actions.

You write and read messages to synthetic files served by the kernel. Kernel files are served via a special # prefix so they can be opened by any program locally. Since user space programs can speak 9p you don't need any special programs to make syscalls to talk to the kernel. e.g. to list disks served by the sd(3) driver run 'ls '#'S'

Everything is just messages. Even unix signals were replaced with notes. To send a note to a process all you do is 'echo hello >/proc/$pid/ctl' and in the program you register one or more note handlers that simply do a strcmp() and if the note matches a string you define then do something. (if you complain about /proc and never used plan 9 /proc then your argument is invalid.)

If you think about it, plan 9 is just a host for microservices.

I recommend using 9front to explore.

The whole L4 family and MACH or Hurd ;) and maybe have a look at Genode where you can have ~7 kernels atm:

nova

okl4_x86

foc

fiasco

pistachio

linux

sel4

https://genode.org/documentation/components

Also QNX and RTEMS need's to be mentioned here.

And Helios/Ares-os:

https://sr.ht/~sircmpwn/helios/

I dare to say that MVS and its successors (OS/390, z/OS) are also, in some ways, microkernels. Sadly, I am not an OS expert to make a proper comparison.

But I think one of the main mechanisms is basically non-kernel services install their own system calls (SVCs) and this SVC will schedule a light-weight thread (SRB) in the requestor's address space.

There was an older book that described how to create a simple OS along similar lines to MVS, but I don't remember the name.

I was about to say macOS uses a microkernel, but on checking it seems that it's hybrid. Also, the source isn't available, so might not be what you're looking for.

XNU is opensource....

https://opensource.apple.com/releases/

Click on the release (Monterey 12.5) and scroll down. xnu-8020.140.41 is there..

Links to: https://github.com/apple-oss-distributions/xnu/tree/xnu-8020...

oh! I was not aware of this. Thank you.

>Also, the source isn't available, so might not be what you're looking for.

It is available, and it's called darwin-xnu:

https://github.com/apple/darwin-xnu

a mix of Mach and a FreeBSD kernel:

https://i0.wp.com/www.linuxandubuntu.com/wp-content/uploads/...

And a really good yt presentation:

24C3: Inside the Mac OS X Kernel

https://www.youtube.com/watch?v=-7GMHB3Plc8

> 24C3: Inside the Mac OS X Kernel

> https://www.youtube.com/watch?v=-7GMHB3Plc8

https://fahrplan.events.ccc.de/congress/2007/Fahrplan/events...

It's based on a microkernel (mach) but is hybrid, and the source is available https://github.com/apple-oss-distributions/xnu/tree/xnu-8020...

For the time being, after all kexts are forbidden, replaced by the respective userspace drivers, the real difference will only be arguing about semantics, as for all practical purposes from 3rd parties, it will be like a proper micro-kernel OS.

https://support.apple.com/guide/security/kernel-extensions-s...

They'd need to replace Mach with something less inefficient first.

Mach is a pre-Liedtke microkernel. It's slow at IPC. Which is bad when IPC is what it has to do the most in a proper multi-server system.

Regardless of what we think, Apple has been quite clear at WWDC what the end goal is, no more kexts allowed when there is a corresponding userspace framework for the respective driver class.

This the the best thing in commercial software, decisions happen, and there are no forks botching the final outcome by disgruntled devs.

so ELI5 here, but aren't modern computers fast enough to overcome many of its original shortcomings?

I'm not a software engineer, but out of curiosity.

Not only they are, many hardcode anti-microkernels folks kind of forget their beloved monolithic Linux kernel nowadays runs on top of type 1 hypervisors (which is basically a tiny micro-kernel), and then there is this whole thing with Docker and Kubernetes deployments for every executable.

Ah. So there's no dire need for Apple to improve Mach's performance.

I wonder if the computer industry in general tend to overlook at performance, that's how I feel about the hardware community, where a tiny differences in benchmarks always taking the crown.

There is also GNU Mach from the venerable HURD.

The nintendo 3DS (and i think the switch too) runs on a microkernel with userspace pretty much everything. The docs on it are all reverse-engineered, though.

http://www.microkernel.info/ probably should list some others mentioned here.

I've only glanced at it, but there's some teaching material from L4 land apparently in the usual excellent German technical English at https://tu-dresden.de/ing/informatik/sya/professur-fuer-betr...

Composite OS is an interesting research micro kernel. It has great resources to help you to dig into it and its underlying principles!

About page: https://composite.seas.gwu.edu/

GitHub: https://github.com/gwsystems/composite

It seemed to be in a similar space to Genode when I had a brief look. Is it clear how it compares?

A system that claims to allow you to configure it in microkernel and other modes might be interesting for comparison of the approaches, but I've only noticed it via a local connexion: https://project-flexos.github.io/

MkLinux for early PowerMacs ran Linux on top of Mach. https://en.wikipedia.org/wiki/MkLinux

OSF/1, the attempt at an industry standard next-gen Unix by what is now the Open Group, holders of the UNIX trademark, also ran on Mach. Only DEC shipped it, though. The filesystem is now FOSS but I don't think the rest of DEC's code was, sadly. https://en.wikipedia.org/wiki/OSF/1

Chorus is out there: https://en.wikipedia.org/wiki/ChorusOS

HelenOS, from the Charles University here in Prague where I write, is a FOSS microkernel OS. http://www.helenos.org/

rcore-os [0] uses a rust-lang port of zircon [1], the kernel that fuschia-os uses. zircon isn't quite a microkernel, but is pretty close to one [2].

FreeRTOS [3] bundles in a microkernel [4].

Speaking of FreeRTOS, you may also be interested in Riot OS developer's blog entry on building a (micro?) kernel [5].

[0] https://github.com/rcore-os/rCore

[1] https://github.com/rcore-os/zCore

[2] https://archive.is/Y49Ih

[3] https://github.com/FreeRTOS/FreeRTOS-Kernel

[4] https://archive.is/u8Hsw

[5] https://archive.is/0MHF1

IMHO it's very misleading to call those RTOS kernels microkernels. There is no address space isolation, it's more like a unikernel - there is no privilege separation.

Mach (used by GNU Hurd) deserves a mention.

And the original basis for the NeXTStep -> OpenStep -> OS X -> iOS / MacOS line. Source for XNU, the current incarnation of Apple's microkernel is available as part of the Darwin stuff: https://github.com/apple/darwin-xnu

It's a good example of how not to do microkernels.

i.e. everything that was wrong with them, before Liedtke proposed L3 and L4.

only a mention

And a long fart

Here are some interesting historical examples:

https://en.wikipedia.org/wiki/Taligent

https://en.wikipedia.org/wiki/Copland_(operating_system)

https://en.wikipedia.org/wiki/Workplace_OS

None of these were FOSS, though...

Gernot Heiser's blog[0] deserves a mention.

I read it chronologically. It was worth every minute.

0. https://microkerneldude.org/

A unikernel is sort of the opposite of a microkernel. Instead of the minimum running in kernel space, the whole thing including the traditionally user code runs in kernel space.

There're a couple of microkernels you can check out: http://www.microkernel.info

Amiga OS. It was and probably still is the only microkernel OS commercially available to the general public.

> It was and probably still is the only microkernel OS commercially available to the general public.

QNX was

QNX gained a GUI and multimedia support mainly because at one point it was going to be the basis of the next-generation AmigaOS, of course.

https://www.theregister.com/1998/11/14/amiga_2_to_use_qnx/

But it didn't work out:

https://www.trollaxor.com/2005/06/how-qnx-failed-amiga.html

My understanding was that QNX wasn't a general purpose OS even though it could run on 90's x86 cards and that it was mainly marketed to engineers, governments, and universities.

Pretty sure it's as general purpose as anything else: https://guidebookgallery.org/screenshots/qnx621

It might be that it was mostly used in embedded stuff, but that's true of Linux too, not an inherent limit.

minix also needs a mention here. Part of Intel Management Engine and close ties to linux childhood.

You need to be specific -- it's Minix 3 that's a µkernel, not the earlier ones.

And someone else already did mention it.

Lol

Minix Forever