"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
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 <devel@sel4.systems> Sent: Thursday, 23 October 2025 11:09 To: devel@sel4.systems 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 -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems 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.
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. Jake On Wed, Oct 22, 2025 at 8:06 PM Julia Vassiliki <julia.vassiliki@unsw.edu.au> 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 <devel@sel4.systems> Sent: Thursday, 23 October 2025 11:09 To: devel@sel4.systems 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 -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
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.
On Thu, 23 Oct 2025 at 10:50, Jake Hamby via Devel <devel@sel4.systems> 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/f34026941141cf246b4458b11bd6f2d9abe8...
Jake
On Wed, Oct 22, 2025 at 8:06 PM Julia Vassiliki <julia.vassiliki@unsw.edu.au> 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 <devel@sel4.systems> Sent: Thursday, 23 October 2025 11:09 To: devel@sel4.systems 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 -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
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 -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
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). 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. 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. 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. For the tutorial my goal was to get people up and running as quickly as possible which means installing the toolchain from a package manager, the aarch64-none-elf toolchain is not in any popular package managers (apt. homebrew etc) other than Nix as far as I am aware. Even with a good internet connection it takes a really long time to download for some reason. Maybe Clang for the tutorial would be better suited than an ARM Linux toolchain, and then making Microkit build with LLVM by default (right now it’s an option when building from source). 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. Ivan 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.
On Thu, Oct 23, 2025 at 4:07 AM Ivan Velickovic <i.velickovic@unsw.edu.au> 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.
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... Regards, Jake
participants (4)
-
Hesham Almatary -
Ivan Velickovic -
Jake Hamby -
Julia Vassiliki