Index: kernel/arch/ia64/src/ia64.c
===================================================================
--- kernel/arch/ia64/src/ia64.c	(revision df4ed852a2d1b242f9bdce0a873009a2cb77cec7)
+++ kernel/arch/ia64/src/ia64.c	(revision 6f4495f5c6915097f277fabc29a874343f77e88a)
@@ -134,5 +134,5 @@
 	psr.bn = 1;				/* start in bank 0 */
 
-	__asm__ volatile ("mov %0 = ar.rsc\n" : "=r" (rsc.value));
+	asm volatile ("mov %0 = ar.rsc\n" : "=r" (rsc.value));
 	rsc.loadrs = 0;
 	rsc.be = false;
Index: kernel/arch/ia64/src/mm/tlb.c
===================================================================
--- kernel/arch/ia64/src/mm/tlb.c	(revision df4ed852a2d1b242f9bdce0a873009a2cb77cec7)
+++ kernel/arch/ia64/src/mm/tlb.c	(revision 6f4495f5c6915097f277fabc29a874343f77e88a)
@@ -73,5 +73,5 @@
 	for(i = 0; i < count1; i++) {
 		for(j = 0; j < count2; j++) {
-			__asm__ volatile (
+			asm volatile (
 				"ptc.e %0 ;;"
 				:
@@ -180,5 +180,5 @@
 	/*cnt+=(page!=va);*/
 	for(; va<(page+cnt*(PAGE_SIZE)); va += (1<<ps))	{
-		__asm__ volatile (
+		asm volatile (
 			"ptc.l %0,%1;;"
 			:
@@ -245,5 +245,5 @@
 	}
 	
-	__asm__ volatile (
+	asm volatile (
 		"mov r8=psr;;\n"
 		"rsm %0;;\n"   			/* PSR_IC_MASK */
@@ -321,5 +321,5 @@
 	}
 
-	__asm__ volatile (
+	asm volatile (
 		"mov r8=psr;;\n"
 		"rsm %0;;\n"			/* PSR_IC_MASK */
@@ -383,5 +383,5 @@
 void dtr_purge(uintptr_t page, count_t width)
 {
-	__asm__ volatile ("ptr.d %0, %1\n" : : "r" (page), "r" (width<<2));
+	asm volatile ("ptr.d %0, %1\n" : : "r" (page), "r" (width<<2));
 }
 
Index: kernel/arch/ia64/src/proc/scheduler.c
===================================================================
--- kernel/arch/ia64/src/proc/scheduler.c	(revision df4ed852a2d1b242f9bdce0a873009a2cb77cec7)
+++ kernel/arch/ia64/src/proc/scheduler.c	(revision 6f4495f5c6915097f277fabc29a874343f77e88a)
@@ -74,5 +74,5 @@
 	 * These values will be found there after switch from userspace.
 	 */
-	__asm__ volatile (
+	asm volatile (
 		"bsw.0\n"
 		"mov r22 = %0\n"
Index: kernel/arch/ia64/src/ski/ski.c
===================================================================
--- kernel/arch/ia64/src/ski/ski.c	(revision df4ed852a2d1b242f9bdce0a873009a2cb77cec7)
+++ kernel/arch/ia64/src/ski/ski.c	(revision 6f4495f5c6915097f277fabc29a874343f77e88a)
@@ -70,5 +70,5 @@
 void ski_putchar(chardev_t *d, const char ch)
 {
-	__asm__ volatile (
+	asm volatile (
 		"mov r15 = %0\n"
 		"mov r32 = %1\n"	/* r32 is in0 */
@@ -96,5 +96,5 @@
 	uint64_t ch;
 	
-	__asm__ volatile (
+	asm volatile (
 		"mov r15 = %1\n"
 		"break 0x80000;;\n"	/* modifies r8 */
@@ -205,5 +205,5 @@
 void ski_init_console(void)
 {
-	__asm__ volatile (
+	asm volatile (
 		"mov r15 = %0\n"
 		"break 0x80000\n"
