An evaluation of capabilities for a multikernel

With ever-increasing numbers of cores in modern hardware and the prospect of heterogeneous architectures becoming more appealing, re-liance on cache-coherent shared memory is a source for hardware design and scalability problems. To accommodate these changing requirements, multi-kernel operating systems aim to reduce the sharing in the kernel by replicating kernel state on every core. To retain the ability to share resources between applications on dif-ferent cores, we design a capability system derived from a single-core capability system used in the seL4 microkernel, but with operations ex-tended to handle the incomplete views of the capability system present on each core. Through the introduction of an ownership property we achieve a design similar to ones found in distributed object systems. We illustrate where synchronization is still needed to ensure consistency, and demonstrate the need for an index datastructure when exchanging infor