5 ms·

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 ambi

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.

riedel 4y ago
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.)
- ddevault 4y ago
  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.
jdub 4y ago
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.
- carapace 4y ago
  > it's not a solely academic exercise, it is being used in industry Yeah, e.g. General Dynamics bought OK Labs. *waggles eyebrows*
LargoLasskhyfv 4y ago
There is https://genode.org/ https://genode.org/ which builds on top of it, as one of a few similar options. Look for Sculpt-OS there.
jnash 4y ago
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.

riedel 4y ago

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.)

ddevault 4y ago
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.

jdub 4y ago

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.

carapace 4y ago
> it's not a solely academic exercise, it is being used in industry Yeah, e.g. General Dynamics bought OK Labs. *waggles eyebrows*

LargoLasskhyfv 4y ago

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

jnash 4y ago

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.