Index: kernel/generic/src/synch/rcu.c
===================================================================
--- kernel/generic/src/synch/rcu.c	(revision 3648ea5631c84c0934c8fbba67ab15bc529f631c)
+++ kernel/generic/src/synch/rcu.c	(revision 09737cc97ffcee4a01bd7eaee34d72d7821ae8c6)
@@ -868,8 +868,8 @@
 				return false;			
 			}
-			
-			upd_missed_gp_in_wait(rcu.completed_gp);
 		}
 	}
+	
+	upd_missed_gp_in_wait(rcu.completed_gp);
 	
 	*completed_gp = rcu.completed_gp;
@@ -1126,5 +1126,6 @@
 	spinlock_unlock(&rcu.gp_lock);	
 	
-	upd_missed_gp_in_wait(*completed_gp);
+	if (!interrupted)
+		upd_missed_gp_in_wait(*completed_gp);
 	
 	return !interrupted;
@@ -1144,6 +1145,4 @@
 		interrupted = (ret == ESYNCH_INTERRUPTED);
 	}
-	
-	ASSERT(wait_on_gp <= rcu.completed_gp);
 	
 	return interrupted;