ReL4:高性能异步微内核设计与实现

摘要

微内核在安全性、稳定性和模块化方面相比于宏内核有着极大的优势.然而以seL4为代表的现代微内核在设计上有3点缺陷：1)在支持同步进程间通信(IPC)的情况下冗余地支持了异步通知，这违背了微内核的最小化原则；2)通知机制依赖内核的转发；3)系统调用和同步IPC需要频繁地进出内核，后两点导致了特权级切换成为系统的性能瓶颈.本文旨在设计一款基于用户态中断的高性能异步微内核ReL4,来解决上述问题，其主要特征有：1)在保证功能完备性的前提下，移除同步IPC,精简微内核机制；2)基于用户态中断，设计了无需内核转发的U-notification,减少了特权级切换的开销；3)在U-notification基础上，借助异步编程机制，设计了无需陷入内核的异步系统调用和异步IPC框架，在简化用户态编程模型的同时，进一步减少特权级的切换次数.经测试验证，ReL4将IPC性能最高提升了3x,在IPC频繁的系统(如网络服务器)中将吞吐量提升了1x,证明了ReL4在高并发系统上有着良好的性能.

关键词

微内核 / 异步 / 进程间通信 / 用户态中断