4 ms·

Sure Genode: https://www.genodians.org/tomga/2019-07-07-rpi-booting https://www.genodians.org/tomga/2019-07-07-rpi-booting FreeRTOS: https://de.wikipedia.or

by nix23 6y ago

Sure Genode: https://www.genodians.org/tomga/2019-07-07-rpi-booting https://www.genodians.org/tomga/2019-07-07-rpi-booting FreeRTOS: https://de.wikipedia.org/wiki/FreeRTOS https://de.wikipedia.org/wiki/FreeRTOS seL4: https://research.csiro.au/tsblog/sel4-raspberry-pi-3/ https://research.csiro.au/tsblog/sel4-raspberry-pi-3/ Fiasco: https://l4re.org/fiasco/features.html https://l4re.org/fiasco/features.html

monocasa 6y ago
FreeRTOS isn't really a microkernel. It arguably doesn't really have a kernel. Also, Genode is a user land. Saying Genode and sel4/fiasco is like saying Debian _and_ Linux.
- nix23 6y ago
  >FreeRTOS isn't really a microkernel. https://www.freertos.org/RTOS.html https://www.freertos.org/RTOS.html >Also, Genode is a user land. No it's a operating system framework, and every kernel they provide is a micro-kernel. > Saying Genode and sel4/fiasco is like saying Debian _and_ Linux. Debian is a Distribution, Linux is a Kernel, you could have said Gnu/Linux and you where less wrong, but your comment is utter bullshit and full of flaws, with my links seL4 and fiasco you have a "fully" working system, reading your comment it's like saying that Linux from scratch is just a kernel.
  - monocasa 6y ago
    > FreeRTOS... I don't really care what FreeRTOS's site says. There's no way to ship a FreeRTOS implementation that doesn't link the drivers (and the user application for that matter) directly into the kernel. It's not a microkernel, but stems from an era when microkernel was such a buzzword people tried to apply the term to operating systems that didn't even have processes. I think they were thinking that if early VXWorks got to call themselves a microkernel then FreeRTOS gets to as well. > No it's a operating system framework, and every kernel they provide is a micro-kernel. Right so the code Genode provides is a userland. They don't have their own kernel but instead give you a selection of several third party kernels. > your comment is utter bullshit and full of flaws Please keep your comments civil. > with my links seL4 and fiasco you have a "fully" working system, reading your comment it's like saying that Linux from scratch is just a kernel. No, you don't have a '"fully" working system'. seL4 for instance needs something like Genode or CAmkES to get there. seL4 in it's verified mode doesn't even have any I/O in it's codebase (and unverified only provides a debug UART). Fiasco needs something like Genode or L4RE. And no, Linux from scratch is very very close to CAmkES/Genode. It'd be almost a 1-1 if Linux from scratch had a more standard build system across it's components.
    - nix23 6y ago
      >I don't really care what FreeRTOS's site says. And i dont care what you personal believe of a Kernel is. https://www.freertos.org/a00020.html https://www.freertos.org/a00020.html >Right so the code Genode provides is a userland. They don't have their own kernel but instead give you a selection of several third party kernels. Like Debian right? The Kernel's are (where) Hurd, Linux and, kFreeBSD >And no, Linux from scratch is very very close to CAmkES/Genode. Ahh an Operating-system with Userland and a Kernel right? >Fiasco needs something like Genode or L4RE Something like...NO its called Userland and you can add them like in LFS.
      - monocasa 6y ago
        > And i dont care what you personal believe of a Kernel is. > https://www.freertos.org/a00020.html https://www.freertos.org/a00020.html That's literally the documentation for what you can directly link against the kernel as a driver writer. That link if anything proves that it's not a microkernel. (By the way, you're talking to someone who's written a few FreeRTOS BSPs). > Like Debian right? The Kernel's are (where) Hurd, Linux and, kFreeBSD So wait, is Genode like Debian or not? You were fighting that just a comment ago.
akavel 6y ago
Unfortunately Genode support for RPi 3 seems to be not yet in a working state, and even then I don't know how much it would translate to RPi 4; see: https://github.com/genodelabs/genode/issues?q=is%3Aissue+is%3Aopen+raspberry https://github.com/genodelabs/genode/issues?q=is%3Aissue+is%... Both seL4 and Fiasco are microkernel names, not full OSes built on those 'kernels, I was asking about OSes. IOW, AFAIU neither seL4 nor Fiasco provide clock or Ethernet drivers for RPi4. Or do they? As to FreeRTOS, people seem to mention it's not really microkernel-based at all? I am interested in proper isolation, so that a crashed filesystem driver can be restarted without taking down other independent drivers, or unloaded completely on the fly. I will take look on it, from wikipedia alone it's not yet clear to me if it has this feature. Thanks for the mention!

by nix23 6y ago

monocasa 6y ago

FreeRTOS isn't really a microkernel. It arguably doesn't really have a kernel. Also, Genode is a user land. Saying Genode and sel4/fiasco is like saying Debian _and_ Linux.

nix23 6y ago
>FreeRTOS isn't really a microkernel. https://www.freertos.org/RTOS.html https://www.freertos.org/RTOS.html >Also, Genode is a user land. No it's a operating system framework, and every kernel they provide is a micro-kernel. > Saying Genode and sel4/fiasco is like saying Debian _and_ Linux. Debian is a Distribution, Linux is a Kernel, you could have said Gnu/Linux and you where less wrong, but your comment is utter bullshit and full of flaws, with my links seL4 and fiasco you have a "fully" working system, reading your comment it's like saying that Linux from scratch is just a kernel.
- monocasa 6y ago
  > FreeRTOS... I don't really care what FreeRTOS's site says. There's no way to ship a FreeRTOS implementation that doesn't link the drivers (and the user application for that matter) directly into the kernel. It's not a microkernel, but stems from an era when microkernel was such a buzzword people tried to apply the term to operating systems that didn't even have processes. I think they were thinking that if early VXWorks got to call themselves a microkernel then FreeRTOS gets to as well. > No it's a operating system framework, and every kernel they provide is a micro-kernel. Right so the code Genode provides is a userland. They don't have their own kernel but instead give you a selection of several third party kernels. > your comment is utter bullshit and full of flaws Please keep your comments civil. > with my links seL4 and fiasco you have a "fully" working system, reading your comment it's like saying that Linux from scratch is just a kernel. No, you don't have a '"fully" working system'. seL4 for instance needs something like Genode or CAmkES to get there. seL4 in it's verified mode doesn't even have any I/O in it's codebase (and unverified only provides a debug UART). Fiasco needs something like Genode or L4RE. And no, Linux from scratch is very very close to CAmkES/Genode. It'd be almost a 1-1 if Linux from scratch had a more standard build system across it's components.
  - nix23 6y ago
    >I don't really care what FreeRTOS's site says. And i dont care what you personal believe of a Kernel is. https://www.freertos.org/a00020.html https://www.freertos.org/a00020.html >Right so the code Genode provides is a userland. They don't have their own kernel but instead give you a selection of several third party kernels. Like Debian right? The Kernel's are (where) Hurd, Linux and, kFreeBSD >And no, Linux from scratch is very very close to CAmkES/Genode. Ahh an Operating-system with Userland and a Kernel right? >Fiasco needs something like Genode or L4RE Something like...NO its called Userland and you can add them like in LFS.
    - monocasa 6y ago
      > And i dont care what you personal believe of a Kernel is. > https://www.freertos.org/a00020.html https://www.freertos.org/a00020.html That's literally the documentation for what you can directly link against the kernel as a driver writer. That link if anything proves that it's not a microkernel. (By the way, you're talking to someone who's written a few FreeRTOS BSPs). > Like Debian right? The Kernel's are (where) Hurd, Linux and, kFreeBSD So wait, is Genode like Debian or not? You were fighting that just a comment ago.

akavel 6y ago

Unfortunately Genode support for RPi 3 seems to be not yet in a working state, and even then I don't know how much it would translate to RPi 4; see: https://github.com/genodelabs/genode/issues?q=is%3Aissue+is%3Aopen+raspberry https://github.com/genodelabs/genode/issues?q=is%3Aissue+is%... Both seL4 and Fiasco are microkernel names, not full OSes built on those 'kernels, I was asking about OSes. IOW, AFAIU neither seL4 nor Fiasco provide clock or Ethernet drivers for RPi4. Or do they? As to FreeRTOS, people seem to mention it's not really microkernel-based at all? I am interested in proper isolation, so that a crashed filesystem driver can be restarted without taking down other independent drivers, or unloaded completely on the fly. I will take look on it, from wikipedia alone it's not yet clear to me if it has this feature. Thanks for the mention!