From: Ben Pfaff <blp@cs.stanford.edu>
Date: Sat, 11 Sep 2004 23:27:29 +0000 (+0000)
Subject: Do console locking.
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=e45f3adbd21cd675c38b1d29394ec60b9cec2e33;hp=404ff9b49909b1648cef613e66d2c54a345e72ad;p=pintos-anon

Do console locking.
Rename printf.c to console.c to better explain its function.
Move puts() from lib to lib/{user,kernel} so it can take console lock.
---

diff --git a/src/lib/kernel/console.c b/src/lib/kernel/console.c
new file mode 100644
index 0000000..7ce9cbf
--- /dev/null
+++ b/src/lib/kernel/console.c
@@ -0,0 +1,93 @@
+#include <stdarg.h>
+#include <stdio.h>
+#include "devices/serial.h"
+#include "devices/vga.h"
+#include "threads/interrupt.h"
+#include "threads/synch.h"
+
+static void vprintf_helper (char, void *);
+static void putchar_unlocked (uint8_t c);
+
+/* The console lock.
+   Both the vga and serial layers do their own locking, so it's
+   safe to call them at any time.
+   But this lock is useful to prevent simultaneous printf() calls
+   from mixing their output, which looks confusing. */
+static struct lock console_lock;
+
+void
+console_init (void) 
+{
+  lock_init (&console_lock, "console");
+}
+
+/* The standard vprintf() function,
+   which is like printf() but uses a va_list.
+   Writes its output to both vga display and serial port. */
+int
+vprintf (const char *format, va_list args) 
+{
+  int char_cnt = 0;
+
+  if (!intr_context ())
+    lock_acquire (&console_lock);
+
+  __vprintf (format, args, vprintf_helper, &char_cnt);
+
+  if (!intr_context ())
+    lock_release (&console_lock);
+
+  return char_cnt;
+}
+
+/* Writes string S to the console, followed by a new-line
+   character. */
+int
+puts (const char *s) 
+{
+  if (!intr_context ())
+    lock_acquire (&console_lock);
+
+  while (*s != '\0')
+    putchar_unlocked (*s++);
+  putchar_unlocked ('\n');
+
+  if (!intr_context ())
+    lock_release (&console_lock);
+
+  return 0;
+}
+
+/* Writes C to the vga display and serial port. */
+int
+putchar (int c) 
+{
+  if (!intr_context ())
+    lock_acquire (&console_lock);
+
+  putchar_unlocked (c);
+
+  if (!intr_context ())
+    lock_release (&console_lock);
+
+  return c;
+}
+
+/* Helper function for vprintf(). */
+static void
+vprintf_helper (char c, void *char_cnt_) 
+{
+  int *char_cnt = char_cnt_;
+  (*char_cnt)++;
+  putchar_unlocked (c);
+}
+
+/* Writes C to the vga display and serial port.
+   The caller has already acquired the console lock if
+   appropriate. */
+static void
+putchar_unlocked (uint8_t c) 
+{
+  serial_putc (c);
+  vga_putc (c);
+}
diff --git a/src/lib/kernel/console.h b/src/lib/kernel/console.h
new file mode 100644
index 0000000..6e5b41b
--- /dev/null
+++ b/src/lib/kernel/console.h
@@ -0,0 +1,6 @@
+#ifndef __LIB_KERNEL_CONSOLE_H
+#define __LIB_KERNEL_CONSOLE_H
+
+void console_init (void);
+
+#endif /* lib/kernel/console.h */
diff --git a/src/lib/kernel/printf.c b/src/lib/kernel/printf.c
deleted file mode 100644
index c139966..0000000
--- a/src/lib/kernel/printf.c
+++ /dev/null
@@ -1,41 +0,0 @@
-#include <stdarg.h>
-#include <stdio.h>
-#include "devices/serial.h"
-#include "devices/vga.h"
-#include "threads/interrupt.h"
-
-static void vprintf_helper (char, void *);
-
-/* The standard vprintf() function,
-   which is like printf() but uses a va_list.
-   Writes its output to both vga display and serial port. */
-int
-vprintf (const char *format, va_list args) 
-{
-  enum intr_level old_level;
-  int char_cnt = 0;
-
-  old_level = intr_disable ();
-  __vprintf (format, args, vprintf_helper, &char_cnt);
-  intr_set_level (old_level);
-
-  return char_cnt;
-}
-
-/* Helper function for vprintf(). */
-static void
-vprintf_helper (char c, void *char_cnt_) 
-{
-  int *char_cnt = char_cnt_;
-  (*char_cnt)++;
-  putchar (c);
-}
-
-/* Writes C to the vga display and serial port. */
-int
-putchar (int c) 
-{
-  serial_putc (c);
-  vga_putc (c);
-  return c;
-}
diff --git a/src/lib/stdio.c b/src/lib/stdio.c
index 95dfdbe..d223d10 100644
--- a/src/lib/stdio.c
+++ b/src/lib/stdio.c
@@ -552,17 +552,6 @@ __printf (const char *format,
   __vprintf (format, args, output, aux);
   va_end (args);
 }
-
-/* Writes string S to the console, followed by a new-line
-   character. */
-int
-puts (const char *s) 
-{
-  while (*s != '\0')
-    putchar (*s++);
-  putchar ('\n');
-  return 0;
-}
 
 /* Dumps the SIZE bytes in BUFFER to the console as hex bytes
    arranged 16 per line.  If ASCII is true then the corresponding
diff --git a/src/lib/user/console.c b/src/lib/user/console.c
new file mode 100644
index 0000000..709a5c8
--- /dev/null
+++ b/src/lib/user/console.c
@@ -0,0 +1,63 @@
+#include <stdio.h>
+#include <syscall.h>
+#include <syscall-nr.h>
+
+static void vprintf_helper (char, void *);
+
+/* Auxiliary data for vprintf_helper(). */
+struct vprintf_aux 
+  {
+    char buf[64];       /* Character buffer. */
+    char *p;            /* Current position in buffer. */
+    int char_cnt;       /* Total characters written so far. */
+  };
+
+/* The standard vprintf() function,
+   which is like printf() but uses a va_list.
+   Writes its output to the STDOUT_FILENO handle. */
+int
+vprintf (const char *format, va_list args) 
+{
+  struct vprintf_aux aux;
+  aux.p = aux.buf;
+  aux.char_cnt = 0;
+  __vprintf (format, args, vprintf_helper, &aux);
+  if (aux.p > aux.buf)
+    write (STDOUT_FILENO, aux.buf, aux.p - aux.buf);
+  return aux.char_cnt;
+}
+
+/* Helper function for vprintf(). */
+static void
+vprintf_helper (char c, void *aux_) 
+{
+  struct vprintf_aux *aux = aux_;
+  *aux->p++ = c;
+  if (aux->p >= aux->buf + sizeof aux->buf)
+    {
+      write (STDOUT_FILENO, aux->buf, aux->p - aux->buf);
+      aux->p = aux->buf;
+    }
+  aux->char_cnt++;
+}
+
+/* Writes string S to the console, followed by a new-line
+   character. */
+int
+puts (const char *s) 
+{
+  while (*s != '\0')
+    putchar (*s++);
+  putchar ('\n');
+
+  return 0;
+}
+
+/* Writes C to the console. */
+int
+putchar (int c) 
+{
+  char c2 = c;
+  write (STDOUT_FILENO, &c2, 1);
+  return c;
+}
diff --git a/src/lib/user/printf.c b/src/lib/user/printf.c
deleted file mode 100644
index 6466e54..0000000
--- a/src/lib/user/printf.c
+++ /dev/null
@@ -1,51 +0,0 @@
-#include <stdio.h>
-#include <syscall.h>
-#include <syscall-nr.h>
-
-static void vprintf_helper (char, void *);
-
-/* Auxiliary data for vprintf_helper(). */
-struct vprintf_aux 
-  {
-    char buf[64];       /* Character buffer. */
-    char *p;            /* Current position in buffer. */
-    int char_cnt;       /* Total characters written so far. */
-  };
-
-/* The standard vprintf() function,
-   which is like printf() but uses a va_list.
-   Writes its output to the STDOUT_FILENO handle. */
-int
-vprintf (const char *format, va_list args) 
-{
-  struct vprintf_aux aux;
-  aux.p = aux.buf;
-  aux.char_cnt = 0;
-  __vprintf (format, args, vprintf_helper, &aux);
-  if (aux.p > aux.buf)
-    write (STDOUT_FILENO, aux.buf, aux.p - aux.buf);
-  return aux.char_cnt;
-}
-
-/* Helper function for vprintf(). */
-static void
-vprintf_helper (char c, void *aux_) 
-{
-  struct vprintf_aux *aux = aux_;
-  *aux->p++ = c;
-  if (aux->p >= aux->buf + sizeof aux->buf)
-    {
-      write (STDOUT_FILENO, aux->buf, aux->p - aux->buf);
-      aux->p = aux->buf;
-    }
-  aux->char_cnt++;
-}
-
-/* Writes C to the console. */
-int
-putchar (int c) 
-{
-  char c2 = c;
-  write (STDOUT_FILENO, &c2, 1);
-  return c;
-}