[RE] seL4 Microkernel: How small can the shim be?

Liam wrote:

> I was not merely looking for a lightweight OS. I had a demanding list
of criteria.

> I looked for:
• a clean, simple OS, with SMP support, that supported pre-emption,
memory management etc.
• in a type-safe language, with a native-object-code compiler — not
JITTed, not using a VM or runtime
• and a readable language, not something far outside the Algol family
of imperative HLLs
• that was portable across different architectures
• that was FOSS and could be forked
• that was documented and had a user community who knew it
• that can be built with FOSS tools (which RISC OS fails, for instance)
• which is or was used by non-specialists for general purpose computing
• which can usefully access the Internet
• which runs on commodity hardware
• which does not have a strongly filesystem-centric design that would
not fit a PMEM-only computer (i.e. not an xNix)


I think you have specified a null set.

Alan Kay said: "The best way to predict the future is to invent it."

You have described the world you want to move into.

My only suggestion here is to look at OSs which are easily ported.  I
would look at RISC-V because the kind of solution you are looking for
will probably appear there first.

Within "type-strict", you might consider a Rust or Haskell oSs.  [I
think Smalltalk is "type-safe", every object knows its class and trying
to access element 41 of a 10 element array gives DNU, but I suspect this
is not your definition].

For small, FreeRTOS and PharOS
(https://sourceforge.net/projects/rtospharos/) look interesting.

 From Wikipedia entry on RISC-V:

"Available RISC-V software tools include a GNU Compiler Collection (GCC)
toolchain (with GDB, the debugger), an LLVM toolchain, the OVPsim
simulator (and library of RISC-V Fast Processor Models), the Spike
simulator, and a simulator in QEMU (RV32GC/RV64GC).

Operating system support exists for the Linux kernel, FreeBSD, and
NetBSD, but the supervisor-mode instructions were unstandardized prior
to June 2019,[14] so this support is provisional. The preliminary
FreeBSD port to the RISC-V architecture was upstreamed in February 2016,
and shipped in FreeBSD 11.0.[96][74] Ports of Debian[97] and Fedora[98]
are stabilizing (both only support 64-bit RISC-V, with no plans to
support 32-bit version). A port of Das U-Boot exists.[99] UEFI Spec v2.7
has defined the RISC-V binding and a TianoCore port has been done by HPE
engineers[100] and is expected to be upstreamed. There is a preliminary
port of the seL4 microkernel.[101][102] Hex Five released the first
Secure IoT Stack for RISC-V with FreeRTOS support.[103] Also xv6, a
modern reimplementation of Sixth Edition Unix in ANSI C used for
pedagogical purposes in MIT, was ported. Pharos RTOS has been ported to
64-bit RISC-V[104] (including time and memory protection). Also see
Comparison of real-time operating systems.
"

Note also OSDev.org.

Good on ya,
-KenD

On Sun, 28 Feb 2021 at 17:16, <[hidden email]> wrote:
>
> I think you have specified a null set.

I know. It sounds unlikely. However, Oberon is real, it has users,
there are native versions for x86 and RISC5 (note, *not* RISC-V) and
hosted versions on Windows, macOS and both x86 & ARM Linux (and
formerly for DOS).

>
> Alan Kay said: "The best way to predict the future is to invent it."
>
> You have described the world you want to move into.

I tried to, certainly.

> My only suggestion here is to look at OSs which are easily ported.  I
> would look at RISC-V because the kind of solution you are looking for
> will probably appear there first.

TBH I am not convinced it's mature enough just yet. I could be wrong.

> Within "type-strict", you might consider a Rust or Haskell oSs.

I am aware of some but they do seem _very_ niche.

> [I
> think Smalltalk is "type-safe", every object knows its class and trying
> to access element 41 of a 10 element array gives DNU, but I suspect this
> is not your definition].

Close enough for government work. :-)

> For small, FreeRTOS and PharOS
> (https://sourceforge.net/projects/rtospharos/) look interesting.

They do indeed. I will do some more reading.

>  From Wikipedia entry on RISC-V:
[...]
> Note also OSDev.org.

Indeed.

There is an experimental RISC-V implementation:
https://github.com/solbjorg/oberon-riscv

Of course, this is doomed to lead to horrible confusion, since
Oberon's "native" platform is Professor Wirth's own RISC5 CPU, now
implemented on several FPGA devices.

https://people.inf.ethz.ch/wirth/ProjectOberon/RISC5.Update.pdf

I have heard a rumour it was done partly because Prof W was irked that
the main extant native versions were on x86.

RISC-V (pronounced "risk five" as opposed to RISC5 (pronounced "risk
five", I think, or I suppose "risk funf")? What could possibly go
wrong?

--
Liam Proven – Profile: https://about.me/liamproven
Email: [hidden email] – gMail/gTalk/gHangouts: [hidden email]
Twitter/Facebook/LinkedIn/Flickr: lproven – Skype: liamproven
UK: +44 7939-087884 – ČR (+ WhatsApp/Telegram/Signal): +420 702 829 053