On Wed, 2023-02-22 at 17:13 -0500, Brian Gerst wrote:
> 
>  /* Control bits for startup_64 */
> -#define STARTUP_SECONDARY      0x80000000
>  #define STARTUP_APICID_CPUID_0B        0x40000000
>  #define STARTUP_APICID_CPUID_01        0x20000000

Might as well change CPUID_01 to 0x80000000 while you're at it?