X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Fdevices%2Ftimer.c;h=ecf6c5aacdfee97c6577c8b60912475ef99e4e77;hb=64f0952217e8b1a53461f5a98a070cb2da266171;hp=8f47c810ffc8af5a1c6804933fad710929450318;hpb=34a1a2cf11500505e74ae5796e88de0d8de00958;p=pintos-anon

diff --git a/src/devices/timer.c b/src/devices/timer.c
index 8f47c81..ecf6c5a 100644
--- a/src/devices/timer.c
+++ b/src/devices/timer.c
@@ -7,6 +7,8 @@
 #include "threads/io.h"
 #include "threads/thread.h"
   
+/* See [8254] for hardware details of the 8254 timer chip. */
+
 #if TIMER_FREQ < 19
 #error 8254 timer requires TIMER_FREQ >= 19
 #endif
@@ -64,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. */
@@ -98,7 +100,7 @@ timer_ns2ticks (int64_t ns)
 void
 timer_print_stats (void) 
 {
-  printf ("Timer: %"PRId64" ticks.\n", ticks);
+  printf ("Timer: %"PRId64" ticks\n", ticks);
 }
 
 /* Timer interrupt handler. */