From mboxrd@z Thu Jan 1 00:00:00 1970 From: mikadoZero Subject: Re: Guix on a microkernel Date: Mon, 01 Apr 2019 11:14:52 -0400 Message-ID: References: Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Return-path: Received: from eggs.gnu.org ([209.51.188.92]:33372) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1hAyf5-0008Dg-Gi for guix-devel@gnu.org; Mon, 01 Apr 2019 11:15:49 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1hAyf2-0006Op-RJ for guix-devel@gnu.org; Mon, 01 Apr 2019 11:15:47 -0400 Received: from forward105j.mail.yandex.net ([5.45.198.248]:47742) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1hAyf1-0006Di-U3 for guix-devel@gnu.org; Mon, 01 Apr 2019 11:15:44 -0400 In-reply-to: List-Id: "Development of GNU Guix and the GNU System distribution." List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-devel-bounces+gcggd-guix-devel=m.gmane.org@gnu.org Sender: "Guix-devel" To: znavko@tutanota.com Cc: Guix-devel I do not have benchmark information. Thank you for sharing the link. znavko@tutanota.com writes: > Thanks for your compilation. > Do you have found actual benchmark tests?=20 > https://www.gnu.org/software/hurd/faq/slow.html > "The Hurd is currently slower than Linux, yes. But not very much, so it i= s completely usable." > Vulnerabilities of processors is also sensitive task. Maybe RISC-V will n= ot 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.=20 >> >> > 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://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.=20 >> * 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.=20 >> >> # 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=3Dbx3KuE7UjGA >> >> 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 >> >> These comments from this thread: >> >> https://lists.gnu.org/archive/html/help-guix/2019-03/msg00158.html >> >> Ricardo Wurmus: "Let=E2=80=99s work on the Hurd, people! It=E2=80=99s = 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 >> >> "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=E2=80=99s 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 >> >> ### 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 >> >> ## 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.=20 >> >> Intel security issues: >> https://libreboot.org/faq.html#intel >> >> ARM security issues: >> 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 >> >> * lowRISC >> > 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.=20 >> >> https://en.wikipedia.org/wiki/Microkernel#Essential_components_and_minim= ality >> >> I see the extra security assurance that formal verification provide as >> desirable. >> >> # Alternative microkernels >> >> I used > http://www.microkernel.info > as= the starting point when I began >> looking into microkernels.=20 >> >> ## 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.=20 >> >> * 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.=20 >> >> ## Projects I have not looked into >> >> I have not looked at the following projects which were also listed on >> http://www.microkernel.info >=20=20 >> >> * github.com/Nils-TUD/Escape >> * github.com/f9micro >> * l4re.org >> * github.com/TUD-OS/M3 >> * hypervisor.org >>