A Performance Evaluation of Rump Kernels as a Multi-server OS Building Block on seL4
A Performance Evaluation of Rump Kernels as a Multi-server OS Building Block on seL4
复制标题
作为 seL4 上的多服务器操作系统构建块的 Rump 内核的性能评估
DOI：
10.1145/3124680.3124727
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Gernot Heiser
中科院分区：
文献类型：
--
作者：
Kevin Elphinstone;Amirreza Zarrabi;Kent McLeod;Gernot Heiser
在本文中，我们认为有必要重新考虑构建基于微内核的多服务器操作系统，并引入一个多服务器操作系统体系结构。我们认为，最近对微内核的正式验证为构建通用系统提供了一个引人注目的平台，并且现有系统不适合利用正式验证的微内核。我们的愿景主要是基于残存内核的POSIX多服务器系统，以及少量的基本服务和框架。我们希望该方法能够在组件化、开发工作和遗留系统兼容性之间取得平衡。我们给出了我们最初的努力，并对在seL4上运行的残基内核进行了有前景的性能评估。
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.