diff --git a/sel4_cspace/src/arch/aarch64/mod.rs b/sel4_cspace/src/arch/aarch64/mod.rs
index ecad74e..fe84756 100644
--- a/sel4_cspace/src/arch/aarch64/mod.rs
+++ b/sel4_cspace/src/arch/aarch64/mod.rs
@@ -30,6 +30,8 @@ impl cap_arch_func for cap {
             // cap_tag::CapPageGlobalDirectoryCap => self.get_pgd_base_ptr(),
             cap_tag::cap_asid_control_cap => 0,
             cap_tag::cap_asid_pool_cap => cap::cap_asid_pool_cap(self).get_capASIDPool() as usize,
+            #[cfg(feature = "KERNEL_MCS")]
+            cap_tag::cap_reply_cap => cap::cap_reply_cap(self).get_capReplyPtr() as usize,
             _ => 0,
         }
     }
diff --git a/sel4_cspace/src/capability/mod.rs b/sel4_cspace/src/capability/mod.rs
index a4a80e5..12f3a48 100644
--- a/sel4_cspace/src/capability/mod.rs
+++ b/sel4_cspace/src/capability/mod.rs
@@ -109,23 +109,47 @@ impl cap_func for cap {
             cap_tag::cap_reply_cap => seL4_ReplyBits,
             #[cfg(not(feature = "KERNEL_MCS"))]
             cap_tag::cap_reply_cap => 0,
+            #[cfg(feature = "KERNEL_MCS")]
+            cap_tag::cap_sched_context_cap => {
+                cap::cap_sched_context_cap(self).get_capSCSizeBits() as usize
+            }
             _ => 0,
         }
     }
 
     fn get_cap_is_physical(&self) -> bool {
-        matches!(
-            self.get_tag(),
-            cap_tag::cap_untyped_cap
-                | cap_tag::cap_endpoint_cap
-                | cap_tag::cap_notification_cap
-                | cap_tag::cap_cnode_cap
-                | cap_tag::cap_frame_cap
-                | cap_tag::cap_asid_pool_cap
-                | cap_tag::cap_page_table_cap
-                | cap_tag::cap_zombie_cap
-                | cap_tag::cap_thread_cap
-        )
+        #[cfg(not(feature = "KERNEL_MCS"))]
+        {
+            matches!(
+                self.get_tag(),
+                cap_tag::cap_untyped_cap
+                    | cap_tag::cap_endpoint_cap
+                    | cap_tag::cap_notification_cap
+                    | cap_tag::cap_cnode_cap
+                    | cap_tag::cap_frame_cap
+                    | cap_tag::cap_asid_pool_cap
+                    | cap_tag::cap_page_table_cap
+                    | cap_tag::cap_zombie_cap
+                    | cap_tag::cap_thread_cap
+            )
+        }
+        #[cfg(feature = "KERNEL_MCS")]
+        {
+            matches!(
+                self.get_tag(),
+                cap_tag::cap_untyped_cap
+                    | cap_tag::cap_endpoint_cap
+                    | cap_tag::cap_notification_cap
+                    | cap_tag::cap_cnode_cap
+                    | cap_tag::cap_frame_cap
+                    | cap_tag::cap_asid_pool_cap
+                    | cap_tag::cap_page_table_cap
+                    | cap_tag::cap_zombie_cap
+                    | cap_tag::cap_thread_cap
+                    | cap_tag::cap_sched_context_cap
+                    | cap_tag::cap_reply_cap
+            )
+        }
     }
 
     fn isArchCap(&self) -> bool {
@@ -186,6 +210,23 @@ pub fn same_region_as(cap1: &cap, cap2: &cap) -> bool {
             }
             false
         }
+        #[cfg(feature = "KERNEL_MCS")]
+        cap_tag::cap_sched_context_cap => {
+            if cap2.get_tag() == cap_tag::cap_sched_context_cap {
+                return (cap::cap_sched_context_cap(cap1).get_capSCPtr()
+                    == cap::cap_sched_context_cap(cap2).get_capSCPtr())
+                    && (cap::cap_sched_context_cap(cap1).get_capSCSizeBits()
+                        == cap::cap_sched_context_cap(cap2).get_capSCSizeBits());
+            }
+            false
+        }
+        #[cfg(feature = "KERNEL_MCS")]
+        cap_tag::cap_sched_control_cap => {
+            if cap2.get_tag() == cap_tag::cap_sched_control_cap {
+                return true;
+            }
+            false
+        }
         _ => false,
     }
 }
diff --git a/sel4_ipc/src/notification.rs b/sel4_ipc/src/notification.rs
index f58f331..d95fbd4 100644
--- a/sel4_ipc/src/notification.rs
+++ b/sel4_ipc/src/notification.rs
@@ -91,7 +91,24 @@ impl notification_func for notification {
             self.set_ntfnQueue_tail(0);
             while let Some(thread) = op_thread {
                 set_thread_state(thread, ThreadState::ThreadStateRestart);
-                thread.sched_enqueue();
+                #[cfg(feature = "KERNEL_MCS")]
+                {
+                    if let Some(sc) =
+                        convert_to_option_mut_type_ref::<sched_context_t>(thread.tcbSchedContext)
+                    {
+                        if sc.sc_sporadic() {
+                            unsafe {
+                                assert!(thread.tcbSchedContext != ksCurSC);
+                                sc.refill_unblock_check();
+                            }
+                        }
+                    }
+                    possible_switch_to(thread);
+                }
+                #[cfg(not(feature = "KERNEL_MCS"))]
+                {
+                    thread.sched_enqueue();
+                }
                 op_thread = convert_to_option_mut_type_ref::<tcb_t>(thread.tcbEPNext);
             }
             rescheduleRequired();