On Thu, Oct 23, 2025 at 4:07 AM Ivan Velickovic <[email protected]> wrote: > > In order for seL4 to act has a hypervisor and therefore be able to have > virtual > machines on Microkit it needs to be in EL2. > > The work the Microkit tool has to do changes a bit for hyp vs non-hyp mode, I > mainly put that error there so people changing the source wouldn’t expect > non-hyp to work. > > If there is some use-case where the limitation of requiring seL4 to run at > EL2 instead > of EL1 is blocking I would be happy to help remove that limitation. Right now > I am not > aware of any such case.
That makes sense for real hardware. I want to be able to run on bare hardware and also in QEMU with KVM or Hypervisor.framework, in which case I only have EL1 and EL0 available. So when I add "-accel kvm" or "-accel hvf" on Linux or Mac, startup fails. > Microkit isn't well-suited for my purposes, except as a reference for > how to create a system build, > > Just out of curiosity is that because you’re trying to build a more dynamic > system > than Microkit can handle right now or some other reason? If is something more > specific I’d be happy to try help fix it. That's a good question. My system config is going to be fairly static but I'd like to be able to detect at startup how many CPUs and how much RAM is available. I don't like the idea of needing separate configs for Raspberry Pi 4 with different amounts of RAM. The same for QEMU configs where CPU count and RAM can change. The other area where Microkit isn't going to be very helpful is that I need to be able to route many hundreds of system calls via both seL4 messages and a legacy 32-bit pass-by-register SWI mechanism that doesn't use any calling standard (the input and output registers for each call were chosen somewhat arbitrarily decades ago), to modules that may be bundled in the image or loaded from a filesystem after boot. So I ultimately need dynamic load/config/unload of both 32-bit RISC OS relocatable modules and new 64-bit seL4-aware modules. It would be great if I could use Microkit, because I would like to leverage the sDDF device drivers, especially for virtio, but I think it's redundant with code I'm going to have to write myself in a more dynamic and backwards-compatible way, with less memory protection than a new design would have, due to modules and programs passing pointers back and forth in a partially-shared, partially-protected 32-bit address space. > I know the Raspberry Pi 5 that I want to support can run 32-bit > ARM code at EL0 only, which is all I need. > > > I have added Raspberry Pi 5B support here [1] but only for 64-bt. > > [1]: https://github.com/seL4/seL4/pull/1515. It doesn't make sense to add 32-bit Raspberry Pi 5B support because the CPU can't run 32-bit code at EL1 or higher. It's been a real source of concern for the RISC OS community. My interest in this porting project is from a desire to keep an OS alive that is otherwise going to become unusable except in emulation. https://www.riscosopen.org/wiki/documentation/show/Addressing%20the%20end-of-life%20of%20AArch32 Regards, Jake _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
