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
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems
