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
