Switch to two level cnodes

example/cap_sharing/Makefile

@@ -55,6 +55,8 @@ LIBS := -lmicrokit -Tmicrokit.ld
 
 IMAGE_FILE = $(BUILD_DIR)/loader.img
 REPORT_FILE = $(BUILD_DIR)/report.txt
+SPEC = $(BUILD_DIR)/capdl_spec.json
+KERNEL_32B = $(BUILD_DIR)/sel4_32.elf
 
 all: $(IMAGE_FILE)
 
@@ -67,5 +69,34 @@ $(BUILD_DIR)/%.o: %.c Makefile | $(BUILD_DIR)
 $(BUILD_DIR)/%.elf: $(BUILD_DIR)/%.o
 	$(LD) $(LDFLAGS) $^ $(LIBS) -o $@
 
-$(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) cap_sharing.system
-	$(MICROKIT_TOOL) cap_sharing.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)
+$(IMAGE_FILE) $(KERNEL_32B) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) cap_sharing.system
+	$(MICROKIT_TOOL) cap_sharing.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE) --capdl-json $(SPEC)
+
+ifeq ($(ARCH),x86_64)
+qemu: $(KERNEL_32B) $(IMAGE_FILE)
+	qemu-system-x86_64                                \
+		-cpu qemu64,+fsgsbase,+pdpe1gb,+xsaveopt,+xsave \
+		-m "1G"                                         \
+		-display none                                   \
+		-serial mon:stdio                               \
+		-kernel $(KERNEL_32B)                           \
+		-initrd $(IMAGE_FILE)
+else ifeq ($(ARCH),aarch64)
+qemu: $(IMAGE_FILE)
+	qemu-system-aarch64                               \
+		-machine virt,virtualization=on -cpu cortex-a53 \
+		-nographic                                      \
+		-m size=2G                                      \
+		-serial mon:stdio                               \
+		-device loader,file=$(IMAGE_FILE),addr=0x70000000,cpu-num=0
+else ifeq ($(ARCH),riscv64)
+qemu: $(IMAGE_FILE)
+	qemu-system-riscv64                               \
+		-machine virt                                   \
+		-kernel $(IMAGE_FILE)                           \
+		-nographic                                      \
+		-m size=2G                                      \
+		-serial mon:stdio
+else
+$(error Unsupported ARCH)
+endif

libmicrokit/include/microkit.h

@@ -33,6 +33,10 @@ typedef seL4_MessageInfo_t microkit_msginfo;
 #define BASE_IOPORT_CAP 394
 #define BASE_USER_CAPS 458
 
+/* This should be kept in sync with `PD_ROOT_CAP_BITS` in capdl/builder.rs */
+#define PD_ROOT_CAP_BITS 6
+#define PD_ROOT_CAP_SIZE (1ULL << PD_ROOT_CAP_BITS)
+
 #define MICROKIT_MAX_USER_CAPS 128
 #define MICROKIT_MAX_CHANNELS 62
 #define MICROKIT_MAX_CHANNEL_ID (MICROKIT_MAX_CHANNELS - 1)
@@ -594,9 +598,9 @@ static inline void microkit_deferred_irq_ack(microkit_channel ch)
  **/
 static inline seL4_CPtr microkit_cspace_root_slot_to_cptr(seL4_Word slot)
 {
-    if (slot > MICROKIT_MAX_USER_CAPS) {
+    if (slot == 0 || slot >= PD_ROOT_CAP_SIZE) {
         return seL4_CapNull;
     }
 
-    return BASE_USER_CAPS + slot;
+    return slot << (seL4_WordBits - PD_ROOT_CAP_BITS);
 }

tool/microkit/src/capdl/builder.rs

@@ -95,14 +95,11 @@ const PD_BASE_PD_TCB_CAP: u64 = PD_BASE_IRQ_CAP + 64;
 const PD_BASE_VM_TCB_CAP: u64 = PD_BASE_PD_TCB_CAP + 64;
 const PD_BASE_VCPU_CAP: u64 = PD_BASE_VM_TCB_CAP + 64;
 const PD_BASE_IOPORT_CAP: u64 = PD_BASE_VCPU_CAP + 64;
-// The following region can be used for whatever the user wants to map into their
-// cspace. We restrict them to use this region so that they don't accidently
-// overwrite other parts of the cspace. The cspace slot that the users provide
-// for mapping in extra caps such as TCBs and SCs will be as an offset to this
-// index. We are bounding this to 128 slots for now.
-const PD_BASE_USER_CAPS: u64 = PD_BASE_IOPORT_CAP + 64;
-
-pub const PD_CAP_SIZE: u32 = 1024;
+
+/* This should be kept in sync with `PD_ROOT_CAP_BITS` in libmicrokit/include/microkit.h */
+const PD_ROOT_CAP_SIZE: u32 = 64;
+const PD_ROOT_CAP_BITS: u8 = PD_ROOT_CAP_SIZE.ilog2() as u8;
+pub const PD_CAP_SIZE: u32 = 512;
 const PD_CAP_BITS: u8 = PD_CAP_SIZE.ilog2() as u8;
 const PD_SCHEDCONTEXT_EXTRA_SIZE: u64 = 256;
 const PD_SCHEDCONTEXT_EXTRA_SIZE_BITS: u64 = PD_SCHEDCONTEXT_EXTRA_SIZE.ilog2() as u64;
@@ -120,6 +117,7 @@ pub struct ExpectedAllocation {
 
 struct PDShadowCspace {
     cspace: ObjectId,
+    microkit_cnode: ObjectId,
     notification: ObjectId,
     endpoint: Option<ObjectId>,
     sched_context: ObjectId,
@@ -1014,11 +1012,29 @@ pub fn build_capdl_spec(
             PD_CAP_BITS,
             caps_to_insert_to_pd_cspace,
         );
-        let pd_guard_size = kernel_config.cap_address_bits - PD_CAP_BITS as u64;
+        let pd_guard_size =
+            kernel_config.cap_address_bits - PD_CAP_BITS as u64 - PD_ROOT_CAP_BITS as u64;
         let pd_cnode_cap = capdl_util_make_cnode_cap(pd_cnode_obj_id, 0, pd_guard_size as u8);
+
+        let pd_root_cnode_obj_id = capdl_util_make_cnode_obj(
+            &mut spec_container,
+            &(pd.name.clone() + "_root"),
+            PD_ROOT_CAP_BITS,
+            Vec::new(),
+        );
+        // leave the guard size root cnode as 0
+        let pd_root_cnode_cap = capdl_util_make_cnode_cap(pd_root_cnode_obj_id, 0, 0);
+        // place microkit managed cnode at slot 0
+        capdl_util_insert_cap_into_cspace(
+            &mut spec_container,
+            pd_root_cnode_obj_id,
+            0,
+            pd_cnode_cap,
+        );
+
         caps_to_bind_to_tcb.push(capdl_util_make_cte(
             TcbBoundSlot::CSpace as u32,
-            pd_cnode_cap,
+            pd_root_cnode_cap,
         ));
 
         // Step 3-14 Set the TCB parameters and all the various caps that we need to bind to this TCB.
@@ -1070,7 +1086,8 @@ pub fn build_capdl_spec(
         pd_shadow_cspaces.insert(
             pd_global_idx,
             PDShadowCspace {
-                cspace: pd_cnode_obj_id,
+                cspace: pd_root_cnode_obj_id,
+                microkit_cnode: pd_cnode_obj_id,
                 endpoint: pd_ep_obj_id,
                 notification: pd_ntfn_obj_id,
                 sched_context: pd_sc_obj_id,
@@ -1084,8 +1101,8 @@ pub fn build_capdl_spec(
     // Step 4. Create channels
     // *********************************
     for channel in system.channels.iter() {
-        let pd_a_cspace_id = pd_shadow_cspaces[&channel.end_a.pd].cspace;
-        let pd_b_cspace_id = pd_shadow_cspaces[&channel.end_b.pd].cspace;
+        let pd_a_cspace_id = pd_shadow_cspaces[&channel.end_a.pd].microkit_cnode;
+        let pd_b_cspace_id = pd_shadow_cspaces[&channel.end_b.pd].microkit_cnode;
         let pd_a_ntfn_id = pd_shadow_cspaces[&channel.end_a.pd].notification;
         let pd_b_ntfn_id = pd_shadow_cspaces[&channel.end_b.pd].notification;
 
@@ -1162,15 +1179,33 @@ pub fn build_capdl_spec(
             let cap_map_obj = match cap_map.cap_type {
                 CapMapType::Tcb => capdl_util_make_tcb_cap(pd_src_shadow_cspace.tcb),
                 CapMapType::Sc => capdl_util_make_sc_cap(pd_src_shadow_cspace.sched_context),
-                CapMapType::VSpace => capdl_util_make_sc_cap(pd_src_shadow_cspace.vspace),
-                CapMapType::CSpace => capdl_util_make_sc_cap(pd_src_shadow_cspace.cspace),
+                CapMapType::VSpace => capdl_util_make_page_table_cap(pd_src_shadow_cspace.vspace),
+                CapMapType::CSpace => {
+                    let Some(named_object) =
+                        spec_container.get_root_object(pd_src_shadow_cspace.cspace)
+                    else {
+                        unreachable!("internal bug: couldn't find cnode with given obj id.");
+                    };
+                    let Object::CNode(ref cnode) = named_object.object else {
+                        unreachable!(
+                            "internal bug: got a non-CNode object id {} with name '{}'",
+                            usize::from(pd_src_shadow_cspace.cspace),
+                            named_object.name.as_ref().unwrap()
+                        );
+                    };
+
+                    let guard_size =
+                        kernel_config.cap_address_bits as u8 - PD_ROOT_CAP_BITS - cnode.size_bits;
+
+                    capdl_util_make_cnode_cap(pd_src_shadow_cspace.cspace, 0, guard_size)
+                }
             };
 
             // Map this into the destination pd's cspace and the specified slot.
             capdl_util_insert_cap_into_cspace(
                 &mut spec_container,
                 pd_dest_cspace_id,
-                (PD_BASE_USER_CAPS + cap_map.slot) as u32,
+                cap_map.slot as u32,
                 cap_map_obj,
             );
         }

tool/microkit/src/sdf.rs

@@ -1372,6 +1372,14 @@ impl CapMap {
 
         let slot = sdf_parse_number(checked_lookup(xml_sdf, node, "slot")?, node)?;
 
+        if slot == 0 {
+            return Err(value_error(
+                xml_sdf,
+                node,
+                ("The destination slot 0 has been reserved for Microkit CNode").to_string(),
+            ));
+        }
+
         // TODO: Rework this so that we don't have a fixed upper limit.
         if slot >= CAP_MAP_MAX_SLOT {
             return Err(value_error(

tool/microkit/tests/sdf/cap_mappings_slot_invalid.system

@@ -0,0 +1,19 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2026, UNSW
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <protection_domain name="pd_a">
+        <program_image path="test" />
+    </protection_domain>
+
+    <protection_domain name="pd_b">
+        <program_image path="test" />
+
+        <cspace>
+            <cap_sc slot="0" pd="pd_a" />
+        </cspace>
+    </protection_domain>
+</system>

tool/microkit/tests/test.rs

@@ -1040,6 +1040,15 @@ mod system {
         )
     }
 
+    #[test]
+    fn test_cap_mappings_slot_invalid() {
+        check_error(
+            &DEFAULT_AARCH64_KERNEL_CONFIG,
+            "cap_mappings_slot_invalid.system",
+            "Error: The destination slot 0 has been reserved for Microkit CNode on element 'cap_sc'",
+        )
+    }
+
     #[test]
     fn test_cap_mappings_invalid() {
         check_error(