From 7da0b26121f3ddca4debfc310fd257e3705da6ad Mon Sep 17 00:00:00 2001 From: Bill Nguyen Date: Mon, 13 Jul 2026 10:16:06 +1000 Subject: [PATCH 1/4] manual: priority is optional for virtual machine Because the tool will default to priority 0 if it is not specified. Signed-off-by: Bill Nguyen --- docs/manual.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/manual.md b/docs/manual.md index 3bfef7a26..53717e867 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -1016,7 +1016,7 @@ On x86-64, a PD with a VCPU cannot have child PDs. The `virtual_machine` element has the following attributes: * `name`: A unique name for the virtual machine -* `priority`: The priority of the virtual machine (integer 0 to 254). +* `priority`: (optional) The priority of the virtual machine (integer 0 to 254); defaults to 0. * `budget`: (optional) The VM's budget in microseconds; defaults to 1,000. * `period`: (optional) The VM's period in microseconds; must not be smaller than the budget; defaults to the budget. From 53e41cd25604b853f5d26b23680ff2007f4139cf Mon Sep 17 00:00:00 2001 From: Bill Nguyen Date: Mon, 13 Jul 2026 10:35:43 +1000 Subject: [PATCH 2/4] tool: refactor scheduling internal representation No behavioural changes. Signed-off-by: Bill Nguyen --- tool/microkit/src/capdl/builder.rs | 16 ++++----- tool/microkit/src/sdf.rs | 57 +++++++++++++++++++----------- tool/microkit/src/viper.rs | 4 +-- 3 files changed, 47 insertions(+), 30 deletions(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index ab9863fb9..4fca52eb5 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -720,8 +720,8 @@ pub fn build_capdl_spec( &mut spec_container, &pd.name, PD_SCHEDCONTEXT_EXTRA_SIZE_BITS as u8, - pd.period, - pd.budget, + pd.sched_params.period, + pd.sched_params.budget, 0x100 + pd_global_idx as u64, ); let pd_sc_cap = capdl_util_make_sc_cap(pd_sc_obj_id); @@ -955,8 +955,8 @@ pub fn build_capdl_spec( &mut spec_container, &format!("{}_{}", virtual_machine.name, vcpu.id), PD_SCHEDCONTEXT_EXTRA_SIZE_BITS as u8, - virtual_machine.period, - virtual_machine.budget, + virtual_machine.sched_params.period, + virtual_machine.sched_params.budget, 0x100 + vcpu_idx as u64, ); caps_to_bind_to_vm_tcbs.push(capdl_util_make_cte( @@ -982,8 +982,8 @@ pub fn build_capdl_spec( extra: Box::new(object::TcbExtraInfo { ipc_buffer_addr: Word(0), affinity: Word(vcpu_affinity.0.into()), - prio: virtual_machine.priority, - max_prio: virtual_machine.priority, + prio: virtual_machine.sched_params.priority, + max_prio: virtual_machine.sched_params.priority, // Given the use cases of VMs, for now we always give them FPU access. fpu_disabled: false, resume: false, @@ -1071,8 +1071,8 @@ pub fn build_capdl_spec( pd_tcb.extra.ipc_buffer_addr = Word(kernel_config.pd_ipc_buffer()); pd_tcb.extra.sp = Word(kernel_config.pd_stack_top()); pd_tcb.extra.master_fault_ep = None; // Not used on MCS kernel. - pd_tcb.extra.prio = pd.priority; - pd_tcb.extra.max_prio = pd.priority; + pd_tcb.extra.prio = pd.priority(); + pd_tcb.extra.max_prio = pd.priority(); pd_tcb.extra.fpu_disabled = !pd.fpu; pd_tcb.extra.resume = true; diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 588b380b6..d347b0744 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -265,14 +265,19 @@ impl Display for CpuCore { } } +#[derive(Debug, PartialEq, Eq)] +pub struct SchedulingParams { + pub priority: u8, + pub budget: u64, + pub period: u64, +} + #[derive(Debug, PartialEq, Eq)] pub struct ProtectionDomain { /// Only populated for child protection domains pub id: Option, pub name: String, - pub priority: u8, - pub budget: u64, - pub period: u64, + pub sched_params: SchedulingParams, pub passive: bool, pub stack_size: u64, pub smc: bool, @@ -338,9 +343,7 @@ pub struct VirtualMachine { pub vcpus: Vec, pub name: String, pub maps: Vec, - pub priority: u8, - pub budget: u64, - pub period: u64, + pub sched_params: SchedulingParams, } #[derive(Debug, PartialEq, Eq)] @@ -498,6 +501,10 @@ impl ProtectionDomain { ioports } + pub fn priority(&self) -> u8 { + self.sched_params.priority + } + fn from_xml( config: &Config, xml_sdf: &XmlSystemDescription, @@ -1204,11 +1211,13 @@ impl ProtectionDomain { Ok(ProtectionDomain { id, name, - // This downcast is safe as we have checked that this is less than - // the maximum PD priority, which fits in a u8. - priority: priority as u8, - budget, - period, + sched_params: SchedulingParams { + // This downcast is safe as we have checked that this is less than + // the maximum PD priority, which fits in a u8. + priority: priority as u8, + budget, + period, + }, passive, stack_size, smc, @@ -1352,11 +1361,13 @@ impl VirtualMachine { vcpus, name, maps, - // This downcast is safe as we have checked that this is less than - // the maximum VM priority, which fits in a u8. - priority: priority as u8, - budget, - period, + sched_params: SchedulingParams { + // This downcast is safe as we have checked that this is less than + // the maximum PD priority, which fits in a u8. + priority: priority as u8, + budget, + period, + }, }) } } @@ -2211,17 +2222,23 @@ pub fn parse( let pd_a = &pds[ch.end_a.pd]; let pd_b = &pds[ch.end_b.pd]; - if ch.end_a.pp && pd_a.priority >= pd_b.priority { + if ch.end_a.pp && pd_a.priority() >= pd_b.priority() { return Err(format!( "Error: PPCs must be to protection domains of strictly higher priorities; \ channel with PPC exists from pd {} (priority: {}) to pd {} (priority: {})", - pd_a.name, pd_a.priority, pd_b.name, pd_b.priority + pd_a.name, + pd_a.priority(), + pd_b.name, + pd_b.priority() )); - } else if ch.end_b.pp && pd_b.priority >= pd_a.priority { + } else if ch.end_b.pp && pd_b.priority() >= pd_a.priority() { return Err(format!( "Error: PPCs must be to protection domains of strictly higher priorities; \ channel with PPC exists from pd {} (priority: {}) to pd {} (priority: {})", - pd_b.name, pd_b.priority, pd_a.name, pd_a.priority + pd_b.name, + pd_b.priority(), + pd_a.name, + pd_a.priority() )); } diff --git a/tool/microkit/src/viper.rs b/tool/microkit/src/viper.rs index bc220f4da..3d459e1cd 100644 --- a/tool/microkit/src/viper.rs +++ b/tool/microkit/src/viper.rs @@ -207,8 +207,8 @@ pub fn get_sdf_view(system: &SystemDescription, current_pd: usize) -> Option Date: Mon, 13 Jul 2026 10:47:26 +1000 Subject: [PATCH 3/4] tool: a VM on x86-64 cannot have scheduling params This is because on x86-64, the VM shares TCB with the parent PD (VMM). Rather than being distinct entities like on ARM. Signed-off-by: Bill Nguyen --- docs/manual.md | 6 ++- tool/microkit/src/capdl/builder.rs | 8 ++-- tool/microkit/src/sdf.rs | 73 +++++++++++++++++------------- 3 files changed, 51 insertions(+), 36 deletions(-) diff --git a/docs/manual.md b/docs/manual.md index 53717e867..269df81bd 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -1013,13 +1013,17 @@ The `protection_domain` element has the same attributes as any other protection On x86-64, a PD with a VCPU cannot have child PDs. -The `virtual_machine` element has the following attributes: +The `virtual_machine` element has the following attribute: * `name`: A unique name for the virtual machine + +On ARM, it supports the following additional attributes: * `priority`: (optional) The priority of the virtual machine (integer 0 to 254); defaults to 0. * `budget`: (optional) The VM's budget in microseconds; defaults to 1,000. * `period`: (optional) The VM's period in microseconds; must not be smaller than the budget; defaults to the budget. +On x86-64, the VM shares its scheduling parameters with the parent PD. + Additionally, it supports the following child elements: * `vcpu`: (one or more) Describes the virtual CPU that will be tied to the virtual machine. diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 4fca52eb5..3763a5a26 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -955,8 +955,8 @@ pub fn build_capdl_spec( &mut spec_container, &format!("{}_{}", virtual_machine.name, vcpu.id), PD_SCHEDCONTEXT_EXTRA_SIZE_BITS as u8, - virtual_machine.sched_params.period, - virtual_machine.sched_params.budget, + virtual_machine.sched_params.as_ref().unwrap().period, + virtual_machine.sched_params.as_ref().unwrap().budget, 0x100 + vcpu_idx as u64, ); caps_to_bind_to_vm_tcbs.push(capdl_util_make_cte( @@ -982,8 +982,8 @@ pub fn build_capdl_spec( extra: Box::new(object::TcbExtraInfo { ipc_buffer_addr: Word(0), affinity: Word(vcpu_affinity.0.into()), - prio: virtual_machine.sched_params.priority, - max_prio: virtual_machine.sched_params.priority, + prio: virtual_machine.sched_params.as_ref().unwrap().priority, + max_prio: virtual_machine.sched_params.as_ref().unwrap().priority, // Given the use cases of VMs, for now we always give them FPU access. fpu_disabled: false, resume: false, diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index d347b0744..6a6488590 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -343,7 +343,7 @@ pub struct VirtualMachine { pub vcpus: Vec, pub name: String, pub maps: Vec, - pub sched_params: SchedulingParams, + pub sched_params: Option, } #[derive(Debug, PartialEq, Eq)] @@ -1246,33 +1246,50 @@ impl VirtualMachine { xml_sdf: &XmlSystemDescription, node: &roxmltree::Node, ) -> Result { - check_attributes(xml_sdf, node, &["name", "budget", "period", "priority"])?; - - let name = checked_lookup(xml_sdf, node, "name")?.to_string(); - // If we do not have an explicit budget the period is equal to the default budget. - let budget = if let Some(xml_budget) = node.attribute("budget") { - sdf_parse_number(xml_budget, node)? + if config.arch == Arch::Aarch64 { + check_attributes(xml_sdf, node, &["name", "budget", "period", "priority"])?; } else { - BUDGET_DEFAULT - }; - let period = if let Some(xml_period) = node.attribute("period") { - sdf_parse_number(xml_period, node)? - } else { - budget - }; - if budget > period { - return Err(value_error( - xml_sdf, - node, - format!("budget ({budget}) must be less than, or equal to, period ({period})"), - )); + check_attributes(xml_sdf, node, &["name"])?; } - // Default to minimum priority - let priority = if let Some(xml_priority) = node.attribute("priority") { - sdf_parse_number(xml_priority, node)? + let name = checked_lookup(xml_sdf, node, "name")?.to_string(); + + let sched_params = if config.arch == Arch::Aarch64 { + // If we do not have an explicit budget the period is equal to the default budget. + let budget = if let Some(xml_budget) = node.attribute("budget") { + sdf_parse_number(xml_budget, node)? + } else { + BUDGET_DEFAULT + }; + let period = if let Some(xml_period) = node.attribute("period") { + sdf_parse_number(xml_period, node)? + } else { + budget + }; + if budget > period { + return Err(value_error( + xml_sdf, + node, + format!("budget ({budget}) must be less than, or equal to, period ({period})"), + )); + } + + // Default to minimum priority + let priority = if let Some(xml_priority) = node.attribute("priority") { + sdf_parse_number(xml_priority, node)? + } else { + 0 + }; + + Some(SchedulingParams { + // This downcast is safe as we have checked that this is less than + // the maximum PD priority, which fits in a u8. + priority: priority as u8, + budget, + period, + }) } else { - 0 + None }; let mut vcpus: Vec = Vec::new(); @@ -1361,13 +1378,7 @@ impl VirtualMachine { vcpus, name, maps, - sched_params: SchedulingParams { - // This downcast is safe as we have checked that this is less than - // the maximum PD priority, which fits in a u8. - priority: priority as u8, - budget, - period, - }, + sched_params, }) } } From 58b2eab8f79e3cc246a2bdc62201ff0a125a2a3f Mon Sep 17 00:00:00 2001 From: Bill Nguyen Date: Mon, 13 Jul 2026 11:00:28 +1000 Subject: [PATCH 4/4] tool: add tests for virtual machine Add tests for valid and invalid VM scenarios. Signed-off-by: Bill Nguyen --- tool/microkit/tests/sdf/vm_valid.system | 13 ++++++++++ .../tests/sdf/vm_with_priority.system | 13 ++++++++++ tool/microkit/tests/test.rs | 24 +++++++++++++++++++ 3 files changed, 50 insertions(+) create mode 100644 tool/microkit/tests/sdf/vm_valid.system create mode 100644 tool/microkit/tests/sdf/vm_with_priority.system diff --git a/tool/microkit/tests/sdf/vm_valid.system b/tool/microkit/tests/sdf/vm_valid.system new file mode 100644 index 000000000..f93fb575e --- /dev/null +++ b/tool/microkit/tests/sdf/vm_valid.system @@ -0,0 +1,13 @@ + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/vm_with_priority.system b/tool/microkit/tests/sdf/vm_with_priority.system new file mode 100644 index 000000000..e7e997fac --- /dev/null +++ b/tool/microkit/tests/sdf/vm_with_priority.system @@ -0,0 +1,13 @@ + + + + + + + + + + diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 3328d23d9..bbd48de81 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -751,6 +751,30 @@ mod protection_domain { mod virtual_machine { use super::*; + #[test] + fn test_vm_valid_aarch64() { + check_success(&DEFAULT_AARCH64_KERNEL_CONFIG, "vm_valid.system") + } + + #[test] + fn test_vm_with_priority_aarch64() { + check_success(&DEFAULT_AARCH64_KERNEL_CONFIG, "vm_with_priority.system") + } + + #[test] + fn test_vm_valid_x86_64() { + check_success(&DEFAULT_X86_64_KERNEL_CONFIG, "vm_valid.system") + } + + #[test] + fn test_vm_with_priority_x86_64() { + check_error( + &DEFAULT_X86_64_KERNEL_CONFIG, + "vm_with_priority.system", + "Error: invalid attribute 'priority' on element 'virtual_machine'", + ) + } + #[test] fn test_vm_not_child() { check_error(