Trustworthy Systems

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


Kevin Elphinstone, Amirreza Zarrabi, Kent Mcleod and Gernot Heiser


UNSW Sydney


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

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