Comment by snvzz

Great debugging effort.

Now, with the complexity (MLoCs!) of the Linux kernel, this is definitely not the only bug to be found in there.

This is why Linux is just an interim kernel for these use cases in which we still cannot use seL4[0].

0. https://sel4.systems/