x86 1-GByte pages?

[joep]

The cloud VM machines we've tried aren't providing PDPE1GB (aka X86_FEATURE_GBPAGES in linux) to guests for whatever reason (at least the 3 we tried don't). SeL4 detects it very early on in the boot sequence and halts with a message. We tried setting 'KernelHugePage: False' for our microkit build but it results in failure because the rust code seems to reference it unconditionally. I'm hardly a x86 hardware expert but using the feature is just a performance optimization I believe? Should it be set for a 'generic' build?

[Ivan-Velickovic]

We've fixed it such that having KernelHugePage: False should now work, but we should consider whether we should have that set by default or not. While we don't support huge pages right now, it is something we do want to do eventually so I'm not sure we want to disable huge pages in seL4 by default.

I'm not sure how complicated it would be to get seL4 to dynamically support huge pages so it we didn't have to decide at build-time. I imagine it's not trivial.

[Indanz]

We've fixed it such that having KernelHugePage: False should now work, but we should consider whether we should have that set by default or not. While we don't support huge pages right now, it is something we do want to do eventually so I'm not sure we want to disable huge pages in seL4 by default.

I don't think it's in the verification subset and it's currently default off in seL4 too, so having it default off in Microkit too would make sense.

I'm not sure how complicated it would be to get seL4 to dynamically support huge pages so it we didn't have to decide at build-time. I imagine it's not trivial.

It seems easy: We just have to change the config_set(CONFIG_HUGE_PAGE) checks to an inline function call that returns whether the CPU supports it or not, in addition to CONFIG_HUGE_PAGE being set.

For the kernel window mapping we could either dynamically choose between 1GB pages or 2MB pages, or just stick to 2MB pages if that's easier.

However, this isn't very user friendly as the user would only get an error when trying to map a huge page. Failing to create huge page objects isn't something user space can normally deal with either. But user space can use cpuid to check for huge pages support via the pdpe1gb flag before doing anything though.

Mind that Arm has the same issue, though no support for 1GB pages is less rare there, but there is no user space accessible cpuid to check for it at runtime.

[joep]

It's difficult to diagnose these early boot issues on cloud hardware. Every other x86 machine we tried worked just fine: qemu host mode & tcg emulation, our in-house kvm, bare hardware. Even though Ivan provided a patched kernel to mirror the kernel uart output to vga, this happens well before that code path is ever reached and so every boot was just completely silent after bootloader hand off. As we also discovered, there are differences between providers as to what machine features are enabled at their various tier levels so the matrix of possibilities is fairly extensive.

From a future microkit user's perspective, I'd recommend either providing microkit kernels that don't assume optional hardware features are present or documenting which optional hardware features are assumed to exist for which builds. From a product marketing perspective, however, kernels that align with the verification subset are just a necessity.

[joep]

Thanks for the KernelHugePage: False fix. It worked to successfully boot on the cloud VMs.

[lsf37]

We've fixed it such that having KernelHugePage: False should now work, but we should consider whether we should have that set by default or not. While we don't support huge pages right now, it is something we do want to do eventually so I'm not sure we want to disable huge pages in seL4 by default.

I don't think it's in the verification subset and it's currently default off in seL4 too, so having it default off in Microkit too would make sense.

KernelHugePage is by default on in seL4 currently and that is the config that is also in the functional correctness proof for x64.

I'm not sure how complicated it would be to get seL4 to dynamically support huge pages so it we didn't have to decide at build-time. I imagine it's not trivial.

It seems easy: We just have to change the config_set(CONFIG_HUGE_PAGE) checks to an inline function call that returns whether the CPU supports it or not, in addition to CONFIG_HUGE_PAGE being set.

There even is already an asm function huge_page_check in src/arch/x86/64/head.S. I think (not) supporting huge pages dynamically would be feasible to do and to add in the functional correctness proof.

If boot handles it dynamically, the only real difference would be in the decode function for mapping huge pages, which would return an error if the CPU doesn't support it. This would be a fairly small verification update only and would remove more ifdefs as well.

(This leaves user space to deal with the problem as you mentioned, but that's pretty much all the kernel can do).

[Indanz]

Oops, not sure how I missed that. I'll blame the hot weather and unfortunate wrapping making me misread the DEFAULT_DISABLED OFF.