reL4项目测试报告 #

1. 概述 #

本报告旨在对reL4微内核和reL4-Linux-kit兼容层进行系统性的评估。评估工作主要围绕两部分展开：一是对系统功能完整性的验证，二是对系统综合性能的评测。

1.1 测试目标 #

• reL4内核与seL4内核的二进制兼容情况分析
• reL4-Linux-kit与部分关键Linux syscall的兼容性情况分析
• reL4-Linux-kit对调用相关Linux syscall的测例集合的运行情况分析
• 基于seL4或者reL4的reL4-Linux-kit运行情况的综合性能评估

2. 功能实现评估 #

2.1 reL4对seL4二进制接口的功能实现评估 #

reL4的基本目标为实现一个兼容seL4接口的Rust内核，通过seL4test测试套件验证功能正确性。

seL4test是seL4官方实现的原生测例，总共有241个测例，这些测例针对seL4内核中不同的syscall接口进行测试，用于测试内核是否被正确地实现了。我们以这些测例作为标准，测试reL4的接口的实现是否和seL4兼容。

在reL4现有实现的feature下能够支持的测例分类及其通过情况如附录A和附录B中所示。在附录A中列举的测例分类中，有部分测例本身虽然存在但无需测试，除此之外，reL4已经支持的feature所需的测例均可以正常通过。

在表1中列举了reL4中无需测试的测例。如EPT和IO Port特性相关的测例主要是在x86下才可以支持的，因此，在目前仅仅支持aarch64和riscv64的reL4中，无需通过，其他的测例也是类似，大多是由于目前reL4项目所涉及的硬件特性不足所无需支持。

表1：reL4未测试的测例分类及其数量

2.2 reL4-Linux-kit对Linux syscall的实现评估 #

reL4-Linux-kit的设计目标为兼容现有的部分Linux用户态程序，但是，这些Linux程序所调用的Linux syscall，只是所有的Linux syscall的一部分，换而言之，只需要实现部分的Linux syscall，即可保证兼容性。

在附录C中列举了reL4-Linux-kit所支持的Linux syscall的数量，这些syscall基本构成了一个Linux系统所需的syscall集合。根据其功能的不同，可以分为进程管理、内存管理、权限管理、设备控制、时间管理、事件管理、文件系统、系统信息、信号处理、资源管理等10类共69个具体syscall。其中部分syscall使用了fake实现，即仅仅返回Ok(0)，而不做任何实际的处理。

基于上述实现的syscall集合，我们采用了一些测例进行功能正确性的验证，主要包括basic、run-static、busybox-testcase、lua、iozone、libc、lmbench等测试集合。在附录D中列举了上述测例集合所使用的syscall，这些测例集合基本能够涵盖我们实现的syscall集合，只有两个在reL4-Linux-kit中实现了的syscall并未被这些测例集合使用，这两个测例在表2中列举。

表2：已实现但未被Linux测例使用的系统调用

最后，必须指出，在我们的测例集合中，还有部分syscall被调用到了，但是并没有在reL4-Linux-kit中实现，这些syscall及其含义在表3列举。这些被调用但未实现的syscall主要集中在网络管理模块，由于reL4-Linux-kit并未实现相应的网络模块，因此这些syscall都无法实现，同时，在run-static测例集合中对应的socket测例也会相应的报错，我们忽略这部分的报错，其余少数未实现的系统调用因不影响测试核心结果的正确性，故在当前阶段予以保留。

表3：Linux测例需要但未实现的系统调用

基于seL4内核和基于reL4内核的reL4-Linux-kit目前均能够正确完成上述的Linux下的测例，这个结果更进一步地证明了reL4内核在实现上的正确性，即reL4内核能够二进制兼容seL4内核，同时也能够说明，reL4-Linux-kit的现有实现能够正确支持Linux下的程序的运行。

3. reL4性能评估 #

对于reL4相关的性能评测，目前seL4内核项目也已经实现了seL4bench的测例，用于测试seL4的各类性能。为了支持这些测试，必须在reL4项目中增加seL4bench相关syscall和一些硬件环境的支持。

3.1 One Way IPC测试 #

这里的IPC相关测试主要指的是单向的IPC的性能。seL4bench的相关测试并没有支持MCS特性，因此MCS相关syscall的测试并没有支持。

seL4bench中单向IPC性能测试涉及到的syscall包括：SYS_CALL、SYS_SEND、SYS_REPLY_RECV这三个syscall。在该测试中的相关测试还对比了IPC的两个线程是否在同一个地址空间下，以及不同IPC消息长度下的差别。

测试结果揭示了以下现象：reL4在各个场景下都缺少IPC的优化，采用了统一的syscall的路径；在seL4下的同一地址空间的IPC具有良好的优化，其开销的Cycles为reL4下同样One Way IPC的五分之一左右；在不同地址空间下，同样为0B长度的IPC消息发送，不同的syscall接口也展现出了不同的性能；在长度为10B的IPC消息发送中，reL4和seL4虽然仍然存在一些性能上的差异，但是差异不大。

对此，后续的工作需要着眼于单向IPC测试中相关的系统调用路径，尤其是fastpath及其优化实现。

3.2 中断相关测试 #

对于reL4和seL4的中断相关性能的对比测试结果表明：seL4的irq，无论是否存在context switch，其波动范围都较小，具有很好的稳定性。reL4的irq稳定性则远不如seL4，其波动范围更大，极值发生概率更高，但是其均值在存在context switch和无context switch的两种情况下，基本相近，可以认为其出现了跟前一节同样的缺少优化的现象。

值得注意的是，在所有其他的测试中，均能表明reL4目前的实现，性能相比seL4存在一定的差距，但是，在本测试中，存在context switch的情形下，seL4进行IRQ处理需要的Cycles比reL4进行IRQ处理需要的Cycles更多。

可以认为reL4的测试依然没有对相关路径进行优化，只有这样才能解释reL4的irq处理需要的Cycles基本接近且远高于seL4的irq处理所需的Cycles。而存在context switch情形下，该数值低于seL4下的数值，应当可以认为使用Rust编写的代码在性能上经过路径优化之后，有一定潜力优于C编写的seL4。

3.3 信号相关测试 #

信号机制同样是seL4下重要的消息发送机制，对于信号相关测试的结果表明：在向高优先级进程发送信号的时候，平均延迟的Cycles呈现出了急剧的增长。在这两个测试结果中，seL4下的测试结果均展现出了很好的稳定性和比reL4更好的性能。

3.4 同步相关测试 #

同步相关测试主要目的是为了测试通过seL4/reL4的通信机制实现消息同步所带来的开销，相比于单纯的One Way IPC性能，该测试提供了更加全面的系统消息传递开销评估。

从测试结果来看，随着消息等待者的数量增长，在reL4和seL4下的平均等待时间均呈现下降趋势。随着消息等待者的数量上升，整体的消息发送和接收的时间一定是增长的，因为更多的消息需要发送和接收。而每个消息接收者存在从发送消息之后，到被调度出来的时延，因此在消息接收者数量少的时候，消息接收者必须等待其他进程被调度出来并执行，这增加了其时延。当消息接收者数量多的时候，一个消息接收者接收到消息之后，下一次调度的进程依然是一个消息接收者，因此其平均接收时间一定会逐步下降。

在测试中，seL4内核在所有测试结果中，均展现出来比reL4更好的性能和稳定性。考虑到reL4的One Way IPC章节所提出的可能，由于可能存的在syscall代码调用路径上的优化不足，在该测试中存在这样数量级别的性能差距，是可以理解的。

3.5 映射相关测试 #

映射相关测试主要针对于系统的内存映射性能的评估，测试项目包括：Prepare Page Tables、Allocate Pages Mapping、Mapping、Propect Pages as Read Only、Unprotect Pages。

从测试结果来看，reL4和seL4之间表现出来的性能行为基本一致，基本可以说明，reL4在功能上可以对标seL4内核，但是存在一个性能gap（请注意坐标轴为对数坐标轴），这在几乎所有的测试中都是存在的。考虑到之前的分析，这样的性能差距是可以理解的，并且是系统性的差距。

4. reL4-Linux-kit综合性能评估 #

对于reL4-Linux-kit的测试，由于其可以基于seL4或者reL4内核运行，因此，可以对比其在reL4和seL4上的执行效率来评测reL4-Linux-kit。同时，由于其支持Linux syscall，也可以将reL4-Linux-kit在reL4上的性能，对比原生Linux的执行性能。

对于reL4-Linux-kit的测试内容，主要包括libc，busybox，lua，iozone，lmbench等测试。除此之外，函数调用转IPC的设计，会导致不同模块合并成一个模块的行为会影响其性能，对此也需要做评估。我们只评测所有可拆分的模块均进行拆分，以及所有模块均进行合并的结果，而不是穷举所有模块的组合可能。

我们评测的平台配置如下：

• CPU: AMD Ryzen 9 9950X3D (32) @ 5.756GHz
• OS: Ubuntu 24.04.3 LTS x86-64
• Kernel: Linux 6.14.0-28-generic
• Memory: 96GB

测试结果如表4所示。

表4：Linux测例在不同操作系统配置下的性能测试结果（单位：秒）

对于表4的测评结果，可以清晰的看到基于seL4/reL4内核的reL4-Linux-kit和Linux内核之间具有较大的性能差距。微内核的几个测例中，以seL4作为内核，并将所有服务组件拼合成为单个服务组件的方式运行时，性能与Linux差距最小。由于取消了系统服务组件间的IPC，因此该测例下与Linux的性能差距主要来源于两个地方，一个是seL4截获用户态Linux app的syscall并转发给用户态系统服务组件，与直接进行syscall进入宏内核的性能差距，这是使用我们所设计的syscall转IPC方法无可避免的一个开销；另一个是用户态系统服务组件本身和Linux执行的性能差距，Linux作为一个经典的宏内核实现，其具有非常良好的优化，而reL4-Linux-kit仅仅作为验证兼容系统可行性的一个尝试。因此，seL4下的reL4-Linux-kit和原生Linux下存在如此巨大的性能差距，实属正常。

其次，对于我们设计的函数调用和IPC调用之间的透明转换机制，分别在reL4内核和seL4内核的基础上进行了评测。这两者之间的性能差距纯粹是来自于函数调用和IPC调用方式之间的差距，在同一个内核下，两者差距始终不大，甚至在libc测试中，使用reL4内核作为基础，拆开所有组件的测试结果比拼合所有组件性能略好的情况。当然在iozone测试中也有拉开一定差距的情况。总体而言，这两种通信方式之间差距相对没有那么巨大，但也跟不同测例集合需要的组件间通信数量有一定关系，在如iozone这样的组件间通信数量较多的测例集中，自然会出现函数调用通信转为IPC通信带来的开销更大的现象。总体而言，根据以上测试结果，可以认为我们设计的函数调用和IPC调用透明转换的机制具有较好的性能优势。

第三，对于reL4和seL4之间的实现性能对比。这是兼容同一个二进制接口的内核的两个不同实现，但是也很明显，reL4实现的性能略落后于seL4实现的性能，总体综合性能差距在10%左右。由于这些测例本身大量调用了seL4/reL4的各类系统调用而非个别系统调用路径，无法简单的认为是其中的某个系统调用路径性能过差而产生这样大的差距。该差距更有可能归因于Rust和C的差距，更确切的说，可能依然来自于重复检查或其他的为了在Rust下能够安全使用一些变量所引入的编译器额外检查开销。这并不意味着Rust的安全机制是没用的，只是在改写一个已经经过完整形式化验证的内核的时候，部分Rust检查可能是冗余的。除此之外，为了能够和seL4进行合并开发，我们实现了以Rust静态库和C代码链接的形式，引入了一些#[no_mangle]的Rust函数，这也会导致为了兼容性，而损失一定的编译优化性能。

最后，必须看到若干不正常的样例。很明显的，在run-static和lmbench两个测例中，Linux所花费的时间都更多，这并不是意味着Linux的性能更差，而是由于其中个别测例的问题。例如，在前面分析功能实现的时候，run-static测例集合中的socket测例集合并未实现，因此会存在fake实现和报错的问题，而Linux对网络socket的超时报错有着自己的机制，并非直接简单的fake实现，因此可能会导致测试完成的时间有所不同。这些差异实际来自于syscall实现的语义兼容性和reL4-Linux-kit只完成了部分Linux syscall导致的，而并非来自内核的实现性能。

5. 结论 #

本章对 reL4-Linux-kit 原型系统进行了全面的评估，主要包括功能实现评估和性能评估两个维度。

第一，在功能实现评估方面，通过系统性的测试验证了 reL4 内核与 seL4 内核的二进制接口兼容性，证实了基于组件化重构的 reL4 内核能够完整保持与 seL4 的二进制兼容特性。同时，详细评估了reL4-Linux-kit对Linux系统调用的兼容性支持范围，并测试了多组Linux应用程序在该环境下的运行情况和系统调用情况。

功能实现评估的实验结果表明，基于组件化架构重构的reL4微内核及其配套的 reL4-Linux-kit 用户态兼容层，作为一个完整的研究原型系统，成功实现了既定的功能性目标。这为构建全栈内存安全的操作系统架构提供了一个可行且具有实践价值的技术方案。

第二，在性能评估方面，我们对比分析了同一测试套件在原生 Linux环境、基于seL4内核的reL4-Linux-kit环境以及基于 reL4 内核的 reL4-Linux-kit 环境下的性能表现。测试还包含了系统组件合并与解耦两种模式下的性能差异比较。对于观察到的性能差异，我们从微内核架构特性、IPC 开销、Rust开发语言等角度进行了初步分析。

性能评估结果显示，尽管 reL4 和 reL4-Linux-kit 的实现与原生 Linux 性能存在预期内的差距，但作为一个研究原型系统，其性能表现仍在可接受范围内，证明了该架构的实用性和进一步发展潜力。这些性能数据也为后续优化工作提供了重要的参考依据。

附录 #

附录A：reL4有效测例分类及数量 #

附录B：reL4具体实现的测例及其依赖的feature #

该表格的含义如下：纵轴为每个测例，横向为各个feature。如果某个测例需要相关feature。如测例1需要feature A和C，就会在测例1所在行的feature A和C所在格添加记录。在开启了feature A和C的情况下，如果这些测试可以正常通过，那么这些记录都会打上√，否则都会打上×（或者在备注中注明无法成功测试的原因）。

目前已经实现的feature所支持的测例均已成功运行。

附录C：reL4-Linux-kit的Linux syscall实现情况 #

附录D：Linux测例syscall调用统计表(aarch64) #