Why Another Real-Time Kernel?
There is no shortage of real-time operating systems. RMP exists because the three existing families each leave a gap that matters for a kernel meant to be both trustworthy and understandable.
- Enterprise systems are built for deployment and are usually excellent all-rounders, but they put their verification documents and formal-safety evidence behind a paywall — even when the code itself is free.
- Hobbyist systems appear constantly, but most are abandoned after a while; long-term commitment and quality control are the exception.
- Teaching systems are written for students and rarely go deep into the advanced topics — formal specification and functional safety in particular.
RMP aims at a fully open, capable and learnable kernel that is certified to the teeth. You can use the repository in three ways:
- modify and deploy it in real products;
- follow its code and documents to understand every detail of how it works;
- throw it away and write your own system with what you learned here.
A three-stage construction plan
The project does not pretend that a hobby kernel is already certifiable. It is building towards certification in public, in three stages.
Stage 1 — a working, portable kernel (complete)
Write the system the way any hobbyist would, without a formal model first. Port it to as many strange machines as possible to validate the flexibility of its abstraction, and run as many application classes as possible to prove that its interface is usable. The result is the RMP tree you see today: one C file, fifty-odd build projects, from 8-bit AVR to Cortex-M55.
Stage 2 — retroverted formal specification (ongoing)
Use the stage-1 implementation as a guide to derive a formal specification of the system, and prove that the model has the properties an RTOS must have: scheduling, resource ownership, blocking and wake-up, interrupt masking. The implementation is not thrown away — it constrains the specification to something that has already survived real hardware.
Stage 3 — verified rewrite
Define a formal semantics for the C subset in use, then rewrite the kernel against the proven model and produce the documentation required for IEC 61508 SIL 4 and ISO 26262 ASIL D (and possibly EAL), with the whole process in the public domain — except the standards themselves, whose copyright the project does not hold.
There is deliberately no timetable. Stage 1 is complete, stage 2 is in progress, and beginners are welcome — unlike many kernel projects, this one is meant to be readable by someone learning the field.
What "minimal" actually means
RMP provides every primitive an RTOS needs and nothing more:
- threads with priorities and timeslices, create/delete/suspend/resume;
- counting semaphores, mailboxes, FIFOs, message queues and blocking message queues;
- periodic alarms, scheduler locking and interrupt-safe variants of every blocking call;
- an efficient memory pool (
RMP_Malloc/RMP_Free) that does not fragment like a naive allocator; - a widget toolkit and FXAA anti-aliasing for small displays.
All of it lives in one C file. Optional subsystems are compiled out rather than linked out, and the optional features do not consume extra RAM: the graphics code operates on caller-supplied buffers.
The payoff is not only size. A kernel that fits in one file, with no hidden allocator and no background threads, can be read end-to-end by one person — and that is a precondition for the verification work in stages 2 and 3.
Reliability today
Formal verification is not finished, and the project says so. What exists today is stronger than the average hobby kernel:
- 100% branch coverage in white-box tests (
Source/Test/rmp_coverage.c), exercised on real silicon; - per-chip WCET tables in the test headers, so the worst case is a measured number rather than an average presented as one;
- a design that keeps the worst case bounded: no average-case-only fast paths, no cooperative switches that skip the scheduler, no RMS-style stackless tricks.
On that basis the current kernel can reasonably be treated as pre-certified IEC 61508 SIL 2, or roughly EAL 4 — a starting point for the formal work, not a substitute for it.
Deliberate limits
RMP targets microcontrollers and does not try to be everything:
| Not supported | Why | Use instead |
|---|---|---|
| PIC18 | Hardware stack architecture | Simpron — RMS state-machine OS |
| AVR32 | In decline | Any supported Cortex-M or RISC-V part |
| x86-64 | Advanced system | Eukaron — RME microkernel OS |
| Cortex-A | Has an MMU | Eukaron |
| Multi-core MCUs | Asymmetric cores, no coherency | One RMP instance per core, talking over IPIs |
If you need memory isolation between applications, run RMP as a guest on RVM — the monitor provides capability-based protection while RMP keeps its ABI and its timing.
Only the worst case matters
The benchmark tables list average-case cycles because they are easy to compare. In a real-time system, only the WCET matters. Optimizations that improve the average case while making the worst case worse are not acceptable in a kernel, and RMP's test headers publish the worst case for every primitive on every supported chip. The project explicitly does not use toolchain-specific peephole tricks, cooperative switches that avoid the scheduler, or designs whose switch time is unbounded.
If maximum speed is the only goal, nothing beats an RMS or a DOS-style single flow — the theoretical context-switch time of an RMS is zero. RMP trades that last increment of speed for predictability and for a kernel you can verify.