1. 19
    1. 8

      This was presented in 2020-01, where proof was “due Q1’20”. FYI, Proof got finished in 2020-06: https://microkerneldude.wordpress.com/2020/06/09/sel4-is-verified-on-risc-v/

    2. 2

      How far away are we from a world where a developer could use seL4 on RISC-V as their daily driver?

      1. 6

        It would depend on what the requisites for daily driver are.

        Right now, devkits with desktop-capable ASICs (e.g. hifive freedom unleashed, with pci-e so that you can e.g. attach a GPU) are expensive, and aren’t amazingly fast.

        V extension (vector instructions, due this September) and B extension (bit manipulation instructions, due soon) will improve the performance considerably, and allow for the applications to expand. I expect competitive smartphone SoCs by next year.

        When no vector instructions are involved, IPC of this oshw implementation is competitive with Intel SkyLake already: https://carrv.github.io/2020/papers/CARRV2020_paper_15_Zhao.pdf

        So expect decent performance from proprietary implementations by risc-v org members.

      2. 3

        I think this is doable within five years, but if and only if enough money and effort is spent on it.

      3. 2

        I don’t think there is any roadmap to a desktop-style OS running on seL4.

        Their applications are more around safety- and security-critical embedded systems. From their About page:

        seL4 is part of an ecosystem supporting active use in various domains including automotive, aviation, infrastructure, medical, and defence

        So the hypothetical developer would be more likely to own a car, fly on a plane, or be exploded by a weapons system running seL4 internally.

        1. 2

          Understood, and thanks for the answer. I think it’s a shame that security, trustworthiness and reliability tend not to be given a higher priority by desktop operating systems. I’m aware of the L4Linux project, which runs a linux kernel on top of L4, but I don’t know how well that works with sel4.

          1. 1

            Making desktop operating systems is a large endeavor which they do well to stay away from.

            It absolutely doesn’t mean seL4, the microkernel, isn’t capable for the task. It simply means that they have limited manpower and would rather work on seL4 itself and the essential ecosystem around it.

            Thus this is left to third parties. A third party working on such a thing would be Genode; Sculpt specifically.