3 ms·

L4 was popular at my university (Karlsruhe). While I never really looked into it in any detail, it always appeared to me like a project that is primarily intere

by hannob 2y ago

L4 was popular at my university (Karlsruhe). While I never really looked into it in any detail, it always appeared to me like a project that is primarily interested in testing some theoretical ideas, but not in building anything that would be practically useful. That was 20 years ago. As far as I can tell, this has not changed. (Quick googling tells me there appear to be some efforts to build an OS on it, but they all look more like proof of concepts, not like something with real-world use.)

yjftsjthsd-h 2y ago
https://en.wikipedia.org/wiki/L4_microkernel_family https://en.wikipedia.org/wiki/L4_microkernel_family seems to describe it having been used all over the place, though mostly in embedded contexts. > OKL4 shipments exceeded 1.5 billion in early 2012,[4] mostly on Qualcomm wireless modem chips. Other deployments include automotive infotainment systems.[13] > Apple A series processors beginning with the A7 contain a Secure Enclave coprocessor running an L4 operating system[14] called sepOS (Secure Enclave Processor OS) based on the L4-embedded kernel developed at NICTA in 2006.[15] As a result, L4 ships on all modern Apple devices including Macs with Apple silicon.
- ryao 2y ago
  I feel like the two of you are talking past each other as the other poster is talking about time sharing systems like UNIX while you are pointing at embedded applications that are OS optional and if there is any semblance of an OS, it is really minimal. People deploying L4 there is not very surprising and does not apply to his remarks. Seeing this is like watching one person discuss an absence of apples and seeing another reply saying that there are oranges.
- hannob 2y ago
  Ok, admittedly, that's more than I expected. And hey, if they found some use cases in the embedded world, fine. Nevertheless, it's not exactly how it was pitched. This Microkernel thing always had a "Linux is doing it wrong, we're doing it better" story behind it. They wanted to be a replacement for a general-purpose OS. That cetainly hasn't happened.
  - ryao 2y ago
    OSF/1 is the closest that microkernels ever came to being used in general purpose operating systems: https://en.wikipedia.org/wiki/OSF/1 https://en.wikipedia.org/wiki/OSF/1 The only still living variant is AIX. Some of the code is in the XNU kernel, although that is a monolithic kernel rather than a microkernel. Apple converted it to a monolithic design for performance reasons. That said, this article suggests that AIX is not using a microkernel either: https://tedium.co/2019/02/28/ibm-workplace-os-taligent-history/ https://tedium.co/2019/02/28/ibm-workplace-os-taligent-histo...
    - Zamiel_Snawley 2y ago
      Genode is an actively developed, general purpose desktop operating system that works today, and can use seL4, among other kernels.
    - skissane 2y ago
      > The only still living variant is AIX. This is incorrect. The thing you have to understand about “AIX” is that historically it was not a single codebase, it was just a common brand for multiple unrelated IBM Unix offerings. (DB2 is the same story.) One of those offerings was AIX/ESA for IBM mainframes - and that was indeed based on the OSF/1 microkernel. But AIX/ESA died in the early 1990s-it was replaced by turning MVS aka OS/390 into a certified Unix, a role carried on by z/OS today, and later on by z/Linux as well. Whereas, the only AIX that survives to this day is the RS/6000 branch which isn’t based on OSF/1, and has a classic monolithic kernel design. Its distant ancestor, AIX version 1 for the RT PC, did use a microkernel (VRM), but that microkernel was very different from Mach and OSF/1 (it was written in a PL/I dialect, PL.8, that’s how alien it was)
      - ryao 2y ago
        Thanks for the clarification.
      - pjmlp 2y ago
        Additionally it is the only UNIX that follows a Windows like approach to shared libraries, which might confuse folks coming from POSIX land.
dloss 2y ago
Well, an L4 variant is used in iPhones: "The Secure Enclave Processor runs an Apple-customized version of the L4 microkernel." https://support.apple.com/de-at/guide/security/sec59b0b31ff/web https://support.apple.com/de-at/guide/security/sec59b0b31ff/...
nabla9 2y ago
L4, L4Ka developed in Karlsruhe is not the same as seL4.
xxmarkuski 2y ago
Jochen Liedtke became a professor in 1999 in Karlsruhe, sadly he passed away only shortly after in 2001. I don't know if his successor Bellosa still does research on L4. There was the L4Ka project which appears to be completed. In the bachelor lecture on OS by him it's not part of the curriculum. Rittinghaus, alumni of Bellosa, is involved with Unikraft [0], which was featured a couple of times on hn, and is using unikernel technology. [0] https://unikraft.org/ https://unikraft.org/
- __bjoernd 2y ago
  After Liedtke's passing, L4 research was continued in groups at UNSW (Gernot Heiser, formal verification -> SeL4) and TU Dresden (Hermann Haertig, Fiasco/L4Re, focusing on real-time and secure systems). Genode (already mentioned in another comment) [1] came out of the TU Dresden group with some nice ideas around managing compartmentalized systems. Kernkonzept [2] is a startup commercializing the L4Re microkernel. [1] https://genode.org/ https://genode.org/ [2] https://www.kernkonzept.com/ https://www.kernkonzept.com/
senko 2y ago
I love the work (and the direction) the Karlsruhe team did on L4Ka, especially with Pistachio - the design was clean, simple, easy to grasp. I did a Pistachio-based OS for my diploma thesis (not at Karlsruhe). I always thought that if I'd been studying there, I'd probably go into OS research.
froh 2y ago
the L4Re derivative (open source) is running in every single id.X Volkswagen car in the central "icas1" ECU, carrying Linux and other guests. https://www.kernkonzept.com/kk_events/elektrobit-advances-automotive-safety-with-l4re/ https://www.kernkonzept.com/kk_events/elektrobit-advances-au... afaics the L4Re kernel also is part of Elektrobit Safe Linux.

by hannob 2y ago

yjftsjthsd-h 2y ago

https://en.wikipedia.org/wiki/L4_microkernel_family https://en.wikipedia.org/wiki/L4_microkernel_family seems to describe it having been used all over the place, though mostly in embedded contexts. > OKL4 shipments exceeded 1.5 billion in early 2012,[4] mostly on Qualcomm wireless modem chips. Other deployments include automotive infotainment systems.[13] > Apple A series processors beginning with the A7 contain a Secure Enclave coprocessor running an L4 operating system[14] called sepOS (Secure Enclave Processor OS) based on the L4-embedded kernel developed at NICTA in 2006.[15] As a result, L4 ships on all modern Apple devices including Macs with Apple silicon.

ryao 2y ago
I feel like the two of you are talking past each other as the other poster is talking about time sharing systems like UNIX while you are pointing at embedded applications that are OS optional and if there is any semblance of an OS, it is really minimal. People deploying L4 there is not very surprising and does not apply to his remarks. Seeing this is like watching one person discuss an absence of apples and seeing another reply saying that there are oranges.
hannob 2y ago
Ok, admittedly, that's more than I expected. And hey, if they found some use cases in the embedded world, fine. Nevertheless, it's not exactly how it was pitched. This Microkernel thing always had a "Linux is doing it wrong, we're doing it better" story behind it. They wanted to be a replacement for a general-purpose OS. That cetainly hasn't happened.
- ryao 2y ago
  OSF/1 is the closest that microkernels ever came to being used in general purpose operating systems: https://en.wikipedia.org/wiki/OSF/1 https://en.wikipedia.org/wiki/OSF/1 The only still living variant is AIX. Some of the code is in the XNU kernel, although that is a monolithic kernel rather than a microkernel. Apple converted it to a monolithic design for performance reasons. That said, this article suggests that AIX is not using a microkernel either: https://tedium.co/2019/02/28/ibm-workplace-os-taligent-history/ https://tedium.co/2019/02/28/ibm-workplace-os-taligent-histo...
  - Zamiel_Snawley 2y ago
    Genode is an actively developed, general purpose desktop operating system that works today, and can use seL4, among other kernels.
  - skissane 2y ago
    > The only still living variant is AIX. This is incorrect. The thing you have to understand about “AIX” is that historically it was not a single codebase, it was just a common brand for multiple unrelated IBM Unix offerings. (DB2 is the same story.) One of those offerings was AIX/ESA for IBM mainframes - and that was indeed based on the OSF/1 microkernel. But AIX/ESA died in the early 1990s-it was replaced by turning MVS aka OS/390 into a certified Unix, a role carried on by z/OS today, and later on by z/Linux as well. Whereas, the only AIX that survives to this day is the RS/6000 branch which isn’t based on OSF/1, and has a classic monolithic kernel design. Its distant ancestor, AIX version 1 for the RT PC, did use a microkernel (VRM), but that microkernel was very different from Mach and OSF/1 (it was written in a PL/I dialect, PL.8, that’s how alien it was)
    - ryao 2y ago
      Thanks for the clarification.
    - pjmlp 2y ago
      Additionally it is the only UNIX that follows a Windows like approach to shared libraries, which might confuse folks coming from POSIX land.

dloss 2y ago

Well, an L4 variant is used in iPhones: "The Secure Enclave Processor runs an Apple-customized version of the L4 microkernel." https://support.apple.com/de-at/guide/security/sec59b0b31ff/web https://support.apple.com/de-at/guide/security/sec59b0b31ff/...

nabla9 2y ago

L4, L4Ka developed in Karlsruhe is not the same as seL4.

xxmarkuski 2y ago

Jochen Liedtke became a professor in 1999 in Karlsruhe, sadly he passed away only shortly after in 2001. I don't know if his successor Bellosa still does research on L4. There was the L4Ka project which appears to be completed. In the bachelor lecture on OS by him it's not part of the curriculum. Rittinghaus, alumni of Bellosa, is involved with Unikraft [0], which was featured a couple of times on hn, and is using unikernel technology. [0] https://unikraft.org/ https://unikraft.org/

__bjoernd 2y ago
After Liedtke's passing, L4 research was continued in groups at UNSW (Gernot Heiser, formal verification -> SeL4) and TU Dresden (Hermann Haertig, Fiasco/L4Re, focusing on real-time and secure systems). Genode (already mentioned in another comment) [1] came out of the TU Dresden group with some nice ideas around managing compartmentalized systems. Kernkonzept [2] is a startup commercializing the L4Re microkernel. [1] https://genode.org/ https://genode.org/ [2] https://www.kernkonzept.com/ https://www.kernkonzept.com/

senko 2y ago

I love the work (and the direction) the Karlsruhe team did on L4Ka, especially with Pistachio - the design was clean, simple, easy to grasp. I did a Pistachio-based OS for my diploma thesis (not at Karlsruhe). I always thought that if I'd been studying there, I'd probably go into OS research.

froh 2y ago

the L4Re derivative (open source) is running in every single id.X Volkswagen car in the central "icas1" ECU, carrying Linux and other guests. https://www.kernkonzept.com/kk_events/elektrobit-advances-automotive-safety-with-l4re/ https://www.kernkonzept.com/kk_events/elektrobit-advances-au... afaics the L4Re kernel also is part of Elektrobit Safe Linux.