Hi Isaac
I am not familiar with ppc64le/IBM Power and don't regular do work
inside the kernel itself so keep that in mind with my answer, but here
is how I would go about porting a new architecture.
Booting is probably one of the hardest and most architecture dependent
parts of seL4. You will notice that for ARM and RISC-V, seL4 requires
some bootloader before it starts to do things like initialise hardware
and enable virtual memory before jumping to the kernel code. Taking
something like U-Boot and booting seL4 directly is not something
possible on those architectures as far as I know.
Whether this matters for IBM Power, I am not sure. For example unlike
ARM and RISC-V, x86 does not require any special bootloader to boot an
seL4 image.
For the kernel, you would probably want to get the simplest
configuration going first for testing, so that would probably be
single-core, no MCS, no hypervisor or anything.
Once you think you've got booting setup the first thing I would do is
get some kind of serial output in the kernel as soon as it starts. For
this, it might not be as simple as just writing a serial driver and
using it as soon as you get into the kernel entry point as, depending on
the architecture, there will probably be some more hardware
initialisation do to first. For example, on AArch64 the
`activate_kernel_vspace` function needs to be called first before any of
the serial output will work in the kernel (more info in [1]).
Once you get enough boot code to print out in the kernel, you can start
following all the other architecture boot code (in
src/arch/<ARCH>/kernel/boot.c) to setup the initial task (aka first user
process). So I guess the next step will be getting the initial task
working. This will require virtual memory working (which is highly
architecture specific) as well as figuring out all the architecture
specific parts of kernel objects. From there, I guess you could check if
the initial task is working with `seL4_DebugPutChar`, getting to this
point will probably be the bulk of the work as it means that the system
call code needs to work.
After that, getting sel4test working would be a good goal.
Last year, there was a PR [2] to add the LoongArch architecture to seL4.
To my knowledge, LoongArch is fairly similar to RISC-V so not sure how
much help it will be but the important thing is that this architecture
port is quite recent and so what kernel code they had to change is a
good guide as it will not be too out of date compared to the last most
recent architecture port (which was RISC-V I believe and was done 5-10
years ago).
[1]: https://github.com/seL4/seL4/issues/540.
[2]: https://github.com/seL4/seL4/pull/970
I hope this helps get you started. Others more familiar with the kernel,
feel free to correct me on anything.
Ivan
On 5/3/24 01:07, Isaac Beckett wrote:
[isaactbeck...@gmail.com appears similar to someone who previously sent you
email, but may not be that person. Learn why this could be a risk at
https://aka.ms/LearnAboutSenderIdentification ]
Hello!
I’m writing to ask how someone would approach porting seL4 to a new CPU
architecture. For example, ppc64le/IBM Power, since those systems can be run
with limited or no black box firmware blobs, they could offer stronger security
under seL4 since you can audit or replace the platform firmware in many cases.
There’s even an OEM manufacturing Power9 systems with this in mind.
That said, I know supporting a new architecture is not trivial. New platform
code would have to be written and verified, and existing userspace code for Arm
and x86-64 may have to be adjusted.
How does one approach something like this? Is it feasible for someone less
familiar with seL4’s internals to get something quick and dirty running as a
proof of concept?
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems
