[seL4] Kernel won't boot on Qemu/KVM Ivy Bridge (was: Overly eager xsave size rejection)

On 01/09/2017 10:39 PM, Adrian.Danis@data61.csiro.au wrote:

This makes sens to me. You have set feature mask to 3, which means support for SSE and FPU. The size for those two features, which is all the the kernel will enable, is 576 bytes. The 832 is if you were to also turn on AVX (which is bit 2). Now if you set feature mask to 7, so that the SSE, FPU and AVX features are enabled then you should get ebx also reporting 832.

Oh, wow, I completely misunderstood the help message for that. I thought 0 was the bitmask for FPU (ie, "can't disable"), 1 for SSE, 2 for AVX, so 1 | 2 = 3 would be AVX + SSE + FPU. I see now that this understanding is flawed, and it's actually the raw state-component bitmap value.

Of course, if you're able to perform AVX instructions on AVX state with the feature mask set to 3 without getting a fault, then something is going very wrong.

This kernel doesn't even seem to boot at all with -cpu host -enable-kvm (or -cpu IvyBridge), regardless of the configuration. Curiously, with -cpu SandyBridge -enable-kvm, it does boot. It seems to be a qemu bug. It seems to be stuck in some sort of loop handling int_0e (page fault). When I attach gdb, I get this sort of behavior:

mov 0xffffffff80745008,%rsp add $0x3e8,%rsp push %rcx

At the start, rsp is x64KSIRQStack, but after an si $rsp is 0? Another si and it's 0x3e8, and trying to execute the push causes gdb to "wait" until I press Ctrl-c, at which point it's back to the top of int_0e and the stack as reported by bt is unchanged: #0 0xffffffff8071537c in int_0e () #1 0x0000000000000002 in ?? () #2 0xffffffff8071538b in int_0e () followed by some garbage. I expect the "waiting" is gdb not knowing what's happening when qemu makes an interrupt happen. If it's at all useful, here's the kernel under consideration: https://files.octayn.net/sel4-4.0.0-x86_64-pc99 It's 4.0.0 with this config: http://ix.io/1PDr Kofi was able to reproduce this in Qemu, but not on Haswell hardware. Any idea what the issue might be? -- cmr http://octayn.net/ +16038524272