- Notifications
You must be signed in to change notification settings - Fork740
arch/x86: Support Xen x86/HVM direct boot ABI#1443
arch/x86: Support Xen x86/HVM direct boot ABI#1443losfair wants to merge 1 commit intoseL4:masterfrom
Conversation
Adds support for booting the kernel with the Xen x86/HVM direct boot ABI(https://xenbits.xen.org/docs/unstable/misc/pvh.html). This allows seL4to boot natively within virtualized environments like QEMU.Signed-off-by: Heyang Zhou <hello@su3.io>
lsf37 commentedApr 2, 2025
I'm not convinced. This complicates the boot code, which is not verified, so it needs extra strong scrutiny, and supporting seL4 in virtualised environments is creating temptation for using it wrong (it breaks the verification assumptions and only makes sense for prototyping). I'm happy to be persuaded otherwise if there are good arguments for it, though. Is there an application scenario that was not supported before that would be supported or much easier now? |
| for (i = 0; i < boot_state.mem_p_regs.count; i++) { | ||
| paddr_t start = MAX(min_paddr, boot_state.mem_p_regs.list[i].start); | ||
| paddr_t start = MAX(boot_state.ki_p_reg.end, MAX(min_paddr, boot_state.mem_p_regs.list[i].start)); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others.Learn more.
why is this change needed and correct?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others.Learn more.
Probably a bugfix, but it should have much more explanation. It should be well defined what the end of the boot state is, now two addresses are checked, which is weird.
| word_t region_size = end - start; | ||
| if (region_size >= image_size) { | ||
| if (end > start &®ion_size >= image_size) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others.Learn more.
what has changed to necessitate a change here?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others.Learn more.
I think that checks for overflows and is just a bugfix. The first two changes should have their own commit(s) with explanations, they're not part of Xen/HVM support directly.
| load_paddr = mods_end_paddr; | ||
| load_paddr = load_boot_module(boot_state.boot_module_start, load_paddr); | ||
| load_paddr = load_boot_module(boot_state.boot_module_start, &mods_end_paddr); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others.Learn more.
mods_end_paddr is a local variable, you are not allowed to take its address in seL4. See alsohttps://docs.sel4.systems/processes/style-guide.html#verification-requirements
| static BOOT_CODE bool_t try_boot_sys_hvm( | ||
| hvm_start_info_t *info | ||
| ) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others.Learn more.
Please use the same style as other declarations.
| if (!add_mem_p_regs((p_region_t) { | ||
| ROUND_UP(entry->addr, PAGE_BITS), ROUND_DOWN(entry->addr + entry->size, PAGE_BITS), | ||
| })) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others.Learn more.
Please use semantic indentation.
Why are all these ROUND_UP, ROUND_DOWN safe?
| } | ||
| BOOT_CODE static paddr_t load_boot_module(word_t boot_module_start, paddr_tload_paddr) | ||
| BOOT_CODE static paddr_t load_boot_module(word_t boot_module_start, paddr_t*load_paddr_p) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others.Learn more.
If there are added side effects like changing the content ofload_paddr_p because things are moved, these should be documented in a comment.
lsf37 left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others.Learn more.
This needs more correctness arguments and currently does not satisfy the C subset requirements.
Uh oh!
There was an error while loading.Please reload this page.
Adds support for booting the kernel with the Xen x86/HVM direct boot ABI (https://xenbits.xen.org/docs/unstable/misc/pvh.html). This allows seL4 to boot natively within virtualized environments like QEMU: