Fwd: Re: I am interested in porting LionOS to X64 architecture

Resend because I forgot to CC the mailing list. Begin forwarded message: From: Jingyao Zhou <jingyao.zhou@unsw.edu.au> Date: 5 June 2025 at 11:47:49 GMT+8 To: Peter Relich <prelich@intellisenseinc.com> Subject: Re: [seL4] Re: I am interested in porting LionOS to X64 architecture Hi Peter, I am glad to see that you are interested in contributing to x86 support for LionsOS! Several x86-related works/plans are going on in the Trustworthy Systems Team. For the seL4 kernel, there are pending pull requests for remappable MSI and IOAPIC supports that need to be updated and tested; we would like to add posted interrupts and MSI-x, but there are no concrete plans yet. For the x86 Microkit, we adopted Neutrality-CH's works and have been updating it (e.g. adding virtulization support). There are two major issues: * We need to figure out a nicer way to generate the machine description for x86 machines * We also need to add IOMMU supports We hope to upstream the work soon. For seL4 Device Driver Framework: we have working examples running on Supermicro servers as well as QEMU. We hope to upstream them soon as well. For adding x86 support for libvmm: the work is on hold due to the prerequisites, plus a kernel issue with multi-IOAPIC support. We will resume it as soon as possible. We apologize for the lack of information; we will keep our progress on x86 supports updated on GitHub in the future. Regards, Jade. ________________________________ From: Peter Relich via Devel <devel@sel4.systems> Sent: Wednesday, June 4, 2025 3:49 AM To: devel@sel4.systems <devel@sel4.systems> Subject: [seL4] Re: I am interested in porting LionOS to X64 architecture Thanks everyone. I got authorized to continue my effort, and I was looking into what is currently available. I don't have to worry about red/black channels for now, so confidentiality is not yet a priority. 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. I saw that Neutrality-CH (Switzerland) had forked the Microkit library for x86 (https://github.com/Neutrality-ch/microkit), but they had only made two commits, the last one was in December 17. I tried to contact them a few weeks ago, but I didn't hear back so I'm not sure the status/funding of their project. Anyway, currently the VMM capabilities are not developed for their fork which would make deployment of an OS tedious. At first glance, it looks like I need to put some work into building a VMM into their fork by studying and then calling the seL4 vcpu, interrupt, x86_src routines into their Microkit fork? I guess my question now as I parse through everything. Is the Neutrality-CH fork the best, most recent x86 fork of the microkit? Or is there another library/fork I should consider for development? I saw that their approach for pre-generating an ELF file for the bootloader was the main obstacle for their pull request, but since I'm working on a specific Intel architecture (8th gen, uses Intel VT-x and VT-d for virtualization), I can avoid over generalizing my solution and focus on this specific application. Is there any value in extracting/porting the work performed in CAmkES x86 virtualization for the microkit x86 fork? Thanks again for all the help! -Peter ________________________________ The information contained in this e-mail and any attachments from Intellisense Systems may contain confidential and/or proprietary information, and is intended only for the named recipient to whom it was originally addressed. If you are not the intended recipient, any disclosure, distribution, or copying of this e-mail or its attachments is strictly prohibited. If you have received this e-mail in error, please notify the sender immediately by return e-mail and permanently delete the e-mail and any attachments. _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems Confidential communication - This email and any files transmitted with it are confidential and are intended solely for the addressee. If you are not the intended recipient, please be advised that you have received this email in error and that any use, dissemination, forwarding, printing, or copying of this email and any file attachments is strictly prohibited. If you have received this email in error, please notify me immediately by return email and destroy this email.
participants (1)
-
Jingyao Zhou