A Performance Evaluation Of Rump Kernels As A Multi-Server Os Building Block On Sel4

In the paper, we argue that it is worthwhile to revisit building microkernel-based multiserver operating systems, and introduce a multiserver OS architecture. We argue that recent formal verification of microkernels provides a compelling platform for constructing general purpose systems, and that existing systems are not appropriate to take advantage of a formally verified microkernel.Our vision is of mostly-POSIX multiserver systems based on rump kernels, with a small set of fundamental services and frameworks. We expect the approach to provide a balance between componentisation, development effort, and legacy system compatibility.We present our initial efforts with a promising performance evaluation of a rump kernel running on seL4.