Skip to content

Latest commit

 

History

History
319 lines (253 loc) · 21 KB

README_CN.md

File metadata and controls

319 lines (253 loc) · 21 KB
Raw

logo

RMP Real-time kernel

Github release Github commits Discord

language Build OpenSSF Best Practices Codacy Badge

Click HERE for English version.

  RMP 是一个专注于形式化验证和简易可用的小型实时系统。它通过采取形式化方法来确保系统的可靠性（当前验证工作还__未完成__；不过，100%的白盒测试分支覆盖率已经达到。目前的内核可以被看作IEC 61508 SIL2预认证等级，或者EAL 4）。所有的实时操作系统必备的功能它都具备，但是并不在此基础上提供更多可选组件以确保内核的精炼性。这样，得到的内核就是一个最小化的内核，可以很方便地对它进行形式化验证。同时，它还可以作为客户操作系统运行在虚拟机监视器上。

  本系统比以 FreeRTOS 和 RT-Thread 为代表的全功能系统相比要小得多，而且理解起来应该也相对容易得多。即便本系统仅仅包含了一个.C文件，它仍然提供了高效的内存管理，抗锯齿图形界面库和其他实用函数，并且这些功能的实现都不消耗任何额外的RAM！

  本系统的手册可以在 这里 找到。

  如果想要参与开发，请阅读 参与 和 规范 两个指导文档。如果要提交拉取请求，请使用 拉取请求模板 。 本软件是EDI的官方作品，因此属于 公有领域 。 所有由EDI保留的版权在所有适用的法律条款下尽最大可能地授权给所有实体。

  对于那些由微控制器厂商提供的硬件抽象层软件包，请到 M0A00_Library 软件仓库自行下载。

为什么要做一个新系统？

  现成的实时操作系统大概可分为三类：企业级、业余爱好和教学用。企业级系统通常是为实地部署准备的，它们在各方面都非常出色。然而，即便其代码可能是开源甚至免费的，其几乎所有的功能安全验证文档和技术细节都是付费内容且叫价奇高。业余爱好者创作的系统则正好相反，虽然免费但缺乏长期的精力投注和合适的质量控制，且屡遭废弃。教学系统介于两者之间，但它专为学生实验开发，缺乏对形式化验证和功能安全等高阶内容的涉猎。

  有鉴于此，RMP努力构建一个完全开放、功能良好和可资学习的经认证系统。可以用三种方法来使用这个项目：（1）修改或部署它，（2）从其代码实现和开发过程熟习其原理，或（3）扔掉这个系统并开发一个适合自己的新系统。

  整个系统的构建分为三个阶段。首先，我们不直接编写系统的形式化模型，而是向业余爱好者那样开发它。我们将它移植到尽量多的稀奇古怪的硬件上以验证其抽象的灵活性，并在其上运行尽量多类型的应用程序以确保其接口的可用性。然后，我们从第一个阶段的稳定原型和心智模式出发，反向提炼出其理想行为的形式化模型，并证明该模型具有某些良好的性质。最后，我们开发一套C子集的语义，根据上一步得到的形式化模型重写整个内核并证明其正确性。在这个阶段还会产生功能安全认证所需的一切文档（IEC 61508 SIL 4和ISO 26262 ASIL D，可能还包括EAL；优先处理前者），并将它们开源到公有领域（不包括标准文档本身，因为本项目不持有它们的版权）。

  本系统并无固定的开发进度安排。第一阶段工作已经完成，当前展开的是第二阶段的工作。如果你对此项目感兴趣，欢迎加入本项目。和其它项目不同，本项目欢迎新手。

快速演示

可在Linux上直接运行的Demo

  到 这里 编译x86-32位Linux系统上可运行的二进制，观察性能测试的运行结果！

可在红白机（FAMICOM/NES）上直接运行的Demo

  从 这里 下载“游戏”镜像，把它装入你喜欢的模拟器（或者支持南梦宫163扩展芯片的烧录卡并插入实机），观察性能测试的运行结果！

FAMICOM

  南梦宫163扩展芯片是必需的，因为系统需要利用它内部的IRQ计时器来测量性能。在所有扩展芯片中，唯一支持可读取计时器的只有南梦宫163，这颗芯片也被用于“星球大战（Star Wars）”、“三国志II 霸王的大陆”等知名游戏。南梦宫163有时也被叫做Namcot 163，或者iNES扩展019。

内建图形库：控件，界面样例和FXAA抗锯齿细节

Controls Calculator FXAA

基础线程操作

创建一个线程

    RMP_Thd_Crt(&Thd_1            /* 线程控制块 */,
                Func_1            /* 线程入口 */,
                &Stack_1          /* 线程栈地址 */,
                sizeof(Stack_1),  /* 线程栈大小 */,
                (void*)0x12345678 /* 参数 */,
                1                 /* 优先级 */, 
                5                 /* 时间片 */);

删除一个线程

    RMP_Thd_Del(&Thd_1            /* 线程控制块 */);

悬起一个线程

    RMP_Thd_Suspend(&Thd_1        /* 线程控制块 */);

解除线程悬起

    RMP_Thd_Resume(&Thd_1         /* 线程控制块 */);

线程延时

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

    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);
    }

计数信号量

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);
    }

内存池操作

    /* 初始化内存池 */
    RMP_Mem_Init(Pool, Pool_Size);

    /* 从内存池分配内存 */
    Mem=RMP_Malloc(Pool, Alloc_Size);

    /* 向内存池归还内存 */
    RMP_Free(Pool, Mem);

所有支持架构上的典型性能数据

  本系统的绝对最小值在1.6k ROM和432Byte RAM左右，这个大小是在STM32F030F4（Cortex-M0+）的移植上达到的，并包括了第一个线程的60Byte的线程控制块和256Byte的线程栈，以及64Byte的内核中断响应用栈。操作系统内核和最精简的HAL库一共仅占用了52Byte存储。如果你对这个数字仍不满意，那么可以不使用厂商提供的HAL库而自己写一个版本。

  当前的能完成基准测试的最小概念性移植是ATMEGA328P上完成的，它仅有32k Flash和2k SRAM。

  在真实项目环境中内核的时间性能如下所示。所有的编译器优化选项都被设为最高（通常是-O3），而且时间优化选项也被打开。所有值均为 CPU 周期的平均值；测试头文件中记录的最坏执行时间约等于该值加上定时器中断造成的最坏干扰。

  • Yield : 两线程间的切换操作。
  • Mail : 两线程间使用邮箱进行发送-接收操作。
  • Sem : 两线程间使用计数信号量进行发布-获取操作。
  • FIFO : 在单个线程内进行FIFO读/写。
  • Msgq : 两线程间的消息队列通信。
  • Bmq : 两线程间的阻塞消息队列通信。
  • Mail/I : 从中断发送到某线程邮箱。
  • Sem/I : 从中断发布信号量。
  • Msgq/I : 从中断发送到消息队列。
  • Bmq/I : 从中断发送到阻塞消息队列。
  • Mem : 进行一对内存分配/释放操作。
  • Alrm : 对五个周期为1/2/3/5/7的闹钟进行一次处理的平均时间。

  Msgq和Bmq的区别在于前者只有接收方可以阻塞，后者双方都可以阻塞。

纪念性移植

芯片 架构 工具链 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

实用性移植

芯片 架构 工具链 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 虚拟化移植

  • V : 普通操作的虚拟化开销。
  • V/I : 中断操作的虚拟化开销。
芯片 架构 工具链 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

  作为对比，RT-Linux 4.12在Cortex-M7上的最好线程切换时间是25000时钟周期（它太大了以至于只能从FMC SDRAM来运行，所以这个对比事实上很不公平）。这是使用futex测得的；如使用其他IPC如管道等，则结果更差。

  以上实验均不包含任何作弊手段（比如激进的针对特定工具链的优化、不经过调度器而切换线程、使用平均情况较快但最坏执行时间不可控的调度器，甚至是使用RMS式的无栈协程切换），且在测试头文件中报告的最坏执行时间均为真实值。尽管我们为了更普遍地进行对比而在列出平均值，但对RTOS而言，最坏执行时间是唯一有意义的时间，因此一切有利于平均性能但不利于最坏执行时间的启发式优化都不适用。如果追求速度是最高目的，不可能有操作系统比RMS或DOS快，因为RMS的理论切换时间是0（所有协程均内联且只有一个状态时），而作为单任务操作系统的DOS则根本不存在切换时间。

明确不考虑支持的架构

架构 原因 替代方案
PIC18 硬件堆栈 使用RMS状态机操作系统
AVR32 正在消亡 使用大众化的Cortex-M和Cortex-R
x86-64 高级系统 使用RME微内核操作系统
Cortex-A 高级系统 使用RME微内核操作系统

  本RTOS主要面向资源受限的微控制器，不会提供对微处理器的支持。本项目也不考虑多核支持，因为多核微控制器很少是对称的，而且各核之间既无原子操作支持又无缓存一致性，即便RMP支持它们，其上的并行编程也极具挑战性。对于多核微控制器，推荐在每个核上起一个RMP实例，实例之间则可以用处理器间中断（Inter-Processor Interrupts，IPIs）互相通信。

新手上路

  下面的说明会帮助你在本地快速建立一个可用来评估测试本系统的工程。请参看系统的中文文档以获取更多信息。

准备工作

  要运行测试，你需要一块含有上述所列的微控制器的开发板。推荐使用 STM32 Nucleo 系列开发板或 MSP430 Launchpad 系列开发板。不要使用QEMU模拟器来测试本系统，因为QEMU有很多不完善之处，与真正的硬件行为并不一致。

  如果你没有开发板，那么RMP也有一个 基于x86处理器的Linux移植 。然而，该移植使用了ptrace系统调用和信号系统，因此性能较差，这一点可以从性能测试的数据看出。

  对于其他平台的支持应该也是容易实现的，但是当前并没有支持计划。对于那些Cortex-A和具备内存管理单元（MMU）的其他处理器，可以使用RME 实时多核心微内核；RME也支持一部分的Cortex-M和全部的Cortex-R。

编译指南

  在 Project 文件夹下能够找到各种微控制器的移植好的 Makefile 、 Keil 、 CCS 和 MPLAB 的工程样板。参看各个工程文件夹下的自述文件以获取更多关于如何编译和运行该工程的信息。某些工程需要额外的厂商硬件抽象层库的支持，它们可以在 M0A00_Library 软件仓库被找到。

运行测试

  要运行测试，只要将测试下载到对应的开发板并开始单步调试即可。某些例子会采用两个LED来指示系统当前的状态，此时要填充LED的点亮和熄灭函数来运行该示例。

  要使用本系统内建的图形库，请参考用户手册的相关章节。

生产部署

  当部署本系统到生产环境时，请仔细阅读本系统自带的手册，以确保各项配置正确。本系统的手册可以在 Document 文件夹下找到。

支持的工具链

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

  其他的工具链现在不推荐或者当前不受支持，虽然要增加新的支持应该也很简单。

参与项目

  请阅读CONTRIBUTING.md文档来获得关于行为规范和提交代码的相关信息。

EDI 工程信息

  • M5P01 R6T1

杰出贡献者

  • 宋磊锋 - ARM Cortex-M3/4/7 的GCC汇编支持。
  • 侯润升 - ARM Cortex-M4/7 的RVM支持，以及lwIP示例。
  • 王逸鹤 - 稳定的x86/linux/ptrace移植。
  • 张然 - C28x数字信号处理器移植。
  • 张凯 - 白盒测试用例。
  • 刘皓天 - RL78的移植。