From: mikadoZero <mikadozero@yandex.com>
To: Guix-devel <guix-devel@gnu.org>
Subject: Guix on a microkernel
Date: Sat, 30 Mar 2019 20:05:40 -0400 [thread overview]
Message-ID: <cuc36n36h7v.fsf@yandex.com> (raw)
# 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
* 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.
* 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
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’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/
"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
### 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.
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.
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/ 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/
* github.com/Nils-TUD/Escape
* github.com/f9micro
* l4re.org
* github.com/TUD-OS/M3
* hypervisor.org
next reply other threads:[~2019-03-31 0:06 UTC|newest]
Thread overview: 10+ messages / expand[flat|nested] mbox.gz Atom feed top
2019-03-31 0:05 mikadoZero [this message]
2019-03-31 6:54 ` Guix on a microkernel znavko
2019-04-01 15:14 ` mikadoZero
2019-03-31 14:08 ` Pjotr Prins
2019-04-01 15:18 ` mikadoZero
2019-04-01 15:33 ` Ludovic Courtès
2019-04-02 17:53 ` Joshua Branson
2019-04-28 19:54 ` Vasilii Kolobkov
2019-04-29 10:21 ` Pronaip
2019-04-30 16:07 ` mikadoZero
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
List information: https://guix.gnu.org/
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=cuc36n36h7v.fsf@yandex.com \
--to=mikadozero@yandex.com \
--cc=guix-devel@gnu.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
Code repositories for project(s) associated with this public inbox
https://git.savannah.gnu.org/cgit/guix.git
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).