diff --git a/src/kernel/core/arch/x86/arch_smp.c b/src/kernel/core/arch/x86/arch_smp.c
index 71164e2a07..b05df677f1 100755
--- a/src/kernel/core/arch/x86/arch_smp.c
+++ b/src/kernel/core/arch/x86/arch_smp.c
@@ -25,9 +25,9 @@
 
 
 static uint32 *apic = NULL;
-static uint32 cpu_apic_id[SMP_MAX_CPUS] = { 0, 0};
-static uint32 cpu_os_id[SMP_MAX_CPUS] = { 0, 0};
-static uint32 cpu_apic_version[SMP_MAX_CPUS] = { 0, 0};
+static uint32 cpu_apic_id[SMP_MAX_CPUS] = {0, 0};
+static uint32 cpu_os_id[SMP_MAX_CPUS] = {0, 0};
+static uint32 cpu_apic_version[SMP_MAX_CPUS] = {0, 0};
 static uint32 *ioapic = NULL;
 static uint32 apic_timer_tics_per_sec = 0;
 
@@ -74,15 +74,15 @@ i386_smp_error_interrupt(void *data)
 }
 
 
-static unsigned int
-apic_read(unsigned int *addr)
+static uint32
+apic_read(uint32 *addr)
 {
 	return *addr;
 }
 
 
 static void
-apic_write(unsigned int *addr, unsigned int data)
+apic_write(uint32 *addr, uint32 data)
 {
 	*addr = data;
 }
@@ -157,9 +157,9 @@ arch_smp_ack_interrupt(void)
 int
 arch_smp_set_apic_timer(bigtime_t relative_timeout)
 {
-	unsigned int config;
+	uint32 config;
+	uint32 ticks;
 	int state;
-	unsigned int ticks;
 
 	if (apic == NULL)
 		return -1;
diff --git a/src/kernel/core/smp.c b/src/kernel/core/smp.c
index 13b1218064..2d579dd954 100644
--- a/src/kernel/core/smp.c
+++ b/src/kernel/core/smp.c
@@ -359,7 +359,7 @@ smp_intercpu_int_handler(void)
 
 
 void
-smp_send_ici(int target_cpu, int message, unsigned long data, unsigned long data2, unsigned long data3, void *data_ptr, int flags)
+smp_send_ici(int target_cpu, int message, uint32 data, uint32 data2, uint32 data3, void *data_ptr, int flags)
 {
 	struct smp_msg *msg;
 
@@ -417,7 +417,7 @@ smp_send_ici(int target_cpu, int message, unsigned long data, unsigned long data
 
 
 void
-smp_send_broadcast_ici(int message, unsigned long data, unsigned long data2, unsigned long data3, void *data_ptr, int flags)
+smp_send_broadcast_ici(int message, uint32 data, uint32 data2, uint32 data3, void *data_ptr, int flags)
 {
 	struct smp_msg *msg;
 
@@ -505,8 +505,8 @@ smp_wait_for_ap_cpus(kernel_args *ka)
 	int retry;
 	do {
 		retry = 0;
-		for(i=1; i < ka->num_cpus; i++) {
-			if(boot_cpu_spin[i] != 1)
+		for (i = 1; i < ka->num_cpus; i++) {
+			if (boot_cpu_spin[i] != 1)
 				retry = 1;
 		}
 	} while (retry == 1);