seL4 Microkernel: How small can the shim be?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
7 messages Options
Reply | Threaded
Open this post in threaded view
|

seL4 Microkernel: How small can the shim be?

KenDickey
Liam wrote:

> 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.
..

Right.  I am thinking of expanding outward from Genode (
https://genode.org/about/index ), start with a small (non-Unix) OS which
runs on (some of) x86/ARM64/RISC-V which can be used as a bootstrap for
Smalltalk->Native runtime, then replace services written in C to
services written in Smalltalk initially with the same API, but later
re-imagined.  An ultra-secure OS which has the right basics for
hotplug/live updates.  Add eMail & Web browsing after getting core St
GUI up.

This is pretty much a scratch effort.  Some C at first, particularly in
the microkernel (e.g. seL4) but this is minimal and kinda like changing
FPGA gates.

We are probably "agreeing loudly" on most of this, particularly given my
ignorance of Oberon.

Later,
-KenD

-KenD
Reply | Threaded
Open this post in threaded view
|

Re: seL4 Microkernel: How small can the shim be?

timrowledge
This might be of some interest - https://hackaday.com/2021/02/24/real-time-os-basics-picking-the-right-rtos-when-you-need-one/

Also - if you're interested in minimal OS with easy low-level access you could do worse than investigating RISC OS. Get a Pi, download the package from riscos direct )https://www.riscosdev.com/direct/) and play.

> On 2021-02-26, at 4:46 PM, [hidden email] wrote:
>
> Liam wrote:
>
>> 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.
> ..
>
> Right.  I am thinking of expanding outward from Genode ( https://genode.org/about/index ), start with a small (non-Unix) OS which runs on (some of) x86/ARM64/RISC-V which can be used as a bootstrap for Smalltalk->Native runtime, then replace services written in C to services written in Smalltalk initially with the same API, but later re-imagined.  An ultra-secure OS which has the right basics for hotplug/live updates.  Add eMail & Web browsing after getting core St GUI up.
>
> This is pretty much a scratch effort.  Some C at first, particularly in the microkernel (e.g. seL4) but this is minimal and kinda like changing FPGA gates.
>
> We are probably "agreeing loudly" on most of this, particularly given my ignorance of Oberon.
>
> Later,
> -KenD
>
>


tim
--
tim Rowledge; [hidden email]; http://www.rowledge.org/tim
Strange OpCodes: RCR: Rewind Card Reader



Reply | Threaded
Open this post in threaded view
|

Re: seL4 Microkernel: How small can the shim be?

Liam Proven
On Sat, 27 Feb 2021 at 20:42, tim Rowledge <[hidden email]> wrote:
>
> Also - if you're interested in minimal OS with easy low-level access you could do worse than investigating RISC OS. Get a Pi, download the package from riscos direct )https://www.riscosdev.com/direct/) and play.

I am well aware of RISC OS. I distributed some fractal generators for
RISC OS back in the 1980s. :-) I have a RPi 3B+ running RISC OS Direct
sitting right next to me.

In fact, I have already been trying to explain some of the limitations
of RISC OS to the people running the Cloverleaf kickstarter campaign.

I wrote some of it up in a blog post, here:
https://liam-on-linux.livejournal.com/73983.html

This generated a bit of discussion on HackerNews, but as usual, lots
of heat but little light.
https://news.ycombinator.com/item?id=24735766

I still play around with RISC OS today. The reasons that I do not
think it is a suitable candidate for new efforts are:
• It is not a clean simple design: it is an old, complex one;
• It is mostly ARM assembler and not even slightly portable; even
moving it to new ARM hardware is hard;
• It is technically very limited, with little memory protection, very
limited CLI-only pre-emptive multitasking, no support for threads or
SMP;
• It is 32-bit only and the only realistic way of doing a 64-bit
version will be using some kind of VM or emulation

Other interesting lightweight vintage OSes which are now FOSS:
• Atari ST TOS/Mint: https://aranym.github.io/afros.html
• A relatively early version of Sinclair QDOS, Minerva:
https://github.com/janbredenbeek/Minerva4Q68
• The final version of the Sinclair OS, rewritten for Atari hardware,
SMSQ/e: http://www.wlenerz.com/smsqe/
• A FOSS re-implementation of the original Amiga OS:
https://aros.sourceforge.io/

But all of these are compromised, limited designs, hard to port, hard
or impossible to modernise while retaining any compatibility.

Really, seriously, this talk was based on _over_ a decade of research
and study. My choices were not casual ones or lightly considered! :-)

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)

If anyone else has any candidates that meet all of these, I would very
much like to know. It took a lot of searching and I don't know
anything else that ticks all the boxes.

--
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

Reply | Threaded
Open this post in threaded view
|

Re: seL4 Microkernel: How small can the shim be?

David T. Lewis
Hi Lian,

I'm not sure if you are aware, but Tim is one of the original core
VM developers and is the author of the RISC OS VM for Squeak. Here
are a few links of interest:

  http://squeakvm.org/riscos/

  http://www.rowledge.org/tim/squeak/

  http://squeakvm.org/cgi-bin/viewvc.cgi/squeak/trunk/platforms/RiscOS/

  http://source.squeak.org/VMMaker


In addition to the official VM releases that Tim provided, the source
code is all still on line in a Subversion repository at squeakvm.org
(platform source code) and in the VMMaker repository at source.squeak.org
(for the VM code written in Smalltalk).

Dave


On Sun, Feb 28, 2021 at 02:11:43PM +0100, Liam Proven wrote:

> On Sat, 27 Feb 2021 at 20:42, tim Rowledge <[hidden email]> wrote:
> >
> > Also - if you're interested in minimal OS with easy low-level access you could do worse than investigating RISC OS. Get a Pi, download the package from riscos direct )https://www.riscosdev.com/direct/) and play.
>
> I am well aware of RISC OS. I distributed some fractal generators for
> RISC OS back in the 1980s. :-) I have a RPi 3B+ running RISC OS Direct
> sitting right next to me.
>
> In fact, I have already been trying to explain some of the limitations
> of RISC OS to the people running the Cloverleaf kickstarter campaign.
>
> I wrote some of it up in a blog post, here:
> https://liam-on-linux.livejournal.com/73983.html
>
> This generated a bit of discussion on HackerNews, but as usual, lots
> of heat but little light.
> https://news.ycombinator.com/item?id=24735766
>
> I still play around with RISC OS today. The reasons that I do not
> think it is a suitable candidate for new efforts are:
> ??? It is not a clean simple design: it is an old, complex one;
> ??? It is mostly ARM assembler and not even slightly portable; even
> moving it to new ARM hardware is hard;
> ??? It is technically very limited, with little memory protection, very
> limited CLI-only pre-emptive multitasking, no support for threads or
> SMP;
> ??? It is 32-bit only and the only realistic way of doing a 64-bit
> version will be using some kind of VM or emulation
>
> Other interesting lightweight vintage OSes which are now FOSS:
> ??? Atari ST TOS/Mint: https://aranym.github.io/afros.html
> ??? A relatively early version of Sinclair QDOS, Minerva:
> https://github.com/janbredenbeek/Minerva4Q68
> ??? The final version of the Sinclair OS, rewritten for Atari hardware,
> SMSQ/e: http://www.wlenerz.com/smsqe/
> ??? A FOSS re-implementation of the original Amiga OS:
> https://aros.sourceforge.io/
>
> But all of these are compromised, limited designs, hard to port, hard
> or impossible to modernise while retaining any compatibility.
>
> Really, seriously, this talk was based on _over_ a decade of research
> and study. My choices were not casual ones or lightly considered! :-)
>
> 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)
>
> If anyone else has any candidates that meet all of these, I would very
> much like to know. It took a lot of searching and I don't know
> anything else that ticks all the boxes.
>
> --
> 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
>

Reply | Threaded
Open this post in threaded view
|

Re: seL4 Microkernel: How small can the shim be?

timrowledge
In reply to this post by Liam Proven


> On 2021-02-28, at 5:11 AM, Liam Proven <[hidden email]> wrote:
>
> I am well aware of RISC OS. I distributed some fractal generators for
> RISC OS back in the 1980s. :-) I have a RPi 3B+ running RISC OS Direct
> sitting right next to me.

Good; not enough people know of it.
I was involved before it was even a Thing, and kept using as my main work system (even coercing assorted research labs in Silicon Valley to support me in this insanity) until about 2010.


> I wrote some of it up in a blog post, here:
> https://liam-on-linux.livejournal.com/73983.html

I'd dispute a few of your assertions there but, yeah, mostly. I don't think one could 'improve' RISC OS into a usefully modern OS but I do think one could create a modern OS with the 'spirit' of RISC OS. And nobody would use it. :-(


> I still play around with RISC OS today. The reasons that I do not
> think it is a suitable candidate for new efforts are:
[snip]
Pretty much the case. It *was* a simple design, but grew .... complicated, over the decades.

>
> Other interesting lightweight vintage OSes which are now FOSS:
Mention not these primitive abacus's.


> 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)

Well, as Ken says, that's pretty much an empty set.

I'd certainly not accept the 'not jitted' criterion since I am going to stand on my claim that it would make it much easier to write and maintain a flexible system.
I'd also point out that the OS per se has nothing at all to do with whether an in-use system is suited to general users or experts - that's the domain of the software running on top of/in the OS. With sufficient work and inspiration one could even make Windows tolerable at the user level.

If you can find a way to engage a few tens of millions of plausible currency units then there may be avenues to success. Some of us on this very list have seriously tried in the past but if you have any way to get it done... fabulous!

tim
--
tim Rowledge; [hidden email]; http://www.rowledge.org/tim
Strange OpCodes: STOP: No Op



Reply | Threaded
Open this post in threaded view
|

Re: seL4 Microkernel: How small can the shim be?

Liam Proven
In reply to this post by David T. Lewis
On Sun, 28 Feb 2021 at 15:31, David T. Lewis <[hidden email]> wrote:
>
> Hi Lian,
>
> I'm not sure if you are aware, but Tim is one of the original core
> VM developers and is the author of the RISC OS VM for Squeak. Here
> are a few links of interest:
[...]

Oh my word!

No, I was not. Actually I did not even realise that Squeak ran on RISC
OS at all. That's quite an achievement.

As I understand it, the current version of RISC OS Direct on the
Raspberry Pi 4 can access 4GB of RAM and is up there,
performance-wise, with the fastest RISC OS boxes ever made. It allows
significantly larger programs, too -- I am not sure of the maximum
WimpSlot but I think it's a gig or 2 now. I suspect Squeak would run
rather well on that.

--
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

Reply | Threaded
Open this post in threaded view
|

Re: seL4 Microkernel: How small can the shim be?

Liam Proven
In reply to this post by timrowledge
On Sun, 28 Feb 2021 at 19:32, tim Rowledge <[hidden email]> wrote:
>
> Good; not enough people know of it.

Agreed.

> I was involved before it was even a Thing, and kept using as my main work system (even coercing assorted research labs in Silicon Valley to support me in this insanity) until about 2010.

:-) Did you know or work with Paul Fellows?

We have a mutual friend and I managed to arrange for him to do a talk
at ROUGOL back in 2012. It was fascinating.

There's a transcript here:
http://www.rougol.jellybaby.net/meetings/2012/PaulFellows/

> I'd dispute a few of your assertions there but, yeah, mostly. I don't think one could 'improve' RISC OS into a usefully modern OS but I do think one could create a modern OS with the 'spirit' of RISC OS. And nobody would use it. :-(

Corrections welcomed, as they say.

A friend of mine was the late great UK IT journalist Guy Kewney, an
exceptional writer and commentator on this field. One of my favourite
bits of his -- I can only paraphrase it, sadly, I've never found it
online -- was a review of WordPerfect 5.

He said, roughly:
"WordPerfect 4.2 was pretty much the best word-processor on any
platform in the world. It had outcompeted all the competition on
everything else. It did everything you could ever want, and it did it
quickly and well with an elegant if odd user interface. Looking at
WordPerfect 5, therefore, I am driven to wonder how the management of
the company decided to create this. Did they look at each other and
say, 'So, we have a great bicycle here. Everyone agrees it's the best
bicycle  in the world. So what we're going to do it, we're going to
put 11 more wheels on it."

WP5 added pull-down CUA menus, bolted rather clumsily on top of 4.2's
function-key based controls. It was bigger, slower, buggier, took more
memory, and had an ugly 2nd UI as well as its original one.

It's funny, looking back now, that the _next_ release, WordPerfect 5.1
for DOS, is the one that almost everyone today looks back upon as
being the peak of the DOS line.

Me -- supporting it back then, but never being a big fan --  I have
WordPerfect 6 for DOS running on PC-DOS 7.1 on a Lenovo Thinkpad. It
was lambasted for being big and slow when it was new. Now, on
decade-old kit, it's blindingly fast, and seems elegant, tiny and
polished.

Funny how time changes our perceptions.

I think I agree with you. It might be possible, with a tonne of work,
to modernise RISC OS into something with pre-emptive multitasking,
multi-threading, multiple processor core support, wifi and bluetooth
and OpenGL and a 3D-composited desktop and all the other things people
expect in a modern OS.

But it wouldn't really be RISC OS any more. Its charm is that it's
tiny and fast and efficient. It's a great bicycle but if anyone tries
to turn it into a motorcycle, I fear it will be a poor one.

There _are_ some things in that blogpost that I got wrong -- I clarify
some in the comments.

RISC OS Developments are porting the OpenBSD TCP-IP stack to RO5. This
will give it IPv6 support and wifi as well with any luck. Bluetooth is
far less important, TBH. And a chap in the ROOL forum has a
proof-of-concept multi-core add-on working. Another chap has NetBSD
executing on one ARM core while RISC OS executes on another, which is
splendidly impressive if slightly insane.

Apparently there is a plan for ARM64 support, too. It's a bit like
Apple did with Classic MacOS on PowerPC: run a tiny kernel underneath
the OS that emulates the old platform on-the-fly. Apparently ARM32
emulation on ARM64 works well and is very fast indeed.

It may get these modernisations anyway. I will be very interested to
see how it goes. I am very tempted to get a RISC OS PineBook as it is.

> Pretty much the case. It *was* a simple design, but grew .... complicated, over the decades.

I agree.

> > Other interesting lightweight vintage OSes which are now FOSS:
> Mention not these primitive abacus's.

:-D Excellent. Very nearly a Douglas Adams quote!

I do have a QL, but I barely know how to operate the thing. SMSQ/E
does seem to have evolved into an interesting, capable OS in the end,
though...

> Well, as Ken says, that's pretty much an empty set.

I don't think it is. I submit that the Oberon OS ticks pretty much
every single box. Only the A2 variant is SMP-capable, but I have it
running in VMs and on the bare metal here and it's very impressive
indeed.

There used to be a StrongARM version. The code is already
cross-platform and runs or has run on x86, NatSemi 32000, ARM, and
RISC5. I suspect that getting it working again on modern ARM would not
be that hard.

> I'd certainly not accept the 'not jitted' criterion since I am going to stand on my claim that it would make it much easier to write and maintain a flexible system.

I have to defer to your superior knowledge on this.

I just want to remind folks that the reason I'm here is that I'd
really like to see Squeak running on A2... I think it could be a good
partnership.

> I'd also point out that the OS per se has nothing at all to do with whether an in-use system is suited to general users or experts - that's the domain of the software running on top of/in the OS. With sufficient work and inspiration one could even make Windows tolerable at the user level.

Very true.

> If you can find a way to engage a few tens of millions of plausible currency units then there may be avenues to success. Some of us on this very list have seriously tried in the past but if you have any way to get it done... fabulous!

Aye, there's the rub.

--
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