--- /home/dario/Desktop/sched_rt.c	2016-03-04 15:47:14.901787122 +0100
+++ xen/common/sched_rt.c	2016-03-04 16:55:06.746641424 +0100
@@ -439,6 +439,8 @@
     struct list_head *replq = rt_replq(ops);
     struct timer* repl_timer = prv->repl_timer;
 
+    ASSERT( __vcpu_on_replq(svc) );
+
     /*
      * Disarm the timer before re-programming it.
      * It doesn't matter if the vcpu to be removed
@@ -580,7 +582,7 @@
 }
 
 static void
-rt_deinit(const struct scheduler *ops)
+rt_deinit(struct scheduler *ops)
 {
     struct rt_private *prv = rt_priv(ops);
 
@@ -1153,6 +1155,7 @@
 {
     struct rt_vcpu * const svc = rt_vcpu(vc);
     s_time_t now = NOW();
+    bool_t missed;
 
     BUG_ON( is_idle_vcpu(vc) );
 
@@ -1181,28 +1184,42 @@
 
     /*
      * If a deadline passed while svc was asleep/blocked, we need new
-     * scheduling parameters ( a new deadline and full budget), and
-     * also a new replenishment event
+     * scheduling parameters (a new deadline and full budget).
      */
-    if ( now >= svc->cur_deadline)
-    {   
+    if ( (missed = now >= svc->cur_deadline) )
         rt_update_deadline(now, svc);
-        __replq_remove(ops, svc);
-    }
-
-   // if( !__vcpu_on_replq(svc) )
-        __replq_insert(ops, svc);
 
-    /* If context hasn't been saved for this vcpu yet, we can't put it on
-     * the Runqueue/DepletedQ. Instead, we set a flag so that it will be
-     * put on the Runqueue/DepletedQ after the context has been saved.
+    /* 
+     * If context hasn't been saved for this vcpu yet, we can't put it on
+     * the run-queue/depleted-queue. Instead, we set the appropriate flag,
+     * it the vcpu will be put back on queue after the context has been saved
+     * (in rt_context_save()).
      */
     if ( unlikely(svc->flags & RTDS_scheduled) )
     {
+        printk("vcpu%d woken while still in scheduling tail\n", vc->vcpu_id);
         set_bit(__RTDS_delayed_runq_add, &svc->flags);
+        /*
+         * The vcpu is waking up already, and we didn't even had the time to
+         * remove its next replenishment event from the replenishment queue
+         * when he blocked! No big deal. If we did not miss the deadline in
+         * the meantime, let's just leave it there. If we did, let's remove it
+         * and queue a new one (to occur at our new deadline).
+         */
+        if ( missed )
+        {
+           // XXX You may want to implement something like replq_reinsert(),
+           //     for dealing with this case, and calling that one from here
+           //     (of course!). I'd do that by merging _remove and _insert
+           //     and killing the duplicated bits.
+           __replq_remove(ops, svc); 
+           __replq_insert(ops, svc); 
+        }
         return;
     }
 
+    /* Replenishment event got cancelled when we blocked. Add it back. */
+    __replq_insert(ops, svc); 
     /* insert svc to runq/depletedq because svc is not in queue now */
     __runq_insert(ops, svc);