Comment by snvzz
That is not too surprising.
Linux is still Linux, and having Linux as a whole be preemptable by a separate RTOS kernel is always going to perform better in the realtime front, relative to trusting Linux to satisfy realtime for the user tasks it runs.
Incidentally, seL4[0] can pull off that trick, and do it even better: It can support mixed criticality (MCS), where hard realtime is guaranteed by proofs despite less important tasks, such as a Linux kernel under VMM, running on the same system.