为什么还要做一个实时内核？

实时操作系统并不稀缺。RMP 之所以存在，是因为现有三类系统各自留有一块空白， 而这块空白对一个既要可信又要可理解的内核来说至关重要。

• 企业级系统为实地部署而造，通常各方面都很出色，但即便代码免费，其 验证文档和功能安全证据也往往被放在付费墙后面。
• 业余爱好系统层出不穷，却大多在一段时间后被废弃；长期投入和质量控制 才是例外。
• 教学系统为学生实验而写，很少深入到形式化规格和功能安全这些高阶内容。

RMP 的目标是一个完全开放、功能良好且可学习、并且经得起认证推敲的内核。 你可以用三种方式使用这个仓库：

1. 修改并部署到真实产品中；
2. 跟随代码和文档理解其中每一个细节；
3. 扔掉这个系统，用从这里学到的知识写出自己的内核。

三阶段构建计划

项目并不假装一个业余内核已经可以直接认证，而是公开地、分三个阶段走向认证。

第一阶段——可用且可移植的内核（已完成）

像任何业余项目那样先写实现，不预先编写形式化模型。把系统移植到尽可能多、 尽可能古怪的硬件上，以验证抽象的灵活性；在它上面运行尽可能多的应用类型， 以证明接口的可用性。成果就是今天这棵 RMP 源码树：一个 C 文件，五十余个 工程，从 8 位 AVR 到 Cortex-M55。

第二阶段——反向提炼形式化规格（进行中）

以第一阶段的实现作为参照，反向提炼系统的形式化规格，并证明该模型具备 RTOS 必须具备的性质：调度、资源归属、阻塞与唤醒、中断屏蔽。实现不会被丢弃， 它把规格约束在已经经受真实硬件检验的范围内。

第三阶段——经验证的改写

定义所用 C 子集的形式化语义，按已证明的模型重写内核，并产出 IEC 61508 SIL 4 与 ISO 26262 ASIL D（可能还包括 EAL）所需的文档。 整个过程（标准文档本身除外，因为项目不持有其版权）都放在公有领域。

项目刻意不设定时间表：第一阶段已经完成，第二阶段正在进行，而且 欢迎新手——与许多内核项目不同，这里的代码就是写给初学这个领域的人看的。

“最小”究竟意味着什么

RMP 提供 RTOS 必需的全部原语，且仅此而已：

• 带优先级与时间片的线程，支持创建、删除、挂起、恢复；
• 计数信号量、邮箱、FIFO、消息队列与阻塞消息队列；
• 周期闹钟、调度器锁定，以及每个阻塞调用的中断安全版本；
• 高效内存池（RMP_Malloc / RMP_Free），不会像朴素分配器那样碎裂；
• 面向小尺寸显示屏的控件库与 FXAA 抗锯齿。

它们全部位于一个 C 文件中。可选的子系统在编译期裁掉，而不是靠链接器 丢弃，并且不额外消耗 RAM——图形代码直接使用调用者提供的缓冲区。

回报不仅是体积。一个能装进单个文件、没有隐藏分配器、没有后台线程的内核， 可以被一个人从头读到尾——而这正是第二阶段、第三阶段验证工作的前提。

今天的可靠性

形式化验证尚未完成，项目对此直言不讳。但今天已经具备的基础，强于一般的 业余内核：

• 白盒测试达到 100% 分支覆盖（Source/Test/rmp_coverage.c），并在真实 芯片上运行；
• 每颗芯片的测试头文件中都记录 WCET 表，最坏情况是实测数字，而不是把 平均值当成最坏情况；
• 设计上保持最坏情况有界：没有只在平均情况下快的路径，没有绕过调度器的 协作式切换，也没有 RMS 式的无栈技巧。

因此当前内核可以被合理地视为 IEC 61508 SIL 2 预认证等级，或大致 EAL 4——它是形式化工作的起点，而不是替代品。

刻意的边界

RMP 面向微控制器，并不试图包打天下：

不支持	原因	替代方案
PIC18	硬件栈架构	Simpron——RMS 状态机 OS
AVR32	已衰落	任一款受支持的 Cortex-M 或 RISC-V
x86-64	高级系统	Eukaron——RME 微内核 OS
Cortex-A	带有 MMU	Eukaron
多核 MCU	核心不对称、无缓存一致性	每个核跑一个 RMP 实例，通过 IPI 通信

如果需要在应用之间做内存隔离，可以把 RMP 作为 RVM 的客机运行——监视器 提供基于权能的保护，而 RMP 保持它的 ABI 和时序。

只有最坏情况才重要

性能表列出平均周期只是便于比较。在实时系统里，只有 WCET 重要。以恶化 最坏情况为代价换取平均情况更快的优化，在内核中不可接受；RMP 的测试头文件 会为每颗芯片、每个原语公布最坏情况。项目明确不使用针对特定工具链的偷巧 指令序列、绕过调度器的协作式切换，或切换时间无界的调度器设计。

如果唯一目标是极限速度，那么没有任何系统快得过 RMS 或 DOS 式的单执行流—— RMS 的理论上下文切换时间为零。RMP 放弃这最后一点速度，换取可预测性，以及 一个可以被验证的内核。