diff --git a/src/kernel/core/arch/x86/arch_cpu.c b/src/kernel/core/arch/x86/arch_cpu.c
index 244bca685e..39a7c2943c 100755
--- a/src/kernel/core/arch/x86/arch_cpu.c
+++ b/src/kernel/core/arch/x86/arch_cpu.c
@@ -14,7 +14,7 @@
 #include <kerrors.h>
 #include <tls.h>
 
-#include <stage2.h>
+#include <boot/stage2.h>
 
 #include <string.h>
 #include <stdio.h>
diff --git a/src/kernel/core/arch/x86/arch_dbg_console.c b/src/kernel/core/arch/x86/arch_dbg_console.c
index b456b129a8..ed5f4c281f 100755
--- a/src/kernel/core/arch/x86/arch_dbg_console.c
+++ b/src/kernel/core/arch/x86/arch_dbg_console.c
@@ -11,7 +11,7 @@
 #include <arch/cpu.h>
 #include <arch/dbg_console.h>
 
-#include <stage2.h>
+#include <boot/stage2.h>
 
 #include <string.h>
 
diff --git a/src/kernel/core/arch/x86/arch_faults.c b/src/kernel/core/arch/x86/arch_faults.c
index be1f62f96a..385e8519ab 100755
--- a/src/kernel/core/arch/x86/arch_faults.c
+++ b/src/kernel/core/arch/x86/arch_faults.c
@@ -17,7 +17,7 @@
 #include <arch/x86/interrupts.h>
 #include <arch/x86/faults.h>
 
-#include <stage2.h>
+#include <boot/stage2.h>
 
 #include <string.h>
 
diff --git a/src/kernel/core/arch/x86/arch_int.c b/src/kernel/core/arch/x86/arch_int.c
index 18f1b0e5b3..25a2fdb889 100755
--- a/src/kernel/core/arch/x86/arch_int.c
+++ b/src/kernel/core/arch/x86/arch_int.c
@@ -26,7 +26,7 @@
 #include <arch/x86/faults.h>
 #include <arch/x86/descriptors.h>
 
-#include <stage2.h>
+#include <boot/stage2.h>
 
 #include <string.h>
 
diff --git a/src/kernel/core/arch/x86/arch_smp.c b/src/kernel/core/arch/x86/arch_smp.c
index d0f4d0c9bc..ad9f03e607 100755
--- a/src/kernel/core/arch/x86/arch_smp.c
+++ b/src/kernel/core/arch/x86/arch_smp.c
@@ -3,7 +3,7 @@
 ** Distributed under the terms of the NewOS License.
 */
 
-#include <stage2.h>
+#include <boot/stage2.h>
 #include <kernel.h>
 #include <console.h>
 #include <debug.h>
diff --git a/src/kernel/core/arch/x86/arch_thread.c b/src/kernel/core/arch/x86/arch_thread.c
index b038710056..e449f41efc 100755
--- a/src/kernel/core/arch/x86/arch_thread.c
+++ b/src/kernel/core/arch/x86/arch_thread.c
@@ -4,7 +4,7 @@
 */
 
 #include <kernel.h>
-#include <stage2.h>
+#include <boot/stage2.h>
 #include <debug.h>
 #include <vm.h>
 #include <memheap.h>
diff --git a/src/kernel/core/arch/x86/arch_timer.c b/src/kernel/core/arch/x86/arch_timer.c
index 527ec033b9..1487cd91b0 100755
--- a/src/kernel/core/arch/x86/arch_timer.c
+++ b/src/kernel/core/arch/x86/arch_timer.c
@@ -3,7 +3,7 @@
 ** Distributed under the terms of the NewOS License.
 */
 
-#include <stage2.h>
+#include <boot/stage2.h>
 #include <kernel.h>
 
 #include <arch/int.h>
@@ -23,7 +23,9 @@
 #define pit_clock_rate 1193180
 #define pit_max_timer_interval ((long long)0xffff * 1000000 / pit_clock_rate)
 
-static void set_isa_hardware_timer(long long relative_timeout)
+
+static void
+set_isa_hardware_timer(long long relative_timeout)
 {
 	unsigned short next_event_clocks;
 
@@ -39,37 +41,47 @@ static void set_isa_hardware_timer(long long relative_timeout)
 	out8((next_event_clocks >> 8) & 0xff, 0x40);
 }
 
-static void clear_isa_hardware_timer()
+
+static void
+clear_isa_hardware_timer(void)
 {
 	// XXX do something here
 }
 
-static int32 isa_timer_interrupt(void* data)
+
+static int32
+isa_timer_interrupt(void *data)
 {
 	return timer_interrupt();
 }
 
-int apic_timer_interrupt()
+
+int
+apic_timer_interrupt(void)
 {
 	return timer_interrupt();
 }
 
-void arch_timer_set_hardware_timer(bigtime_t timeout)
+
+void
+arch_timer_set_hardware_timer(bigtime_t timeout)
 {
 	// try the apic timer first
-	if(arch_smp_set_apic_timer(timeout) < 0) {
+	if (arch_smp_set_apic_timer(timeout) < 0)
 		set_isa_hardware_timer(timeout);
-	}
 }
 
-void arch_timer_clear_hardware_timer()
+
+void
+arch_timer_clear_hardware_timer(void)
 {
-	if(arch_smp_clear_apic_timer() < 0) {
+	if (arch_smp_clear_apic_timer() < 0)
 		clear_isa_hardware_timer();
-	}
 }
 
-int arch_init_timer(kernel_args *ka)
+
+int
+arch_init_timer(kernel_args *ka)
 {
 	dprintf("arch_init_timer: entry\n");
 	
@@ -78,3 +90,4 @@ int arch_init_timer(kernel_args *ka)
 
 	return 0;
 }
+
diff --git a/src/kernel/core/arch/x86/arch_vm_translation_map.c b/src/kernel/core/arch/x86/arch_vm_translation_map.c
index 1f08fb782d..398ca4547d 100755
--- a/src/kernel/core/arch/x86/arch_vm_translation_map.c
+++ b/src/kernel/core/arch/x86/arch_vm_translation_map.c
@@ -15,7 +15,7 @@
 #include <OS.h>
 #include <queue.h>
 #include <string.h>
-#include <stage2.h>
+#include <boot/stage2.h>
 #include <Errors.h>
 #include <kerrors.h>