barrelfish-master/kernel/schedule_rbed.c

80 static struct dcb *lastdisp = NULL;
304     if(lastdisp != NULL) {
305         assert(lastdisp->last_dispatch <= now);
306         if(lastdisp->release_time <= now) {
307             lastdisp->etime += now -
308                 MAX(lastdisp->last_dispatch, lastdisp->release_time);
344         lastdisp = NULL;
377         if(lastdisp == todisp && dcb_current != NULL && in_queue(dcb_current)) {
387         lastdisp = todisp;
421     lastdisp = NULL;
567     lastdisp = NULL;    // Don't account for us anymore
589     lastdisp = NULL;