Hello Li, On 2023-05-30 05:06, yadong.li wrote:

I have one question about sel4 kernel preemptionPoint on smp platform such as ARMv8. Take an example, when kernel takes long time to clear memory when UntypedRetype kernel object on core1, it will check preemptionPoint, when pending IRQ exists on core1, it will handle this irq, and return to userspace let other syscall or cores such as core2 have chance to run, but irq pending only check current cpu(PerCPU), no all cores of smp system, if core1 execute long seL4_Untyped_Retype syscall, core2 has a pending irq, the pending irq will not be checked in current core1, it will block until the execution of long syscall is completed if we take no account of archtimer irq, This phenomenon looks inconsistent at the system level between signal core and mutil core

This seems an oversight in preemptionPoint() and a bug, I opened a new issue on github for this: https://github.com/seL4/seL4/issues/1054 Thanks for reporting this!

I want to know the current design intent about preemptionPoint of archtimer interrupt and other peripheral interrupts on SMP platform, only take current core interrupt as soon as possible or give other core and high priority task a chance to entry kernel and take big kernel lock?

I think this code predates SMP support and wasn't updated when SMP support was added. Logically the system WCET should be the single core WCET multiplied by the number of cpu cores. With that in mind, other cores should get a chance to take the lock. Taking the interrupt first or later does not matter for WCET, but it does for interrupt latency, and taking the interrupt was already delayed by a long running kernel action, so I would say handling the interrupt first would be better. Greetings, Indan