On Fri, Nov 9, 2018 at 6:10 AM <Anna.Lyons@data61.csiro.au> wrote:
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.

Out of interest, what's the reason for the different approaches?