Hacker News Reader

Comment by alphazard | Hacker News Reader

> As about SEL4 - it is so elegant because it leaves all the difficult problems to the upper layer (coincidentally making them much more difficult).

I completely buy this as an explanation for why SEL4 for user environments hasn't (and probably will never) take off. But there's just not that much to do to connect a server application to the network, where it can access all of its resources. I think a better explanation for the lack of server side adoption is poor marketing, lack of good documentation, and no company selling support for it as a best practice.

View on HN

The lack of adoption is because it’s not a complete operating system.

Using sel4 on a server requires complex software development to produce an operating environment in which you can actually do anything.

I’m not speaking ill of sel4; I’m a huge fan, and things like it’s take-grant capability model are extremely interesting and valuable contributions.

It’s just not a usable standalone operating system. It’s a tool kit for purpose-built appliances, or something that you could, with an enormous amount of effort, build a complete operating system on top of.

Yes. I really hope someone builds a nice, usable OS with SeL4 as a base. If SeL4 is like the linux kernel, we need a userland (GNU). And a distribution that's simple to install and make use of.

I'd love to work on this. It'd be a fun problem!

seL4 needs a ‘the rest of the kernel’ to be like linux

It needs device drivers for modern x86 hardware. And filesystems, and a TCP stack. All of that code can be done in "SeL4 userland", but yeah - I see your point.

Are there any projects like that going on? It feels like an obvious thing.

A lot of deployments essentially virtualize Linux or run portions of NetBSD (e.g. via their "rump" kernel mechanism) to achieve driver support, file systems, etc. That's not really a general-purpose solution, though.

There is work within major consumer product companies building such things (either with sel4, or things based on sel4's ideas), and there's Genode on seL4.

Are you aware of https://genode.org ?

> But there's just not that much to do to connect a server application to the network, where it can access all of its resources.

If you only care to run stateless stuff that never write anything (or at least never read what they wrote) - it's comparatively easy. Still gotta deal with the thousand drivers - even on the server there are a lot of quirky stuff. But then you gotta run the database somewhere. And once you run a database you get all the problems Linus warned about. So you gotta run the database on a separate Linux box (at that point - what do you win vs. using Linux for everything?) or develop a new database tailored for SeL4 (and that's quite a bit more complex than an OS kernel). An elegant solution that only solves a narrow set of cases stands no chance over a crude solution that solves every case.

Also, with the current sexy containerized stacks it's easy to forget, but having same kind of environment on the programmer's workbench and on the sever was once Unix's main selling point. It's kinda expensive to support a separate abstraction stack for a single purpose.

Reply on news.ycombinator.com