Skip to main content


A performance evaluation of rump kernels as a multi-server OS building block on seL4


Kevin Elphinstone, Amirreza Zarrabi, Kent Mcleod and Gernot Heiser



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.

BibTeX Entry

    publisher        = {ACM},
    doi              = {10.1145/3124680.3124727},
    booktitle        = {Asia-Pacific Workshop on Systems (APSys)},
    author           = {Elphinstone, Kevin and Zarrabi, Amirreza and Mcleod, Kent and Heiser, Gernot},
    month            = sep,
    year             = {2017},
    date             = {2017-9-3},
    title            = {{A} Performance Evaluation of Rump Kernels as a Multi-server {OS} Building Block on {seL4}},
    address          = {India}


Served by Apache on Linux on seL4.