Trustworthy Systems

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

Authors

Kevin Elphinstone, Amirreza Zarraby, Kent McLeod and Gernot Heiser

DATA61

UNSW Sydney

Abstract

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

  @inproceedings{Elphinstone_ZMH_17,
    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              = {https://doi.org/10.1145/3124680.3124727},
    month            = sep,
    numpages         = {8 p.},
    paperurl         = {https://trustworthy.systems/publications/full_text/Elphinstone_ZMH_17.pdf},
    publisher        = {ACM},
    title            = {{A} Performance Evaluation of Rump Kernels as a Multi-server {OS} Building Block on {seL4}},
    year             = {2017}
  }

Download