diff --git a/libsel4/Kconfig b/libsel4/Kconfig
index d58affd0d..383a07212 100644
--- a/libsel4/Kconfig
+++ b/libsel4/Kconfig
@@ -26,18 +26,6 @@ config LIB_SEL4_INLINE_INVOCATIONS
         for verification, so setting to 'n' will forcively prevent the function
         from being inlined
 
-config LIB_SEL4_HAVE_REGISTER_STUBS
-    bool "Support syscall stubs without IPC buffer"
-    depends on LIB_SEL4 && !USER_OPTIMISATION_O0 && ARCH_ARM
-    default y
-    help
-        Generate the 'WithMRs' variants of the syscall stubs. These stubs
-        avoid the use of the IPC buffer where possible and attempt to
-        place syscall arguments directly into and out of cpu registers.
-        GCC's register allocation is a hint only and cannot be relied upon,
-        as a result these stubs are known to be broken, and are disabled,
-        at -O0
-
 config HAVE_LIB_SEL4
     bool
 endmenu
diff --git a/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/syscalls.h b/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/syscalls.h
index a29e5b5a6..298357c6c 100644
--- a/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/syscalls.h
+++ b/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/syscalls.h
@@ -15,224 +15,236 @@
 #include <sel4/arch/functions.h>
 #include <sel4/types.h>
 
-#define __SEL4_SWINUM(x) ((x) & 0x00ffffff)
-
-#ifndef __OPTIMIZE__
-/* With no optimisations (-O0) GCC's register allocator clobbers the
- * syscall arguments before you reach the 'swi' and you invoke the kernel
- * incorrectly.
- * See SELFOUR-187
+/*
+ * To simplify the definition of the various seL4 syscalls/syscall-wrappers we define
+ * some helper assembly functions. These functions are designed to cover the different
+ * cases of sending/receiving data in registers to/from the kernel. The most 'complex'
+ * version is arm_sys_send_recv, and all other functions are limited versions that allow
+ * for registers to not be unnecessarily clobbered
+ *
+ * arm_sys_send: Fills all registers into the kernel, expects nothing to be sent back
+ *      by the kernel. Used for direction one way sends that contain data (e.g. seL4_Send,
+ *      seL4_NBSend)
+ *
+ * arm_sys_send_null: Only fills metadata registers into the kernel (skips message
+ *      registers). Expects nothing to be sent back by the kernel. Used by directional
+ *      one way sends that do not contain data (e.g. seL4_Notify)
+ *
+ * arm_sys_reply: Similar to arm_sys_send except it does not take a word for the
+ *      destination register. Used for undirected one way sends that contain data
+ *      (e.g. seL4_Reply)
+ *
+ * arm_sys_recv: Sends one register (destination) to the kernel and expects all
+ *      registers to be returned by the kernel. Used for directed receives that return
+ *      data (e.g. seL4_Recv)
+ *
+ * arm_sys_send_recv: Fills all registers into the kernel and expects all of them
+ *      to be filled on return by the kernel. Used for directed send+receives
+ *      where data flows both directions (e.g. seL4_Call, seL4_ReplyWait)
+ *
+ * arm_sys_null: Does not send any registers to the kernel or expect anything to
+ *      be returned from the kernel. Used to trigger implicit kernel actions without
+ *      any data (e.g. seL4_Yield)
  */
-#warning you are compiling with -O0; syscalls will most likely not work
-#endif
+
+static inline void
+arm_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info_arg, seL4_Word mr0, seL4_Word mr1, seL4_Word mr2, seL4_Word mr3)
+{
+    register seL4_Word destptr asm("r0") = dest;
+    register seL4_Word info asm("r1") = info_arg;
+
+    /* Load beginning of the message into registers. */
+    register seL4_Word msg0 asm("r2") = mr0;
+    register seL4_Word msg1 asm("r3") = mr1;
+    register seL4_Word msg2 asm("r4") = mr2;
+    register seL4_Word msg3 asm("r5") = mr3;
+
+    /* Perform the system call. */
+    register seL4_Word scno asm("r7") = sys;
+    asm volatile (
+        "swi $0"
+        : "+r" (destptr), "+r" (msg0), "+r" (msg1), "+r" (msg2),
+          "+r" (msg3), "+r" (info)
+        : "r"(scno)
+    );
+}
+
+static inline void arm_sys_reply(seL4_Word sys, seL4_Word info_arg, seL4_Word mr0, seL4_Word mr1, seL4_Word mr2, seL4_Word mr3)
+{
+    register seL4_Word info asm("r1") = info_arg;
+
+    /* Load beginning of the message into registers. */
+    register seL4_Word msg0 asm("r2") = mr0;
+    register seL4_Word msg1 asm("r3") = mr1;
+    register seL4_Word msg2 asm("r4") = mr2;
+    register seL4_Word msg3 asm("r5") = mr3;
+
+    /* Perform the system call. */
+    register seL4_Word scno asm("r7") = sys;
+    asm volatile (
+        "swi $0"
+        : "+r" (msg0), "+r" (msg1), "+r" (msg2), "+r" (msg3),
+          "+r" (info)
+        : "r"(scno)
+    );
+}
+
+static inline void
+arm_sys_send_null(seL4_Word sys, seL4_Word src, seL4_Word info_arg)
+{
+    register seL4_Word destptr asm("r0") = src;
+    register seL4_Word info asm("r1") = info_arg;
+
+    /* Perform the system call. */
+    register seL4_Word scno asm("r7") = sys;
+    asm volatile (
+        "swi $0"
+        : "+r" (destptr), "+r" (info)
+        : "r"(scno)
+    );
+}
+
+static inline void
+arm_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word *out_info, seL4_Word *out_mr0, seL4_Word *out_mr1, seL4_Word *out_mr2, seL4_Word *out_mr3)
+{
+    register seL4_Word src_and_badge asm("r0") = src;
+    register seL4_Word info asm("r1");
+
+    /* Incoming message registers. */
+    register seL4_Word msg0 asm("r2");
+    register seL4_Word msg1 asm("r3");
+    register seL4_Word msg2 asm("r4");
+    register seL4_Word msg3 asm("r5");
+
+    /* Perform the system call. */
+    register seL4_Word scno asm("r7") = sys;
+    asm volatile (
+        "swi $0"
+        : "=r" (msg0), "=r" (msg1), "=r" (msg2), "=r" (msg3),
+          "=r" (info), "+r" (src_and_badge)
+        : "r"(scno)
+        : "memory"
+    );
+    *out_badge = src_and_badge;
+    *out_info = info;
+    *out_mr0 = msg0;
+    *out_mr1 = msg1;
+    *out_mr2 = msg2;
+    *out_mr3 = msg3;
+}
+
+static inline void
+arm_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *out_badge, seL4_Word info_arg, seL4_Word *out_info, seL4_Word *in_out_mr0, seL4_Word *in_out_mr1, seL4_Word *in_out_mr2, seL4_Word *in_out_mr3)
+{
+    register seL4_Word destptr asm("r0") = dest;
+    register seL4_Word info asm("r1") = info_arg;
+
+    /* Load beginning of the message into registers. */
+    register seL4_Word msg0 asm("r2") = *in_out_mr0;
+    register seL4_Word msg1 asm("r3") = *in_out_mr1;
+    register seL4_Word msg2 asm("r4") = *in_out_mr2;
+    register seL4_Word msg3 asm("r5") = *in_out_mr3;
+
+    /* Perform the system call. */
+    register seL4_Word scno asm("r7") = sys;
+    asm volatile (
+        "swi $0"
+        : "+r" (msg0), "+r" (msg1), "+r" (msg2), "+r" (msg3),
+          "+r" (info), "+r" (destptr)
+        : "r"(scno)
+        : "memory"
+    );
+    *out_info = info;
+    *out_badge = destptr;
+    *in_out_mr0 = msg0;
+    *in_out_mr1 = msg1;
+    *in_out_mr2 = msg2;
+    *in_out_mr3 = msg3;
+}
+
+static inline void
+arm_sys_null(seL4_Word sys)
+{
+    register seL4_Word scno asm("r7") = sys;
+    asm volatile (
+        "swi $0"
+        : /* no outputs */
+        : "r"(scno)
+    );
+}
 
 static inline void
 seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
 {
-    register seL4_Word destptr asm("r0") = (seL4_Word)dest;
-    register seL4_Word info asm("r1") = msgInfo.words[0];
-
-    /* Load beginning of the message into registers. */
-    register seL4_Word msg0 asm("r2") = seL4_GetMR(0);
-    register seL4_Word msg1 asm("r3") = seL4_GetMR(1);
-    register seL4_Word msg2 asm("r4") = seL4_GetMR(2);
-    register seL4_Word msg3 asm("r5") = seL4_GetMR(3);
-
-    /* Perform the system call. */
-    register seL4_Word scno asm("r7") = seL4_SysSend;
-    asm volatile ("swi %[swi_num]"
-                  : "+r" (destptr), "+r" (msg0), "+r" (msg1), "+r" (msg2),
-                  "+r" (msg3), "+r" (info)
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysSend), "r"(scno)
-                  : "memory");
+    arm_sys_send(seL4_SysSend, dest, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1), seL4_GetMR(2), seL4_GetMR(3));
 }
 
-#ifdef CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS
 static inline void
 seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
                  seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
 {
-    register seL4_Word destptr asm("r0") = (seL4_Word)dest;
-    register seL4_Word info asm("r1") = msgInfo.words[0];
-
-    /* Load beginning of the message into registers. */
-    register seL4_Word msg0 asm("r2");
-    register seL4_Word msg1 asm("r3");
-    register seL4_Word msg2 asm("r4");
-    register seL4_Word msg3 asm("r5");
-    register seL4_Word scno asm("r7") = seL4_SysSend;
-
-    if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
-        msg0 = *mr0;
-    }
-    if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
-        msg1 = *mr1;
-    }
-    if (mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 2) {
-        msg2 = *mr2;
-    }
-    if (mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 3) {
-        msg3 = *mr3;
-    }
-
-    /* Perform the system call. */
-    asm volatile ("swi %[swi_num]"
-                  : "+r" (destptr), "+r" (msg0), "+r" (msg1), "+r" (msg2),
-                  "+r" (msg3), "+r" (info)
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysSend), "r"(scno)
-                  : "memory");
+    arm_sys_send(seL4_SysSend, dest, msgInfo.words[0],
+        mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr0 : 0,
+        mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0,
+        mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr2 : 0,
+        mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr3 : 0
+    );
 }
-#endif
 
 static inline void
 seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
 {
-    register seL4_Word destptr asm("r0") = (seL4_Word)dest;
-    register seL4_Word info asm("r1") = msgInfo.words[0];
-
-    /* Load beginning of the message into registers. */
-    register seL4_Word msg0 asm("r2") = seL4_GetMR(0);
-    register seL4_Word msg1 asm("r3") = seL4_GetMR(1);
-    register seL4_Word msg2 asm("r4") = seL4_GetMR(2);
-    register seL4_Word msg3 asm("r5") = seL4_GetMR(3);
-
-    /* Perform the system call. */
-    register seL4_Word scno asm("r7") = seL4_SysNBSend;
-    asm volatile ("swi %[swi_num]"
-                  : "+r" (destptr), "+r" (msg0), "+r" (msg1), "+r" (msg2),
-                  "+r" (msg3), "+r" (info)
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysNBSend), "r"(scno)
-                  : "memory");
+    arm_sys_send(seL4_SysNBSend, dest, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1), seL4_GetMR(2), seL4_GetMR(3));
 }
 
-#ifdef CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS
 static inline void
 seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
                    seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
 {
-    register seL4_Word destptr asm("r0") = (seL4_Word)dest;
-    register seL4_Word info asm("r1") = msgInfo.words[0];
-
-    /* Load beginning of the message into registers. */
-    register seL4_Word msg0 asm("r2");
-    register seL4_Word msg1 asm("r3");
-    register seL4_Word msg2 asm("r4");
-    register seL4_Word msg3 asm("r5");
-    register seL4_Word scno asm("r7") = seL4_SysNBSend;
-
-    if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
-        msg0 = *mr0;
-    }
-    if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
-        msg1 = *mr1;
-    }
-    if (mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 2) {
-        msg2 = *mr2;
-    }
-    if (mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 3) {
-        msg3 = *mr3;
-    }
-
-    /* Perform the system call. */
-    asm volatile ("swi %[swi_num]"
-                  : "+r" (destptr), "+r" (msg0), "+r" (msg1), "+r" (msg2),
-                  "+r" (msg3), "+r" (info)
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysNBSend), "r"(scno)
-                  : "memory");
+    arm_sys_send(seL4_SysNBSend, dest, msgInfo.words[0],
+        mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr0 : 0,
+        mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0,
+        mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr2 : 0,
+        mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr3 : 0
+    );
 }
-#endif
 
 static inline void
 seL4_Reply(seL4_MessageInfo_t msgInfo)
 {
-    register seL4_Word info asm("r1") = msgInfo.words[0];
-
-    /* Load beginning of the message into registers. */
-    register seL4_Word msg0 asm("r2") = seL4_GetMR(0);
-    register seL4_Word msg1 asm("r3") = seL4_GetMR(1);
-    register seL4_Word msg2 asm("r4") = seL4_GetMR(2);
-    register seL4_Word msg3 asm("r5") = seL4_GetMR(3);
-
-    /* Perform the system call. */
-    register seL4_Word scno asm("r7") = seL4_SysReply;
-    asm volatile ("swi %[swi_num]"
-                  : "+r" (msg0), "+r" (msg1), "+r" (msg2), "+r" (msg3),
-                  "+r" (info)
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysReply), "r"(scno)
-                  : "memory");
+    arm_sys_reply(seL4_SysReply, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1), seL4_GetMR(2), seL4_GetMR(3));
 }
 
-#ifdef CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS
 static inline void
 seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo,
                   seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
 {
-    register seL4_Word info asm("r1") = msgInfo.words[0];
-
-    /* Load beginning of the message into registers. */
-    register seL4_Word msg0 asm("r2");
-    register seL4_Word msg1 asm("r3");
-    register seL4_Word msg2 asm("r4");
-    register seL4_Word msg3 asm("r5");
-    register seL4_Word scno asm("r7") = seL4_SysReply;
-
-    if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
-        msg0 = *mr0;
-    }
-    if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
-        msg1 = *mr1;
-    }
-    if (mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 2) {
-        msg2 = *mr2;
-    }
-    if (mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 3) {
-        msg3 = *mr3;
-    }
-
-    /* Perform the system call. */
-    asm volatile ("swi %[swi_num]"
-                  : "+r" (msg0), "+r" (msg1), "+r" (msg2), "+r" (msg3),
-                  "+r" (info)
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysReply), "r"(scno)
-                  : "memory");
+    arm_sys_reply(seL4_SysReply, msgInfo.words[0],
+        mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr0 : 0,
+        mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0,
+        mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr2 : 0,
+        mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr3 : 0
+    );
 }
-#endif
 
 static inline void
 seL4_Signal(seL4_CPtr dest)
 {
-    register seL4_Word destptr asm("r0") = (seL4_Word)dest;
-    register seL4_Word info asm("r1") = 0;
-
-    /* Perform the system call. */
-    register seL4_Word scno asm("r7") = seL4_SysSend;
-    asm volatile ("swi %[swi_num]"
-                  : "+r" (destptr), "+r" (info)
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysSend), "r"(scno)
-                  : "memory");
+    arm_sys_send_null(seL4_SysSend, dest, seL4_MessageInfo_new(0, 0, 0, 0).words[0]);
 }
 
 static inline seL4_MessageInfo_t
 seL4_Recv(seL4_CPtr src, seL4_Word* sender)
 {
-    register seL4_Word src_and_badge asm("r0") = (seL4_Word)src;
-    register seL4_MessageInfo_t info asm("r1");
+    seL4_MessageInfo_t info;
+    seL4_Word badge;
+    seL4_Word msg0;
+    seL4_Word msg1;
+    seL4_Word msg2;
+    seL4_Word msg3;
 
-    /* Incoming message registers. */
-    register seL4_Word msg0 asm("r2");
-    register seL4_Word msg1 asm("r3");
-    register seL4_Word msg2 asm("r4");
-    register seL4_Word msg3 asm("r5");
+    arm_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3);
 
-    /* Perform the system call. */
-    register seL4_Word scno asm("r7") = seL4_SysRecv;
-    asm volatile ("swi %[swi_num]"
-                  : "=r" (msg0), "=r" (msg1), "=r" (msg2), "=r" (msg3),
-                  "=r" (info), "+r" (src_and_badge)
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysRecv), "r"(scno)
-                  : "memory");
-
-    /* Write the message back out to memory. */
     seL4_SetMR(0, msg0);
     seL4_SetMR(1, msg1);
     seL4_SetMR(2, msg2);
@@ -240,34 +252,23 @@ seL4_Recv(seL4_CPtr src, seL4_Word* sender)
 
     /* Return back sender and message information. */
     if (sender) {
-        *sender = src_and_badge;
+        *sender = badge;
     }
-    return (seL4_MessageInfo_t) {
-        .words = {info.words[0]}
-    };
+    return info;
 }
 
-#ifdef CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS
 static inline seL4_MessageInfo_t
 seL4_RecvWithMRs(seL4_CPtr src, seL4_Word* sender,
                  seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
 {
-    register seL4_Word src_and_badge asm("r0") = (seL4_Word)src;
-    register seL4_MessageInfo_t info asm("r1");
+    seL4_MessageInfo_t info;
+    seL4_Word badge;
+    seL4_Word msg0;
+    seL4_Word msg1;
+    seL4_Word msg2;
+    seL4_Word msg3;
 
-    /* Incoming message registers. */
-    register seL4_Word msg0 asm("r2");
-    register seL4_Word msg1 asm("r3");
-    register seL4_Word msg2 asm("r4");
-    register seL4_Word msg3 asm("r5");
-
-    /* Perform the system call. */
-    register seL4_Word scno asm("r7") = seL4_SysRecv;
-    asm volatile ("swi %[swi_num]"
-                  : "=r" (msg0), "=r" (msg1), "=r" (msg2), "=r" (msg3),
-                  "=r" (info.words[0]), "+r" (src_and_badge)
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysRecv), "r"(scno)
-                  : "memory");
+    arm_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3);
 
     /* Write the message back out to memory. */
     if (mr0 != seL4_Null) {
@@ -285,36 +286,23 @@ seL4_RecvWithMRs(seL4_CPtr src, seL4_Word* sender,
 
     /* Return back sender and message information. */
     if (sender) {
-        *sender = src_and_badge;
+        *sender = badge;
     }
-    return (seL4_MessageInfo_t) {
-        .words = {info.words[0]}
-    };
+    return info;
 }
 
-#endif
-
 static inline seL4_MessageInfo_t
 seL4_NBRecv(seL4_CPtr src, seL4_Word* sender)
 {
-    register seL4_Word src_and_badge asm("r0") = (seL4_Word)src;
-    register seL4_MessageInfo_t info asm("r1");
+    seL4_MessageInfo_t info;
+    seL4_Word badge;
+    seL4_Word msg0;
+    seL4_Word msg1;
+    seL4_Word msg2;
+    seL4_Word msg3;
 
-    /* Incoming message registers. */
-    register seL4_Word msg0 asm("r2");
-    register seL4_Word msg1 asm("r3");
-    register seL4_Word msg2 asm("r4");
-    register seL4_Word msg3 asm("r5");
+    arm_sys_recv(seL4_SysNBRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3);
 
-    /* Perform the system call. */
-    register seL4_Word scno asm("r7") = seL4_SysNBRecv;
-    asm volatile ("swi %[swi_num]"
-                  : "=r" (msg0), "=r" (msg1), "=r" (msg2), "=r" (msg3),
-                  "=r" (info), "+r" (src_and_badge)
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysNBRecv), "r"(scno)
-                  : "memory");
-
-    /* Write the message back out to memory. */
     seL4_SetMR(0, msg0);
     seL4_SetMR(1, msg1);
     seL4_SetMR(2, msg2);
@@ -322,32 +310,21 @@ seL4_NBRecv(seL4_CPtr src, seL4_Word* sender)
 
     /* Return back sender and message information. */
     if (sender) {
-        *sender = src_and_badge;
+        *sender = badge;
     }
-    return (seL4_MessageInfo_t) {
-        .words = { info.words[0]}
-    };
+    return info;
 }
 
 static inline seL4_MessageInfo_t
 seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
 {
-    register seL4_Word destptr asm("r0") = (seL4_Word)dest;
-    register seL4_MessageInfo_t info asm("r1") = msgInfo;
+    seL4_MessageInfo_t info;
+    seL4_Word msg0 = seL4_GetMR(0);
+    seL4_Word msg1 = seL4_GetMR(1);
+    seL4_Word msg2 = seL4_GetMR(2);
+    seL4_Word msg3 = seL4_GetMR(3);
 
-    /* Load beginning of the message into registers. */
-    register seL4_Word msg0 asm("r2") = seL4_GetMR(0);
-    register seL4_Word msg1 asm("r3") = seL4_GetMR(1);
-    register seL4_Word msg2 asm("r4") = seL4_GetMR(2);
-    register seL4_Word msg3 asm("r5") = seL4_GetMR(3);
-
-    /* Perform the system call. */
-    register seL4_Word scno asm("r7") = seL4_SysCall;
-    asm volatile ("swi %[swi_num]"
-                  : "+r" (msg0), "+r" (msg1), "+r" (msg2), "+r" (msg3),
-                  "+r" (info), "+r" (destptr)
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysCall), "r"(scno)
-                  : "memory");
+    arm_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3);
 
     /* Write out the data back to memory. */
     seL4_SetMR(0, msg0);
@@ -355,24 +332,18 @@ seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
     seL4_SetMR(2, msg2);
     seL4_SetMR(3, msg3);
 
-    return (seL4_MessageInfo_t) {
-        .words = {info.words[0]}
-    };
+    return info;
 }
 
-#ifdef CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS
 static inline seL4_MessageInfo_t
 seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
                  seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
 {
-    register seL4_Word destptr asm("r0") = (seL4_Word)dest;
-    register seL4_MessageInfo_t info asm("r1") = msgInfo;
-
-    register seL4_Word msg0 asm("r2");
-    register seL4_Word msg1 asm("r3");
-    register seL4_Word msg2 asm("r4");
-    register seL4_Word msg3 asm("r5");
-    register seL4_Word scno asm("r7") = seL4_SysCall;
+    seL4_MessageInfo_t info;
+    seL4_Word msg0;
+    seL4_Word msg1;
+    seL4_Word msg2;
+    seL4_Word msg3;
 
     /* Load beginning of the message into registers. */
     if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
@@ -388,12 +359,7 @@ seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
         msg3 = *mr3;
     }
 
-    /* Perform the system call. */
-    asm volatile ("swi %[swi_num]"
-                  : "+r" (msg0), "+r" (msg1), "+r" (msg2), "+r" (msg3),
-                  "+r" (info), "+r" (destptr)
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysCall), "r"(scno)
-                  : "memory");
+    arm_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3);
 
     /* Write out the data back to memory. */
     if (mr0 != seL4_Null) {
@@ -409,31 +375,26 @@ seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
         *mr3 = msg3;
     }
 
-    return (seL4_MessageInfo_t) {
-        .words = {info.words[0]}
-    };
+    return info;
 }
-#endif
 
 static inline seL4_MessageInfo_t
 seL4_ReplyRecv(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender)
 {
-    register seL4_Word src_and_badge asm("r0") = (seL4_Word)src;
-    register seL4_MessageInfo_t info asm("r1") = msgInfo;
+    seL4_MessageInfo_t info;
+    seL4_Word badge;
+    seL4_Word msg0;
+    seL4_Word msg1;
+    seL4_Word msg2;
+    seL4_Word msg3;
 
     /* Load beginning of the message into registers. */
-    register seL4_Word msg0 asm("r2") = seL4_GetMR(0);
-    register seL4_Word msg1 asm("r3") = seL4_GetMR(1);
-    register seL4_Word msg2 asm("r4") = seL4_GetMR(2);
-    register seL4_Word msg3 asm("r5") = seL4_GetMR(3);
+    msg0 = seL4_GetMR(0);
+    msg1 = seL4_GetMR(1);
+    msg2 = seL4_GetMR(2);
+    msg3 = seL4_GetMR(3);
 
-    /* Perform the syscall. */
-    register seL4_Word scno asm("r7") = seL4_SysReplyRecv;
-    asm volatile ("swi %[swi_num]"
-                  : "+r" (msg0), "+r" (msg1), "+r" (msg2), "+r" (msg3),
-                  "+r" (info), "+r" (src_and_badge)
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysReplyRecv), "r"(scno)
-                  : "memory");
+    arm_sys_send_recv(seL4_SysReplyRecv, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3);
 
     /* Write the message back out to memory. */
     seL4_SetMR(0, msg0);
@@ -443,27 +404,22 @@ seL4_ReplyRecv(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender)
 
     /* Return back sender and message information. */
     if (sender) {
-        *sender = src_and_badge;
+        *sender = badge;
     }
-    return (seL4_MessageInfo_t) {
-        .words = {info.words[0]}
-    };
+
+    return info;
 }
 
-#ifdef CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS
 static inline seL4_MessageInfo_t
 seL4_ReplyRecvWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender,
                       seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
 {
-    register seL4_Word src_and_badge asm("r0") = (seL4_Word)src;
-    register seL4_MessageInfo_t info asm("r1") = msgInfo;
-
-    /* Load beginning of the message into registers. */
-    register seL4_Word msg0 asm("r2");
-    register seL4_Word msg1 asm("r3");
-    register seL4_Word msg2 asm("r4");
-    register seL4_Word msg3 asm("r5");
-    register seL4_Word scno asm("r7") = seL4_SysReplyRecv;
+    seL4_MessageInfo_t info;
+    seL4_Word badge;
+    seL4_Word msg0;
+    seL4_Word msg1;
+    seL4_Word msg2;
+    seL4_Word msg3;
 
     if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
         msg0 = *mr0;
@@ -478,12 +434,7 @@ seL4_ReplyRecvWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *send
         msg3 = *mr3;
     }
 
-    /* Perform the syscall. */
-    asm volatile ("swi %[swi_num]"
-                  : "+r" (msg0), "+r" (msg1), "+r" (msg2), "+r" (msg3),
-                  "+r" (info), "+r" (src_and_badge)
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysReplyRecv), "r"(scno)
-                  : "memory");
+    arm_sys_send_recv(seL4_SysReplyRecv, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3);
 
     /* Write out the data back to memory. */
     if (mr0 != seL4_Null) {
@@ -501,62 +452,57 @@ seL4_ReplyRecvWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *send
 
     /* Return back sender and message information. */
     if (sender) {
-        *sender = src_and_badge;
+        *sender = badge;
     }
-    return (seL4_MessageInfo_t) {
-        .words = {info.words[0]}
-    };
+
+    return info;
 }
-#endif
 
 static inline void
 seL4_Yield(void)
 {
-    register seL4_Word scno asm("r7") = seL4_SysYield;
-    asm volatile ("swi %[swi_num]"
-                  : /* no outputs */
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysYield), "r"(scno)
-                  : "memory");
+    arm_sys_null(seL4_SysYield);
+    asm volatile("" ::: "memory");
 }
 
 #ifdef CONFIG_DEBUG_BUILD
 static inline void
 seL4_DebugPutChar(char c)
 {
-    register seL4_Word arg1 asm("r0") = c;
-    register seL4_Word scno asm("r7") = seL4_SysDebugPutChar;
-    asm volatile ("swi %[swi_num]"
-                  : /* no outputs */
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysDebugPutChar), "r" (arg1), "r"(scno));
+    seL4_Word unused0 = 0;
+    seL4_Word unused1 = 0;
+    seL4_Word unused2 = 0;
+    seL4_Word unused3 = 0;
+    seL4_Word unused4 = 0;
+    seL4_Word unused5 = 0;
+
+    arm_sys_send_recv(seL4_SysDebugPutChar, c, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5);
 }
 
 static inline void
 seL4_DebugHalt(void)
 {
-    register seL4_Word scno asm("r7") = seL4_SysDebugHalt;
-    asm volatile ("swi %[swi_num]"
-                  : /* no outputs */
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysDebugHalt), "r"(scno));
+    arm_sys_null(seL4_SysDebugHalt);
 }
 
 static inline void
 seL4_DebugSnapshot(void)
 {
-    register seL4_Word scno asm("r7") = seL4_SysDebugSnapshot;
-    asm volatile ("swi %[swi_num]"
-                  : /* no outputs */
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysDebugSnapshot), "r"(scno));
+    arm_sys_null(seL4_SysDebugSnapshot);
+    asm volatile("" ::: "memory");
 }
 
 static inline seL4_Uint32
 seL4_DebugCapIdentify(seL4_CPtr cap)
 {
-    register seL4_Word arg1 asm("r0") = cap;
-    register seL4_Word scno asm("r7") = seL4_SysDebugCapIdentify;
-    asm volatile ("swi %[swi_num]"
-                  : "+r"(arg1)
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysDebugCapIdentify), "r"(scno));
-    return (seL4_Uint32)arg1;
+    seL4_Word unused0 = 0;
+    seL4_Word unused1 = 0;
+    seL4_Word unused2 = 0;
+    seL4_Word unused3 = 0;
+    seL4_Word unused4 = 0;
+
+    arm_sys_send_recv(seL4_SysDebugCapIdentify, cap, &cap, 0, &unused0, &unused1, &unused2, &unused3, &unused4);
+    return (seL4_Uint32)cap;
 }
 
 char *strcpy(char *, const char *);
@@ -565,12 +511,14 @@ seL4_DebugNameThread(seL4_CPtr tcb, const char *name)
 {
     strcpy((char*)seL4_GetIPCBuffer()->msg, name);
 
-    register seL4_Word arg1 asm("r0") = tcb;
-    register seL4_Word scno asm("r7") = seL4_SysDebugNameThread;
-    asm volatile ("swi %[swi_num]"
-                  : "+r"(arg1)
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysDebugNameThread), "r"(scno)
-                  : "memory");
+    seL4_Word unused0 = 0;
+    seL4_Word unused1 = 0;
+    seL4_Word unused2 = 0;
+    seL4_Word unused3 = 0;
+    seL4_Word unused4 = 0;
+    seL4_Word unused5 = 0;
+
+    arm_sys_send_recv(seL4_SysDebugNameThread, tcb, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5);
 }
 #endif
 
@@ -578,14 +526,8 @@ seL4_DebugNameThread(seL4_CPtr tcb, const char *name)
 static inline void
 seL4_DebugRun(void (* userfn) (void *), void* userarg)
 {
-    register seL4_Word arg1 asm("r0") = (seL4_Word)userfn;
-    register seL4_Word arg2 asm("r1") = (seL4_Word)userarg;
-    register seL4_Word scno asm("r7") = seL4_SysDebugRun;
-    asm volatile ("swi %[swi_num]"
-                  : /* no outputs */
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysDebugRun), "r" (arg1), "r" (arg2), "r"(scno)
-                  : "memory"
-                 );
+    arm_sys_send_nnull(seL4_SysDebugRun, (seL4_Word)userfn, (seL4_Word)userarg, 0, 0);
+    asm volatile("" ::: "memory");
 }
 #endif
 
@@ -594,70 +536,71 @@ seL4_DebugRun(void (* userfn) (void *), void* userarg)
 static inline seL4_Error
 seL4_BenchmarkResetLog(void)
 {
-    register seL4_Word retval asm("r0") = 0; /* required for retval */
-    register seL4_Word scno asm("r7") = seL4_SysBenchmarkResetLog;
-    asm volatile ("swi %[swi_num]"
-                  : "+r" (retval)
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysBenchmarkResetLog), "r"(scno)
-                 );
+    seL4_Word unused0 = 0;
+    seL4_Word unused1 = 0;
+    seL4_Word unused2 = 0;
+    seL4_Word unused3 = 0;
+    seL4_Word unused4 = 0;
 
-    return (seL4_Error) retval;
+    seL4_Word ret;
+    arm_sys_send_recv(seL4_SysBenchmarkResetLog, 0, &ret, 0, &unused0, &unused1, &unused2, &unused3, &unused4);
+
+    return (seL4_Error) ret;
 }
 
 static inline void
 seL4_BenchmarkFinalizeLog(void)
 {
-    register seL4_Word scno asm("r7") = seL4_SysBenchmarkFinalizeLog;
-    asm volatile ("swi %[swi_num]"
-                  : /* no outputs */
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysBenchmarkFinalizeLog), "r"(scno)
-                 );
+    arm_sys_null(seL4_SysBenchmarkFinalizeLog);
+    asm volatile("" ::: "memory");
 }
 
 static inline seL4_Error
 seL4_BenchmarkSetLogBuffer(seL4_Word frame_cptr)
 {
-    register seL4_Word arg1 asm("r0") = frame_cptr;
-    register seL4_Word scno asm("r7") = seL4_SysBenchmarkSetLogBuffer;
-    asm volatile ("swi %[swi_num]"
-                  : "+r" (arg1)
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysBenchmarkSetLogBuffer),  "r"(scno)
-                 );
+    seL4_Word unused0 = 0;
+    seL4_Word unused1 = 0;
+    seL4_Word unused2 = 0;
+    seL4_Word unused3 = 0;
+    seL4_Word unused4 = 0;
 
-    return (seL4_Error) arg1;
+    arm_sys_send_recv(seL4_SysBenchmarkSetLogBuffer, frame_cptr, &frame_cptr, 0, &unused0, &unused1, &unused2, &unused3, &unused4);
+
+    return (seL4_Error) frame_cptr;
 }
 
 static inline void
 seL4_BenchmarkNullSyscall(void)
 {
-    register seL4_Word scno asm("r7") = seL4_SysBenchmarkNullSyscall;
-    asm volatile ("swi %[swi_num]"
-                  : /* no outputs */
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysBenchmarkNullSyscall), "r"(scno)
-                  : "memory");
+    arm_sys_null(seL4_SysBenchmarkNullSyscall);
+    asm volatile("" ::: "memory");
 }
 
 #ifdef CONFIG_BENCHMARK_TRACK_UTILISATION
 static inline void
 seL4_BenchmarkGetThreadUtilisation(seL4_Word tcp_cptr)
 {
-    register seL4_Word arg1 asm("r0") = tcp_cptr;
-    register seL4_Word scno asm("r7") = seL4_SysBenchmarkGetThreadUtilisation;
-    asm volatile ("swi %[swi_num]"
-                  : /* no outputs */
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysBenchmarkGetThreadUtilisation), "r" (arg1), "r"(scno)
-                  : "memory");
+    seL4_Word unused0 = 0;
+    seL4_Word unused1 = 0;
+    seL4_Word unused2 = 0;
+    seL4_Word unused3 = 0;
+    seL4_Word unused4 = 0;
+    seL4_Word unused5 = 0;
+
+    arm_sys_send_recv(seL4_BenchmarkGetThreadUtilization, tcb_cptr, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5);
 }
 
 static inline void
 seL4_BenchmarkResetThreadUtilisation(seL4_Word tcp_cptr)
 {
-    register seL4_Word arg1 asm("r0") = tcp_cptr;
-    register seL4_Word scno asm("r7") = seL4_SysBenchmarkResetThreadUtilisation;
-    asm volatile ("swi %[swi_num]"
-                  : /* no outputs */
-                  : [swi_num] "i" __SEL4_SWINUM(seL4_SysBenchmarkResetThreadUtilisation), "r" (arg1), "r"(scno)
-                  : "memory");
+    seL4_Word unused0 = 0;
+    seL4_Word unused1 = 0;
+    seL4_Word unused2 = 0;
+    seL4_Word unused3 = 0;
+    seL4_Word unused4 = 0;
+    seL4_Word unused5 = 0;
+
+    arm_sys_send_recv(seL4_BenchmarkResetThreadUtilization, tcb_cptr, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5);
 }
 #endif /* CONFIG_BENCHMARK_TRACK_UTILISATION */
 #endif /* CONFIG_ENABLE_BENCHMARKS */