Index: generic/src/main/main.c
===================================================================
--- generic/src/main/main.c	(revision 0132630e277cac256d68387347726af617f4270d)
+++ generic/src/main/main.c	(revision 96cacc151c2f49c7146a7f6e2384a276d4f1ffe3)
@@ -38,17 +38,9 @@
 #include <proc/task.h>
 #include <main/kinit.h>
+#include <main/version.h>
 #include <console/kconsole.h>
 #include <cpu.h>
 #include <align.h>
 #include <interrupt.h>
-#include <main/version.h>
-
-#ifdef CONFIG_SMP
-#include <arch/smp/apic.h>
-#include <arch/smp/mps.h>
-#endif /* CONFIG_SMP */
-
-#include <smp/smp.h>
-
 #include <arch/mm/memory_init.h>
 #include <mm/heap.h>
@@ -57,14 +49,18 @@
 #include <mm/tlb.h>
 #include <mm/vm.h>
-
 #include <synch/waitq.h>
-
 #include <arch/arch.h>
 #include <arch.h>
 #include <arch/faddr.h>
-
 #include <typedefs.h>
 
-config_t config;
+#ifdef CONFIG_SMP
+#include <arch/smp/apic.h>
+#include <arch/smp/mps.h>
+#endif /* CONFIG_SMP */
+#include <smp/smp.h>
+
+config_t config;	/**< Global configuration structure. */
+
 context_t ctx;
 
@@ -98,4 +94,6 @@
  *
  * Initializes the kernel by bootstrap CPU.
+ * This function passes control directly to
+ * main_bsp_separated_stack().
  *
  * Assuming interrupts_disable().
@@ -205,4 +203,5 @@
 		panic("can't create kinit thread\n");
 	thread_ready(t);
+
 	/*
 	 * This call to scheduler() will return to kinit,
@@ -219,4 +218,6 @@
  * Executed by application processors, temporary stack
  * is at ctx.sp which was set during BP boot.
+ * This function passes control directly to
+ * main_ap_separated_stack().
  *
  * Assuming interrupts_disable()'d.