Predictable Communication and Migration in the Quest-V Separation Kernel

摘要

Quest-V is a separation kernel, which partitions a system into a collection of sandboxes. Each sandbox encapsulates one or more processing cores, a region of machine physical memory, and a subset of I/O devices. Quest-V behaves like a distributed system on a chip, using explicit communication channels to exchange data and migrate addresses spaces between sandboxes, which operate like traditional hosts. This design has benefits in safety-critical systems, which require continued availability in the presence of failures. Additionally, online faults can be recovered without rebooting an entire system. However, the programming model for such a system is more complicated. Each sandbox has its own local scheduler, and threads must communicate using message passing with those in remote sandboxes. Similarly, address spaces may need to be migrated between sandboxes, to ensure newly forked processes do not violate the feasibility of existing local task schedules. Migration may also be needed to move a thread closer to its required resources, such as I/O devices that are not directly available in the local sandbox. This paper describes how Quest-V performs real-time communication and migration without violating service guarantees for existing threads.