diff --git a/Makefile b/Makefile
index 894000b7e5356dfed67fb9d0153547ba48da1a35..e0485c71cb02ab6dd3b0ec738e14c4b6c99062d8 100644
--- a/Makefile
+++ b/Makefile
@@ -15,7 +15,7 @@
 ### Build parameters
 ############################################################
 
-ARCH_LIST:=arm ia32
+ARCH_LIST:=arm x86
 CPU_LIST:=arm1136jf-s ixp420 cortex-a8 cortex-a9 cortex-a15
 PLAT_LIST:=imx31 pc99 ixp420 omap3 am335x exynos4 exynos5 imx6 apq8064 zynq7000 allwinnerA20
 ARMV_LIST:=armv6 armv7-a
@@ -29,7 +29,7 @@ endif
 # we don't ARCH or PLAT for the style target, but other 
 # targets fail -- so just bluff.
 ifeq (${MAKECMDGOALS}, style)
-ARCH:=ia32
+ARCH:=x86
 PLAT:=pc99
 endif
 
diff --git a/include/arch/ia32/arch/Makefile b/include/arch/x86/arch/Makefile
similarity index 100%
rename from include/arch/ia32/arch/Makefile
rename to include/arch/x86/arch/Makefile
diff --git a/include/arch/ia32/arch/api/objecttype.h b/include/arch/x86/arch/api/objecttype.h
similarity index 100%
rename from include/arch/ia32/arch/api/objecttype.h
rename to include/arch/x86/arch/api/objecttype.h
diff --git a/include/arch/ia32/arch/api/types.h b/include/arch/x86/arch/api/types.h
similarity index 100%
rename from include/arch/ia32/arch/api/types.h
rename to include/arch/x86/arch/api/types.h
diff --git a/include/arch/ia32/arch/benchmark.h b/include/arch/x86/arch/benchmark.h
similarity index 100%
rename from include/arch/ia32/arch/benchmark.h
rename to include/arch/x86/arch/benchmark.h
diff --git a/include/arch/ia32/arch/fastpath/fastpath.h b/include/arch/x86/arch/fastpath/fastpath.h
similarity index 100%
rename from include/arch/ia32/arch/fastpath/fastpath.h
rename to include/arch/x86/arch/fastpath/fastpath.h
diff --git a/include/arch/ia32/arch/kernel/apic.h b/include/arch/x86/arch/kernel/apic.h
similarity index 100%
rename from include/arch/ia32/arch/kernel/apic.h
rename to include/arch/x86/arch/kernel/apic.h
diff --git a/include/arch/ia32/arch/kernel/boot.h b/include/arch/x86/arch/kernel/boot.h
similarity index 100%
rename from include/arch/ia32/arch/kernel/boot.h
rename to include/arch/x86/arch/kernel/boot.h
diff --git a/include/arch/ia32/arch/kernel/boot_sys.h b/include/arch/x86/arch/kernel/boot_sys.h
similarity index 100%
rename from include/arch/ia32/arch/kernel/boot_sys.h
rename to include/arch/x86/arch/kernel/boot_sys.h
diff --git a/include/arch/ia32/arch/kernel/cmdline.h b/include/arch/x86/arch/kernel/cmdline.h
similarity index 100%
rename from include/arch/ia32/arch/kernel/cmdline.h
rename to include/arch/x86/arch/kernel/cmdline.h
diff --git a/include/arch/ia32/arch/kernel/elf.h b/include/arch/x86/arch/kernel/elf.h
similarity index 100%
rename from include/arch/ia32/arch/kernel/elf.h
rename to include/arch/x86/arch/kernel/elf.h
diff --git a/include/arch/ia32/arch/kernel/lock.h b/include/arch/x86/arch/kernel/lock.h
similarity index 100%
rename from include/arch/ia32/arch/kernel/lock.h
rename to include/arch/x86/arch/kernel/lock.h
diff --git a/include/arch/ia32/arch/kernel/multiboot.h b/include/arch/x86/arch/kernel/multiboot.h
similarity index 100%
rename from include/arch/ia32/arch/kernel/multiboot.h
rename to include/arch/x86/arch/kernel/multiboot.h
diff --git a/include/arch/ia32/arch/kernel/thread.h b/include/arch/x86/arch/kernel/thread.h
similarity index 100%
rename from include/arch/ia32/arch/kernel/thread.h
rename to include/arch/x86/arch/kernel/thread.h
diff --git a/include/arch/ia32/arch/kernel/vspace.h b/include/arch/x86/arch/kernel/vspace.h
similarity index 100%
rename from include/arch/ia32/arch/kernel/vspace.h
rename to include/arch/x86/arch/kernel/vspace.h
diff --git a/include/arch/ia32/arch/linker.h b/include/arch/x86/arch/linker.h
similarity index 100%
rename from include/arch/ia32/arch/linker.h
rename to include/arch/x86/arch/linker.h
diff --git a/include/arch/ia32/arch/machine.h b/include/arch/x86/arch/machine.h
similarity index 100%
rename from include/arch/ia32/arch/machine.h
rename to include/arch/x86/arch/machine.h
diff --git a/include/arch/ia32/arch/machine/capdl.h b/include/arch/x86/arch/machine/capdl.h
similarity index 100%
rename from include/arch/ia32/arch/machine/capdl.h
rename to include/arch/x86/arch/machine/capdl.h
diff --git a/include/arch/ia32/arch/machine/cpu_registers.h b/include/arch/x86/arch/machine/cpu_registers.h
similarity index 100%
rename from include/arch/ia32/arch/machine/cpu_registers.h
rename to include/arch/x86/arch/machine/cpu_registers.h
diff --git a/include/arch/ia32/arch/machine/fpu.h b/include/arch/x86/arch/machine/fpu.h
similarity index 100%
rename from include/arch/ia32/arch/machine/fpu.h
rename to include/arch/x86/arch/machine/fpu.h
diff --git a/include/arch/ia32/arch/machine/hardware.h b/include/arch/x86/arch/machine/hardware.h
similarity index 100%
rename from include/arch/ia32/arch/machine/hardware.h
rename to include/arch/x86/arch/machine/hardware.h
diff --git a/include/arch/ia32/arch/machine/pat.h b/include/arch/x86/arch/machine/pat.h
similarity index 100%
rename from include/arch/ia32/arch/machine/pat.h
rename to include/arch/x86/arch/machine/pat.h
diff --git a/include/arch/ia32/arch/machine/registerset.h b/include/arch/x86/arch/machine/registerset.h
similarity index 100%
rename from include/arch/ia32/arch/machine/registerset.h
rename to include/arch/x86/arch/machine/registerset.h
diff --git a/include/arch/ia32/arch/model/statedata.h b/include/arch/x86/arch/model/statedata.h
similarity index 100%
rename from include/arch/ia32/arch/model/statedata.h
rename to include/arch/x86/arch/model/statedata.h
diff --git a/include/arch/ia32/arch/object/Makefile b/include/arch/x86/arch/object/Makefile
similarity index 100%
rename from include/arch/ia32/arch/object/Makefile
rename to include/arch/x86/arch/object/Makefile
diff --git a/include/arch/ia32/arch/object/interrupt.h b/include/arch/x86/arch/object/interrupt.h
similarity index 100%
rename from include/arch/ia32/arch/object/interrupt.h
rename to include/arch/x86/arch/object/interrupt.h
diff --git a/include/arch/ia32/arch/object/ioport.h b/include/arch/x86/arch/object/ioport.h
similarity index 100%
rename from include/arch/ia32/arch/object/ioport.h
rename to include/arch/x86/arch/object/ioport.h
diff --git a/include/arch/ia32/arch/object/iospace.h b/include/arch/x86/arch/object/iospace.h
similarity index 100%
rename from include/arch/ia32/arch/object/iospace.h
rename to include/arch/x86/arch/object/iospace.h
diff --git a/include/arch/ia32/arch/object/objecttype.h b/include/arch/x86/arch/object/objecttype.h
similarity index 100%
rename from include/arch/ia32/arch/object/objecttype.h
rename to include/arch/x86/arch/object/objecttype.h
diff --git a/include/arch/ia32/arch/object/structures.bf b/include/arch/x86/arch/object/structures.bf
similarity index 100%
rename from include/arch/ia32/arch/object/structures.bf
rename to include/arch/x86/arch/object/structures.bf
diff --git a/include/arch/ia32/arch/object/structures.h b/include/arch/x86/arch/object/structures.h
similarity index 100%
rename from include/arch/ia32/arch/object/structures.h
rename to include/arch/x86/arch/object/structures.h
diff --git a/include/arch/ia32/arch/object/tcb.h b/include/arch/x86/arch/object/tcb.h
similarity index 100%
rename from include/arch/ia32/arch/object/tcb.h
rename to include/arch/x86/arch/object/tcb.h
diff --git a/include/arch/ia32/arch/stdint.h b/include/arch/x86/arch/stdint.h
similarity index 100%
rename from include/arch/ia32/arch/stdint.h
rename to include/arch/x86/arch/stdint.h
diff --git a/include/arch/ia32/arch/types.h b/include/arch/x86/arch/types.h
similarity index 100%
rename from include/arch/ia32/arch/types.h
rename to include/arch/x86/arch/types.h
diff --git a/libsel4/arch_include/ia32/interfaces/sel4arch.xml b/libsel4/arch_include/x86/interfaces/sel4arch.xml
similarity index 100%
rename from libsel4/arch_include/ia32/interfaces/sel4arch.xml
rename to libsel4/arch_include/x86/interfaces/sel4arch.xml
diff --git a/libsel4/arch_include/ia32/sel4/arch/constants.h b/libsel4/arch_include/x86/sel4/arch/constants.h
similarity index 100%
rename from libsel4/arch_include/ia32/sel4/arch/constants.h
rename to libsel4/arch_include/x86/sel4/arch/constants.h
diff --git a/libsel4/arch_include/ia32/sel4/arch/exIPC.h b/libsel4/arch_include/x86/sel4/arch/exIPC.h
similarity index 100%
rename from libsel4/arch_include/ia32/sel4/arch/exIPC.h
rename to libsel4/arch_include/x86/sel4/arch/exIPC.h
diff --git a/libsel4/arch_include/ia32/sel4/arch/functions.h b/libsel4/arch_include/x86/sel4/arch/functions.h
similarity index 100%
rename from libsel4/arch_include/ia32/sel4/arch/functions.h
rename to libsel4/arch_include/x86/sel4/arch/functions.h
diff --git a/libsel4/arch_include/ia32/sel4/arch/objecttype.h b/libsel4/arch_include/x86/sel4/arch/objecttype.h
similarity index 100%
rename from libsel4/arch_include/ia32/sel4/arch/objecttype.h
rename to libsel4/arch_include/x86/sel4/arch/objecttype.h
diff --git a/libsel4/arch_include/ia32/sel4/arch/pfIPC.h b/libsel4/arch_include/x86/sel4/arch/pfIPC.h
similarity index 100%
rename from libsel4/arch_include/ia32/sel4/arch/pfIPC.h
rename to libsel4/arch_include/x86/sel4/arch/pfIPC.h
diff --git a/libsel4/arch_include/ia32/sel4/arch/syscalls.h b/libsel4/arch_include/x86/sel4/arch/syscalls.h
similarity index 100%
rename from libsel4/arch_include/ia32/sel4/arch/syscalls.h
rename to libsel4/arch_include/x86/sel4/arch/syscalls.h
diff --git a/libsel4/arch_include/ia32/sel4/arch/types.h b/libsel4/arch_include/x86/sel4/arch/types.h
similarity index 100%
rename from libsel4/arch_include/ia32/sel4/arch/types.h
rename to libsel4/arch_include/x86/sel4/arch/types.h
diff --git a/libsel4/tools/syscall_stub_gen.py b/libsel4/tools/syscall_stub_gen.py
index 944030a2eb068664e5b3b333a3d3840ccd41ac9a..4b9ce221c313cf752045f9a55a60a64285cfa386 100644
--- a/libsel4/tools/syscall_stub_gen.py
+++ b/libsel4/tools/syscall_stub_gen.py
@@ -58,7 +58,7 @@ MAX_MESSAGE_LENGTH = 32
 
 MESSAGE_REGISTERS_FOR_ARCH = {
     "arm": 4,
-    "ia32": 2,
+    "x86": 2,
 }
 
 class Type(object):
@@ -220,7 +220,7 @@ arch_types = {
         StructType("seL4_UserContext", WORD_SIZE_BITS * 17),
         ],
 
-    "ia32" : [
+    "x86" : [
         Type("seL4_IA32_VMAttributes", WORD_SIZE_BITS),
         CapType("seL4_IA32_ASIDControl"),
         CapType("seL4_IA32_ASIDPool"),
diff --git a/src/arch/ia32/Makefile b/src/arch/x86/Makefile
similarity index 100%
rename from src/arch/ia32/Makefile
rename to src/arch/x86/Makefile
diff --git a/src/arch/ia32/api/Makefile b/src/arch/x86/api/Makefile
similarity index 100%
rename from src/arch/ia32/api/Makefile
rename to src/arch/x86/api/Makefile
diff --git a/src/arch/ia32/api/benchmark.c b/src/arch/x86/api/benchmark.c
similarity index 100%
rename from src/arch/ia32/api/benchmark.c
rename to src/arch/x86/api/benchmark.c
diff --git a/src/arch/ia32/api/faults.c b/src/arch/x86/api/faults.c
similarity index 100%
rename from src/arch/ia32/api/faults.c
rename to src/arch/x86/api/faults.c
diff --git a/src/arch/ia32/c_traps.c b/src/arch/x86/c_traps.c
similarity index 100%
rename from src/arch/ia32/c_traps.c
rename to src/arch/x86/c_traps.c
diff --git a/src/arch/ia32/fastpath/Makefile b/src/arch/x86/fastpath/Makefile
similarity index 100%
rename from src/arch/ia32/fastpath/Makefile
rename to src/arch/x86/fastpath/Makefile
diff --git a/src/arch/ia32/fastpath/fastpath.c b/src/arch/x86/fastpath/fastpath.c
similarity index 100%
rename from src/arch/ia32/fastpath/fastpath.c
rename to src/arch/x86/fastpath/fastpath.c
diff --git a/src/arch/ia32/halt.S b/src/arch/x86/halt.S
similarity index 100%
rename from src/arch/ia32/halt.S
rename to src/arch/x86/halt.S
diff --git a/src/arch/ia32/head.S b/src/arch/x86/head.S
similarity index 100%
rename from src/arch/ia32/head.S
rename to src/arch/x86/head.S
diff --git a/src/arch/ia32/idle.S b/src/arch/x86/idle.S
similarity index 100%
rename from src/arch/ia32/idle.S
rename to src/arch/x86/idle.S
diff --git a/src/arch/ia32/kernel/Makefile b/src/arch/x86/kernel/Makefile
similarity index 100%
rename from src/arch/ia32/kernel/Makefile
rename to src/arch/x86/kernel/Makefile
diff --git a/src/arch/ia32/kernel/apic.c b/src/arch/x86/kernel/apic.c
similarity index 100%
rename from src/arch/ia32/kernel/apic.c
rename to src/arch/x86/kernel/apic.c
diff --git a/src/arch/ia32/kernel/boot.c b/src/arch/x86/kernel/boot.c
similarity index 100%
rename from src/arch/ia32/kernel/boot.c
rename to src/arch/x86/kernel/boot.c
diff --git a/src/arch/ia32/kernel/boot_sys.c b/src/arch/x86/kernel/boot_sys.c
similarity index 100%
rename from src/arch/ia32/kernel/boot_sys.c
rename to src/arch/x86/kernel/boot_sys.c
diff --git a/src/arch/ia32/kernel/cmdline.c b/src/arch/x86/kernel/cmdline.c
similarity index 100%
rename from src/arch/ia32/kernel/cmdline.c
rename to src/arch/x86/kernel/cmdline.c
diff --git a/src/arch/ia32/kernel/elf.c b/src/arch/x86/kernel/elf.c
similarity index 100%
rename from src/arch/ia32/kernel/elf.c
rename to src/arch/x86/kernel/elf.c
diff --git a/src/arch/ia32/kernel/lock.c b/src/arch/x86/kernel/lock.c
similarity index 100%
rename from src/arch/ia32/kernel/lock.c
rename to src/arch/x86/kernel/lock.c
diff --git a/src/arch/ia32/kernel/thread.c b/src/arch/x86/kernel/thread.c
similarity index 100%
rename from src/arch/ia32/kernel/thread.c
rename to src/arch/x86/kernel/thread.c
diff --git a/src/arch/ia32/kernel/vspace.c b/src/arch/x86/kernel/vspace.c
similarity index 100%
rename from src/arch/ia32/kernel/vspace.c
rename to src/arch/x86/kernel/vspace.c
diff --git a/src/arch/ia32/kernel/vspace_32.c b/src/arch/x86/kernel/vspace_32.c
similarity index 100%
rename from src/arch/ia32/kernel/vspace_32.c
rename to src/arch/x86/kernel/vspace_32.c
diff --git a/src/arch/ia32/kernel/vspace_pae.c b/src/arch/x86/kernel/vspace_pae.c
similarity index 100%
rename from src/arch/ia32/kernel/vspace_pae.c
rename to src/arch/x86/kernel/vspace_pae.c
diff --git a/src/arch/ia32/machine/Makefile b/src/arch/x86/machine/Makefile
similarity index 100%
rename from src/arch/ia32/machine/Makefile
rename to src/arch/x86/machine/Makefile
diff --git a/src/arch/ia32/machine/capdl.c b/src/arch/x86/machine/capdl.c
similarity index 100%
rename from src/arch/ia32/machine/capdl.c
rename to src/arch/x86/machine/capdl.c
diff --git a/src/arch/ia32/machine/fpu.c b/src/arch/x86/machine/fpu.c
similarity index 100%
rename from src/arch/ia32/machine/fpu.c
rename to src/arch/x86/machine/fpu.c
diff --git a/src/arch/ia32/machine/hardware.c b/src/arch/x86/machine/hardware.c
similarity index 100%
rename from src/arch/ia32/machine/hardware.c
rename to src/arch/x86/machine/hardware.c
diff --git a/src/arch/ia32/machine/registerset.c b/src/arch/x86/machine/registerset.c
similarity index 100%
rename from src/arch/ia32/machine/registerset.c
rename to src/arch/x86/machine/registerset.c
diff --git a/src/arch/ia32/machine_asm.S b/src/arch/x86/machine_asm.S
similarity index 100%
rename from src/arch/ia32/machine_asm.S
rename to src/arch/x86/machine_asm.S
diff --git a/src/arch/ia32/model/Makefile b/src/arch/x86/model/Makefile
similarity index 100%
rename from src/arch/ia32/model/Makefile
rename to src/arch/x86/model/Makefile
diff --git a/src/arch/ia32/model/statedata.c b/src/arch/x86/model/statedata.c
similarity index 100%
rename from src/arch/ia32/model/statedata.c
rename to src/arch/x86/model/statedata.c
diff --git a/src/arch/ia32/object/Makefile b/src/arch/x86/object/Makefile
similarity index 100%
rename from src/arch/ia32/object/Makefile
rename to src/arch/x86/object/Makefile
diff --git a/src/arch/ia32/object/interrupt.c b/src/arch/x86/object/interrupt.c
similarity index 100%
rename from src/arch/ia32/object/interrupt.c
rename to src/arch/x86/object/interrupt.c
diff --git a/src/arch/ia32/object/ioport.c b/src/arch/x86/object/ioport.c
similarity index 100%
rename from src/arch/ia32/object/ioport.c
rename to src/arch/x86/object/ioport.c
diff --git a/src/arch/ia32/object/iospace.c b/src/arch/x86/object/iospace.c
similarity index 100%
rename from src/arch/ia32/object/iospace.c
rename to src/arch/x86/object/iospace.c
diff --git a/src/arch/ia32/object/objecttype.c b/src/arch/x86/object/objecttype.c
similarity index 100%
rename from src/arch/ia32/object/objecttype.c
rename to src/arch/x86/object/objecttype.c
diff --git a/src/arch/ia32/object/tcb.c b/src/arch/x86/object/tcb.c
similarity index 100%
rename from src/arch/ia32/object/tcb.c
rename to src/arch/x86/object/tcb.c
diff --git a/src/arch/ia32/traps.S b/src/arch/x86/traps.S
similarity index 100%
rename from src/arch/ia32/traps.S
rename to src/arch/x86/traps.S