Hello Peter, On 2025-06-03 18:49, Peter Relich via Devel wrote:
My main priority is to create a steel thread so that if the main operating system crashes, a giant robotic vehicle can be teleoperated or shutdown without hurting anyone.
Wouldn't you want such watchdog kind of functionality (also) on the robotic vehicle itself? E.g. in case a cable or antenna breaks. If you have that, it is questionable whether running just Linux in a VM on top of seL4 adds anything. It will complicate things and increase the chance of software misbehaving on the Linux side, as running it as a VM is not fully transparent.
I saw that their approach for pre-generating an ELF file for the bootloader was the main obstacle for their pull request
They were trying to shoe-horn the Arm/RISC-V way of doing things onto x86, where it doesn't make sense. Instead, they should move what the loader does to the startup/monitor task, like Ivan said in one of the comments: "One potential solution to look into is appending the PD data to the monitor and having its initialisation process slightly differ so that it reads from that memory instead of device memory. This would mean we do not have to make patches to the kernel as well." So my advise would be to work on that instead of adapting the existing x86 patches for seL4 itself. You should be able to re-use some of their Microkit commits though. But then again, if you want something ready to use and don't have much requirements about the seL4 part of things, why not use camkes? I would also port the Linux code to seL4 instead of VMing it all, as that setup doesn't make much sense to me. All in all, if you have control over the robot software, running seL4 there seems to make more sense than running it on the Linux based control side. Greetings, Indan