diff --git a/include/arch/x86/arch/32/mode/machine.h b/include/arch/x86/arch/32/mode/machine.h
index bc3d7f48c..0461f40cc 100644
--- a/include/arch/x86/arch/32/mode/machine.h
+++ b/include/arch/x86/arch/32/mode/machine.h
@@ -65,6 +65,13 @@ static inline void setCurrentPD(paddr_t addr)
     write_cr3(addr);
 }
 
+static inline void setCurrentVSpaceRoot(paddr_t addr, word_t pcid)
+{
+    /* pcid is not supported on ia32 and so we should always be passed zero */
+    assert(pcid == 0);
+    setCurrentPD(addr);
+}
+
 static inline void invalidateTLBEntry(vptr_t vptr)
 {
     asm volatile("invlpg (%[vptr])" :: [vptr] "r"(vptr));
@@ -146,4 +153,9 @@ static inline void x86_write_gs_base(word_t base)
 void ia32_load_fs(word_t selector);
 void ia32_load_gs(word_t selector);
 
+static inline void init_syscall_msrs(void)
+{
+    fail("syscall not supported on ia32");
+}
+
 #endif
diff --git a/include/arch/x86/arch/machine/hardware.h b/include/arch/x86/arch/machine/hardware.h
index 02cc0abee..a77f979bf 100644
--- a/include/arch/x86/arch/machine/hardware.h
+++ b/include/arch/x86/arch/machine/hardware.h
@@ -24,7 +24,8 @@ typedef word_t vm_fault_type_t;
 
 enum vm_page_size {
     X86_SmallPage,
-    X86_LargePage
+    X86_LargePage,
+    X64_HugePage
 };
 typedef word_t vm_page_size_t;
 
@@ -47,6 +48,9 @@ pageBitsForSize(vm_page_size_t pagesize)
     case X86_LargePage:
         return seL4_LargePageBits;
 
+    case X64_HugePage:
+        return seL4_HugePageBits;
+
     default:
         fail("Invalid page size");
     }
@@ -67,6 +71,9 @@ pageBitsForSize_phys(vm_page_size_t pagesize)
     case X86_LargePage:
         return seL4_LargePageBits;
 
+    case X64_HugePage:
+        return seL4_HugePageBits;
+
     default:
         fail("Invalid page size");
     }
diff --git a/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h b/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h
index 3c1d5010b..ba2067553 100644
--- a/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h
+++ b/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h
@@ -32,10 +32,11 @@
 #define seL4_IOPageTableBits 12
 #define seL4_ASIDPoolBits    12
 
+#define seL4_HugePageBits    30 /* 1GB */
+
 #ifdef CONFIG_PAE_PAGING
 #define seL4_PDPTBits        5
 #define seL4_LargePageBits   21 /* 2MB */
-#define seL4_HugePageBits    30 /* 1GB */
 #else
 #define seL4_PDPTBits         0
 #define seL4_LargePageBits    22 /* 4MB */
diff --git a/src/arch/x86/c_traps.c b/src/arch/x86/c_traps.c
index f5635d7ef..64b4cda3b 100644
--- a/src/arch/x86/c_traps.c
+++ b/src/arch/x86/c_traps.c
@@ -75,8 +75,13 @@ void NORETURN
 slowpath(syscall_t syscall)
 {
     ARCH_NODE_STATE(x86KScurInterrupt) = -1;
-    /* increment NextIP to skip sysenter */
-    ksCurThread->tcbArch.tcbContext.registers[NextIP] += 2;
+    if (config_set(CONFIG_SYSENTER)) {
+        /* increment NextIP to skip sysenter */
+        ksCurThread->tcbArch.tcbContext.registers[NextIP] += 2;
+    } else {
+        /* set FaultIP */
+        setRegister(ksCurThread, FaultIP, getRegister(ksCurThread, NextIP) - 2);
+    }
     /* check for undefined syscall */
     if (unlikely(syscall < SYSCALL_MIN || syscall > SYSCALL_MAX)) {
 #ifdef TRACK_KERNEL_ENTIRES
diff --git a/src/arch/x86/kernel/boot.c b/src/arch/x86/kernel/boot.c
index e6e3230a2..e4a8a2241 100644
--- a/src/arch/x86/kernel/boot.c
+++ b/src/arch/x86/kernel/boot.c
@@ -421,8 +421,14 @@ init_cpu(
     /* initialise CPU's descriptor table registers (GDTR, IDTR, LDTR, TR) */
     init_dtrs();
 
-    /* initialise MSRs (needs an initialised TSS) */
-    init_sysenter_msrs();
+    if (config_set(CONFIG_SYSENTER)) {
+        /* initialise MSRs (needs an initialised TSS) */
+        init_sysenter_msrs();
+    } else if (config_set(CONFIG_SYSCALL)) {
+        init_syscall_msrs();
+    } else {
+        return false;
+    }
 
     /* setup additional PAT MSR */
     if (!init_pat_msr()) {
diff --git a/src/arch/x86/kernel/boot_sys.c b/src/arch/x86/kernel/boot_sys.c
index 7b37fa87c..5dee6b50a 100644
--- a/src/arch/x86/kernel/boot_sys.c
+++ b/src/arch/x86/kernel/boot_sys.c
@@ -195,7 +195,7 @@ try_boot_sys_node(cpu_id_t cpu_id)
             )) {
         return false;
     }
-    setCurrentPD(kpptr_to_paddr(X86_GLOBAL_VSPACE_ROOT));
+    setCurrentVSpaceRoot(kpptr_to_paddr(X86_GLOBAL_VSPACE_ROOT), 0);
     /* Sync up the compilers view of the world here to force the PD to actually
      * be set *right now* instead of delayed */
     asm volatile("" ::: "memory");
diff --git a/src/plat/pc99/Kconfig b/src/plat/pc99/Kconfig
index e289a6ba1..dbbce07c5 100644
--- a/src/plat/pc99/Kconfig
+++ b/src/plat/pc99/Kconfig
@@ -50,6 +50,22 @@ config PAE_PAGING
         PAE paging uses 4K/2M pages and has three levels of paging. If this
         is not used the old 32-bit paging with 4K/4M pages will be used
 
+choice
+    prompt "Kernel syscall style"
+    depends on ARCH_X86
+    default SYSENTER if ARCH_IA32
+    help
+        The kernel only ever supports one method of performing syscalls
+        at a time. This config should be set to the most efficient one
+        that is support by the hardware the system will run on
+
+    config SYSENTER
+        bool "sysenter+sysexit"
+    config SYSCALL
+        depends on !ARCH_IA32
+        bool "syscall+sysret"
+endchoice
+
 choice
     prompt "FPU state implementation"
     depends on ARCH_X86