diff --git a/apps/system/components/kata-os-common/src/sel4-sys/arch/aarch64.rs b/apps/system/components/kata-os-common/src/sel4-sys/arch/aarch64.rs
index 2a1b877..af2da58 100644
--- a/apps/system/components/kata-os-common/src/sel4-sys/arch/aarch64.rs
+++ b/apps/system/components/kata-os-common/src/sel4-sys/arch/aarch64.rs
@@ -262,6 +262,14 @@ macro_rules! swinum {
     };
 }
 
+macro_rules! opt_assign {
+    ($loc:expr, $val:expr) => {
+        if !$loc.is_null() {
+            *$loc = $val;
+        }
+    };
+}
+
 #[inline(always)]
 pub unsafe fn seL4_Send(dest: seL4_CPtr, msgInfo: seL4_MessageInfo) {
     asm!("svc 0",
@@ -275,14 +283,6 @@ pub unsafe fn seL4_Send(dest: seL4_CPtr, msgInfo: seL4_MessageInfo) {
     );
 }
 
-macro_rules! opt_assign {
-    ($loc:expr, $val:expr) => {
-        if !$loc.is_null() {
-            *$loc = $val;
-        }
-    };
-}
-
 #[inline(always)]
 pub unsafe fn seL4_SendWithMRs(
     dest: seL4_CPtr,
@@ -372,56 +372,6 @@ pub unsafe fn seL4_NBSendWithMRs(
     );
 }
 
-#[cfg(not(feature = "CONFIG_KERNEL_MCS"))]
-#[inline(always)]
-pub unsafe fn seL4_Reply(msgInfo: seL4_MessageInfo) {
-    asm!("svc 0",
-        in("x7") swinum!(SyscallId::Reply),
-        in("x1") msgInfo.words[0],
-        in("x2") seL4_GetMR(0),
-        in("x3") seL4_GetMR(1),
-        in("x4") seL4_GetMR(2),
-        in("x5") seL4_GetMR(3),
-    );
-}
-
-#[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,
-) {
-    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!("svc 0",
-        in("x7") swinum!(SyscallId::Reply),
-        in("x1") msgInfo.words[0],
-        in("x2") msg0,
-        in("x3") msg1,
-        in("x4") msg2,
-        in("x5") msg3,
-    );
-}
-
 #[inline(always)]
 pub unsafe fn seL4_Signal(dest: seL4_CPtr) {
     let info = seL4_MessageInfo::new(0, 0, 0, 0).words[0];
@@ -432,62 +382,6 @@ pub unsafe fn seL4_Signal(dest: seL4_CPtr) {
     )
 }
 
-#[inline(always)]
-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();
-
-    asm!("svc 0",
-        in("x7") swinum!(SyscallId::Recv),
-        out("x0") src,
-        out("x1") info,
-        out("x2") msg0,
-        out("x3") msg1,
-        out("x4") msg2,
-        out("x5") msg3
-    );
-
-    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_NBRecv(mut src: seL4_CPtr, sender: *mut seL4_Word) -> seL4_MessageInfo {
-    let 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();
-
-    asm!("svc 0",
-        in("x7") swinum!(SyscallId::NBRecv),
-        inout("x0") src,
-        out("x1") info,
-        out("x2") msg0,
-        out("x3") msg1,
-        out("x4") msg2,
-        out("x5") msg3
-    );
-
-    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;
@@ -560,271 +454,6 @@ pub unsafe fn seL4_CallWithMRs(
     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!("svc 0",
-        in("x7") swinum!(SyscallId::ReplyRecv),
-        inout("x0") src,
-        inout("x1") msgInfo.words[0] => info,
-        inout("x2") msg0,
-        inout("x3") msg1,
-        inout("x4") msg2,
-        inout("x5") msg3
-    );
-
-    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!("svc 0",
-        in("x7") swinum!(SyscallId::ReplyRecv),
-        inout("x0") src => badge,
-        inout("x1") msgInfo.words[0] => info,
-        inout("x2") msg0,
-        inout("x3") msg1,
-        inout("x4") msg2,
-        inout("x5") msg3
-    );
-
-    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_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);
-
-    asm!("svc 0",
-        in("x7") swinum!(SyscallId::NBSendRecv),
-        inout("x0") src => badge,
-        inout("x1") msgInfo.words[0] => info,
-        inout("x2") msg0,
-        inout("x3") msg1,
-        inout("x4") msg2,
-        inout("x5") msg3,
-        in("x6") reply,
-        in("x8") dest,
-    );
-
-    /* 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_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() && 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!("svc 0",
-        in("x7") swinum!(SyscallId::NBSendRecv),
-        inout("x0") src => badge,
-        inout("x1") msgInfo.words[0] => info,
-        inout("x2") msg0,
-        inout("x3") msg1,
-        inout("x4") msg2,
-        inout("x5") msg3,
-        in("x6") reply,
-        in("x8") dest,
-    );
-
-    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_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!("svc 0",
-        in("x7") swinum!(SyscallId::NBSendWait),
-        inout("x0") src => badge,
-        inout("x1") msgInfo.words[0] => info,
-        inout("x2") msg0,
-        inout("x3") msg1,
-        inout("x4") msg2,
-        inout("x5") msg3,
-        in("x6") dest,
-        in("x8") 0,  // XXX dest
-    );
-
-    /* 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!("svc 0",
-        in("x7") swinum!(SyscallId::NBSendRecv),
-        inout("x0") src => badge,
-        inout("x1") msgInfo.words[0] => info,
-        inout("x2") msg0,
-        inout("x3") msg1,
-        inout("x4") msg2,
-        inout("x5") msg3,
-        in("x6") dest,
-        in("x8") 0,  // XXX does this dtrt
-    );
-
-    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() {
     asm!("svc 0",
@@ -833,174 +462,86 @@ pub unsafe fn seL4_Yield() {
     );
 }
 
-#[cfg(feature = "CONFIG_KERNEL_MCS")]
-#[inline(always)]
-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();
-
-    asm!("svc 0",
-        in("x7") swinum!(SyscallId::Wait),
-        inout("x0") src => badge,
-        out("x1") info,
-        inout("x2") msg0,
-        inout("x3") msg1,
-        inout("x4") msg2,
-        inout("x5") msg3,
-    );
-
-    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_if! {
+    if #[cfg(feature = "CONFIG_KERNEL_MCS")] {
+        include!("aarch64_mcs.rs");
+    } else {
+        include!("aarch64_no_mcs.rs");
+    }
 }
 
-#[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();
+cfg_if! {
+    if #[cfg(feature = "CONFIG_PRINTING")] {
+        #[inline(always)]
+        pub unsafe fn seL4_DebugPutChar(c: u8) {
+            asm!("svc 0",
+                in("x7") swinum!(SyscallId::DebugPutChar),
+                in("x0") c,
+                options(nostack),
+            );
+        }
 
-    asm!("svc 0",
-        in("x7") swinum!(SyscallId::Wait),
-        inout("x0") src => badge,
-        out("x1") info,
-        inout("x2") msg0,
-        inout("x3") msg1,
-        inout("x4") msg2,
-        inout("x5") msg3,
-    );
+        #[inline(always)]
+        pub unsafe fn seL4_DebugDumpScheduler() {
+            asm!("svc 0",
+                in("x7") swinum!(SyscallId::DebugDumpScheduler),
+                options(nomem, nostack),
+            );
+        }
 
-    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_DebugDumpCNode(mut cap: seL4_CPtr) {
+            asm!("svc 0",
+                in("x7") swinum!(SyscallId::DebugDumpCNode),
+                inout("x0") cap,
+                options(nomem, nostack),
+            );
+        }
+    } // CONFIG_PRINTING
 }
 
-#[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();
+cfg_if! {
+    if #[cfg(feature = "CONFIG_DEBUG_BUILD")] {
+        #[inline(always)]
+        pub unsafe fn seL4_DebugHalt() {
+            asm!("svc 0",
+                in("x7") swinum!(SyscallId::DebugHalt),
+                options(nomem, nostack),
+            );
+        }
 
-    asm!("svc 0",
-        in("x7") swinum!(SyscallId::NBWait),
-        inout("x0") src => badge,
-        out("x1") info,
-        inout("x2") msg0,
-        inout("x3") msg1,
-        inout("x4") msg2,
-        inout("x5") msg3,
-    );
+        #[inline(always)]
+        pub unsafe fn seL4_DebugSnapshot() {
+            asm!("svc 0",
+                in("x7") swinum!(SyscallId::DebugSnapshot),
+                options(nomem, nostack),
+            );
+        }
 
-    seL4_SetMR(0, msg0);
-    seL4_SetMR(1, msg1);
-    seL4_SetMR(2, msg2);
-    seL4_SetMR(3, msg3);
+        #[inline(always)]
+        pub unsafe fn seL4_DebugCapIdentify(mut cap: seL4_CPtr) -> u32 {
+            asm!("svc 0",
+                in("x7") swinum!(SyscallId::DebugCapIdentify),
+                inout("x0") cap,
+                options(nomem, nostack),
+            );
+            cap as _
+        }
 
-    opt_assign!(sender, badge);
-
-    seL4_MessageInfo { words: [info] }
-}
-
-#[cfg(feature = "CONFIG_PRINTING")]
-#[inline(always)]
-pub unsafe fn seL4_DebugPutChar(c: u8) {
-    asm!("svc 0",
-        in("x7") swinum!(SyscallId::DebugPutChar),
-        in("x0") c,
-        options(nostack),
-    );
-}
-
-#[cfg(feature = "CONFIG_PRINTING")]
-#[inline(always)]
-pub unsafe fn seL4_DebugDumpScheduler() {
-    asm!("svc 0",
-        in("x7") swinum!(SyscallId::DebugDumpScheduler),
-        options(nomem, nostack),
-    );
-}
-
-#[cfg(feature = "CONFIG_DEBUG_BUILD")]
-#[inline(always)]
-pub unsafe fn seL4_DebugHalt() {
-    asm!("svc 0",
-        in("x7") swinum!(SyscallId::DebugHalt),
-        options(nomem, nostack),
-    );
-}
-
-#[cfg(feature = "CONFIG_DEBUG_BUILD")]
-#[inline(always)]
-pub unsafe fn seL4_DebugSnapshot() {
-    asm!("svc 0",
-        in("x7") swinum!(SyscallId::DebugSnapshot),
-        options(nomem, nostack),
-    );
-}
-
-#[cfg(feature = "CONFIG_DEBUG_BUILD")]
-#[inline(always)]
-pub unsafe fn seL4_DebugCapIdentify(mut cap: seL4_CPtr) -> u32 {
-    asm!("svc 0",
-        in("x7") swinum!(SyscallId::DebugCapIdentify),
-        inout("x0") cap,
-        options(nomem, nostack),
-    );
-    cap as _
-}
-
-#[cfg(feature = "CONFIG_PRINTING")]
-#[inline(always)]
-pub unsafe fn seL4_DebugDumpCNode(mut cap: seL4_CPtr) {
-    asm!("svc 0",
-        in("x7") swinum!(SyscallId::DebugDumpCNode),
-        inout("x0") cap,
-        options(nomem, nostack),
-    );
-}
-
-// 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(),
-    );
-    asm!("svc 0",
-        in("x7") swinum!(SyscallId::DebugNameThread),
-        in("x0") tcb,
-    );
+        // Note: name MUST be NUL-terminated.
+        #[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(),
+            );
+            asm!("svc 0",
+                in("x7") swinum!(SyscallId::DebugNameThread),
+                in("x0") tcb,
+            );
+        }
+    } // CONFIG_DEBUG_BUILD
 }
 
 #[cfg(feature = "CONFIG_DANGEROUS_CODE_INJECTION")]
@@ -1014,20 +555,22 @@ pub unsafe fn seL4_DebugRun(userfn: extern "C" fn(*mut u8), userarg: *mut u8) {
     );
 }
 
-#[cfg(feature = "CONFIG_ENABLE_BENCHMARKS")]
-#[inline(always)]
-pub unsafe fn seL4_BenchmarkResetLog() {
-    asm!("svc 0",
-        in("x7") swinum!(SyscallId::BenchmarkResetLog),
-        options(nomem, nostack),
-    );
-}
+cfg_if! {
+    if #[cfg(feature = "CONFIG_ENABLE_BENCHMARKS")] {
+        #[inline(always)]
+        pub unsafe fn seL4_BenchmarkResetLog() {
+            asm!("svc 0",
+                in("x7") swinum!(SyscallId::BenchmarkResetLog),
+                options(nomem, nostack),
+            );
+        }
 
-#[cfg(feature = "CONFIG_ENABLE_BENCHMARKS")]
-#[inline(always)]
-pub unsafe fn seL4_BenchmarkFinalizeLog() {
-    asm!("svc 0",
-        in("x7") swinum!(SyscallId::BenchmarkFinalizeLog),
-        options(nomem, nostack),
-    );
+        #[inline(always)]
+        pub unsafe fn seL4_BenchmarkFinalizeLog() {
+            asm!("svc 0",
+                in("x7") swinum!(SyscallId::BenchmarkFinalizeLog),
+                options(nomem, nostack),
+            );
+        }
+    } // CONFIG_ENABLE_BENCHMARKS
 }
diff --git a/apps/system/components/kata-os-common/src/sel4-sys/arch/aarch64_mcs.rs b/apps/system/components/kata-os-common/src/sel4-sys/arch/aarch64_mcs.rs
new file mode 100644
index 0000000..887c9a4
--- /dev/null
+++ b/apps/system/components/kata-os-common/src/sel4-sys/arch/aarch64_mcs.rs
@@ -0,0 +1,443 @@
+/*
+ * Copyright 2015, Killian Coddington
+ * Copyright 2014, NICTA
+ *
+ * This software may be distributed and modified according to the terms of
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
+ *
+ * @TAG(NICTA_BSD)
+ */
+
+assert_cfg!(feature = "CONFIG_KERNEL_MCS");
+
+#[inline(always)]
+pub unsafe fn seL4_Recv(
+    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 = ::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!("svc 0",
+        in("x7") swinum!(SyscallId::Recv),
+        inout("x0") src => badge,
+        out("x1") info,
+        out("x2") msg0,
+        out("x3") msg1,
+        out("x4") msg2,
+        out("x5") msg3,
+        in("x6") reply,
+    );
+
+    seL4_SetMR(0, msg0);
+    seL4_SetMR(1, msg1);
+    seL4_SetMR(2, msg2);
+    seL4_SetMR(3, msg3);
+
+    opt_assign!(sender, badge);
+
+    seL4_MessageInfo { words: [info] }
+}
+
+#[inline(always)]
+pub unsafe fn seL4_NBRecv(
+    src: seL4_CPtr,
+    sender: *mut seL4_Word,
+    reply: seL4_CPtr,
+) -> seL4_MessageInfo {
+    let 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!("svc 0",
+        in("x7") swinum!(SyscallId::NBRecv),
+        inout("x0") src => badge,
+        out("x1") info,
+        out("x2") msg0,
+        out("x3") msg1,
+        out("x4") msg2,
+        out("x5") msg3,
+        in("x6") reply,
+    );
+
+    seL4_SetMR(0, msg0);
+    seL4_SetMR(1, msg1);
+    seL4_SetMR(2, msg2);
+    seL4_SetMR(3, msg3);
+
+    opt_assign!(sender, badge);
+
+    seL4_MessageInfo { words: [info] }
+}
+
+#[inline(always)]
+pub unsafe fn seL4_ReplyRecv(
+    src: seL4_CPtr,
+    msgInfo: seL4_MessageInfo,
+    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);
+
+    asm!("svc 0",
+        in("x7") swinum!(SyscallId::ReplyRecv),
+        inout("x0") src => badge,
+        inout("x1") msgInfo.words[0] => info,
+        inout("x2") msg0,
+        inout("x3") msg1,
+        inout("x4") msg2,
+        inout("x5") msg3,
+        in("x6") reply,
+    );
+
+    seL4_SetMR(0, msg0);
+    seL4_SetMR(1, msg1);
+    seL4_SetMR(2, msg2);
+    seL4_SetMR(3, msg3);
+
+    opt_assign!(sender, badge);
+
+    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,
+    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() && 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!("svc 0",
+        in("x7") swinum!(SyscallId::ReplyRecv),
+        inout("x0") src => badge,
+        inout("x1") msgInfo.words[0] => info,
+        inout("x2") msg0,
+        inout("x3") msg1,
+        inout("x4") msg2,
+        inout("x5") msg3,
+        in("x6") reply,
+    );
+
+    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_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);
+
+    asm!("svc 0",
+        in("x7") swinum!(SyscallId::NBSendRecv),
+        inout("x0") src => badge,
+        inout("x1") msgInfo.words[0] => info,
+        inout("x2") msg0,
+        inout("x3") msg1,
+        inout("x4") msg2,
+        inout("x5") msg3,
+        in("x6") reply,
+        in("x8") dest,
+    );
+
+    /* 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] }
+}
+
+#[inline(always)]
+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() && 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!("svc 0",
+        in("x7") swinum!(SyscallId::NBSendRecv),
+        inout("x0") src => badge,
+        inout("x1") msgInfo.words[0] => info,
+        inout("x2") msg0,
+        inout("x3") msg1,
+        inout("x4") msg2,
+        inout("x5") msg3,
+        in("x6") reply,
+        in("x8") dest,
+    );
+
+    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_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!("svc 0",
+        in("x7") swinum!(SyscallId::NBSendWait),
+        inout("x0") src => badge,
+        inout("x1") msgInfo.words[0] => info,
+        inout("x2") msg0,
+        inout("x3") msg1,
+        inout("x4") msg2,
+        inout("x5") msg3,
+        in("x6") dest,
+        in("x8") 0,  // XXX dest
+    );
+
+    /* 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] }
+}
+
+#[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!("svc 0",
+        in("x7") swinum!(SyscallId::NBSendRecv),
+        inout("x0") src => badge,
+        inout("x1") msgInfo.words[0] => info,
+        inout("x2") msg0,
+        inout("x3") msg1,
+        inout("x4") msg2,
+        inout("x5") msg3,
+        in("x6") dest,
+        in("x8") 0,  // XXX does this dtrt
+    );
+
+    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_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();
+
+    asm!("svc 0",
+        in("x7") swinum!(SyscallId::Wait),
+        inout("x0") src => badge,
+        out("x1") info,
+        inout("x2") msg0,
+        inout("x3") msg1,
+        inout("x4") msg2,
+        inout("x5") msg3,
+        in("x6") 0,  // XXX needed?
+    );
+
+    seL4_SetMR(0, msg0);
+    seL4_SetMR(1, msg1);
+    seL4_SetMR(2, msg2);
+    seL4_SetMR(3, msg3);
+
+    opt_assign!(sender, badge);
+
+    seL4_MessageInfo { words: [info] }
+}
+
+#[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!("svc 0",
+        in("x7") swinum!(SyscallId::Wait),
+        inout("x0") src => badge,
+        out("x1") info,
+        inout("x2") msg0,
+        inout("x3") msg1,
+        inout("x4") msg2,
+        inout("x5") msg3,
+        in("x6") 0,  // XXX needed?
+    );
+
+    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_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!("svc 0",
+        in("x7") swinum!(SyscallId::NBWait),
+        inout("x0") src => badge,
+        out("x1") info,
+        inout("x2") msg0,
+        inout("x3") msg1,
+        inout("x4") msg2,
+        inout("x5") msg3,
+        in("x6") 0,  // XXX needed?
+    );
+
+    seL4_SetMR(0, msg0);
+    seL4_SetMR(1, msg1);
+    seL4_SetMR(2, msg2);
+    seL4_SetMR(3, msg3);
+
+    opt_assign!(sender, badge);
+
+    seL4_MessageInfo { words: [info] }
+}
diff --git a/apps/system/components/kata-os-common/src/sel4-sys/arch/aarch64_no_mcs.rs b/apps/system/components/kata-os-common/src/sel4-sys/arch/aarch64_no_mcs.rs
new file mode 100644
index 0000000..d544e54
--- /dev/null
+++ b/apps/system/components/kata-os-common/src/sel4-sys/arch/aarch64_no_mcs.rs
@@ -0,0 +1,200 @@
+/*
+ * Copyright 2015, Killian Coddington
+ * Copyright 2014, NICTA
+ *
+ * This software may be distributed and modified according to the terms of
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
+ *
+ * @TAG(NICTA_BSD)
+ */
+
+assert_cfg!(not(feature = "CONFIG_KERNEL_MCS"));
+
+#[inline(always)]
+pub unsafe fn seL4_Reply(msgInfo: seL4_MessageInfo) {
+    asm!("svc 0",
+        in("x7") swinum!(SyscallId::Reply),
+        in("x1") msgInfo.words[0],
+        in("x2") seL4_GetMR(0),
+        in("x3") seL4_GetMR(1),
+        in("x4") seL4_GetMR(2),
+        in("x5") seL4_GetMR(3),
+    );
+}
+
+#[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,
+) {
+    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!("svc 0",
+        in("x7") swinum!(SyscallId::Reply),
+        in("x1") msgInfo.words[0],
+        in("x2") msg0,
+        in("x3") msg1,
+        in("x4") msg2,
+        in("x5") msg3,
+    );
+}
+
+#[inline(always)]
+pub unsafe fn seL4_Recv(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!("svc 0",
+        in("x7") swinum!(SyscallId::Recv),
+        inout("x0") src => badge,
+        out("x1") info,
+        out("x2") msg0,
+        out("x3") msg1,
+        out("x4") msg2,
+        out("x5") msg3
+    );
+
+    seL4_SetMR(0, msg0);
+    seL4_SetMR(1, msg1);
+    seL4_SetMR(2, msg2);
+    seL4_SetMR(3, msg3);
+
+    opt_assign!(sender, badge);
+
+    seL4_MessageInfo { words: [info] }
+}
+
+#[inline(always)]
+pub unsafe fn seL4_NBRecv(src: seL4_CPtr, sender: *mut seL4_Word) -> seL4_MessageInfo {
+    let 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!("svc 0",
+        in("x7") swinum!(SyscallId::NBRecv),
+        inout("x0") src => badge,
+        out("x1") info,
+        out("x2") msg0,
+        out("x3") msg1,
+        out("x4") msg2,
+        out("x5") msg3
+    );
+
+    seL4_SetMR(0, msg0);
+    seL4_SetMR(1, msg1);
+    seL4_SetMR(2, msg2);
+    seL4_SetMR(3, msg3);
+
+    opt_assign!(sender, badge);
+
+    seL4_MessageInfo { words: [info] }
+}
+
+#[inline(always)]
+pub unsafe fn seL4_ReplyRecv(
+    src: seL4_CPtr,
+    msgInfo: seL4_MessageInfo,
+    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!("svc 0",
+        in("x7") swinum!(SyscallId::ReplyRecv),
+        inout("x0") src => badge,
+        inout("x1") msgInfo.words[0] => info,
+        inout("x2") msg0,
+        inout("x3") msg1,
+        inout("x4") msg2,
+        inout("x5") msg3
+    );
+
+    seL4_SetMR(0, msg0);
+    seL4_SetMR(1, msg1);
+    seL4_SetMR(2, msg2);
+    seL4_SetMR(3, msg3);
+
+    opt_assign!(sender, badge);
+
+    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!("svc 0",
+        in("x7") swinum!(SyscallId::ReplyRecv),
+        inout("x0") src => badge,
+        inout("x1") msgInfo.words[0] => info,
+        inout("x2") msg0,
+        inout("x3") msg1,
+        inout("x4") msg2,
+        inout("x5") msg3
+    );
+
+    opt_assign!(mr0, msg0);
+    opt_assign!(mr1, msg1);
+    opt_assign!(mr2, msg2);
+    opt_assign!(mr3, msg3);
+
+    opt_assign!(sender, badge);
+
+    seL4_MessageInfo { words: [info] }
+}