Hacker News Reader

Comment by senko | Hacker News Reader

The post mentiones seL4 as an inspiration:

> Again, much of the design comes from seL4, but unlike seL4, we intend to build upon this kernel and develop a userspace as well.

I'm wondering why they didn't decide to build the rest of the system on top of that.

I'd totally respect answers like "because building kernels is fun" or "because I wanted to do that in my programming language". I'm just wondering if there was another reason seL4 was unsuitable.

View on HN

seL4 has an interesting API design but I'm not fond of the internals or implementation. It's largely an academic exercise, in my opinion. They also have no ambitions in userspace, and limit themselves to working on the kernel alone, which is not a great idea - other people have criticized seL4 on the basis that not building a system with your kernel is a good way to be blind to the design flaws of your kernel.

In short, seL4 is cool, but not very practical, and I think it can be done better.

AFAIK l4se focussed on verifiability and simultaneous performance (with actual customers in defense I guess). L4RE seems more focussed on application (one being the simk3 'merkle phone') . So I wonder which part of inspiration comes from seL4 and which part from L4 in general . Especially can you elaborate the shortcomings of the general design in terms of user land (I only had to build a toy OS on l4 in a practical course more than 15 years ago at liedke's OS group just after he passed away so suddenly. We obviously never got to the nasty parts.)

The actual API differences between Helios and seL4 are somewhat subtle, rather than a broader difference of design philosophy. For instance, the layout of the bootinfo structure is different - PML4/PDPT/PD/PT objects are stored in separate capability regions so that userspace can more reliably distinguish them without architecture-aware heuristics. Little things like that. And of course, the implementation is wildly different from seL4.

To be clear, I am specific about the "seL4" inspiration rather than the "L4". Naturally L4 plays a role, but Helios's API design has a pretty obvious influence from seL4 specifically.

A few thoughts:

- the seL4 team definitely works on user space stuff (see the rest of the repos in the seL4 organisation on GitHub), but it's very basic thus far. there is some design work going on to standardise some user space bits and pieces. but i don't think they're ever going to build an top-to-bottom opinionated operating system stack – that's for other people to do.

- it's not a solely academic exercise, it is being used in industry, but most of what everyone sees is the output of the research group, which gives it an academic sheen.

- the unfamiliar internals and implementation are driven by a fundamental difference between seL4 and almost all other kernels... it is verified.

> it's not a solely academic exercise, it is being used in industry

Yeah, e.g. General Dynamics bought OK Labs. *waggles eyebrows*

There is https://genode.org/ which builds on top of it, as one of a few similar options. Look for Sculpt-OS there.

The "academic exercise" you are talking about has been used and is being used in space, defense, and consumer mobile devices. Very few micro kernels have had that amount of practical real-world usage.

As someone who worked with seL4, it's because the development experience is literally the worst you can possible have. It's zero fun and anyone who has to deal with it inevitably ends up hating seL4. It exists to brag about verification, developing real applications on it is a fool's errand.

> It exists to brag about verification

That is pretty much my own experience with sel4. Not very useful for real world

That's interesting, do you think the poor DX is due to not enough effort being made to make it more useful for outside devs, or because making it possible to do verification makes other things ugly and inconvenient?

I was considering seL4 for a hobby project (having worked with L4Ka:Pistachio a long time ago), but didn't dig deep enough to spot these problems.

The latter, in the sense that it has been scaled down significantly to make verification possible.

As soon as you start adding stuff or running it in a different hardware the verification will no longer apply, so why bother?

That's interesting, could you provide more details? What are the un-fun bits? Too restricted? Too slow? Too hard to debug the application?

I had the same concerns when Fuchsia was first announced. It seems ... almost reckless... to build a new microkernel from scratch in this day and age when sel4 (or just L4 generally) exists and is so heavily tested and developed.

All of these people are frankly better engineers than me, of course, so my opinion doesn't matter here, really. But I do have a worry about people in our industry seeking novelty instead of building on the proven.

(Except of course for research or hobby projects. Go for it.)

Linux started out as a hobby project.

Sure, and I used it back then. There were kind of no other realistic options with momentum behind them. But also we just accepted that it was a bit cowboy and that was part of the fun. I guess it could have been FreeBSD or even Minix that got the momentum maybe, but Linux caught on with enthusiasts, it made the right compromises and then big names like IBM put weight behind it.

I think that the 'big names' that threw their weight behind it mostly did so because they realized that (1) they'd never manage to get a community like that going and (2) because it did not seem to compete with their core business.

SUN, DEC, SGI and many others besides that aimed to dominate the server market were left by the wayside, and even Microsoft was running (very) scared. If not for their illegal behavior they too would have lost the server market.

Yeah it was a crazy time to watch the whole bottom of the workstation market fall out. Solaris managed to hold on in datacentres for a while, but the others not as much. And a 486 or Pentium running Linux was just as good as most proprietary Unix at the time, or was well on its way to getting there.

I did a summer contract job at an IBM subsidiary in summer 98 or so, and I had a manager there fight me on installing Linux on some spare PCs, because he thought they should be running, y'know, SCO. A Real Unix. It already looked preposterous by then.

One of those SUN pizza boxes held out so long that the bearings on the drives were completely worn out, everything was moved onto a different machine and when it was powered down you could hear the harddrives have a most horrible crash. The drives would not even spin when powered up again.

The thing is seL4 had (has?) many limitations which made it not very interesting for the real world: at some point it wasn't able to use multiple cores, or use low power states.. I think that only people who have closely looked at seL4 can tell whether it's really usable for their use case.

Reply on news.ycombinator.com