[seL4] Re: Question on TCB without SC in receiveSignal

OK, thanks Indan. ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

[seL4] Re: Question on TCB without SC in receiveSignal

Thanks Indan for your detail reply. By ready queue, I did mean the scheduling queue since the code named it as ksReadyQueues. For threads unbound from a SC, this thread will be removed from both ksReadyQueues and ksReleaseHead according the code below: void schedContext_unbindTCB(sched_context_t

[seL4] Re: Question on TCB without SC in receiveSignal

Hi Indan, I come back again. It confused me that Chapter 6.1.7 Passive Threads of seL4-manual-latest.pdf said: Threads can be unbound from a scheduling context with seL4_SchedContext_UnbindObject().This is distinct from suspending a thread, in that threads that are blocked waiting in an endpoi

[seL4] Re: Question on TCB without SC in receiveSignal

Thanks Indan. I'll try to have some debugging to fullly understand what you said. Thanks a lot. ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

[seL4] Re: Question on TCB without SC in receiveSignal

Thanks Indan for you patient and professional answer. I read your reply more than 10 times, ^_^. Still one thing to confirm: Threads which are blocked waiting for notification/endpoint without schedule context will remain in the ready queue, right? __

[seL4] Question on TCB without SC in receiveSignal

Hello guys, I got confused on the implementation of receiveSignal in sel4 with MCS. When the notification status is NtfnState_Active, the kernel will try to donate the notification's schedule context to the thread by calling maybeDonateSchedContext. My confusion point is that: If the thread does

[seL4] Re: How to avoid priority inversion in seL4

Thanks Gernot for the quick response. Your answer confirms my understanding. Thanks a lot. ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

[seL4] How to avoid priority inversion in seL4

Hello experts, I'm reading the code of seL4 kernel, but I got confused how seL4 could help to avoid priority inversion. seL4 itself doesn't change the priority of TCB at the kernel level, does it mean that seL4 leaves the user level to handle priority inversion? Regards Neil.

[seL4] Re: Where are the interrupts disabled in the kernel mode?

Thanks Indan. Your tips help to clear out my confusion. Thanks. ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

[seL4] Re: Where are the interrupts disabled in the kernel mode?

Hi Indan, Thanks a lot for your quick reply. And will interrupts be enabled again automatically after exiting trapping? (Is this done automatically by the CPU? So invisible from the source code.) ___ Devel mailing list -- devel@sel4.systems To unsubscri

[seL4] Where are the interrupts disabled in the kernel mode?

Hi experts, The sel4 whitepaper says "seL4, like most members of the L4 microkernel family, executes with interrupts disabled while in kernel mode.". But I didn't find the code which disabled interrupts when entering kernel mode, for example, when a syscall is triggered. Can anybody help to po

[seL4] Re: Bug on sel4 rootserver?

Hi Chris, Your tips help a lot. The issue was resolved by using your trick. Thanks a lot! Regards Neil. ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

[seL4] Bug on sel4 rootserver?

Hello guys, I'm trying to run sel4 using qemu under macosx, but it looks crash happened(Same steps were done on Ubuntu, but nothing bad happened.). More info: I'm following the doc here with docker as the build environment: https://docs.sel4.systems/GettingStarted.html Any tips are appreciated.

[seL4] How to enable SMP on qemu-arm-virt

Hello cool guys, I'm trying SEL4 using qemu-arm-virt platform with command： ../init-build.sh -DPLATFORM=qemu-arm-virt -DSIMULATION=true I noticed that SMP was not enabled by default, so I added: set(KernelMaxNumNodes "4") into kernel\src\plat\qemu-arm-virt\config.cmake. After running it with com