On Thu, 23 Oct 2025 at 10:50, Jake Hamby via Devel <[email protected]> wrote: > > Thanks for the quick, informative reply. I noticed that Microkit also > explicitly requires EL2 support and has comments to that effect in its > build tool (and gives an error if you try to turn it off in the build > config). > > Microkit isn't well-suited for my purposes, except as a reference for > how to create a system build, and the recommendation when building the > Microkit SDK itself to download the ARM GCC cross-compiler tools for > aarch64-none-elf, which seems like a slightly more appropriate build > target than the aarch64-unknown-linux-gnu tools from someone's > Homebrew repo that the Microkit tutorial recommended. > np: if you're on Macs M1+ (eg AArch64) and have a recent Microkit revision after this commit that adds LLVM support [1], you can just use the host's LLVM/Clang by passing the "--llvm" flag when building the SDK, and not rely on GCC at all for that.
[1] https://github.com/seL4/microkit/commit/f34026941141cf246b4458b11bd6f2d9abe8bb6e > Jake > > On Wed, Oct 22, 2025 at 8:06 PM Julia Vassiliki > <[email protected]> wrote: > > > > > > Hi Jake > > > > Regarding SMP on QEMU, yes, it is currently the case that the elfloader > > (not part of seL4 itself) does not support SMP *without* HYP. See for > > reference > > https://github.com/seL4/seL4/pull/1275. > > > > Note that you can still use a non-hyp build of seL4 in QEMU with hypervisor > > mode > > turned on. I'm not sure if you can do this with elfloader, but the microkit > > loader > > works this way, and can drop privilege level from EL2 to EL1 when booting > > the kernel. > > > > tldr; yes currently HVC doesn't work, and we need to add support to the > > elfloader for it. > > > > > The one area of seL4 that I know I will need to modify will be to add > > a 32-bit ARM mode for running existing RISC OS software and modules. > > The only special criteria it needs to have is to route all SWI (SVC) > > calls to a fault handler so I can pass them to either a 32-bit handler > > or to the new 64-bit SWI handlers that I'll hopefully be able to start > > porting one at a time from the original A32 code. > > > > For running A32 code atop of an Aarch64 kernel, I'm not certain what's > > required there, > > but any exceptions such as SVC that are not allowed in EL0 should be sent > > as a fault > > to the registered fault handler for such a thread (likely as an > > UserException), so should be fine. > > > > Julia > > > > (P.S. Sorry for the double email, Jake, I forgot to reply All). > > > > ________________________________________ > > From: Jake Hamby via Devel <[email protected]> > > Sent: Thursday, 23 October 2025 11:09 > > To: [email protected] > > Subject: [seL4] "HVC is not supported for PSCI!" error for SMP on QEMU > > > > I've just started looking at seL4 for a hobby project to port RISC OS > > to run on 64-bit ARM. Since the OS is written primarily in 32-bit ARM > > assembly language, that means rewriting a lot of code in C, which is > > fine since I won't be having to write the supervisor-mode code that > > seL4 handles (the most difficult part to get right). > > > > I'm still working through the seL4 tutorials, and I'm sure I'll have > > more questions later, but here's an easy one that maybe someone can > > provide context for. When I tried running a tutorial in QEMU with SMP > > enabled, it failed with "HVC is not supported for PSCI!" Some > > investigation revealed that ARM has two different opcodes to make the > > same calls to the PSCI interface to turn on the other CPU cores. The > > only difference is HVC goes to EL2 and SMC goes to EL3. As part of the > > build, QEMU dumps a device tree that specifically defines "hvc" as the > > method to use. I also noticed the Raspberry Pi device trees have no > > "psci' nodes. > > > > I can patch seL4 to only work with HVC by patching the check and the > > assembly file to use "hvc" instead of "smc" but it'd be nice if there > > were a build config option to specify one or the other method for > > making PSCI calls, and then fail at runtime if the other method was > > found, especially since QEMU is so popular for testing that I assume > > people run into this often. It'd be a small #ifdef to require and use > > one or the other opcode. > > > > The one area of seL4 that I know I will need to modify will be to add > > a 32-bit ARM mode for running existing RISC OS software and modules. > > The only special criteria it needs to have is to route all SWI (SVC) > > calls to a fault handler so I can pass them to either a 32-bit handler > > or to the new 64-bit SWI handlers that I'll hopefully be able to start > > porting one at a time from the original A32 code. The 32-bit SWI > > handler can get/set the input/output parameters from the machine > > registers in the TCB, so that part's straightforward. I'll need to do > > some fakery for 32-bit code that wants to run in supervisor mode, to > > fake success when it calls privileged instructions. > > > > I'll know more as I continue designing and start implementing code. > > Unfortunately there'll eventually need to be an A32/T32 emulation mode > > of some sort for 64-bit only ARM CPUs like Apple's M-series, but that > > can come later, and I can use QEMU's CPU emulation until then (as > > opposed to hypervisor mode with "-accel hvf", which is 64-bit only). > > Also, 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. > > > > If anyone has suggestions or can see some fatal flaws in my > > assumptions, please let me know. > > > > Best regards, > > Jake Hamby > > _______________________________________________ > > Devel mailing list -- [email protected] > > To unsubscribe send an email to [email protected] > > > > This email and any files transmitted with it may contain confidential > > information. If you believe you have received this email or any of its > > contents in error, please notify me immediately by return email and destroy > > this email. Do not use, disseminate, forward, print or copy any contents of > > an email received in error. > > > _______________________________________________ > Devel mailing list -- [email protected] > To unsubscribe send an email to [email protected] _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
