diff --git a/platform/include/platform.h b/platform/include/platform.h
index 7d9445a8..598a43b1 100644
--- a/platform/include/platform.h
+++ b/platform/include/platform.h
@@ -7,8 +7,11 @@
  */
 #pragma once
 
-#include <sys/types.h>
 #include <lk/compiler.h>
+#include <sys/types.h>
+
+/* TODO: move all callers to using time.h directly */
+#include <platform/time.h>
 
 __BEGIN_CDECLS
 
@@ -32,9 +35,6 @@ typedef enum {
     HALT_REASON_SW_UPDATE,      // SW triggered reboot in order to begin firmware update
 } platform_halt_reason;
 
-lk_time_t current_time(void);
-lk_bigtime_t current_time_hires(void);
-
 /* super early platform initialization, before almost everything */
 void platform_early_init(void);
 
diff --git a/platform/include/platform/debug.h b/platform/include/platform/debug.h
index c03f999a..3f6449a8 100644
--- a/platform/include/platform/debug.h
+++ b/platform/include/platform/debug.h
@@ -7,17 +7,16 @@
  */
 #pragma once
 
-#include <sys/types.h>
-#include <stdbool.h>
-#include <stdarg.h>
 #include <lk/compiler.h>
+#include <stdbool.h>
 
 __BEGIN_CDECLS
 
+/* Standard console output routines that may be buffered */
 void platform_dputc(char c);
 int platform_dgetc(char *c, bool wait);
 
-// Should be available even if the system has panicked.
+/* Unbuffered versions of above, usually used a panic or crash time */
 void platform_pputc(char c);
 int platform_pgetc(char *c, bool wait);
 
diff --git a/platform/include/platform/interrupts.h b/platform/include/platform/interrupts.h
index 5d3c8b1f..ffcb990e 100644
--- a/platform/include/platform/interrupts.h
+++ b/platform/include/platform/interrupts.h
@@ -7,11 +7,21 @@
  */
 #pragma once
 
+#include <lk/compiler.h>
 #include <sys/types.h>
 
+__BEGIN_CDECLS
+
+/* Routines implemented by the platform or system specific interrupt controller
+ * to allow for installation and masking/unmask of interrupt vectors.
+ *
+ * Some platforms do not allow for dynamic registration.
+ */
 status_t mask_interrupt(unsigned int vector);
 status_t unmask_interrupt(unsigned int vector);
 
 typedef enum handler_return (*int_handler)(void *arg);
 
 void register_int_handler(unsigned int vector, int_handler handler, void *arg);
+
+__END_CDECLS
diff --git a/platform/include/platform/time.h b/platform/include/platform/time.h
new file mode 100644
index 00000000..84cea7de
--- /dev/null
+++ b/platform/include/platform/time.h
@@ -0,0 +1,26 @@
+/*
+ * Copyright (c) 2008 Travis Geiselbrecht
+ *
+ * Use of this source code is governed by a MIT-style
+ * license that can be found in the LICENSE file or at
+ * https://opensource.org/licenses/MIT
+ */
+#pragma once
+
+#include <lk/compiler.h>
+#include <sys/types.h>
+
+/* Routines to read the current system time since an arbitrary point in the
+ * past. Usually system boot time.
+ */
+
+__BEGIN_CDECLS
+
+/* Time in units of milliseconds */
+lk_time_t current_time(void);
+
+/* Time in units of microseconds */
+lk_bigtime_t current_time_hires(void);
+
+__END_CDECLS
+
diff --git a/platform/include/platform/timer.h b/platform/include/platform/timer.h
index 7e3d1d46..765cf6c3 100644
--- a/platform/include/platform/timer.h
+++ b/platform/include/platform/timer.h
@@ -7,14 +7,29 @@
  */
 #pragma once
 
+#include <lk/compiler.h>
 #include <sys/types.h>
 
+__BEGIN_CDECLS
+
+/* Routines the core kernel calls to set up and use hardware timer based callbacks at
+ * interrupt context.
+ *
+ * Most of the time this is handled in the platform layer but a few standalone timer
+ * implementations in other parts of the system may implement, depending on the
+ * configuration of the build.
+ */
+
 typedef enum handler_return (*platform_timer_callback)(void *arg, lk_time_t now);
 
+/* If the platform only supports a single monotonic (fixed rate) timer */
 status_t platform_set_periodic_timer(platform_timer_callback callback, void *arg, lk_time_t interval);
 
+/* If the platform implements a full dynamic (can be set to arbitary points in the future) timer */
 #if PLATFORM_HAS_DYNAMIC_TIMER
 status_t platform_set_oneshot_timer (platform_timer_callback callback, void *arg, lk_time_t interval);
 void     platform_stop_timer(void);
 #endif
 
+__END_CDECLS
+