in src/arch/x86/machine/fpu.c:140 on 4.0.0, there is
if (x86_cpuid_ebx(0x0d, 0x0) != CONFIG_XSAVE_SIZE) { printf("XSAVE buffer set set to %d, but should be %d\n", CONFIG_XSAVE_SIZE, x86_cpuid_ebx(0x0d, 0x0)); return false; }
I want to force a large(r than 576) xsave region so that TCBBits is always 11, to help my userspace be vaguely more kernel-config-independent. I don't think it's a problem if the xsave buffer in the TCB is larger than the hardware will actually use?
I also think this is buggy. Shouldn't it be querying ecx, since things like AVX aren't enabled in the kernel?
To be clear, this is my suggested change:
if (x86_cpuid_ecx(0x0d, 0x0) > CONFIG_XSAVE_SIZE) { printf("XSAVE buffer set set to %d, but should be at least %d\n", CONFIG_XSAVE_SIZE, x86_cpuid_ecx(0x0d, 0x0)); return false; }