Index: kernel/arch/ia32/include/barrier.h
===================================================================
--- kernel/arch/ia32/include/barrier.h	(revision 933cadfdb63d0a16870db764880b5c144894e112)
+++ kernel/arch/ia32/include/barrier.h	(revision b678410d7e2eada8e2e3f65aaf7c4efc831777d6)
@@ -54,4 +54,5 @@
 NO_TRACE static inline void cpuid_serialization(void)
 {
+#ifndef __IN_SHARED_LIBC__
 	asm volatile (
 		"xorl %%eax, %%eax\n"
@@ -59,4 +60,14 @@
 		::: "eax", "ebx", "ecx", "edx", "memory"
 	);
+#else
+	/* Must not clobber PIC register ebx */
+	asm volatile (
+		"movl %%ebx, %%esi\n"
+		"xorl %%eax, %%eax\n"
+		"cpuid\n"
+		"movl %%esi, %%ebx\n"
+		::: "eax", "ecx", "edx", "esi", "memory"
+	);
+#endif
 }
 
Index: kernel/generic/include/syscall/syscall.h
===================================================================
--- kernel/generic/include/syscall/syscall.h	(revision 933cadfdb63d0a16870db764880b5c144894e112)
+++ kernel/generic/include/syscall/syscall.h	(revision b678410d7e2eada8e2e3f65aaf7c4efc831777d6)
@@ -90,4 +90,5 @@
 	SYS_SYSINFO_GET_DATA,
 	
+	SYS_DEBUG_PUTINT,
 	SYS_DEBUG_ENABLE_CONSOLE,
 	SYS_DEBUG_DISABLE_CONSOLE,
Index: kernel/generic/src/syscall/syscall.c
===================================================================
--- kernel/generic/src/syscall/syscall.c	(revision 933cadfdb63d0a16870db764880b5c144894e112)
+++ kernel/generic/src/syscall/syscall.c	(revision b678410d7e2eada8e2e3f65aaf7c4efc831777d6)
@@ -55,4 +55,11 @@
 #include <console/console.h>
 #include <udebug/udebug.h>
+
+/** Print a hex integer into klog */
+static sysarg_t sys_debug_putint(sysarg_t i)
+{
+	printf("[task:0x%x]", i);
+	return 0;
+}
 
 /** Dispatch system call */
@@ -180,4 +187,5 @@
 	
 	/* Debug calls */
+	(syshandler_t) sys_debug_putint,
 	(syshandler_t) sys_debug_enable_console,
 	(syshandler_t) sys_debug_disable_console
