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 endpoint or notification queue will remain in the queue and can still recieve messages and signals. However, the unbound thread will not be schedulable again until it receives a scheduling context. Threads without scheduling contexts are referred to as passive threads, as they cannot execute without the action of another thread. By saying " threads that are blocked waiting in an endpoint or notification queue will remain in the queue and can still recieve messages and signals.", does it mean that those threads blocked waiting in an endpoint or notification queue will remain in the READY QUEUE? Or maybe the manual was not accurate?