News for hackers. Stuff that matters.

A comment on The Helios microkernel. Parent comment

Re:The Helios microkernel by ddevault on Thursday June 16, 2022 @04:19AM (#31763646)
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.

[ Parent | on HN ]
Re:The Helios microkernel by jdub on Thursday June 16, 2022 @06:01AM (#31764231)
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.

[ Parent | on HN ]
Re:The Helios microkernel by carapace on Thursday June 16, 2022 @10:32AM (#31766511)
> it's not a solely academic exercise, it is being used in industry

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

[ Parent | on HN ]
Re:The Helios microkernel by jnash on Thursday June 16, 2022 @11:50PM (#31773923)
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.
[ Parent | on HN ]
Re:The Helios microkernel by riedel on Thursday June 16, 2022 @04:57AM (#31763853)
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.)
[ Parent | on HN ]
Re:The Helios microkernel by ddevault on Thursday June 16, 2022 @05:42AM (#31764123)
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.

[ Parent | on HN ]
Re:The Helios microkernel by LargoLasskhyfv on Thursday June 16, 2022 @12:23PM (#31767889)
There is https://genode.org/ which builds on top of it, as one of a few similar options. Look for Sculpt-OS there.
[ Parent | on HN ]