6 ms·

Yeah, I wish they had teamed up with Robigalia in order to build on seL4 or at least translated that 1:1 to Rust, foregoing the verified nature of seL4.

by cm3 10y ago

snvzz 10y ago
> foregoing the verified nature of seL4 If anything, seL4 is the fastest L4 out there, proving that they can be fast and proven at the same time. So, why would anyone want to do that?
- cm3 10y ago
  Because Redox's aim is to be as little non-Rust as possible. I agree it'd be ill-advised to rewrite seL4 rather than use it, even though it's been a while since a revision was verified, because it's been battle tested, is continually improved and small enough to trust.
  - cm3 10y ago
    We really need to have a mainstream desktop microkernel operating system because: 1. no need anymore for kernel bypass mechanisms (too many to name for linux, btw) 2. decoupling of drivers from the kernel 3. instead of waiting for a backport of a new syscall to an LTS kernel, something like that will be just part of your system's stdlib 4. extremely reduced need to reboot a machine 5. driver faults can be recovered from gracefully, just like in Erlang's supervisor scheme 6. seL4's capability system allows for a safer system overall, with less hacks Seeing how even Intel is introducing a message passing network with growing number of cores in their mainstream CPU designs, we should be over the general objections regarding a message passing design. They call it QMD, and it's something they already have in their Xeon Phi line for some time for obvious reasons, just as countless other general purpose or special purpose chip designs have had for a long time. I wonder if one could get funding for an effort like Robigalia to reach production quality and have Servo running on it. Given the feature set of Servo, it's a safe bet that the required features would provide a reasonably complete system to replace your Linux machine. The bigger struggle would be getting hardware vendors to contribute to FreeBSD and Linux drivers to also provide some level of support for a non-C code base. Though, moving up to that abstraction and language level should make it easier to write working hardware drivers.
    - cm3 10y ago
      Oh, and if you extend it with multi-kernel functionality, scaling to very large number of cores/chips will also be solved in a fundamentally cleaner way. I haven't looked into it but there's an seL4 branch that implements multi-kernel support. If you don't know what this is, it's simply a way to have one kernel instance per processor, making scalability easier. Fujitsu has a linux variant to achieve the same and I think it's a goal of Barrelfish as well. Similar solutions exist in certain linux and dragonflybsd subsystems where, say, the network stack uses one scheduler or queue per core, removing the need for synchronization in a coarse way. Then, of course, you have to be smarter about scheduling things, but if you bind certain hardware bits to cores long-term, it should avoid accidental overhead via random migration. Language runtime VMs do the same for green threads with job stealing designs and pinning schedulers to cores. None of it is bleeding edge research material, we just have to use what's been invented.
      - brandmeyer 10y ago
        I'm not sure that you need a kernel per-core. However, it would be nice for the microkernel to provide reliably per-cpu data structures to userspace. For example, via per-cpu replicated receive capabilities. That way, a capability send request from a client program would get routed to the same CPU's capability in the server. That would provide some very cache-friendly superfast machine-local IPC.
      - johncolanduoni 10y ago
        Completely eliminating shared-memory multiprocessing in userspace seems like a non-starter to me. Message passing is great, but there are plenty of cases where it's slower by many orders of magnitude. A good example is sparse matrix solvers; there's no way to get any kind of acceptable performance if you can't share the underlying data.
    - cmrx64 10y ago
      > I wonder if one could get funding for an effort like Robigalia to reach production quality and have Servo running on it. Given the feature set of Servo, it's a safe bet that the required features would provide a reasonably complete system to replace your Linux machine. If I got funding, Robigalia would definitely progress at least 10x faster than it does currently :) If anyone is interested in that, email me: corey@octayn.net... As an aside, Robigalia has been picking up steam. The first developer preview should be out by Robigalia 2017 (April 25). Design documents and prototypes should be out by December 26 (the project's anniversary).
  - cmrx64 10y ago
    the master branch of sel4 is always passing verification, for the verified platform: armv7-a on a Sabre Lite. the x86_64 verification is coming out soon according to the roadmap.
cmrx64 10y ago
I wrote on their forum about why they "shouldn't" use seL4, and definitely shouldn't port it to Rust: https://discourse.redox-os.org/t/why-not-port-sel4-microkernel-instead-of-starting-from-scratch/337/5 https://discourse.redox-os.org/t/why-not-port-sel4-microkern... If the goal is trusthworthy, reliable software, then you should use seL4. If the goal is to yell about how great Rust is, you could port seL4 to Rust.
- pjmlp 10y ago
  Fully support your point of view. What we always see on programming languages is that when shortcuts for arriving faster at our goals are taken, usually they give ammunition to remarks of the sort "language X cannot do Y". Apparently most lack vision and need to be proven wrong. So I hope they manage to just use Rust and Assembly. EDIT: Improved the sentence

Yeah, I wish they had teamed up with Robigalia in order to build on seL4 or at least translated that 1:1 to Rust, foregoing the verified nature of seL4.

by cm3 10y ago

Yeah, I wish they had teamed up with Robigalia in order to build on seL4 or at least translated that 1:1 to Rust, foregoing the verified nature of seL4.

snvzz 10y ago

> foregoing the verified nature of seL4 If anything, seL4 is the fastest L4 out there, proving that they can be fast and proven at the same time. So, why would anyone want to do that?

cm3 10y ago
Because Redox's aim is to be as little non-Rust as possible. I agree it'd be ill-advised to rewrite seL4 rather than use it, even though it's been a while since a revision was verified, because it's been battle tested, is continually improved and small enough to trust.
- cm3 10y ago
  We really need to have a mainstream desktop microkernel operating system because: 1. no need anymore for kernel bypass mechanisms (too many to name for linux, btw) 2. decoupling of drivers from the kernel 3. instead of waiting for a backport of a new syscall to an LTS kernel, something like that will be just part of your system's stdlib 4. extremely reduced need to reboot a machine 5. driver faults can be recovered from gracefully, just like in Erlang's supervisor scheme 6. seL4's capability system allows for a safer system overall, with less hacks Seeing how even Intel is introducing a message passing network with growing number of cores in their mainstream CPU designs, we should be over the general objections regarding a message passing design. They call it QMD, and it's something they already have in their Xeon Phi line for some time for obvious reasons, just as countless other general purpose or special purpose chip designs have had for a long time. I wonder if one could get funding for an effort like Robigalia to reach production quality and have Servo running on it. Given the feature set of Servo, it's a safe bet that the required features would provide a reasonably complete system to replace your Linux machine. The bigger struggle would be getting hardware vendors to contribute to FreeBSD and Linux drivers to also provide some level of support for a non-C code base. Though, moving up to that abstraction and language level should make it easier to write working hardware drivers.
  - cm3 10y ago
    Oh, and if you extend it with multi-kernel functionality, scaling to very large number of cores/chips will also be solved in a fundamentally cleaner way. I haven't looked into it but there's an seL4 branch that implements multi-kernel support. If you don't know what this is, it's simply a way to have one kernel instance per processor, making scalability easier. Fujitsu has a linux variant to achieve the same and I think it's a goal of Barrelfish as well. Similar solutions exist in certain linux and dragonflybsd subsystems where, say, the network stack uses one scheduler or queue per core, removing the need for synchronization in a coarse way. Then, of course, you have to be smarter about scheduling things, but if you bind certain hardware bits to cores long-term, it should avoid accidental overhead via random migration. Language runtime VMs do the same for green threads with job stealing designs and pinning schedulers to cores. None of it is bleeding edge research material, we just have to use what's been invented.
    - brandmeyer 10y ago
      I'm not sure that you need a kernel per-core. However, it would be nice for the microkernel to provide reliably per-cpu data structures to userspace. For example, via per-cpu replicated receive capabilities. That way, a capability send request from a client program would get routed to the same CPU's capability in the server. That would provide some very cache-friendly superfast machine-local IPC.
    - johncolanduoni 10y ago
      Completely eliminating shared-memory multiprocessing in userspace seems like a non-starter to me. Message passing is great, but there are plenty of cases where it's slower by many orders of magnitude. A good example is sparse matrix solvers; there's no way to get any kind of acceptable performance if you can't share the underlying data.
  - cmrx64 10y ago
    > I wonder if one could get funding for an effort like Robigalia to reach production quality and have Servo running on it. Given the feature set of Servo, it's a safe bet that the required features would provide a reasonably complete system to replace your Linux machine. If I got funding, Robigalia would definitely progress at least 10x faster than it does currently :) If anyone is interested in that, email me: corey@octayn.net... As an aside, Robigalia has been picking up steam. The first developer preview should be out by Robigalia 2017 (April 25). Design documents and prototypes should be out by December 26 (the project's anniversary).
- cmrx64 10y ago
  the master branch of sel4 is always passing verification, for the verified platform: armv7-a on a Sabre Lite. the x86_64 verification is coming out soon according to the roadmap.

cmrx64 10y ago

I wrote on their forum about why they "shouldn't" use seL4, and definitely shouldn't port it to Rust: https://discourse.redox-os.org/t/why-not-port-sel4-microkernel-instead-of-starting-from-scratch/337/5 https://discourse.redox-os.org/t/why-not-port-sel4-microkern... If the goal is trusthworthy, reliable software, then you should use seL4. If the goal is to yell about how great Rust is, you could port seL4 to Rust.

pjmlp 10y ago
Fully support your point of view. What we always see on programming languages is that when shortcuts for arriving faster at our goals are taken, usually they give ammunition to remarks of the sort "language X cannot do Y". Apparently most lack vision and need to be proven wrong. So I hope they manage to just use Rust and Assembly. EDIT: Improved the sentence