Guix and sel4

Guix and sel4

[radoslaw]

Hi,

In 2016 David Craven has sent an email about his attempt in using sel4 
(genode with sel4 to be exact) with guix 
(https://lists.gnu.org/archive/html/help-guix/2016-12/msg00058.html). Do 
You know if he succeeded or not? And if not where there any substantial 
blockers or just lack of time?

Also while I'm asking would it be possible to use only the microkernel 
without the genode ecosystem in the guixsd? And on that topic is guixsd 
able to cross-compile? It already has the sandboxing for the packages so 
I would imagine it couldn't be that difficult but maybe it wasn't tried 
out before. I should probably RTFM but this is just a side-note 
question.

Cheers,
Radek

Re: Guix and sel4

[Paul Boddie]

On Sunday 14. January 2018 22.16.39 radoslaw@chmielarz.xyz wrote:
> 
> In 2016 David Craven has sent an email about his attempt in using sel4
> (genode with sel4 to be exact) with guix
> (https://lists.gnu.org/archive/html/help-guix/2016-12/msg00058.html). Do
> You know if he succeeded or not? And if not where there any substantial
> blockers or just lack of time?

He referenced some work done to use Nix with Genode, since abandoned, but the 
Genode documentation provides more details about this:

"The design of Genode's package-management concept is largely influenced by 
Git as well as the Nix package manager. In particular the latter opened our 
eyes to discover the potential that lies beyond the package management 
employed in state-of-the art commodity systems. Even though we considered 
adapting Nix for Genode and actually conducted intensive experiments in this 
direction (thanks to Emery Hemingway who pushed forward this line of work), we 
settled on a custom solution that leverages Genode's holistic view on all 
levels of the operating system including the build system and tooling, source 
structure, ABI design, framework API, system configuration, inter-component 
interaction, and the components itself. Whereby Nix is designed for being used 
on top of Linux, Genode's whole-systems view led us to simplifications that 
eliminated the needs for Nix' powerful features like its custom description 
language."

http://genode.org/documentation/developer-resources/package_management

(This is actually quite typical of Genode's online documentation, which seems 
to have a "white paper" feel at times (and a "manifest" feel, just summarising 
details, at others), so digesting it all can be time-consuming work.)

Personally, I have spent some time looking at L4Re rather than Genode, mostly 
because I have been wanting to deploy Fiasco.OC and it would appear that these 
two things (L4Re and Fiasco.OC) are developed more closely together. Genode 
seems to bundle specific versions of Fiasco.OC, but I have been needing to get 
updates and make fixes in a more convenient relationship with Fiasco.OC's 
upstream.

There was a remark about the Hurd in the previous thread. The one difference I 
tend to perceive between the Hurd and systems like L4Re and Genode is that the 
latter things tend to be demonstrated almost like embedded solutions - you 
build a specific payload and that is your system - whereas the Hurd behaves 
like the open-ended system we are familiar with from our desktop computers.

That said, Genode is supposed to be usable as a desktop operating system, and 
will apparently introduce "a minimalistic generic live system that can be 
interactively shaped into a desktop scenario by the user without any reboot":

https://genode.org/documentation/release-notes/17.11

Another difference, this time between Genode and L4Re, is the way the 
components seem to be wired up. Genode appears to use some kind of XML syntax 
for this:

http://genode.org/documentation/developer-resources/init

Whereas L4Re employs Lua for the same job. I cannot comment on Genode, but the 
L4Re framework seems to be something of a work in progress.

A vague goal of mine is to try and bring Fiasco.OC or something similar within 
the realm of the Hurd again. There was once a project to port the Hurd to a L4 
microkernel, but that stalled in various ways and also didn't involve the more 
modern L4 variants that are around today and are supported by Genode.

Sorry if this was something of a digression from the topic!

Paul

Re: Guix and sel4

[radoslaw]

Hi,

It wasn't entirely what I was hoping for but thank You for answering. So 
to dig a little deeper how closely is guix connected to linux kernel? In 
other words what would have to be changed in order to work with a 
different kernel and therefore different syscalls? I don't mean the 
whole system but the minimal set. I would assume that a toolchain (make, 
binutils, gcc), obviously guile if there is anything specific to linux 
in it. Anything else?

Cheers,
Radek

W dniu 2018-01-15 00:26, Paul Boddie napisał(a):
> On Sunday 14. January 2018 22.16.39 radoslaw@chmielarz.xyz wrote:
>> 
>> In 2016 David Craven has sent an email about his attempt in using sel4
>> (genode with sel4 to be exact) with guix
>> (https://lists.gnu.org/archive/html/help-guix/2016-12/msg00058.html). 
>> Do
>> You know if he succeeded or not? And if not where there any 
>> substantial
>> blockers or just lack of time?
> 
> He referenced some work done to use Nix with Genode, since abandoned, 
> but the
> Genode documentation provides more details about this:
> 
> "The design of Genode's package-management concept is largely 
> influenced by
> Git as well as the Nix package manager. In particular the latter opened 
> our
> eyes to discover the potential that lies beyond the package management
> employed in state-of-the art commodity systems. Even though we 
> considered
> adapting Nix for Genode and actually conducted intensive experiments in 
> this
> direction (thanks to Emery Hemingway who pushed forward this line of 
> work), we
> settled on a custom solution that leverages Genode's holistic view on 
> all
> levels of the operating system including the build system and tooling, 
> source
> structure, ABI design, framework API, system configuration, 
> inter-component
> interaction, and the components itself. Whereby Nix is designed for 
> being used
> on top of Linux, Genode's whole-systems view led us to simplifications 
> that
> eliminated the needs for Nix' powerful features like its custom 
> description
> language."
> 
> http://genode.org/documentation/developer-resources/package_management
> 
> (This is actually quite typical of Genode's online documentation, which 
> seems
> to have a "white paper" feel at times (and a "manifest" feel, just 
> summarising
> details, at others), so digesting it all can be time-consuming work.)
> 
> Personally, I have spent some time looking at L4Re rather than Genode, 
> mostly
> because I have been wanting to deploy Fiasco.OC and it would appear 
> that these
> two things (L4Re and Fiasco.OC) are developed more closely together. 
> Genode
> seems to bundle specific versions of Fiasco.OC, but I have been needing 
> to get
> updates and make fixes in a more convenient relationship with 
> Fiasco.OC's
> upstream.
> 
> There was a remark about the Hurd in the previous thread. The one 
> difference I
> tend to perceive between the Hurd and systems like L4Re and Genode is 
> that the
> latter things tend to be demonstrated almost like embedded solutions - 
> you
> build a specific payload and that is your system - whereas the Hurd 
> behaves
> like the open-ended system we are familiar with from our desktop 
> computers.
> 
> That said, Genode is supposed to be usable as a desktop operating 
> system, and
> will apparently introduce "a minimalistic generic live system that can 
> be
> interactively shaped into a desktop scenario by the user without any 
> reboot":
> 
> https://genode.org/documentation/release-notes/17.11
> 
> Another difference, this time between Genode and L4Re, is the way the
> components seem to be wired up. Genode appears to use some kind of XML 
> syntax
> for this:
> 
> http://genode.org/documentation/developer-resources/init
> 
> Whereas L4Re employs Lua for the same job. I cannot comment on Genode, 
> but the
> L4Re framework seems to be something of a work in progress.
> 
> A vague goal of mine is to try and bring Fiasco.OC or something similar 
> within
> the realm of the Hurd again. There was once a project to port the Hurd 
> to a L4
> microkernel, but that stalled in various ways and also didn't involve 
> the more
> modern L4 variants that are around today and are supported by Genode.
> 
> Sorry if this was something of a digression from the topic!
> 
> Paul

Re: Guix and sel4

[Paul Boddie]

On Monday 15. January 2018 21.44.08 radoslaw@chmielarz.xyz wrote:
> 
> It wasn't entirely what I was hoping for but thank You for answering. So
> to dig a little deeper how closely is guix connected to linux kernel?

Some people are using Guix with the Hurd, so maybe they can explain the 
relationship between Guix and things other than the Linux kernel.

I would guess that Guix shouldn't really care too much about the underlying 
system below a certain level, but then again I haven't looked into the details 
of the project that was mentioned involving Nix and Genode and why the Genode 
developers subsequently decided to do their own thing.

The L4Re (as opposed to Genode) sources contains package modules that are 
reminiscent of things in the source trees of distributions like OpenWrt and 
OpenEmbedded (if I remember the latter correctly), but I don't think there is 
any notion of installing these packages while running the system. Instead, 
they appear to be bundled in the payload deployed to a system, at least within 
the scope of my own experiments.

But package installation would mostly involve making files available in the 
filesystem that can then be accessed and executed, so I can imagine that with 
filesystem and program launching capabilities, you could have a package 
manager for L4Re. Maybe one already exists.

All this said, I'm obviously still learning about L4Re and associated 
technologies, so I should probably investigate further before saying anything 
else. ;-)

Paul

Re: Guix and sel4

[Efraim Flashner]

[-- Attachment #1: Type: text/plain, Size: 1138 bytes --]

On Mon, Jan 15, 2018 at 09:44:08PM +0100, radoslaw@chmielarz.xyz wrote:
> Hi,
> 
> It wasn't entirely what I was hoping for but thank You for answering. So to
> dig a little deeper how closely is guix connected to linux kernel? In other
> words what would have to be changed in order to work with a different kernel
> and therefore different syscalls? I don't mean the whole system but the
> minimal set. I would assume that a toolchain (make, binutils, gcc),
> obviously guile if there is anything specific to linux in it. Anything else?
> 
> Cheers,
> Radek
> 

from 'git grep linux-{libre-}headers' it comes up a few times, but
really in make-boostrap, cross-base and commencement. For a start I
would focus on make-bootstrap (to make the boostrap binaries) and then
commencement (to build up again).

As far as different syscalls, I assume mist things should just work, but
I haven't looked into it.

-- 
Efraim Flashner   <efraim@flashner.co.il>   אפרים פלשנר
GPG key = A28B F40C 3E55 1372 662D  14F7 41AA E7DC CA3D 8351
Confidentiality cannot be guaranteed on emails sent or received unencrypted

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 833 bytes --]

Re: Guix and sel4

[Ludovic Courtès]

Hello,

Paul Boddie <paul@boddie.org.uk> skribis:

> There was a remark about the Hurd in the previous thread. The one difference I 
> tend to perceive between the Hurd and systems like L4Re and Genode is that the 
> latter things tend to be demonstrated almost like embedded solutions - you 
> build a specific payload and that is your system - whereas the Hurd behaves 
> like the open-ended system we are familiar with from our desktop computers.

I really like the work that has been put into Genode, it’s impressive.

That said, I think GuixSD on GNU/Hurd is slowly but surely materializing
thanks to Manolis and rennes, and like you write, GNU/Hurd is designed
to be like GNU/Linux from the looks but with tons of goodies inside.  :-)
So I’d encourage you to give Manolis and rennes a hand.

Ludo’.