Hi

I mainly want to know how threads is scheduled in SMP configuration. Is there any documents or manuals on SMP configuration?

Basically each thread is bound to a core and each core runs its own round robin scheduler with priority queues (assuming MCS is not used). Threads can be moved from one core to another manually using seL4_TCB_SetAffinity(). There is no global scheduling and load management in the kernel. Some details can be found at https://docs.sel4.systems/Tutorials/threads.html and Kent explained some seL4 internals in his answers at https://sel4.discourse.group/t/scheduling-in-smp-configuration/503 I'm not sure what information you are missing, would be nice if you could ask a more specific question. We can use this to extend the documentation. Axel