On 18 Apr 2024, at 08:02, Isaac Beckett isaactbeckett@gmail.com wrote:
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.
The sDDF is not inherently dependent on the Microkit. It uses Notifications and memory regions as abstracted by the Microkit, and is structured as Microkit event handlers.
It should be straightforward to provide wrappers of this functionality from other OSes. I actually planned on getting this done, but it was somehow dropped. We do want the sDDF to be usable by other seL4-based OSes.
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.
Similar features are provided by “self-virtualising” NICs (see comment in S5.1.2 of the sDDF Design doc). Yes, to make use of this you’d need a small driver to set up the virtual devices, and then each one would appear as a separate device with its own driver (incl mapping some of them as pass-through devices to Linux). And yes, you’d get timing channels as with any shared hardware resources.
Gernot