Re: [seL4] Scheduling of vCPUs on x86