microkit_pd_stop()/microkit_pd_resume() behavior

Start by reviewing the microkit_pd_stop()/microkit_pd_resume() wrappers and Monitor's passive-PD request handling, then compare them with seL4_TCB_Suspend/seL4_TCB_Resume semantics. Check both the schedContext-less TCB case and replayed requests while a passive transition is pending. Done should be an agreed behavior with corresponding handling or documentation.

seL4's seL4_TCB_Suspend/seL4_TCB_Resume (which are invoked by the thin microkit wrappers) implicitly assumes a normal case: an SC bound to the TCB that is being suspended. From our reading of the kernel source:

• suspend() unconditionally dequeues the thread and sets ThreadState_Inactive, with no special handling for a notification-bound SC.
• restart() sets ThreadState_Restart, but only actually reschedules the thread if isSchedulable() — which requires tcbSchedContext != NULL.

The result is that a passive PD (tcbSchedContext==NULL) remains permanently unrunnable.

From the kernel perspective, given its overall minimalist philosophy, this seems like reasonable behavior: a TCB and its SC are just two independent objects that just happen to usually be bound together and the result is well-defined in either case. [I would suggest, however, that seL4_TCB_Resume's manual/spec document the schedContext-less-TCB case, where success is returned but the thread is never again scheduled.]

Whether this is desirable behavior from microkit's perspective I think could be reasonably argued either way. But passive PDs are microkit abstractions so it definitively involves, at a minimum, a gap in the documentation. Using microkit_pd_stop()/microkit_pd_resume() is unsafe once Monitor has made the PD passive. The passive PD will never be scheduled to run again, yet no error is ever indicated.

I will add here that there can be a secondary issue. If the timing is right, a seL4_TCB_Suspend may hit a passive PD during its 'Please make me passive' request to the Monitor. If the request has been sent but has not been responded to yet (i.e., the passive PD is in blocked waiting on the reply) and a seL4_TCB_Resume is issued to the passive PD, then seL4 semantics are to replay the entire system call. This results in a second message being sent to the Monitor. Monitor handles both messages unconditionally by attempting to do a seL4_SchedContext_Bind. The second message results in seL4 issuing a TCB already bound error message, and microkit also issuing a "MON|ERROR: could not bind scheduling context to notification object" message.