From fffa8bb2e8ce17fe0bec7f4a28c798a0c28f93ff Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Wed, 5 Nov 2025 16:17:36 +1100 Subject: [PATCH 01/14] tool: Map sc of children into parent cspace Signed-off-by: Krishnan Winter --- libmicrokit/include/microkit.h | 7 ++++--- tool/microkit/src/capdl/builder.rs | 11 ++++++++++- 2 files changed, 14 insertions(+), 4 deletions(-) diff --git a/libmicrokit/include/microkit.h b/libmicrokit/include/microkit.h index 90155d21e..e61417723 100644 --- a/libmicrokit/include/microkit.h +++ b/libmicrokit/include/microkit.h @@ -25,9 +25,10 @@ typedef seL4_MessageInfo_t microkit_msginfo; #define BASE_ENDPOINT_CAP 74 #define BASE_IRQ_CAP 138 #define BASE_TCB_CAP 202 -#define BASE_VM_TCB_CAP 266 -#define BASE_VCPU_CAP 330 -#define BASE_IOPORT_CAP 394 +#define BASE_SC_CAP 266 +#define BASE_VM_TCB_CAP 330 +#define BASE_VCPU_CAP 394 +#define BASE_IOPORT_CAP 458 #define MICROKIT_MAX_CHANNELS 62 #define MICROKIT_MAX_CHANNEL_ID (MICROKIT_MAX_CHANNELS - 1) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 4173a2feb..c953412af 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -92,7 +92,8 @@ const PD_BASE_OUTPUT_NOTIFICATION_CAP: u64 = 10; const PD_BASE_OUTPUT_ENDPOINT_CAP: u64 = PD_BASE_OUTPUT_NOTIFICATION_CAP + 64; const PD_BASE_IRQ_CAP: u64 = PD_BASE_OUTPUT_ENDPOINT_CAP + 64; 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_PD_SC_CAP: u64 = PD_BASE_PD_TCB_CAP + 64; +const PD_BASE_VM_TCB_CAP: u64 = PD_BASE_PD_SC_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; @@ -677,6 +678,14 @@ pub fn build_capdl_spec( capdl_util_make_tcb_cap(pd_tcb_obj_id), ); + // Allow the parent PD to access the child's SC: + capdl_util_insert_cap_into_cspace( + &mut spec, + *parent_cspace_obj_id, + (PD_BASE_PD_SC_CAP + pd.id.unwrap()) as usize, + capdl_util_make_sc_cap(pd_sc_obj_id), + ); + fault_ep_cap } else { // badge = pd_global_idx + 1 because seL4 considers badge = 0 as no badge. From e743f88fcae1a8a242d33c9d51781876118effea Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Thu, 4 Dec 2025 15:12:00 +1100 Subject: [PATCH 02/14] tool: Add mapping a pd's tcb cap into another pd Signed-off-by: Krishnan Winter --- tool/microkit/src/capdl/builder.rs | 41 +++++++++++++++++++++++++++--- tool/microkit/src/sdf.rs | 38 ++++++++++++++++++++++++++- 2 files changed, 75 insertions(+), 4 deletions(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index c953412af..ce175b429 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -541,11 +541,17 @@ pub fn build_capdl_spec( None }; + // Mapping between pd name and id for faster lookups + let mut pd_name_to_id: HashMap = HashMap::new(); + // Keep tabs on each PD's CSpace, Notification and Endpoint objects so we can create channels between them at a later step. let mut pd_id_to_cspace_id: HashMap = HashMap::new(); let mut pd_id_to_ntfn_id: HashMap = HashMap::new(); let mut pd_id_to_ep_id: HashMap = HashMap::new(); + // Keep tabs on caps such as TCB so that we can create additional mappings for the cap into other PD's cspaces. + let mut pd_id_to_tcb_id: HashMap = HashMap::new(); + // Keep track of the global count of vCPU objects so we can bind them to the monitor for setting TCB name in debug config. // Only used on ARM and RISC-V as on x86-64 VMs share the same TCB as PD's which will have their TCB name set separately. let mut monitor_vcpu_idx = 0; @@ -556,6 +562,8 @@ pub fn build_capdl_spec( for (pd_global_idx, pd) in system.protection_domains.iter().enumerate() { let elf_obj = &elfs[pd_global_idx]; + pd_name_to_id.insert(pd.name.clone(), pd_global_idx); + let mut caps_to_bind_to_tcb: Vec = Vec::new(); let mut caps_to_insert_to_pd_cspace: Vec = Vec::new(); @@ -565,6 +573,9 @@ pub fn build_capdl_spec( .unwrap(); let pd_vspace_obj_id = capdl_util_get_vspace_id_from_tcb_id(&spec_container, pd_tcb_obj_id); + pd_id_to_tcb_id.insert(pd_global_idx, pd_tcb_obj_id); + + // In the benchmark configuration, we allow PDs to access their own TCB. // This is necessary for accessing kernel's benchmark API. if kernel_config.benchmark { @@ -680,9 +691,9 @@ pub fn build_capdl_spec( // Allow the parent PD to access the child's SC: capdl_util_insert_cap_into_cspace( - &mut spec, + &mut spec_container, *parent_cspace_obj_id, - (PD_BASE_PD_SC_CAP + pd.id.unwrap()) as usize, + (PD_BASE_PD_SC_CAP + pd.id.unwrap()) as u32, capdl_util_make_sc_cap(pd_sc_obj_id), ); @@ -1088,7 +1099,31 @@ pub fn build_capdl_spec( } // ********************************* - // Step 5. Sort the root objects + // Step 5. Handle extra cap mappings + // ********************************* + + for (pd_dest_idx, pd) in system.protection_domains.iter().enumerate() { + let pd_dest_cspace_id = *pd_id_to_cspace_id.get(&pd_dest_idx).unwrap(); + + for cap_map in pd.tcb_cap_maps.iter() { + // Get the TCB of the pd referenced in cap_map name + let pd_src_idx = pd_name_to_id.get(&cap_map.pd_name) + .ok_or(format!("PD: {}, does not exist when trying to map extra TCB cap into PD: {}", cap_map.pd_name, pd.name))?; + let pd_tcb_id = *pd_id_to_tcb_id.get(&pd_src_idx).unwrap(); + + // Map this into the destination pd's cspace and the specified slot. + let pd_tcb_cap = capdl_util_make_tcb_cap(pd_tcb_id); + capdl_util_insert_cap_into_cspace( + &mut spec_container, + pd_dest_cspace_id, + (PD_BASE_PD_TCB_CAP + cap_map.dest_cspace_slot) as u32, + pd_tcb_cap, + ); + } + } + + // ********************************* + // Step 6. Sort the root objects // ********************************* // The CapDL initialiser expects objects with paddr to come first, then sorted by size so that the // allocation algorithm at run-time can run more efficiently. diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index ab5b6f3b3..7b9f757a8 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -262,6 +262,7 @@ pub struct ProtectionDomain { pub irqs: Vec, pub ioports: Vec, pub setvars: Vec, + pub tcb_cap_maps: Vec, pub virtual_machine: Option, /// Only used when parsing child PDs. All elements will be removed /// once we flatten each PD and its children into one list. @@ -276,6 +277,12 @@ pub struct ProtectionDomain { text_pos: Option, } +#[derive(Debug, PartialEq, Eq)] +pub struct TcbCapMap { + pub pd_name: String, + pub dest_cspace_slot: u64, +} + #[derive(Debug, PartialEq, Eq)] pub struct VirtualMachine { pub vcpus: Vec, @@ -589,6 +596,7 @@ impl ProtectionDomain { let mut ioports = Vec::new(); let mut setvars: Vec = Vec::new(); let mut child_pds = Vec::new(); + let mut tcb_cap_maps = Vec::new(); let mut program_image = None; let mut program_image_for_symbols = None; @@ -1036,6 +1044,9 @@ impl ProtectionDomain { virtual_machine = Some(vm); } + "tcb_cap_map" => { + tcb_cap_maps.push(TcbCapMap::from_xml(xml_sdf, &child)?); + } _ => { let pos = xml_sdf.doc.text_pos_at(child.range().start); return Err(format!( @@ -1073,6 +1084,7 @@ impl ProtectionDomain { irqs, ioports, setvars, + tcb_cap_maps, child_pds, virtual_machine, has_children, @@ -1209,6 +1221,31 @@ impl VirtualMachine { } } +impl TcbCapMap { + fn from_xml( + xml_sdf: &XmlSystemDescription, + node: &roxmltree::Node, + ) -> Result { + check_attributes(xml_sdf, node, &["src_pd_name", "dest_cspace_slot"])?; + + let pd_name = checked_lookup(xml_sdf, node, "src_pd_name")?.to_string(); + let dest_cspace_slot = sdf_parse_number(checked_lookup(xml_sdf, node, "dest_cspace_slot")?, node)?; + + if dest_cspace_slot >= 64 { + return Err(value_error( + xml_sdf, + node, + "There are only 64 destination cspace slots available. Max slot allowed is 63".to_string(), + )); + } + + Ok(TcbCapMap { + pd_name, + dest_cspace_slot, + }) + } +} + impl SysMemoryRegion { fn from_xml( config: &Config, @@ -1625,7 +1662,6 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result Date: Thu, 4 Dec 2025 17:51:40 +1100 Subject: [PATCH 03/14] tool: Error checking for cap maps. User cap region Signed-off-by: Krishnan Winter --- libmicrokit/include/microkit.h | 3 +++ tool/microkit/src/capdl/builder.rs | 14 +++++++--- tool/microkit/src/sdf.rs | 41 ++++++++++++++++++++++++------ 3 files changed, 46 insertions(+), 12 deletions(-) diff --git a/libmicrokit/include/microkit.h b/libmicrokit/include/microkit.h index e61417723..822d6727b 100644 --- a/libmicrokit/include/microkit.h +++ b/libmicrokit/include/microkit.h @@ -30,6 +30,9 @@ typedef seL4_MessageInfo_t microkit_msginfo; #define BASE_VCPU_CAP 394 #define BASE_IOPORT_CAP 458 +// @kwinter: Bounding user caps to 128. Is this restriction ok for now? +#define BASE_USER_CAPS 522 + #define MICROKIT_MAX_CHANNELS 62 #define MICROKIT_MAX_CHANNEL_ID (MICROKIT_MAX_CHANNELS - 1) #define MICROKIT_MAX_IOPORT_ID MICROKIT_MAX_CHANNELS diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index ce175b429..727534f87 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -96,8 +96,14 @@ const PD_BASE_PD_SC_CAP: u64 = PD_BASE_PD_TCB_CAP + 64; const PD_BASE_VM_TCB_CAP: u64 = PD_BASE_PD_SC_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; - -pub const PD_CAP_SIZE: u32 = 512; +// 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; 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; @@ -1108,7 +1114,7 @@ pub fn build_capdl_spec( for cap_map in pd.tcb_cap_maps.iter() { // Get the TCB of the pd referenced in cap_map name let pd_src_idx = pd_name_to_id.get(&cap_map.pd_name) - .ok_or(format!("PD: {}, does not exist when trying to map extra TCB cap into PD: {}", cap_map.pd_name, pd.name))?; + .ok_or(format!("PD: '{}', does not exist when trying to map extra TCB cap into PD: '{}'", cap_map.pd_name, pd.name))?; let pd_tcb_id = *pd_id_to_tcb_id.get(&pd_src_idx).unwrap(); // Map this into the destination pd's cspace and the specified slot. @@ -1116,7 +1122,7 @@ pub fn build_capdl_spec( capdl_util_insert_cap_into_cspace( &mut spec_container, pd_dest_cspace_id, - (PD_BASE_PD_TCB_CAP + cap_map.dest_cspace_slot) as u32, + (PD_BASE_USER_CAPS + cap_map.dest_cspace_slot) as u32, pd_tcb_cap, ); } diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 7b9f757a8..8e8b6aabf 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -262,7 +262,7 @@ pub struct ProtectionDomain { pub irqs: Vec, pub ioports: Vec, pub setvars: Vec, - pub tcb_cap_maps: Vec, + pub tcb_cap_maps: Vec, pub virtual_machine: Option, /// Only used when parsing child PDs. All elements will be removed /// once we flatten each PD and its children into one list. @@ -278,7 +278,7 @@ pub struct ProtectionDomain { } #[derive(Debug, PartialEq, Eq)] -pub struct TcbCapMap { +pub struct CapMap { pub pd_name: String, pub dest_cspace_slot: u64, } @@ -1045,7 +1045,7 @@ impl ProtectionDomain { virtual_machine = Some(vm); } "tcb_cap_map" => { - tcb_cap_maps.push(TcbCapMap::from_xml(xml_sdf, &child)?); + tcb_cap_maps.push(CapMap::from_xml(xml_sdf, &child)?); } _ => { let pos = xml_sdf.doc.text_pos_at(child.range().start); @@ -1221,25 +1221,25 @@ impl VirtualMachine { } } -impl TcbCapMap { +impl CapMap { fn from_xml( xml_sdf: &XmlSystemDescription, node: &roxmltree::Node, - ) -> Result { + ) -> Result { check_attributes(xml_sdf, node, &["src_pd_name", "dest_cspace_slot"])?; let pd_name = checked_lookup(xml_sdf, node, "src_pd_name")?.to_string(); let dest_cspace_slot = sdf_parse_number(checked_lookup(xml_sdf, node, "dest_cspace_slot")?, node)?; - if dest_cspace_slot >= 64 { + if dest_cspace_slot >= 128 { return Err(value_error( xml_sdf, node, - "There are only 64 destination cspace slots available. Max slot allowed is 63".to_string(), + "There are only 128 destination cspace slots available. Max slot allowed is 63".to_string(), )); } - Ok(TcbCapMap { + Ok(CapMap { pd_name, dest_cspace_slot, }) @@ -1921,6 +1921,31 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result Date: Fri, 5 Dec 2025 11:24:05 +1100 Subject: [PATCH 04/14] tool: Add mapping a pd's sc cap into another pd Signed-off-by: Krishnan Winter --- tool/microkit/src/capdl/builder.rs | 25 ++++++++++++++++++++++++- tool/microkit/src/sdf.rs | 28 ++++++++++++++++++++++++++++ 2 files changed, 52 insertions(+), 1 deletion(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 727534f87..340f40ed8 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -555,8 +555,9 @@ pub fn build_capdl_spec( let mut pd_id_to_ntfn_id: HashMap = HashMap::new(); let mut pd_id_to_ep_id: HashMap = HashMap::new(); - // Keep tabs on caps such as TCB so that we can create additional mappings for the cap into other PD's cspaces. + // Keep tabs on caps such as TCB and SC so that we can create additional mappings for the cap into other PD's cspaces. let mut pd_id_to_tcb_id: HashMap = HashMap::new(); + let mut pd_id_to_sc_id: HashMap = HashMap::new(); // Keep track of the global count of vCPU objects so we can bind them to the monitor for setting TCB name in debug config. // Only used on ARM and RISC-V as on x86-64 VMs share the same TCB as PD's which will have their TCB name set separately. @@ -672,6 +673,9 @@ pub fn build_capdl_spec( pd.budget, 0x100 + pd_global_idx as u64, ); + + pd_id_to_sc_id.insert(pd_global_idx, pd_sc_obj_id); + let pd_sc_cap = capdl_util_make_sc_cap(pd_sc_obj_id); caps_to_bind_to_tcb.push(capdl_util_make_cte( TcbBoundSlot::SchedContext as u32, @@ -1126,6 +1130,25 @@ pub fn build_capdl_spec( pd_tcb_cap, ); } + + for cap_map in pd.sc_cap_maps.iter() { + let pd_src_idx = pd_name_to_id.get(&cap_map.pd_name) + .ok_or(format!("PD: '{}', does not exist when trying to map extra SC cap into PD: '{}'", cap_map.pd_name, pd.name))?; + + if system.protection_domains[*pd_src_idx].passive { + return Err(format!("Trying to map scheduling context of a passive PD: '{}' into PD: '{}'", cap_map.pd_name, pd.name)); + } + + let pd_sc_id = *pd_id_to_sc_id.get(&pd_src_idx).unwrap(); + + let pd_sc_cap = capdl_util_make_tcb_cap(pd_sc_id); + capdl_util_insert_cap_into_cspace( + &mut spec_container, + pd_dest_cspace_id, + (PD_BASE_USER_CAPS + cap_map.dest_cspace_slot) as u32, + pd_sc_cap, + ); + } } // ********************************* diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 8e8b6aabf..0cc41a35a 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -263,6 +263,7 @@ pub struct ProtectionDomain { pub ioports: Vec, pub setvars: Vec, pub tcb_cap_maps: Vec, + pub sc_cap_maps: Vec, pub virtual_machine: Option, /// Only used when parsing child PDs. All elements will be removed /// once we flatten each PD and its children into one list. @@ -597,6 +598,7 @@ impl ProtectionDomain { let mut setvars: Vec = Vec::new(); let mut child_pds = Vec::new(); let mut tcb_cap_maps = Vec::new(); + let mut sc_cap_maps = Vec::new(); let mut program_image = None; let mut program_image_for_symbols = None; @@ -1047,6 +1049,9 @@ impl ProtectionDomain { "tcb_cap_map" => { tcb_cap_maps.push(CapMap::from_xml(xml_sdf, &child)?); } + "sc_cap_map" => { + sc_cap_maps.push(CapMap::from_xml(xml_sdf, &child)?); + } _ => { let pos = xml_sdf.doc.text_pos_at(child.range().start); return Err(format!( @@ -1085,6 +1090,7 @@ impl ProtectionDomain { ioports, setvars, tcb_cap_maps, + sc_cap_maps, child_pds, virtual_machine, has_children, @@ -1925,6 +1931,8 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result Result Date: Mon, 5 Jan 2026 13:52:26 +1100 Subject: [PATCH 05/14] tool: Change format of specifying cap maps for pds Signed-off-by: Krishnan Winter --- tool/microkit/src/capdl/builder.rs | 66 +++++++++--------- tool/microkit/src/sdf.rs | 107 +++++++++++++++-------------- 2 files changed, 90 insertions(+), 83 deletions(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 340f40ed8..fb47d35c7 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -24,8 +24,8 @@ use crate::{ }, elf::ElfFile, sdf::{ - CpuCore, SysMap, SysMapPerms, SystemDescription, BUDGET_DEFAULT, MONITOR_PD_NAME, - MONITOR_PRIORITY, + CapMapType, CpuCore, SysMap, SysMapPerms, SystemDescription, BUDGET_DEFAULT, + MONITOR_PD_NAME, MONITOR_PRIORITY, }, sel4::{Arch, Config, PageSize}, util::{ranges_overlap, round_down, round_up}, @@ -582,7 +582,6 @@ pub fn build_capdl_spec( pd_id_to_tcb_id.insert(pd_global_idx, pd_tcb_obj_id); - // In the benchmark configuration, we allow PDs to access their own TCB. // This is necessary for accessing kernel's benchmark API. if kernel_config.benchmark { @@ -1115,39 +1114,42 @@ pub fn build_capdl_spec( for (pd_dest_idx, pd) in system.protection_domains.iter().enumerate() { let pd_dest_cspace_id = *pd_id_to_cspace_id.get(&pd_dest_idx).unwrap(); - for cap_map in pd.tcb_cap_maps.iter() { - // Get the TCB of the pd referenced in cap_map name - let pd_src_idx = pd_name_to_id.get(&cap_map.pd_name) - .ok_or(format!("PD: '{}', does not exist when trying to map extra TCB cap into PD: '{}'", cap_map.pd_name, pd.name))?; - let pd_tcb_id = *pd_id_to_tcb_id.get(&pd_src_idx).unwrap(); + for cap_map in pd.cap_maps.iter() { + let pd_src_idx = pd_name_to_id.get(&cap_map.pd_name).ok_or(format!( + "PD: '{}', does not exist when trying to map extra TCB cap into PD: '{}'", + cap_map.pd_name, pd.name + ))?; - // Map this into the destination pd's cspace and the specified slot. - let pd_tcb_cap = capdl_util_make_tcb_cap(pd_tcb_id); - capdl_util_insert_cap_into_cspace( - &mut spec_container, - pd_dest_cspace_id, - (PD_BASE_USER_CAPS + cap_map.dest_cspace_slot) as u32, - pd_tcb_cap, - ); - } + if cap_map.cap_type == CapMapType::Tcb { + // Get the TCB of the pd referenced in cap_map name + let pd_tcb_id = *pd_id_to_tcb_id.get(pd_src_idx).unwrap(); - for cap_map in pd.sc_cap_maps.iter() { - let pd_src_idx = pd_name_to_id.get(&cap_map.pd_name) - .ok_or(format!("PD: '{}', does not exist when trying to map extra SC cap into PD: '{}'", cap_map.pd_name, pd.name))?; - - if system.protection_domains[*pd_src_idx].passive { - return Err(format!("Trying to map scheduling context of a passive PD: '{}' into PD: '{}'", cap_map.pd_name, pd.name)); - } + // Map this into the destination pd's cspace and the specified slot. + let pd_tcb_cap = capdl_util_make_tcb_cap(pd_tcb_id); + capdl_util_insert_cap_into_cspace( + &mut spec_container, + pd_dest_cspace_id, + (PD_BASE_USER_CAPS + cap_map.dest_cspace_slot) as u32, + pd_tcb_cap, + ); + } else if cap_map.cap_type == CapMapType::Sc { + if system.protection_domains[*pd_src_idx].passive { + return Err(format!( + "Trying to map scheduling context of a passive PD: '{}' into PD: '{}'", + cap_map.pd_name, pd.name + )); + } - let pd_sc_id = *pd_id_to_sc_id.get(&pd_src_idx).unwrap(); + let pd_sc_id = *pd_id_to_sc_id.get(pd_src_idx).unwrap(); - let pd_sc_cap = capdl_util_make_tcb_cap(pd_sc_id); - capdl_util_insert_cap_into_cspace( - &mut spec_container, - pd_dest_cspace_id, - (PD_BASE_USER_CAPS + cap_map.dest_cspace_slot) as u32, - pd_sc_cap, - ); + let pd_sc_cap = capdl_util_make_tcb_cap(pd_sc_id); + capdl_util_insert_cap_into_cspace( + &mut spec_container, + pd_dest_cspace_id, + (PD_BASE_USER_CAPS + cap_map.dest_cspace_slot) as u32, + pd_sc_cap, + ); + } } } diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 0cc41a35a..84d5bc4bc 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -262,8 +262,7 @@ pub struct ProtectionDomain { pub irqs: Vec, pub ioports: Vec, pub setvars: Vec, - pub tcb_cap_maps: Vec, - pub sc_cap_maps: Vec, + pub cap_maps: Vec, pub virtual_machine: Option, /// Only used when parsing child PDs. All elements will be removed /// once we flatten each PD and its children into one list. @@ -278,8 +277,15 @@ pub struct ProtectionDomain { text_pos: Option, } +#[derive(Debug, PartialEq, Eq)] +pub enum CapMapType { + Tcb = 1, + Sc = 2, +} + #[derive(Debug, PartialEq, Eq)] pub struct CapMap { + pub cap_type: CapMapType, pub pd_name: String, pub dest_cspace_slot: u64, } @@ -597,8 +603,7 @@ impl ProtectionDomain { let mut ioports = Vec::new(); let mut setvars: Vec = Vec::new(); let mut child_pds = Vec::new(); - let mut tcb_cap_maps = Vec::new(); - let mut sc_cap_maps = Vec::new(); + let mut cap_maps = Vec::new(); let mut program_image = None; let mut program_image_for_symbols = None; @@ -1046,11 +1051,8 @@ impl ProtectionDomain { virtual_machine = Some(vm); } - "tcb_cap_map" => { - tcb_cap_maps.push(CapMap::from_xml(xml_sdf, &child)?); - } - "sc_cap_map" => { - sc_cap_maps.push(CapMap::from_xml(xml_sdf, &child)?); + "cap" => { + cap_maps.push(CapMap::from_xml(xml_sdf, &child)?); } _ => { let pos = xml_sdf.doc.text_pos_at(child.range().start); @@ -1089,8 +1091,7 @@ impl ProtectionDomain { irqs, ioports, setvars, - tcb_cap_maps, - sc_cap_maps, + cap_maps, child_pds, virtual_machine, has_children, @@ -1228,24 +1229,36 @@ impl VirtualMachine { } impl CapMap { - fn from_xml( - xml_sdf: &XmlSystemDescription, - node: &roxmltree::Node, - ) -> Result { - check_attributes(xml_sdf, node, &["src_pd_name", "dest_cspace_slot"])?; + fn from_xml(xml_sdf: &XmlSystemDescription, node: &roxmltree::Node) -> Result { + check_attributes(xml_sdf, node, &["type", "pd", "dest_cspace_slot"])?; + + let cap_type = match checked_lookup(xml_sdf, node, "type")? { + "tcb" => CapMapType::Tcb, + "sc" => CapMapType::Sc, + _ => { + return Err(value_error( + xml_sdf, + node, + "type must be 'tcb' or 'sc' ".to_string(), + )) + } + }; - let pd_name = checked_lookup(xml_sdf, node, "src_pd_name")?.to_string(); - let dest_cspace_slot = sdf_parse_number(checked_lookup(xml_sdf, node, "dest_cspace_slot")?, node)?; + let pd_name = checked_lookup(xml_sdf, node, "pd")?.to_string(); + let dest_cspace_slot = + sdf_parse_number(checked_lookup(xml_sdf, node, "dest_cspace_slot")?, node)?; if dest_cspace_slot >= 128 { return Err(value_error( xml_sdf, node, - "There are only 128 destination cspace slots available. Max slot allowed is 63".to_string(), + "There are only 128 destination cspace slots available. Max slot allowed is 63" + .to_string(), )); } Ok(CapMap { + cap_type, pd_name, dest_cspace_slot, }) @@ -1928,48 +1941,40 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result Date: Tue, 20 Jan 2026 16:48:38 +1100 Subject: [PATCH 06/14] tool: generalise extra cap mapping implementation Signed-off-by: Krishnan Winter --- tool/microkit/src/capdl/builder.rs | 65 +++++++++++------------------- tool/microkit/src/sdf.rs | 7 ++-- 2 files changed, 28 insertions(+), 44 deletions(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index fb47d35c7..1e96ea068 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -11,8 +11,8 @@ use std::{ }; use sel4_capdl_initializer_types::{ - object, CapTableEntry, Fill, FillEntry, FillEntryContent, NamedObject, Object, ObjectId, Spec, - Word, + object, Cap, CapTableEntry, Fill, FillEntry, FillEntryContent, NamedObject, Object, ObjectId, + Spec, Word, }; use crate::{ @@ -556,8 +556,7 @@ pub fn build_capdl_spec( let mut pd_id_to_ep_id: HashMap = HashMap::new(); // Keep tabs on caps such as TCB and SC so that we can create additional mappings for the cap into other PD's cspaces. - let mut pd_id_to_tcb_id: HashMap = HashMap::new(); - let mut pd_id_to_sc_id: HashMap = HashMap::new(); + let mut pd_shadow_cspace: HashMap>> = HashMap::new(); // Keep track of the global count of vCPU objects so we can bind them to the monitor for setting TCB name in debug config. // Only used on ARM and RISC-V as on x86-64 VMs share the same TCB as PD's which will have their TCB name set separately. @@ -580,15 +579,18 @@ pub fn build_capdl_spec( .unwrap(); let pd_vspace_obj_id = capdl_util_get_vspace_id_from_tcb_id(&spec_container, pd_tcb_obj_id); - pd_id_to_tcb_id.insert(pd_global_idx, pd_tcb_obj_id); + let pd_tcb_obj = capdl_util_make_tcb_cap(pd_tcb_obj_id); + + pd_shadow_cspace + .entry(pd_global_idx) + .or_insert_with(|| vec![None; CapMapType::__Len as usize])[CapMapType::Tcb as usize] = + Some(pd_tcb_obj.clone()); // In the benchmark configuration, we allow PDs to access their own TCB. // This is necessary for accessing kernel's benchmark API. if kernel_config.benchmark { - caps_to_insert_to_pd_cspace.push(capdl_util_make_cte( - PD_TCB_CAP_IDX as u32, - capdl_util_make_tcb_cap(pd_tcb_obj_id), - )); + caps_to_insert_to_pd_cspace + .push(capdl_util_make_cte(PD_TCB_CAP_IDX as u32, pd_tcb_obj)); } // Allow PD to access their own VSpace for ops such as cache cleaning on ARM. @@ -672,10 +674,11 @@ pub fn build_capdl_spec( pd.budget, 0x100 + pd_global_idx as u64, ); + let pd_sc_cap = capdl_util_make_sc_cap(pd_sc_obj_id); - pd_id_to_sc_id.insert(pd_global_idx, pd_sc_obj_id); + pd_shadow_cspace.get_mut(&pd_global_idx).unwrap()[CapMapType::Sc as usize] = + Some(pd_sc_cap.clone()); - let pd_sc_cap = capdl_util_make_sc_cap(pd_sc_obj_id); caps_to_bind_to_tcb.push(capdl_util_make_cte( TcbBoundSlot::SchedContext as u32, pd_sc_cap, @@ -1120,36 +1123,16 @@ pub fn build_capdl_spec( cap_map.pd_name, pd.name ))?; - if cap_map.cap_type == CapMapType::Tcb { - // Get the TCB of the pd referenced in cap_map name - let pd_tcb_id = *pd_id_to_tcb_id.get(pd_src_idx).unwrap(); - - // Map this into the destination pd's cspace and the specified slot. - let pd_tcb_cap = capdl_util_make_tcb_cap(pd_tcb_id); - capdl_util_insert_cap_into_cspace( - &mut spec_container, - pd_dest_cspace_id, - (PD_BASE_USER_CAPS + cap_map.dest_cspace_slot) as u32, - pd_tcb_cap, - ); - } else if cap_map.cap_type == CapMapType::Sc { - if system.protection_domains[*pd_src_idx].passive { - return Err(format!( - "Trying to map scheduling context of a passive PD: '{}' into PD: '{}'", - cap_map.pd_name, pd.name - )); - } - - let pd_sc_id = *pd_id_to_sc_id.get(pd_src_idx).unwrap(); - - let pd_sc_cap = capdl_util_make_tcb_cap(pd_sc_id); - capdl_util_insert_cap_into_cspace( - &mut spec_container, - pd_dest_cspace_id, - (PD_BASE_USER_CAPS + cap_map.dest_cspace_slot) as u32, - pd_sc_cap, - ); - } + let pd_obj = pd_shadow_cspace.get(pd_src_idx).unwrap()[cap_map.cap_type as usize] + .as_ref() + .unwrap(); + // 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.dest_cspace_slot) as u32, + pd_obj.clone(), + ); } } diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 84d5bc4bc..02250b43c 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -277,10 +277,11 @@ pub struct ProtectionDomain { text_pos: Option, } -#[derive(Debug, PartialEq, Eq)] +#[derive(Debug, PartialEq, Eq, Clone, Copy)] pub enum CapMapType { - Tcb = 1, - Sc = 2, + Tcb = 0, + Sc, + __Len, } #[derive(Debug, PartialEq, Eq)] From a60c79e803a8a104d4aee26b0b49791e56e8d362 Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Wed, 21 Jan 2026 15:08:09 +1100 Subject: [PATCH 07/14] tool: Support vspace and cnode extra cap maps Signed-off-by: Krishnan Winter --- tool/microkit/src/capdl/builder.rs | 7 ++++++- tool/microkit/src/sdf.rs | 24 ++++++++++++++++++++++++ 2 files changed, 30 insertions(+), 1 deletion(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 1e96ea068..a7d11c9a2 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -580,11 +580,14 @@ pub fn build_capdl_spec( let pd_vspace_obj_id = capdl_util_get_vspace_id_from_tcb_id(&spec_container, pd_tcb_obj_id); let pd_tcb_obj = capdl_util_make_tcb_cap(pd_tcb_obj_id); + let pd_vspace_obj = capdl_util_make_page_table_cap(pd_vspace_obj_id); pd_shadow_cspace .entry(pd_global_idx) .or_insert_with(|| vec![None; CapMapType::__Len as usize])[CapMapType::Tcb as usize] = Some(pd_tcb_obj.clone()); + pd_shadow_cspace.get_mut(&pd_global_idx).unwrap()[CapMapType::Vspace as usize] = + Some(pd_vspace_obj.clone()); // In the benchmark configuration, we allow PDs to access their own TCB. // This is necessary for accessing kernel's benchmark API. @@ -596,7 +599,7 @@ pub fn build_capdl_spec( // Allow PD to access their own VSpace for ops such as cache cleaning on ARM. caps_to_insert_to_pd_cspace.push(capdl_util_make_cte( PD_VSPACE_CAP_IDX as u32, - capdl_util_make_page_table_cap(pd_vspace_obj_id), + pd_vspace_obj, )); // Step 3-2: Map in all Memory Regions @@ -995,6 +998,8 @@ pub fn build_capdl_spec( ); 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); + pd_shadow_cspace.get_mut(&pd_global_idx).unwrap()[CapMapType::Cnode as usize] = + Some(pd_cnode_cap.clone()); caps_to_bind_to_tcb.push(capdl_util_make_cte( TcbBoundSlot::CSpace as u32, pd_cnode_cap, diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 02250b43c..b105b90c4 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -281,6 +281,8 @@ pub struct ProtectionDomain { pub enum CapMapType { Tcb = 0, Sc, + Vspace, + Cnode, __Len, } @@ -1236,6 +1238,8 @@ impl CapMap { let cap_type = match checked_lookup(xml_sdf, node, "type")? { "tcb" => CapMapType::Tcb, "sc" => CapMapType::Sc, + "vspace" => CapMapType::Vspace, + "cnode" => CapMapType::Cnode, _ => { return Err(value_error( xml_sdf, @@ -1947,6 +1951,8 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result Result Date: Wed, 21 Jan 2026 15:28:35 +1100 Subject: [PATCH 08/14] sdf: Simplify error checking for extra cap maps Signed-off-by: Krishnan Winter --- tool/microkit/src/sdf.rs | 48 +++++++--------------------------------- 1 file changed, 8 insertions(+), 40 deletions(-) diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index b105b90c4..19a34d3ff 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -1946,13 +1946,10 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result = Vec::new(); for cap_map in pd.cap_maps.iter() { if user_cap_slots.contains(&cap_map.dest_cspace_slot) { @@ -1964,42 +1961,13 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result Date: Tue, 27 Jan 2026 12:06:19 +1100 Subject: [PATCH 09/14] address pr comments Signed-off-by: Krishnan Winter --- libmicrokit/include/microkit.h | 1 + tool/microkit/src/capdl/builder.rs | 14 ++++++------- tool/microkit/src/sdf.rs | 33 +++++++++++++++--------------- 3 files changed, 24 insertions(+), 24 deletions(-) diff --git a/libmicrokit/include/microkit.h b/libmicrokit/include/microkit.h index 822d6727b..3a231a09d 100644 --- a/libmicrokit/include/microkit.h +++ b/libmicrokit/include/microkit.h @@ -33,6 +33,7 @@ typedef seL4_MessageInfo_t microkit_msginfo; // @kwinter: Bounding user caps to 128. Is this restriction ok for now? #define BASE_USER_CAPS 522 +#define MICROKIT_MAX_USER_CAPS 128 #define MICROKIT_MAX_CHANNELS 62 #define MICROKIT_MAX_CHANNEL_ID (MICROKIT_MAX_CHANNELS - 1) #define MICROKIT_MAX_IOPORT_ID MICROKIT_MAX_CHANNELS diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index a7d11c9a2..e5745d81e 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -24,7 +24,7 @@ use crate::{ }, elf::ElfFile, sdf::{ - CapMapType, CpuCore, SysMap, SysMapPerms, SystemDescription, BUDGET_DEFAULT, + CapMapType, CpuCore, SysMap, SysMapPerms, SystemDescription, BUDGET_DEFAULT, CAP_MAP_TYPES, MONITOR_PD_NAME, MONITOR_PRIORITY, }, sel4::{Arch, Config, PageSize}, @@ -584,7 +584,7 @@ pub fn build_capdl_spec( pd_shadow_cspace .entry(pd_global_idx) - .or_insert_with(|| vec![None; CapMapType::__Len as usize])[CapMapType::Tcb as usize] = + .or_insert_with(|| vec![None; CAP_MAP_TYPES])[CapMapType::Tcb as usize] = Some(pd_tcb_obj.clone()); pd_shadow_cspace.get_mut(&pd_global_idx).unwrap()[CapMapType::Vspace as usize] = Some(pd_vspace_obj.clone()); @@ -597,10 +597,8 @@ pub fn build_capdl_spec( } // Allow PD to access their own VSpace for ops such as cache cleaning on ARM. - caps_to_insert_to_pd_cspace.push(capdl_util_make_cte( - PD_VSPACE_CAP_IDX as u32, - pd_vspace_obj, - )); + caps_to_insert_to_pd_cspace + .push(capdl_util_make_cte(PD_VSPACE_CAP_IDX as u32, pd_vspace_obj)); // Step 3-2: Map in all Memory Regions for map in pd.maps.iter() { @@ -1120,7 +1118,7 @@ pub fn build_capdl_spec( // ********************************* for (pd_dest_idx, pd) in system.protection_domains.iter().enumerate() { - let pd_dest_cspace_id = *pd_id_to_cspace_id.get(&pd_dest_idx).unwrap(); + let pd_dest_cspace_id = pd_id_to_cspace_id[&pd_dest_idx]; for cap_map in pd.cap_maps.iter() { let pd_src_idx = pd_name_to_id.get(&cap_map.pd_name).ok_or(format!( @@ -1128,7 +1126,7 @@ pub fn build_capdl_spec( cap_map.pd_name, pd.name ))?; - let pd_obj = pd_shadow_cspace.get(pd_src_idx).unwrap()[cap_map.cap_type as usize] + let pd_obj = pd_shadow_cspace[pd_src_idx][cap_map.cap_type as usize] .as_ref() .unwrap(); // Map this into the destination pd's cspace and the specified slot. diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 19a34d3ff..fea2bf84b 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -37,6 +37,10 @@ use std::path::{Path, PathBuf}; const PD_MAX_ID: u64 = 61; const VCPU_MAX_ID: u64 = PD_MAX_ID; +/// This is the maximum slot allowed for cap maps. This can change if you wish, +/// but also update the MICROKIT_MAX_USER_CAPS define in `microkit.h`. +const CAP_MAP_MAX_SLOT: u64 = 128; + pub const MONITOR_PRIORITY: u8 = 255; const PD_MAX_PRIORITY: u8 = 254; /// In microseconds @@ -277,13 +281,15 @@ pub struct ProtectionDomain { text_pos: Option, } +/// Update CAP_MAP_TYPES whenever making changes to the CapMapType enum +pub const CAP_MAP_TYPES: usize = 4; + #[derive(Debug, PartialEq, Eq, Clone, Copy)] pub enum CapMapType { Tcb = 0, Sc, Vspace, Cnode, - __Len, } #[derive(Debug, PartialEq, Eq)] @@ -1235,29 +1241,24 @@ impl CapMap { fn from_xml(xml_sdf: &XmlSystemDescription, node: &roxmltree::Node) -> Result { check_attributes(xml_sdf, node, &["type", "pd", "dest_cspace_slot"])?; - let cap_type = match checked_lookup(xml_sdf, node, "type")? { + let xml_cap_type = checked_lookup(xml_sdf, node, "type")?; + let cap_type = match xml_cap_type { "tcb" => CapMapType::Tcb, "sc" => CapMapType::Sc, "vspace" => CapMapType::Vspace, "cnode" => CapMapType::Cnode, - _ => { - return Err(value_error( - xml_sdf, - node, - "type must be 'tcb' or 'sc' ".to_string(), - )) - } + _ => return Err(format!("Cap type: '{xml_cap_type}' is not supported.")), }; let pd_name = checked_lookup(xml_sdf, node, "pd")?.to_string(); let dest_cspace_slot = sdf_parse_number(checked_lookup(xml_sdf, node, "dest_cspace_slot")?, node)?; - if dest_cspace_slot >= 128 { + if dest_cspace_slot >= CAP_MAP_MAX_SLOT { return Err(value_error( xml_sdf, node, - "There are only 128 destination cspace slots available. Max slot allowed is 63" + format!("There are only {CAP_MAP_MAX_SLOT} destination cspace slots available.") .to_string(), )); } @@ -1951,7 +1952,7 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result = Vec::new(); - for cap_map in pd.cap_maps.iter() { + for cap_map in &pd.cap_maps { if user_cap_slots.contains(&cap_map.dest_cspace_slot) { return Err(format!( "Error: Overlapping cap slot: {} in protection domain: '{}'", @@ -1963,11 +1964,11 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result Date: Wed, 28 Jan 2026 14:29:47 +1100 Subject: [PATCH 10/14] switch to nested hashmaps Signed-off-by: Krishnan Winter --- tool/microkit/src/capdl/builder.rs | 36 ++++++++++++++---------------- tool/microkit/src/sdf.rs | 5 +---- 2 files changed, 18 insertions(+), 23 deletions(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index e5745d81e..5dc6ab5c3 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -24,7 +24,7 @@ use crate::{ }, elf::ElfFile, sdf::{ - CapMapType, CpuCore, SysMap, SysMapPerms, SystemDescription, BUDGET_DEFAULT, CAP_MAP_TYPES, + CapMapType, CpuCore, SysMap, SysMapPerms, SystemDescription, BUDGET_DEFAULT, MONITOR_PD_NAME, MONITOR_PRIORITY, }, sel4::{Arch, Config, PageSize}, @@ -548,7 +548,7 @@ pub fn build_capdl_spec( }; // Mapping between pd name and id for faster lookups - let mut pd_name_to_id: HashMap = HashMap::new(); + let mut pd_name_to_id: HashMap<&String, usize> = HashMap::new(); // Keep tabs on each PD's CSpace, Notification and Endpoint objects so we can create channels between them at a later step. let mut pd_id_to_cspace_id: HashMap = HashMap::new(); @@ -556,7 +556,7 @@ pub fn build_capdl_spec( let mut pd_id_to_ep_id: HashMap = HashMap::new(); // Keep tabs on caps such as TCB and SC so that we can create additional mappings for the cap into other PD's cspaces. - let mut pd_shadow_cspace: HashMap>> = HashMap::new(); + let mut pd_shadow_cspace: HashMap> = HashMap::new(); // Keep track of the global count of vCPU objects so we can bind them to the monitor for setting TCB name in debug config. // Only used on ARM and RISC-V as on x86-64 VMs share the same TCB as PD's which will have their TCB name set separately. @@ -568,8 +568,9 @@ pub fn build_capdl_spec( for (pd_global_idx, pd) in system.protection_domains.iter().enumerate() { let elf_obj = &elfs[pd_global_idx]; - pd_name_to_id.insert(pd.name.clone(), pd_global_idx); + pd_name_to_id.insert(&pd.name, pd_global_idx); + let mut pd_shadow_cspace_inner: HashMap = HashMap::new(); let mut caps_to_bind_to_tcb: Vec = Vec::new(); let mut caps_to_insert_to_pd_cspace: Vec = Vec::new(); @@ -582,12 +583,8 @@ pub fn build_capdl_spec( let pd_tcb_obj = capdl_util_make_tcb_cap(pd_tcb_obj_id); let pd_vspace_obj = capdl_util_make_page_table_cap(pd_vspace_obj_id); - pd_shadow_cspace - .entry(pd_global_idx) - .or_insert_with(|| vec![None; CAP_MAP_TYPES])[CapMapType::Tcb as usize] = - Some(pd_tcb_obj.clone()); - pd_shadow_cspace.get_mut(&pd_global_idx).unwrap()[CapMapType::Vspace as usize] = - Some(pd_vspace_obj.clone()); + pd_shadow_cspace_inner.insert(CapMapType::Tcb, pd_tcb_obj.clone()); + pd_shadow_cspace_inner.insert(CapMapType::Vspace, pd_vspace_obj.clone()); // In the benchmark configuration, we allow PDs to access their own TCB. // This is necessary for accessing kernel's benchmark API. @@ -677,8 +674,7 @@ pub fn build_capdl_spec( ); let pd_sc_cap = capdl_util_make_sc_cap(pd_sc_obj_id); - pd_shadow_cspace.get_mut(&pd_global_idx).unwrap()[CapMapType::Sc as usize] = - Some(pd_sc_cap.clone()); + pd_shadow_cspace_inner.insert(CapMapType::Sc, pd_sc_cap.clone()); caps_to_bind_to_tcb.push(capdl_util_make_cte( TcbBoundSlot::SchedContext as u32, @@ -996,8 +992,7 @@ pub fn build_capdl_spec( ); 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); - pd_shadow_cspace.get_mut(&pd_global_idx).unwrap()[CapMapType::Cnode as usize] = - Some(pd_cnode_cap.clone()); + pd_shadow_cspace_inner.insert(CapMapType::Cnode, pd_cnode_cap.clone()); caps_to_bind_to_tcb.push(capdl_util_make_cte( TcbBoundSlot::CSpace as u32, pd_cnode_cap, @@ -1048,6 +1043,7 @@ pub fn build_capdl_spec( capdl_util_make_ntfn_cap(pd_ntfn_obj_id, true, true, 0), ); } + pd_shadow_cspace.insert(pd_global_idx, pd_shadow_cspace_inner); } // ********************************* @@ -1119,22 +1115,24 @@ pub fn build_capdl_spec( for (pd_dest_idx, pd) in system.protection_domains.iter().enumerate() { let pd_dest_cspace_id = pd_id_to_cspace_id[&pd_dest_idx]; - for cap_map in pd.cap_maps.iter() { let pd_src_idx = pd_name_to_id.get(&cap_map.pd_name).ok_or(format!( "PD: '{}', does not exist when trying to map extra TCB cap into PD: '{}'", cap_map.pd_name, pd.name ))?; - let pd_obj = pd_shadow_cspace[pd_src_idx][cap_map.cap_type as usize] - .as_ref() - .unwrap(); + let pd_shadow_cspace_inner = pd_shadow_cspace.get(pd_src_idx).unwrap(); + + let pd_obj = pd_shadow_cspace_inner + .get(&cap_map.cap_type) + .unwrap() + .clone(); // 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.dest_cspace_slot) as u32, - pd_obj.clone(), + pd_obj, ); } } diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index fea2bf84b..a7f3e2695 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -281,10 +281,7 @@ pub struct ProtectionDomain { text_pos: Option, } -/// Update CAP_MAP_TYPES whenever making changes to the CapMapType enum -pub const CAP_MAP_TYPES: usize = 4; - -#[derive(Debug, PartialEq, Eq, Clone, Copy)] +#[derive(Debug, PartialEq, Eq, Copy, Clone, Hash)] pub enum CapMapType { Tcb = 0, Sc, From 34735485029b840ce5d4143e243a53058167640b Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Fri, 5 Jun 2026 17:26:15 +1000 Subject: [PATCH 11/14] Remove extra SC mapping via parents The only reason why we're keeping the parent PD hierarchy is for backwards compatability, if users want this they should use the new cap sharing API. Signed-off-by: Julia Vassiliki --- libmicrokit/include/microkit.h | 11 ++++------- tool/microkit/src/capdl/builder.rs | 11 +---------- 2 files changed, 5 insertions(+), 17 deletions(-) diff --git a/libmicrokit/include/microkit.h b/libmicrokit/include/microkit.h index 3a231a09d..4ccc2502a 100644 --- a/libmicrokit/include/microkit.h +++ b/libmicrokit/include/microkit.h @@ -25,13 +25,10 @@ typedef seL4_MessageInfo_t microkit_msginfo; #define BASE_ENDPOINT_CAP 74 #define BASE_IRQ_CAP 138 #define BASE_TCB_CAP 202 -#define BASE_SC_CAP 266 -#define BASE_VM_TCB_CAP 330 -#define BASE_VCPU_CAP 394 -#define BASE_IOPORT_CAP 458 - -// @kwinter: Bounding user caps to 128. Is this restriction ok for now? -#define BASE_USER_CAPS 522 +#define BASE_VM_TCB_CAP 266 +#define BASE_VCPU_CAP 330 +#define BASE_IOPORT_CAP 394 +#define BASE_USER_CAPS 458 #define MICROKIT_MAX_USER_CAPS 128 #define MICROKIT_MAX_CHANNELS 62 diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 70b90148e..68958ff93 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -92,8 +92,7 @@ const PD_BASE_OUTPUT_NOTIFICATION_CAP: u64 = 10; const PD_BASE_OUTPUT_ENDPOINT_CAP: u64 = PD_BASE_OUTPUT_NOTIFICATION_CAP + 64; const PD_BASE_IRQ_CAP: u64 = PD_BASE_OUTPUT_ENDPOINT_CAP + 64; const PD_BASE_PD_TCB_CAP: u64 = PD_BASE_IRQ_CAP + 64; -const PD_BASE_PD_SC_CAP: u64 = PD_BASE_PD_TCB_CAP + 64; -const PD_BASE_VM_TCB_CAP: u64 = PD_BASE_PD_SC_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 @@ -731,14 +730,6 @@ pub fn build_capdl_spec( capdl_util_make_tcb_cap(pd_tcb_obj_id), ); - // Allow the parent PD to access the child's SC: - capdl_util_insert_cap_into_cspace( - &mut spec_container, - *parent_cspace_obj_id, - (PD_BASE_PD_SC_CAP + pd.id.unwrap()) as u32, - capdl_util_make_sc_cap(pd_sc_obj_id), - ); - fault_ep_cap } else { // badge = pd_global_idx + 1 because seL4 considers badge = 0 as no badge. From 44cc38845c0a6731e18b3a79e42fb725a1743d5a Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Fri, 5 Jun 2026 17:59:32 +1000 Subject: [PATCH 12/14] capitalisation of CapMapType Signed-off-by: Julia Vassiliki --- tool/microkit/src/capdl/builder.rs | 4 ++-- tool/microkit/src/sdf.rs | 10 +++++----- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 68958ff93..6bc1cfc10 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -616,7 +616,7 @@ pub fn build_capdl_spec( let pd_vspace_obj = capdl_util_make_page_table_cap(pd_vspace_obj_id); pd_shadow_cspace_inner.insert(CapMapType::Tcb, pd_tcb_obj.clone()); - pd_shadow_cspace_inner.insert(CapMapType::Vspace, pd_vspace_obj.clone()); + pd_shadow_cspace_inner.insert(CapMapType::VSpace, pd_vspace_obj.clone()); // In the benchmark configuration, we allow PDs to access their own TCB. // This is necessary for accessing kernel's benchmark API. @@ -1021,7 +1021,7 @@ pub fn build_capdl_spec( ); 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); - pd_shadow_cspace_inner.insert(CapMapType::Cnode, pd_cnode_cap.clone()); + pd_shadow_cspace_inner.insert(CapMapType::CSpace, pd_cnode_cap.clone()); caps_to_bind_to_tcb.push(capdl_util_make_cte( TcbBoundSlot::CSpace as u32, pd_cnode_cap, diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index a76cba86a..279839bba 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -298,10 +298,10 @@ pub struct ProtectionDomain { #[derive(Debug, PartialEq, Eq, Copy, Clone, Hash)] pub enum CapMapType { - Tcb = 0, + Tcb, Sc, - Vspace, - Cnode, + VSpace, + CSpace, } #[derive(Debug, PartialEq, Eq)] @@ -1339,8 +1339,8 @@ impl CapMap { let cap_type = match xml_cap_type { "tcb" => CapMapType::Tcb, "sc" => CapMapType::Sc, - "vspace" => CapMapType::Vspace, - "cnode" => CapMapType::Cnode, + "vspace" => CapMapType::VSpace, + "cspace" => CapMapType::CSpace, _ => return Err(format!("Cap type: '{xml_cap_type}' is not supported.")), }; From 16c88c604bae956458b18803ab42f6fb5e11eb6a Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Fri, 5 Jun 2026 17:59:47 +1000 Subject: [PATCH 13/14] Remove error about duplicate mappings + make the duplicate slot warn better Signed-off-by: Julia Vassiliki --- tool/microkit/src/sdf.rs | 39 +++++++++++++++++++++++---------------- 1 file changed, 23 insertions(+), 16 deletions(-) diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 279839bba..845b218f0 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -21,7 +21,7 @@ use crate::sel4::{ }; use crate::util::{get_full_path, ranges_overlap, round_up, str_to_bool}; use crate::MAX_PDS; -use std::collections::HashSet; +use std::collections::{HashMap, HashSet}; use std::fmt::Display; use std::fs; use std::path::{Path, PathBuf}; @@ -309,6 +309,8 @@ pub struct CapMap { pub cap_type: CapMapType, pub pd_name: String, pub dest_cspace_slot: u64, + /// Location in the parsed SDF file + text_pos: roxmltree::TextPos, } #[derive(Debug, PartialEq, Eq)] @@ -1361,6 +1363,7 @@ impl CapMap { cap_type, pd_name, dest_cspace_slot, + text_pos: xml_sdf.doc.text_pos_at(node.range().start), }) } } @@ -2141,26 +2144,30 @@ pub fn parse( // Ensure that there are no overlapping extra cap maps in the user caps region // and we are not mapping in the same cap from the same source more than once for pd in &pds { - let mut user_cap_slots = Vec::new(); - let mut seen_pd_cap_maps: Vec<(CapMapType, String)> = Vec::new(); + let mut user_cap_slots = HashMap::>::new(); for cap_map in &pd.cap_maps { - if user_cap_slots.contains(&cap_map.dest_cspace_slot) { - return Err(format!( - "Error: Overlapping cap slot: {} in protection domain: '{}'", - cap_map.dest_cspace_slot, pd.name - )); - } else { - user_cap_slots.push(cap_map.dest_cspace_slot); - } + user_cap_slots + .entry(cap_map.dest_cspace_slot) + .and_modify(|v| v.push(cap_map)) + .or_insert(vec![cap_map]); + } - if seen_pd_cap_maps.contains(&(cap_map.cap_type, cap_map.pd_name.clone())) { + for (slot, cap_maps) in user_cap_slots.iter() { + if cap_maps.len() > 1 { + let mut lines = String::new(); + for mapping in cap_maps { + lines.push_str(&format!( + "\n type {:?} from '{}' at '{}'", + mapping.cap_type, + mapping.pd_name, + loc_string(&xml_sdf, mapping.text_pos) + )); + } return Err(format!( - "Error: Duplicate cap mapping of type '{:?}'. Src PD: '{}', dest PD: '{}'.", - cap_map.cap_type, cap_map.pd_name, pd.name + "Error: overlapping user caps in slot {slot} of protection domain '{}':{}", + pd.name, lines )); - } else { - seen_pd_cap_maps.push((cap_map.cap_type, cap_map.pd_name.clone())) } } } From 157c7c7ffe943dfa8c8bf37467d6f01d2b555c6e Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Fri, 5 Jun 2026 18:00:10 +1000 Subject: [PATCH 14/14] add test Signed-off-by: Julia Vassiliki --- tool/microkit/src/sdf.rs | 10 ++++++-- .../tests/sdf/pd_cap_mappings_invalid.system | 17 +++++++++++++ .../sdf/pd_cap_mappings_overlapping.system | 25 +++++++++++++++++++ tool/microkit/tests/test.rs | 20 +++++++++++++++ 4 files changed, 70 insertions(+), 2 deletions(-) create mode 100644 tool/microkit/tests/sdf/pd_cap_mappings_invalid.system create mode 100644 tool/microkit/tests/sdf/pd_cap_mappings_overlapping.system diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 845b218f0..d59fdcd72 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -1336,6 +1336,7 @@ impl VirtualMachine { impl CapMap { fn from_xml(xml_sdf: &XmlSystemDescription, node: &roxmltree::Node) -> Result { check_attributes(xml_sdf, node, &["type", "pd", "dest_cspace_slot"])?; + let text_pos = xml_sdf.doc.text_pos_at(node.range().start); let xml_cap_type = checked_lookup(xml_sdf, node, "type")?; let cap_type = match xml_cap_type { @@ -1343,7 +1344,12 @@ impl CapMap { "sc" => CapMapType::Sc, "vspace" => CapMapType::VSpace, "cspace" => CapMapType::CSpace, - _ => return Err(format!("Cap type: '{xml_cap_type}' is not supported.")), + _ => { + return Err(format!( + "Cap type: '{xml_cap_type}' is not supported at '{}'", + loc_string(&xml_sdf, text_pos) + )) + } }; let pd_name = checked_lookup(xml_sdf, node, "pd")?.to_string(); @@ -1363,7 +1369,7 @@ impl CapMap { cap_type, pd_name, dest_cspace_slot, - text_pos: xml_sdf.doc.text_pos_at(node.range().start), + text_pos, }) } } diff --git a/tool/microkit/tests/sdf/pd_cap_mappings_invalid.system b/tool/microkit/tests/sdf/pd_cap_mappings_invalid.system new file mode 100644 index 000000000..7debd4bab --- /dev/null +++ b/tool/microkit/tests/sdf/pd_cap_mappings_invalid.system @@ -0,0 +1,17 @@ + + + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/pd_cap_mappings_overlapping.system b/tool/microkit/tests/sdf/pd_cap_mappings_overlapping.system new file mode 100644 index 000000000..0baa66ed5 --- /dev/null +++ b/tool/microkit/tests/sdf/pd_cap_mappings_overlapping.system @@ -0,0 +1,25 @@ + + + + + + + + + + + + + + + + + + + + + diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 056a32368..568b7adae 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -996,4 +996,24 @@ mod system { "Error: fpu must be 'true' or 'false'", ) } + + #[test] + fn test_cap_mappings_overlapping() { + check_error( + &DEFAULT_AARCH64_KERNEL_CONFIG, + "pd_cap_mappings_overlapping.system", + r#"Error: overlapping user caps in slot 4 of protection domain 'pd_b': + type CSpace from 'pd_a' at 'pd_cap_mappings_overlapping.system:21:9' + type CSpace from 'pd_a' at 'pd_cap_mappings_overlapping.system:23:9'"#, + ) + } + + #[test] + fn test_cap_mappings_invalid() { + check_error( + &DEFAULT_AARCH64_KERNEL_CONFIG, + "pd_cap_mappings_invalid.system", + "Cap type: 'gerbils' is not supported at 'pd_cap_mappings_invalid.system:15:9'", + ) + } }