void burn_credits(struct csched2_runqueue_data *rqd, struct csched2_vcpu *svc, s_time_t now)
{
    s_time_t delta;

    delta = now - svc->start_time;

    if ( delta > 0 ) {
        SCHED_STAT_CRANK(burn_credits_t2c);
        t2c_update(rqd, delta, svc);
        svc->start_time = now;
    }
    else
    {
        printk(XENLOG_WARNING "%s: Time went backwards? "
               "now %"PRI_stime" start_time %"PRI_stime"\n",
               __func__, now, svc->start_time);




(XEN) [  129.126370] burn_credits: Time went backwards? now 129126357182 start_time 129126357659
(XEN) [  129.590457] burn_credits: Time went backwards? now 129590442023 start_time 129590442953
(XEN) [  129.590461] burn_credits: Time went backwards? now 129590442023 start_time 129590442953
(XEN) [  129.590466] burn_credits: Time went backwards? now 129590442023 start_time 129590442953
(XEN) [  130.254463] burn_credits: Time went backwards? now 130254450552 start_time 130254451068
(XEN) [  131.158537] burn_credits: Time went backwards? now 131158524688 start_time 131158524750