Hi Alexander, > Following patch seems to fix the issue. Can you please have a look and > verify that it is correct ? Or should it be solved on another place in > the kernel differently.
Yes, the patch is correct and definitely fixes a bug. Thanks! Would you like me to apply this directly or will you raise a PR? In order to not cause unneccessary headaches for verification, I would undo the convert to switch and leave the statement as an if. > Just out of curiosity, why is a separate thread state in the scheduler > for x86 (CONFIG_VFX) required that is not needed for scheduling of a > vCPU on ARM ? I didn't expect the scheduler thread states to be > different between hardware architectures in seL4. seL4's x86 and ARM virtualisation architectures are indeed different. On x86, we use one kernel thread for both guest and host, and use the thread state to differentiate what is currently running. On ARM, guest and host run in different kernel threads so this isn't required. Cheers, Anna. _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
