diff --git a/apps/system/components/kata-os-common/src/sel4-sys/arch/x86_64.rs b/apps/system/components/kata-os-common/src/sel4-sys/arch/x86_64.rs
index beef0b8..2a9df9f 100644
--- a/apps/system/components/kata-os-common/src/sel4-sys/arch/x86_64.rs
+++ b/apps/system/components/kata-os-common/src/sel4-sys/arch/x86_64.rs
@@ -1,12 +1,13 @@
-
-use core::mem::uninitialized;
-
 pub const seL4_WordBits: usize = 64;
 pub const seL4_PageBits: usize = 12;
 pub const seL4_SlotBits: usize = 5;
 pub const seL4_TCBBits: usize = 11;
 pub const seL4_EndpointBits: usize = 4;
+#[cfg(not(feature = "CONFIG_KERNEL_MCS"))]
 pub const seL4_NotificationBits: usize = 5;
+#[cfg(feature = "CONFIG_KERNEL_MCS")]
+pub const seL4_NotificationBits: usize = 6;
+pub const seL4_ReplyBits: usize = 6; // Only relevant when CONFIG_KERNEL_MCS is enabled
 pub const seL4_PageTableBits: usize = 12;
 pub const seL4_PageDirBits: usize = 12;
 pub const seL4_PDPTBits: usize = 12;
@@ -34,7 +35,6 @@ pub const seL4_NumExclusiveWatchpoints: usize = 0;
 pub const seL4_FirstDualFunctionMonitor: usize = 0;
 pub const seL4_NumDualFunctionMonitors: usize = 4;
 
-
 pub type seL4_X86_ASIDControl = seL4_CPtr;
 pub type seL4_X86_ASIDPool = seL4_CPtr;
 pub type seL4_X86_IOSpace = seL4_CPtr;
@@ -43,6 +43,7 @@ pub type seL4_X86_Page = seL4_CPtr;
 pub type seL4_X86_PageDirectory = seL4_CPtr;
 pub type seL4_X86_PageTable = seL4_CPtr;
 pub type seL4_X86_IOPageTable = seL4_CPtr;
+pub type seL4_X86_IOPortControl = seL4_CPtr;
 pub type seL4_X86_PDPT = seL4_CPtr;
 pub type seL4_X64_PML4 = seL4_CPtr;
 
@@ -130,7 +131,8 @@ pub struct seL4_UserContext {
     pub r13: seL4_Word,
     pub r14: seL4_Word,
     pub r15: seL4_Word,
-    pub tls_base: seL4_Word,
+    pub fs_base: seL4_Word,
+    pub gs_base: seL4_Word,
 }
 
 #[repr(C, packed)]
@@ -218,190 +220,103 @@ pub struct seL4_X86_BootInfo_VBE {
     pub vbeInterfaceLen: u32,
 }
 
-
 #[inline(always)]
-pub unsafe fn seL4_GetMR(regnum: isize) -> seL4_Word {
-    let mr;
-    asm!("movq %gs:8(,$1,0x8), $0" : "=r"(mr) : "r"(regnum) : : "volatile");
-    mr
+pub unsafe fn seL4_GetIPCBuffer() -> *mut seL4_IPCBuffer {
+    // Use magic external symbol setup by runtime once TLS is primed
+    enum c_void {}
+    extern "C" {
+        #[thread_local]
+        static __sel4_ipc_buffer: *const c_void;
+    }
+    __sel4_ipc_buffer as *mut seL4_IPCBuffer
 }
 
 #[inline(always)]
-pub unsafe fn seL4_SetMR(regnum: isize, value: seL4_Word) {
-    asm!("movq $0, %gs:8(,$1,0x8)" : : "r"(value), "r"(regnum) : "memory" : "volatile");
+pub unsafe fn seL4_GetMR(regnum: usize) -> seL4_Word {
+    (*seL4_GetIPCBuffer()).msg[regnum]
+}
+
+#[inline(always)]
+pub unsafe fn seL4_SetMR(regnum: usize, value: seL4_Word) {
+    (*seL4_GetIPCBuffer()).msg[regnum] = value;
 }
 
 #[inline(always)]
 pub unsafe fn seL4_GetUserData() -> seL4_Word {
-    let data;
-    asm!("movq %gs:968, $0" : "=r"(data) : : : "volatile");
-    data
-}
-
-#[inline(always)]
-pub unsafe fn seL4_GetIPCBuffer() -> *mut seL4_IPCBuffer {
-    seL4_GetUserData() as isize as *mut seL4_IPCBuffer
+    (*seL4_GetIPCBuffer()).userData
 }
 
 #[inline(always)]
 pub unsafe fn seL4_SetUserData(data: seL4_Word) {
-    asm!("movq $0, %gs:968" : : "r"(data) : "memory" : "volatile");
+    (*seL4_GetIPCBuffer()).userData = data;
 }
 
 #[inline(always)]
-pub unsafe fn seL4_GetBadge(index: isize) -> seL4_CapData {
-    let mut badge: seL4_CapData = uninitialized();
-    asm!("movq %gs:976(,$1,0x8), $0" : "=r"(badge.words[0]) : "r"(index) : : "volatile");
-    badge
+pub unsafe fn seL4_GetBadge(index: usize) -> seL4_Word {
+    (*seL4_GetIPCBuffer()).caps_or_badges[index]
 }
 
 #[inline(always)]
-pub unsafe fn seL4_GetCap(index: isize) -> seL4_CPtr {
-    let cptr;
-    asm!("movq %gs:976(,$1,0x8), $0" : "=r"(cptr) : "r"(index) : : "volatile");
-    cptr
+pub unsafe fn seL4_GetCap(index: usize) -> seL4_CPtr {
+    (*seL4_GetIPCBuffer()).caps_or_badges[index] as seL4_CPtr
 }
 
 #[inline(always)]
-pub unsafe fn seL4_SetCap(index: isize, cptr: seL4_CPtr) {
-    asm!("movq $0, %gs:976(,$1,0x8)" : : "r"(cptr), "r"(index) : "memory" : "volatile");
+pub unsafe fn seL4_SetCap(index: usize, cptr: seL4_CPtr) {
+    (*seL4_GetIPCBuffer()).caps_or_badges[index] = cptr as seL4_Word;
 }
 
 #[inline(always)]
-pub unsafe fn seL4_GetCapReceivePath(receiveCNode: *mut seL4_CPtr,
-                                     receiveIndex: *mut seL4_CPtr,
-                                     receiveDepth: *mut seL4_Word) {
+pub unsafe fn seL4_GetCapReceivePath(
+    receiveCNode: *mut seL4_CPtr,
+    receiveIndex: *mut seL4_CPtr,
+    receiveDepth: *mut seL4_Word,
+) {
+    let ipcbuffer = seL4_GetIPCBuffer();
     if !receiveCNode.is_null() {
-        asm!("movq %gs:1000, $0" : "=r"(*receiveCNode) : : : "volatile");
+        *receiveCNode = (*ipcbuffer).receiveCNode;
     }
-
     if !receiveIndex.is_null() {
-        asm!("movq %gs:1008, $0" : "=r"(*receiveIndex) : : : "volatile");
+        *receiveIndex = (*ipcbuffer).receiveIndex;
     }
-
     if !receiveDepth.is_null() {
-        asm!("movq %gs:1016, $0" : "=r"(*receiveDepth) : : : "volatile");
+        *receiveDepth = (*ipcbuffer).receiveDepth;
     }
 }
 
 #[inline(always)]
-pub unsafe fn seL4_SetCapReceivePath(receiveCNode: seL4_CPtr,
-                                     receiveIndex: seL4_CPtr,
-                                     receiveDepth: seL4_Word) {
-    asm!("movq $0, %gs:1000" : : "r"(receiveCNode) : "memory" : "volatile");
-    asm!("movq $0, %gs:1008" : : "r"(receiveIndex) : "memory" : "volatile");
-    asm!("movq $0, %gs:1016" : : "r"(receiveDepth) : "memory" : "volatile");
+pub unsafe fn seL4_SetCapReceivePath(
+    receiveCNode: seL4_CPtr,
+    receiveIndex: seL4_CPtr,
+    receiveDepth: seL4_Word,
+) {
+    let ipcbuffer = seL4_GetIPCBuffer();
+    (*ipcbuffer).receiveCNode = receiveCNode;
+    (*ipcbuffer).receiveIndex = receiveIndex;
+    (*ipcbuffer).receiveDepth = receiveDepth;
 }
 
-#[inline(always)]
-unsafe fn x64_sys_send(sys: seL4_Word, dest: seL4_Word, info: seL4_Word, mr1: seL4_Word, mr2: seL4_Word, mr3: seL4_Word, mr4: seL4_Word) {
-    asm!("movq %rsp, %rbx
-          syscall
-          movq %rbx, %rsp"
-          : 
-          : "{rdx}" (sys),
-            "{rdi}" (dest),
-            "{rsi}" (info),
-            "{r10}" (mr1),
-            "{r8}" (mr2),
-            "{r9}" (mr3),
-            "{r15}" (mr4)
-          : "%rcx", "%rbx", "%r11"
-          : "volatile");
-}
-
-#[inline(always)]
-unsafe fn x64_sys_reply(sys: seL4_Word, info: seL4_Word, mr1: seL4_Word, mr2: seL4_Word, mr3: seL4_Word, mr4: seL4_Word) {
-    asm!("movq %rsp, %rbx
-          syscall
-          movq %rbx, %rsp"
-          :
-          : "{rdx}" (sys),
-            "{rsi}" (info),
-            "{r10}" (mr1),
-            "{r8}" (mr2),
-            "{r9}" (mr3),
-            "{r15}" (mr4)
-          : "%rcx", "%rbx", "%r11"
-          : "volatile");
-}
-
-#[inline(always)]
-unsafe fn x64_sys_send_null(sys: seL4_Word, dest: seL4_Word, info: seL4_Word) {
-    asm!("movq %rsp, %rbx
-          syscall
-          movq %rbx, %rsp"
-          : 
-          : "{rdx}" (sys),
-            "{rdi}" (dest),
-            "{rsi}" (info)
-          : "%rcx", "%rbx", "%r11"
-          : "volatile");
-}
-
-#[inline(always)]
-unsafe fn x64_sys_recv(sys: seL4_Word, src: seL4_Word, out_badge: *mut seL4_Word, out_info: *mut seL4_Word, out_mr1: *mut seL4_Word, out_mr2: *mut seL4_Word, out_mr3: *mut seL4_Word, out_mr4: *mut seL4_Word) {
-    asm!("movq %rsp, %rbx
-          syscall
-          movq %rbx, %rsp"
-          : "={rsi}" (*out_info)
-            "={r10}" (*out_mr1),
-            "={r8}" (*out_mr2),
-            "={r9}" (*out_mr3),
-            "={r15}" (*out_mr4),
-            "={rdi}" (*out_badge)
-          : "{rdx}" (sys),
-            "{rdi}" (src)
-          : "memory", "%rcx", "%rbx", "%r11"
-          : "volatile");
-}
-
-#[inline(always)]
-unsafe fn x64_sys_send_recv(sys: seL4_Word, dest: seL4_Word, out_dest: *mut seL4_Word, info: seL4_Word, out_info: *mut seL4_Word, in_out_mr1: *mut seL4_Word, in_out_mr2: *mut seL4_Word, in_out_mr3: *mut seL4_Word, in_out_mr4: *mut seL4_Word) {
-    asm!("movq %rsp, %rbx
-          syscall
-          movq %rbx, %rsp"
-          : "={rsi}" (*out_info)
-            "={r10}" (*in_out_mr1),
-            "={r8}" (*in_out_mr2),
-            "={r9}" (*in_out_mr3),
-            "={r15}" (*in_out_mr4),
-            "={rdi}" (*out_dest)
-          : "{rdx}" (sys),
-            "{rsi}" (info),
-            "{r10}" (*in_out_mr1),
-            "{r8}" (*in_out_mr2),
-            "{r9}" (*in_out_mr3),
-            "{r15}" (*in_out_mr4),
-            "{rdi}" (dest)
-          : "memory", "%rcx", "%rbx", "%r11"
-          : "volatile");
-}
-
-#[inline(always)]
-unsafe fn x64_sys_null(sys: seL4_Word) {
-    asm!("movq %rsp, %rbx
-          syscall
-          movq %rbx, %rsp"
-          :
-          : "{rdx}" (sys)
-          : "%rcx", "%rbx", "%r11", "%rsi", "%rdi"
-          : "volatile");
+macro_rules! swinum {
+    ($val:expr) => {
+        $val as seL4_Word
+    };
 }
 
 #[inline(always)]
 pub unsafe fn seL4_Send(dest: seL4_CPtr, msgInfo: seL4_MessageInfo) {
-    x64_sys_send(SyscallId::Send as seL4_Word, dest, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1), seL4_GetMR(2), seL4_GetMR(3));
-}
-
-macro_rules! opt_deref {
-    ($name:expr) => {
-        if !$name.is_null() {
-            *$name
-        } else {
-            0
-        }
-    }
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::Send),
+        in("rdi") dest,
+        in("rsi") msgInfo.words[0],
+        in("r10") seL4_GetMR(0),
+        in("r8") seL4_GetMR(1),
+        in("r9") seL4_GetMR(2),
+        in("r15") seL4_GetMR(3),
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _);
 }
 
 macro_rules! opt_assign {
@@ -409,92 +324,404 @@ macro_rules! opt_assign {
         if !$loc.is_null() {
             *$loc = $val;
         }
-    }
+    };
 }
 
 #[inline(always)]
-pub unsafe fn seL4_SendWithMRs(dest: seL4_CPtr, msgInfo: seL4_MessageInfo,
-                               mr0: *mut seL4_Word, mr1: *mut seL4_Word,
-                               mr2: *mut seL4_Word, mr3: *mut seL4_Word) {
-    x64_sys_send(SyscallId::Send as seL4_Word, dest, msgInfo.words[0],
-                 if mr0.is_null() { 0 } else { *mr0 },
-                 if mr1.is_null() { 0 } else { *mr1 },
-                 if mr2.is_null() { 0 } else { *mr2 },
-                 if mr3.is_null() { 0 } else { *mr3 },
-                 );
+pub unsafe fn seL4_SendWithMRs(
+    dest: seL4_CPtr,
+    msgInfo: seL4_MessageInfo,
+    mr0: *mut seL4_Word,
+    mr1: *mut seL4_Word,
+    mr2: *mut seL4_Word,
+    mr3: *mut seL4_Word,
+) {
+    let mut msg0 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg1 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg2 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg3 = ::core::mem::MaybeUninit::uninit().assume_init();
+
+    if !mr0.is_null() && msgInfo.get_length() > 0 {
+        msg0 = *mr0;
+    }
+    if !mr1.is_null() && msgInfo.get_length() > 1 {
+        msg1 = *mr1;
+    }
+    if !mr2.is_null() && msgInfo.get_length() > 2 {
+        msg2 = *mr2;
+    }
+    if !mr3.is_null() && msgInfo.get_length() > 3 {
+        msg3 = *mr3;
+    }
+
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::Send),
+        in("rdi") dest,
+        in("rsi") msgInfo.words[0],
+        in("r10") msg0,
+        in("r8") msg1,
+        in("r9") msg2,
+        in("r15") msg3,
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _);
 }
 
 #[inline(always)]
 pub unsafe fn seL4_NBSend(dest: seL4_CPtr, msgInfo: seL4_MessageInfo) {
-    x64_sys_send(SyscallId::NBSend as seL4_Word, dest, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1), seL4_GetMR(2), seL4_GetMR(3));
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::NBSend),
+        in("rdi") dest,
+        in("rsi") msgInfo.words[0],
+        in("r10") seL4_GetMR(0),
+        in("r8") seL4_GetMR(1),
+        in("r9") seL4_GetMR(2),
+        in("r15") seL4_GetMR(3),
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _);
 }
 
 #[inline(always)]
-pub unsafe fn seL4_NBSendWithMRs(dest: seL4_CPtr, msgInfo: seL4_MessageInfo,
-                                 mr0: *mut seL4_Word, mr1: *mut seL4_Word,
-                                 mr2: *mut seL4_Word, mr3: *mut seL4_Word) {
-    x64_sys_send(SyscallId::NBSend as seL4_Word, dest, msgInfo.words[0],
-                 if mr0.is_null() { 0 } else { *mr0 },
-                 if mr1.is_null() { 0 } else { *mr1 },
-                 if mr2.is_null() { 0 } else { *mr2 },
-                 if mr3.is_null() { 0 } else { *mr3 });
+pub unsafe fn seL4_NBSendWithMRs(
+    dest: seL4_CPtr,
+    msgInfo: seL4_MessageInfo,
+    mr0: *mut seL4_Word,
+    mr1: *mut seL4_Word,
+    mr2: *mut seL4_Word,
+    mr3: *mut seL4_Word,
+) {
+    let mut msg0 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg1 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg2 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg3 = ::core::mem::MaybeUninit::uninit().assume_init();
+
+    if !mr0.is_null() && msgInfo.get_length() > 0 {
+        msg0 = *mr0;
+    }
+    if !mr1.is_null() && msgInfo.get_length() > 1 {
+        msg1 = *mr1;
+    }
+    if !mr2.is_null() && msgInfo.get_length() > 2 {
+        msg2 = *mr2;
+    }
+    if !mr3.is_null() && msgInfo.get_length() > 3 {
+        msg3 = *mr3;
+    }
+
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::NBSend),
+        in("rdi") dest,
+        in("rsi") msgInfo.words[0],
+        in("r10") msg0,
+        in("r8") msg1,
+        in("r9") msg2,
+        in("r15") msg3,
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _);
 }
 
+#[cfg(not(feature = "CONFIG_KERNEL_MCS"))]
 #[inline(always)]
 pub unsafe fn seL4_Reply(msgInfo: seL4_MessageInfo) {
-    x64_sys_reply(SyscallId::Reply as seL4_Word, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1), seL4_GetMR(2), seL4_GetMR(3));
-
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::Reply),
+        in("rsi") msgInfo.words[0],
+        in("r10") seL4_GetMR(0),
+        in("r8") seL4_GetMR(1),
+        in("r9") seL4_GetMR(2),
+        in("r15") seL4_GetMR(3),
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _);
 }
+
+#[cfg(not(feature = "CONFIG_KERNEL_MCS"))]
 #[inline(always)]
-pub unsafe fn seL4_ReplyWithMRs(msgInfo: seL4_MessageInfo,
-                                mr0: *mut seL4_Word, mr1: *mut seL4_Word,
-                                mr2: *mut seL4_Word, mr3: *mut seL4_Word) {
-    x64_sys_reply(SyscallId::Reply as seL4_Word, msgInfo.words[0],
-                  if mr0.is_null() { 0 } else { *mr0 },
-                  if mr1.is_null() { 0 } else { *mr1 },
-                  if mr2.is_null() { 0 } else { *mr2 },
-                  if mr3.is_null() { 0 } else { *mr3 });
-}
+pub unsafe fn seL4_ReplyWithMRs(
+    msgInfo: seL4_MessageInfo,
+    mr0: *mut seL4_Word,
+    mr1: *mut seL4_Word,
+    mr2: *mut seL4_Word,
+    mr3: *mut seL4_Word,
+) {
+    let mut msg0 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg1 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg2 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg3 = ::core::mem::MaybeUninit::uninit().assume_init();
 
+    if !mr0.is_null() && msgInfo.get_length() > 0 {
+        msg0 = *mr0;
+    }
+    if !mr1.is_null() && msgInfo.get_length() > 1 {
+        msg1 = *mr1;
+    }
+    if !mr2.is_null() && msgInfo.get_length() > 2 {
+        msg2 = *mr2;
+    }
+    if !mr3.is_null() && msgInfo.get_length() > 3 {
+        msg3 = *mr3;
+    }
+
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::Reply),
+        in("rsi") msgInfo.words[0],
+        in("r10") msg0,
+        in("r8") msg1,
+        in("r9") msg2,
+        in("r15") msg3,
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _);
+}
 
 #[inline(always)]
 pub unsafe fn seL4_Signal(dest: seL4_CPtr) {
-    x64_sys_send_null(SyscallId::Send as seL4_Word, dest, seL4_MessageInfo::new(0,0,0,0).words[0]);
+    let info = seL4_MessageInfo::new(0, 0, 0, 0).words[0];
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::Send),
+        in("rdi") dest,
+        in("rsi") info,
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _);
 }
 
 #[inline(always)]
-pub unsafe fn seL4_Recv(src: seL4_CPtr, sender: *mut seL4_Word) -> seL4_MessageInfo {
-    let mut info: seL4_MessageInfo = uninitialized();
-    let mut badge: seL4_Word = uninitialized();
-    let mut mr0: seL4_Word = uninitialized();
-    let mut mr1: seL4_Word = uninitialized();
-    let mut mr2: seL4_Word = uninitialized();
-    let mut mr3: seL4_Word = uninitialized();
+pub unsafe fn seL4_Recv(mut src: seL4_CPtr, sender: *mut seL4_Word) -> seL4_MessageInfo {
+    let mut info: seL4_Word;
+    let mut msg0 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg1 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg2 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg3 = ::core::mem::MaybeUninit::uninit().assume_init();
 
-    x64_sys_recv(SyscallId::Recv as seL4_Word, src, &mut badge, &mut info.words[0], &mut mr0, &mut mr1, &mut mr2, &mut mr3);
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::Recv),
+        out("rdi") src,
+        out("rsi") info,
+        out("r10") msg0,
+        out("r8") msg1,
+        out("r9") msg2,
+        out("r15") msg3,
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _);
 
-    seL4_SetMR(0, mr0);
-    seL4_SetMR(1, mr1);
-    seL4_SetMR(2, mr2);
-    seL4_SetMR(3, mr3);
+    seL4_SetMR(0, msg0);
+    seL4_SetMR(1, msg1);
+    seL4_SetMR(2, msg2);
+    seL4_SetMR(3, msg3);
 
-    opt_assign!(sender, badge);
+    opt_assign!(sender, src);
 
-    info
+    seL4_MessageInfo { words: [info] }
 }
 
 #[inline(always)]
-pub unsafe fn seL4_RecvWithMRs(src: seL4_CPtr, sender: *mut seL4_Word,
-                               mr0: *mut seL4_Word, mr1: *mut seL4_Word,
-                               mr2: *mut seL4_Word, mr3: *mut seL4_Word) -> seL4_MessageInfo {
-    let mut info: seL4_MessageInfo = uninitialized();
-    let mut badge: seL4_Word = uninitialized();
-    let mut msg0: seL4_Word = uninitialized();
-    let mut msg1: seL4_Word = uninitialized();
-    let mut msg2: seL4_Word = uninitialized();
-    let mut msg3: seL4_Word = uninitialized();
+pub unsafe fn seL4_NBRecv(mut src: seL4_CPtr, sender: *mut seL4_Word) -> seL4_MessageInfo {
+    let mut info: seL4_Word;
+    let mut msg0 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg1 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg2 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg3 = ::core::mem::MaybeUninit::uninit().assume_init();
 
-    x64_sys_recv(SyscallId::Recv as seL4_Word, src, &mut badge, &mut info.words[0], &mut msg0, &mut msg1, &mut msg2, &mut msg3);
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::NBRecv),
+        inout("rdi") src,
+        out("rsi") info,
+        out("r10") msg0,
+        out("r8") msg1,
+        out("r9") msg2,
+        out("r15") msg3,
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _);
+
+    seL4_SetMR(0, msg0);
+    seL4_SetMR(1, msg1);
+    seL4_SetMR(2, msg2);
+    seL4_SetMR(3, msg3);
+
+    opt_assign!(sender, src);
+
+    seL4_MessageInfo { words: [info] }
+}
+
+#[inline(always)]
+pub unsafe fn seL4_Call(dest: seL4_CPtr, msgInfo: seL4_MessageInfo) -> seL4_MessageInfo {
+    let mut info: seL4_Word;
+    let mut msg0 = seL4_GetMR(0);
+    let mut msg1 = seL4_GetMR(1);
+    let mut msg2 = seL4_GetMR(2);
+    let mut msg3 = seL4_GetMR(3);
+
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::Call),
+        in("rdi") dest,
+        inout("rsi") msgInfo.words[0] => info,
+        inout("r10") msg0,
+        inout("r8") msg1,
+        inout("r9") msg2,
+        inout("r15") msg3,
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _);
+
+    seL4_SetMR(0, msg0);
+    seL4_SetMR(1, msg1);
+    seL4_SetMR(2, msg2);
+    seL4_SetMR(3, msg3);
+
+    seL4_MessageInfo { words: [info] }
+}
+
+#[inline(always)]
+pub unsafe fn seL4_CallWithMRs(
+    dest: seL4_CPtr,
+    msgInfo: seL4_MessageInfo,
+    mr0: *mut seL4_Word,
+    mr1: *mut seL4_Word,
+    mr2: *mut seL4_Word,
+    mr3: *mut seL4_Word,
+) -> seL4_MessageInfo {
+    let mut info: seL4_Word;
+    let mut msg0 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg1 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg2 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg3 = ::core::mem::MaybeUninit::uninit().assume_init();
+
+    if !mr0.is_null() && msgInfo.get_length() > 0 {
+        msg0 = *mr0;
+    }
+    if !mr1.is_null() && msgInfo.get_length() > 1 {
+        msg1 = *mr1;
+    }
+    if !mr2.is_null() && msgInfo.get_length() > 2 {
+        msg2 = *mr2;
+    }
+    if !mr3.is_null() && msgInfo.get_length() > 3 {
+        msg3 = *mr3;
+    }
+
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::Call),
+        in("rdi") dest,
+        inout("rsi") msgInfo.words[0] => info,
+        inout("r10") msg0,
+        inout("r8") msg1,
+        inout("r9") msg2,
+        inout("r15") msg3,
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _);
+
+    opt_assign!(mr0, msg0);
+    opt_assign!(mr1, msg1);
+    opt_assign!(mr2, msg2);
+    opt_assign!(mr3, msg3);
+
+    seL4_MessageInfo { words: [info] }
+}
+
+#[inline(always)]
+pub unsafe fn seL4_ReplyRecv(
+    mut src: seL4_CPtr,
+    msgInfo: seL4_MessageInfo,
+    sender: *mut seL4_Word,
+) -> seL4_MessageInfo {
+    let mut info: seL4_Word;
+    let mut msg0 = seL4_GetMR(0);
+    let mut msg1 = seL4_GetMR(1);
+    let mut msg2 = seL4_GetMR(2);
+    let mut msg3 = seL4_GetMR(3);
+
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::ReplyRecv),
+        inout("rdi") src,
+        inout("rsi") msgInfo.words[0] => info,
+        inout("r10") msg0,
+        inout("r8") msg1,
+        inout("r9") msg2,
+        inout("r15") msg3,
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _);
+
+    seL4_SetMR(0, msg0);
+    seL4_SetMR(1, msg1);
+    seL4_SetMR(2, msg2);
+    seL4_SetMR(3, msg3);
+
+    opt_assign!(sender, src);
+
+    seL4_MessageInfo { words: [info] }
+}
+
+#[inline(always)]
+pub unsafe fn seL4_ReplyRecvWithMRs(
+    src: seL4_CPtr,
+    msgInfo: seL4_MessageInfo,
+    sender: *mut seL4_Word,
+    mr0: *mut seL4_Word,
+    mr1: *mut seL4_Word,
+    mr2: *mut seL4_Word,
+    mr3: *mut seL4_Word,
+) -> seL4_MessageInfo {
+    let mut info: seL4_Word;
+    let mut badge: seL4_Word;
+    let mut msg0 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg1 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg2 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg3 = ::core::mem::MaybeUninit::uninit().assume_init();
+    if !mr0.is_null() && msgInfo.get_length() > 0 {
+        msg0 = *mr0;
+    }
+    if !mr1.is_null() && msgInfo.get_length() > 1 {
+        msg1 = *mr1;
+    }
+    if !mr2.is_null() && msgInfo.get_length() > 2 {
+        msg2 = *mr2;
+    }
+    if !mr3.is_null() && msgInfo.get_length() > 3 {
+        msg3 = *mr3;
+    }
+
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::ReplyRecv),
+        inout("rdi") src => badge,
+        inout("rsi") msgInfo.words[0] => info,
+        inout("r10") msg0,
+        inout("r8") msg1,
+        inout("r9") msg2,
+        inout("r15") msg3,
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _);
 
     opt_assign!(mr0, msg0);
     opt_assign!(mr1, msg1);
@@ -503,144 +730,99 @@ pub unsafe fn seL4_RecvWithMRs(src: seL4_CPtr, sender: *mut seL4_Word,
 
     opt_assign!(sender, badge);
 
-    info
+    seL4_MessageInfo { words: [info] }
 }
 
+#[cfg(feature = "CONFIG_KERNEL_MCS")]
 #[inline(always)]
-pub unsafe fn seL4_NBRecv(src: seL4_CPtr, sender: *mut seL4_Word) -> seL4_MessageInfo {
-    let mut info: seL4_MessageInfo = uninitialized();
-    let mut badge: seL4_Word = uninitialized();
-    let mut mr0: seL4_Word = uninitialized();
-    let mut mr1: seL4_Word = uninitialized();
-    let mut mr2: seL4_Word = uninitialized();
-    let mut mr3: seL4_Word = uninitialized();
+pub unsafe fn seL4_NBSendRecv(
+    dest: seL4_CPtr,
+    msgInfo: seL4_MessageInfo,
+    src: seL4_CPtr,
+    sender: *mut seL4_Word,
+    reply: seL4_CPtr,
+) -> seL4_MessageInfo {
+    let mut info: seL4_Word;
+    let mut badge: seL4_Word;
+    let mut msg0 = seL4_GetMR(0);
+    let mut msg1 = seL4_GetMR(1);
+    let mut msg2 = seL4_GetMR(2);
+    let mut msg3 = seL4_GetMR(3);
 
-    x64_sys_recv(SyscallId::NBRecv as seL4_Word, src, &mut badge, &mut info.words[0], &mut mr0, &mut mr1, &mut mr2, &mut mr3);
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::NBSendRecv),
+        inout("rdi") src => badge,
+        inout("rsi") msgInfo.words[0] => info,
+        inout("r10") msg0,
+        inout("r8") msg1,
+        inout("r9") msg2,
+        inout("r15") msg3,
+        in("r12") reply,
+        in("r13") dest,
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _);
 
-    seL4_SetMR(0, mr0);
-    seL4_SetMR(1, mr1);
-    seL4_SetMR(2, mr2);
-    seL4_SetMR(3, mr3);
+    /* Write the message back out to memory. */
+    seL4_SetMR(0, msg0);
+    seL4_SetMR(1, msg1);
+    seL4_SetMR(2, msg2);
+    seL4_SetMR(3, msg3);
 
     opt_assign!(sender, badge);
 
-    info
+    seL4_MessageInfo { words: [info] }
 }
 
+#[cfg(feature = "CONFIG_KERNEL_MCS")]
 #[inline(always)]
-pub unsafe fn seL4_Call(mut dest: seL4_CPtr, msgInfo: seL4_MessageInfo) -> seL4_MessageInfo {
-    let mut info: seL4_MessageInfo = uninitialized();
-    let mut mr0 = seL4_GetMR(0);
-    let mut mr1 = seL4_GetMR(1);
-    let mut mr2 = seL4_GetMR(2);
-    let mut mr3 = seL4_GetMR(3);
-
-    x64_sys_send_recv(SyscallId::Call as seL4_Word, dest, &mut dest, msgInfo.words[0], &mut info.words[0], &mut mr0, &mut mr1, &mut mr2, &mut mr3);
-
-    seL4_SetMR(0, mr0);
-    seL4_SetMR(1, mr1);
-    seL4_SetMR(2, mr2);
-    seL4_SetMR(3, mr3);
-
-    info
-}
-
-#[inline(always)]
-pub unsafe fn seL4_CallWithMRs(mut dest: seL4_CPtr, msgInfo: seL4_MessageInfo,
-                               mr0: *mut seL4_Word, mr1: *mut seL4_Word,
-                               mr2: *mut seL4_Word, mr3: *mut seL4_Word) -> seL4_MessageInfo {
-    let mut info: seL4_MessageInfo = uninitialized();
-    let mut msg0: seL4_Word = 0;
-    let mut msg1: seL4_Word = 0;
-    let mut msg2: seL4_Word = 0;
-    let mut msg3: seL4_Word = 0;
-
-    if !mr0.is_null() {
-        if msgInfo.get_length() > 0 {
-            msg0 = *mr0;
-        }
+pub unsafe fn seL4_NBSendRecvWithMRs(
+    dest: seL4_CPtr,
+    msgInfo: seL4_MessageInfo,
+    src: seL4_CPtr,
+    sender: *mut seL4_Word,
+    mr0: *mut seL4_Word,
+    mr1: *mut seL4_Word,
+    mr2: *mut seL4_Word,
+    mr3: *mut seL4_Word,
+    reply: seL4_CPtr,
+) -> seL4_MessageInfo {
+    let mut info: seL4_Word;
+    let mut badge: seL4_Word;
+    let mut msg0 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg1 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg2 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg3 = ::core::mem::MaybeUninit::uninit().assume_init();
+    if !mr0.is_null() && msgInfo.get_length() > 0 {
+        msg0 = *mr0;
     }
-    if !mr1.is_null() {
-        if msgInfo.get_length() > 1 {
-            msg1 = *mr1;
-        }
+    if !mr1.is_null() && msgInfo.get_length() > 1 {
+        msg1 = *mr1;
     }
-    if !mr2.is_null() {
-        if msgInfo.get_length() > 2 {
-            msg2 = *mr2;
-        }
+    if !mr2.is_null() && msgInfo.get_length() > 2 {
+        msg2 = *mr2;
     }
-    if !mr3.is_null() {
-        if msgInfo.get_length() > 3 {
-            msg3 = *mr3;
-        }
+    if !mr3.is_null() && msgInfo.get_length() > 3 {
+        msg3 = *mr3;
     }
 
-    x64_sys_send_recv(SyscallId::Call as seL4_Word, dest, &mut dest, msgInfo.words[0], &mut info.words[0], &mut msg0, &mut msg1, &mut msg2, &mut msg3);
-
-    opt_assign!(mr0, msg0);
-    opt_assign!(mr1, msg1);
-    opt_assign!(mr2, msg2);
-    opt_assign!(mr3, msg3);
-
-    info
-}
-
-#[inline(always)]
-pub unsafe fn seL4_ReplyRecv(dest: seL4_CPtr, msgInfo: seL4_MessageInfo,
-                             sender: *mut seL4_Word) -> seL4_MessageInfo {
-    let mut info: seL4_MessageInfo = uninitialized();
-    let mut badge: seL4_Word = uninitialized();
-    let mut mr0 = seL4_GetMR(0);
-    let mut mr1 = seL4_GetMR(1);
-    let mut mr2 = seL4_GetMR(2);
-    let mut mr3 = seL4_GetMR(3);
-
-    x64_sys_send_recv(SyscallId::ReplyRecv as seL4_Word, dest, &mut badge, msgInfo.words[0], &mut info.words[0], &mut mr0, &mut mr1, &mut mr2, &mut mr3);
-
-    seL4_SetMR(0, mr0);
-    seL4_SetMR(1, mr1);
-    seL4_SetMR(2, mr2);
-    seL4_SetMR(3, mr3);
-
-    opt_assign!(sender, badge);
-
-    info
-}
-
-#[inline(always)]
-pub unsafe fn seL4_ReplyWaitWithMRs(dest: seL4_CPtr, msgInfo: seL4_MessageInfo, sender: *mut seL4_Word,
-                                     mr0: *mut seL4_Word, mr1: *mut seL4_Word,
-                                     mr2: *mut seL4_Word, mr3: *mut seL4_Word) -> seL4_MessageInfo {
-    let mut info: seL4_MessageInfo = uninitialized();
-    let mut badge: seL4_Word = uninitialized();
-    let mut msg0: seL4_Word = 0;
-    let mut msg1: seL4_Word = 0;
-    let mut msg2: seL4_Word = 0;
-    let mut msg3: seL4_Word = 0;
-
-    if !mr0.is_null() {
-        if msgInfo.get_length() > 0 {
-            msg0 = *mr0;
-        }
-    }
-    if !mr1.is_null() {
-        if msgInfo.get_length() > 1 {
-            msg1 = *mr1;
-        }
-    }
-    if !mr2.is_null() {
-        if msgInfo.get_length() > 2 {
-            msg2 = *mr2;
-        }
-    }
-    if !mr3.is_null() {
-        if msgInfo.get_length() > 3 {
-            msg3 = *mr3;
-        }
-    }
-
-    x64_sys_send_recv(SyscallId::ReplyRecv as seL4_Word, dest, &mut badge, msgInfo.words[0], &mut info.words[0], &mut msg0, &mut msg1, &mut msg2, &mut msg3);
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::NBSendRecv),
+        inout("rdi") src => badge,
+        inout("rsi") msgInfo.words[0] => info,
+        inout("r10") msg0,
+        inout("r8") msg1,
+        inout("r9") msg2,
+        inout("r15") msg3,
+        in("r12") reply,
+        in("r13") dest,
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _);
 
     opt_assign!(mr0, msg0);
     opt_assign!(mr1, msg1);
@@ -649,175 +831,363 @@ pub unsafe fn seL4_ReplyWaitWithMRs(dest: seL4_CPtr, msgInfo: seL4_MessageInfo,
 
     opt_assign!(sender, badge);
 
-    info
+    seL4_MessageInfo { words: [info] }
+}
+
+#[cfg(feature = "CONFIG_KERNEL_MCS")]
+#[inline(always)]
+pub unsafe fn seL4_NBSendWait(
+    dest: seL4_CPtr,
+    msgInfo: seL4_MessageInfo,
+    src: seL4_CPtr,
+    sender: *mut seL4_Word,
+) -> seL4_MessageInfo {
+    let mut info: seL4_Word;
+    let mut badge: seL4_Word;
+    let mut msg0 = seL4_GetMR(0);
+    let mut msg1 = seL4_GetMR(1);
+    let mut msg2 = seL4_GetMR(2);
+    let mut msg3 = seL4_GetMR(3);
+
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::NBSendWait),
+        inout("rdi") src => badge,
+        inout("rsi") msgInfo.words[0] => info,
+        inout("r10") msg0,
+        inout("r8") msg1,
+        inout("r9") msg2,
+        inout("r15") msg3,
+        in("r12") dest,
+        in("r13") 0,
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _);
+
+    /* Write the message back out to memory. */
+    seL4_SetMR(0, msg0);
+    seL4_SetMR(1, msg1);
+    seL4_SetMR(2, msg2);
+    seL4_SetMR(3, msg3);
+
+    opt_assign!(sender, badge);
+
+    seL4_MessageInfo { words: [info] }
+}
+
+#[cfg(feature = "CONFIG_KERNEL_MCS")]
+#[inline(always)]
+pub unsafe fn seL4_NBSendWaitWithMRs(
+    dest: seL4_CPtr,
+    msgInfo: seL4_MessageInfo,
+    src: seL4_CPtr,
+    sender: *mut seL4_Word,
+    mr0: *mut seL4_Word,
+    mr1: *mut seL4_Word,
+    mr2: *mut seL4_Word,
+    mr3: *mut seL4_Word,
+) -> seL4_MessageInfo {
+    let mut info: seL4_Word;
+    let mut badge: seL4_Word;
+    let mut msg0 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg1 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg2 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg3 = ::core::mem::MaybeUninit::uninit().assume_init();
+    if !mr0.is_null() && msgInfo.get_length() > 0 {
+        msg0 = *mr0;
+    }
+    if !mr1.is_null() && msgInfo.get_length() > 1 {
+        msg1 = *mr1;
+    }
+    if !mr2.is_null() && msgInfo.get_length() > 2 {
+        msg2 = *mr2;
+    }
+    if !mr3.is_null() && msgInfo.get_length() > 3 {
+        msg3 = *mr3;
+    }
+
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::NBSendRecv),
+        inout("rdi") src => badge,
+        inout("rsi") msgInfo.words[0] => info,
+        inout("r10") msg0,
+        inout("r8") msg1,
+        inout("r9") msg2,
+        inout("r15") msg3,
+        in("r12") dest,
+        in("r13") 0,
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _);
+
+    opt_assign!(mr0, msg0);
+    opt_assign!(mr1, msg1);
+    opt_assign!(mr2, msg2);
+    opt_assign!(mr3, msg3);
+
+    opt_assign!(sender, badge);
+
+    seL4_MessageInfo { words: [info] }
 }
 
 #[inline(always)]
 pub unsafe fn seL4_Yield() {
-    x64_sys_null(SyscallId::Yield as seL4_Word);
-    asm!("" ::: "memory" : "volatile");
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::Yield),
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _,
+        options(nomem, nostack),
+    );
 }
 
+#[cfg(feature = "CONFIG_KERNEL_MCS")]
 #[inline(always)]
-pub unsafe fn seL4_VMEnter(vcpu: seL4_CPtr, sender: *mut seL4_Word) -> seL4_Word {
-    let mut fault: seL4_Word = uninitialized();
-    let mut badge: seL4_Word = uninitialized();
-    let mut mr0 = seL4_GetMR(0);
-    let mut mr1 = seL4_GetMR(1);
-    let mut mr2 = seL4_GetMR(2);
-    let mut mr3 = seL4_GetMR(3);
+pub unsafe fn seL4_Wait(src: seL4_CPtr, sender: *mut seL4_Word) -> seL4_MessageInfo {
+    let mut info: seL4_Word;
+    let mut badge: seL4_Word;
+    let mut msg0 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg1 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg2 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg3 = ::core::mem::MaybeUninit::uninit().assume_init();
 
-    x64_sys_send_recv(SyscallId::VMEnter as seL4_Word, vcpu, &mut badge, 0, &mut fault, &mut mr0, &mut mr1, &mut mr2, &mut mr3);
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::Wait),
+        inout("rdi") src => badge,
+        out("rsi") info,
+        inout("r10") msg0,
+        inout("r8") msg1,
+        inout("r9") msg2,
+        inout("r15") msg3,
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _);
 
-    seL4_SetMR(0, mr0);
-    seL4_SetMR(1, mr1);
-    seL4_SetMR(2, mr2);
-    seL4_SetMR(3, mr3);
+    seL4_SetMR(0, msg0);
+    seL4_SetMR(1, msg1);
+    seL4_SetMR(2, msg2);
+    seL4_SetMR(3, msg3);
 
-    if fault == 0 && !sender.is_null() {
-        *sender = badge;
-    }
+    opt_assign!(sender, badge);
 
-    fault
+    seL4_MessageInfo { words: [info] }
 }
 
-//#[inline(always)]
+#[cfg(feature = "CONFIG_KERNEL_MCS")]
+#[inline(always)]
+pub unsafe fn seL4_WaitWithMRs(
+    src: seL4_CPtr,
+    sender: *mut seL4_Word,
+    mr0: *mut seL4_Word,
+    mr1: *mut seL4_Word,
+    mr2: *mut seL4_Word,
+    mr3: *mut seL4_Word,
+) -> seL4_MessageInfo {
+    let mut info: seL4_Word;
+    let mut badge: seL4_Word;
+    let mut msg0 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg1 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg2 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg3 = ::core::mem::MaybeUninit::uninit().assume_init();
+
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::Wait),
+        inout("rdi") src => badge,
+        out("rsi") info,
+        inout("r10") msg0,
+        inout("r8") msg1,
+        inout("r9") msg2,
+        inout("r15") msg3,
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _);
+
+    opt_assign!(mr0, msg0);
+    opt_assign!(mr1, msg1);
+    opt_assign!(mr2, msg2);
+    opt_assign!(mr3, msg3);
+
+    opt_assign!(sender, badge);
+
+    seL4_MessageInfo { words: [info] }
+}
+
+#[cfg(feature = "CONFIG_KERNEL_MCS")]
+#[inline(always)]
+pub unsafe fn seL4_NBWait(src: seL4_CPtr, sender: *mut seL4_Word) -> seL4_MessageInfo {
+    let mut info: seL4_Word;
+    let mut badge: seL4_Word;
+    let mut msg0 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg1 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg2 = ::core::mem::MaybeUninit::uninit().assume_init();
+    let mut msg3 = ::core::mem::MaybeUninit::uninit().assume_init();
+
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::NBWait),
+        inout("rdi") src => badge,
+        out("rsi") info,
+        inout("r10") msg0,
+        inout("r8") msg1,
+        inout("r9") msg2,
+        inout("r15") msg3,
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _);
+
+    seL4_SetMR(0, msg0);
+    seL4_SetMR(1, msg1);
+    seL4_SetMR(2, msg2);
+    seL4_SetMR(3, msg3);
+
+    opt_assign!(sender, badge);
+
+    seL4_MessageInfo { words: [info] }
+}
+
+#[cfg(feature = "CONFIG_PRINTING")]
+#[inline(always)]
 pub unsafe fn seL4_DebugPutChar(c: u8) {
-    let mut unused0 = 0;
-    let mut unused1 = 0;
-    let mut unused2 = 0;
-    let mut unused3 = 0;
-    let mut unused4 = 0;
-    let mut unused5 = 0;
-    x64_sys_send_recv(SyscallId::DebugPutChar as seL4_Word, c as seL4_Word, &mut unused0, 0, &mut
-                      unused1, &mut unused2, &mut unused3, &mut unused4, &mut unused5);
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::DebugPutChar),
+        in("rdi") c as i16,
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _,
+        options(nostack),
+    );
 }
 
+#[cfg(feature = "CONFIG_PRINTING")]
+#[inline(always)]
+pub unsafe fn seL4_DebugDumpScheduler() {
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::DebugDumpScheduler),
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _,
+        options(nomem, nostack),
+    );
+}
+
+#[cfg(feature = "CONFIG_DEBUG_BUILD")]
 #[inline(always)]
 pub unsafe fn seL4_DebugHalt() {
-    x64_sys_null(SyscallId::DebugHalt as seL4_Word);
-    asm!("" ::: "memory" : "volatile");
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::DebugHalt),
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _,
+        options(nomem, nostack),
+    );
 }
 
+#[cfg(feature = "CONFIG_DEBUG_BUILD")]
 #[inline(always)]
 pub unsafe fn seL4_DebugSnapshot() {
-    x64_sys_null(SyscallId::DebugSnapshot as seL4_Word);
-    asm!("" ::: "%esi", "%edi", "memory" : "volatile");
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::DebugSnapshot),
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _,
+        options(nomem, nostack),
+    );
 }
 
+#[cfg(feature = "CONFIG_DEBUG_BUILD")]
 #[inline(always)]
 pub unsafe fn seL4_DebugCapIdentify(mut cap: seL4_CPtr) -> u32 {
-    let mut unused0 = 0;
-    let mut unused1 = 0;
-    let mut unused2 = 0;
-    let mut unused3 = 0;
-    let mut unused4 = 0;
-    x64_sys_send_recv(SyscallId::DebugCapIdentify as seL4_Word, 
-                      cap, &mut cap, 0, &mut unused0, &mut unused1, &mut unused2, &mut unused3, &mut unused4);
-    cap as u32
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::DebugCapIdentify),
+        inout("rdi") cap,
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _,
+        options(nomem, nostack),
+    );
+    cap as _
 }
 
-/// Note: name MUST be NUL-terminated.
+// Note: name MUST be NUL-terminated.
+#[cfg(feature = "CONFIG_DEBUG_BUILD")]
 #[inline(always)]
 pub unsafe fn seL4_DebugNameThread(tcb: seL4_CPtr, name: &[u8]) {
-    core::ptr::copy_nonoverlapping(name.as_ptr() as *mut u8, (&mut (*seL4_GetIPCBuffer()).msg).as_mut_ptr() as *mut u8,name.len());
-    let mut unused0 = 0;
-    let mut unused1 = 0;
-    let mut unused2 = 0;
-    let mut unused3 = 0;
-    let mut unused4 = 0;
-    let mut unused5 = 0;
-    x64_sys_send_recv(SyscallId::DebugNameThread as seL4_Word, tcb, &mut unused0, 0, &mut unused1,
-                      &mut unused2, &mut unused3, &mut unused4, &mut unused5);
+    core::ptr::copy_nonoverlapping(
+        name.as_ptr() as *mut u8,
+        (&mut (*seL4_GetIPCBuffer()).msg).as_mut_ptr() as *mut u8,
+        name.len(),
+    );
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::DebugNameThread),
+        in("rdi") tcb,
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _,
+    );
 }
 
+#[cfg(feature = "CONFIG_DANGEROUS_CODE_INJECTION")]
 #[inline(always)]
-#[cfg(feature = "SEL4_DANGEROUS_CODE_INJECTION")]
-pub unsafe fn seL4_DebugRun(userfn: extern fn(*mut u8), userarg: *mut u8) {
+pub unsafe fn seL4_DebugRun(userfn: extern "C" fn(*mut u8), userarg: *mut u8) {
     let userfnptr = userfn as *mut ();
-    x64_sys_send_null(SyscallId::DebugRun as seL4_Word, userfnptr as seL4_Word, userarg as seL4_Word);
-    asm!("" ::: "memory" : "volatile");
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::DebugRun),
+        in("rdi") userfnptr,
+        in("r10") userfnptr,
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _,
+    );
 }
 
+#[cfg(feature = "CONFIG_ENABLE_BENCHMARKS")]
 #[inline(always)]
-#[cfg(feature = "SEL4_CONFIG_BENCHMARK")]
-pub unsafe fn seL4_BenchmarkResetLog() -> seL4_Word {
-    let mut unused0 = 0;
-    let mut unused1 = 0;
-    let mut unused2 = 0;
-    let mut unused3 = 0;
-    let mut unused4 = 0;
-
-    let mut ret = 0;
-
-    x64_sys_send_recv(SyscallId::BenchmarkResetLog as seL4_Word, 0, &mut ret, 0, &mut unused0, &mut unused1, &mut unused2, &mut unused3, &mut unused4);
-
-    ret
+pub unsafe fn seL4_BenchmarkResetLog() {
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::BenchmarkResetLog),
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _,
+        options(nomem, nostack),
+    );
 }
 
+#[cfg(feature = "CONFIG_ENABLE_BENCHMARKS")]
 #[inline(always)]
-#[cfg(feature = "SEL4_CONFIG_BENCHMARK")]
 pub unsafe fn seL4_BenchmarkFinalizeLog() {
-    let mut unused0 = 0;
-    let mut unused1 = 0;
-    let mut unused2 = 0;
-    let mut unused3 = 0;
-    let mut unused4 = 0;
-    let mut index_ret = 0;
-    x64_sys_send_recv(SyscallId::BenchmarkFinalizeLog as seL4_Word, 0, &mut index_ret, &mut unused0, &mut unused1, &mut unused2, &mut unused3, &mut unused4);
-}
-
-#[inline(always)]
-#[cfg(feature = "SEL4_CONFIG_BENCHMARK")]
-pub unsafe fn seL4_BenchmarkSetLogBuffer(mut frame_cptr: seL4_Word) -> seL4_Word {
-    let mut unused0 = 0;
-    let mut unused1 = 0;
-    let mut unused2 = 0;
-    let mut unused3 = 0;
-    let mut unused4 = 0;
-
-    x64_sys_send_recv(SyscallId::BenchmarkSetLogBuffer as seL4_Word, 
-                      frame_cptr, &mut frame_cptr, 0, &mut unused0, &mut unused1, &mut unused2, &mut unused3, &mut unused4);
-    frame_cptr
-}
-
-#[inline(always)]
-#[cfg(feature = "SEL4_CONFIG_BENCHMARK")]
-pub unsafe fn seL4_BenchmarkNullSyscall() {
-    x64_sys_null(SyscallId::BenchmarkNullSyscall as seL4_Word);
-    asm!("" ::: "memory" : "volatile");
-}
-
-#[inline(always)]
-#[cfg(feature = "SEL4_CONFIG_BENCHMARK")]
-pub unsafe fn seL4_BenchmarkFlushCaches() {
-    x64_sys_null(SyscallId::BenchmarkFlushCaches as seL4_Word);
-    asm!("" ::: "%esi", "%edi", "memory" : "volatile");
-}
-
-#[inline(always)]
-#[cfg(feature = "SEL4_CONFIG_BENCHMARK")]
-pub unsafe fn seL4_BenchmarkGetThreadUtilization(tcb: seL4_Word) {
-    let mut unused0 = 0;
-    let mut unused1 = 0;
-    let mut unused2 = 0;
-    let mut unused3 = 0;
-    let mut unused4 = 0;
-    let mut unused5 = 0;
-    x64_sys_send_recv(SyscallId::BenchmarkGetThreadUtilisation as seL4_Word, tcb, &mut unused0, 0,
-                      &mut unused1, &mut unused2, &mut unused3, &mut unused3, &mut unused4, &mut unused5);
-}
-
-#[inline(always)]
-#[cfg(feature = "SEL4_CONFIG_BENCHMARK")]
-pub unsafe fn seL4_BenchmarkGetThreadUtilization(tcb: seL4_Word) {
-    let mut unused0 = 0;
-    let mut unused1 = 0;
-    let mut unused2 = 0;
-    let mut unused3 = 0;
-    let mut unused4 = 0;
-    let mut unused5 = 0;
-
-    x64_sys_send_recv(SyscallId::BenchmarkResetThreadUtilisation as seL4_Word, tcb, &mut unused0, 0,
-                      &mut unused1, &mut unused2, &mut unused3, &mut unused4, &mut unused5);
+    asm!("mov r14, rsp
+          syscall
+          mov rsp, r14",
+        in("rdx") swinum!(SyscallId::BenchmarkFinalizeLog),
+        lateout("rcx") _,
+        lateout("r11") _,
+        lateout("r14") _,
+        options(nomem, nostack),
+    );
 }