diff --git a/build_sdk.py b/build_sdk.py index 93fa0505b..a335e01c4 100644 --- a/build_sdk.py +++ b/build_sdk.py @@ -239,11 +239,10 @@ def test_tool() -> None: assert r == 0 -def build_tool(tool_target: Path, target_triple: str, experimental_domain_support: bool = False) -> None: - build_cmd = f"cd tool/microkit && cargo build --release --target {target_triple}" - if experimental_domain_support: - build_cmd = f"{build_cmd} --features experimental-domain-support" - r = system(build_cmd) +def build_tool(tool_target: Path, target_triple: str) -> None: + r = system( + f"cd tool/microkit && cargo build --release --target {target_triple}" + ) assert r == 0 tool_output = f"./tool/microkit/target/{target_triple}/release/microkit" @@ -502,7 +501,7 @@ def main() -> None: if not args.skip_tool: tool_target = root_dir / "bin" / "microkit" test_tool() - build_tool(tool_target, args.tool_target_triple, args.experimental_domain_support) + build_tool(tool_target, args.tool_target_triple) if not args.skip_docs: build_doc(root_dir) diff --git a/tool/microkit/Cargo.toml b/tool/microkit/Cargo.toml index e5ddbd87d..590b840e9 100644 --- a/tool/microkit/Cargo.toml +++ b/tool/microkit/Cargo.toml @@ -13,9 +13,6 @@ edition = "2021" name = "microkit" path = "src/main.rs" -[features] -experimental-domain-support = [] - [dependencies] roxmltree = "0.19.0" serde = "1.0.203" diff --git a/tool/microkit/src/main.rs b/tool/microkit/src/main.rs index 4d9d9053b..7f132a8e3 100644 --- a/tool/microkit/src/main.rs +++ b/tool/microkit/src/main.rs @@ -2906,6 +2906,7 @@ fn main() -> Result<(), String> { fan_out_limit: json_str_as_u64(&kernel_config_json, "RETYPE_FAN_OUT_LIMIT")?, arm_pa_size_bits: 40, hypervisor: json_str_as_bool(&kernel_config_json, "ARM_HYPERVISOR_SUPPORT")?, + domain_scheduler: json_str_as_u64(&kernel_config_json, "NUM_DOMAINS")? != 1, }; match kernel_config.arch { diff --git a/tool/microkit/src/sel4.rs b/tool/microkit/src/sel4.rs index 64f6b13d9..e7486fce4 100644 --- a/tool/microkit/src/sel4.rs +++ b/tool/microkit/src/sel4.rs @@ -48,6 +48,7 @@ pub struct Config { pub fan_out_limit: u64, pub hypervisor: bool, pub arm_pa_size_bits: usize, + pub domain_scheduler: bool, } pub enum Arch { diff --git a/tool/microkit/src/sysxml.rs b/tool/microkit/src/sysxml.rs index 1dc74eb4d..d002468b1 100644 --- a/tool/microkit/src/sysxml.rs +++ b/tool/microkit/src/sysxml.rs @@ -75,6 +75,7 @@ fn loc_string(xml_sdf: &XmlSystemDescription, pos: roxmltree::TextPos) -> String pub struct PlatformDescription { /// Note that we have the invariant that page sizes are be ordered by size page_sizes: [u64; 2], + domain_scheduler: bool, } impl PlatformDescription { @@ -83,7 +84,10 @@ impl PlatformDescription { Arch::Aarch64 => [0x1000, 0x200_000], }; - PlatformDescription { page_sizes } + PlatformDescription { + page_sizes, + domain_scheduler: kernel_config.domain_scheduler, + } } } @@ -291,6 +295,7 @@ impl ProtectionDomain { node: &roxmltree::Node, is_child: bool, domain_schedule: &Option, + plat_desc: &PlatformDescription, ) -> Result { let mut attrs = vec![ "name", "priority", "pp", "budget", "period", "passive", "domain", @@ -375,7 +380,7 @@ impl ProtectionDomain { return Err(format!("System specifies a domain schedule but protection domain {} does not specify a domain", name)) } (_, Ok(domain)) => { - if cfg!(feature = "experimental-domain-support") { + if plat_desc.domain_scheduler { return Err(format!("Protection domain {} specifies a domain {} but system does not specify a domain schedule", name, domain)); } else { return Err(format!("Assigning PDs to domains is only supported if SDK is built with --experimental-domain-support")); @@ -498,6 +503,7 @@ impl ProtectionDomain { &child, true, &domain_schedule, + &plat_desc, )?), "virtual_machine" => { if virtual_machine.is_some() { @@ -1050,7 +1056,7 @@ pub fn parse( // then parse the channels. let mut channel_nodes = Vec::new(); - if cfg!(feature = "experimental-domain-support") { + if plat_desc.domain_scheduler { if let Some(domain_schedule_node) = system .children() .filter(|&child| child.is_element()) @@ -1072,11 +1078,12 @@ pub fn parse( &child, false, &domain_schedule, + &plat_desc, )?), "channel" => channel_nodes.push(child), "memory_region" => mrs.push(SysMemoryRegion::from_xml(&xml_sdf, &child, plat_desc)?), "domain_schedule" => { - if !cfg!(feature = "experimental-domain-support") { + if !plat_desc.domain_scheduler { let pos = xml_sdf.doc.text_pos_at(child.range().start); return Err(format!("Domain schedule is only supported if SDK is built with --experimental-domain-support: {}", loc_string(&xml_sdf, pos))); } diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 1913fab82..0755c5daf 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -17,6 +17,7 @@ const DEFAULT_KERNEL_CONFIG: sel4::Config = sel4::Config { fan_out_limit: 256, hypervisor: true, arm_pa_size_bits: 40, + domain_scheduler: false, }; const DEFAULT_PLAT_DESC: sysxml::PlatformDescription =