Re: Guix on a microkernel

[<znavko@tutanota.com>]

[-- Attachment #1: Type: text/plain, Size: 7421 bytes --]

Thanks for your compilation.
Do you have found actual benchmark tests? 
https://www.gnu.org/software/hurd/faq/slow.html <https://www.gnu.org/software/hurd/faq/slow.html>
"The Hurd is currently slower than Linux, yes. But not very much, so it is completely usable."
Vulnerabilities of processors is also sensitive task. Maybe RISC-V will not have such bugs? Need to know in a practice.

Mar 31, 2019, 12:05 AM by mikadozero@yandex.com:

> # Appreciation
>
> I appreciate:
>
> * many of Guix's design decisions.  The one that is relevant to this
>  discussion is the kernel.  I like that Guix uses the linux-libre (no
>  binary blobs) instead of the linux kernel.
>
> * that work is underway to get Guix to work with GNU Hurd.  I like that
>  a microkernel is a potential kernel option. 
>
>  > http://lists.gnu.org/archive/html/guix-devel/2016-12/msg00857.html <http://lists.gnu.org/archive/html/guix-devel/2016-12/msg00857.html>
>
> * the effort that has been put into GNU Hurd to get it to where it is.
>
> * the bootsrapping initiative.
>
>  > https://bootstrappable.org <https://bootstrappable.org/>
>  > https://fosdem.org/2019/schedule/event/gnumes <https://fosdem.org/2019/schedule/event/gnumes/>
>
> # Intent
>
> * I would like to understand why GNU Hurd is being focused
>  on (my perception) given other microkernel options. 
> * I want to share what I have found after doing some looking into
>  microkernels.
> * I am curious what others think of microkernels.
>
> I mention the appreciations above because I am aiming for a tone of
> appreciation and curiosity and not a critical one.  The tone can be a
> challenge for written communication. 
>
> # My microkernel experience
>
> Currently I do not have any practical experience using any microkernel.
> I have just spent time looking into the topic as it is interesting to
> me.
>
> # Why microkernels?
>
> I think Andrew Tanenbaum explains benefits of microkernel entertainingly
> in this talk:
> http://www.youtube.com/watch?v=bx3KuE7UjGA <http://www.youtube.com/watch?v=bx3KuE7UjGA>
>
> The talks has a focus on Minix but I think the benefits are transferable
> to other microkernels.
>
> # GNU Hurd
>
> ## Perceived focus
>
> I looks to me like there is a effort (which I appreciate) to get Guix
> working on Hurd.  I get this perception from:
>
> http://lists.gnu.org/archive/html/guix-devel/2016-12/msg00857.html <http://lists.gnu.org/archive/html/guix-devel/2016-12/msg00857.html>
>
> These comments from this thread:
>
> https://lists.gnu.org/archive/html/help-guix/2019-03/msg00158.html <https://lists.gnu.org/archive/html/help-guix/2019-03/msg00158.html>
>
> Ricardo Wurmus:  "Let’s work on the Hurd, people!  It’s beautiful!"
>
> Jan Nieuwenhuizen: "FWIW the Mes port to the Hurd is ongoing and mes now
> runs, next thing up is fork which we need for running mescc."
>
> ## Critiques of Hurd
>
> I would be curious what people think about these third party critiques
> (not mine) of Hurd.
>
> ### From X15
>
> https://www.sceen.net/x15 <https://www.sceen.net/x15/>
>
> "Although the design of the Hurd is promising and attractive, its
> implementation has a number of severe issues. X15 takes the approach of
> the complete rewrite to make sure that key ideas are kept in mind at all
> times during development. Since it’s not meant to be compatible with the
> Hurd, critical interfaces such as IPC and signals can be re-implemented
> completely differently. There is a lot of emphasis on code quality and
> ease of maintenance, obtained from disciplined application of best
> practices."
>
> ### From HelenOS
>
> http://www.helenos.org/wiki/FAQ#HowisHelenOSdifferentfromGNUHurd <http://www.helenos.org/wiki/FAQ#HowisHelenOSdifferentfromGNUHurd>
>
> ### Why Hurd?
>
> Why the focus on Hurd given other microkernel options?  I ask this
> question out of curiosity and a lack of practical experience with
> microkernels.
>
> # Microkernel wish list
>
> These are things that I see as desirable in a microkernel.
>
> ## Free software
>
> It should be completely free software.  No binary blobs included.  It
> looks like all of the microkernel listed here are:
> http://www.microkernel.info <http://www.microkernel.info/>
>
> ## RISC-V
>
> RISC-V a free and open instruction set architecture is a nice complement
> to a free operating system.  It is nice if a mircokernel already has
> plans to run on RISC-V. 
>
> Intel security issues:
> https://libreboot.org/faq.html#intel <https://libreboot.org/faq.html#intel>
>
> ARM security issues:
> https://libreboot.org/faq.html#amd <https://libreboot.org/faq.html#amd>
>
> ### Entirely free RISC-V computers
>
> These two initiatives are entirely free hardware based on RISC-V.
>
> * HiFive Unleashed
>  > https://www.sifive.com/boards/hifive-unleashed <https://www.sifive.com/boards/hifive-unleashed>
>
> * lowRISC
>  > https://www.lowrisc.org <https://www.lowrisc.org>
>
> ## Formal verification
>
> An application of the minimality principle in the design of microkernel
> leads to smaller code bases which are amenable to formal verification. 
>
> https://en.wikipedia.org/wiki/Microkernel#Essential_components_and_minimality <https://en.wikipedia.org/wiki/Microkernel#Essential_components_and_minimality>
>
> I see the extra security assurance that formal verification provide as
> desirable.
>
> # Alternative microkernels
>
> I used > http://www.microkernel.info <http://www.microkernel.info/>>  as the starting point when I began
> looking into microkernels. 
>
> ## Summary of interesting microkernels
>
> This is a high level summary based on the "Microkernel wish list" above.
> All of these are free software.  I am likely missing some other
> interesting microkernel projects.
>
> | projects     | RISC-V efforts | Formal verification |
> |--------------+----------------+---------------------|
> | sel4.systems | Yes            | Yes                 |
> | genode.org   | Yes            | Yes                 |
> | helenos.org  | Yes            | No                  |
> | muen.sk      | ?/No           | Yes                 |
> | minix3.org   | ?/No           | No                  |
> | hurd.gnu.org | ?/No           | No                  |
>
> Note:
>
> * ?/No is where (to me without asking) there does not look like there
>  have been efforts to make the project work with RISC-V. 
>
> * Genode is different than the others as it is not just a microkernel.
>  I have given Genode Yes for both RISC-V and Formal verification
>  because it can use the seL4 microkernel.  It can also use other
>  microkernels beyond just seL4.
>
> ## Other interesting projects
>
> robigalia.org:  based on seL4 microkernel which is formally verified and
> has RISC-V efforts underway.  It is using Rust to build the parts that
> would normally be part of a monolithic kernel in user space.  It looks
> like a young project.
>
> redox-os.org:  Rust based microkernel project.  It looks like a young
> project. 
>
> ## Projects I have not looked into
>
> I have not looked at the following projects which were also listed on
> http://www.microkernel.info <http://www.microkernel.info/>>  
>
> * github.com/Nils-TUD/Escape
> * github.com/f9micro
> * l4re.org
> * github.com/TUD-OS/M3
> * hypervisor.org
>


[-- Attachment #2: Type: text/html, Size: 16718 bytes --]