Hi Corey,

The original intention of the 'aggressive' check was to somewhat prevent your case where the user has set the size higher than required and may be inadvertently be wasting memory by having the TCBBits end up larger than needed. I agree that it can be a little inconvenient, so will change it allow sizes that are larger, but emit a warning.

Comparing against ebx instead of ecx is quite deliberate as this way we only measure the size required for the features that the user actually wanted to use as defined in CONFIG_XSAVE_FEATURE_SET. This is why we do this check just after performing 'write_xcr0' with said desired features.

Adrian

On Fri 06-Jan-2017 6:05 PM, Corey Richardson wrote:
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;
}





 


_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel