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.
Show replies by date