5 ms·

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 user

by senko 4y ago

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.

ddevault 4y ago
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.
cmrdporcupine 4y ago
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.)
- jacquesm 4y ago
  Linux started out as a hobby project.
  - cmrdporcupine 4y ago
    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.
    - jacquesm 4y ago
      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.
      - cmrdporcupine 4y ago
        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.
ashafer 4y ago
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.
- kramerger 4y ago
  > It exists to brag about verification That is pretty much my own experience with sel4. Not very useful for real world
  - senko 4y ago
    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.
    - kramerger 4y ago
      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?
- dale_glass 4y ago
  That's interesting, could you provide more details? What are the un-fun bits? Too restricted? Too slow? Too hard to debug the application?

by senko 4y ago

ddevault 4y ago

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.

cmrdporcupine 4y ago

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

jacquesm 4y ago
Linux started out as a hobby project.
- cmrdporcupine 4y ago
  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.
  - jacquesm 4y ago
    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.
    - cmrdporcupine 4y ago
      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.

ashafer 4y ago

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.

kramerger 4y ago
> It exists to brag about verification That is pretty much my own experience with sel4. Not very useful for real world
- senko 4y ago
  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.
  - kramerger 4y ago
    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?
dale_glass 4y ago
That's interesting, could you provide more details? What are the un-fun bits? Too restricted? Too slow? Too hard to debug the application?