search

seL4 / microkit

Microkit - A simple operating system framework for the seL4 microkernel
Other
70 stars 37 forks source link

Support for additional platforms #15

Closed podhrmic closed 9 months ago

podhrmic commented 1 year ago

Hi! What is required in order to support the SDK on other platforms (specifically on Raspberry Pi 4)? Looking at the code base, looks like the board specific code is only the https://github.com/BreakawayConsulting/sel4cp/blob/main/loader/src/loader.c and https://github.com/BreakawayConsulting/sel4cp/blob/main/build_sdk.py

Would all platform specific details be part of the .system file connecting irqs and defining memory regions (such as in the ethernet example)?

hlyytine commented 1 year ago

Hi @podhrmic, please check https://github.com/tiiuae/sel4cp/tree/rpi4b_support -- there's a bug in how you create untypeds from regions -- you are supposed to do bit size aligning based on virtual addresses, not physical ones. sel4cp needs this fix before it can be used with rpi4.

hlyytine commented 1 year ago

Also as a shameless plug, try our container to build sel4cp's Hello World to rpi4: https://github.com/tiiuae/tii_sel4_build/tree/wip/hlyytine-sel4cp#sel4cp

podhrmic commented 1 year ago

Thanks @hlyytine that is very cool! Looking at your commits, it seems that the platform support provided by the SDK is really just a loader and a kernel debug print, right?

hlyytine commented 1 year ago

From peripherals point of view, pretty much yes. There's also the monitor and sel4cp goes a long way internally abstracting away differences between different architectures and use cases (for example, seL4 running on EL1 or EL2 on ARM). But that does not mean you could not build complex systems with sel4cp. For example, check this out: https://github.com/Ivan-Velickovic/sel4cp_vmm

So we at TII are experimenting with QEMU (or other VMM-like software, such as crosvm) running in dedicated "driver-VM" providing virtio devices to other Linux guests (not using those as VMMs per se). But it shouldn't be a problem to have native seL4 applications using these virtio devices. UNSW is working with the driver framework called sDDF and eventually they would like to have native drivers (which you might be looking after). But our solution (use dedicated VM to run Linux and provide virtio devices to other guests) is an intermediate step. And whenever sDDF is mature enough, we think we could use it as a virtio transport instead of our custom solution. Which means as long as you can get Linux running on any given board, you can configure a sel4cp VMM to run Linux in driver-VM there and provide virtio services, to either other VMs or native seL4 apps. Then you could incrementally implement more proper native drivers and finally ditch the driver-VM Linux.

Our prototype is for CAmkES VMM and we are currently migrating it to seL4 Core Platform, hoping to get first light within a month or so.

Ivan-Velickovic commented 9 months ago

An official guide for porting Microkit will be made, the relevant tracking issue is here https://github.com/seL4/microkit/issues/48. It contains details already for doing a port until a proper guide is merged.