diff --git a/libsel4simple-default/src/libsel4simple-default.c b/libsel4simple-default/src/libsel4simple-default.c
index 89b314c..946b734 100644
--- a/libsel4simple-default/src/libsel4simple-default.c
+++ b/libsel4simple-default/src/libsel4simple-default.c
@@ -200,7 +200,7 @@
 seL4_CPtr simple_default_sched_control(void *data, int core)
 {
     assert(core < simple_default_core_count(data));
-#if CONFIG_KERNEL_RT
+#if CONFIG_KERNEL_MCS
     return ((seL4_BootInfo *) data)->schedcontrol.start + core;
 #else
     ZF_LOGW("not implemented");
diff --git a/libsel4simple/include/simple/simple.h b/libsel4simple/include/simple/simple.h
index 3f3b30b..b7f65be 100644
--- a/libsel4simple/include/simple/simple.h
+++ b/libsel4simple/include/simple/simple.h
@@ -418,7 +418,7 @@
 static inline seL4_CPtr
 simple_get_sc(UNUSED simple_t *simple)
 {
-#ifdef CONFIG_KERNEL_RT
+#ifdef CONFIG_KERNEL_MCS
     return simple_init_cap(simple, seL4_CapInitThreadSC);
 #else
     return seL4_CapNull;
diff --git a/libsel4sync/include/sync/sem-bare.h b/libsel4sync/include/sync/sem-bare.h
index e0d7ef7..3218e42 100644
--- a/libsel4sync/include/sync/sem-bare.h
+++ b/libsel4sync/include/sync/sem-bare.h
@@ -40,13 +40,13 @@
     }
     if (oldval <= 0) {
 #ifdef CONFIG_ARCH_IA32
-#ifdef CONFIG_KERNEL_RT
+#ifdef CONFIG_KERNEL_MCS
         seL4_WaitWithMRs(ep, NULL, NULL);
 #else
         seL4_RecvWithMRs(ep, NULL, NULL, NULL);
-#endif /* CONFIG_KERNEL_RT */
+#endif /* CONFIG_KERNEL_MCS */
 #else // all other platforms have 4 mrs
-#ifdef CONFIG_KERNEL_RT
+#ifdef CONFIG_KERNEL_MCS
         seL4_WaitWithMRs(ep, NULL, NULL, NULL, NULL, NULL);
 #else
         seL4_RecvWithMRs(ep, NULL, NULL, NULL, NULL, NULL);
diff --git a/libsel4utils/include/sel4utils/mcs_api.h b/libsel4utils/include/sel4utils/mcs_api.h
index eb57361..c79388c 100644
--- a/libsel4utils/include/sel4utils/mcs_api.h
+++ b/libsel4utils/include/sel4utils/mcs_api.h
@@ -24,7 +24,7 @@
 #include <sel4/sel4.h>
 #include <sel4utils/sel4_zf_logif.h>
 
-#ifdef CONFIG_KERNEL_RT
+#ifdef CONFIG_KERNEL_MCS
 #define CONFIG_TIMER_TICK_MS CONFIG_BOOT_THREAD_TIME_SLICE
 #else
 #define CONFIG_BOOT_THREAD_TIME_SLICE CONFIG_TIMER_TICK_MS
@@ -32,7 +32,7 @@
 
 static inline seL4_MessageInfo_t api_wait(seL4_CPtr ep, seL4_Word *badge)
 {
-#ifdef CONFIG_KERNEL_RT
+#ifdef CONFIG_KERNEL_MCS
     return seL4_Wait(ep, badge);
 #else
     return seL4_Recv(ep, badge);
@@ -41,7 +41,7 @@
 
 static inline seL4_MessageInfo_t api_recv(seL4_CPtr ep, seL4_Word *badge, UNUSED seL4_CPtr reply)
 {
-#ifdef CONFIG_KERNEL_RT
+#ifdef CONFIG_KERNEL_MCS
     return seL4_Recv(ep, badge, reply);
 #else
     return seL4_Recv(ep, badge);
@@ -50,7 +50,7 @@
 
 static inline seL4_MessageInfo_t api_nbrecv(seL4_CPtr ep, seL4_Word *badge, UNUSED seL4_CPtr reply)
 {
-#ifdef CONFIG_KERNEL_RT
+#ifdef CONFIG_KERNEL_MCS
     return seL4_NBRecv(ep, badge, reply);
 #else
     return seL4_NBRecv(ep, badge);
@@ -59,7 +59,7 @@
 
 static inline void api_reply(UNUSED seL4_CPtr reply, seL4_MessageInfo_t msg)
 {
-#ifdef CONFIG_KERNEL_RT
+#ifdef CONFIG_KERNEL_MCS
     seL4_Send(reply, msg);
 #else
     seL4_Reply(msg);
@@ -69,7 +69,7 @@
 static inline seL4_MessageInfo_t api_reply_recv(seL4_CPtr ep, seL4_MessageInfo_t msg, seL4_Word *badge,
                                                 UNUSED seL4_CPtr reply)
 {
-#ifdef CONFIG_KERNEL_RT
+#ifdef CONFIG_KERNEL_MCS
     return seL4_ReplyRecv(ep, msg, badge, reply);
 #else
     return seL4_ReplyRecv(ep, msg, badge);
@@ -80,8 +80,8 @@
                                                  UNUSED seL4_CPtr recv, UNUSED seL4_Word *badge,
                                                  UNUSED seL4_CPtr reply)
 {
-    ZF_LOGF_IF(!config_set(CONFIG_KERNEL_RT), "Not available on non MCS kernel");
-#ifdef CONFIG_KERNEL_RT
+    ZF_LOGF_IF(!config_set(CONFIG_KERNEL_MCS), "Not available on non MCS kernel");
+#ifdef CONFIG_KERNEL_MCS
     return seL4_NBSendRecv(send, info, recv, badge, reply);
 #else
     return seL4_MessageInfo_new(0, 0, 0, 0);
@@ -91,8 +91,8 @@
 static inline seL4_MessageInfo_t api_nbsend_wait(UNUSED seL4_CPtr send, UNUSED seL4_MessageInfo_t info,
                                                  UNUSED seL4_CPtr recv, UNUSED seL4_Word *badge)
 {
-    ZF_LOGF_IF(!config_set(CONFIG_KERNEL_RT), "Not available on non MCS kernel");
-#ifdef CONFIG_KERNEL_RT
+    ZF_LOGF_IF(!config_set(CONFIG_KERNEL_MCS), "Not available on non MCS kernel");
+#ifdef CONFIG_KERNEL_MCS
     return seL4_NBSendWait(send, info, recv, badge);
 #else
     return seL4_MessageInfo_new(0, 0, 0, 0);
@@ -104,7 +104,7 @@
                                            seL4_Word cdata, seL4_CPtr vspace, seL4_Word vdata,
                                            seL4_Word ipc_buffer_addr, seL4_CPtr ipc_buffer_cap)
 {
-#ifdef CONFIG_KERNEL_RT
+#ifdef CONFIG_KERNEL_MCS
     seL4_Error error = seL4_TCB_SetSpace(tcb, ep, cspace, cdata, vspace, vdata);
     if (!error) {
         error = seL4_TCB_SetIPCBuffer(tcb, ipc_buffer_addr, ipc_buffer_cap);
@@ -125,7 +125,7 @@
 static inline seL4_Error api_tcb_set_sched_params(seL4_CPtr tcb, seL4_CPtr auth, seL4_Word prio,
                                                   seL4_Word mcp, UNUSED seL4_CPtr sc, UNUSED seL4_CPtr ep)
 {
-#ifdef CONFIG_KERNEL_RT
+#ifdef CONFIG_KERNEL_MCS
     return seL4_TCB_SetSchedParams(tcb, auth, mcp, prio, sc, ep);
 #else
     return seL4_TCB_SetSchedParams(tcb, auth, mcp, prio);
@@ -142,30 +142,30 @@
 
 static inline seL4_Error api_sc_bind(UNUSED seL4_CPtr sc, UNUSED seL4_CPtr tcb)
 {
-    if (!config_set(CONFIG_KERNEL_RT)) {
+    if (!config_set(CONFIG_KERNEL_MCS)) {
         return (seL4_Error) - ENOSYS;
     }
-#ifdef CONFIG_KERNEL_RT
+#ifdef CONFIG_KERNEL_MCS
     return seL4_SchedContext_Bind(sc, tcb);
 #endif
 }
 
 static inline seL4_Error api_sc_unbind_object(UNUSED seL4_CPtr sc, UNUSED seL4_CPtr tcb)
 {
-    if (!config_set(CONFIG_KERNEL_RT)) {
+    if (!config_set(CONFIG_KERNEL_MCS)) {
         return (seL4_Error) - ENOSYS;
     }
-#ifdef CONFIG_KERNEL_RT
+#ifdef CONFIG_KERNEL_MCS
     return seL4_SchedContext_UnbindObject(sc, tcb);
 #endif
 }
 
 static inline seL4_Error api_sc_unbind(UNUSED seL4_CPtr sc)
 {
-    if (!config_set(CONFIG_KERNEL_RT)) {
+    if (!config_set(CONFIG_KERNEL_MCS)) {
         return (seL4_Error) - ENOSYS;
     }
-#ifdef CONFIG_KERNEL_RT
+#ifdef CONFIG_KERNEL_MCS
     return seL4_SchedContext_Unbind(sc);
 #endif
 }
@@ -174,10 +174,10 @@
                                                   UNUSED uint64_t budget, UNUSED uint64_t period,
                                                   UNUSED seL4_Word refills, UNUSED seL4_Word badge)
 {
-    if (!config_set(CONFIG_KERNEL_RT)) {
+    if (!config_set(CONFIG_KERNEL_MCS)) {
         return (seL4_Error) - ENOSYS;
     }
-#ifdef CONFIG_KERNEL_RT
+#ifdef CONFIG_KERNEL_MCS
     return seL4_SchedControl_Configure(sched_ctrl, sc, budget, period, refills, badge);
 #endif
 }
diff --git a/libsel4utils/include/sel4utils/process_config.h b/libsel4utils/include/sel4utils/process_config.h
index 2acd883..ffbc34d 100644
--- a/libsel4utils/include/sel4utils/process_config.h
+++ b/libsel4utils/include/sel4utils/process_config.h
@@ -189,7 +189,7 @@
     config = process_config_create_vspace(config, NULL, 0);
     config = process_config_create_fault_endpoint(config);
 
-    if (config_set(CONFIG_KERNEL_RT)) {
+    if (config_set(CONFIG_KERNEL_MCS)) {
         uint64_t timeslice = CONFIG_BOOT_THREAD_TIME_SLICE;
         config.sched_params = sched_params_round_robin(config.sched_params, simple, 0, timeslice * US_IN_MS);
     }
diff --git a/libsel4utils/include/sel4utils/thread.h b/libsel4utils/include/sel4utils/thread.h
index 7b15e96..1d745b2 100644
--- a/libsel4utils/include/sel4utils/thread.h
+++ b/libsel4utils/include/sel4utils/thread.h
@@ -216,7 +216,7 @@
  *
  * On master, only use sched_params_set_core to set the core then call this function.
  *
- * If CONFIG_KERNEL_RT is set, the sched params must be fully populated or the scheduling
+ * If CONFIG_KERNEL_MCS is set, the sched params must be fully populated or the scheduling
  * context will be empty when it changes core as scheduling parameters of scheduling
  * contexts are not maintained across migrations.
  */
diff --git a/libsel4utils/include/sel4utils/thread_config.h b/libsel4utils/include/sel4utils/thread_config.h
index 3799a9b..7ea6e9e 100644
--- a/libsel4utils/include/sel4utils/thread_config.h
+++ b/libsel4utils/include/sel4utils/thread_config.h
@@ -71,7 +71,7 @@
                                                    uint64_t period_us,
                                                    uint64_t budget_us, seL4_Word extra_refills, seL4_Word badge)
 {
-    if (!config_set(CONFIG_KERNEL_RT)) {
+    if (!config_set(CONFIG_KERNEL_MCS)) {
         ZF_LOGW("Setting sched params on non-RT kernel will have no effect");
     }
     params.sched_ctrl = simple_get_sched_ctrl(simple, core);
@@ -91,7 +91,7 @@
 
 static inline sched_params_t sched_params_core(sched_params_t params, seL4_Word core)
 {
-    if (!config_set(CONFIG_KERNEL_RT)) {
+    if (!config_set(CONFIG_KERNEL_MCS)) {
         ZF_LOGW("Setting core on RT kernel will have no effect - sched ctrl required");
     }
     params.core = core;
@@ -180,7 +180,7 @@
     config = thread_config_cspace(config, cnode, data);
     config = thread_config_fault_endpoint(config, fault_ep);
     config = thread_config_priority(config, prio);
-    if (config_set(CONFIG_KERNEL_RT)) {
+    if (config_set(CONFIG_KERNEL_MCS)) {
         uint64_t timeslice = CONFIG_BOOT_THREAD_TIME_SLICE;
         config.sched_params = sched_params_round_robin(config.sched_params, simple, 0, timeslice * US_IN_MS);
     }
diff --git a/libsel4utils/src/irq_server/irq_server.c b/libsel4utils/src/irq_server/irq_server.c
index f44d296..952cdcd 100644
--- a/libsel4utils/src/irq_server/irq_server.c
+++ b/libsel4utils/src/irq_server/irq_server.c
@@ -344,7 +344,7 @@
 
     error = ps_calloc(malloc_ops, 1, sizeof(irq_server_t), (void **) &new);
 
-    if (config_set(CONFIG_KERNEL_RT) && vka_alloc_reply(vka, &(new->reply)) != 0) {
+    if (config_set(CONFIG_KERNEL_MCS) && vka_alloc_reply(vka, &(new->reply)) != 0) {
         ZF_LOGE("Failed to allocate reply object");
         return NULL;
     }
diff --git a/libsel4utils/src/process.c b/libsel4utils/src/process.c
index acb2463..2ee9fd0 100644
--- a/libsel4utils/src/process.c
+++ b/libsel4utils/src/process.c
@@ -604,7 +604,7 @@
      * the required virtual memory*/
     sel4utils_thread_config_t thread_config = {0};
     thread_config = thread_config_cspace(thread_config, process->cspace.cptr, cspace_root_data);
-    if (config_set(CONFIG_KERNEL_RT)) {
+    if (config_set(CONFIG_KERNEL_MCS)) {
         /* on the MCS kernel, use the fault endpoint in the current cspace */
         thread_config = thread_config_fault_endpoint(thread_config, process->fault_endpoint.cptr);
     } else if (process->fault_endpoint.cptr != 0) {
@@ -632,7 +632,7 @@
     }
 
     if (config.create_cspace) {
-        if (config_set(CONFIG_KERNEL_RT)) {
+        if (config_set(CONFIG_KERNEL_MCS)) {
             seL4_CPtr UNUSED slot = sel4utils_copy_cap_to_process(process, vka, process->thread.sched_context.cptr);
             assert(slot == SEL4UTILS_SCHED_CONTEXT_SLOT);
             slot = sel4utils_copy_cap_to_process(process, vka, process->thread.reply.cptr);
@@ -733,7 +733,7 @@
         return SEL4UTILS_PD_SLOT;
     case seL4_CapInitThreadASIDPool:
         return SEL4UTILS_ASID_POOL_SLOT;
-#ifdef CONFIG_KERNEL_RT
+#ifdef CONFIG_KERNEL_MCS
     case seL4_CapInitThreadSC:
         return SEL4UTILS_SCHED_CONTEXT_SLOT;
 #endif
diff --git a/libsel4utils/src/thread.c b/libsel4utils/src/thread.c
index 13e94a2..0dc13ab 100644
--- a/libsel4utils/src/thread.c
+++ b/libsel4utils/src/thread.c
@@ -64,7 +64,7 @@
         }
     }
 
-    if (config_set(CONFIG_KERNEL_RT) && config.create_reply) {
+    if (config_set(CONFIG_KERNEL_MCS) && config.create_reply) {
         if (vka_alloc_reply(vka, &res->reply)) {
             ZF_LOGE("Failed to allocate reply");
             sel4utils_clean_up_thread(vka, alloc, res);
@@ -76,7 +76,7 @@
     }
 
     if (config.sched_params.create_sc) {
-        if (!config_set(CONFIG_KERNEL_RT)) {
+        if (!config_set(CONFIG_KERNEL_MCS)) {
             ZF_LOGE("Cannot create a scheduling context on a non-RT kernel");
             sel4utils_clean_up_thread(vka, alloc, res);
             return -1;
@@ -90,7 +90,7 @@
         }
 
         /* configure the scheduling context */
-        if (config_set(CONFIG_KERNEL_RT)) {
+        if (config_set(CONFIG_KERNEL_MCS)) {
             error = api_sched_ctrl_configure(config.sched_params.sched_ctrl, res->sched_context.cptr,
                                              config.sched_params.budget, config.sched_params.period,
                                              config.sched_params.extra_refills, config.sched_params.badge);
@@ -275,7 +275,7 @@
                (void *) seL4_Fault_CapFault_get_Addr(fault),
                COLOR_NORMAL);
         break;
-#ifdef CONFIG_KERNEL_RT
+#ifdef CONFIG_KERNEL_MCS
     case seL4_Fault_Timeout:
         printf("Timeout fault from %s\n", thread_name);
         break;
@@ -389,7 +389,7 @@
 
 int sel4utils_set_sched_affinity(sel4utils_thread_t *thread, sched_params_t params) {
 #if CONFIG_MAX_NUM_NODES > 1
-#ifdef CONFIG_KERNEL_RT
+#ifdef CONFIG_KERNEL_MCS
     return api_sched_ctrl_configure(params.sched_ctrl, thread->sched_context.cptr, params.budget, params.period,
                                     params.extra_refills, params.badge);
 
diff --git a/libsel4vka/include/vka/capops.h b/libsel4vka/include/vka/capops.h
index d684884..42b1958 100644
--- a/libsel4vka/include/vka/capops.h
+++ b/libsel4vka/include/vka/capops.h
@@ -23,7 +23,7 @@
 #include <vka/cspacepath_t.h>
 #include <vka/object.h>
 
-#ifndef CONFIG_KERNEL_RT
+#ifndef CONFIG_KERNEL_MCS
 static inline int vka_cnode_saveCaller(const cspacepath_t *src)
 {
     return seL4_CNode_SaveCaller(
diff --git a/libsel4vka/include/vka/kobject_t.h b/libsel4vka/include/vka/kobject_t.h
index cad1865..370bc8d 100644
--- a/libsel4vka/include/vka/kobject_t.h
+++ b/libsel4vka/include/vka/kobject_t.h
@@ -64,7 +64,7 @@
         return seL4_PageDirBits;
     case KOBJECT_PAGE_TABLE:
         return seL4_PageTableBits;
-#ifdef CONFIG_KERNEL_RT
+#ifdef CONFIG_KERNEL_MCS
     case KOBJECT_REPLY:
         return seL4_ReplyBits;
     case KOBJECT_SCHED_CONTEXT:
@@ -95,7 +95,7 @@
         return seL4_EndpointObject;
     case KOBJECT_NOTIFICATION:
         return seL4_NotificationObject;
-#ifdef CONFIG_KERNEL_RT
+#ifdef CONFIG_KERNEL_MCS
     case KOBJECT_SCHED_CONTEXT:
         return seL4_SchedContextObject;
     case KOBJECT_REPLY:
diff --git a/libsel4vka/include/vka/object.h b/libsel4vka/include/vka/object.h
index 56c477d..b7665d8 100644
--- a/libsel4vka/include/vka/object.h
+++ b/libsel4vka/include/vka/object.h
@@ -152,7 +152,7 @@
 
 static inline int vka_alloc_sched_context(UNUSED vka_t *vka, UNUSED vka_object_t *result)
 {
-#ifdef CONFIG_KERNEL_RT
+#ifdef CONFIG_KERNEL_MCS
     return vka_alloc_object(vka, seL4_SchedContextObject, seL4_MinSchedContextBits, result);
 #else
     ZF_LOGW("Allocating sched context on non RT kernel");
@@ -162,7 +162,7 @@
 
 static inline int vka_alloc_sched_context_size(UNUSED vka_t *vka, UNUSED vka_object_t *result, UNUSED uint32_t size_bits)
 {
-#ifdef CONFIG_KERNEL_RT
+#ifdef CONFIG_KERNEL_MCS
     if (size_bits < seL4_MinSchedContextBits) {
         ZF_LOGE("Invalid size bits for sc");
         return -1;
@@ -193,7 +193,7 @@
 
 static inline int vka_alloc_reply(UNUSED vka_t *vka, vka_object_t *result)
 {
-#ifdef CONFIG_KERNEL_RT
+#ifdef CONFIG_KERNEL_MCS
     return vka_alloc_object(vka, seL4_ReplyObject, seL4_ReplyBits, result);
 #else
     *result = (vka_object_t) {};
@@ -310,7 +310,7 @@
         return objectSize;
     case seL4_TCBObject:
         return seL4_TCBBits;
-#ifdef CONFIG_KERNEL_RT
+#ifdef CONFIG_KERNEL_MCS
     case seL4_SchedContextObject:
         return objectSize > seL4_MinSchedContextBits ? objectSize : seL4_MinSchedContextBits;
     case seL4_ReplyObject: