Scheduling in smp configuration

In the case of multiple cores, is the scheduling of each core judged according to the
kscurdomain, that is, the scheduling table of the domain is maintained by an operating
system, rather than an independent kscurdomain in a core and a scheduling table of the
domain in each core?
And those data structures referring to scheduling ,are they global instances or instances per core?

In the case of multiple cores, the value of KernelNumDomains must be 1. A configuration with multiple domains and multiple cores is currently unsupported and would produce a build time error or automatically switch off SMP support during reconfiguration.

There is a proposed PR to support this functionality here Domain scheduler multicore support by Furao · Pull Request #691 · seL4/seL4 · GitHub which isn’t ready for merging yet. The intention is for ksCurDomain to be a global variable that’s the same on all cores and the domain schedule is the same on all cores. Each core has its own per-domain scheduling queue but always schedules threads from the ksCurDomain domain. Switching domains would likely be synchronized across all cores - but this is something that still needs to be discussed and added to any pending PRs.

Therefore, in the current seL4, if I want to configure multi-core, I can only have one domain, and each core has its corresponding kscurthread, ksscheduler action and ready queues

The multi-core and multi domain mechanism has not been implemented yet. If it is implemented, it should share a kscurdomain between multiple cores. Is my understanding correct?

I’m sorry, my understanding of English is not very good. Please point out my misunderstanding.

Each core has its own kscurthread, ksSchedulerAction, ksReadyQueues and ksIdleThread. Any variable in the kernel declared with NODE_STATE_DECLARE() within the NODE_STATE_BEGIN(nodeState) block has a per-core instance.

The multi-core and multi domain mechanism has not been implemented in mainline yet. If it is implemented it is likely that ksCurDomain will be shared between multiple cores but this isn’t confirmed yet and may end up being implemented differently.

Your understanding seems correct to me.

Thank you so much! It’s very helpful to me!