paper

A Performance Evaluation of Rump Kernels as a Multi-server OS Building Block on seL4

  • Authors:
Read the paper

📜 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.

✨ Summary

Paper summary

The paper proposes revisiting microkernel-based multiserver operating systems using seL4 as a formally verified foundation and rump kernels as a practical way to reuse NetBSD-derived operating-system components. Its envisioned architecture decomposes services such as naming, process management, memory management, device access, networking, and file systems into isolated components, while using capability-based protection and least-authority principles to reduce the trusted computing base and contain faults.

The authors ported the Rumprun bare-metal unikernel platform layer to seL4. The port adapted execution contexts, interrupt delivery, synchronization, memory management, DMA, MMIO, timers, console output, and low-level device access. Evaluation used an Iperf TCP server and compared Rumprun on bare metal, Rumprun on seL4, native NetBSD, and Linux on a single-core 32-bit system with Gigabit Ethernet. The seL4 version had little performance impact relative to the bare-metal version and, according to the paper’s measurements, exceeded native NetBSD performance. Using IOAPIC or MSI interrupt mechanisms reduced seL4-specific CPU overhead to below 0.3% of total available CPU. The port removed 1,402 lines of code and added 677 lines, indicating that most of the adaptation effort was confined to the platform layer.

Subsequent use

The paper is cited as prior work by LibrettOS, a later multiserver-library OS prototype that also uses rump kernels to reuse NetBSD drivers and POSIX/BSD-compatible software. (ssrg.ece.vt.edu) It is also cited by Kite, a later system for lightweight critical service domains, as part of the prior work on multiserver operating-system architectures. (ssrg.ece.vt.edu) These citations document continued use of the paper as background for research on rump kernels, multiserver systems, and componentized operating-system designs; they do not by themselves establish that the paper directly caused those systems to be developed.