From mboxrd@z Thu Jan 1 00:00:00 1970 From: Subject: Re: Guix on a microkernel Date: Sun, 31 Mar 2019 08:54:03 +0200 (CEST) Message-ID: References: Mime-Version: 1.0 Content-Type: multipart/alternative; boundary="----=_Part_30661_1398126369.1554015243787" Return-path: Received: from eggs.gnu.org ([209.51.188.92]:44199) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1hAUM4-0007Ck-Ld for guix-devel@gnu.org; Sun, 31 Mar 2019 02:54:10 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1hAUM2-0005j5-Dk for guix-devel@gnu.org; Sun, 31 Mar 2019 02:54:08 -0400 Received: from w1.tutanota.de ([81.3.6.162]:3176) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1hAUM1-0005iK-Jn for guix-devel@gnu.org; Sun, 31 Mar 2019 02:54:06 -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: mikadoZero Cc: Guix-devel ------=_Part_30661_1398126369.1554015243787 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable 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 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.=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 b= eautiful!" > > 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 w= ith 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_minima= lity > > 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 > ------=_Part_30661_1398126369.1554015243787 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Thanks for your compilation.
Do you have found actual benchma= rk tests?
"The= Hurd is currently slower than Linux, yes. But not very much, so it is comp= letely usable."
Vulnerabil= ities of processors is also sensitive task. Maybe RISC-V will not have such= bugs? Need to know in a practice.

Mar 31, 2019, 1= 2:05 AM by mikadozero@yandex.com:
# Appreciation
<= div style=3D"16px" text-align=3D"left">
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 l= inux-libre (no
binary blo= bs) instead of the linux kernel.

* that work is und= erway to get Guix to work with GNU Hurd. I like that
a microkernel is a potential kernel option. =


* the effort that has been put into GNU Hurd to get it= to where it is.

# Inten= t

* I would like to understand why GNU Hurd is bein= g focused
on (my percepti= on) given other microkernel options.
* I want to share what I have found after doing some looking in= to
microkernels.
* I am curious what others think o= f microkernels.

=
I mention the appreciations above b= ecause I am aiming for a tone of
appreciation and curiosity and not a critical one. The tone can be = a
challenge for written co= mmunication.

# My microkernel experience
=

Currently I do not have any practical experience using any m= icrokernel.
I have just sp= ent time looking into the topic as it is interesting to
me.

# Why microkern= els?

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 mic= rokernels.

# GNU Hurd

## Pe= rceived focus

I looks to me like there is a effort = (which I appreciate) to get Guix
working on Hurd. I get this perception from:


The= se comments from this thread:

<= br>
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 u= p is fork which we need for running mescc."

## Crit= iques of Hurd

I would be curious what people think = about these third party critiques
(not mine) of Hurd.

### From X15


"Although the design of the Hurd is promising and attractive, its
<= /div>
implementation has a number of= severe issues. X15 takes the approach of
the complete rewrite to make sure that key ideas are kept i= n mind at all
times during= development. Since it=E2=80=99s not meant to be compatible with the
Hurd, critical interfaces such a= s IPC and signals can be re-implemented
completely differently. There is a lot of emphasis on code qu= ality and
ease of maintena= nce, obtained from disciplined application of best
practices."

### From Helen= OS

= http://www.helenos.org/wiki/FAQ#HowisHelenOSdifferentfromGNUHurd

### Why Hurd?

Why the focus on Hu= rd given other microkernel options? I ask this
question out of curiosity and a lack of practical exp= erience with
microkernels.=

# Microkernel wish list

Th= ese 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:

## 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:

ARM secu= rity issues:

### Ent= irely free RISC-V computers

These two initiatives a= re entirely free hardware based on RISC-V.

* HiFive= Unleashed
https://www.sifive.com/boards/hifive-unleashed

* lowRISC

## Formal verif= ication

An application of the minimality principle = in the design of microkernel
leads to smaller code bases which are amenable to formal verification. <= br>


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 i= nteresting microkernels
This is a high level summar= y based on the "Microkernel wish list" above.
All of these are free software. I am likely missing so= me other
interesting micro= kernel projects.

| projects | RISC-V efforts | = Formal verification |
|---= -----------+----------------+---------------------|
| sel4.systems | Yes | Yes = |
| genode.org | Ye= s | Yes |
| helenos.org | Yes | No |
| muen.sk | ?/No | = Yes |
| mi= nix3.org | ?/No | No |
| hurd.gnu.org | ?/No | No = |

Note:

* ?/No is wher= e (to me without asking) there does not look like there
have been efforts to make the project work w= ith 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

<= /div>
robigalia.org: based on seL4 = microkernel which is formally verified and
has RISC-V efforts underway. It is using Rust to build th= e parts that
would normall= y 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<= br>
project.

## Projects I have not looked into

I have= not looked at the following projects which were also listed on
http://www.microkernel.in= fo

* github.com/Nils-TUD/Escape
* github.com/f9micro
* l4re.org
* github.com/TUD-OS/M3
* hypervisor.org

------=_Part_30661_1398126369.1554015243787--