timer_sleep() need interrupts on.

[pintos-anon] / src / devices / timer.c

diff --git a/src/devices/timer.c b/src/devices/timer.c
index ec9778321e3339aa2f32bb5496ece5e71a5ea969..ecf6c5aacdfee97c6577c8b60912475ef99e4e77 100644 (file)
--- a/src/devices/timer.c
+++ b/src/devices/timer.c
@@ -66,9 +66,9 @@ timer_sleep (int64_t ticks)
 {
   int64_t start = timer_ticks ();
 
+  ASSERT (intr_get_level () == INTR_ON);
   while (timer_elapsed (start) < ticks) 
-    if (intr_get_level () == INTR_ON)
-      thread_yield ();
+    thread_yield ();
 }
 
 /* Returns MS milliseconds in timer ticks, rounding up. */