[seL4] Re: Question about LionsOS

Sorry, I should clarify. I meant making a dynamic OS that uses the sDDF. Not on Microkit, since it’s not meant for that. But something that is more flexible at runtime, designed for general purpose use so that it can load components when they’re needed instead of having a fixed set of components running at all times. So like, detecting a device being attached, and loading drivers for it from the disk. Or loading an emulation layer/OS personality for another operating system, like for Linux or Windows programs. While I was thinking of that I also got another idea. Some graphics cards support technology similar to hardware virtualization extensions on CPUs, such that they can be configured (with appropriate drivers, of course) to behave as multiple logical devices on one physical device. The term for this I believe is SR-IOV. Support for this is patchy, from what I hear, since this feature was originally marketed for enterprise customers and not made available to individuals, so setting it up involved (or used to involve) hacks to trick the driver and/or firmware into allowing those features to be used. So I was thinking, it may make sense to write a smaller, simpler native driver for seL4 that does very little but configure logical/virtual devices, and then those can be given to either native drivers written from scratch, or to ported Linux code, or to Linux VMs. Of course this doesn’t consider the possibility (probably very likely) of hardware side channels in the GPU, but then again neither does seL4.

On Apr 17, 2024, at 5:43 PM, Peter Chubb wrote:

It's quite hard to make a fully dynamic OS on top of Microkit