microkit_pd_stop()/microkit_pd_resume() behavior

[joep]

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.

[midnightveil]

Yes.

1. Fix approach used for making PDs passive at run-time #91 (specifically lazy rebind in init) will fix the double rebind issue.

2. Yes, seL4_Resume() on passive threads seL4#1582. It's possible that we could do better for documentation here. I don't know how we'd fix this properly. The issue is that getting a passive thread back to the blocked-on-recv state is impossible without giving it a temporary scheduling context. You can use the cap-mapping (<cspace> and <cap_tcb> <cap_sc>) features to mimic this yourself.

[joep]

Yeah, I agree there really doesn't seem to be a good fix given the underlying conditions. Our own fix is simply not doing suspend/resume on passive PDs. Control-C in the debugger doesn't stop every PD immediately since any passive PDs will continue to process a notification until they block again. This is non-optimal but it's the way it is. This does require us to do passive/non-passive bookkeeping. That same bookkeeping is also done by the Monitor, so I suppose it might be relocated into the microkit library and the library handle it for both. But that adds more complexity to the microkit correctness argument for not much gain, so I think just documenting it is probably the right thing.

[Indanz]

You have to make the thread active prior to resuming it, so it can at least run until it becomes passive in the right state again. If the TCB has a SC bound to its bound notification, then assign that to the TCB before resuming the task, it will be automatically unbound when the task does the next blocking call (lazy unbind).

MCS doesn't really interact with suspend/resume very well, it's easy to lose track of the SC. E.g. a thread doing a call to a passive server will donate its SC. I'm not sure what will happen if you suspend that task while it's waiting for a reply, it may never gets its original SC back. I think on suspend the IPC will be cancelled and the reply chain broken, but without returning the SC (that would have effectively suspended the thread currently using it too). Unlike for passive servers, for clients you don't know what state they are and can't fix or avoid this situation.

seL4_TCB_Suspend is not a good tool for debug suspend, as it changes task state too much.