Skip to main content

TS

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

Authors

Kevin Elphinstone, Amirreza Zarrabi, Kent Mcleod and Gernot Heiser

DATA61

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,
    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}},
    type             = {Conference Paper - Refereed},
    pages            = {8 p.},
    address          = {India}
  }

Download

Served by Apache on Linux on seL4.