Index: kernel/generic/include/synch/spinlock.h
===================================================================
--- kernel/generic/include/synch/spinlock.h	(revision b24786a3475ffcd354ab3fd707a7bb77ce9fa0d7)
+++ kernel/generic/include/synch/spinlock.h	(revision ff3b7da7acb81fa6d9a3a13f7c7f96b11b4cb59d)
@@ -37,4 +37,5 @@
 
 #include <arch/types.h>
+#include <arch/barrier.h>
 #include <preemption.h>
 #include <atomic.h>
Index: kernel/generic/src/mm/tlb.c
===================================================================
--- kernel/generic/src/mm/tlb.c	(revision b24786a3475ffcd354ab3fd707a7bb77ce9fa0d7)
+++ kernel/generic/src/mm/tlb.c	(revision ff3b7da7acb81fa6d9a3a13f7c7f96b11b4cb59d)
@@ -135,5 +135,7 @@
 void tlb_shootdown_ipi_send(void)
 {
+#ifndef ia64
 	ipi_broadcast(VECTOR_TLB_SHOOTDOWN_IPI);
+#endif	
 }
 
Index: kernel/generic/src/proc/thread.c
===================================================================
--- kernel/generic/src/proc/thread.c	(revision b24786a3475ffcd354ab3fd707a7bb77ce9fa0d7)
+++ kernel/generic/src/proc/thread.c	(revision ff3b7da7acb81fa6d9a3a13f7c7f96b11b4cb59d)
@@ -296,5 +296,4 @@
 	if (!t)
 		return NULL;
-	
 	/* Not needed, but good for debugging */
 	memsetb(t->kstack, THREAD_STACK_SIZE * 1 << STACK_FRAMES, 0);