There are countless real-time operating systems available with a wide array of features. There is a significant overlap between real-time operating systems and the Linux kernel, especially with the mainlining of the real-time patches. This picture is further complicated by implementations like RTKernel and Xenomai, which use the Linux kernel with an RTOS. There was also a μClinux variant of the Linux kernel targeting microcontrollers without an MMU that has mainlined in 2.x kernels. Some of the architectures it supported have since been dropped.
When selecting an implementation there are numerous considerations that are project dependent. Those may include code size, integration effort, determinism, latency, verifiability and safety. Often these factors are interdependent, which makes properly addressing the underlying project goal more challenging.
Most real-time operating systems use a task model in which logical and physical addresses are the same. Typically, Linux uses a process model where a MMU is used to map from a logical to a physical address. The process model provides more isolation and therefore safety and security, but does have some overhead. Some RTOS implementations use a Memory Protection Unit (MPU) to protect memory not being used by the running task, by generating a trap, which adds some safety and security.
Latency and power consumption can be dramatically improved by not using DRAM and instead just using SRAM or even just an L2 cache.
The Real-Time Linux project was focused on integrated solutions with mixed-criticality workloads rather than specialized applications. Often those applications require verifiability, which may be achieved using a mathematical proof of worst-case execution time. Currently, real-time Linux can not be fully validated. However on February, 21, 2019 the Linux Foundation launched the ELISA project to help build safety-critical systems based on Linux.1
An alternative is to use a hypervisor to split real-time and other applications into separate virtual machines. This is the goal of the Linux Foundation Project named Project ACRN. It supports one real-time virtual machine (e.g. Zephyr, VxWorks, Xenomai).
Note, there are existing and upcoming chip hardware updates that may improve access to shared resources to help improve determinism.
Formal verification uses mathematics to prove the correctness of a system relative to a formalized specification description. Typically this is done using model checking, which requires defining a model of the system in a formal language. Examples of model checkers include TLA+, SPIN and P.2 Alternatively, deductive verification can be used (e.g. Coq).
A Red Hat and ELISA developer began addressing runtime verification with a patchset in 2021.3 It verifies a running system by converting a model in the dot language into template code using the new dot2k tool. That template code will be hooked into the kernel at tracepoints.
Linux Plumbers Conference 2021 included a Kernel Dependability and Assurance Microconference.
There are competing interests between manufacturers of safety-oriented devices and fabricators of integrated circuits. This is exemplified by automobile manufactures who lost significant revenue due to a shortage of particular chips that often depend on legacy silicon manufacturing processes. New chip manufacturing is naturally focused on newer processes, which means the industry is especially slow at responding to increased demand of legacy chips.4
Two Red Hat developers presented on work being done to make Linux better suited for safety-critical applications. Their work consists of generating models based on updated kernel source code documentation and then adding an interface for runtime verification based on those models.5 They mentioned the Israeli autonomous driving company, Mobile Eye, which is supported by Intel.