[seL4] Virtual Machine and scheduling query