Microkernel & guix

Microkernel & guix

[David Craven]

Hi,

So I assume that many have already heard of the SEL4 microkernel that
contains a (~full) correctness proof (equivalence to the Haskell
functional model) and proof of various interesting properties
including confidentiality and integrity of the IPC communication and
worst case execution time for hard real time guarantees. [0]

Some other interesting developments in the OS scene is the Genode
operating system [1]. Genode is an implementation of the user-space
part of a microkernel based OS. It supports various microkernels
including the SEL4 and a handful of other microkernel implementations.
It has a driver execution environment for repurposing Linux drivers,
iPXE drivers and NetBSD drivers and provides a POSIX interface to
existing applications.

I think at some point it would be nice to start thinking about how
guix and genode could complement each other. Work is being done on
exploring how nix can help genode with it's "package management
problems" [2]. I suggest waiting to see what develops from that first.

Just thought I'd share in case someone is interested :) And make sure
that Guix devs stay on top of current developements =P

[0] https://github.com/seL4/seL4
[1] https://github.com/genodelabs/genode
[2] https://github.com/ehmry/genode-nix

Re: Microkernel & guix

[Ludovic Courtès]

Hello!

Thanks for sharing!  I’m aware of the developments, and I think each of
them brings a lot.

There’s also this thing called “GNU/Hurd”.  ;-)  People like to make fun
of it, and indeed there’s a lot to be said on how the project used to be
unable to publish releases, or how it lacked drivers.

But I think that (1) the situation has improved (on the driver side, it
now uses Rump for sound and networking drivers), and (2) few people
realize that it’s the most practical of all these microkernel-based OS
projects: it has all the GNU user-land software and a full POSIX
personality, which in turn means that today it can run GNOME, KDE,
IceCat, LibreOffice, and whatnot.  To me that’s an important feature.

My 2¢.  :-)

Ludo’.

Re: Microkernel & guix

[ng0]

Ludovic Courtès <ludo@gnu.org> writes:

> Hello!
>
> Thanks for sharing!  I’m aware of the developments, and I think each of
> them brings a lot.
>
> There’s also this thing called “GNU/Hurd”.  ;-)  People like to make fun
> of it, and indeed there’s a lot to be said on how the project used to be
> unable to publish releases, or how it lacked drivers.
…
> Ludo’.

I think it would be nice to explore a multiplicity of options in
addition to Hurd, if possible.
So if someone is willing to start a port, it will take a long
time anyway.

-- 
♥Ⓐ  ng0  | PGP keys and more: https://n0is.noblogs.org/
         |                    http://ng0.chaosnet.org

Re: Microkernel & guix

[David Craven]

So after doing some hardcore reading of most of the genode operating
system manual today (excluding the build system, under the hood and
functional specification parts) I think I have a better understanding
of how guix and genode could complement each other and what steps
could be taken. Here are my initial thoughts:

1. genode-build-system would be used for building genode components.
2. genode-operating-system would specify the configuration of genode
components and generate their xml configuration and guix system vm
would assemble a full bootable genode system.
3. guix-daemon component based on the nix-daemon component is needed.
4. using this new component support for generations and genode system
reconfiguration can be added
5. a shepherd component is created and the genode-operating-system is
extended to take one or more operating-system declarations to spawn
guix userspaces. For a genode-operating-system implementing a headless
hypervisor each application can run in it's own shepherd component,
maybe requiring an additional shepherd-multiplexer component. If
building a desktop os it can be run in a single shepherd component
with exclusive access to the framebuffer and input components.

I'll have to see if my time, skill and discipline is enough to
materialize into something useful :)

Re: Microkernel & guix

[Ludovic Courtès]

David Craven <david@craven.ch> skribis:

> So after doing some hardcore reading of most of the genode operating
> system manual today (excluding the build system, under the hood and
> functional specification parts) I think I have a better understanding
> of how guix and genode could complement each other and what steps
> could be taken. Here are my initial thoughts:
>
> 1. genode-build-system would be used for building genode components.
> 2. genode-operating-system would specify the configuration of genode
> components and generate their xml configuration and guix system vm
> would assemble a full bootable genode system.
> 3. guix-daemon component based on the nix-daemon component is needed.
> 4. using this new component support for generations and genode system
> reconfiguration can be added
> 5. a shepherd component is created and the genode-operating-system is
> extended to take one or more operating-system declarations to spawn
> guix userspaces. For a genode-operating-system implementing a headless
> hypervisor each application can run in it's own shepherd component,
> maybe requiring an additional shepherd-multiplexer component. If
> building a desktop os it can be run in a single shepherd component
> with exclusive access to the framebuffer and input components.
>
> I'll have to see if my time, skill and discipline is enough to
> materialize into something useful :)

Sounds like fun anyway.  :-)

Ludo’.