[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Guix on a microkernel
From: |
mikadoZero |
Subject: |
Re: Guix on a microkernel |
Date: |
Mon, 01 Apr 2019 11:14:52 -0400 |
User-agent: |
mu4e 1.0; emacs 26.1 |
I do not have benchmark information.
Thank you for sharing the link.
address@hidden writes:
> 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 address@hidden:
>
>> # 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
>>
- Re: Guix on a microkernel,
mikadoZero <=