People mostly use seL4 as a hypervisor, running Linux on top of it. QNX has a POSIX API, so you don't need another layer.

▲

naasking 4 hours ago | parent [-]

QNX is allegedly a microkernel. Either the QNX POSIX API is itself another layer over the microkernel, or QNX cannot be a microkernel (hint: it's the former [1]).

People run L4 as a hypervisor only because they want access to the full Linux API. That's not really what you're talking about though, and there's nothing stopping a thin QNX-style POSIX compatibility layer as a user-space server or library as with QNX. The point being, the mature, widely deployed, robust and widely tested microkernel you're looking for already exists, so you just need to focus on the POSIX layer.

[1] https://www.qnx.com/developers/docs/8.0/com.qnx.doc.neutrino...

▲

Animats 4 hours ago | parent [-]

Actually, most of the POSIX compatibility stuff is in QNX's equivalent of "libc". When you call Unix "write", the library does a MsgSend to the appropriate service. MsgSend is in the kernel, but whatever performs the write is in some other process.

Some other functions, such as program loading, are in user space .so files. When you spawn a new process (in QNX, spawn is the usual function, and fork/exec are emulated for backwards compatibility), the library in your program attaches to the .so file that contains the program loader. The user process requests memory and decodes the executable image, and sets up the new process environment. If something in executable file decode does something wrong, the process faults in the usual user space way.

There's no privileged emulation layer.

At boot, the .so files for this sort of thing are part of the boot image and are loaded into memory, so they are available even before there's a file system. As are the userspace programs needed during startup. You can build your own boot image, with whatever programs you want. You might, for example, include the "dashboard driver" for a car, and omit terminal support. There's no assumption in QNX that there's a console, because, often, there isn't.

	▲	jacquesm 3 hours ago \| parent [-]
		That's exactly how I did it too. The biggest hack for me was the 'open' call when using a device. That first does a lookup for a service with the name following the /dev/ bit and then it redirects the 'open' message to that process rather than to the active drive's filesystem. This allows for the appearance of a /dev/ directory without it actually existing anywhere. This makes some Unix like mechanisms hard to implement (for instance, you can't just do 'ls /dev/') but it made enough stuff work out of the box that it seemed worth the trade-off of bypassing the filesystem. It also makes the file system optional, which can come in very handy, because that means no file system is every privileged in the sense of a Unix '/' filesystem. They're all equal and you can kill each and every one of them and still have a running system.