- if ( rts_n_waiting_workers > 0 ) {
- IF_DEBUG(scheduler,
- fprintf(stderr,"worker thread (%p): giving up RTS token\n", osThreadId()));
- releaseCapability(*pCap);
- /* And wait for work */
- waitForWorkCapability(pMutex, pCap, pThreadCond);
- IF_DEBUG(scheduler,
- fprintf(stderr,"worker thread (%p): got back RTS token (after yieldToReturningWorker)\n",
- osThreadId()));
- }
- return;
+ // Pre-condition: pMutex is assumed held, the current thread
+ // holds the capability pointed to by pCap.
+
+ if ( rts_n_waiting_workers > 0 || passingCapability ) {
+ IF_DEBUG(scheduler, sched_belch("worker: giving up capability"));
+ releaseCapability(*pCap);
+ *pCap = NULL;
+ }
+
+ // Post-condition: pMutex is assumed held, and either:
+ //
+ // 1. *pCap is NULL, in which case the current thread does not
+ // hold a capability now, or
+ // 2. *pCap is not NULL, in which case the current thread still
+ // holds the capability.
+ //
+ return;