There’s been some discussion recently on the mailing list about multiprocessing and multikernels, and the lack of user libraries to support this scenario.
Does the seL4 kernel itself support running in a multikernel configuration right now?
If not, what changes would be required to the kernel for this?
Are there any features you’d like to add to the kernel to better support this scenario?
For example, could it be possible to transfer untyped memory from one kernel to another, instead of it being statically partitioned?
We do not currently provide a mechanism to implement a multikernel system. Such a system would likely require additional APIs to the seL4 kernel to start distinct images on multiple clusters of cores.
We would like to extend the existing seL4 model and principles in order to provide this mechanism but much of how the kernel currently operates is made more tractable by the mutually exclusive kernel heap. The heap in this case is the collection of all untyped memory objects and all kernel objects derived from the untyped memory objects.
The kernel ensures that all state in the kernel heap and the scheduler for each core remains consistent but enforces minimal policy on the kernel objects themselves. User level is free to use the kernel object to implement whichever policy they like, this includes access from any thread in the system with the appropriate capabilities.
The benefit of a multikernel would be that each kernel operates on a distinct heap allowing multiple kernels to run concurrently without interfering with each other’s local correctness. Currently, objects in the kernel’s heap are connected by references in a few important ways that make splitting the heap difficult.
The capability derivation tree (CDT) describes the relationship between capabilities produced in the process of seL4_CNode_Copy, seL4_CNode_Mint, and seL4_Untyped_Retype. The CDT is essential for seL4 to achieve its goal of security through delegation and revocation. Whenever you delegate access to a resource by deriving a capability original capability you can then use that original capability to revoke all derived capabilities.
The graph created by seL4_CNode objects (including the embedded CNode within each seL4_TCB also links objects in the kernel heap. An entry in any CNode could be a capability to any object in the entire kernel heap. This allows for a thread to be granted access to any object and is fundamental to the policy freedom of the seL4 kernel.
Virtual address spaces form yet another way in which heap objects are linked. Each object in a virtual address space requires a reference to the root of the address space so that the address space may be correctly updated if that object is removed or unmapped. Each address space is assigned a globally unique address space identifier (ASID) which is stored in every capability to objects mapped into that address space.
There are numerous other ways in which kernel objects may be linked to one another.
Splitting the heap into portions assigned to individual cores impacts each of the above mechanisms within seL4 as any useful design requires that the references used in many of the above could potentially span heaps of distinct kernel images.
Adding support for multikernels is certainly desirable but requires a lot of thought before we have a model that is sufficient for all of the use cases we could possibly support and that also maintains the existing design goals of seL4.
I haven’t looked closely at that part of the POSIX specification recently, but I suspect that much of that interface depends on the operating system being tightly coupled, so that whatever is managing threads is aware of dynamic memory and address space management. Supporting this directly on seL4 would make little sense; you’d have to build a system specifically to support that interface and deciding how to do that also depends greatly on the design of the rest of the operating system.
I haven’t looked closely at that part of the POSIX specification recently, but I suspect that much of that interface depends on the operating system being tightly coupled, so that whatever is managing threads is aware of dynamic memory and address space management. Supporting this directly on seL4 would make little sense; you’d have to build a system specifically to support that interface and deciding how to do that also depends greatly on the design of the rest of the operating system.
In seL4 terminology, threads appear to share both a CSpace and a VSpace, and existing programs rely heavily on this. I say “appear” because there need not be a 1-to-1 correspondence between seL4 capabilities and application-level handles.