[SPITBALL] Jehanne as another kernel option / porting target

[SPITBALL] Jehanne as another kernel option / porting target

[raingloom]

http://jehanne.io/2021/01/06/gcc_on_jehanne.html

Should support more architectures than Hurd ;)

Anyways, just throwing this out there, as I - and I imagine every
other contributor - have some more pressing projects.

It probably wouldn't be able to run most packages and services without
some significant work but it could maybe still use Guix as a package
manager.

seL4 would be cool too.

Re: [SPITBALL] Jehanne as another kernel option / porting target

[pinoaffe]

raingloom writes:
> http://jehanne.io/2021/01/06/gcc_on_jehanne.html
>
> Should support more architectures than Hurd ;)
>
> Anyways, just throwing this out there, as I - and I imagine every
> other contributor - have some more pressing projects.
>
> It probably wouldn't be able to run most packages and services without
> some significant work but it could maybe still use Guix as a package
> manager.
I'm far from in the loop, but from a cursory glance I'd think that
porting to Jehanne is significantly more involved than porting to the
Hurd, considering that Hurd seems to provide more POSIX compatibility
than Jehenne.

> seL4 would be cool too.
Didn't someone do some work on making hurd run on SEL4?
Or am I misremembering

Re: [SPITBALL] Jehanne as another kernel option / porting target

[Joshua Branson]

pinoaffe <pinoaffe@airmail.cc> writes:

> raingloom writes:
>
>> seL4 would be cool too.
> Didn't someone do some work on making hurd run on SEL4?
> Or am I misremembering

You are correct.  :)

https://www.gnu.org/software/hurd/history/port_to_another_microkernel.html

By now (that is, after 2006), there were some new L4 variants available,
which added protected IPC paths and other features necessary for
object-capability systems; so it might be possible to implement the Hurd
on top of these. However, by that time the developers concluded that
microkernel design and system design are interconnected in very
intricate ways, and thus trying to use a third-party microkernel will
always result in trouble. So Neal Walfield created the experimental
Viengoos kernel instead -- based on the experience from the previous
experiments with L4 and Coyotos -- for his research on resource
management. Currently he works in another research area though, and thus
Viengoos is on hold.

So essentially most of the active hurd developers considered a port to a
different microkernel to be impractical.  :(

However, one of the main hurd developers (he has since stepped away from
active development), started a hurd clone:  x15.

https://www.sceen.net/x15/

He claimed that the original GNU Hurd has too many bad design
decisions.  So he started from scratch writing a kernel.  His kernel x15
is NOT a mach replacement.  However, some of the code he wrote for x15
has been incorporated in the GNU Hurd.  :)

--
Joshua Branson (joshuaBPMan in #guix)
Sent from Emacs and Gnus
  https://gnucode.me
  https://video.hardlimit.com/accounts/joshua_branson/video-channels
  https://propernaming.org
  "You can have whatever you want, as long as you help
enough other people get what they want." - Zig Ziglar

Re: [SPITBALL] Jehanne as another kernel option / porting target

[Vincent Legoll]

Hello,

On Fri, Mar 19, 2021 at 5:45 PM Joshua Branson <jbranso@dismail.de> wrote:
> >> seL4 would be cool too.
> > Didn't someone do some work on making hurd run on SEL4?
> > Or am I misremembering
>
> You are correct.  :)

It was a member of the L4 family, but I think it was not seL4 (looks like seL4
started in 2006).

I have created a guix build recipe for seL4 recently, it builds, but I don't
know what to do with it :-)

I'll send it as a followup to this thread, if any one is interested.

-- 
Vincent Legoll

Re: [SPITBALL] Jehanne as another kernel option / porting target

[Vincent Legoll]

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

On Fri, Mar 19, 2021 at 7:02 PM Vincent Legoll <vincent.legoll@gmail.com> wrote:
> I have created a guix build recipe for seL4 recently, it builds, but I don't
> know what to do with it :-)
>
> I'll send it as a followup to this thread, if any one is interested.

Here it is, ukernel only, hardcoded arch, nothing fancy like camkes, etc.

-- 
Vincent Legoll

[-- Attachment #2: 0001-gnu-Add-sel4.patch --]
[-- Type: text/x-patch, Size: 4243 bytes --]

From 607cef41839131fd740fbf754d30f3a9277c5a0a Mon Sep 17 00:00:00 2001
From: Vincent Legoll <vincent.legoll@gmail.com>
Date: Fri, 19 Feb 2021 23:49:43 +0100
Subject: [PATCH] gnu: Add sel4.

* gnu/packages/sel4.scm: New file...
* gnu/local.mk (GNU_SYSTEM_MODULES): ...Add it here.
---
 gnu/local.mk          |  1 +
 gnu/packages/sel4.scm | 83 +++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 84 insertions(+)
 create mode 100644 gnu/packages/sel4.scm

diff --git a/gnu/local.mk b/gnu/local.mk
index 33da7b979a..6d4ddb2bdd 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -502,6 +502,7 @@ GNU_SYSTEM_MODULES =				\
   %D%/packages/sdl.scm				\
   %D%/packages/search.scm			\
   %D%/packages/security-token.scm		\
+  %D%/packages/sel4.scm				\
   %D%/packages/selinux.scm			\
   %D%/packages/sequoia.scm			\
   %D%/packages/serialization.scm		\
diff --git a/gnu/packages/sel4.scm b/gnu/packages/sel4.scm
new file mode 100644
index 0000000000..6fc3f88ac2
--- /dev/null
+++ b/gnu/packages/sel4.scm
@@ -0,0 +1,83 @@
+;;; GNU Guix --- Functional package management for GNU
+;;; Copyright © 2021 Vincent Legoll <vincent.legoll@gmail.com>
+;;;
+;;; This file is part of GNU Guix.
+;;;
+;;; GNU Guix is free software; you can redistribute it and/or modify it
+;;; under the terms of the GNU General Public License as published by
+;;; the Free Software Foundation; either version 3 of the License, or (at
+;;; your option) any later version.
+;;;
+;;; GNU Guix is distributed in the hope that it will be useful, but
+;;; WITHOUT ANY WARRANTY; without even the implied warranty of
+;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+;;; GNU General Public License for more details.
+;;;
+;;; You should have received a copy of the GNU General Public License
+;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.
+
+(define-module (gnu packages sel4)
+  #:use-module (gnu packages)
+  #:use-module (gnu packages python)
+  #:use-module (gnu packages python-xyz)
+  #:use-module (gnu packages python-web)
+  #:use-module (gnu packages ninja)
+  #:use-module (gnu packages xml)
+  #:use-module (guix build-system cmake)
+  #:use-module ((guix licenses) #:prefix license:)
+  #:use-module (guix packages)
+  #:use-module (guix git-download))
+
+(define-public sel4
+  (package
+    (name "sel4")
+    (version "12.0.0")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url "https://github.com/seL4/seL4")
+             (commit version)))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32 "1zkx6x5jly8f75ph9jxd2jrp1kg5l001zkfqpmjf8ancsi1b43y7"))))
+    (build-system cmake-build-system)
+    (arguments
+     '(#:tests? #f ;; No need for tests when you have formal proof of correctness
+       #:configure-flags
+       (list
+        "-G" "Ninja"
+        "-DKernelArch=x86"
+        "-DCROSS_COMPILER_PREFIX="
+        "-DCMAKE_TOOLCHAIN_FILE=../source/gcc.cmake"
+        "-C" "../source/configs/X64_verified.cmake")
+       #:phases (modify-phases %standard-phases
+                  (replace 'build
+                    (lambda _
+                      (invoke "ninja" "kernel.elf")))
+                  (replace 'install
+                    (lambda _
+                      (mkdir-p %output)
+                      (copy-file "kernel.elf"
+                                 (string-append %output "/kernel.elf")))))))
+    (native-inputs
+     `(("libxml2" ,libxml2)
+       ("ninja" ,ninja)
+       ("python" ,python-3)
+       ("python-future" ,python-future)
+       ("python-jinja2" ,python-jinja2)
+       ("python-paste" ,python-paste)
+       ("python-ply" ,python-ply)
+       ("python-six" ,python-six)
+       ))
+    (synopsis "Operating System microkernel")
+    (description "Formally verified member of the L4 microkernel family.")
+    (home-page "https://sel4.systems")
+    (license (list license:asl2.0 ; And also a variant in LICENSES/SHL-0.51.txt
+                   license:bsd-2
+                   license:bsd-3
+                   license:cc-by-sa4.0
+                   license:gpl2
+                   license:gpl2+
+                   license:lppl1.3c
+                   license:x11))))
-- 
2.30.0

Re: [SPITBALL] Jehanne as another kernel option / porting target

[Vincent Legoll]

On Fri, Mar 19, 2021 at 8:42 PM Vincent Legoll <vincent.legoll@gmail.com> wrote:
>
> On Fri, Mar 19, 2021 at 7:02 PM Vincent Legoll <vincent.legoll@gmail.com> wrote:
> > I have created a guix build recipe for seL4 recently, it builds, but I don't
> > know what to do with it :-)
> >
> > I'll send it as a followup to this thread, if any one is interested.
>
> Here it is, ukernel only, hardcoded arch, nothing fancy like camkes, etc.

vince@guix ~/dev/repo/guix [env]$ file
/gnu/store/8j7zdpnagz2i90cbmrqnk1vbsdck4d21-sel4-12.0.0/kernel.elf
/gnu/store/8j7zdpnagz2i90cbmrqnk1vbsdck4d21-sel4-12.0.0/kernel.elf:
ELF 64-bit LSB executable, x86-64, version 1 (SYSV), statically
linked, not stripped

vince@guix ~/dev/repo/guix [env]$ l
/gnu/store/8j7zdpnagz2i90cbmrqnk1vbsdck4d21-sel4-12.0.0/kernel.elf
-r-xr-xr-x 2 root root 179K Jan  1  1970
/gnu/store/8j7zdpnagz2i90cbmrqnk1vbsdck4d21-sel4-12.0.0/kernel.elf

vince@guix ~/dev/repo/guix [env]$ ./pre-inst-env guix build --check
--rounds=5 sel4
[...]
successfully built /gnu/store/laxxpkng3rs3kq1b5gbyzqsvlw97hdwk-sel4-12.0.0.drv
The following builds are still in progress:
  /gnu/store/laxxpkng3rs3kq1b5gbyzqsvlw97hdwk-sel4-12.0.0.drv
  /gnu/store/laxxpkng3rs3kq1b5gbyzqsvlw97hdwk-sel4-12.0.0.drv
  /gnu/store/laxxpkng3rs3kq1b5gbyzqsvlw97hdwk-sel4-12.0.0.drv
  /gnu/store/laxxpkng3rs3kq1b5gbyzqsvlw97hdwk-sel4-12.0.0.drv

successfully built /gnu/store/laxxpkng3rs3kq1b5gbyzqsvlw97hdwk-sel4-12.0.0.drv
The following builds are still in progress:
  /gnu/store/laxxpkng3rs3kq1b5gbyzqsvlw97hdwk-sel4-12.0.0.drv
  /gnu/store/laxxpkng3rs3kq1b5gbyzqsvlw97hdwk-sel4-12.0.0.drv
  /gnu/store/laxxpkng3rs3kq1b5gbyzqsvlw97hdwk-sel4-12.0.0.drv

Looks even reproducible...

-- 
Vincent Legoll

Re: [SPITBALL] Jehanne as another kernel option / porting target

[raingloom]

On Fri, 19 Mar 2021 20:42:19 +0100
Vincent Legoll <vincent.legoll@gmail.com> wrote:

> +     '(#:tests? #f ;; No need for tests when you have formal proof
> of correctness
In just about any talk about Idris and Type Driven Development, Edwin
Brady always starts with "you still need tests".

Re: [SPITBALL] Jehanne as another kernel option / porting target

[Vincent Legoll]

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

On Sunday, March 21, 2021, raingloom <raingloom@riseup.net> wrote:

> On Fri, 19 Mar 2021 20:42:19 +0100
> Vincent Legoll <vincent.legoll@gmail.com> wrote:
>
> > +     '(#:tests? #f ;; No need for tests when you have formal proof
> > of correctness
> In just about any talk about Idris and Type Driven Development, Edwin
> Brady always starts with "you still need tests".
>

That package is not intended to be included, as it is far from finished,
sorry, I should have added " pun intended" with the accompanying smiley
😀...


-- 
Vincent Legoll

[-- Attachment #2: Type: text/html, Size: 867 bytes --]

Re: [SPITBALL] Jehanne as another kernel option / porting target

[François]

Hello,

On Fri, Mar 19, 2021 at 12:44:47PM -0400, Joshua Branson wrote:
> pinoaffe <pinoaffe@airmail.cc> writes:
> > raingloom writes:
> >
> >> seL4 would be cool too.


> So essentially most of the active hurd developers considered a port to a
> different microkernel to be impractical.  :(
> 
> However, one of the main hurd developers (he has since stepped away from
> active development), started a hurd clone:  x15.

On the microkernel front there is also [Genode] which seems to have
nice ideas. I don't know if it would suit Guix or not.

[Genode]: https://genode.org/