5 ms·

I think this is good for everyone. This team and associated groups around the world (a famous researcher once called it "the German army") have been receiving

by zibzab 5y ago

I think this is good for everyone. This team and associated groups around the world (a famous researcher once called it "the German army") have been receiving a lot of grants, been too dominant in conferences and to be honest have not done much practical work for some time. (If you think sel4 is extremely useful in practical applications, go ahead and try it yourself. Port an existing project to use sel4 and see how well it works)

johndoe0815 5y ago
L4 shows that not only US-based researchers can do great systems research - and this is a very good think IMHO. Billions of iOS devices use L4 (though net seL4 AFAIK) as the OS for their security processor and there are numerous other embedded use cases. The 30 years of efforts by Jochen Liedtke at GMD/Karlsruhe, Hermann Härtig at TU Dresden and Gernot Heiser at UNSW (and the countless students and postdocs) have significantly advanced the field of microkernel research and OS research in general. Microkernels were a dead field of research after Mach etc. didn't live up to their expectations, only to be revived by Liedtke's work. It is extremely confusing that you think a successful team publishing great papers and receiving significant research founding is "too dominant" (and the anti-German tone of the "army" comment is certainly inappropriate).
- zibzab 5y ago
  Let me explain my comment: For a while it was really hard to do something in the OS, security or embedded system field of it didn't align with the L4 way of doing things. This harmed progress, and in particular young researchers with new controversial ideas.
  - saithound 5y ago
    Can you be specific? Who are these young researchers with new controversial ideas who are harmed by L4?
  - johndoe0815 5y ago
    I know the German OS research landscape pretty well and I can assure you that there were a large number of successful systems projects and good PhD theses which were not in any way related to L4. Of course, the groups for which L4 was fundamental (such as Hermann Härtig's TU Dresden group) had a natural focus on L4. But there is a lot of internationally renowned research in OS going on in Germany, I will only mention two examples, Wolfgang Schröder-Preikschat's group at FAU Erlangen and Frank Bellosa's group at KIT. But I would certainly love to discuss your view of the research landscape further - for me, it is always interesting to get to know different views and insights. So if you are interested to talk about this, feel free to contact me directly.
    - zibzab 5y ago
      It's hard to know how common this is. But I have personally witnessed the L4 top folks talking down someones novel contributions as "this is nothing knew, you should have used L4, we did this stuff 10 years ago" and making a young researcher feel miserable. (IIRC the very same people also published a paper introducing the same novel idea in L4 some months later, but that's another discussion)
- brandmeyer 5y ago
  Cell phone baseband and virtualization supervisor hosts are the only niches where L4 gained any traction. Considering the lack of publicly available information about baseband operating environments, those could actually be the same niche (ie, L4 is acting as a hypervisor for the baseband). Hurd-on-L4 was a flop. Fuscha went a completely different direction with dissimilar communication primitives. From the outside, L4 looks like a perfect example of a line of academic research that has no industrial relevance.
  - johndoe0815 5y ago
    I think some people from industry would disagree. Certainly L4 has found use cases mostly in the field of embedded systems, but I wouldn't call this a niche (or at least it's a pretty big one). Companies like Hensoldt Cyber (https://hensoldt-cyber.com https://hensoldt-cyber.com - Gernot Heiser is involved in this) but also SYSGO with PikeOS (an independently developed L4-family microkernel - https://www.sysgo.com https://www.sysgo.com), Kernkonzept (https://www.kernkonzept.com https://www.kernkonzept.com) or Genode Labs (https://genode.org https://genode.org) have successfully used and deployed L4-based systems with many customers from industry. Yes, this is again very much focused on Germany, but that's also where a lot of the research was done. Fuchsia at Google is probably a result of the "not-invented-here" syndrome that seems to be popular at Google. I haven't taken a closer look at the system but would certainly be interested in reading about the differences to an L4-based microkernel. And Hurd-on-L4 is certainly coming next year ;-) (or a bit later, due to Corona or so...).
    - saithound 5y ago
      Other active seL4 users include Real-Time Innovations (autonomous systems), Cog Systems (connected devices), Raytheon (defense/aerospace), DornerWorks (IoT/medical), Ghost (self-driving cars), Penten (communications securty).
    - tilt_error 5y ago
      Oh yes: https://xkcd.com/1508/ https://xkcd.com/1508/
    - 5y ago
GregarianChild 5y ago
I think seL4 is orthogonal to the team's core achievements which are in verification of low-level code. Those technologies transfer to other settings.

by zibzab 5y ago

johndoe0815 5y ago

L4 shows that not only US-based researchers can do great systems research - and this is a very good think IMHO. Billions of iOS devices use L4 (though net seL4 AFAIK) as the OS for their security processor and there are numerous other embedded use cases. The 30 years of efforts by Jochen Liedtke at GMD/Karlsruhe, Hermann Härtig at TU Dresden and Gernot Heiser at UNSW (and the countless students and postdocs) have significantly advanced the field of microkernel research and OS research in general. Microkernels were a dead field of research after Mach etc. didn't live up to their expectations, only to be revived by Liedtke's work. It is extremely confusing that you think a successful team publishing great papers and receiving significant research founding is "too dominant" (and the anti-German tone of the "army" comment is certainly inappropriate).

zibzab 5y ago
Let me explain my comment: For a while it was really hard to do something in the OS, security or embedded system field of it didn't align with the L4 way of doing things. This harmed progress, and in particular young researchers with new controversial ideas.
- saithound 5y ago
  Can you be specific? Who are these young researchers with new controversial ideas who are harmed by L4?
- johndoe0815 5y ago
  I know the German OS research landscape pretty well and I can assure you that there were a large number of successful systems projects and good PhD theses which were not in any way related to L4. Of course, the groups for which L4 was fundamental (such as Hermann Härtig's TU Dresden group) had a natural focus on L4. But there is a lot of internationally renowned research in OS going on in Germany, I will only mention two examples, Wolfgang Schröder-Preikschat's group at FAU Erlangen and Frank Bellosa's group at KIT. But I would certainly love to discuss your view of the research landscape further - for me, it is always interesting to get to know different views and insights. So if you are interested to talk about this, feel free to contact me directly.
  - zibzab 5y ago
    It's hard to know how common this is. But I have personally witnessed the L4 top folks talking down someones novel contributions as "this is nothing knew, you should have used L4, we did this stuff 10 years ago" and making a young researcher feel miserable. (IIRC the very same people also published a paper introducing the same novel idea in L4 some months later, but that's another discussion)
brandmeyer 5y ago
Cell phone baseband and virtualization supervisor hosts are the only niches where L4 gained any traction. Considering the lack of publicly available information about baseband operating environments, those could actually be the same niche (ie, L4 is acting as a hypervisor for the baseband). Hurd-on-L4 was a flop. Fuscha went a completely different direction with dissimilar communication primitives. From the outside, L4 looks like a perfect example of a line of academic research that has no industrial relevance.
- johndoe0815 5y ago
  I think some people from industry would disagree. Certainly L4 has found use cases mostly in the field of embedded systems, but I wouldn't call this a niche (or at least it's a pretty big one). Companies like Hensoldt Cyber (https://hensoldt-cyber.com https://hensoldt-cyber.com - Gernot Heiser is involved in this) but also SYSGO with PikeOS (an independently developed L4-family microkernel - https://www.sysgo.com https://www.sysgo.com), Kernkonzept (https://www.kernkonzept.com https://www.kernkonzept.com) or Genode Labs (https://genode.org https://genode.org) have successfully used and deployed L4-based systems with many customers from industry. Yes, this is again very much focused on Germany, but that's also where a lot of the research was done. Fuchsia at Google is probably a result of the "not-invented-here" syndrome that seems to be popular at Google. I haven't taken a closer look at the system but would certainly be interested in reading about the differences to an L4-based microkernel. And Hurd-on-L4 is certainly coming next year ;-) (or a bit later, due to Corona or so...).
  - saithound 5y ago
    Other active seL4 users include Real-Time Innovations (autonomous systems), Cog Systems (connected devices), Raytheon (defense/aerospace), DornerWorks (IoT/medical), Ghost (self-driving cars), Penten (communications securty).
  - tilt_error 5y ago
    Oh yes: https://xkcd.com/1508/ https://xkcd.com/1508/
  - 5y ago

GregarianChild 5y ago

I think seL4 is orthogonal to the team's core achievements which are in verification of low-level code. Those technologies transfer to other settings.