diff --git a/driver-collect/.gitrepo b/driver-collect/.gitrepo
index 97c20df..2f78906 100644
--- a/driver-collect/.gitrepo
+++ b/driver-collect/.gitrepo
@@ -7,6 +7,6 @@
 	remote = git@github.com:rel4team/driver-collect.git
 	branch = mi_dev
 	commit = 3667ef6ab3d6c4831680310e4b8f0947258569ae
- 	parent = 493b5dca37f6d34e2e26bcb49fa32f726cd2ddf1
+ 	parent = 038099532c29c681c9500b3091b3bdd3ac05db85
 	method = merge
 	cmdver = 0.4.9
diff --git a/kernel/.gitrepo b/kernel/.gitrepo
index 76930a4..aba202f 100644
--- a/kernel/.gitrepo
+++ b/kernel/.gitrepo
@@ -6,7 +6,7 @@
 [subrepo]
 	remote = git@github.com:rel4team/rel4_kernel.git
 	branch = mi_dev
-	commit = 79ad922b4afd2c37b256b632522ec924de1ed4bc
- 	parent = 493b5dca37f6d34e2e26bcb49fa32f726cd2ddf1
+	commit = 2e4bfee939a1658e8effb04e42a91bcfb8f2d947
+ 	parent = 038099532c29c681c9500b3091b3bdd3ac05db85
 	method = merge
 	cmdver = 0.4.9
diff --git a/kernel/src/syscall/invocation/decode/mod.rs b/kernel/src/syscall/invocation/decode/mod.rs
index 954ef08..50950de 100644
--- a/kernel/src/syscall/invocation/decode/mod.rs
+++ b/kernel/src/syscall/invocation/decode/mod.rs
@@ -104,21 +104,29 @@ pub fn decode_invocation(
         }
 
         cap_Splayed::reply_cap(data) => {
-            if unlikely(data.get_capReplyMaster() != 0) {
-                debug!("Attempted to invoke an invalid reply cap {}.", cap_index);
-                unsafe {
-                    current_syscall_error._type = seL4_InvalidCapability;
-                    current_syscall_error.invalidCapNumber = 0;
-                    return exception_t::EXCEPTION_SYSCALL_ERROR;
+            #[cfg(feature = "KERNEL_MCS")]
+            {
+                // TODO: MCS
+                exception_t::EXCEPTION_NONE
+            }
+            #[cfg(not(feature = "KERNEL_MCS"))]
+            {
+                if unlikely(data.get_capReplyMaster() != 0) {
+                    debug!("Attempted to invoke an invalid reply cap {}.", cap_index);
+                    unsafe {
+                        current_syscall_error._type = seL4_InvalidCapability;
+                        current_syscall_error.invalidCapNumber = 0;
+                        return exception_t::EXCEPTION_SYSCALL_ERROR;
+                    }
                 }
+                set_thread_state(get_currenct_thread(), ThreadState::ThreadStateRestart);
+                get_currenct_thread().do_reply(
+                    convert_to_mut_type_ref::<tcb_t>(data.get_capTCBPtr() as usize),
+                    slot,
+                    data.get_capReplyCanGrant() != 0,
+                );
+                exception_t::EXCEPTION_NONE
             }
-            set_thread_state(get_currenct_thread(), ThreadState::ThreadStateRestart);
-            get_currenct_thread().do_reply(
-                convert_to_mut_type_ref::<tcb_t>(data.get_capTCBPtr() as usize),
-                slot,
-                data.get_capReplyCanGrant() != 0,
-            );
-            exception_t::EXCEPTION_NONE
         }
         cap_Splayed::thread_cap(data) => {
             decode_tcb_invocation(label, length, &data, slot, call, buffer)
diff --git a/patches/README.md b/patches/README.md
new file mode 100644
index 0000000..165ec24
--- /dev/null
+++ b/patches/README.md
@@ -0,0 +1,3 @@
+| 补丁路径               | 补丁描述                                                                            | 补丁应用命令                       |
+| ---------------------- | ----------------------------------------------------------------------------------- | ---------------------------------- |
+| patches/microkit.patch | 使rel4_kernel对齐在microkit上基于seL4内核的部分改造，在boot时增加了一块设备内存区域 | `git apply patches/microkit.patch` |
\ No newline at end of file
diff --git a/patches/microkit.patch b/patches/microkit.patch
new file mode 100644
index 0000000..85b6298
--- /dev/null
+++ b/patches/microkit.patch
@@ -0,0 +1,165 @@
+diff --git a/kernel/src/arch/aarch64/boot.rs b/kernel/src/arch/aarch64/boot.rs
+index 3eded36..74b80c3 100644
+--- a/kernel/src/arch/aarch64/boot.rs
++++ b/kernel/src/arch/aarch64/boot.rs
+@@ -9,8 +9,8 @@ use crate::arch::aarch64::platform::{cleanInvalidateL1Caches, init_cpu, invalida
+ use crate::{
+     arch::init_freemem,
+     boot::{
+-        bi_finalise, calculate_extra_bi_size_bits, create_untypeds, init_core_state, init_dtb,
+-        ksNumCPUs, ndks_boot, paddr_to_pptr_reg, root_server_init,
++        bi_finalise, calculate_extra_bi_size_bits, create_untypeds, create_untypeds_for_region,
++        init_core_state, init_dtb, ksNumCPUs, ndks_boot, paddr_to_pptr_reg, root_server_init,
+     },
+     config::{BI_FRAME_SIZE_BITS, USER_TOP},
+     structures::{p_region_t, seL4_SlotRegion, v_region_t},
+@@ -26,6 +26,8 @@ pub fn try_init_kernel(
+     dtb_phys_addr: usize,
+     dtb_size: usize,
+     ki_boot_end: usize,
++    extra_device_addr_start: usize,
++    extra_deviec_size: usize,
+ ) -> bool {
+     // Init logging for log crate
+     sel4_common::logging::init();
+@@ -38,6 +40,12 @@ pub fn try_init_kernel(
+         start: ui_p_reg_start,
+         end: ui_p_reg_end,
+     };
++
++    let extra_device_p_reg = p_region_t {
++        start: extra_device_addr_start,
++        end: extra_device_addr_start + extra_deviec_size,
++    };
++
+     let ui_reg = paddr_to_pptr_reg(&ui_p_reg);
+ 
+     let mut extra_bi_size = 0;
+@@ -84,7 +92,11 @@ pub fn try_init_kernel(
+     }
+ 
+     // FIXED: init_freemem should be p_region_t, but is region_t before.
+-    if !init_freemem(ui_p_reg.clone(), dtb_p_reg.unwrap().clone()) {
++    if !init_freemem(
++        ui_p_reg.clone(),
++        dtb_p_reg.unwrap().clone(),
++        extra_device_p_reg.clone(),
++    ) {
+         debug!("ERROR: free memory management initialization failed\n");
+         return false;
+     }
+@@ -102,7 +114,18 @@ pub fn try_init_kernel(
+         create_idle_thread();
+         cleanInvalidateL1Caches();
+         init_core_state(initial_thread);
+-        if !create_untypeds(&root_cnode_cap, boot_mem_reuse_reg) {
++
++        let first_untyped_slot = unsafe { ndks_boot.slot_pos_cur };
++        if extra_device_addr_start != 0 {
++            create_untypeds_for_region(
++                &root_cnode_cap,
++                true,
++                paddr_to_pptr_reg(&extra_device_p_reg),
++                first_untyped_slot,
++            );
++        }
++
++        if !create_untypeds(&root_cnode_cap, boot_mem_reuse_reg, first_untyped_slot) {
+             debug!("ERROR: could not create untypteds for kernel image boot memory");
+         }
+         unsafe {
+diff --git a/kernel/src/arch/aarch64/platform.rs b/kernel/src/arch/aarch64/platform.rs
+index 5659251..5bf33a4 100644
+--- a/kernel/src/arch/aarch64/platform.rs
++++ b/kernel/src/arch/aarch64/platform.rs
+@@ -54,7 +54,11 @@ pub fn init_cpu() -> bool {
+     true
+ }
+ 
+-pub fn init_freemem(ui_p_reg: p_region_t, dtb_p_reg: p_region_t) -> bool {
++pub fn init_freemem(
++    ui_p_reg: p_region_t,
++    dtb_p_reg: p_region_t,
++    extra_device_p_reg: p_region_t,
++) -> bool {
+     unsafe {
+         res_reg[0].start = paddr_to_pptr(kpptr_to_paddr(KERNEL_ELF_BASE));
+         res_reg[0].end = paddr_to_pptr(kpptr_to_paddr(ffi_addr!(ki_end)));
+@@ -69,8 +73,13 @@ pub fn init_freemem(ui_p_reg: p_region_t, dtb_p_reg: p_region_t) -> bool {
+         }
+         unsafe {
+             res_reg[index] = paddr_to_pptr_reg(&dtb_p_reg);
+-            index += 1;
+         }
++        index += 1;
++    }
++
++    if extra_device_p_reg.start != 0 {
++        unsafe { res_reg[index] = paddr_to_pptr_reg(&extra_device_p_reg) }
++        index += 1;
+     }
+ 
+     // here use the MODE_RESERVED:ARRAY_SIZE(mode_reserved_region) to judge
+diff --git a/kernel/src/boot/interface.rs b/kernel/src/boot/interface.rs
+index 3725848..70448d0 100644
+--- a/kernel/src/boot/interface.rs
++++ b/kernel/src/boot/interface.rs
+@@ -25,6 +25,8 @@ pub fn rust_try_init_kernel(
+     v_entry: usize,
+     dtb_phys_addr: usize,
+     dtb_size: usize,
++    extra_device_addr_start: usize,
++    extra_deviec_size: usize,
+ ) -> bool {
+     try_init_kernel(
+         ui_p_reg_start,
+@@ -34,6 +36,8 @@ pub fn rust_try_init_kernel(
+         dtb_phys_addr,
+         dtb_size,
+         ki_boot_end as usize,
++        extra_device_addr_start,
++        extra_deviec_size,
+     )
+ }
+ 
+diff --git a/kernel/src/boot/mod.rs b/kernel/src/boot/mod.rs
+index 1199737..e782e2a 100644
+--- a/kernel/src/boot/mod.rs
++++ b/kernel/src/boot/mod.rs
+@@ -27,7 +27,7 @@ use sel4_task::*;
+ use sel4_vspace::*;
+ 
+ pub use root_server::root_server_init;
+-pub use untyped::create_untypeds;
++pub use untyped::{create_untypeds, create_untypeds_for_region};
+ 
+ #[cfg(feature = "ENABLE_SMP")]
+ pub use utils::{provide_cap, write_slot};
+diff --git a/kernel/src/boot/untyped.rs b/kernel/src/boot/untyped.rs
+index af60762..c3272ba 100644
+--- a/kernel/src/boot/untyped.rs
++++ b/kernel/src/boot/untyped.rs
+@@ -13,9 +13,12 @@ use sel4_common::{
+ };
+ use sel4_vspace::*;
+ 
+-pub fn create_untypeds(root_cnode_cap: &cap_cnode_cap, boot_mem_reuse_reg: region_t) -> bool {
++pub fn create_untypeds(
++    root_cnode_cap: &cap_cnode_cap,
++    boot_mem_reuse_reg: region_t,
++    first_untyped_slot: seL4_SlotPos,
++) -> bool {
+     unsafe {
+-        let first_untyped_slot = ndks_boot.slot_pos_cur;
+         let mut start = 0;
+         for i in 0..ndks_boot.resv_count {
+             let reg = paddr_to_pptr_reg(&p_region_t {
+@@ -80,7 +83,7 @@ pub fn create_untypeds(root_cnode_cap: &cap_cnode_cap, boot_mem_reuse_reg: regio
+     }
+ }
+ 
+-fn create_untypeds_for_region(
++pub fn create_untypeds_for_region(
+     root_cnode_cap: &cap_cnode_cap,
+     device_memory: bool,
+     mut reg: region_t,
diff --git a/sel4_common/.gitrepo b/sel4_common/.gitrepo
index a09c847..b13615e 100644
--- a/sel4_common/.gitrepo
+++ b/sel4_common/.gitrepo
@@ -6,7 +6,7 @@
 [subrepo]
 	remote = git@github.com:rel4team/sel4_common.git
 	branch = mi_dev
-	commit = 9060ef3dc02fbf4f10196572e1b4b633b9e34316
- 	parent = 493b5dca37f6d34e2e26bcb49fa32f726cd2ddf1
+	commit = 831ca7d4bb0f53f524a05fe0207151c3300ad50f
+ 	parent = 038099532c29c681c9500b3091b3bdd3ac05db85
 	method = merge
 	cmdver = 0.4.9
diff --git a/sel4_common/src/sched_context.rs b/sel4_common/src/sched_context.rs
new file mode 100644
index 0000000..8a5c58b
--- /dev/null
+++ b/sel4_common/src/sched_context.rs
@@ -0,0 +1,21 @@
+/// 时钟ticks
+pub type ticks_t = usize;
+
+pub type sched_context_t = sched_context;
+#[repr(C)]
+#[derive(Debug, Clone)]
+pub struct sched_context {
+    // TODO: MCS
+    pub scPeriod: ticks_t,
+    pub scConsumed: ticks_t,
+    pub scCore: usize,
+    pub scTcb: usize,
+    pub scReply: usize,
+    pub scNotification: usize,
+    pub scBadge: usize,
+    pub scYieldFrom: usize,
+    pub scRefillMax: usize,
+    pub scRefillHead: usize,
+    pub scRefillTail: usize,
+    pub scSporadic: bool,
+}
diff --git a/sel4_cspace/.gitrepo b/sel4_cspace/.gitrepo
index 7b19bb0..d3e574d 100644
--- a/sel4_cspace/.gitrepo
+++ b/sel4_cspace/.gitrepo
@@ -6,7 +6,7 @@
 [subrepo]
 	remote = git@github.com:rel4team/sel4_cspace.git
 	branch = mi_dev
-	commit = e053937baff8452e02983724db31d6e3f667ea30
- 	parent = 493b5dca37f6d34e2e26bcb49fa32f726cd2ddf1
+	commit = 59b7edaa7893ec1bd485b84f7648b82c1cff589a
+ 	parent = 038099532c29c681c9500b3091b3bdd3ac05db85
 	method = merge
 	cmdver = 0.4.9
diff --git a/sel4_ipc/.gitrepo b/sel4_ipc/.gitrepo
index 3375f75..9c85881 100644
--- a/sel4_ipc/.gitrepo
+++ b/sel4_ipc/.gitrepo
@@ -6,7 +6,7 @@
 [subrepo]
 	remote = git@github.com:rel4team/sel4_ipc.git
 	branch = mi_dev
-	commit = bebf7ea40201fe59ae82a56a37101adb8e6aed40
- 	parent = 493b5dca37f6d34e2e26bcb49fa32f726cd2ddf1
+	commit = f49b85f55b5552575e808fa2f1ad42421cf163cf
+ 	parent = 038099532c29c681c9500b3091b3bdd3ac05db85
 	method = merge
 	cmdver = 0.4.9
diff --git a/sel4_task/.gitrepo b/sel4_task/.gitrepo
index ed9143a..e280780 100644
--- a/sel4_task/.gitrepo
+++ b/sel4_task/.gitrepo
@@ -6,7 +6,7 @@
 [subrepo]
 	remote = git@github.com:rel4team/sel4_task.git
 	branch = mi_dev
-	commit = f8e03f79957fb7d4ea914f94daa6b029b972af53
- 	parent = 493b5dca37f6d34e2e26bcb49fa32f726cd2ddf1
+	commit = 09f051669f0d347d06fdfad41e86acff0a4ae311
+ 	parent = 038099532c29c681c9500b3091b3bdd3ac05db85
 	method = merge
 	cmdver = 0.4.9
diff --git a/sel4_task/src/lib.rs b/sel4_task/src/lib.rs
index aa1c15f..4b6e944 100644
--- a/sel4_task/src/lib.rs
+++ b/sel4_task/src/lib.rs
@@ -24,3 +24,4 @@ pub use structures::*;
 pub use tcb::*;
 pub use tcb_queue::*;
 pub use thread_state::*;
+pub use ffi::*;
\ No newline at end of file
diff --git a/sel4_vspace/.gitrepo b/sel4_vspace/.gitrepo
index 7937555..3d37ecf 100644
--- a/sel4_vspace/.gitrepo
+++ b/sel4_vspace/.gitrepo
@@ -7,6 +7,6 @@
 	remote = git@github.com:rel4team/sel4_vspace.git
 	branch = mi_dev
 	commit = aa09a5551f4590c2aac6ab311f89a1727f21b18c
- 	parent = 493b5dca37f6d34e2e26bcb49fa32f726cd2ddf1
+ 	parent = 038099532c29c681c9500b3091b3bdd3ac05db85
 	method = merge
 	cmdver = 0.4.9
diff --git a/serial-frame/.gitrepo b/serial-frame/.gitrepo
index 9acf57e..0dfe03c 100644
--- a/serial-frame/.gitrepo
+++ b/serial-frame/.gitrepo
@@ -7,6 +7,6 @@
 	remote = git@github.com:rel4team/serial-frame.git
 	branch = mi_dev
 	commit = 84501a7640813af351464cbb915ba1f63a9f68fe
- 	parent = 493b5dca37f6d34e2e26bcb49fa32f726cd2ddf1
+ 	parent = 038099532c29c681c9500b3091b3bdd3ac05db85
 	method = merge
 	cmdver = 0.4.9
diff --git a/serial-impl/pl011/.gitrepo b/serial-impl/pl011/.gitrepo
index 6c8dc8a..4d124bb 100644
--- a/serial-impl/pl011/.gitrepo
+++ b/serial-impl/pl011/.gitrepo
@@ -7,6 +7,6 @@
 	remote = git@github.com:rel4team/serial-impl-pl011.git
 	branch = mi_dev
 	commit = 83e073e19e74420a877b7b099e02c7667e6d6244
- 	parent = 493b5dca37f6d34e2e26bcb49fa32f726cd2ddf1
+ 	parent = 038099532c29c681c9500b3091b3bdd3ac05db85
 	method = merge
 	cmdver = 0.4.9
diff --git a/serial-impl/sbi/.gitrepo b/serial-impl/sbi/.gitrepo
index c874d85..cc54648 100644
--- a/serial-impl/sbi/.gitrepo
+++ b/serial-impl/sbi/.gitrepo
@@ -7,6 +7,6 @@
 	remote = git@github.com:rel4team/serial-impl-sbi.git
 	branch = mi_dev
 	commit = 4face963815d4a453f47589ced43cdf9068fde7b
- 	parent = 493b5dca37f6d34e2e26bcb49fa32f726cd2ddf1
+ 	parent = 038099532c29c681c9500b3091b3bdd3ac05db85
 	method = merge
 	cmdver = 0.4.9