From 065e54eee5742a8be026213400073f0fcd76e75e Mon Sep 17 00:00:00 2001 From: Szymon Duchniewicz Date: Thu, 5 Feb 2026 17:09:55 +1100 Subject: [PATCH 1/5] Add SDF attribute for untyped handoff * Add boolean attribute to Protection Domain node in System Description File `receive_all_untypeds`, which selects which PD is to receive all remaining untyped objects after CapDL initialiser runs Signed-off-by: Szymon Duchniewicz --- tool/microkit/src/sdf.rs | 31 ++++++++++++++++++++++++++++++- 1 file changed, 30 insertions(+), 1 deletion(-) diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 17b5adba..2b7bcd21 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -271,6 +271,9 @@ pub struct ProtectionDomain { pub parent: Option, /// Value of the setvar_id attribute, if a parent protection domain exists pub setvar_id: Option, + /// If true, CapDL initialiser will hand off all remaining untyped + /// capabilities to this PD. (Can only be set by one PD) + pub receive_all_untypeds: bool, /// Location in the parsed SDF file text_pos: Option, } @@ -456,6 +459,7 @@ impl ProtectionDomain { // but we do the error-checking further down. "smc", "cpu", + "receive_all_untypeds", ]; if is_child { attrs.push("id"); @@ -544,6 +548,21 @@ impl ProtectionDomain { } } + let receive_all_untypeds = if let Some(xml_receive_all_untypeds) = node.attribute("receive_all_untypeds") { + match str_to_bool(xml_receive_all_untypeds) { + Some(val) => val, + None => { + return Err(value_error( + xml_sdf, + node, + "receive_all_untypeds must be 'true' or 'false'".to_string(), + )) + } + } + } else { + false + }; + let cpu = CpuCore( sdf_parse_number(node.attribute("cpu").unwrap_or("0"), node)? .try_into() @@ -1083,6 +1102,7 @@ impl ProtectionDomain { has_children, parent: None, setvar_id, + receive_all_untypeds, text_pos: Some(xml_sdf.doc.text_pos_at(node.range().start)), }) } @@ -1713,7 +1733,7 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result 1 { return Err(format!( @@ -1726,6 +1746,15 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result Date: Fri, 13 Feb 2026 17:00:34 +1100 Subject: [PATCH 2/5] Add parsing for specific MR with patched vaddr for receive all untypeds Signed-off-by: Szymon Duchniewicz --- example/hello/hello.c | 1 + example/hello/hello.system | 7 ++++- tool/microkit/src/capdl/builder.rs | 4 +++ tool/microkit/src/capdl/util.rs | 3 +- tool/microkit/src/sdf.rs | 44 ++++++++++++++++-------------- 5 files changed, 37 insertions(+), 22 deletions(-) diff --git a/example/hello/hello.c b/example/hello/hello.c index 493c9574..68fedda8 100644 --- a/example/hello/hello.c +++ b/example/hello/hello.c @@ -6,6 +6,7 @@ #include #include +uintptr_t remaining_untypeds_vaddr; void init(void) { microkit_dbg_puts("hello, world\n"); diff --git a/example/hello/hello.system b/example/hello/hello.system index dd40ea35..5335391c 100644 --- a/example/hello/hello.system +++ b/example/hello/hello.system @@ -5,7 +5,12 @@ SPDX-License-Identifier: BSD-2-Clause --> + + - \ No newline at end of file + + + + diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index c4057587..0b04afe9 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -439,6 +439,7 @@ pub fn build_capdl_spec( capdl_util_make_cte(MON_REPLY_CAP_IDX as u32, mon_reply_cap), ] .to_vec(), + false, ); let mon_guard_size = kernel_config.cap_address_bits - PD_CAP_BITS as u64; let mon_cnode_cap = capdl_util_make_cnode_cap(mon_cnode_obj_id, 0, mon_guard_size as u8); @@ -839,6 +840,7 @@ pub fn build_capdl_spec( &format!("{}_{}", virtual_machine.name, vcpu.id), PD_CAP_BITS, [].to_vec(), + false, ); let vm_guard_size = kernel_config.cap_address_bits - PD_CAP_BITS as u64; let vm_cnode_cap = @@ -955,11 +957,13 @@ pub fn build_capdl_spec( } // Step 3-13 Create CSpace and add all caps that the PD code and libmicrokit need to access. + let pd_cnode_obj_id = capdl_util_make_cnode_obj( &mut spec_container, &pd.name, PD_CAP_BITS, caps_to_insert_to_pd_cspace, + pd.receive_all_untypeds, ); let pd_guard_size = kernel_config.cap_address_bits - PD_CAP_BITS as u64; let pd_cnode_cap = capdl_util_make_cnode_cap(pd_cnode_obj_id, 0, pd_guard_size as u8); diff --git a/tool/microkit/src/capdl/util.rs b/tool/microkit/src/capdl/util.rs index a1c20e3c..90a96682 100644 --- a/tool/microkit/src/capdl/util.rs +++ b/tool/microkit/src/capdl/util.rs @@ -219,8 +219,9 @@ pub fn capdl_util_make_cnode_obj( pd_name: &str, size_bits: u8, slots: Vec, + receive_all_untypeds: bool, ) -> ObjectId { - let cnode_inner_obj = Object::CNode(object::CNode { size_bits, slots }); + let cnode_inner_obj = Object::CNode(object::CNode { size_bits, slots, receive_all_untypeds }); let cnode_obj = CapDLNamedObject { name: format!("cnode_{pd_name}").into(), object: cnode_inner_obj, diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 2b7bcd21..ef890900 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -459,7 +459,7 @@ impl ProtectionDomain { // but we do the error-checking further down. "smc", "cpu", - "receive_all_untypeds", + //"receive_all_untypeds", ]; if is_child { attrs.push("id"); @@ -548,20 +548,20 @@ impl ProtectionDomain { } } - let receive_all_untypeds = if let Some(xml_receive_all_untypeds) = node.attribute("receive_all_untypeds") { - match str_to_bool(xml_receive_all_untypeds) { - Some(val) => val, - None => { - return Err(value_error( - xml_sdf, - node, - "receive_all_untypeds must be 'true' or 'false'".to_string(), - )) - } - } - } else { - false - }; + //let receive_all_untypeds = if let Some(xml_receive_all_untypeds) = node.attribute("receive_all_untypeds") { + // match str_to_bool(xml_receive_all_untypeds) { + // Some(val) => val, + // None => { + // return Err(value_error( + // xml_sdf, + // node, + // "receive_all_untypeds must be 'true' or 'false'".to_string(), + // )) + // } + // } + //} else { + // false + //}; let cpu = CpuCore( sdf_parse_number(node.attribute("cpu").unwrap_or("0"), node)? @@ -626,6 +626,7 @@ impl ProtectionDomain { )); } + let mut receive_all_untypeds = false; for child in node.children() { if !child.is_element() { continue; @@ -648,6 +649,9 @@ impl ProtectionDomain { "map" => { let map_max_vaddr = config.pd_map_max_vaddr(stack_size); let map = SysMap::from_xml(xml_sdf, &child, true, map_max_vaddr)?; + if map.mr == "remaining_untypeds" { + receive_all_untypeds = true; + } if let Some(setvar_vaddr) = child.attribute("setvar_vaddr") { let setvar = SysSetVar { @@ -1733,7 +1737,7 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result 1 { return Err(format!( @@ -1746,13 +1750,13 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result Date: Fri, 6 Mar 2026 14:11:07 +1100 Subject: [PATCH 3/5] Working: handing off untypeds to microkit PD requires modified rust-sel4, szymon/handoff-untypeds branch --- example/hello/hello.c | 47 ++++++++++++- example/hello/hello.system | 9 ++- example/hierarchy/Makefile | 3 +- tool/microkit/src/capdl/builder.rs | 104 +++++++++++++++++++++++++---- 4 files changed, 146 insertions(+), 17 deletions(-) diff --git a/example/hello/hello.c b/example/hello/hello.c index 68fedda8..efcf37d8 100644 --- a/example/hello/hello.c +++ b/example/hello/hello.c @@ -5,11 +5,56 @@ */ #include #include +//#include +#include uintptr_t remaining_untypeds_vaddr; +typedef struct { + seL4_CNode untyped_cnode_cap; + seL4_SlotRegion untypeds; + seL4_UntypedDesc untypedList[CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; +} capDLBootInfo_t; + +capDLBootInfo_t *capDLBootInfo; + +void print_64(seL4_Word w) { + microkit_dbg_put32((seL4_Uint32) (w >> 32)); + microkit_dbg_put32((seL4_Uint32) w); +} void init(void) { - microkit_dbg_puts("hello, world\n"); + capDLBootInfo = (capDLBootInfo_t*) remaining_untypeds_vaddr; + microkit_dbg_puts("hello, world\nuntyped_cnode_cap: "); + microkit_dbg_put32((seL4_Uint32) (capDLBootInfo->untyped_cnode_cap >> 32)); + microkit_dbg_putc(32); + microkit_dbg_put32((seL4_Uint32) capDLBootInfo->untyped_cnode_cap); + microkit_dbg_puts("\nend\n"); + + microkit_dbg_puts("idx paddr sizeBits isDevice\n"); + for (uint32_t i = capDLBootInfo->untypeds.start; i < capDLBootInfo->untypeds.end; i++) { + microkit_dbg_put32(i); + microkit_dbg_puts(" "); + print_64(capDLBootInfo->untypedList[i].paddr); + microkit_dbg_puts(" "); + print_64(capDLBootInfo->untypedList[i].sizeBits); + microkit_dbg_puts(" "); + if(capDLBootInfo->untypedList[i].isDevice) { + microkit_dbg_puts("true\n"); + } else { + microkit_dbg_puts("false\n"); + } + } + + // Try retype untyped idx 39 + microkit_dbg_puts("Creating new untyped from Untyped Idx 39 of size 4 at idx 68"); + seL4_Error err = seL4_Untyped_Retype(capDLBootInfo->untyped_cnode_cap + 39, seL4_UntypedObject, 4, capDLBootInfo->untyped_cnode_cap, 0, 0, 68, 1); + + microkit_dbg_puts("seL4_NoError: "); + microkit_dbg_put32(seL4_NoError); + microkit_dbg_puts("\n"); + microkit_dbg_puts("err: "); + microkit_dbg_put32(err); + microkit_dbg_puts("\n"); } void notified(microkit_channel ch) diff --git a/example/hello/hello.system b/example/hello/hello.system index 5335391c..84d31cba 100644 --- a/example/hello/hello.system +++ b/example/hello/hello.system @@ -5,12 +5,19 @@ SPDX-License-Identifier: BSD-2-Clause --> - + + + + + + diff --git a/example/hierarchy/Makefile b/example/hierarchy/Makefile index b117946b..d0020c93 100644 --- a/example/hierarchy/Makefile +++ b/example/hierarchy/Makefile @@ -56,6 +56,7 @@ LIBS := -lmicrokit -Tmicrokit.ld IMAGE_FILE = $(BUILD_DIR)/loader.img REPORT_FILE = $(BUILD_DIR)/report.txt +SPEC = $(BUILD_DIR)/capdl_spec.json all: $(IMAGE_FILE) @@ -75,4 +76,4 @@ $(BUILD_DIR)/hello.elf: $(addprefix $(BUILD_DIR)/, $(HELLO_OBJS)) $(LD) $(LDFLAGS) $^ $(LIBS) -o $@ $(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) hierarchy.system - $(MICROKIT_TOOL) hierarchy.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE) + $(MICROKIT_TOOL) hierarchy.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE) --capdl-json ${SPEC} diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 0b04afe9..d366fdb4 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -957,21 +957,97 @@ pub fn build_capdl_spec( } // Step 3-13 Create CSpace and add all caps that the PD code and libmicrokit need to access. + // If this pd is supposed to receive all remaining untypeds, do what + // https://github.com/Neutrality-ch/microkit/commit/34d4b8d2e246dd77bcd538027277e37a5ba97764 + // proposed: create a new root CNode, and insert the Microkit CNode at index 0, (this means + // old CPtr's will still point to valid capabilities in the Microkit CNode), and create a + // placeholder CNode at index 1 of the new root CNode which will be receiving the untypeds. + // Mark the receiving CNode. + if pd.receive_all_untypeds { + let root_cnode_size_bits = 6; // XXX: for now 64 slots (2^{64}) + let receiving_untyped_cnode_size_bits = 8; // TODO: + // log2(MAX_NUM_BOOTINFO_UNTYPED_CAPS)?, + // some other precalculated value? + // Populate the below with pd_cnode_cap and pd_receiving_untyped_cnode_cap or use + // capdl_util_insert_cap_into_cspace instead? (whats the benefit of the first + // approach?) + //let mut caps_to_insert_to_pd_root_cspace: Vec = Vec::new(); + // TODO: slots: for pd_root_cnode_obj will need to contain the original Microkit CNode + // and the to-be-populated untyped receiving CNode + let pd_cnode_obj_id = capdl_util_make_cnode_obj( + &mut spec_container, + &pd.name, + PD_CAP_BITS, + caps_to_insert_to_pd_cspace, + false, + ); + let mut pd_guard_size = kernel_config.cap_address_bits - PD_CAP_BITS as u64 - root_cnode_size_bits as u64; + println!("pd cnode guard size: {}", pd_guard_size); + let pd_cnode_cap = capdl_util_make_cnode_cap(pd_cnode_obj_id, 0, pd_guard_size as u8); + + let pd_receiving_untyped_cnode_obj_id = capdl_util_make_cnode_obj( + &mut spec_container, + &(pd.name.clone() + "_receiving_untypeds"), + receiving_untyped_cnode_size_bits, + Vec::new(), + true, + ); + // OLD: pd_guard_size = kernel_config.cap_address_bits - receiving_untyped_cnode_size_bits as u64 - root_cnode_size_bits as u64; + pd_guard_size = kernel_config.cap_address_bits - receiving_untyped_cnode_size_bits as u64 - root_cnode_size_bits as u64; + // XXX: for the cap, do guard size up to the size_bits, so when addressing from the + // receiving_untypeds_cnode_cap, one can use max depth + println!("receivning untyped guard size: {}", pd_guard_size); + let pd_receiving_untyped_cnode_cap = capdl_util_make_cnode_cap(pd_receiving_untyped_cnode_obj_id, 0, pd_guard_size as u8); + let pd_receiving_untyped_cnode_cap_self_ref = capdl_util_make_cnode_cap(pd_receiving_untyped_cnode_obj_id, 0, pd_guard_size as u8); + capdl_util_insert_cap_into_cspace(&mut spec_container, pd_receiving_untyped_cnode_obj_id, 0, pd_receiving_untyped_cnode_cap_self_ref); + + // ------- FIGURE OUT + //caps_to_insert_to_pd_root_cspace.push(pd_cnode_cap); + //// XXX: INSTEAD do: pub fn capdl_util_insert_cap_into_cspace(? + //caps_to_insert_to_pd_root_cspace.push(capdl_util_make_cte( + // PD_TCB_CAP_IDX as u32, + // capdl_util_make_tcb_cap(pd_tcb_obj_id), + //)); + // ------- + let pd_root_cnode_obj_id = capdl_util_make_cnode_obj( + &mut spec_container, + &(pd.name.clone() + "_root"), + root_cnode_size_bits, + Vec::new(), + false, + ); + pd_guard_size = 0; // so the old Microkit CNode indexes work as expected, but other + // CNode's (such as receiving untyped one) can be addressed at the + // root_cnode_size_bits most significant bits of the address. + println!("root cnode guard size: {}", pd_guard_size); + let pd_root_cnode_cap = capdl_util_make_cnode_cap(pd_root_cnode_obj_id, 0, pd_guard_size as u8); + // XXX: insert original Microkit CNode at idx 0, and receiving untyped Cnode at idx 1 + capdl_util_insert_cap_into_cspace(&mut spec_container, pd_root_cnode_obj_id, 0, pd_cnode_cap); + capdl_util_insert_cap_into_cspace(&mut spec_container, pd_root_cnode_obj_id, 1, pd_receiving_untyped_cnode_cap); + + caps_to_bind_to_tcb.push(capdl_util_make_cte( + TcbBoundSlot::CSpace as u32, + pd_root_cnode_cap, + )); + // XXX: change this to root? or is this fine + pd_id_to_cspace_id.insert(pd_global_idx, pd_cnode_obj_id); + } else { + let pd_cnode_obj_id = capdl_util_make_cnode_obj( + &mut spec_container, + &pd.name, + PD_CAP_BITS, + caps_to_insert_to_pd_cspace, + pd.receive_all_untypeds, + ); + let pd_guard_size = kernel_config.cap_address_bits - PD_CAP_BITS as u64; + let pd_cnode_cap = capdl_util_make_cnode_cap(pd_cnode_obj_id, 0, pd_guard_size as u8); + caps_to_bind_to_tcb.push(capdl_util_make_cte( + TcbBoundSlot::CSpace as u32, + pd_cnode_cap, + )); + pd_id_to_cspace_id.insert(pd_global_idx, pd_cnode_obj_id); + } - let pd_cnode_obj_id = capdl_util_make_cnode_obj( - &mut spec_container, - &pd.name, - PD_CAP_BITS, - caps_to_insert_to_pd_cspace, - pd.receive_all_untypeds, - ); - let pd_guard_size = kernel_config.cap_address_bits - PD_CAP_BITS as u64; - let pd_cnode_cap = capdl_util_make_cnode_cap(pd_cnode_obj_id, 0, pd_guard_size as u8); - caps_to_bind_to_tcb.push(capdl_util_make_cte( - TcbBoundSlot::CSpace as u32, - pd_cnode_cap, - )); - pd_id_to_cspace_id.insert(pd_global_idx, pd_cnode_obj_id); // Step 3-14 Set the TCB parameters and all the various caps that we need to bind to this TCB. if let Object::Tcb(pd_tcb) = &mut spec_container From 9e37ff20939447247b7d98a68eaed5f958b75127 Mon Sep 17 00:00:00 2001 From: Szymon Duchniewicz Date: Mon, 9 Mar 2026 15:50:57 +1100 Subject: [PATCH 4/5] Handoff untypeds: mark frame for receiving untypeds Signed-off-by: Szymon Duchniewicz --- Cargo.toml | 12 +++-- tool/microkit/src/capdl/builder.rs | 19 ++++---- tool/microkit/src/capdl/util.rs | 2 + tool/microkit/src/sdf.rs | 71 ++++++++++++++++++------------ 4 files changed, 63 insertions(+), 41 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index 225db1c1..d5facdda 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -12,12 +12,16 @@ members = [ ] [workspace.dependencies.sel4-capdl-initializer] -git = "https://github.com/seL4/rust-seL4" -rev = "0ac1c27ee6cb9edac7a1a41a69b0d421e170d6a4" +git = "https://github.com/au-ts/rust-seL4" +branch = "szymon/handoff-untypeds" +#git = "https://github.com/seL4/rust-seL4" +#rev = "0ac1c27ee6cb9edac7a1a41a69b0d421e170d6a4" [workspace.dependencies.sel4-capdl-initializer-types] -git = "https://github.com/seL4/rust-seL4" -rev = "0ac1c27ee6cb9edac7a1a41a69b0d421e170d6a4" +git = "https://github.com/au-ts/rust-seL4" +branch = "szymon/handoff-untypeds" +#git = "https://github.com/seL4/rust-seL4" +#rev = "0ac1c27ee6cb9edac7a1a41a69b0d421e170d6a4" [profile.release.package.microkit-tool] strip = true diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index d366fdb4..b6e86c8f 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -246,6 +246,7 @@ impl CapDLSpecContainer { &format!("elf_{pd_name}_{frame_sequence:09}"), None, PageSize::Small.fixed_size_bits(sel4_config) as u8, + false, ); let frame_cap = capdl_util_make_frame_cap( frame_obj_id, @@ -286,6 +287,7 @@ impl CapDLSpecContainer { &format!("ipcbuf_{pd_name}"), None, PageSize::Small.fixed_size_bits(sel4_config) as u8, + false, ); let ipcbuf_frame_cap = capdl_util_make_frame_cap(ipcbuf_frame_obj_id, true, true, false, true); @@ -453,6 +455,7 @@ pub fn build_capdl_spec( &format!("{MONITOR_PD_NAME}_stack"), None, PageSize::Small.fixed_size_bits(kernel_config) as u8, + false, ); let mon_stack_frame_cap = capdl_util_make_frame_cap(mon_stack_frame_obj_id, true, true, false, true); @@ -507,6 +510,8 @@ pub fn build_capdl_spec( let mut frame_ids = Vec::new(); let frame_size_bits = mr.page_size.fixed_size_bits(kernel_config); + // If this MR is supposed to receive untyped metadata, mark the first frame in the spec + let mut receive_all_untypeds = mr.receive_all_untypeds; for frame_sequence in 0..mr.page_count { let paddr = mr .paddr() @@ -519,7 +524,10 @@ pub fn build_capdl_spec( &format!("mr_{}_{:09}", mr.name, frame_sequence), paddr, frame_size_bits as u8, + receive_all_untypeds, )); + // Only mark the first frame in the Memory Region + receive_all_untypeds = false; } mr_name_to_frames.insert(&mr.name, frame_ids); @@ -630,6 +638,7 @@ pub fn build_capdl_spec( &format!("{}_stack_{:09}", pd.name, stack_frame_seq), None, PageSize::Small.fixed_size_bits(kernel_config) as u8, + false, ); let stack_frame_cap = capdl_util_make_frame_cap(stack_frame_obj_id, true, true, false, true); @@ -860,6 +869,7 @@ pub fn build_capdl_spec( None, // Must be consistent with the granule bits used in spec serialisation PageSize::Small.fixed_size_bits(kernel_config) as u8, + false, ); let vm_ipcbuf_frame_cap = capdl_util_make_frame_cap(vm_ipcbuf_frame_obj_id, true, true, false, true); @@ -1001,14 +1011,6 @@ pub fn build_capdl_spec( let pd_receiving_untyped_cnode_cap_self_ref = capdl_util_make_cnode_cap(pd_receiving_untyped_cnode_obj_id, 0, pd_guard_size as u8); capdl_util_insert_cap_into_cspace(&mut spec_container, pd_receiving_untyped_cnode_obj_id, 0, pd_receiving_untyped_cnode_cap_self_ref); - // ------- FIGURE OUT - //caps_to_insert_to_pd_root_cspace.push(pd_cnode_cap); - //// XXX: INSTEAD do: pub fn capdl_util_insert_cap_into_cspace(? - //caps_to_insert_to_pd_root_cspace.push(capdl_util_make_cte( - // PD_TCB_CAP_IDX as u32, - // capdl_util_make_tcb_cap(pd_tcb_obj_id), - //)); - // ------- let pd_root_cnode_obj_id = capdl_util_make_cnode_obj( &mut spec_container, &(pd.name.clone() + "_root"), @@ -1021,7 +1023,6 @@ pub fn build_capdl_spec( // root_cnode_size_bits most significant bits of the address. println!("root cnode guard size: {}", pd_guard_size); let pd_root_cnode_cap = capdl_util_make_cnode_cap(pd_root_cnode_obj_id, 0, pd_guard_size as u8); - // XXX: insert original Microkit CNode at idx 0, and receiving untyped Cnode at idx 1 capdl_util_insert_cap_into_cspace(&mut spec_container, pd_root_cnode_obj_id, 0, pd_cnode_cap); capdl_util_insert_cap_into_cspace(&mut spec_container, pd_root_cnode_obj_id, 1, pd_receiving_untyped_cnode_cap); diff --git a/tool/microkit/src/capdl/util.rs b/tool/microkit/src/capdl/util.rs index 90a96682..8e6017d0 100644 --- a/tool/microkit/src/capdl/util.rs +++ b/tool/microkit/src/capdl/util.rs @@ -29,11 +29,13 @@ pub fn capdl_util_make_frame_obj( name: &str, paddr: Option, size_bits: u8, + receive_all_untypeds: bool, ) -> ObjectId { let frame_inner_obj = Object::Frame(object::Frame { size_bits, paddr, init: frame_init, + receive_all_untypeds, }); let frame_obj = CapDLNamedObject { name: format!("frame_{name}").into(), diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index ef890900..a0cb8b7e 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -125,6 +125,10 @@ pub struct SysMemoryRegion { /// due to the user's SDF or created by the tool for setting up the /// stack, ELF, etc. pub kind: SysMemoryRegionKind, + // Set to true means the PD which maps this memory region (only one allowed) + // will receive all untyped memory capabilities and this memory region will + // receive metadata on all of these untyped objects. + pub receive_all_untypeds: bool, } impl SysMemoryRegion { @@ -459,7 +463,6 @@ impl ProtectionDomain { // but we do the error-checking further down. "smc", "cpu", - //"receive_all_untypeds", ]; if is_child { attrs.push("id"); @@ -548,20 +551,6 @@ impl ProtectionDomain { } } - //let receive_all_untypeds = if let Some(xml_receive_all_untypeds) = node.attribute("receive_all_untypeds") { - // match str_to_bool(xml_receive_all_untypeds) { - // Some(val) => val, - // None => { - // return Err(value_error( - // xml_sdf, - // node, - // "receive_all_untypeds must be 'true' or 'false'".to_string(), - // )) - // } - // } - //} else { - // false - //}; let cpu = CpuCore( sdf_parse_number(node.attribute("cpu").unwrap_or("0"), node)? @@ -626,7 +615,6 @@ impl ProtectionDomain { )); } - let mut receive_all_untypeds = false; for child in node.children() { if !child.is_element() { continue; @@ -649,9 +637,6 @@ impl ProtectionDomain { "map" => { let map_max_vaddr = config.pd_map_max_vaddr(stack_size); let map = SysMap::from_xml(xml_sdf, &child, true, map_max_vaddr)?; - if map.mr == "remaining_untypeds" { - receive_all_untypeds = true; - } if let Some(setvar_vaddr) = child.attribute("setvar_vaddr") { let setvar = SysSetVar { @@ -1106,7 +1091,7 @@ impl ProtectionDomain { has_children, parent: None, setvar_id, - receive_all_untypeds, + receive_all_untypeds: false, text_pos: Some(xml_sdf.doc.text_pos_at(node.range().start)), }) } @@ -1244,7 +1229,7 @@ impl SysMemoryRegion { xml_sdf: &XmlSystemDescription, node: &roxmltree::Node, ) -> Result { - check_attributes(xml_sdf, node, &["name", "size", "page_size", "phys_addr"])?; + check_attributes(xml_sdf, node, &["name", "size", "page_size", "phys_addr", "receive_all_untypeds"])?; let name = checked_lookup(xml_sdf, node, "name")?; let size = sdf_parse_number(checked_lookup(xml_sdf, node, "size")?, node)?; @@ -1293,6 +1278,21 @@ impl SysMemoryRegion { let page_count = size / page_size; + let receive_all_untypeds = if let Some(xml_receive_all_untypeds) = node.attribute("receive_all_untypeds") { + match str_to_bool(xml_receive_all_untypeds) { + Some(val) => val, + None => { + return Err(value_error( + xml_sdf, + node, + "receive_all_untypeds must be 'true' or 'false'".to_string(), + )) + } + } + } else { + false + }; + Ok(SysMemoryRegion { name: name.to_string(), size, @@ -1302,6 +1302,7 @@ impl SysMemoryRegion { phys_addr, text_pos: Some(xml_sdf.doc.text_pos_at(node.range().start)), kind: SysMemoryRegionKind::User, + receive_all_untypeds: receive_all_untypeds, }) } } @@ -1738,7 +1739,8 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result 1 { return Err(format!( "Error: duplicate protection domain name '{}'.", @@ -1750,17 +1752,30 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result 1 { + return Err( + "Error: only one MR can receive the remaining untypeds".to_string() + ); + } for mr in &mrs { if mrs.iter().filter(|x| mr.name == x.name).count() > 1 { return Err(format!( From fcce0c5c451853516d2d9ae86677814c9704140d Mon Sep 17 00:00:00 2001 From: Szymon Duchniewicz Date: Mon, 9 Mar 2026 16:13:06 +1100 Subject: [PATCH 5/5] Clean up: add new example for untyped handoff Signed-off-by: Szymon Duchniewicz --- example/handoff_untypeds/Makefile | 72 +++++++++++++++++++ example/handoff_untypeds/README.md | 23 ++++++ .../handoff_untypeds/handoff_untypeds.system | 13 ++++ example/handoff_untypeds/hello.c | 68 ++++++++++++++++++ example/hello/hello.c | 48 +------------ example/hello/hello.system | 14 +--- example/hierarchy/Makefile | 3 +- 7 files changed, 179 insertions(+), 62 deletions(-) create mode 100644 example/handoff_untypeds/Makefile create mode 100644 example/handoff_untypeds/README.md create mode 100644 example/handoff_untypeds/handoff_untypeds.system create mode 100644 example/handoff_untypeds/hello.c diff --git a/example/handoff_untypeds/Makefile b/example/handoff_untypeds/Makefile new file mode 100644 index 00000000..6b270321 --- /dev/null +++ b/example/handoff_untypeds/Makefile @@ -0,0 +1,72 @@ +# +# Copyright 2026, UNSW +# Copyright 2021, Breakaway Consulting Pty. Ltd. +# +# SPDX-License-Identifier: BSD-2-Clause +# +ifeq ($(strip $(BUILD_DIR)),) +$(error BUILD_DIR must be specified) +endif + +ifeq ($(strip $(MICROKIT_SDK)),) +$(error MICROKIT_SDK must be specified) +endif + +ifeq ($(strip $(MICROKIT_BOARD)),) +$(error MICROKIT_BOARD must be specified) +endif + +ifeq ($(strip $(MICROKIT_CONFIG)),) +$(error MICROKIT_CONFIG must be specified) +endif + +BOARD_DIR := $(MICROKIT_SDK)/board/$(MICROKIT_BOARD)/$(MICROKIT_CONFIG) + +ARCH := ${shell grep 'CONFIG_SEL4_ARCH ' $(BOARD_DIR)/include/kernel/gen_config.h | cut -d' ' -f4} + +ifeq ($(ARCH),aarch64) + TARGET_TRIPLE := aarch64-none-elf + CFLAGS_ARCH := -mstrict-align +else ifeq ($(ARCH),riscv64) + TARGET_TRIPLE := riscv64-unknown-elf + CFLAGS_ARCH := -march=rv64imafdc_zicsr_zifencei -mabi=lp64d +else ifeq ($(ARCH),x86_64) + TARGET_TRIPLE := x86_64-elf + CFLAGS_ARCH := -march=x86-64 -mtune=generic +else +$(error Unsupported ARCH) +endif + +ifeq ($(strip $(LLVM)),True) + CC := clang -target $(TARGET_TRIPLE) + AS := clang -target $(TARGET_TRIPLE) + LD := ld.lld +else + CC := $(TARGET_TRIPLE)-gcc + LD := $(TARGET_TRIPLE)-ld + AS := $(TARGET_TRIPLE)-as +endif + +MICROKIT_TOOL ?= $(MICROKIT_SDK)/bin/microkit + +HELLO_OBJS := hello.o + +IMAGES := hello.elf +CFLAGS := -nostdlib -ffreestanding -g -O3 -Wall -Wno-unused-function -Werror -I$(BOARD_DIR)/include $(CFLAGS_ARCH) +LDFLAGS := -L$(BOARD_DIR)/lib +LIBS := -lmicrokit -Tmicrokit.ld + +IMAGE_FILE = $(BUILD_DIR)/loader.img +REPORT_FILE = $(BUILD_DIR)/report.txt +SPEC = $(BUILD_DIR)/capdl_spec.json + +all: $(IMAGE_FILE) + +$(BUILD_DIR)/%.o: %.c Makefile + $(CC) -c $(CFLAGS) $< -o $@ + +$(BUILD_DIR)/hello.elf: $(addprefix $(BUILD_DIR)/, $(HELLO_OBJS)) + $(LD) $(LDFLAGS) $^ $(LIBS) -o $@ + +$(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) handoff_untypeds.system + $(MICROKIT_TOOL) handoff_untypeds.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE) --capdl-json ${SPEC} diff --git a/example/handoff_untypeds/README.md b/example/handoff_untypeds/README.md new file mode 100644 index 00000000..1215cd8d --- /dev/null +++ b/example/handoff_untypeds/README.md @@ -0,0 +1,23 @@ + +# Example - Handoff untypeds + +This is a basic example that has a single protection domain +that receives capabilities to all remaining untyped memory, +prints information about the untypeds upon initialisation and +has an example of using these untypeds for creating new kernel objects. + +All supported platforms are supported in this example. + +## Building + +```sh +mkdir build +make BUILD_DIR=build MICROKIT_BOARD= MICROKIT_CONFIG= MICROKIT_SDK=/path/to/sdk +``` + +## Running + +See instructions for your board in the manual. diff --git a/example/handoff_untypeds/handoff_untypeds.system b/example/handoff_untypeds/handoff_untypeds.system new file mode 100644 index 00000000..0ddc140d --- /dev/null +++ b/example/handoff_untypeds/handoff_untypeds.system @@ -0,0 +1,13 @@ + + + + + + + + + diff --git a/example/handoff_untypeds/hello.c b/example/handoff_untypeds/hello.c new file mode 100644 index 00000000..2baafb91 --- /dev/null +++ b/example/handoff_untypeds/hello.c @@ -0,0 +1,68 @@ +/* + * Copyright 2026, UNSW + * + * SPDX-License-Identifier: BSD-2-Clause + */ +#include +#include +//#include +#include + +uintptr_t remaining_untypeds_vaddr; +typedef struct { + seL4_CNode untyped_cnode_cptr; + seL4_SlotRegion untypeds; + seL4_UntypedDesc untypedList[CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; +} capDLBootInfo_t; + +capDLBootInfo_t *capDLBootInfo; + +void print_64(seL4_Word w) { + microkit_dbg_put32((seL4_Uint32) (w >> 32)); + microkit_dbg_put32((seL4_Uint32) w); +} +void init(void) +{ + capDLBootInfo = (capDLBootInfo_t*) remaining_untypeds_vaddr; + microkit_dbg_puts("hello, world\nuntyped_cnode_cptr: "); + microkit_dbg_put32((seL4_Uint32) (capDLBootInfo->untyped_cnode_cptr >> 32)); + microkit_dbg_putc(32); + microkit_dbg_put32((seL4_Uint32) capDLBootInfo->untyped_cnode_cptr); + microkit_dbg_puts("\nend\n"); + + microkit_dbg_puts("idx paddr sizeBits isDevice\n"); + for (uint32_t i = capDLBootInfo->untypeds.start; i < capDLBootInfo->untypeds.end; i++) { + microkit_dbg_put32(i); + microkit_dbg_puts(" "); + print_64(capDLBootInfo->untypedList[i].paddr); + microkit_dbg_puts(" "); + print_64(capDLBootInfo->untypedList[i].sizeBits); + microkit_dbg_puts(" "); + if(capDLBootInfo->untypedList[i].isDevice) { + microkit_dbg_puts("true\n"); + } else { + microkit_dbg_puts("false\n"); + } + } + + // Try retype untyped idx 39 + uint32_t untyped_idx = 40; + microkit_dbg_puts("Creating new untyped from Untyped Idx "); + microkit_dbg_put32(untyped_idx); + microkit_dbg_puts(" of size 4 at idx "); + microkit_dbg_put32(capDLBootInfo->untypeds.end); + seL4_Error err = seL4_Untyped_Retype(capDLBootInfo->untyped_cnode_cptr + untyped_idx, seL4_UntypedObject, 4, capDLBootInfo->untyped_cnode_cptr, 0, 0, capDLBootInfo->untypeds.end, 1); + // XXX: add Capability to the root CNode for Djawula (maybe?) + //seL4_Error err = seL4_Untyped_Retype(capDLBootInfo->untyped_cnode_cptr + 39, seL4_CNodeObject, 4, (uint64_t) 2 << (64-6), 0, 0, 68, 1); + + microkit_dbg_puts("\nseL4_NoError: "); + microkit_dbg_put32(seL4_NoError); + microkit_dbg_puts("\n"); + microkit_dbg_puts("err: "); + microkit_dbg_put32(err); + microkit_dbg_puts("\n"); +} + +void notified(microkit_channel ch) +{ +} diff --git a/example/hello/hello.c b/example/hello/hello.c index efcf37d8..493c9574 100644 --- a/example/hello/hello.c +++ b/example/hello/hello.c @@ -5,56 +5,10 @@ */ #include #include -//#include -#include -uintptr_t remaining_untypeds_vaddr; -typedef struct { - seL4_CNode untyped_cnode_cap; - seL4_SlotRegion untypeds; - seL4_UntypedDesc untypedList[CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; -} capDLBootInfo_t; - -capDLBootInfo_t *capDLBootInfo; - -void print_64(seL4_Word w) { - microkit_dbg_put32((seL4_Uint32) (w >> 32)); - microkit_dbg_put32((seL4_Uint32) w); -} void init(void) { - capDLBootInfo = (capDLBootInfo_t*) remaining_untypeds_vaddr; - microkit_dbg_puts("hello, world\nuntyped_cnode_cap: "); - microkit_dbg_put32((seL4_Uint32) (capDLBootInfo->untyped_cnode_cap >> 32)); - microkit_dbg_putc(32); - microkit_dbg_put32((seL4_Uint32) capDLBootInfo->untyped_cnode_cap); - microkit_dbg_puts("\nend\n"); - - microkit_dbg_puts("idx paddr sizeBits isDevice\n"); - for (uint32_t i = capDLBootInfo->untypeds.start; i < capDLBootInfo->untypeds.end; i++) { - microkit_dbg_put32(i); - microkit_dbg_puts(" "); - print_64(capDLBootInfo->untypedList[i].paddr); - microkit_dbg_puts(" "); - print_64(capDLBootInfo->untypedList[i].sizeBits); - microkit_dbg_puts(" "); - if(capDLBootInfo->untypedList[i].isDevice) { - microkit_dbg_puts("true\n"); - } else { - microkit_dbg_puts("false\n"); - } - } - - // Try retype untyped idx 39 - microkit_dbg_puts("Creating new untyped from Untyped Idx 39 of size 4 at idx 68"); - seL4_Error err = seL4_Untyped_Retype(capDLBootInfo->untyped_cnode_cap + 39, seL4_UntypedObject, 4, capDLBootInfo->untyped_cnode_cap, 0, 0, 68, 1); - - microkit_dbg_puts("seL4_NoError: "); - microkit_dbg_put32(seL4_NoError); - microkit_dbg_puts("\n"); - microkit_dbg_puts("err: "); - microkit_dbg_put32(err); - microkit_dbg_puts("\n"); + microkit_dbg_puts("hello, world\n"); } void notified(microkit_channel ch) diff --git a/example/hello/hello.system b/example/hello/hello.system index 84d31cba..dd40ea35 100644 --- a/example/hello/hello.system +++ b/example/hello/hello.system @@ -5,19 +5,7 @@ SPDX-License-Identifier: BSD-2-Clause --> - - - - - - - - + \ No newline at end of file diff --git a/example/hierarchy/Makefile b/example/hierarchy/Makefile index d0020c93..b117946b 100644 --- a/example/hierarchy/Makefile +++ b/example/hierarchy/Makefile @@ -56,7 +56,6 @@ LIBS := -lmicrokit -Tmicrokit.ld IMAGE_FILE = $(BUILD_DIR)/loader.img REPORT_FILE = $(BUILD_DIR)/report.txt -SPEC = $(BUILD_DIR)/capdl_spec.json all: $(IMAGE_FILE) @@ -76,4 +75,4 @@ $(BUILD_DIR)/hello.elf: $(addprefix $(BUILD_DIR)/, $(HELLO_OBJS)) $(LD) $(LDFLAGS) $^ $(LIBS) -o $@ $(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) hierarchy.system - $(MICROKIT_TOOL) hierarchy.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE) --capdl-json ${SPEC} + $(MICROKIT_TOOL) hierarchy.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)