diff --git a/libmicrokit/include/microkit.h b/libmicrokit/include/microkit.h index db43ff99a..b0e3710fb 100644 --- a/libmicrokit/include/microkit.h +++ b/libmicrokit/include/microkit.h @@ -26,9 +26,13 @@ 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 + +// @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) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index c40575871..c92025cb7 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}, @@ -92,11 +92,18 @@ 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; - -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; @@ -540,11 +547,18 @@ 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 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. let mut monitor_vcpu_idx = 0; @@ -555,6 +569,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(); @@ -564,6 +580,8 @@ 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 { @@ -654,6 +672,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, @@ -681,6 +702,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_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 }; caps_to_insert_to_pd_cspace.push(capdl_util_make_cte( @@ -1079,7 +1108,53 @@ 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.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 + ))?; + + 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, + ); + } + } + } + + // ********************************* + // 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 17b5adbae..2540ebd2c 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -261,6 +261,7 @@ pub struct ProtectionDomain { pub irqs: Vec, pub ioports: Vec, pub setvars: 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. @@ -275,6 +276,19 @@ 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, +} + #[derive(Debug, PartialEq, Eq)] pub struct VirtualMachine { pub vcpus: Vec, @@ -588,6 +602,7 @@ impl ProtectionDomain { let mut ioports = Vec::new(); let mut setvars: Vec = Vec::new(); let mut child_pds = Vec::new(); + let mut cap_maps = Vec::new(); let mut program_image = None; let mut virtual_machine = None; @@ -1042,6 +1057,9 @@ impl ProtectionDomain { virtual_machine = Some(vm); } + "cap" => { + cap_maps.push(CapMap::from_xml(xml_sdf, &child)?); + } _ => { let pos = xml_sdf.doc.text_pos_at(child.range().start); return Err(format!( @@ -1078,6 +1096,7 @@ impl ProtectionDomain { irqs, ioports, setvars, + cap_maps, child_pds, virtual_machine, has_children, @@ -1214,6 +1233,43 @@ 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 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, "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(), + )); + } + + Ok(CapMap { + cap_type, + pd_name, + dest_cspace_slot, + }) + } +} + impl SysMemoryRegion { fn from_xml( config: &Config, @@ -1630,7 +1686,6 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result Result