From mboxrd@z Thu Jan 1 00:00:00 1970 From: mikadoZero Subject: Guix on a microkernel Date: Sat, 30 Mar 2019 20:05:40 -0400 Message-ID: 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]:59860) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1hANzY-0007bf-3G for guix-devel@gnu.org; Sat, 30 Mar 2019 20:06:29 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1hANzW-0003v9-5U for guix-devel@gnu.org; Sat, 30 Mar 2019 20:06:28 -0400 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: Guix-devel # 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 bea= utiful!" 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 wit= h 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_minimali= ty 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 * github.com/Nils-TUD/Escape * github.com/f9micro * l4re.org * github.com/TUD-OS/M3 * hypervisor.org