Just a nitpic, Linux can run on CPUs without MMUs, and it has APIs for locking memory and real time scheduling but that's not why it is not a hard-realtime OS.
Yes you are correct. I am currently having a project, making Linux "as real-time as possible": locking memory with mlockall, isolating cores, preempt kernel patch, .... It is still not real-time because you have no guarantees, but you typically get a max jitter of 0.1 ms, which is good enough for my use case.
You could use Linux without a MMU (uClinux), e.g. on a Cortex-M, but is a horribly experience and no standard program works.
Preempt RT does give guarantees in the sense that unbounded latency is a bug and theoretical maximum latency bounds are known (see [0]). It is neither certifiable nor formally proven, but it's good enough for almost anything that isn't safety-critical. For the things that do require functional safety, you can use AGL and other hypervisor architectures that partition the critical and non-critical tasks with a few more changes to your code.
Preempt RT doesn't really give that. It might give that when you run a subset of Linux, but that is not Linux like nommu Linux is not Linux. They might say that's a bug, but there are countless algorithms and data structures in Linux that mean the state of the system and other workloads can slow down other parts of the system. Even setting aside the fact that a lower privileged process can take spin locks (not "preempt spinlocks" but real low level spin locks), disable interrupts, etc., they can influence shared data structures such that allocations, lookups, etc can take longer for the higher privileged thread. So you still end up with a "look we tried really hard and if you don't use any kernel facilities including blocking and isolate this CPU entirely, lock everything and don't allocate memory or take page faults after that, you might get something approaching hard-realtime".
People try to paint it as soft-hard-RT or something, but it's not, there already exists a good word for it which is soft-RT. Which is fine, it's highly useful.
There aren't really formally proven hard realtime operating systems of any non-trivial complexity are there? They are either extremely simple executive layers, or some very limited privileged functionality that sits on top of the rest of the kernel.
I'd highly recommend you read the link and the paper it's based on. It's pretty thorough in addressing the limitations. Those same limitations apply to virtually every commercial RTOS out there as well though.
As for formally verified systems, depends on your definition of "nontrivial". You can build complex systems from the building blocks provided by the well known examples like SeL4 and pikeos. On a practical level though, complete formal verification is incredibly uncommon for exactly the reasons you'd expect. There's usually a mix of formal methods and other verification methods employed in safety critical applications. It's "good enough" given current capabilities.
I did read it. I understand and work on Linux including real time Linux. Nothing of what I said is wrong. Hard realtime operating systems of course are more limited than general purpose Linux too, but they tend to have a much better handle on limiting and controlling latency and how non-critical workload can impact critical tasks.
And seL4 is formally verified but as far as I know it has not been formally verified for hard realtime. Funny thing about formal verification is that it's easy to do if you control the requirements :) (/s - nothing to take away from the incredible work of sel4). Last I heard people had sketched or theorized about ways it could be approached, but not done.
Very interesting. Thanks for the link to the paper. Isn't the provided paper "just" about the scheduler? Eventually, I would have to output some data, e.g. on the CAN bus with socketcan through the network stack. This is probably a huge amount of code for which worst-case-execution-times are probably hard to get.
Does AGL mean automotive grade linux? What would be other hypervisors?
The time it takes to put things on a physical bus will depend on your hardware and can be bounded, but this isn't the guarantee you're getting from any RTOS.
The main thing the "RT" in RTOS guarantees is that the OS will return control back to you in a defined amount of time as soon as you're ready to run. You're still responsible for ensuring all of the other system requirements for bounded latency are fulfilled, like hardware that doesn't introduce unbounded latencies the OS can't control (surprisingly difficult with modern HW). Assuming you've done all of that, preempt-rt will give you essentially the same guarantees because of the scheduler work linked.
