Hello Yadong, I guess this is a side effect of delivering maintenance interrupts and virtual timer interrupts as VCPU faults on SMP systems. It is not ideal since the VCPU on core 1 should not be blocked until the VMM thread on core0 handles the interrupt. Can you create an issue on seL4 github? Alternatively, I am happy to create and track the issue if you are OK with that. Thanks for reporting this. Regards, Yanyan From: yadong.limailto:yadong.li@horizon.ai Sent: Friday, 6 August 2021 6:32 PM To: devel@sel4.systemsmailto:devel@sel4.systems Subject: [seL4] some unexpected phenomenon about scheduling Hi: Recently, I found some unexpected phenomenon about scheduling on our project. My environment as follows: I run linux guest on seL4, Linux guest has 8 vcpu on 8 Arm PE from core0 ~ core7. WFI is not trap, seL4 is master kernel not mcs kernel I think seL4 idle task will not be run on core1, it will always run vcpu task. But the truth is the idle task will be run. I found when the maintenance and timer interrupt of Linux guest came, it will switch to idle, Because above interrupts handle will call handleFault, the sendIPC will set the ksCurThread(vcpu task) block on send, and the ksReadyQueuesL1Bitmap is empty. The idle task wille be run. But the recv task maybe run on core0, now core1 is in idle, is it reasonable? Thank you very much _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems