[squeak-dev] seL4 Microkernel: How small can the shim be?

Liam Proven lproven at gmail.com
Thu Feb 25 23:17:29 UTC 2021


On Wed, 24 Feb 2021 at 17:40, <ken.dickey at whidbey.com> wrote:
>
> Liam,
>
> The reason I keep coming back to this is the complexity of modern OS
> threats and requirements and the desire to spend less of my time here.
>
> The core drivers of the seL4 API are (from
> https://microkerneldude.wordpress.com/ ; good reads here BTW):
[...]
> I would think that all of this maps into (perhaps grad level) student
> projects as well, so [a] we can get a bit of "free labor" boost plus [b]
> more beginning and advanced students get exposed to Smalltalk and the
> ideas of the community.

:-D

Some excellent points there.

I was and am slightly aware of the seL4 µkernel, but I did not
seriously consider it.

I want to stress that I am not really an expert in this stuff, merely
an interested dilettante! But few people seem to be considering new OS
designs these days, so I thought that maybe this amateur could make
some interesting points.

So, my reasoning for suggesting Oberon and specifically A2:

• I really wanted a total and clean break from C and C-based designs;
something really different.

• I was hoping for a type-safe, memory-managed compiler suitable for
low-level and kernel work – and I found one in Oberon.

• A2 is a complete OS, with multicore support, TCP/IP stack, working
USB drivers, things like that, not just a kernel. It also provides a
compiler and rudimentary sort of IDE suitable for writing new drivers
in. L4 is just a microkernel and needs an OS building around it, as I
understand it.

• I do not know much about the whole L4 family but what little I know
some of the existing OSes based upon them were very vaguely Unix-ish.
That's precisely what I'm trying to move away from.

• I do not know if SEL4 has working multiprocessor support. I know
that QNX does, which demonstrates that a Unix-like true microkernel
can do this; but I also believe that Minix 3 so far lacks one, and
lacks some APIs needed for POSIX and xNix compatibility. This is not
an easy thing to do.

• This is wild supposition on my part, but I wonder if the traditional
C language's design and features, and the design philosophy of xNix,
its design of separate isolated execution environments which mainly
exchange data through the filesystem or IPC mechanisms, make things
like microkernels seem like a desirable design: to extend this
compartmentalisation right down into the kernel itself.

Plan 9's developers originally intended to replace C with Aleph, but
in the end abandoned that approach but applied much stricter standards
to Plan 9 C than ordinary xNix/Linux C. I have read 1 isolated comment
lacking more context that the design of Plan 9 makes considerations of
microkernels largely irrelevant, but I do not know how or why that
might be. I would very much like to know.


-- 
Liam Proven – Profile: https://about.me/liamproven
Email: lproven at cix.co.uk – gMail/gTalk/gHangouts: lproven at gmail.com
Twitter/Facebook/LinkedIn/Flickr: lproven – Skype: liamproven
UK: +44 7939-087884 – ČR (+ WhatsApp/Telegram/Signal): +420 702 829 053


More information about the Squeak-dev mailing list