Skip to content

A tiny real-time kernel focusing on formal reliability and simplicity.

License

Notifications You must be signed in to change notification settings

EDI-Systems/M5P01_Prokaron

Repository files navigation

logo

RMP Real-time Kernel

Github release Github commits Discord

language Build OpenSSF Best Practices Codacy Badge

点击 这里 查看中文版。

  RMP is a small hobbyist real-time operating system which focuses on formal reliability and simplicity. It achieves reliability by deployment of formal techniques(not completed yet; only whitebox testing with 100% branch coverage done. The kernel can be regarded as pre-certified IEC 61508 SIL2, or EAL 4). All the basic functionalities that are necessary for RTOSes are provided, but nothing more. This guarantees that the system is the minimum possible kernel and is also suitable to be used as a guest operating system when hosted on virtual machine monitors.

  This operating system is much leaner than any other RTOSes, especially when compared to FreeRTOS or RT-Thread, and understanding it should be simple enough. Yet it provides a complete set of functions that you may need during resource-constrained microcontroller development, such as efficient memory management, anti-aliasing graphics, and various helper functions. All these features come in a single .C file, and are without any extra RAM consumption!

  The manual of the operating system can be found here.

  Read Contributing and Code of Conduct if you want to contribute, and Pull Request Template when you make pull requests. This software is an official work of EDI, and thus belongs to the public domain. All copyrights reserved by EDI are granted to all entities under all applicable laws to the maximum extent.

  For vendor-supplied packages and hardware abstraction libraries, please refer to the M0A00_Library repo to download and use them properly.

Why a New Hobbyist System?

  Existing RTOSes can be divided into three categories: enterprise, hobbyist and teaching. Enterprise systems are usually developed for real-world deployment and are great all-round, yet they at least put all verification documents and techniques behind a paywall, if code itself is free. Hobbyist systems are numerous with new repositories created nearly every day, but they lack long-term commitment and are frequently abandoned after a while. Teaching systems are built for college students, and lack depth when it comes to advanced topics such as verification.

  To this end, RMP seeks to build a fully open, capable and understandable system that is certified to the teeth. You can use the repository in three ways: (1) modify and deploy it in real-world environments, (2) follow its code and documents to get a full understanding of all details of the technologies involved, and (3) throw the system away and roll your own with the knowledge gained from this project.

  The construction of the system will proceed in three stages. In the first stage, we refrain from writing a formal specification beforehand but develop the system like any other hobbyist system. We port the system to as many architectures as possible to validate the flexibility of its abstraction, and run as many application classes as possible to guarantee the usability of its interface. In the second stage, we use the first implementation as a guide to retrovert a formal specification of the system, and prove the system model have certain desirable properties. In the last stage, we develop a formal semantics of the chosen C subset and rewrite the entire kernel according to the formal model while producing the required documents for functional safety (specifically, IEC 61508 SIL 4 and ISO 26262 ASIL D, maybe EAL as well, and we focus on the former first), and put the entire process (excluding those that we don't have copyright on, i.e. the standards) in public domain.

  No specific timetables are set for the development of the system. Currently the first stage is currently considered complete, and the second stage is a ongoing process. If you are interested in the project, please feel free to join; unlike other projects, beginners are welcome here.

Quick Demo

Linux Minimal Runnable Binary

  Compile the 32-bit linux binary here and watch the benchmark results!

NES (FAMICOM) Minimal Runnable Binary

  Download the precompiled "game" here, load it into your favorite emulator (or a flashable Namco 163 mapper cartridge and plug it into the real console), and watch the benchmark results!

FAMICOM

  The Namco 163 is not optional, as the system relies on it to provide IRQ timers for performance measurement. Namco 163 is the only mapper that featured a readable timestamp counter, and can be found on cartridges that also originally host famous games such as "Star Wars" and "Sangokushi II: Hanou no Tairiku (三国志II 覇王の大陸)". The chip is sometimes also known as Namcot 163, or iNES mapper 019.

Built-in Graphics : Widgets, Example and FXAA Anti-Aliasing

Controls Calculator FXAA

Basic Thread Operations

Create a thread

    RMP_Thd_Crt(&Thd_1            /* Thread control block */,
                Func_1            /* Thread entry */,
                &Stack_1          /* Stack address */,
                sizeof(Stack_1),  /* Stack size */,
                (void*)0x12345678 /* Parameter */,
                1                 /* Priority */, 
                5                 /* Timeslices */);

Delete a thread

    RMP_Thd_Del(&Thd_1            /* Thread control block */);

Suspend a thread

    RMP_Thd_Suspend(&Thd_1        /* Thread control block */);

Resume a thread

    RMP_Thd_Resume(&Thd_1         /* Thread control block */);

Delaying a Thread

Delay

    void Func_1(void* Param)
    {
        RMP_LOG_S("Parameter passed is ");
        RMP_LOG_H((ptr_t)Param);
        RMP_LOG_S("\r\n");
        while(1)
        {
            RMP_Thd_Delay(30000);
            RMP_LOG_S("Delayed 30000 cycles\r\n\r\n");
        };
    }

    void RMP_Init_Hook(void)
    {
        RMP_Thd_Crt(&Thd_1, Func_1, &Stack_1, sizeof(Stack_1), (void*)0x12345678, 1, 5);
    }

Send from One Thread to Another

Send

    void Func_1(void* Param)
    {
        ptr_t Time=0;
        while(1)
        {
            RMP_Thd_Delay(30000);
            RMP_Thd_Snd(&Thd_2, Time, RMP_SLICE_MAX);
            Time  ;
        };
    }

    void Func_2(void* Param)
    {
        ptr_t Data;
        while(1)
        {
            RMP_Thd_Rcv(&Data, RMP_SLICE_MAX);
            RMP_LOG_S("Received ");
            RMP_LOG_I(Data);
            RMP_LOG_S("\n");
        };
    }

    void RMP_Init_Hook(void)
    {
        RMP_Thd_Crt(&Thd_1, Func_1, &Stack_1, sizeof(Stack_1), (void*)0x12345678, 1, 5);
        RMP_Thd_Crt(&Thd_2, Func_2, &Stack_2, sizeof(Stack_2), (void*)0x87654321, 1, 5);
    }

Counting Semaphores

Semaphore

    void Func_1(void* Param)
    {
        while(1)
        {
            RMP_Thd_Delay(30000);
            RMP_Sem_Post(&Sem_1, 1);
        };
    }

    void Func_2(void* Param)
    {
        ptr_t Data;
        while(1)
        {
            RMP_Sem_Pend(&Sem_1, RMP_SLICE_MAX);
            RMP_LOG_S("Semaphore successfully acquired!\r\n\r\n");
        };
    }

    void RMP_Init_Hook(void)
    {
        RMP_Sem_Crt(&Sem_1,0);
        RMP_Thd_Crt(&Thd_1, Func_1, &Stack_1, sizeof(Stack_1), (void*)0x12345678, 1, 5);
        RMP_Thd_Crt(&Thd_2, Func_2, &Stack_2, sizeof(Stack_2), (void*)0x87654321, 1, 5);
    }

Memory Pool Operations

    /* Initialize memory pool */
    RMP_Mem_Init(Pool, Pool_Size);

    /* Allocate from the pool */
    Mem=RMP_Malloc(Pool, Alloc_Size);

    /* Free allocated memory */
    RMP_Free(Pool, Mem);

Performance on all Supported Architectures

  The absolute minimum value for RMP is about 1.6k ROM and 432 byte RAM, which is reached on the STM32F030F4 (Cortex-M0) port, and this number even included the 60-byte thread control block and 256-byte stack of the first thread, and a 64-byte kernel interrupt response stack. The OS kernel and the stripped down HAL only consumes 52 bytes of memory combined. If you are willing to push this limit even further, then the manufacturer HAL is a rip-off for you and you can roll your own.

  The current minimal proof-of-concept implementation that can finish the benchmark test is achieved with ATMEGA328P. It only has a meager 32k Flash and 2k SRAM.

  The timing performance of the kernel in real action is shown as follows. All compiler options are the highest optimization (usually -O3 with LTO when available) and optimized for time, and all values are average case in CPU cycles; the WCET registered in test header files is roughly equivalent to this value plus the tick timer interrupt interference.

  • Yield : Yield from one thread to another.
  • Mail : Mailbox communication from one thread to another.
  • Sem : Semaphore communication from one thread to another.
  • FIFO : FIFO read/write pair within a single thread.
  • Msgq : Message queue communication from one thread to another.
  • Bmq : Blocking message queue communication from one thread to another.
  • Mail/I : Send to a mailbox from interrupt.
  • Sem/I : Post to a semaphore from interrupt.
  • Msgq/I : Send to a message queue from interrupt.
  • Bmq/I : Send to a blocking message queue from interrupt.
  • Mem : A pair of memory pool malloc/free.
  • Alrm : Average processing time of five periodic alarms triggered every 1/2/3/5/7 ticks.

  The difference between Msgq and Bmq is, in Msgq, only the receiver may block, whereas in Bmq both may block.

Monumental ports

Chipname Platform Build Yield Mail Sem FIFO Msgq Bmq Mail/I Sem/I Msgq/I Bmq/I Mem Alrm
RP2A03/FC-84 MOS6502 CC65 4073 5435 5435 2028 7726 10445 4831 5180 7220 8350 7484 TBD
RP2A03/MESEN ... ... 4060 5439 5424 2040 7728 10443 4836 5185 7227 8355 7446 TBD
SPCE061A unSP GCC 694 1732 1548 927 2671 3709 1619 1475 2242 2889 3518 TBD
PIC32MZ2048 MIPS XC32 190 345 305 150 475 620 295 260 370 465 365 TBD
... MIPS-FR64 .. 475 630 585 160 775 935 400 360 490 585 371 TBD

Useful ports

Chipname Platform Build Yield Mail Sem FIFO Msgq Bmq Mail/I Sem/I Msgq/I Bmq/I Mem Alrm
ATMEGA328P AVR GCC 408 719 686 313 1065 1318 624 626 905 1073 N/A TBD
ATMEGA1284P ... ... 437 751 717 314 1098 1352 637 639 921 1087 1680 TBD
ATMEGA2560 ... ... 449 774 736 326 1131 1396 656 654 942 1117 1686 TBD
R5F104PJ RL78 CCRL 261 565 520 308 924 1225 539 500 789 964 1854 TBD
PIC24FJ128 PIC24F XC16 152 334 271 168 468 654 274 213 352 461 379 TBD
DSPIC33EP512 DSPIC33E ... 214 447 353 219 608 851 368 278 455 602 448 TBD
MSP430F149 MSP430 CCS 312 641 573 312 985 1278 528 487 739 898 N/A TBD
MSP430FR5994 MSP430X ... 468 1054 891 492 1573 2072 891 784 1176 1464 3291 TBD
STM32F030F4 Cortex-M0 Keil 362 763 666 379 1196 1609 689 616 950 1211 N/A TBD
... ... GCC 366 802 690 396 1246 1685 705 622 954 1200 N/A TBD
HC32L136K8 Cortex-M0 Keil 211 422 370 219 646 873 403 350 532 673 542 TBD
STM32L071CB Cortex-M0 Keil 335 581 532 253 892 1167 554 524 756 945 N/A TBD
... ... GCC 337 656 600 284 947 1260 578 602 794 1003 N/A TBD
STM32F103RE Cortex-M3 Keil 203 438 385 226 684 930 392 354 542 707 518 TBD
... ... GCC TBD TBD TBD TBD TBD TBD TBD TBD TBD TBD TBD TBD
STM32F405RG Cortex-M4F Keil 180 345 321 180 667 886 309 302 498 626 455 TBD
... ... GCC 196 388 345 192 677 953 381 349 566 743 411 TBD
STM32F767IG Cortex-M7F Keil 176 329 277 174 510 694 328 259 413 516 334 TBD
... ... GCC 182 335 288 156 473 643 313 264 375 514 332 TBD
TMS570LS0432 Cortex-R4 CCS 306 493 460 193 686 897 480 464 592 736 533 TBD
TMS570LC4357 Cortex-R5 ... 275 479 467 216 746 998 440 435 595 763 482 TBD
TMS320F2812 C28x CCS 217 493 407 229 706 954 436 381 583 727 939 TBD
TMS320F28335 C28x/FPU32 ... 246 513 440 235 751 1001 440 413 622 770 946 TBD
CH32V307VC RV32IMAC GCC 209 386 336 172 538 698 350 306 436 555 433 TBD
... RV32IMAFC ... 217 398 341 172 557 705 358 307 444 556 433 TBD
Xeon 6326 X86-LINUX ... 24k 24k 24k 46 24k 24k 31k 30k 34k 53k 159 TBD

RVM virtualized ports

  • V : Virtualization overhead of normal operations.
  • V/I : Virtualization overhead of interrupt operations.
Chipname Platform Build Yield Mail Sem FIFO Msgq Bmq V Mail/I Sem/I Msgq/I Bmq/I V/I Mem Alrm
STM32L071CB Cortex-M0 Keil 382 701 609 302 1007 1347 14% 1370 1292 1545 1741 147% N/A 1216
... ... GCC 400 751 649 321 1064 1420 19% 1424 1341 1603 1796 210% N/A 1291
STM32F405RG Cortex-M4F Keil 252 436 372 200 708 924 40% 1180 1088 1288 1452 281% 385 798
... ... GCC 312 540 448 204 656 1008 59% 1336 1252 1404 1572 250% 380 739
STM32F767IG Cortex-M7F Keil 184 293 275 144 504 705 6% 772 742 899 983 135% 275 578
... ... GCC 192 352 292 148 466 650 6% 903 853 1001 1119 239% 270 508
CH32V307VC RV32IMAC GCC 233 384 336 148 489 629 17% 1287 1239 1340 1421 267% 390 605
... RV32IMAFC ... 325 497 436 169 616 767 50% 1789 1742 1857 1951 399% 390 608

  In contrast, RT-Linux 4.12's best context switch time on Cortex-M7 is bigger than 25000 cycles (it has to run from FMC SDRAM due to its sheer size, so this is not a fair comparison). This is measured with futex; if other forms of IPC such as pipes are used, this time is even longer.

  No cheating methods (such as toolchain-specific peephole optimizations that harm portability, cooperative switches that don't invoke the scheduler, scheduler designs that are fast in average case but have unbounded WCET, or even RMS-style stackless coroutine switches) are used in the experiments, and the reported WCETs in test headers are real. Despite the fact that we list the average case values for generic comparisons, it is important to realize that only WCETs matter in a RTOS; optimizations that help the average case but hurt the worst-case are never suitable for such kernels. If maximum speed is your utmost goal, no system is faster than RMS or DOS; the theoretical context switch time of the RMS is zero (when all tasks have a single state and are inlined), while DOS does not need context switches altogether because it only allows one execution flow.

Architectures NOT Supported

Architecture Reason Workaround
PIC18 Hardware stack Use RMS State-machine based OS
AVR32 In decline Use more popular Cortex-M and RISC-Vs
x86-64 Advanced system Use RME Microkernel-based OS
Cortex-A Advanced system Use RME Microkernel-based OS

  This RTOS focuses on microcontrollers and will never support microprocessors. Multi-core support is also considered out of scope, because most multi-core microcontrollers are not symmetric, and have neither atomic instructions nor no cache coherency; even if RMP would support them, they pose challenges for unaware programmers. For multi-core microcontrollers, it is recommended to boot one RMP instance on each core, and the different instances may communicate with each other through Inter-Processor Interrupts (IPIs).

Getting Started

  These instructions will get you a copy of the project up and running on your board for development and testing purposes.

Prerequisites

  You need a microcontroller development kit containing on of the chips above to run the system. STM32 Nucleo boards and MSP430 Launchpad boards are recommended. Do not use QEMU to test the projects because they do not behave correctly in many scenarios.

  If you don't have a development board, a x86-based Linux port of RMP is also available. However, running RMP on top of linux uses the ptrace system call and signal system, thus it is not particularly fast. Just run the example and observe benchmark output.

  Other platform supports should be simple to implement, however they are not scheduled yet. For Cortex-A and other CPUs with a memory management unit (MMU), use RME Real-Time Multi-Core Microkernel instead; RME supports some microcontrollers as well.

Compilation

  The Makefile, Keil, CCS and MPLAB projects for various microcontrollers are available in the Project folder. Refer to the readme files in each folder for specific instructions about how to run them. However, keep in mind that some examples may need vendor-specific libraries such as the STMicroelectronics HAL. Some additional drivers may be required too. These can be found in M0A00_Library repo.

Running the Tests

  To run the sample programs, simply download them into the development board and start step-by-step debugging. Some examples will use one or two LEDs to indicate the system status. In that case, it is necessary to fill the LED blinking wrapper functions.

  To use the graphics library and other advanced features, please refer to the user manual.

Deployment

   When deploying this into a production system, it is recommended that you read the manual in the Document folder carefully to configure all macros correctly.

Supported Toolchains

  • GCC/Clang-LLVM
  • Keil uVision (ARMCC/ARMCLANG)
  • Code Composer Studio
  • MPLAB X XC16/XC32

  Other toolchains are not recommended nor supported at this point, though it might be possible to support them later on.

Contributing

  Please read CONTRIBUTING.md for details on our code of conduct, and the process for submitting pull requests to us.

EDI Project Information

  • M5P01 R6T1

Starring Contributors

  • Leifeng Song - ARM Cortex-M3/4/7 assembly port.
  • Runsheng Hou - ARM Cortex-M4/7 RVM port and lwIP demo.
  • Yihe Wang - Stable x86/linux/ptrace port.
  • Ran Zhang - C28x DSP port.
  • Kai Zhang - White-box testing.
  • Haotian Liu - RL78 port.