Hi, I am a 2nd-year grad student at the Systopia Lab in UBC. I am using seL4 for the OS research project at I have a few independent questions: 1. Virtual Machines can be implemented with different levels of support from the hardware. If we talk about x86_64, in the most basic terms, you could have VMs without or without VT-X extensions. Looking at the resources available on the seL4 site, I think the given VMM libraries assume VT-X. Is there an example that does not use VT-X? 2. The scheduler inside seL4 is relatively simple. I have heard(Thanks Nick!) that if a complicated scheduling policy is desired, it can be done in userspace. A user-level component that has the capabilities to all the TCB's can play with the priority, resume/pause, and achieve any arbitrary scheduling. Is there an example available which I could look at? 3. I would like to implement a new functionality of memory quota, where different user-apps can be assigned memory quota and not just the physical pages. Does such a functionality belong in the kernel or the userspace component(say memory quota manager)? In the latter case, it would be just an endPoint capability to the quota manager service, so how does one split it - say split a quota of 100MB into two separate 50MB quotas. This is more a generic micro-kernel query rather than seL4 specific, but any insights would help. Thanks, Sid sid-agrawal.ca