Hi:
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
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?
Thanks for your help
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems
