Hi Ivan, Ah, I see, thanks for letting me know. Let's try pasting then. The notes are Markdown formatted, so if this gets somehow mangled, pasting it somwhere else and rendering it as Markdown might help (especially for the table at the end). Daniel # seL4 Summit 2025: BoF Multikernel 2025-09-05 ## Agenda - Who are the main stakeholders in the multikernel? - What are their requirements? - How do we converge on an implementation? ## Stakeholders The main stakeholders (currently) are - Neutrality, represented by - Mathieu Mirmont - David Cock - Daniel Schwyn - DARPA INSPECTA, represented by - Darren Cofer, Collins Aerospace - Nathan Studer, DornerWorks - John Hatcliff, Kansas State University - Kry10, represented by - Mattthew Brecknell ### Stakeholder requirements #### Neutrality - Hypervisor running on x86_64 - Resources on x86_64 are runtime-discovered over ACPI - Arm and RISCV are moving in the same direction in the server space - Neutrality's hypervisor will run on 100s of cores - The hypervisor gets loaded via UEFI - Dynamic discovery happens before seL4 boot - The private resources (mainly memory) are partitioned before kernel boot - Once seL4 kernels boot, the system is static - VM memory is globaly shared and allocated in userspace - Cross-core communication only in userspace - Polling on shared memory channels is enough - IPIs would be a performance optimization - Single VM per core - Multiple cores per VM - Dynamic IOMMU page table updates necessary #### INSPECTA - Armv8 and some x86 - Smaller platforms than Neutrality - Resources partitioned statically from model-based build system (AADL etc.) - Uses microkit #### Kry10 - Embedded system similar to INSPECTA - Dynamic system but static resource partitioning works - Also hypervisor similar to neutrality but Armv8 ## Discussion ### IRQs - Gerwin Klein, Proofcraft: - IPIs supported on arm, not yet on x86 - arm has a global part to the IRQ configuration - David Cock, Neutrality - x86 IRQ controllers are sane, can be partitioned between cores - Indan Zupancic, seL4 Foundation: Do we need more cross-core communication than IPIs? - Gernot Heiser, UNSW: No - David Cock, Neutrality: Barrelfish has shown them to be sufficient - Martin Decky, Kernkonzept: Some x86 chips implement user interrupts now, could be used as an optimization. ### Global ASIDs - Gerwin Klein, Proofcraft: ASIDs have to be consistent across cores for same address spaces on armv8 - David Cock, Neutrality: Not on x86, requirement on armv8 is for shared TLBs that never got implemented - Conclusion: Global ASIDs are necessary on armv8 when VMs/tasks run on multiple cores ### Verification - David Swasey, Riverside Research: For statically partitioned multikernel, correctness hinges on the pre-boot part that partitions. What about the verification story? - David Cock, Neutrality: We have a verification story for it, cannot say more for now. ## Summary - Kry10 needs to check but there should not be conflicting requirements as of now - We should form a special interest / work group - Neutrality volunteers to organize - We are ready to write an RFC - Boot process needs to be further discussed ### Requirements | Stakholder \ Requirement | Architectures | Dynamic discovery | IPIs | Dynamic IOMMU | Cross-core VMs / tasks | Global ASID assignment | | ------------------------ | ------------- | ----------------- | ---- | ------------- | ---------------------- | ---------------------- | | Neutrality | x86_64 | yes | opt. | yes | yes | no | | INSPECTA | Armv8, x86_64 | no | yes | no | no | no | | Kry10 | Armv8 | no | ? | ? | yes | yes | On Tuesday, October 7th, 2025 at 02:22, Ivan Velickovic via Devel <devel@sel4.systems> wrote:

Hi Daniel

I don’t think email attachments show up on the mailing list, maybe you could just paste the notes directly instead?

Ivan

...

On 6 Oct 2025, at 20:01, Daniel Schwyn via Devel devel@sel4.systems wrote:

Dear all,

Attached you will find the notes from the Birds of a feather session on the multikernel at the summit in Prague. Please let me know if something is missing or misrepresented.

Best regards, Daniel _______________________________________________ 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